Document proc

tactics/hl/proc-I.md

@@ -0,0 +1,14 @@
+# Syntax
+`proc I` where `I` is a logical statement possibly involving program variables.
+# Overview
+Proves the goal using the invariant `I` that must hold throughout the procedure
+# Current Goal
+`hoare[M(O,...).p: P ==> Q]`
+# Additional Requirements
+- `M` has to be abstract
+- The globals of any module mentioned in `I` have to be inaccessible to `M`
+# New goals
+- `forall &hr, P{hr} => I{hr}`
+- `forall &hr, I{hr} => Q{hr}`
+and one goal for each oracle procedure `O.q` available to `M` of the form
+- `hoare[O.q: I ==> I]`

tactics/hl/proc-star.md

@@ -0,0 +1,8 @@
+# Syntax
+`proc*`
+# Overview
+Replaces a goal with a hoare statement involving a procedure with hoare statement with a call to that procedure.
+# Current Goal
+`hoare[M.p: P ==> Q]`
+# New goal
+`hoare[{r <- M.p(x,y,...); return r;}: P[arg\(x,y,...)] ==> Q[res\r]]`

tactics/hl/proc.md

@@ -0,0 +1,10 @@
+# Syntax
+`proc`
+# Overview
+Replaces a goal with a hoare statement involving a procedure with its body
+# Current Goal
+`hoare[M.p: P ==> Q]`
+# Additional Requirements
+`M` has to be concrete
+# New goal
+`hoare[{...}: P ==> Q]` where the ellipses are the body of `M.p`

tactics/phl/proc-I.md

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

tactics/phl/proc-star.md

@@ -0,0 +1,8 @@
+# Syntax
+`proc*`
+# Overview
+Replaces a goal with a phoare statement involving a procedure with phoare statement with a call to that procedure.
+# Current Goal
+`phoare[M.p: P ==> Q] o a`, where `o` is one of `>=`, `=` or `<=`
+# New goal
+`phoare[{r <- M.p(x,y,...); return r;}: P[arg\(x,y,...)] ==> Q[res\r]] o a`

tactics/phl/proc.md

@@ -0,0 +1,10 @@
+# Syntax
+`proc`
+# Overview
+Replaces a goal with a hoare statement involving a procedure with its body
+# Current Goal
+`phoare[M.p: P ==> Q] o a`, where `o` is one of `>=`, `=` or `<=`.
+# Additional Requirements
+`M` has to be concrete
+# New goal
+`phoare[{...}: P ==> Q]` where the ellipses are the body of `M.p`

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

@@ -0,0 +1,20 @@
+# Syntax
+`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.
+# Overview
+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
+# Current Goal
+`equiv[M(O1,...).p ~ M(P1,...).p: P ==> Q]`
+# Additional Requirements
+- `M` has to be abstract
+- The globals of any module mentioned in `I`, `B` or `J` have to be inaccessible to `M`
+- 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`
+# New goals
+- `forall &1 &2, P{1,2} => if B{2} then J else ={arg} /\ ={glob M} /\ I{1,2}`
+- `forall &1 &2, (if B{2} then J else ={arg} /\ ={glob M} /\ I{1,2}) => Q{1,2}`
+- For any module parameters of `M`, losslessness of all procedures available to `M` through its module parameters implies losslessness of `M`
+one goal for each oracle procedure `O1.q` available to `M` and corresponding `P1.q` on the other side of the form
+- `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]`
+one goal for each oracle procedure `O1.q` available to `M` on the left side of the form
+- `forall &hr, B{hr} => phoare[O1.q: J{_,hr} ==> J{_,hr}]`
+one goal for each oracle procedure `P1.q` available to `M` on the right side of the form
+- `forall &hr, phoare[P1.q: B /\ J{hr,_} ==> B /\ J{hr,_}] = 1%r`

tactics/prhl/proc-B-I.md

@@ -0,0 +1,21 @@
+# Syntax
+`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.
+# Overview
+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`
+# Current Goal
+`equiv[M(O1,...).p ~ M(P1,...).p: P ==> Q]`
+# Additional Requirements
+- `M` has to be abstract
+- The globals of any module mentioned in `I` have to be inaccessible to `M`
+- 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`
+# New goals
+- `forall &1 &2, P{1,2} => !B{2} => ={arg} /\ ={glob M} /\ I{1,2}`
+- `forall &1 &2, (!B{2} => ={arg} /\ ={glob M} /\ I{1,2}) => Q{1,2}`
+- For any module parameters of `M`, losslessness of all procedures available to `M` through its module parameters implies losslessness of `M`
+one goal for each oracle procedure `O1.q` available to `M` and corresponding `P1.q` on the other side of the form
+- `equiv[O1.q ~ P1.q: !B{2} /\ ={arg} /\ ={glob M} /\ I ==> !B{2} => ={res} /\ ={glob M} /\ I]`
+one goal for each oracle procedure `O1.q` available to `M` on the left side of the form
+- `forall &2, B{2} => islossless O1.q`
+one goal for each oracle procedure `P1.q` available to `M` on the right side of the form
+- `forall _, phoare[P1.q: B /\ true ==> B /\ true] = 1%r` 
+Note: *Maybe this goal should automatically have its quantifier removed and pre- and post-condition simplified?*

tactics/prhl/proc-I.md

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

tactics/prhl/proc-star.md

@@ -0,0 +1,8 @@
+# Syntax
+`proc*`
+# Overview
+Replaces a goal with an equiv statement involving procedures with an equiv involving calls to those procedures.
+# Current Goal
+`equiv[M1.p ~ M2.q: P ==> Q]`
+# New goal
+`phoare[{r <- M1.p(x,y,...)} ~ {r <- M2.p(x,y,...)}: P ==> Q]`

tactics/prhl/proc.md

@@ -0,0 +1,10 @@
+# Syntax
+`proc`
+# Overview
+Replaces a goal with an equiv statement involving procedures with their body
+# Current Goal
+`equiv[M1.p ~ M2.q: P ==> Q]`
+# Additional Requirements
+`M1` and `M2` have to be concrete
+# New goal
+`phoare[{...} ~ {...}: P ==> Q]` where the ellipses are the bodies of `M1.p` and `M2.q`

units/hl/proc-I.ec

@@ -0,0 +1,14 @@
+require import AllCore.
+
+module type OT = {
+  proc g(x : int, y : int) : int
+}.
+
+module type MT(O: OT) = {
+  proc f(x : int) : int
+}.
+
+lemma L (O<: OT) (M<: MT) : hoare[M(O).f : 0 < x ==> 0 < res].
+proof.
+proc (1+1=3).
+abort.

units/hl/proc-star.ec

@@ -0,0 +1,10 @@
+require import AllCore.
+
+module type MT = {
+  proc f(x : int): int
+}.
+
+lemma L (M<: MT) : hoare[M.f : 0 < x ==> 0 < 0].
+proof.
+proc*.
+abort.

units/phl/proc-I.ec

@@ -0,0 +1,23 @@
+require import AllCore.
+
+module type OT = {
+  proc g(x : int, y : int) : int
+}.
+
+module type MT(O: OT) = {
+  proc f(x : int) : int
+}.
+
+module O: OT = {
+  var b: bool
+  proc g(x: int, y: int): int = {var r;
+    b <- true;
+    return r;
+  }
+}.
+
+lemma L (M<: MT{-O}) : phoare[M(O).f : 0 < x ==> 0 < res] =
+1%r.
+proof.
+proc (1+1=3).
+abort.

units/phl/proc-star.ec

@@ -0,0 +1,10 @@
+require import AllCore.
+
+module type MT = {
+  proc f(x : int) : int
+}.
+
+lemma L (M<: MT): phoare[M.f : 0 < x ==> 0 < res] <= (1%r/2%r).
+proof.
+proc*.
+abort.

units/phl/proc.ec

@@ -0,0 +1,19 @@
+require import AllCore.
+
+module M = {
+  proc g(x : int, y : int) : int = {
+    return x * y;
+  }
+
+  proc f(x : int) : int = {
+    var aout : int;
+
+    aout <@ g(x, x);
+    return aout;
+  }
+}.
+
+lemma L : phoare[M.f : 0 < x ==> 0 < res] <= (1%r/2%r).
+proof.
+proc.
+abort.

units/prhl/proc-B-I.ec

@@ -0,0 +1,15 @@
+require import AllCore.
+
+module type OT = {
+  proc g(x : int, y : int) : int
+}.
+
+module type MT(O: OT) = {
+  proc f(x : int) : int
+}.
+
+lemma L (O1<:OT) (O2<:OT) (M<: MT{-O1}): 
+  equiv[M(O1).f ~M(O2).f: 0 < x{1} ==> 0 = res{2}].
+proof. 
+proc (glob O1=witness) (={glob O1}).
+abort.

units/prhl/proc-I.ec

@@ -0,0 +1,15 @@
+require import AllCore.
+
+module type OT = {
+  proc g(x : int, y : int) : int
+}.
+
+module type MT(O: OT) = {
+  proc f(x : int) : int
+}.
+
+lemma L (O1<:OT) (O2<:OT) (M<: MT): 
+  equiv[M(O1).f ~M(O2).f: 0 < x{1} ==> 0 = res{2}].
+proof.
+proc (1=1).
+abort.

units/prhl/proc-star.ec

@@ -0,0 +1,14 @@
+require import AllCore.
+
+module type MT1 = {
+  proc f(x : int) : int
+}.
+
+module type MT2 = {
+  proc h(x: bool): bool
+}.
+
+lemma L (M1<: MT1) (M2<:MT2) : equiv[M1.f ~ M2.h : 0 < x{1} ==> res{2}].
+proof.
+proc*.
+abort.

units/prhl/proc.ec

@@ -0,0 +1,27 @@
+require import AllCore.
+
+module M1 = {
+  proc g(x : int, y : int) : int = {
+    return x * y;
+  }
+
+  proc f(x : int) : int = {
+    var aout : int;
+
+    aout <@ g(x, x);
+    return aout;
+  }
+}.
+
+module M2 = {
+  proc h(x: bool): bool = {
+    var bout: bool;
+    bout <- true;
+    return bout;
+  }
+}.
+
+lemma L : equiv[M1.f ~ M2.h : 0 < x{1} ==> res{2}].
+proof.
+proc.
+abort.