Skip to content

Commit dcdaf72

Browse files
oskgooskgo
committed
document proc upto bad
1 parent 4f5d01d commit dcdaf72

File tree

13 files changed

+140
-52
lines changed

13 files changed

+140
-52
lines changed

‎tactics/hl/proc-I.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# Syntax
2+
`proc I` where `I` is a logical statement possibly involving program variables.
3+
# Overview
4+
Proves the goal using the invariant `I` that must hold throughout the procedure
5+
# Current Goal
6+
`hoare[M(O,...).p: P ==> Q]`
7+
# Additional Requirements
8+
- `M` has to be abstract
9+
- The globals of any module mentioned in `I` have to be inaccessible to `M`
10+
# New goals
11+
- `forall &hr, P{hr} => I{hr}`
12+
- `forall &hr, I{hr} => Q{hr}`
13+
and one goal for each oracle procedure `O.q` available to `M` of the form
14+
- `hoare[O.q: I ==> I]`

‎tactics/hl/proc-star.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# Syntax
2+
`proc*`
3+
# Overview
4+
Replaces a goal with a hoare statement involving a procedure with hoare statement with a call to that procedure.
5+
# Current Goal
6+
`hoare[M.p: P ==> Q]`
7+
# New goal
8+
`hoare[{r <- M.p(x,y,...); return r;}: P[arg\(x,y,...)] ==> Q[res\r]]`

‎tactics/hl/proc.md‎

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1+
# Syntax
2+
`proc`
13
# Overview
2-
3-
All variants work to break down goals of the form `hoare[M.p : C ==> R]` where `M` is some module with a procedure `p`.
4-
5-
# Variants
6-
7-
`proc*.`: Replaces `M.p` with a procedure call to `M.p` assigning to a fresh variable. Occurences of `res` in the postcondition are replaced with the fresh variable. Occurrences of `arg` in the postcondition are replaced with the arguments to the procedure.
8-
9-
## Concrete module
10-
11-
`proc.`: Expands `M.p` into its body. This requires `M` to be concrete. Occurrences of `arg` in the precondition are replaced with the arguments to the procedure. Occurences of `res` in the postcondition are replaced with the expression in the return.
12-
13-
## Module parameters
14-
15-
`proc I`: Proves the goal using the invariant `I`. Produces goals stating that the precondition implies the invariant, that the invariant implies the postcondition, and that the invariant is preserved by any procedure calls `M` could make through the module parameters it's given. Requires `M` to be abstract.
4+
Replaces a goal with a hoare statement involving a procedure with its body
5+
# Current Goal
6+
`hoare[M.p: P ==> Q]`
7+
# Additional Requirements
8+
`M` has to be concrete
9+
# New goal
10+
`hoare[{...}: P ==> Q]` where the ellipses are the body of `M.p`

‎tactics/phl/proc-I.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
# Syntax
2+
`proc I`, where `I` is a logical statement possibly involving program variables.
3+
# Overview
4+
Proves the goal using the invariant `I` that must hold throughout the procedure
5+
# Current Goal
6+
`phoare[M(O,...).p: P ==> Q] = 1%r`
7+
# Additional Requirements
8+
- `M` has to be abstract
9+
- The globals of any module mentioned in `I` have to be inaccessible to `M`
10+
- The globals of any module parameter to `M` that are accessed by any procedure available to `M` have to be inaccessible to `M`
11+
# New goals
12+
- `forall &hr, P{hr} => I{hr}`
13+
- `forall &hr, I{hr} => Q{hr}`
14+
- For any module parameters of `M`, losslessness of all procedures available to `M` through its module parameters implies losslessness of `M`
15+
and one goal for each oracle procedure `O.q` available to `M` of the form
16+
- `phoare[O.q: I ==> I] = 1%r`

‎tactics/phl/proc-star.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# Syntax
2+
`proc*`
3+
# Overview
4+
Replaces a goal with a phoare statement involving a procedure with phoare statement with a call to that procedure.
5+
# Current Goal
6+
`phoare[M.p: P ==> Q] o a`, where `o` is one of `>=`, `=` or `<=`
7+
# New goal
8+
`phoare[{r <- M.p(x,y,...); return r;}: P[arg\(x,y,...)] ==> Q[res\r]] o a`

‎tactics/phl/proc.md‎

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,10 @@
1+
# Syntax
2+
`proc`
13
# Overview
2-
3-
All variants work to break down goals of the form `phoare[M.p : C ==> R] o r` where `M` is some module with a procedure `p`, `o` is one of the strings `<=`, `>=` or `=`, and `r` is a real number.
4-
5-
# Variants
6-
7-
`proc*.`: Replaces `M.p` with a procedure call to `M.p` assigning to a fresh variable. Occurences of `res` in the postcondition are replaced with the fresh variable. Occurrences of `arg` in the postcondition are replaced with the arguments to the procedure.
8-
9-
## Concrete module
10-
11-
`proc.`: Expands `M.p` into its body. This requires `M` to be concrete. Occurrences of `arg` in the precondition are replaced with the arguments to the procedure. Occurences of `res` in the postcondition are replaced with the expression in the return.
12-
13-
## Module parameters
14-
15-
`proc I`: Proves the goal using the invariant `I`. Produces goals stating that the precondition implies the invariant, that the invariant implies the postcondition, that `M.p` is lossless assuming all the procedure calls `M` could make through the module parameters it's given are also lossless, and that all those procedure calls losslessly preserve the invariant. Requires `M` to be abstract, the `o` to be `=` and `r` to be `1%r`. We also require `M` to not have direct access to globals of any modules mentioned in `I`. Finally, for any module parameters of `M`, if they may have globals that are accessible by `M` and are accessed by its procedures callable by `M` we require `M` to not have direct access to the globals of this module parameter.
4+
Replaces a goal with a hoare statement involving a procedure with its body
5+
# Current Goal
6+
`phoare[M.p: P ==> Q] o a`, where `o` is one of `>=`, `=` or `<=`.
7+
# Additional Requirements
8+
`M` has to be concrete
9+
# New goal
10+
`phoare[{...}: P ==> Q]` where the ellipses are the body of `M.p`

‎tactics/prhl/proc-B-I-J.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Syntax
2+
`proc B I J`, where `B`, `I` and `J` are logical statements possibly involving program variables where those in `I` and `J` have a side parameter and those in `B` do not.
3+
# Overview
4+
Proves the goal using the invariant `I` that must hold until the bad event `B` happens on the right side. This is a generalization of `proc B I` where a new invariant `J` holds after the bad event happens
5+
# Current Goal
6+
`equiv[M(O1,...).p ~ M(P1,...).p: P ==> Q]`
7+
# Additional Requirements
8+
- `M` has to be abstract
9+
- The globals of any module mentioned in `I`, `B` or `J` have to be inaccessible to `M`
10+
- The globals of any module parameter to `M` that are accessed by any procedure available to `M` on the right side have to be inaccessible to `M`
11+
# New goals
12+
- `forall &1 &2, P{1,2} => if B{2} then J else ={arg} /\ ={glob M} /\ I{1,2}`
13+
- `forall &1 &2, (if B{2} then J else ={arg} /\ ={glob M} /\ I{1,2}) => Q{1,2}`
14+
- For any module parameters of `M`, losslessness of all procedures available to `M` through its module parameters implies losslessness of `M`
15+
one goal for each oracle procedure `O1.q` available to `M` and corresponding `P1.q` on the other side of the form
16+
- `equiv[O1.q ~ P1.q: if B{2} then J else ={arg} /\ ={glob M} /\ I ==> if B{2} then J else ={res} /\ ={glob M} /\ I]`
17+
one goal for each oracle procedure `O1.q` available to `M` on the left side of the form
18+
- `forall &hr, B{hr} => phoare[O1.q: J{_,hr} ==> J{_,hr}]`
19+
one goal for each oracle procedure `P1.q` available to `M` on the right side of the form
20+
- `forall &hr, phoare[P1.q: B /\ J{hr,_} ==> B /\ J{hr,_}] = 1%r`

‎tactics/prhl/proc-B-I.md‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
# Syntax
2+
`proc B I`, where `B` and `I` are logical statements possibly involving program variables where those in `I` have a side parameter and those in `B` do not.
3+
# Overview
4+
Proves the goal using the invariant `I` that must hold until the bad event `B` happens on the right side. This is a specialization of `proc B I` for `J = true`
5+
# Current Goal
6+
`equiv[M(O1,...).p ~ M(P1,...).p: P ==> Q]`
7+
# Additional Requirements
8+
- `M` has to be abstract
9+
- The globals of any module mentioned in `I` have to be inaccessible to `M`
10+
- The globals of any module parameter to `M` that are accessed by any procedure available to `M` on the right side have to be inaccessible to `M`
11+
# New goals
12+
- `forall &1 &2, P{1,2} => !B{2} => ={arg} /\ ={glob M} /\ I{1,2}`
13+
- `forall &1 &2, (!B{2} => ={arg} /\ ={glob M} /\ I{1,2}) => Q{1,2}`
14+
- For any module parameters of `M`, losslessness of all procedures available to `M` through its module parameters implies losslessness of `M`
15+
one goal for each oracle procedure `O1.q` available to `M` and corresponding `P1.q` on the other side of the form
16+
- `equiv[O1.q ~ P1.q: !B{2} /\ ={arg} /\ ={glob M} /\ I ==> !B{2} => ={res} /\ ={glob M} /\ I]`
17+
one goal for each oracle procedure `O1.q` available to `M` on the left side of the form
18+
- `forall &2, B{2} => islossless O1.q`
19+
one goal for each oracle procedure `P1.q` available to `M` on the right side of the form
20+
- `forall _, phoare[P1.q: B /\ true ==> B /\ true] = 1%r`
21+
Note: *Maybe this goal should automatically have its quantifier removed and pre- and post-condition simplified?*

‎tactics/prhl/proc-I.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# Syntax
2+
`proc I`, where `I` is a logical statement possibly involving program variables with a side parameter.
3+
# Overview
4+
Proves the goal using the invariant `I` that must hold throughout
5+
# Current Goal
6+
`equiv[M(O1,...).p ~ M(P1,,...).p: P ==> Q]`
7+
# Additional Requirements
8+
- `M` has to be abstract
9+
- The globals of any module mentioned in `I` have to be inaccessible to `M`
10+
# New goals
11+
- `forall &1 &2, P{1,2} => ={arg} /\ ={glob M} /\ I{1,2}`
12+
- `forall &1 &2, ={arg} /\ ={glob M} /\ I{1,2} => Q{1,2}`
13+
and one goal for each oracle procedure `O1.q` available to `M` and corresponding `P1.q` on the other side of the form
14+
- `equiv[O1.q ~ P1.q: ={arg} /\ ={glob M} /\ I ==> ={res} /\ ={glob M} /\ I]`

‎tactics/prhl/proc-star.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
# Syntax
2+
`proc*`
3+
# Overview
4+
Replaces a goal with an equiv statement involving procedures with an equiv involving calls to those procedures.
5+
# Current Goal
6+
`equiv[M1.p ~ M2.q: P ==> Q]`
7+
# New goal
8+
`phoare[{r <- M1.p(x,y,...)} ~ {r <- M2.p(x,y,...)}: P ==> Q]`

0 commit comments

Comments
 (0)