[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 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 where inline *; auto. will not prove equivalence between the two programs.
• Same as above but for B, and resr <@ M.g(argsr); using {2} sided formulae.

This gives the appearance of "rewriting" the (inlined) code of M.f into the (inlined) code of M.g.

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