Copyright (c) 2016

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

Some general advice for working on exercises:

• Most of the Coq proofs we ask you to do are similar to proofs that we've provided. Before starting to work on exercises problems, take the time to work through our proofs (both informally, on paper, and in Coq) and make sure you understand them in detail. This will save you a lot of time.
• The Coq proofs we're doing now are sufficiently complicated that it is more or less impossible to complete them simply by random experimentation or "following your nose." You need to start with an idea about why the property is true and how the proof is going to go. The best way to do this is to write out at least a sketch of an informal proof on paper — one that intuitively convinces you of the truth of the theorem — before starting to work on the formal one. Alternately, grab a friend and try to convince them that the theorem is true; then try to formalize your explanation.
• Use automation to save work! Some of the proofs in this chapter's exercises are pretty long if you try to write out all the cases explicitly.

Behavioral Equivalence

In an earlier chapter, we investigated the correctness of a very simple program transformation: the optimize_0plus function. The programming language we were considering was the first version of the language of arithmetic expressions — with no variables — so in that setting it was very easy to define what it means for a program transformation to be correct: it should always yield a program that evaluates to the same number as the original. To go further and talk about the correctness of program transformations in the full Imp language, we need to consider the role of variables and state.

Definitions

For aexps and bexps with variables, the definition we want is clear. We say that two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

For commands, the situation is a little more subtle. We can't simply say "two commands are behaviorally equivalent if they evaluate to the same ending state whenever they are started in the same initial state," because some commands, when run in some starting states, don't terminate in any final state at all! What we need instead is this: two commands are behaviorally equivalent if, for any given starting state, they either both diverge or both terminate in the same final state. A compact way to express this is "if the first one terminates in a particular state then so does the second, and vice versa."

Exercise: 2 stars (equiv_classes)

Given the following programs, group together those that are equivalent in Imp. Your answer should be given as a list of lists, where each sub-list represents a group of equivalent programs. For example, if you think programs (a) through (h) are all equivalent to each other, but not to (i), your answer should look like this: Write down your answer below in the definition of equiv_classes.

☐

Examples

Here are some simple examples of equivalences of arithmetic and boolean expressions.

For examples of command equivalence, let's start by looking at some trivial program transformations involving SKIP:

Exercise: 2 stars (skip_right)

Prove that adding a SKIP after a command results in an equivalent program

☐ Similarly, here is a simple transformations that optimizes IFB commands:

Of course, few programmers would be tempted to write a conditional whose guard is literally BTrue. A more interesting case is when the guard is equivalent to true: Theorem: If b is equivalent to BTrue, then IFB b THEN c₁ ELSE c₂ FI is equivalent to c₁. Proof:

• (→) We must show, for all st and st', that if IFB b THEN c₁ ELSE c₂ FI / st ⇓ st' then c₁ / st ⇓ st'.
  Proceed by cases on the rules that could possibly have been used to show IFB b THEN c₁ ELSE c₂ FI / st ⇓ st', namely E_IfTrue and E_IfFalse.
  • Suppose the final rule rule in the derivation of IFB b THEN c₁ ELSE c₂ FI / st ⇓ st' was E_IfTrue. We then have, by the premises of E_IfTrue, that c₁ / st ⇓ st'. This is exactly what we set out to prove.
  • On the other hand, suppose the final rule in the derivation of IFB b THEN c₁ ELSE c₂ FI / st ⇓ st' was E_IfFalse. We then know that beval st b = false and c₂ / st ⇓ st'.
    Recall that b is equivalent to BTrue, i.e., forall st, beval st b = beval st BTrue. In particular, this means that beval st b = true, since beval st BTrue = true. But this is a contradiction, since E_IfFalse requires that beval st b = false. Thus, the final rule could not have been E_IfFalse.
• (←) We must show, for all st and st', that if c₁ / st ⇓ st' then IFB b THEN c₁ ELSE c₂ FI / st ⇓ st'.
  Since b is equivalent to BTrue, we know that beval st b = beval st BTrue = true. Together with the assumption that c₁ / st ⇓ st', we can apply E_IfTrue to derive IFB b THEN c₁ ELSE c₂ FI / st ⇓ st'. ☐

Here is the formal version of this proof:

Exercise: 2 stars, recommended (IFB_false)

☐

Exercise: 3 stars (swap_if_branches)

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

☐ For WHILE loops, we can give a similar pair of theorems. A loop whose guard is equivalent to BFalse is equivalent to SKIP, while a loop whose guard is equivalent to BTrue is equivalent to WHILE BTrue DO SKIP END (or any other non-terminating program). The first of these facts is easy.

Exercise: 2 stars, advanced, optional (WHILE_false_informal)

Write an informal proof of WHILE_false. (* FILL IN HERE *)
☐ To prove the second fact, we need an auxiliary lemma stating that WHILE loops whose guards are equivalent to BTrue never terminate: Lemma: If b is equivalent to BTrue, then it cannot be the case that (WHILE b DO c END) / st ⇓ st'. Proof: Suppose that (WHILE b DO c END) / st ⇓ st'. We show, by induction on a derivation of (WHILE b DO c END) / st ⇓ st', that this assumption leads to a contradiction.

• Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule E_WhileEnd. Then by assumption beval st b = false. But this contradicts the assumption that b is equivalent to BTrue.
• Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule E_WhileLoop. Then we are given the induction hypothesis that (WHILE b DO c END) / st ⇓ st' is contradictory, which is exactly what we are trying to prove!
• Since these are the only rules that could have been used to prove (WHILE b DO c END) / st ⇓ st', the other cases of the induction are immediately contradictory. ☐

Exercise: 2 stars, optional (WHILE_true_nonterm_informal)

Explain what the lemma WHILE_true_nonterm means in English. (* FILL IN HERE *)
☐

Exercise: 2 stars, recommended (WHILE_true)

Prove the following theorem. Hint: You'll want to use WHILE_true_nonterm here.

☐

Exercise: 2 stars, optional (seq_assoc)

☐ Proving program properties involving assignments is one place where the functional-extensionality axiom introduced in the Logic chapter often comes in handy. Here are an example and an exercise.

Exercise: 2 stars, recommended (assign_aequiv)

☐

Properties of Behavioral Equivalence

We now turn to developing some of the properties of the program equivalences we have defined.

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.

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 a1 a1'
cequiv (i ::= a1) (i ::= a1')

cequiv c1 c1'
cequiv c2 c2'
cequiv (c1;;c2) (c1';;c2')

...and so on for the other forms of commands. (Note that we are using the inference rule notation here not as part of a definition, but simply to write down some valid implications in a readable format. We prove these implications below.) We will see a concrete example of why these congruence properties are important in the following section (in the proof of fold_constants_com_sound), but the main idea is that they allow us to replace a small part of a large program with an equivalent small part and know that the whole large programs are equivalent without doing an explicit proof about the non-varying parts — i.e., the "proof burden" of a small change to a large program is proportional to the size of the change, not the program.

The congruence property for loops is a little more interesting, since it requires induction. Theorem: Equivalence is a congruence for WHILE — that is, if b₁ is equivalent to b₁' and c₁ is equivalent to c₁', then WHILE b₁ DO c₁ END is equivalent to WHILE b₁' DO c₁' END. Proof: Suppose b₁ is equivalent to b₁' and c₁ is equivalent to c₁'. We must show, for every st and st', that WHILE b₁ DO c₁ END / st ⇓ st' iff WHILE b₁' DO c₁' END / st ⇓ st'. We consider the two directions separately.

• (→) We show that WHILE b₁ DO c₁ END / st ⇓ st' implies WHILE b₁' DO c₁' END / st ⇓ st', by induction on a derivation of WHILE b₁ DO c₁ END / st ⇓ st'. The only nontrivial cases are when the final rule in the derivation is E_WhileEnd or E_WhileLoop.
  • E_WhileEnd: In this case, the form of the rule gives us beval st b₁ = false and st = st'. But then, since b₁ and b₁' are equivalent, we have beval st b₁' = false, and E-WhileEnd applies, giving us WHILE b₁' DO c₁' END / st ⇓ st', as required.
  • E_WhileLoop: The form of the rule now gives us beval st b₁ = true, with c₁ / st ⇓ st'0 and WHILE b₁ DO c₁ END / st'0 ⇓ st' for some state st'0, with the induction hypothesis WHILE b₁' DO c₁' END / st'0 ⇓ st'.
    Since c₁ and c₁' are equivalent, we know that c₁' / st ⇓ st'0. And since b₁ and b₁' are equivalent, we have beval st b₁' = true. Now E-WhileLoop applies, giving us WHILE b₁' DO c₁' END / st ⇓ st', as required.
• (←) Similar. ☐

Exercise: 3 stars, optional (CSeq_congruence)

☐

Exercise: 3 stars (CIf_congruence)

☐ For example, here are two equivalent programs and a proof of their equivalence...

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.

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.

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.

Not only can we lift fold_constants_aexp to bexps (in the BEq and BLe cases), we can also find constant boolean expressions and evaluate them in-place.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.

Soundness of Constant Folding

Now we need to show that what we've done is correct. Here's the proof for arithmetic expressions:

Exercise: 3 stars, optional (fold_bexp_Eq_informal)

Here is an informal proof of the BEq case of the soundness argument for boolean expression constant folding. Read it carefully and compare it to the formal proof that follows. Then fill in the BLe case of the formal proof (without looking at the BEq case, if possible). Theorem: The constant folding function for booleans, fold_constants_bexp, is sound. Proof: We must show that b is equivalent to fold_constants_bexp, for all boolean expressions b. Proceed by induction on b. We show just the case where b has the form BEq a₁ a₂. In this case, we must show There are two cases to consider:

• First, suppose fold_constants_aexp a₁ = ANum n₁ and fold_constants_aexp a₂ = ANum n₂ for some n₁ and n₂.
  In this case, we have
      fold_constants_bexp (BEq a₁ a₂)
    = if beq_nat n₁ n₂ then BTrue else BFalse
  and
      beval st (BEq a₁ a₂)
    = beq_nat (aeval st a₁) (aeval st a₂).
  By the soundness of constant folding for arithmetic expressions (Lemma fold_constants_aexp_sound), we know
      aeval st a₁
    = aeval st (fold_constants_aexp a₁)
    = aeval st (ANum n₁)
    = n₁
  and
      aeval st a₂
    = aeval st (fold_constants_aexp a₂)
    = aeval st (ANum n₂)
    = n₂,
  so
      beval st (BEq a₁ a₂)
    = beq_nat (aeval a₁) (aeval a₂)
    = beq_nat n₁ n₂.
  Also, it is easy to see (by considering the cases n₁ = n₂ and n₁ ≠ n₂ separately) that
      beval st (if beq_nat n₁ n₂ then BTrue else BFalse)
    = if beq_nat n₁ n₂ then beval st BTrue else beval st BFalse
    = if beq_nat n₁ n₂ then true else false
    = beq_nat n₁ n₂.
  So
      beval st (BEq a₁ a₂)
    = beq_nat n₁ n₂.
    = beval st (if beq_nat n₁ n₂ then BTrue else BFalse),
  as required.
• Otherwise, one of fold_constants_aexp a₁ and fold_constants_aexp a₂ is not a constant. In this case, we must show
      beval st (BEq a₁ a₂)
    = beval st (BEq (fold_constants_aexp a₁)
                    (fold_constants_aexp a₂)),
  which, by the definition of beval, is the same as showing
      beq_nat (aeval st a₁) (aeval st a₂)
    = beq_nat (aeval st (fold_constants_aexp a₁))
              (aeval st (fold_constants_aexp a₂)).
  But the soundness of constant folding for arithmetic expressions (fold_constants_aexp_sound) gives us
    aeval st a₁ = aeval st (fold_constants_aexp a₁)
    aeval st a₂ = aeval st (fold_constants_aexp a₂),
  completing the case. ☐

(Doing induction when there are a lot of constructors makes specifying variable names a chore, but Coq doesn't always choose nice variable names. We can rename entries in the context with the rename tactic: rename a into a₁ will change a to a₁ in the current goal and context.)

The only interesting case is when both a₁ and a₂ become constants after folding

☐

Exercise: 3 stars (fold_constants_com_sound)

Complete the WHILE case of the following proof.

(If the optimization doesn't eliminate the if, then the result is easy to prove from the IH and fold_constants_bexp_sound.)

☐

Soundness of (0 + n) Elimination, Redux

Exercise: 4 stars, advanced, optional (optimize_0plus)

Recall the definition optimize_0plus from the Imp chapter: Note that this function is defined over the old aexps, without states. Write a new version of this function that accounts for variables, plus analogous ones for bexps and commands: Prove that these three functions are sound, as we did for fold_constants_*. Make sure you use the congruence lemmas in the proof of optimize_0plus_com — otherwise it will be long! Then define an optimizer on commands that first folds constants (using fold_constants_com) and then eliminates 0 + n terms (using optimize_0plus_com).

• Give a meaningful example of this optimizer's output.
• Prove that the optimizer is sound. (This part should be very easy.)

☐

Proving That Programs Are Not Equivalent

Suppose that c₁ is a command of the form X ::= a₁;; Y ::= a₂ and c₂ is the command X ::= a₁;; Y ::= a₂', where a₂' is formed by substituting a₁ for all occurrences of X in a₂. For example, c₁ and c₂ might be: Clearly, this particular c₁ and c₂ are equivalent. Is this true in general? We will see in a moment that it is not, but it is worthwhile to pause, now, and see if you can find a counter-example on your own. Here, formally, is the function that substitutes an arithmetic expression for each occurrence of a given variable in another expression:

And here is the property we are interested in, expressing the claim that commands c₁ and c₂ as described above are always equivalent.

Sadly, the property does not always hold. Theorem: It is not the case that, for all i₁, i₂, a₁, and a₂, Proof: Suppose, for a contradiction, that for all i₁, i₂, a₁, and a₂, we have Consider the following program: Note that where st₁ = { X ↦ 1, Y ↦ 1 }. By our assumption, we know that so, by the definition of cequiv, we have But we can also derive where st₂ = { X ↦ 1, Y ↦ 2 }. Note that st₁ ≠ st₂; this is a contradiction, since ceval is deterministic! ☐

Exercise: 4 stars, optional (better_subst_equiv)

The equivalence we had in mind above was not complete nonsense — it was actually almost right. To make it correct, we just need to exclude the case where the variable X occurs in the right-hand-side of the first assignment statement.

Using var_not_used_in_aexp, formalize and prove a correct verson of subst_equiv_property.

☐

Exercise: 3 stars, optional (inequiv_exercise)

Prove that an infinite loop is not equivalent to SKIP

☐

Extended Exercise: Nondeterministic 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 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 nondeterministic 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, nondeterministically. For example, after executing the program: 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 nondeterministic code. In a sense, a variable on which we do HAVOC roughly corresponds to an unitialized variable in a low-level language like C. 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'').

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

Exercise: 2 stars (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?

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

☐ Finally, we repeat the definition of command equivalence from above:

Let's apply this definition to prove some nondeterministic programs equivalent / inequivalent.

Exercise: 3 stars (havoc_swap)

Are the following two programs equivalent?

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

☐

Exercise: 4 stars, optional (havoc_copy)

Are the following two programs equivalent?

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

☐ 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 nondeterminism, like Himp, some programs always terminate, some programs always diverge, and some programs can nondeterministically terminate in some runs and diverge in others. The final part of the following exercise illustrates this phenomenon.

Exercise: 5 stars, advanced (p1_p2_equiv)

Prove that p₁ and p₂ are equivalent. In this and the following exercises, try to understand why the cequiv definition has the behavior it has on these examples.

Intuitively, the programs have the same termination behavior: either they loop forever, or they terminate in the same state they started in. We can capture the termination behavior of p₁ and p₂ individually with these lemmas:

You should use these lemmas to prove that p₁ and p₂ are actually equivalent.

☐

Exercise: 4 stars, advanced (p3_p4_inquiv)

Prove that the following programs are not equivalent.

☐

Exercise: 5 stars, advanced, optional (p5_p6_equiv)

☐

Additional Exercises

Exercise: 4 stars, optional (for_while_equiv)

This exercise extends the optional add_for_loop exercise from the Imp chapter, where you were asked to extend the language of commands with C-style for loops. Prove that the command: is equivalent to:

☐

Exercise: 3 stars, optional (swap_noninterfering_assignments)

(Hint: You'll need functional_extensionality for this one.)