From 7bc6fdbb6d3533f5e958b47618e3e9a0fecc7583 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Tue, 4 Feb 2025 17:40:44 +0000
Subject: [PATCH 1/2] everything except upto bad

---
 tactics/hl/proc.md                      | 15 ++++++++++++++
 tactics/phl/proc.md                     | 15 ++++++++++++++
 tactics/prhl/proc.md                    | 21 +++++++++++++++++++
 units/hl/proc-I.ec                      | 14 +++++++++++++
 units/hl/proc-star.ec                   | 10 +++++++++
 units/{proc-hoare.ec => hl/proc.ec}     |  0
 units/{while-hoare.ec => hl/while.ec}   |  0
 units/{wp-hoare.ec => hl/wp.ec}         |  0
 units/phl/proc-I.ec                     | 23 +++++++++++++++++++++
 units/phl/proc-star.ec                  | 10 +++++++++
 units/phl/proc.ec                       | 19 +++++++++++++++++
 units/{while-phoare.ec => phl/while.ec} |  0
 units/prhl/proc-B-I.ec                  | 15 ++++++++++++++
 units/prhl/proc-I.ec                    | 15 ++++++++++++++
 units/prhl/proc-star.ec                 | 14 +++++++++++++
 units/prhl/proc.ec                      | 27 +++++++++++++++++++++++++
 16 files changed, 198 insertions(+)
 create mode 100644 tactics/hl/proc.md
 create mode 100644 tactics/phl/proc.md
 create mode 100644 tactics/prhl/proc.md
 create mode 100644 units/hl/proc-I.ec
 create mode 100644 units/hl/proc-star.ec
 rename units/{proc-hoare.ec => hl/proc.ec} (100%)
 rename units/{while-hoare.ec => hl/while.ec} (100%)
 rename units/{wp-hoare.ec => hl/wp.ec} (100%)
 create mode 100644 units/phl/proc-I.ec
 create mode 100644 units/phl/proc-star.ec
 create mode 100644 units/phl/proc.ec
 rename units/{while-phoare.ec => phl/while.ec} (100%)
 create mode 100644 units/prhl/proc-B-I.ec
 create mode 100644 units/prhl/proc-I.ec
 create mode 100644 units/prhl/proc-star.ec
 create mode 100644 units/prhl/proc.ec

diff --git a/tactics/hl/proc.md b/tactics/hl/proc.md
new file mode 100644
index 0000000..21ee55a
--- /dev/null
+++ b/tactics/hl/proc.md
@@ -0,0 +1,15 @@
+# Overview
+
+All variants work to break down goals of the form `hoare[M.p : C ==> R]` where `M` is some module with a procedure `p`.
+
+# Variants
+
+`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.
+
+## Concrete module
+
+`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.
+
+## Module parameters
+
+`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.
\ No newline at end of file
diff --git a/tactics/phl/proc.md b/tactics/phl/proc.md
new file mode 100644
index 0000000..27c222c
--- /dev/null
+++ b/tactics/phl/proc.md
@@ -0,0 +1,15 @@
+# Overview
+
+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.
+
+# Variants
+
+`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.
+
+## Concrete module
+
+`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. 
+
+## Module parameters
+
+`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.
\ No newline at end of file
diff --git a/tactics/prhl/proc.md b/tactics/prhl/proc.md
new file mode 100644
index 0000000..84b3547
--- /dev/null
+++ b/tactics/prhl/proc.md
@@ -0,0 +1,21 @@
+# Overview
+
+All variants work to break down goals of the form `equiv[M1.p ~ M2.q: C ==> R] o r` where `M1` and `M2` are modules with procedures `p` and `q` respectively.
+
+# Variants
+
+`proc*.`: Replaces `M1.p` and `M2.p` with a procedure call to them assigning to fresh variables. Occurences of `res{i}` in the postcondition are replaced with the fresh variable on side `i`. Occurrences of `arg{i}` in the precondition are replaced with the arguments to the procedure.
+
+## Concrete Module
+
+`proc.`: Expands `M1.p` and `M2.q` into their body. This requires `M1` and `M2` to be concrete. Occurrences of `arg{i}` in the postcondition are replaced with the arguments to the procedure on side `i`. Occurences of `res{i}` in the precondition are replaced with the expression in the return of the procedure on side `i`.
+
+## Module Parameters
+
+`proc I`: Requires `M1` and `M2` to be the same. Proves the goal using the invariant `I`. Produces goals stating that the precondition implies the invariant, that the invariant implies the postcondition, and that all for any corresponding pair of procedure calls, `O1.p` and `O2.p` available through procedure calls to `M1` and `M2` respectively we have `equiv[M1 ~ M2: ={arg} /\ I ==> ={res} /\ I]`. We also require `M1` (and thus also `M2`) to not have direct access to globals of any modules mentioned in `I`.
+
+## Module Parameters upto bad
+
+`proc B I J`. Like proc I, but just for pRHL judgements and uses “upto-bad” (upto-failure) reasoning, where the bad (failure) event, B, is evaluated in the second program’s memory, and the invariant I only holds up to the point when failure occurs. In addition to subgoals whose conclusions are pRHL judgments involving the oracles the abstract procedure may query (their preconditions assume I and the equality of oracles’ parameters, as well as that B is false; their postconditions assert I and the equality of the oracles’ results—but only when B does not hold), subgoals are generated that check that: the original judgement’s pre- and postconditions support the reduction; the abstract procedure is lossless, assuming the losslessness of the oracles it may query; the oracles used by the abstract procedure in the first program are lossless once the bad event occurs; and the oracles used by the abstract procedure in the second program guarantee the stability of the failure event with probability 1.
+
+`proc B I` Same as `proc B I `
\ No newline at end of file
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..395c18d
--- /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 (false) (3=3). admit. admit.
+abort.
diff --git a/units/prhl/proc-I.ec b/units/prhl/proc-I.ec
new file mode 100644
index 0000000..3a92a19
--- /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{-O1}): 
+  equiv[M(O1).f ~M(O2).f: 0 < x{1} ==> 0 = res{2}].
+proof.
+proc (={glob O1}).
+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.

From c02360bb3b21fa65c17ed49832870f3275107558 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Thu, 6 Feb 2025 15:03:16 +0000
Subject: [PATCH 2/2] document proc upto bad

---
 tactics/hl/proc-I.md       | 14 ++++++++++++++
 tactics/hl/proc-star.md    |  8 ++++++++
 tactics/hl/proc.md         | 23 +++++++++--------------
 tactics/phl/proc-I.md      | 16 ++++++++++++++++
 tactics/phl/proc-star.md   |  8 ++++++++
 tactics/phl/proc.md        | 23 +++++++++--------------
 tactics/prhl/proc-B-I-J.md | 20 ++++++++++++++++++++
 tactics/prhl/proc-B-I.md   | 21 +++++++++++++++++++++
 tactics/prhl/proc-I.md     | 14 ++++++++++++++
 tactics/prhl/proc-star.md  |  8 ++++++++
 tactics/prhl/proc.md       | 29 +++++++++--------------------
 units/prhl/proc-B-I.ec     |  4 ++--
 units/prhl/proc-I.ec       |  4 ++--
 13 files changed, 140 insertions(+), 52 deletions(-)
 create mode 100644 tactics/hl/proc-I.md
 create mode 100644 tactics/hl/proc-star.md
 create mode 100644 tactics/phl/proc-I.md
 create mode 100644 tactics/phl/proc-star.md
 create mode 100644 tactics/prhl/proc-B-I-J.md
 create mode 100644 tactics/prhl/proc-B-I.md
 create mode 100644 tactics/prhl/proc-I.md
 create mode 100644 tactics/prhl/proc-star.md

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
index 21ee55a..8d34004 100644
--- a/tactics/hl/proc.md
+++ b/tactics/hl/proc.md
@@ -1,15 +1,10 @@
+# Syntax
+`proc`
 # Overview
-
-All variants work to break down goals of the form `hoare[M.p : C ==> R]` where `M` is some module with a procedure `p`.
-
-# Variants
-
-`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.
-
-## Concrete module
-
-`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.
-
-## Module parameters
-
-`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.
\ No newline at end of file
+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
index 27c222c..fab692e 100644
--- a/tactics/phl/proc.md
+++ b/tactics/phl/proc.md
@@ -1,15 +1,10 @@
+# Syntax
+`proc`
 # Overview
-
-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.
-
-# Variants
-
-`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.
-
-## Concrete module
-
-`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. 
-
-## Module parameters
-
-`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.
\ No newline at end of file
+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
index 84b3547..3d6cc6b 100644
--- a/tactics/prhl/proc.md
+++ b/tactics/prhl/proc.md
@@ -1,21 +1,10 @@
+# Syntax
+`proc`
 # Overview
-
-All variants work to break down goals of the form `equiv[M1.p ~ M2.q: C ==> R] o r` where `M1` and `M2` are modules with procedures `p` and `q` respectively.
-
-# Variants
-
-`proc*.`: Replaces `M1.p` and `M2.p` with a procedure call to them assigning to fresh variables. Occurences of `res{i}` in the postcondition are replaced with the fresh variable on side `i`. Occurrences of `arg{i}` in the precondition are replaced with the arguments to the procedure.
-
-## Concrete Module
-
-`proc.`: Expands `M1.p` and `M2.q` into their body. This requires `M1` and `M2` to be concrete. Occurrences of `arg{i}` in the postcondition are replaced with the arguments to the procedure on side `i`. Occurences of `res{i}` in the precondition are replaced with the expression in the return of the procedure on side `i`.
-
-## Module Parameters
-
-`proc I`: Requires `M1` and `M2` to be the same. Proves the goal using the invariant `I`. Produces goals stating that the precondition implies the invariant, that the invariant implies the postcondition, and that all for any corresponding pair of procedure calls, `O1.p` and `O2.p` available through procedure calls to `M1` and `M2` respectively we have `equiv[M1 ~ M2: ={arg} /\ I ==> ={res} /\ I]`. We also require `M1` (and thus also `M2`) to not have direct access to globals of any modules mentioned in `I`.
-
-## Module Parameters upto bad
-
-`proc B I J`. Like proc I, but just for pRHL judgements and uses “upto-bad” (upto-failure) reasoning, where the bad (failure) event, B, is evaluated in the second program’s memory, and the invariant I only holds up to the point when failure occurs. In addition to subgoals whose conclusions are pRHL judgments involving the oracles the abstract procedure may query (their preconditions assume I and the equality of oracles’ parameters, as well as that B is false; their postconditions assert I and the equality of the oracles’ results—but only when B does not hold), subgoals are generated that check that: the original judgement’s pre- and postconditions support the reduction; the abstract procedure is lossless, assuming the losslessness of the oracles it may query; the oracles used by the abstract procedure in the first program are lossless once the bad event occurs; and the oracles used by the abstract procedure in the second program guarantee the stability of the failure event with probability 1.
-
-`proc B I` Same as `proc B I `
\ No newline at end of file
+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/prhl/proc-B-I.ec b/units/prhl/proc-B-I.ec
index 395c18d..d7f4b1c 100644
--- a/units/prhl/proc-B-I.ec
+++ b/units/prhl/proc-B-I.ec
@@ -10,6 +10,6 @@ module type MT(O: OT) = {
 
 lemma L (O1<:OT) (O2<:OT) (M<: MT{-O1}): 
   equiv[M(O1).f ~M(O2).f: 0 < x{1} ==> 0 = res{2}].
-proof.
-proc (false) (3=3). admit. admit.
+proof. 
+proc (glob O1=witness) (={glob O1}).
 abort.
diff --git a/units/prhl/proc-I.ec b/units/prhl/proc-I.ec
index 3a92a19..a8cc7e1 100644
--- a/units/prhl/proc-I.ec
+++ b/units/prhl/proc-I.ec
@@ -8,8 +8,8 @@ module type MT(O: OT) = {
   proc f(x : int) : int
 }.
 
-lemma L (O1<:OT) (O2<:OT) (M<: MT{-O1}): 
+lemma L (O1<:OT) (O2<:OT) (M<: MT): 
   equiv[M(O1).f ~M(O2).f: 0 < x{1} ==> 0 = res{2}].
 proof.
-proc (={glob O1}).
+proc (1=1).
 abort.