Library ex8


Blatt 8 —- Program Equivalences

SemProg SoSe 2013, Set 8

Based on the material of the online course "Software Foundations" by Pierce et al. Submit your solutions to tadeusz.m.litak at cs.fau.de
Please submit by Jun 30, anywhere on earth.
As we start a new material block with Hoare logic next week, I am going to be away and I still need to clear the stack of old exercises, there is no reason to hurry now. You have 2 weeks to this material.
However, as most of exercises are rather easy and quite often they simply fill in things we did not manage to do during the last lecture, please try at least some earlier.
Please remember to download a corrected version of Imp.v, recompile it and recompile Equiv.v Otherwise, the Bonusaufgabe will not go through...
The file consists of 6 obligatory exercises, yielding 35 points altogether and one bonus exercise, which yields 15 additional points for those willing.

Require Export Equiv.

Exercise 1: 5 points (Lemmas on behavorial equivalence)

Behavioral Equivalence is an Equivalence

Unusually, this exercise consists of lemmas only. This is just something we did not finish during the lecture, a bunch of lemmas we need later. The proofs are all unspeakably trivial.

Lemma refl_aequiv : forall (a : aexp), aequiv a a.
Proof.
 Admitted.

Lemma sym_aequiv : forall (a1 a2 : aexp),
  aequiv a1 a2 -> aequiv a2 a1.
Proof.
  Admitted.

Lemma trans_aequiv : forall (a1 a2 a3 : aexp),
  aequiv a1 a2 -> aequiv a2 a3 -> aequiv a1 a3.
Proof.
  Admitted.

Lemma refl_bequiv : forall (b : bexp), bequiv b b.
Proof.
  Admitted.

Lemma sym_bequiv : forall (b1 b2 : bexp),
  bequiv b1 b2 -> bequiv b2 b1.
Proof.
  Admitted.

Lemma trans_bequiv : forall (b1 b2 b3 : bexp),
  bequiv b1 b2 -> bequiv b2 b3 -> bequiv b1 b3.
Proof.
  Admitted.

Lemma refl_cequiv : forall (c : com), cequiv c c.
Proof.
  Admitted.

Lemma sym_cequiv : forall (c1 c2 : com),
  cequiv c1 c2 -> cequiv c2 c1.
Proof.
  Admitted.

Lemma iff_trans : forall (P1 P2 P3 : Prop),
  (P1 <-> P2) -> (P2 <-> P3) -> (P1 <-> P3).
Proof.
  Admitted.

Lemma trans_cequiv : forall (c1 c2 c3 : com),
  cequiv c1 c2 -> cequiv c2 c3 -> cequiv c1 c3.
Proof.
  Admitted.

Exercise 2: 5 points (skip_right)

Recall that during the lecutre we did a theorem skip_left. Now prove that adding a SKIP after a command results in an equivalent program

Theorem skip_right: forall c,
  cequiv
    (c; SKIP)
    c.
Proof. Admitted.

Exercise 3: 7.5 points (swap_if_branches)

Show that we can swap the branches of an IF by negating its condition

Theorem swap_if_branches: forall b e1 e2,
  cequiv
    (IFB b THEN e1 ELSE e2 FI)
    (IFB BNot b THEN e2 ELSE e1 FI).
Proof. Admitted.

Exercise 4: 5 points (seq_assoc)


Theorem seq_assoc : forall c1 c2 c3,
  cequiv ((c1;c2);c3) (c1;(c2;c3)).
Proof. Admitted.

Exercise 5: 5 points (assign_aequiv)

HINT: this is an exercise for the functional equivalence axiom

Theorem assign_aequiv : forall X e,
  aequiv (AId X) e ->
  cequiv SKIP (X ::= e).
Proof. Admitted.

Exercise 6: 7.5 points (CWhile_congruence, CSeq_congruence, CIf_congruence)

Again, this is just leftover from the lecture. We did one direction of CWHile_congruence and have not finished the other direction. We also failed to prove congruence theorems for Seq and If. Go for it now.

Theorem CWhile_congruence : forall b1 b1' c1 c1',
  bequiv b1 b1' -> cequiv c1 c1' ->
  cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' END).
Proof.
  unfold bequiv,cequiv.
  intros b1 b1' c1 c1' Hb1e Hc1e st st'.
  split; intros Hce.
  Case "->".
    remember (WHILE b1 DO c1 END) as cwhile.
    induction Hce; inversion Heqcwhile; subst.
    SCase "E_WhileEnd". apply E_WhileEnd. rewrite <- Hb1e. assumption.
    SCase "E_WhileLoop". apply E_WhileLoop with (st' := st').
       SSCase "a) show that guard evaluates to true". rewrite <- Hb1e. assumption.
       SSCase "b) c1' indeed evaluates to st'". apply Hc1e. assumption.
       SSCase "c) subsequent loop execution". apply IHHce2. reflexivity.
  Case "<-". Admitted.

Theorem CSeq_congruence : forall c1 c1' c2 c2',
  cequiv c1 c1' -> cequiv c2 c2' ->
  cequiv (c1;c2) (c1';c2').
Proof.
Admitted.

Theorem CIf_congruence : forall b b' c1 c1' c2 c2',
  bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
  cequiv (IFB b THEN c1 ELSE c2 FI) (IFB b' THEN c1' ELSE c2' FI).
Proof.
Admitted.

This is the end of obligatory exercises.

Extended Bonusaufgabe: 15 points (Non-deterministic Imp)

As we have seen (in theorem ceval_deterministic in the Imp chapter), Imp's evaluation relation is deterministic. However, non-determinism is an important part of the definition of many real programming languages. For example, in many imperative languages (such as C and its relatives), the order in which function arguments are evaluated is unspecified. The program fragment x = 0; f(++x, x); might call f with arguments (1, 0) or (1, 1), depending how the compiler chooses to order things. This can be a little confusing for programmers, but it gives the compiler writer useful freedom.
In this exercise, we will extend Imp with a simple non-deterministic command and study how this change affects program equivalence. The new command has the syntax HAVOC X, where X is an identifier. The effect of executing HAVOC X is to assign an arbitrary number to the variable X, non-deterministically. For example, after executing the program: HAVOC Y; Z ::= Y * 2 the value of Y can be any number, while the value of Z is twice that of Y (so Z is always even). Note that we are not saying anything about the probabilities of the outcomes — just that there are (infinitely) many different outcomes that can possibly happen after executing this non-deterministic code.
In a sense a variable on which we do HAVOC roughly corresponds to an unitialized variable in the C programming language. After the HAVOC the variable holds a fixed but arbitrary number. Most sources of nondeterminism in language definitions are there precisely because programmers don't care which choice is made (and so it is good to leave it open to the compiler to choose whichever will run faster).
We call this new language Himp (``Imp extended with HAVOC'').

Module Himp.

To formalize the language, we first add a clause to the definition of commands.

Inductive com : Type :=
  | CSkip : com
  | CAss : id -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com
  | CHavoc : id -> com.
Tactic Notation "com_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
  | Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "HAVOC" ].

Notation "'SKIP'" :=
  CSkip.
Notation "X '::=' a" :=
  (CAss X a) (at level 60).
Notation "c1 ; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
  (CIf e1 e2 e3) (at level 80, right associativity).
Notation "'HAVOC' l" := (CHavoc l) (at level 60).

(himp_ceval)

Now, we must extend the operational semantics. We have provided a template for the ceval relation below, specifying the big-step semantics. What rule(s) must be added to the definition of ceval to formalize the behavior of the HAVOC command?

Reserved Notation "c1 '/' st '||' st'" (at level 40, st at level 39).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st : state, SKIP / st || st
  | E_Ass : forall (st : state) (a1 : aexp) (n : nat) (X : id),
            aeval st a1 = n -> (X ::= a1) / st || update st X n
  | E_Seq : forall (c1 c2 : com) (st st' st'' : state),
            c1 / st || st' -> c2 / st' || st'' -> (c1 ; c2) / st || st''
  | E_IfTrue : forall (st st' : state) (b1 : bexp) (c1 c2 : com),
               beval st b1 = true ->
               c1 / st || st' -> (IFB b1 THEN c1 ELSE c2 FI) / st || st'
  | E_IfFalse : forall (st st' : state) (b1 : bexp) (c1 c2 : com),
                beval st b1 = false ->
                c2 / st || st' -> (IFB b1 THEN c1 ELSE c2 FI) / st || st'
  | E_WhileEnd : forall (b1 : bexp) (st : state) (c1 : com),
                 beval st b1 = false -> (WHILE b1 DO c1 END) / st || st
  | E_WhileLoop : forall (st st' st'' : state) (b1 : bexp) (c1 : com),
                  beval st b1 = true ->
                  c1 / st || st' ->
                  (WHILE b1 DO c1 END) / st' || st'' ->
                  (WHILE b1 DO c1 END) / st || st''

  where "c1 '/' st '||' st'" := (ceval c1 st st').

Tactic Notation "ceval_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"
  | Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"
  | Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"

].

As a sanity check, the following claims should be provable for your definition:

Example havoc_example1 : (HAVOC X) / empty_state || update empty_state X 0.
Proof.
Admitted.

Example havoc_example2 :
  (SKIP; HAVOC Z) / empty_state || update empty_state Z 42.
Proof.
Admitted.
Finally, we repeat the definition of command equivalence from above:

Definition cequiv (c1 c2 : com) : Prop := forall st st' : state,
  c1 / st || st' <-> c2 / st || st'.

This definition still makes perfect sense in the case of always terminating programs, so let's apply it to prove some non-deterministic programs equivalent or non-equivalent.

The first reasonably difficult past of the exercise: (havoc_swap)

Are the following two programs equivalent?

Definition pXY :=
  HAVOC X; HAVOC Y.

Definition pYX :=
  HAVOC Y; HAVOC X.

If you think they are equivalent, prove it. If you think they are not, prove that.

Theorem pXY_cequiv_pYX :
  cequiv pXY pYX \/ ~cequiv pXY pYX.
Proof. Admitted.

A more interesting part of the exercise: (havoc_copy)

Are the following two programs equivalent?

Definition ptwice :=
  HAVOC X; HAVOC Y.

Definition pcopy :=
  HAVOC X; Y ::= AId X.

If you think they are equivalent, then prove it. If you think they are not, then prove that. (Hint: You may find the assert tactic useful.)

Theorem ptwice_cequiv_pcopy :
  cequiv ptwice pcopy \/ ~cequiv ptwice pcopy.
Proof. Admitted.
The definition of program equivalence we are using here has some subtle consequences on programs that may loop forever. What cequiv says is that the set of possible terminating outcomes of two equivalent programs is the same. However, in a language with non-determinism, like Himp, some programs always terminate, some programs always diverge, and some programs can non-deterministically terminate in some runs and diverge in others. The final part of the following exercise illustrates this phenomenon.

The really interesting and difficult part of the exercise: (havoc_diverge)

Prove the following program equivalences and non-equivalences, and try to understand why the cequiv definition has the behavior it has on these examples.

Definition p1 : com :=
  WHILE (BNot (BEq (AId X) (ANum 0))) DO
    HAVOC Y;
    X ::= APlus (AId X) (ANum 1)
  END.

Definition p2 : com :=
  WHILE (BNot (BEq (AId X) (ANum 0))) DO
    SKIP
  END.

Just a bunch of lemmas you can find useful and illuminating...

Lemma nateq_helper : forall n m, negb (beq_nat n m) = false -> n = m.
Proof. Admitted.
Super-easy, just like the next one...

Lemma natneq_helper : forall n m, negb (beq_nat n m) = true -> n <> m.
Proof. Admitted.


Lemma p1_may_diverge : forall st st', st X <> 0 ->
  ~ p1 / st || st'.
Proof.
  Admitted.

Lemma p2_may_diverge : forall st st', st X <> 0 ->
  ~ p2 / st || st'.
Proof. Admitted.

Theorem p1_p2_equiv : cequiv p1 p2.
Proof. Admitted.

Programs p3 and p4 are not equivalent: when p3 terminates, even though X definitely has value 0, Z might have any natural number as the value.

Definition p3 : com :=
  Z ::= ANum 1;
  WHILE (BNot (BEq (AId X) (ANum 0))) DO
    HAVOC X;
    HAVOC Z
  END.

Definition p4 : com :=
  X ::= (ANum 0);
  Z ::= (ANum 1).

Theorem p3_p4_inequiv : ~ cequiv p3 p4.
Proof. Admitted.

Definition p5 : com :=
  WHILE (BNot (BEq (AId X) (ANum 1))) DO
    HAVOC X
  END.

Definition p6 : com :=
  X ::= ANum 1.

Programs p5 and p6 are equivalent although p5 may diverge, while p6 always terminates. The definition we took for cequiv cannot distinguish between these two scenarios. It accepts the two programs as equivalent on the basis that: if p5 terminates it produces the same final state as p6, and there exists an execution in which p5 terminates and does exactly as p6.
There are two directions to the proof:
->: Observe that whenever p5 terminates, it does so with X set to 1, and no other variable changed. But this is exactly the behavior of p6. Thus given a pair of states st and st' and that p5 / st || st', the answer to the question "Does p6 / st || st'?" is "Yes".
<- (and more controversially): Given that p6 / st || st' for some st and st', can we show that p5 / st | st'? Observe that we can use the hypothesis to conclude that st' = update st X 1. Is there some execution of p5 starting from st which also ends up in st'? Yes!
Hence their equivalence.

Lemma p5_summary : forall st st', p5 / st || st' -> st' = update st X 1.
Proof. Admitted.

Theorem p5_p6_equiv : cequiv p5 p6.
Proof. Admitted.

End Himp.