EquivProgram Equivalence

Behavioral Equivalence

In the last chapter, we studied a simple transformation on arithmetic expressions and showed that it was correct in the sense that it preserved the value of the expressions.
To play a similar game with programs involving mutable state, we need a more sophisticated notion of correctness, called behavioral equivalence.

Definitions

For aexps and bexps with variables, the definition we want is clear: Two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.
Definition aequiv (a1 a2 : aexp) : Prop :=
  ∀ (st : state),
    aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
  ∀ (st : state),
    beval st b1 = beval st b2.
Theorem aequiv_example: aequiv <{ X - X }> <{ 0 }>.
Theorem bequiv_example: bequiv <{ X - X = 0 }> <{ true }>.

For commands, we need to deal with the possibility of nontermination.
We do this by defining command equivalence as "if the first one terminates in a particular state then so does the second, and vice versa":
Definition cequiv (c1 c2 : com) : Prop :=
  ∀ (st st' : state),
    (st =[ c1 ]=> st') ↔ (st =[ c2 ]=> st').
Are these two programs equivalent?
    X := 1;
    Y := 2 and
    Y := 2;
    X := 1
(1) Yes
(2) No
(3) Not sure
What about these?

    X := 1;
    Y := 2 and
    X := 2;
    Y := 1
(1) Yes
(2) No
(3) Not sure
What about these?

    while 1 ≤ X do
      X := X + 1
    end and
    while 2 ≤ X do
      X := X + 1
    end
(1) Yes
(2) No
(3) Not sure
These?
    while true do
      while false do X := X + 1 end
    end and
    while false do
      while true do X := X + 1 end
    end
(1) Yes
(2) No
(3) Not sure

Simple Examples

For examples of command equivalence, let's start by looking at some trivial program transformations involving skip:
Theorem skip_left : ∀ c,
  cequiv
    <{ skip; c }>
    c.
Proof.
  (* WORK IN CLASS *) Admitted.

Similarly, here is a simple transformation that optimizes if commands:
Theorem if_true_simple : ∀ c1 c2,
  cequiv
    <{ if true then c1 else c2 end }>
    c1.

Of course, no (human) programmer would write a conditional whose guard is literally true. But they might write one whose guard is equivalent to true:
Theorem if_true: ∀ b c1 c2,
  bequiv b <{true}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c1.
Similarly:
Theorem if_false : ∀ b c1 c2,
  bequiv b <{false}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c2.

For while loops, we can give a similar pair of theorems. A loop whose guard is equivalent to false is equivalent to skip, while a loop whose guard is equivalent to true is equivalent to while true do skip end (or any other non-terminating program). The first of these facts is easy.
Theorem while_false : ∀ b c,
  bequiv b <{false}> →
  cequiv
    <{ while b do c end }>
    <{ skip }>.

To prove the second fact, we need an auxiliary lemma stating that while loops whose guards are equivalent to true never terminate.
Lemma while_true_nonterm : ∀ b c st st',
  bequiv b <{true}> →
  ~( st =[ while b do c end ]=> st' ).
Proof.
  (* WORK IN CLASS *) Admitted.
Theorem while_true : ∀ b c,
  bequiv b <{true}> →
  cequiv
    <{ while b do c end }>
    <{ while true do skip end }>.

A more interesting fact about while commands is that any number of copies of the body can be "unrolled" without changing meaning.
Loop unrolling is an important transformation in real compilers!
Theorem loop_unrolling : ∀ b c,
  cequiv
    <{ while b do c end }>
    <{ if b then c ; while b do c end else skip end }>.
Proof.
  (* WORK IN CLASS *) Admitted.

Properties of Behavioral Equivalence

We next consider some fundamental properties of program equivalence.

Behavioral Equivalence Is an Equivalence

First, we verify that the equivalences on aexps, bexps, and coms really are equivalences -- i.e., that they are reflexive, symmetric, and transitive. The proofs are all easy.
Lemma refl_aequiv : ∀ (a : aexp), aequiv a a.
Lemma sym_aequiv : ∀ (a1 a2 : aexp),
  aequiv a1 a2 → aequiv a2 a1.
Lemma trans_aequiv : ∀ (a1 a2 a3 : aexp),
  aequiv a1 a2 → aequiv a2 a3 → aequiv a1 a3.
Lemma refl_bequiv : ∀ (b : bexp), bequiv b b.
Lemma sym_bequiv : ∀ (b1 b2 : bexp),
  bequiv b1 b2 → bequiv b2 b1.
Lemma trans_bequiv : ∀ (b1 b2 b3 : bexp),
  bequiv b1 b2 → bequiv b2 b3 → bequiv b1 b3.
Lemma refl_cequiv : ∀ (c : com), cequiv c c.
Lemma sym_cequiv : ∀ (c1 c2 : com),
  cequiv c1 c2 → cequiv c2 c1.
Lemma trans_cequiv : ∀ (c1 c2 c3 : com),
  cequiv c1 c2 → cequiv c2 c3 → cequiv c1 c3.

Behavioral Equivalence Is a Congruence

Less obviously, behavioral equivalence is also a congruence. That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded:
aequiv a a'  
cequiv (x := a) (x := a')
cequiv c1 c1'
cequiv c2 c2'  
cequiv (c1;c2) (c1';c2')
... and so on for the other forms of commands.

These properties allow us to reason that a large program behaves the same when we replace a small part with something equivalent.
Theorem CAsgn_congruence : ∀ x a a',
  aequiv a a' →
  cequiv <{x := a}> <{x := a'}>.
Theorem CWhile_congruence : ∀ b b' c c',
  bequiv b b' → cequiv c c' →
  cequiv <{ while b do c end }> <{ while b' do c' end }>.
Proof.
  (* WORK IN CLASS *) Admitted.
Theorem CSeq_congruence : ∀ c1 c1' c2 c2',
  cequiv c1 c1' → cequiv c2 c2' →
  cequiv <{ c1;c2 }> <{ c1';c2' }>.
Theorem CIf_congruence : ∀ b b' c1 c1' c2 c2',
  bequiv b b' → cequiv c1 c1' → cequiv c2 c2' →
  cequiv <{ if b then c1 else c2 end }>
         <{ if b' then c1' else c2' end }>.

For example, here are two equivalent programs and a proof of their equivalence...
Example congruence_example:
  cequiv
    (* Program 1: *)
    <{ X := 0;
       if (X = 0)
       then
         Y := 0
       else
         Y := 42
       end }>
    (* Program 2: *)
    <{ X := 0;
       if (X = 0)
       then
         Y := X - X (* <--- Changed here *)
       else
         Y := 42
       end }>.
Proof.
  apply CSeq_congruence.
  - apply refl_cequiv.
  - apply CIf_congruence.
    + apply refl_bequiv.
    + apply CAsgn_congruence. unfold aequiv. simpl.
      symmetry. apply minus_diag.
    + apply refl_cequiv.
Qed.

Program Transformations

A program transformation is a function that takes a program as input and produces some variant of the program as output. Compiler optimizations such as constant folding are a canonical example, but there are many others.
A program transformation is sound if it preserves the behavior of the original program.
Definition atrans_sound (atrans : aexp → aexp) : Prop :=
  ∀ (a : aexp),
    aequiv a (atrans a).
Definition btrans_sound (btrans : bexp → bexp) : Prop :=
  ∀ (b : bexp),
    bequiv b (btrans b).
Definition ctrans_sound (ctrans : com → com) : Prop :=
  ∀ (c : com),
    cequiv c (ctrans c).

The Constant-Folding Transformation

An expression is constant when it contains no variable references.
Constant folding is an optimization that finds constant expressions and replaces them by their values.
Fixpoint fold_constants_aexp (a : aexp) : aexp :=
  match a with
  | ANum n ⇒ ANum n
  | AId x ⇒ AId x
  | <{ a1 + a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 + n2)
    | (a1', a2') ⇒ <{ a1' + a2' }>
    end
  | <{ a1 - a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 - n2)
    | (a1', a2') ⇒ <{ a1' - a2' }>
    end
  | <{ a1 × a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 × n2)
    | (a1', a2') ⇒ <{ a1' × a2' }>
    end
  end.

Example fold_aexp_ex1 :
    fold_constants_aexp <{ (1 + 2) × X }>
  = <{ 3 × X }>.
Note that this version of constant folding doesn't eliminate trivial additions, etc. -- we are focusing attention on a single optimization for the sake of simplicity. It is not hard to incorporate other ways of simplifying expressions; the definitions and proofs just get longer.
Example fold_aexp_ex2 :
  fold_constants_aexp <{ X - ((0 × 6) + Y) }> = <{ X - (0 + Y) }>.

Not only can we lift fold_constants_aexp to bexps (in the BEq and BLe cases); we can also look for constant boolean expressions and evaluate them in-place.
Fixpoint fold_constants_bexp (b : bexp) : bexp :=
  match b with
  | <{true}> ⇒ <{true}>
  | <{false}> ⇒ <{false}>
  | <{ a1 = a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 =? n2 then <{true}> else <{false}>
      | (a1', a2') ⇒
          <{ a1' = a2' }>
      end
  | <{ a1 ≤ a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 <=? n2 then <{true}> else <{false}>
      | (a1', a2') ⇒
          <{ a1' ≤ a2' }>
      end
  | <{ ¬b1 }> ⇒
      match (fold_constants_bexp b1) with
      | <{true}> ⇒ <{false}>
      | <{false}> ⇒ <{true}>
      | b1' ⇒ <{ ¬b1' }>
      end
  | <{ b1 && b2 }> ⇒
      match (fold_constants_bexp b1,
             fold_constants_bexp b2) with
      | (<{true}>, <{true}>) ⇒ <{true}>
      | (<{true}>, <{false}>) ⇒ <{false}>
      | (<{false}>, <{true}>) ⇒ <{false}>
      | (<{false}>, <{false}>) ⇒ <{false}>
      | (b1', b2') ⇒ <{ b1' && b2' }>
      end
  end.

Example fold_bexp_ex1 :
  fold_constants_bexp <{ true && ~(false && true) }>
  = <{ true }>.
Example fold_bexp_ex2 :
  fold_constants_bexp <{ (X = Y) && (0 = (2 - (1 + 1))) }>
  = <{ (X = Y) && true }>.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.
Fixpoint fold_constants_com (c : com) : com :=
  match c with
  | <{ skip }> ⇒
      <{ skip }>
  | <{ x := a }> ⇒
      <{ x := (fold_constants_aexp a) }>
  | <{ c1 ; c2 }> ⇒
      <{ fold_constants_com c1 ; fold_constants_com c2 }>
  | <{ if b then c1 else c2 end }> ⇒
      match fold_constants_bexp b with
      | <{true}> ⇒ fold_constants_com c1
      | <{false}> ⇒ fold_constants_com c2
      | b' ⇒ <{ if b' then fold_constants_com c1
                       else fold_constants_com c2 end}>
      end
  | <{ while b do c1 end }> ⇒
      match fold_constants_bexp b with
      | <{true}> ⇒ <{ while true do skip end }>
      | <{false}> ⇒ <{ skip }>
      | b' ⇒ <{ while b' do (fold_constants_com c1) end }>
      end
  end.

Example fold_com_ex1 :
  fold_constants_com
    (* Original program: *)
    <{ X := 4 + 5;
       Y := X - 3;
       if ((X - Y) = (2 + 4)) then skip
       else Y := 0 end;
       if (0 ≤ (4 - (2 + 1))) then Y := 0
       else skip end;
       while (Y = 0) do
         X := X + 1
       end }>
  = (* After constant folding: *)
    <{ X := 9;
       Y := X - 3;
       if ((X - Y) = 6) then skip
       else Y := 0 end;
       Y := 0;
       while (Y = 0) do
         X := X + 1
       end }>.

Soundness of Constant Folding

Now we need to show that what we've done is correct.
Theorem fold_constants_aexp_sound :
  atrans_sound fold_constants_aexp.
Theorem fold_constants_bexp_sound:
  btrans_sound fold_constants_bexp.
Theorem fold_constants_com_sound :
  ctrans_sound fold_constants_com.

Proving Inequivalence

Suppose that c1 is a command of the form X := a1; Y := a2 and c2 is the command X := a1; Y := a2', where a2' is formed by substituting a1 for all occurrences of X in a2. For example, c1 and c2 might be:
       c1 = (X := 42 + 53;
               Y := Y + X)
       c2 = (X := 42 + 53;
               Y := Y + (42 + 53)) Clearly, this particular c1 and c2 are equivalent. Is this true in general?

More formally, here is the function that substitutes an arithmetic expression u for each occurrence of a given variable x in another expression a:
Fixpoint subst_aexp (x : string) (u : aexp) (a : aexp) : aexp :=
  match a with
  | ANum n ⇒
      ANum n
  | AId x' ⇒
      if eqb_string x x' then u else AId x'
  | <{ a1 + a2 }> ⇒
      <{ (subst_aexp x u a1) + (subst_aexp x u a2) }>
  | <{ a1 - a2 }> ⇒
      <{ (subst_aexp x u a1) - (subst_aexp x u a2) }>
  | <{ a1 × a2 }> ⇒
      <{ (subst_aexp x u a1) × (subst_aexp x u a2) }>
  end.
Example subst_aexp_ex :
  subst_aexp X <{42 + 53}> <{Y + X}>
  = <{ Y + (42 + 53)}>.

And here is the property we are interested in, expressing the claim that commands c1 and c2 as described above are always equivalent.
Definition subst_equiv_property := ∀ x1 x2 a1 a2,
  cequiv <{ x1 := a1; x2 := a2 }>
         <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>.

Sadly, the property does not always hold.
We can show the following counterexample:
       X := X + 1; Y := X If we perform the substitution, we get
       X := X + 1; Y := X + 1 which clearly isn't equivalent to the original program. ☐
Theorem subst_inequiv :
  ¬subst_equiv_property.