[Tactic] Rewrite Equiv

Rewrite Equiv

Syntax

rewrite equiv [{s} L argsl resl argsr resr] where:

• s is either 1 or 2 indicating the direction L will be applied.
• L is a lemma proving equiv[M.f ~ M.g: P ==> Q]
• argsl(/argsr) is a tuple of arguments that M.f(/M.g) receives.
• resl(/resr) is a variable that M.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.

Operation

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 four subgoals:

• Two trivial subgoals, one for each side, P implies conjunction of P and the existence of variables for copied memory.
• 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 where inline *; auto. will not prove equivalence between the two programs.
• Same as above but for B, and resr <@ M.f(argsr); using {2} sided formulae.

Example

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 three subgoals

Current goal (remaining: 3)

Type variables: <none>

------------------------------------------------------------------------
forall &1 &2,
  b{2} = true /\ x{2} = 2 /\ z{2} = 1 /\ s{1} = true /\ x{1} = 1 =>
  exists (s0 : bool) (x0 y0 : int),
   (s{1} = s0 /\
    x{1} = x0 /\
    y{1} = y0 /\ x{1} = x0 /\ (s{1} = true /\ x{1} = 1) /\ s{1} = s0) /\
    b{2} = true /\ x{2} = 2 /\ z{2} = 1 /\ s0 = true /\ x0 = 1

Which discharges with by move=> &1 &2 P; exists s{1} x{1} y{1}; move: P..

Current goal (remaining: 2)

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 by sim..

Current goal

Type variables: <none>

------------------------------------------------------------------------
forall &1 &2,
  b{2} = true /\ x{2} = 2 /\ z{2} = 1 /\ s{1} = true /\ x{1} = 1 =>
  exists (b0 : bool) (x0 y0 z0 : int),
    (b0 = true /\ x0 = 2 /\ z0 = 1 /\ s{1} = true /\ x{1} = 1) /\
    b{2} = b0 /\
    x{2} = x0 /\
    z{2} = z0 /\
    y{2} = y0 /\
    x{2} = x0 /\
    z{2} = z0 /\ (b{2} = true /\ x{2} = 2 /\ z{2} = 1) /\ b{2} = b0

Which discharges with by move=> &1 &2 P; exists b{2} x{2} y{2} z{2}; move: P..