More Details

This chapter develops the soundness proof for wpgen. The key theorem asserts that, for any term and and postcondition, wpgen (on an empty substitution context) yields a formula that entails wp. Formally: wpgen nil t Q ==> wp t Q. The present "more details" section contains the proof of this theorem. The "optional material" section details the proofs of two technical lemmas related to permutation of substitutions. This chapter may be safely skipped.

Definition of the Predicate formula_sound

The soundness theorem that we aim to establish for wpgen is:
    Parameter wpgen_sound : ∀ E t Q,
      wpgen E t Q ==> wp (isubst E t) Q. Before entering into the details of the proof, let us reformulate the statement of the soundness theorem to make proof obligations and induction hypotheses easier to read. To that end, we introduce the predicate formula_sound t F, read "F is a formula sound for t". It asserts that F is a weakest-precondition style formula that entails wp t. Formally:

Using formula_sound, the soundness theorem for wpgen is reformulated as follows.
    Parameter wpgen_sound : ∀ E t,
      formula_sound (isubst E t) (wpgen E t). The soundness theorem wpgen_sound is proved by induction on t. Each case of this inductive proof corresponds to a term construct. For each term construct, we need to exploit two lemmas. The first lemma, common to all term constructs, is called mkstruct_sound, and is used to argue that the presence of mkstruct in the definition of wpgen is sound. The second lemma is specific to the term construct. For example, wpgen_sound_seq is of the form formula_sound (trm_seq t₁ t₂) (wpgen_seq F₁ F₂). We next explain the details of how to state and prove wpgen_sound_seq, then present the other auxiliary lemmas useful for completing the proof by induction of wpgen_sound.

Soundness for the Case of Sequences

Consider the soundness theorem wpgen_sound and let us specialize it to the particular case where t is of the form trm_seq t₁ t₂. The corresponding statement is:

Let us ignore mkstruct for a minute -- that is, pretend that wpgen is defined without mkstruct. Under this assumption, wpgen E (trm_seq t₁ t₂) evaluates to wpgen_seq (wpgen E t₁) (wpgen E t₂). Besides, the expression isubst E (trm_seq t₁ t₂) evaluates to trm_seq (isubst E t₁) (isubst E t₂). Therefore, the soundness statement to establish can be reformulated as:

By induction hypothesis, we can assume that wpgen E t₁ is a sound formula for isubst E t₁, and likewise wpgen E t₂ is a sound formula for isubst E t₂. Thus, what we actually will need to prove as part of the induction is:

In the above statement, let us abstract isubst E t₁ as t₁' and wpgen t₁ as F₁, and similarly isubst E t₂ as t₂' and wpgen t₂ as F₂. The statement reformulates as:

This statement captures the essence of the correctness of the definition of wpgen_seq. Now let's prove it.

Soundness for the Other Term Constructs

Similarly, for every other language construct, we state and prove a lemma about formula_sound. The reader may skip over the proof details. What is most interesting here is the pattern followed by the statements.

Additional lemmas establishing the soundness of a version of wpgen that does not recurse inside local function definitions.

Soundness of the Predicate Transformer mkstruct

Above, we have ignored the existence of mkstruct at the head of formulae produced by wpgen. We next show that the insertion of mkstruct in formulae preserves their soundness. In other words, if the formula F is a valid weakest precondition for t, then so is mkstruct F.
    Lemma mkstruct_sound : ∀ t F,
      formula_sound t F →
      formula_sound t (mkstruct F). In order to prove this result, we first need to show that mkstruct is a predicate transformer that does not affect the meaning of any formula of the form wp t. Intuitively, mkstruct adds support for applying structural rules of Separation Logic; but a formula wp t inherently satisfies all the structural rules; hence wrapping wp t inside a call to mkstruct does not increase (nor decrease) its expressive power.

We are now ready to prove the desired result mkstruct_sound.

Another, lower-level proof for the same result reveals the definition of mkstruct and exploits the consequence-frame rule for wp.

Another interesting property of mkstruct is its idempotence property, that is, it is such that mkstruct (mkstruct F) = mkstruct F. Idempotence asserts that applying the predicate mkstruct more than once does not provide more expressiveness than applying it just once. Intuitively, idempotence reflects in particular the fact that two nested applications of the rule of consequence can always be combined into a single application of that rule (due to the transitivity of entailment); and that, similarly, two nested applications of the frame rule can always be combined into a single application of that rule (framing on H₁ then framing on H₂ is equivalent to framing on H₁ \* H₂).

Exercise: 3 stars, standard, especially useful (mkstruct_idempotent)

Complete the proof of the idempotence of mkstruct. Hint: leverage xpull and xsimpl.

Lemmas Capturing Properties of Iterated Substitutions

In the soundness proof for wpgen, we need to exploit two basic properties of the iterated substitution function isubst. The first property asserts that the substitution for the empty context is the identity. This result is useful to beautify the final statement of the soundness theorem.

The second property asserts that the substitution for a context (x,v)::E is the same as the substitution for the context rem x E followed with the substitution of subst x v. This second property is needed to handle the case of let-bindings.

The proofs for these two lemmas is fairly technical and of limited interest for the course. They can be found in the "optional material" near the end of this chapter.

Main Induction for the Soundness Proof of wpgen

At last, we are ready to establish the soundness of wpgen E t. As previously announced, the proof is by structural induction on t. For each term construct, the proof has two steps:

• first, invoke the lemma mkstruct_sound to justify soundness of the leading mkstruct produced by wpgen,
• second, invoke the the soundness lemma specific to that term construct, e.g. wpgen_seq_sound for sequences.

Statement of Soundness of wpgen for Closed Terms

For a closed term t, the context E is instantiated as nil, and isubst nil t simplifies to t. We derive the main soundness statement for wpgen.

The lemma triple_of_wpgen triggers the initial evaluation of wpgen for a given program t that appears in a triple.

The lemma triple_app_fun_from_wpgen is at the core of the implementation of the tactic xwp. It is a specialized version of triple_of_wpgen] specialized for establishing a triple for a function application. In essence, this lemma is a reformulation of the rule triple_app_fun, but triggering an evaluation of wpgen for the body of the function.

The lemma triple_app_fix_from_wpgen is similar but handles recursive functions.

Optional Material

Proofs of Properties of Iterated Substitution

Recall that isubst E t denotes the multi-substitution in the term t of all bindings form the association list E. The soundness proof for wpgen and the proof of its corollary triple_app_fun_from_wpgen rely on two key properties of iterated substitutions, captured by the lemmas called isubst_nil and isubst_rem, which we state and prove next.
    isubst nil t = t

    subst x v (isubst (rem x E) t) = isubst ((x,v)::E) t The first lemma is straightforward by induction. The TLC tactic fequals is an enhanced variant of Coq's tactic f_equal.

The second lemma is much more involved to prove. We introduce the notion of "two equivalent contexts" E₁ and E₂, and argue that substitution for two equivalent contexts yields the same result. We then introduce the notion of "contexts with disjoint domains", and argue that if E₁ and E₂ are disjoint then isubst (E₁ ++ E₂) t = isubst E₁ (isubst E₂ t). Before we start, we describe the tactic case_var, which helps with the case_analyses on variable equalities, and we prove an auxiliary lemma that describes the result of a lookup on a context from which a binding has been removed. It is defined in the file LibSepVar.v as:
    Tactic Notation "case_var" :=
      repeat rewrite var_eq_spec in *; repeat case_if. The tactic case_var* is a shorthand for case_var followed with automation (essentially, eauto). A key auxiliary lemma relates subst and isubst.

A lemma about the lookup in a removal.

A lemma about the removal over an append.

The definition of equivalent contexts.

The fact that removal preserves equivalence.

The fact that substitution for equivalent contexts yields equal results.

The definition of disjoint contexts.

Removal preserves disjointness.

Lookup in the concatenation of two disjoint contexts E₁ and E₂ is equivalent to a lookup in E₁ if it succeeds, or a lookup in E₂ otherwise.

The key induction shows that isubst distributes over context concatenation.

The next lemma asserts that the concatenation order is irrelevant in a substitution if the contexts have disjoint domains.

At last, we derive the desired property of isubst.

We also prove the variant lemma which is useful for handling recursive functions in the soundness proof for wpgen.