First Pass

In previous chapters, we have considered a quasi-deterministic language; only the addresses of allocated data could vary between two executions of a same term starting in a same state. In this chapter, we discuss the interpretation of Separation Logic triples in the more general case of non-deterministic languages. To that end, we extend the language with a new primitive operator that produces a random number: the term val_rand n non-deterministically evaluates to an integer between 0 inclusive and n exclusive. This chapter is organized as follows:

• Statement of a big-step semantics for non-deterministic languages
• Proof of reasoning rules for triples
• Proof of reasoning rules in weakest-precondition style
• Bonus section: definition of triples for non-deterministic languages with respect to small-step semantics.

For simplicity, we omit from the semantics the treatment of non-recursive functions, which can be encoded using recursive functions; and, likewise, omit the treatment of sequences, which can be encoded using let-bindings.

Non-Deterministic Big-Step Semantics: the Predicate evaln

Previously, we worked with the big-step judgment eval s t s' v, which relates one input state (and term) with one output state (and value). This judgment is well-suited for a deterministic semantics, because one input state leads to at most one result. For a non-deterministic semantics, however, we need to relate one input with a set of possible results. In Coq, a set of output states can be represented as a set of pairs made of a state and a value, that is, (state*val)->Prop. This type is isomorphic to the type val→state→Prop, which corresponds exactly to the type of postconditions val→hprop. Thus, we are interested in setting up a judgment that relates an "input configuration", described by a state and a term, with a postcondition describing the set of possible "output configurations". The non-deterministic big-step judgment therefore takes the form evaln s t Q, and relates an input state s and a term t with a postcondition Q. An output configuration consists of an output state s' and an output value v that, together, satisfy the postcondition Q, in the sense that Q v s' holds. In the context of program verification, we are not so much interested in characterizing exactly the set of all output configurations reachable by the program, but mainly interested in showing that all output configurations satisfy a desired postcondition Q. For this reason, it is perfectly fine for the set of configurations described by Q to over- approximate the set of configurations actually reachable by the program. We'll explain later on how to characterize the set of output configurations in a precise manner. The judgment evaln s t Q is defined inductively. It asserts that every possible execution starting from configuration (s,t) satisfies the postcondition Q. The definition of evaln is adapted from that of eval. Four cases are particularly interesting.

• Consider the case of a value. The judgment evaln s t Q asserts that the value v in the state s satisfies the postcondition Q. The premise for deriving that judgment is thus that Q v s must hold.
• Consider the case of a let-binding. let x = t₁ in t₂. The first premise of the evaluation rule describes the evaluation of the subterm t₁. It takes the form evaln s t₁ Q. The second premise describes the evaluation of the the continuation subst x v₁ t₂ in a state s₂, where the value v₁ and the state s₂ correspond to a configuration that can be produced by t₁. In other words, v₁ and s₂ are assumed to satisfy Q₁ v₁ s₂.
• Consider the case of a non-deterministic term: val_rand n, evaluated in a state s. The first premise of the rule requires n > 0. The second premise requires that, for any value n₁ that val_rand n may evaluate to (that is, such that 0 ≤ n₁ < n), the configuration made of n₁ and s satisfies the postcondition Q, in the sense that Q n₁ s holds.
• Consider the case of an allocation: val_ref v, evaluated in a state s. The premise of the rule asserts that the postcondition Q should hold of any configuration made of a fresh location p and a state s' obtained as the update of s with a binding from p to v.

Observe that evaln s t Q cannot hold if there exists one possible execution of (s,t) that runs into an error, i.e., that reaches a configuration that is stuck. This property reflects on the fact that the judgment evaln asserts that every possible execution terminates safely. Observe also that evaln is covariant in the postcondition: if evaln s t Q₁ holds, and Q₂ is weaker than Q₁, then evaln s t Q₂ also holds. This property reflects on the fact that it is always possible to further over-approximate the set of possible results.

The judgment evaln s t Q can interpreted in at least five different ways:

• The judgment evaln may be viewed as the natural generalization of eval, generalizing from one output to a set of possible output.
• The judgment evaln may be viewed as an inductive definition of a weakest-precondition judgment. Interestingly, if we swap the order of the arguments to evaln t Q s, then the partial application evaln t Q has type hprop, and its interpretation matches exactly that of a weakest precondition for a Hoare triple. We'll formalize this claim further on in this chapter, and we'll point out shortly afterwards the difference between the rules that define evaln and the tradition weakest-precondition reasoning rules.
• The judgment evaln may be viewed as a CPS-version of the predicate eval. Indeed, The output of eval, made of an output value and an output state, are "passed on" to the continuation Q.
• The judgment evaln may be viewed as a particular form of denotational semantics for the language. Each program is interpreted as (i.e., mapped to) a set of mathematical objects, which "simply" consists of pairs of states and "syntactic" values. In particular, functions are interpreted as plain pieces of syntax (not as functions over Scott domains, as usually done).
• The judgment evaln may be viewed as a generalized form of a typing relation. To make the analogy clear, let us adapt the definition of evaln in two ways, and focus on the evaluation rule for let-bindings. First, let us get read of the state, i.e., consider a language without side-effects, for simplicity.
       evaln t₁ Q₁ →
       (∀ v₁, Q₁ v₁ → evaln (subst x v₁ t₂) Q) →
       evaln (trm_let x t₁ t₂) Q Second, let us switch from a substitution-based semantics to an environment-based semantics---nothing but change of presentation.
       evaln E t₁ Q₁ →
       (∀ v₁, Q₁ v₁ → evaln ((x,v₁)::E) t₂ Q) →
       evaln E (trm_let x t₁ t₂) Q Now, let's consider a typing property. For example, expressing that a term has type int amounts to asserting that this term produces a value v of the form val_int n for some n. This property may be captured by the postcondition fun v ⇒ ∃ n, v = val_int n. Let us compare the previous rule with the traditional typing rule shown below.
       typing E t₁ Q₁ →
       typing ((x,Q₁)::E) t₂ Q →
       typing E (trm_let x t₁ t₂) Q The only difference is that the evaluation rule maps x to any value v₁ such that v₁ has type Q₁, whereas the typing rule directly maps x to the type Q₁. The two presentations are thus essentially equivalent.

In what follows, we discuss the difference between the presentation of the judgment evaln, and the rules that define a weakest precondition. We focus on the particular case of a let-binding.

Exercise: 1 star, standard, optional (evaln_let')

The rule evaln_let shares similarities with the statement of the weakest-precondition style reasoning rule for let-bindings. Prove the following alternative statement, with a wp-style flavor.

Exercise: 2 stars, standard, optional (evaln_let_of_evaln_let')

Reciprocally, prove that the statement considered in the inductive definition of evaln is derivable from evaln_let'. More precisely, prove the statement below by using evaln_let' and evaln_conseq.

One way wonder whether we could have used the wp-style formulation of the semantics of let-bindings directly in the definition of evaln. The answer is negative. Doing so would lead to an invalid inductive definition, involving a "non strictly positive occurrence". To check it out, uncomment the definition below to observe Coq's complaint.
  Inductive evaln' : state → trm → (val→state→Prop) → Prop :=
    | evaln'_let : ∀ Q₁ s₁ x t₁ t₂ Q,
       evaln' s₁ t₁ (fun v₁ s₂ ⇒ evaln' s₂ (subst x v₁ t₂) Q) →
       evaln' s₁ (trm_let x t₁ t₂) Q.

Interpretation of evaln w.r.t. eval

Given that evaln describes "all possible executions" and that eval describes "one possible execution", there must be formal relationships between the two predicates. These relationships are investigated next. Recall the big-step evaluation judgment eval. It is the same as before, only extended with evaluation rule for the random number generator, namely eval_rand.

The judgment evaln s t Q asserts that any possible execution of the program (t,s) terminates on an output satisfying the postcondition Q. Thus, if one particular execution terminates on the output (s',v), as described by the judgment eval s t s' v, it must be the case that Q v s' holds. This result is formalized by the following lemma.

Exercise: 3 stars, standard, optional (evaln_inv_eval)

Assume evaln s t Q to hold. Prove that the postcondition Q holds of any output that (s,t) may evaluate to according to the judgment eval.

The judgment evaln s t Q asserts that any possible execution of the program (t,s) terminates on an output satisfying the postcondition Q. This judgment implies, in particular, that there exists at least one such execution, described by a judgment of the form eval s t s' v, where v and s' satisfy the postcondition Q. This second result is formalized by the following lemma.

Exercise: 4 stars, standard, especially useful (evaln_inv_exists_eval)

Assume evaln s t Q to hold. Prove that there exists an output (s',v) that (s,t) may evaluate to according to the judgment eval, and that this output satisfies Q. Hint: the proof may be carried out either with or without leveraging the lemma evaln_inv_eval, proved above. Hint: for the case eval_ref, use the following line to assert the existence of a fresh location: forwards* (p&D&N): (exists_fresh null s)..

The judgment evaln s t Q associates with a program configuration (s,t) an over-approximation of its possible output configurations, described by Q. For the purpose of defining of Hoare triple, working with over-approximation is perfectly fine. In other contexts, however, it might be interesting to characterize exactly the set of output configurations. The set of results to which a program (s,t) may evaluate is precisely characterized by the predicate fun v s' ⇒ eval s t s' v. Let post s t denote exactly that predicate.

The judgment evaln s t (post s t) essentially captures the safety of the program (s,t): it asserts that all possible executions terminate without error. Let us prove that post s t corresponds to the smallest possible post-condition for evaln. In other words, assuming that evaln s t Q holds for some Q, we can prove that evaln s t (post s t) holds, and that the entailment post s t ===> Q holds. This entailment captures the fact that post s t denotes a smaller set of results than Q. Note that evaln s t (post s t) does not hold for a program for which one particular execution may diverge or get stuck.

Exercise: 5 stars, standard, especially useful (evaln_post_of_evaln)

Prove the fact that if evaln s t Q holds for some Q, then it holds for the smallest postcondition, namely post s t. Hint: in the let-binding case, you'll need to guess an appropriate intermediate postcondition for the subterm t₁.

Exercise: 2 stars, standard, especially useful (evaln_inv_post_qimpl)

Prove the fact that if evaln s t Q holds, then post s t ===> Q, i.e. the smallest-possible postcondition entails the postcondition Q. Hint: the proof is only one line long.

Triples for Non-Deterministic Big-Step Semantics

A Hoare triple, written hoaren t H Q, asserts that, for any input state s satisfying the precondition H, all executions of t in that state s terminate and produce an output satisfying the postcondition Q.

A Separation Logic triple, written triplen t H Q, asserts that the term t satisfies a Hoare triple with precondition H \* H' and postcondition Q \* H', for any heap predicate H' describing the "rest of the word". Compared with the definition of triple, we simply replaced hoare with hoaren.

Triple-Style Reasoning Rules for a Non-Deterministic Semantics.

To derive reasoning rules for triples, we proceed in two steps, just as in the previous chapters: first, we establish rules for hoaren, then we derive rules for triplen. For the first part, the proofs are very similar to those form previous chapters. For the second part, the proofs are exactly the same as in the previous chapters. Structural rules

Rules for term constructs

Rules for primitive operations

The proofs of reasoning rules for triplens are exactly the same as in the chapter Rules. For example, we show below the proof of the reasoning rule for let-bindings.

Statements and proofs of reasoning rules for other term constructs can be directly adapted from those in the file LibSepReference.

More Details

Weakest-Precondition Style Presentation.

In chapter WPsem, we discussed several possible definitions of the weakest-precondition operator, namely wp, in Separation Logic. In this chapter, we present yet another possible definition, based on the judgment evaln. Consider the judgment evaln s t Q. Assume the arguments were reordered, yielding the judgment evaln t Q s. Consider now the partial application evaln t Q. This partial application has type state→Prop, that is, hprop. This predicate evaln t Q denotes a predicate that characterizes the set of input states s in which the evaluation (or, rather, any possible evaluation) of the term t produces an output satisfying Q. It thus corresponds exactly to the notion of weakest precondition for Hoare Logic. The judgment hoarewpn t Q, defined below, simply reorder the arguments of evaln so as to produce this weakest-precondition operator. Note that this is a Hoare Logic style predicate, which talks about the full state.

On top of hoarewpn, we can define the Separation Logic version of weakest precondition, written wpn t Q. At a high level, wpn extends hoarewpn with a description of "the rest of the world". More precisely, wpn t Q describes a heap predicate, that, if extended with a heap predicate H describing the rest of the world, yields the weakest precondition with respect to the postcondition Q \*+ H, that is, Q extended with H.

This definition is associated with the following introduction rule, which reads as follows: to prove H ==> wpn t Q, which asserts that t admits H as precondition and Q as postcondition, it suffices to prove that, for any H' describing the rest of the world, the entailment H \* H'==> hoarewpn t (Q \*+ H') holds, asserting that the term t admits, in Hoare logic, the precondition H \* H' and the postcondition Q \*+ H'.

Exercise: 4 stars, standard, especially useful (wpn_equiv)

Prove the standard equivalence (H ==> wp t Q) ↔ (triple t H Q) to relate the predicates wpn and triplen. Hint: using lemma wpn_of_hoarewpn can be helpful.

Remark: as mentioned in the chapter WPsem, it is possible to define the predicate triplen t H Q as H ==> wpn t Q, that is, to define triplen as a notion derived from hoarewpn and wpn.

Hoare Logic WP-Style Rules for a Non-Deterministic Semantics.

Given that the semantics expressed by the predicate evaln has a weakest- precondition flavor, there are good chances that deriving weakest- precondition style reasoning rules from evaln could be even easier than deriving the rules for triplen. Thus, let us investigate whether this is indeed the case, by stating and proving reasoning rules for the judgments hoarewpn and wpn. We begin with rules for hoarewpn. Structural rules

Rules for term constructs

Rules for primitives. We state their specifications following the presentation described near the end of chapter Wand.

Separation Logic WP-Style Rules for a Non-Deterministic Semantics.

In the previous section, we established reasoning rules for hoarewpn. Based on these rules, we are ready to derive reasoning rules for wpn. Structural rules

Rules for term constructs

Exercise: 4 stars, standard, especially useful (wpn_let)

Derive the reasoning rule wpn_let from hoarewpn_let.

Rules for primitives.

Rules for primitives, alternative presentation using triples.

Exercise: 4 stars, standard, optional (wpn_rand_of_triplen_rand)

The proof of lemma triplen_rand shows that a triple-based specification of val_rand is derivable from a wp-style specification. In this exercise, we aim to prove the reciprocal. Concretely, prove the following specification by exploiting wpn_rand. Hint: make use of wpn_equiv.

Optional Material

So far, this chapter has focused on handling non-determinism in the context of using a big-step semantics. In this bonus section, we investigate the treatment of non-determinism using a small-step semantics. Moreover, we establish equivalence proofs relating (non-deterministic) small-step and big-step semantics.

Interpretation of evaln w.r.t. eval and terminates

The predicate terminates s t asserts that all executions of the configuration t/s terminate---none of them diverges or get stuck. Its definition is a simplified version of evaln where all occurences of Q are removed. In the rule for let-bindings, namely terminates_let, the quantification over the configuration v₁/s₂ is done by refering to the big-step judgment eval.

Exercise: 5 stars, standard, especially useful (evaln_iff_terminates_and_post)

Prove that evaln s t Q is equivalent to the conjunction of terminates s t and to a partial correctness result asserting that if an evaluation of t/s terminates on some result then this result satisfies Q.

Let Any denotes the postcondition that accepts any result.

Exercise: 2 stars, standard, especially useful (terminates_iff_evaln_any)

Prove that terminates s t is equivalent to evaln s t Any. Hint: exploit evaln_iff_terminates_and_post.

Small-Step Evaluation Relation

The judgment step s t s' t' describes the small-step reduction relation: it asserts that the program configuration (s,t) can take one reduction step towards the program configuration (s',t'). Its definition, shown below, is standard.