diff --git a/tactics/hl/proc-I.md b/tactics/hl/proc-I.md new file mode 100644 index 0000000..850b58d --- /dev/null +++ b/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]` \ No newline at end of file diff --git a/tactics/hl/proc-star.md b/tactics/hl/proc-star.md new file mode 100644 index 0000000..9a4ce70 --- /dev/null +++ b/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]]` diff --git a/tactics/hl/proc.md b/tactics/hl/proc.md new file mode 100644 index 0000000..8d34004 --- /dev/null +++ b/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` diff --git a/tactics/phl/proc-I.md b/tactics/phl/proc-I.md new file mode 100644 index 0000000..19c5d16 --- /dev/null +++ b/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` diff --git a/tactics/phl/proc-star.md b/tactics/phl/proc-star.md new file mode 100644 index 0000000..6c87e3d --- /dev/null +++ b/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` diff --git a/tactics/phl/proc.md b/tactics/phl/proc.md new file mode 100644 index 0000000..fab692e --- /dev/null +++ b/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` diff --git a/tactics/prhl/proc-B-I-J.md b/tactics/prhl/proc-B-I-J.md new file mode 100644 index 0000000..f1d121c --- /dev/null +++ b/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` diff --git a/tactics/prhl/proc-B-I.md b/tactics/prhl/proc-B-I.md new file mode 100644 index 0000000..65f4c40 --- /dev/null +++ b/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?* \ No newline at end of file diff --git a/tactics/prhl/proc-I.md b/tactics/prhl/proc-I.md new file mode 100644 index 0000000..c8c6f4e --- /dev/null +++ b/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]` diff --git a/tactics/prhl/proc-star.md b/tactics/prhl/proc-star.md new file mode 100644 index 0000000..bae6b73 --- /dev/null +++ b/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]` diff --git a/tactics/prhl/proc.md b/tactics/prhl/proc.md new file mode 100644 index 0000000..3d6cc6b --- /dev/null +++ b/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` diff --git a/units/hl/proc-I.ec b/units/hl/proc-I.ec new file mode 100644 index 0000000..93ae847 --- /dev/null +++ b/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. diff --git a/units/hl/proc-star.ec b/units/hl/proc-star.ec new file mode 100644 index 0000000..0b4df20 --- /dev/null +++ b/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. diff --git a/units/proc-hoare.ec b/units/hl/proc.ec similarity index 100% rename from units/proc-hoare.ec rename to units/hl/proc.ec diff --git a/units/while-hoare.ec b/units/hl/while.ec similarity index 100% rename from units/while-hoare.ec rename to units/hl/while.ec diff --git a/units/wp-hoare.ec b/units/hl/wp.ec similarity index 100% rename from units/wp-hoare.ec rename to units/hl/wp.ec diff --git a/units/phl/proc-I.ec b/units/phl/proc-I.ec new file mode 100644 index 0000000..c756e3a --- /dev/null +++ b/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. diff --git a/units/phl/proc-star.ec b/units/phl/proc-star.ec new file mode 100644 index 0000000..6f78757 --- /dev/null +++ b/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. diff --git a/units/phl/proc.ec b/units/phl/proc.ec new file mode 100644 index 0000000..d694d06 --- /dev/null +++ b/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. diff --git a/units/while-phoare.ec b/units/phl/while.ec similarity index 100% rename from units/while-phoare.ec rename to units/phl/while.ec diff --git a/units/prhl/proc-B-I.ec b/units/prhl/proc-B-I.ec new file mode 100644 index 0000000..d7f4b1c --- /dev/null +++ b/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. diff --git a/units/prhl/proc-I.ec b/units/prhl/proc-I.ec new file mode 100644 index 0000000..a8cc7e1 --- /dev/null +++ b/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. diff --git a/units/prhl/proc-star.ec b/units/prhl/proc-star.ec new file mode 100644 index 0000000..be7d728 --- /dev/null +++ b/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. diff --git a/units/prhl/proc.ec b/units/prhl/proc.ec new file mode 100644 index 0000000..50f9d43 --- /dev/null +++ b/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.