ImpEquiv

Equivalence of Imp programs

Each piece of syntax can be given a meaning in two steps:
         syntax
           → (representation)
       itree MemE
           → (interpretation)
   stateT mem (itree ∅)

Definitions and elementary properties

That means we have several notions of equivalence:
  • syntactic equality (equal syntax)
  • representation equality (equality as uninterpreted trees)
  • semantic equality (equality as computations in the state monad )
Definition aexp_equiv : rel aexp :=
  fun a1 a2 ⇒ ∀ σ, ℑ ⟦ a1 ⟧a σ ≈ ℑ ⟦ a2 ⟧a σ.
Definition bexp_equiv : rel bexp :=
  fun b1 b2 ⇒ ∀ σ, ℑ ⟦ b1 ⟧b σ ≈ ℑ ⟦ b2 ⟧b σ.
Definition com_eq : rel com :=
  fun c1 c2 ⇒ ⟦ c1 ⟧ ≈ ⟦ c2 ⟧.
Definition com_equiv : rel com :=
  fun c1 c2 ⇒ ∀ σ, ℑ ⟦ c1 ⟧ σ ≈ ℑ ⟦ c2 ⟧ σ.
Infix "≈ₐ" := aexp_equiv (at level 20).
Infix "≈ᵦ" := bexp_equiv (at level 20).
Infix "≡" := com_eq (at level 20).
Infix "≊" := com_equiv (at level 20).

Elementary properties of program equivalences

We establish the following central properties:
  • All equivalences of syntax considered are equivalence relations
  • Representation equality is strictly tighter than semantic equality
  • All equivalences are congruences: they are compatible with every construction of the language

Semantically characterizing the MemE events

Lemma interp_state_rd : ∀ x σ, ℑ (rd x) σ ≈ Ret (σ, σ x).
Proof.
  unfold rd; intros; now norm.
Qed.

Lemma interp_state_wr : ∀ x v σ, ℑ (wr x v) σ ≈ Ret (x !-> v ; σ, tt).
Proof.
  unfold wr; intros; now norm.
Qed.

Semantically Characterizing Evaluation

We can prove that the evaluation of arithmetic and boolean expressions in Imp is pure, and that it computes the same things as the "naive" evaluator.
We will need that arithmetic and boolean expressions are pure
Lemma aexp_pure_aeval : ∀ a σ,
    interp_state handle_Mem ⟦ a ⟧a σ ≈ Ret (σ, aeval σ a).
Proof.
  intros.
  induction a; cbn.
  - now norm.
  - now norm.
  - norm; rewrite IHa1.
    norm; rewrite IHa2.
    now norm.
  - norm; rewrite IHa1.
    norm; rewrite IHa2.
    now norm.
  - norm; rewrite IHa1.
    norm; rewrite IHa2.
    now norm.
Qed.

Lemma bexp_pure_beval : ∀ b σ,
    interp_state handle_Mem ⟦ b ⟧b σ ≈ Ret (σ, beval σ b).
Proof.
  intros.
  induction b; cbn.
  - now norm.
  - now norm.
  - norm.
    rewrite (aexp_pure_aeval a1 σ).
    norm.
    rewrite (aexp_pure_aeval a2 σ).
    now norm.
  - norm.
    rewrite (aexp_pure_aeval a1 σ).
    norm. rewrite (aexp_pure_aeval a2 σ).
    now norm.
  - norm.
    rewrite (aexp_pure_aeval a1 σ).
    norm. rewrite (aexp_pure_aeval a2 σ).
    now norm.
  - norm.
    rewrite (aexp_pure_aeval a1 σ).
    norm. rewrite (aexp_pure_aeval a2 σ).
    now norm.
  - norm. rewrite IHb.
    now norm.
  - norm.
    rewrite IHb1.
    norm.
    rewrite IHb2.
    now norm.
Qed.

Universally valid static rewrite rules: an inventory

We can prove many properties of Imp programs even without understanding how the semantics of memory works.
We can create an inventory of such rewrite rules.
Note that these rules would be valid even if we change the semantics of memory operations (assuming arithmetic and booleans are pure).

Rules for arithmetic expressions

Variant red_aexp : rel aexp :=
  | rplus (n m : val) : red_aexp <{ APlus n m }> <{ aop_sem op_plus n m }>
  | rminus (n m : val) : red_aexp <{ AMinus n m }> <{ aop_sem op_minus n m }>
  | rmult (n m : val) : red_aexp <{ AMult n m }> <{ aop_sem op_mult n m }>
  | minus_inv e : red_aexp <{ e - e }> <{ 0 }>
  | mult_zero e : red_aexp <{ 0 × e }> <{ 0 }>
  | mult_one e : red_aexp <{ 1 × e }> <{ e }>
  | plus_zero a : red_aexp <{ 0 + a }> <{ a }>
  | plus_comm a1 a2 : red_aexp <{ a1 + a2 }> <{ a2 + a1 }>
  | mult_comm a1 a2 : red_aexp <{ a1 × a2 }> <{ a2 × a1 }>
.

Rules on boolean expressions

Variant red_bexp : rel bexp :=
  | req n m : red_bexp <{ BEq (ANum n) (ANum m) }> (if Nat.eqb n m then <{true}> else <{false}>)
  | rneq n m : red_bexp <{ BNeq (ANum n) (ANum m) }> (if Nat.eqb n m then <{false}> else <{true}>)
  | rle n m : red_bexp <{ BLe (ANum n) (ANum m) }> (if Nat.leb n m then <{true}> else <{false}>)
  | rgt n m : red_bexp <{ BGt (ANum n) (ANum m) }> (if Nat.leb n m then <{false}> else <{true}>)
  | rnegt : red_bexp <{ ¬true }> <{false}>
  | rnegf : red_bexp <{ ¬false }> <{true}>
  | randtt : red_bexp <{ true && true }> <{ true}>
  | randft : red_bexp <{ false && true }> <{ false }>
  | randff : red_bexp <{ false && false }> <{ false }>
  | and_comm b b' : red_bexp <{ b && b' }> <{ b' && b }>
.

Rules on commands (1)

These are straight-up validated by ≡ (strong equivalence
Variant red_com1 : rel com :=
| skipL c : red_com1 <{ skip ; c }> <{c}>
| skipR c : red_com1 <{ c ; skip }> <{c}>
| iftrue c1 c2 : red_com1 <{ if true then c1 else c2 end }> c1
| iffalse c1 c2 : red_com1 <{ if false then c1 else c2 end }> c2
| whilefalse c : red_com1 <{ while false do c end }> <{ skip }>
| ifComm b c1 c2 : red_com1 <{ if b then c1 else c2 end }> <{ if ¬b then c2 else c1 end }>
| ifDist b c1 c2 c : red_com1 <{ if b then c1 else c2 end ; c }> <{ if b then c1 ; c else c2 ; c end }>
| seqA c1 c2 c3 : red_com1 <{ (c1 ; c2) ; c3 }> <{ c1 ; (c2 ; c3) }>
| loop_unroll1 b c : red_com1 <{ while b do c end }> <{ if b then c ; while b do c end else skip end }>.
Rules on commands that are only validated by ≊
Variant red_com2 : com → com → Prop :=
| whiletrue c : red_com2 <{ while true do c end }> <{ while true do skip end }>
| loop_unroll2 b c : red_com2 <{ while b do c end }> <{ while b do c ; if b then c else skip end end }>.

Semantic validity of our calculus

For each equivalence, we justify the correctness by proving a lemma.
Lemma minus_inv_sound : ∀ e,
    <{ e - e }> ≈ₐ 0.
Proof.
  intros e σ.
  cbn.
  norm.
  pose proof aexp_pure e σ as [v EQ]. (* Note that if e was impure (if it diverged for instance), then the equation would be invalid *)
  rewrite EQ; norm.
  rewrite EQ; norm.
  cbn.
  now rewrite PeanoNat.Nat.sub_diag.
Qed.

Lemma mult_zero_sound : ∀ e,
    <{ 0 × e }> ≈ₐ 0.
Proof.
  intros e σ.
  rewrite aexp_pure_aeval.
  cbn.
  norm.
  reflexivity.
Qed.

Proofs of equivalences of commands

And we can prove interesting semantic equivalenes of Imp programs.
Lemma skipL_sound : ∀ c,
    <{ skip ; c }> ≡
    <{c}>.
Proof.
  intros; red; cbn; now norm.
Qed.

Lemma whiletrue_sound c : <{ while true do c end }> ≊ <{ while true do skip end}>.
Proof.
  intros σ.
  unfold model_com, compose.
  rewrite while_true_skip_spin.
  rewrite loop_unroll1_strong.
  rewrite interp_state_bind.
  setoid_rewrite interp_state_tau.
  rewrite whiletrue_sound_aux.
  reflexivity.
Qed.

A sound static calculus

The elementary soundness lemmas characterizes that each set of reduction rule is a subrelation of the corresponding semantic equivalence.
Theorem red_aexp_sound : ∀ a1 a2,
    red_aexp a1 a2 →
    a1 ≈ₐ a2.
Proof.
  intros × RED; inversion RED; subst; eauto with opt.
Qed.

Theorem red_bexp_sound : ∀ b1 b2,
    red_bexp b1 b2 →
    b1 ≈ᵦ b2.
Proof.
  intros × RED; inversion RED; subst; eauto with opt.
Qed.

Proving program equivalences

We can use our static calculus to prove program equivalences.
Note what happens to justify this rewrite:
  • red_aexp is a subrelation to ≈ₐ
  • ≈ₐ is compatible with Asgn x, leading to a ≈ relation
  • ≈ is a congruence, hence being lifted to all the surrounding contexts
  • ≈ is transitive, hence allowing the rewrite of the substituted program
Example congruence_example:
    (* 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.
  rewrite minus_inv.
  reflexivity.
Qed.

Constant folding as a tactic

Our set of rules can be used to define "proof-level optimizations". We can "run" constant folding in proofs of equivalences by picking out a set of rewrite rules to use.
#[global] Hint Rewrite
  rplus rminus rmult PeanoNat.Nat.eqb_refl (* we compute variable-free aexp *)
  req rle randft randtt randff rnegt rnegf (* we compute variable-free bexp *)
  iftrue iffalse whiletrue whilefalse (* we collapse trivial control flow*)
  : cst_folding.
Ltac cst_fold := autorewrite with cst_folding; cbn.

Example

And we can run it in proofs to simplify programs Examples from plf
Example fold_aexp_ex1 :
  <{ (1 + 2) × X }> ≈ₐ <{ 3 × X }>.
Proof.
  cst_fold.
  reflexivity.
Qed.

More interesting example

Example fold_com_ex1 :
    (* 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 }>.
Proof.
  cst_fold.
  reflexivity.
Qed.

Constant folding as a sound optimization

We can implement a transformation on Imp syntax and verify that it is a correct optimization.
Fixpoint fold_constants_aexp (a : aexp) : aexp :=
  match a with
  | ANum n ⇒ ANum n
  | AId x ⇒ AId x
  | APlus a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (aop_sem op_plus n1 n2)
    | (a1', a2') ⇒ <{ APlus a1' a2' }>
    end
  | AMinus a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (aop_sem op_minus n1 n2)
    | (a1', a2') ⇒ <{ AMinus a1' a2' }>
    end
  | AMult a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (aop_sem op_mult n1 n2)
    | (a1', a2') ⇒ <{ AMult a1' a2' }>
    end
  end.
And its proof of correctness
Lemma fold_constants_aexp_sound a :
  fold_constants_aexp a ≈ₐ a.
Proof.
  induction a; try rewrite <- IHa1, <- IHa2; try reflexivity; cbn.
  -
  destruct (fold_constants_aexp a1).
  2,3,4,5: now rewrite IHa1, IHa2. (* These rewrites rely on ≈ₐ being a congruence *)
  destruct (fold_constants_aexp a2); try rewrite <- IHa1, <- IHa2; try reflexivity.
  rewrite rplus. (* The optimization in this case corresponds exactly to raop *)
  reflexivity.
  -
  destruct (fold_constants_aexp a1).
  2,3,4,5: now rewrite IHa1, IHa2. (* These rewrites rely on ≈ₐ being a congruence *)
  destruct (fold_constants_aexp a2); try rewrite <- IHa1, <- IHa2; try reflexivity.
  rewrite rminus. (* The optimization in this case corresponds exactly to raop *)
  reflexivity.
  -
  destruct (fold_constants_aexp a1).
  2,3,4,5: now rewrite IHa1, IHa2. (* These rewrites rely on ≈ₐ being a congruence *)
  destruct (fold_constants_aexp a2); try rewrite <- IHa1, <- IHa2; try reflexivity.
  rewrite rmult. (* The optimization in this case corresponds exactly to raop *)
  reflexivity.
Qed.

Constant folding over commands

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.
Lemma fold_constants_com_sound c :
  fold_constants_com c ≊ c.
Proof.
  induction c; try reflexivity.
  - now cbn; rewrite fold_constants_aexp_sound.
  - now cbn; rewrite IHc1,IHc2.
  - cbn.
    repeat break_match.
    all: rewrite ?IHc1, ?IHc2.
    all: rewrite <- (fold_constants_bexp_sound b), EQ.
    all: try reflexivity.
    now rewrite iftrue. (* The optimization in this case corresponds exactly to iftrue *)
    now rewrite iffalse. (* The optimization in this case corresponds exactly to iffalse *)
  - cbn.
    repeat break_match.
    all: rewrite <- (fold_constants_bexp_sound b), EQ.
    all: try now rewrite IHc.
    now rewrite <- whiletrue. (* The optimization in this case corresponds exactly to whiletrue *)
    now rewrite <- whilefalse. (* The optimization in this case corresponds exactly to whilefalse *)
Qed.

Example of optimizing Commands

Of course now that we have a sound syntactic level transformation, we can use this instead of our tactic for better efficiency.
Example fold_com_ex1_revisited :
    (* 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 }>.
Proof.
  rewrite <- fold_constants_com_sound.
  cbn.
  reflexivity.
Qed.