-
Notifications
You must be signed in to change notification settings - Fork 47
[Tactic] Rewrite Equiv
rewrite equiv [{s} L argsl resl argsr resr]
where:
-
s
is either 1 or 2 indicating the directionL
will be applied. -
L
is a lemma provingequiv[M.f ~ M.g: P ==> Q]
-
argsl
(/argsr
) is a tuple of arguments thatM.f
(/M.g
) receives. -
resl
(/resr
) is a variable thatM.f
(/M.g
) will return it's value to.
Program variables used in argsl
and resl
will come from {s}
, and argsr
and resr
take from the other memory.
When a goal's conclusion is a pRHL statement judgement, with post condition P and pre condition Q, relating two programs A and B, generate up to two subgoals:
- A pRHL statement judgement between A and
resl <@ M.f(argsl);
with a minimal pre-condition on equality of program variables and all {1} sided formulae from P, and minimal post-condition on equality of program variables. This will be produced in cases whereinline *; auto.
will not prove equivalence between the two programs. - Same as above but for B, and
resr <@ M.f(argsr);
using {2} sided formulae.
Assume we have proved doubleSample
lemma relating the programs M.f
and M.g
shown below.
op dst : int distr.
module M = {
proc f(b: bool) : int = {
var y;
y <$ dst;
if (b) {
y <$ dst;
}
return y;
}
proc g(s: bool): int = {
var a, b;
a <$ dst;
b <$ dst;
return (if s then b else a);
}
}.
equiv doubleSample: M.f ~ M.g: ={arg} ==> ={res}.
Now suppose we wish to prove an equivalence between the following programs,
module N = {
proc foo(): int = {
var s, x, y;
s <- true;
x <- 1;
y <$ dst;
if (s) {
y <$ dst;
}
x <- y + x;
return x;
}
proc bar(): int = {
var b, w, x, y, z;
b <- true;
x <- 2;
z <- 1;
y <$ dst;
w <$ dst;
y <- if b then w else y;
x <- y + x - z;
return x;
}
}.
In other words, after a proc
, we have the goal:
Current goal
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {s : bool, x, y : int}
&2 (right) : {b : bool, w, x, y, z : int}
pre = true
s <- true (1--) b <- true
x <- 1 (2--) x <- 2
y <$ dst (3--) z <- 1
if (s) { (4--) y <$ dst
y <$ dst (4.1)
} (4--)
x <- (5--) w <$ dst
y + x ( -)
(6--) y <-
( -) if b
( -) then
( -) w
( -) else y
(7--) x <-
( -) y + x -
( -) z
post = ={x}
We first isolate the sections corresponding to the programs M.f
and M.g
with sp; wp 2 3
. Giving us,
Current goal
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {s : bool, x, y : int}
&2 (right) : {b : bool, w, x, y, z : int}
pre = b{2} = true /\ x{2} = 2 /\ z{2} = 1 /\ s{1} = true /\ x{1} = 1
y <$ dst (1--) y <$ dst
if (s) { (2--) w <$ dst
y <$ dst (2.1)
} (2--)
(3--) y <-
( -) if b
( -) then
( -) w
( -) else y
post = y{1} + x{1} = y{2} + x{2} - z{2}
Now, we are in a position to call rewrite equiv [{1} doubleSample (s) y (b) y].
. In this case, we receive a single subgoal
Current goal
Type variables: <none>
------------------------------------------------------------------------
&1 (left ) : {s : bool, x, y : int}
&2 (right) : {s, b : bool, x, y, y0 : int}
pre = ={s} /\ ={x} /\ ={y} /\ ={x} /\ (s{1} = true /\ x{1} = 1) /\ ={s}
y <$ dst (1--) b <- s
if (s) { (2--) y0 <$ dst
y <$ dst (2.1)
} (2--)
(3--) if (b) {
(3.1) y0 <$ dst
(3--) }
(4--) y <- y0
post = ={y, x}
Which discharges with sim.
.