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 traditional 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 rid 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 either exploit evaln_inv_eval or to provide an explicit intermediate postcondition for the subterm t₁ that revers to Q₁.

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.

In prior chapters, we defined a Separation Logic triple, written triplen t H Q, by quantifying over the "rest of the word". Concretely, we used the definition ∀ (H':hprop), hoare t (H \* H') (Q \*+ H'). Doing so was necessary because the definition we had for hoare did not satisfy the frame rule. It turns out that hoaren does satisfy the frame rule. Thus, we can define Separation Logic triples directly as the predicate hoaren.

The most important step of the proof is to argue that evaln is stable by extension with a disjoint piece of heap. This proof is by induction. The most (and only) interesting step is that of allocation. In a derivation built using evaln_ref, we are given an assumption about all locations p fresh from h₁. What we are trying to build is a fact mentioning all locations p fresh from h₁ \u h₂. We are thus restricting the set of p that can be considered for allocation, hence the result holds.

From evaln_frame, we can derive the standard frame rule for triplen.

Other structural rules

Rules for term constructs

Rules for primitive operations

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

We can check the standard equivalence (H ==> wp t Q) ↔ (triple t H Q), for the predicates wpn and triplen.

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 wpn and wpn.

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 judgment wpn. Structural rules

Derived structural rules

Rules for term constructs

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

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

Consider a configuration (s,t), where t is not a value. If this configuration cannot take any reduction step, it is said to be "stuck". The judgment evals s t s' t' corresponds to the reflexive-transitive closure of step. Concretely, this judgment asserts that the configuration (s,t) can reduce in zero, one, or several evals to (s',t').

Small-Step Characterization of evalns: Attempts

For a non-determinstic language, evals s t s' t' asserts that there exists one possible evaluation from (s,t) to (s',t'). This judgment says nothing about all other possible evaluations. On the contrary, the predicate evaln s t Q, introduced earlier in this chapter, says something about all possible evaluations. More precisely, evaln s t Q asserts that all possible evaluations of (s,t) reach a final configuration satisfying the postcondition Q. We are thus interested in defining a judgment of the form evalns s t Q, that is logically equivalent to evaln s t Q, but whose definition is based on the small-step semantics. In the particular case of a deterministic semantics, we could define evalns s t Q in terms of the transitive evaluation relation evals as follows.