The file LibSepReference.v contains definitions that are essentially the same as those from Hprop.v and Himpl.v, but with one key difference: LibSepReference makes the definition of Separation Logic operators opaque. This chapter and the following ones import LibSepReference.v instead of Hprop.v and Himpl.v. As a result, we cannot unfold the definition of hstar, hpure, etc. any more. To reason, we must instead use the introduction and elimination lemmas, such as hstar_intro and hstar_elim. These lemmas enforce abstraction, ensuring that the proofs do not depend on the particular choice of the definitions used for constructing Separation Logic. For example, we should not depend on whether \[P] is internally implemented as fun h ⇒ h = empty ∧ P or as \∃ (p:P), \[].

First Pass

In chapter Hprop, we formalized heap predicates, of type hprop, and several operators on them: \[], \[P], p ~~> v, H₁ \* H₂, Q₁ \*+ H₂, and \∃ x, H. In chapter Himpl, we formalized the heap entailment relations H₁ ==> H₂ and Q₁ ===> Q₂. The goal of the present chapter and the next one is to formalize the definition of triples, written triple t H Q, and the reasoning rules of Separation Logic. More precisely, the present chapter focuses on the definition of triples and the proofs of the "structural rules", which are essential in particular for implementing the tactics xpull and xapp. The structural rules include the "frame rule", which lies at the heart of Separation Logic, as well as the "consequence rule" and two "extraction rules", which admit similar statements as in Hoare Logic. The reasoning rules concerned with term constructs are discussed in the next chapter (Rules). This chapter starts with a formalization of the syntax and the semantics of the programming language we are using for examples. The semantics is axiomatized using a variant of big-step semantics called "omni-big-step semantics". This presentation is well suited for capturing safety and termination in nondeterministic programming languages. Near the end of the chapter, we explain how an omni-big-step semantics can be formally related to a standard small-step semantics. This chapter exploits a few additional TLC tactics to enable concise proofs. Recall from chapter Himpl that applys is an enhanced version of eapply, which takes as argument a lemma or hypothesis, followed by a variable number of arguments, which are fed to the lemma on a first-match basis. For example, applys L x y is equivalent to eapply (L _ _ .. _ x _ _ .. _ _ y _ _ ..) for an appropriate number of underscore symbols. Likewise, the tactics lets, forwards, and specializes can be used to instantiate a lemma or an existing hypothesis:

• lets H: L x y introduces an hypothesis named H, whose statement is the specialization of the lemma L on the arguments x and y. It is equivalent to generalize (L _ _ .. _ x _ _ .. _ _ y); intros H, for the appropriate number of underscore symbols.
• forwards H: L x y is very similar to lets, except that it attempts to instantiate all arguments of L. It is equivalent to generalize (L _ _ .. _ x _ _ .. _ _ y _ _ .. _ _); intros H.
• specializes H x y specializes an existing hypothesis H in place. It is equivalent to lets H₂: H x y; clear H; rename H₂ into H.

The reader will find many occurrences of these tactics in proofs and solutions. However, exploiting these tactics is never required for solving exercises.

Syntax

In what follows, we present the formalization of the syntax of the programming language. This material corresponds to a large subset of the material from the file LibSepReference. Further on in this file, we will want to refer to the definitions from LibSepReference, to avoid having to copy-paste all the construction of Separation Logic operators, which depend on the type state and therefore depend on the type val associated with program values. Hence, we wrap the definitions of syntax presented below inside a module.

Values and Terms

The syntax of our example programming language is described using an abstract syntax tree. Its presentation distiguishes between closed values (i.e., values with no free variables inside) and terms. This presentation simplifies the definition and evaluation of the substitution function. Indeed, since values are always closed, the substitution function never needs to traverse through values. The grammar for values includes the unit value, booleans, integers, locations, functions, recursive functions, and primitive operations. For example, val_int 3 denotes the integer value 3, while val_fun x t denotes the function fun x ⇒ t, and val_fix f x t denotes the function fix f x ⇒ t, which is written let rec f x = t in f in OCaml syntax. For conciseness, we include just a few primitive operations: val_ref, val_get, val_set, and val_free for manipulating the mutable state, val_add to illustrate a simple arithmetic operation, val_div to illustrate a partial operation, and val_rand to illustrate nondeterminism.

The grammar for terms includes values, variables, function definitions, recursive function definitions, function applications, sequences, let-bindings, and conditionals.

Note that trm_fun and trm_fix denote functions that may feature free variables, unlike val_fun and val_fix, which denote closed values. More concretely, in the term trm_fun x t, the term t may refer to the variable x or to other free variables. In contrast, in the term val_fun x t, the only free variable that t may have is x. We will see, below, evaluation rules asserting that trm_fun x t reduces, in the empty context, to val_fun x t. Likewise, trm_fix f x t reduces, in the empty context, to val_fix f x t. At a high level, the term val_fun x t may be thought of as the term trm_fun x t augmented with a proof that this term trm_fun x t is a closed term. The syntax that we consider therefore embeds "proofs that values are closed". Thanks to this presentation, the substitution function subst, which will be presented shortly afterwards, need not recurse through values. Moreover, we never need to manipulate proofs that specific terms are closed. Functions of several arguments are encoded as nested functions (curried functions). For example, the syntax fun x₁ x₂ x₃ ⇒ t used to define a top-level function in the chapters Basic and Repr is encoded as val_fun x₁ (trm_fun x₂ (trm_fun x₃ t)). Observe how the outer constructor asserts that the whole function is a closed value, whereas the inner functions are terms. In particular t may refer to x₁ and x₂, which are free variables for the term trm_fun x₃ t. Likewise, a closed recursive function fix f x₁ x₂ x₃ ⇒ t is encoded as val_fix f x₁ (trm_fun x₂ (trm_fun x₃ t)). Here only the outermost function is recursive (and closed). In the rest of the course, we will focus on functions with a single argument. The treatment of n-ary functions is the topic of a yet-to-be-released chapter.

State

The language we consider is imperative, with primitive functions for manipulating the state. Thus, the statements of the evaluation rules involve memory states. Recall from chapter Hprop that a state is represented as a finite map from location to values. Finite maps are presented using the type fmap. Details of the construction of finite maps may be found in the file LibSepFmap.v. (The construction is beyond the scope of this course, because it leverages dependent pairs to realize the type of finite maps.)

Recall from chapter Hprop that our convention is to write s for a full memory state, of type state, and write h for a piece of memory state, of type heap.

For technical reasons related to the internal representation of finite maps, to enable reading in a state, we need to justify that the grammar of values is inhabited. This property is captured by the following command, whose details are not relevant for understanding the rest of the chapter.

Substitution

The semantics of the evaluation of a program function is described by means of a substitution function, written subst y w t, which replaces all occurrences of a variable y with a value w inside a term t. The substitution function is always the identity on values, because our language only considers closed values. In other words, we define subst y w (trm_val v) = (trm_val v). When it reaches a variable, substitution performs a comparison between two variables. To that end, it exploits the comparison function var_eq x y, which produces a boolean value indicating whether x and y denote the same variable. The remainder of this subsection describes the implementation of the substitution function subst. This operation traverses all other language constructs in a structural manner. It takes care of avoiding "variable capture" when traversing binders: subst y w t does not recurse below the scope of binders whose bound name is equal to y. For example, the result of subst y w (trm_let x t₁ t₂) is trm_let x (subst y w t₁) (if var_eq x y then t₂ else (subst y w t₂)). The auxiliary function if_y_eq, which appears in the definition of subst, helps factorizing the comparisons required to prevent variable capture.

Implicit Types and Coercions

To improve the readability of the evaluation rules below, we take advantage of Coq's implicit types and coercions. First off, we give several Implicit Types declarations. For example, the first command indicates that variables whose name begins with the letter 'b' are, by default, of type bool.

Next, we give a collection of coercions. Coercions correspond to implicit function calls, which aim to make statements more concise. For example, val_loc is declared as a coercion, so that a location p of type loc can be viewed as the value val_loc p where an expression of type val is expected. Likewise, a boolean b may be viewed as the value val_bool b, and an integer n may be viewed as the value val_int n.

The constructor trm_val is also declared as a coercion. Thus, instead of writing trm_val v at a place where a term is expected, we can write just v.

The constructor trm_app is declared as a "Funclass" coercion. This bit of magic enables us to write t₁ t₂ as a shorthand for trm_app t₁ t₂. The idea of associating trm_app as the "Funclass" coercion for the type trm is that if a term t₁ of type trm is applied like a function to an argument, then t₁ should be interpreted as trm_app t₁.

The "Funclass" coercion for trm_app can be iterated. The expression t₁ t₂ t₃ is parsed by Coq as (t₁ t₂) t₃. The first application t₁ t₂ is interpreted as trm_app t₁ t₂. This expression, which itself has type trm, is applied to t₃. Hence, t₁ t₂ t₃ is interpreted as trm_app (trm_app t₁ t₂) t₃.

Loading Definitions from LibSepReference

As announced earlier, we will carry out proofs not with respect to the above definitions, but with respect to the definitions from LibSepReference.v. Concretely, we close the scope of the module Syntax, and re-enter the scope of the definitions from LibSepReference.

Formalizing the Semantics of the Programming Language

Standard Big-Step Semantics

We are now ready to present a formal semantics for the language. To begin with, we present a big-step evaluation judgment, written big s t s' v. This judgment asserts that, starting from state s, the evaluation of the term t terminates in a state s', and produces an output value v. For simplicity, we assume terms to be in "A-normal form": the arguments of applications and of conditionals are restricted to variables and values. Such a requirement does not limit expressiveness, but it simplifies the statement of the evaluation rules. For example, if a source program includes a conditional trm_if t₀ t₁ t₂, then it is required that t₀ be either a variable or a value. This is not a real restriction, because trm_if t₀ t₁ t₂ can always be encoded as let x = t₀ in if x then t₁ else t₂. The big-step judgment is inductively defined as follows.

1. big for values and function definitions. A value evaluates to itself. A term function evaluates to a value function. Likewise for a recursive function.

2. big for function applications. The beta-reduction rule asserts that (val_fun x t₁) v₂ evaluates to the same result as subst x v₂ t₁. Likewise, (val_fix f x t₁) v₂ evaluates to subst x v₂ (subst f v₁ t₁), where v₁ denotes the recursive function itself, that is, val_fix f x t₁.

3. big for structural constructs. A sequence trm_seq t₁ t₂ first evaluates t₁, taking the state from s₁ to s₂, then drops the result of t₁ and evaluates t₂, taking the state from s₂ to s₃. The let-binding trm_let x t₁ t₂ is similar, except that the variable x gets substituted with the result of t₁ inside t₂.

4. big for conditionals. A conditional in a source program is assumed to be of the form if t₀ then t₁ else t₂, where t₀ is either a variable or a value. If t₀ is a variable, then, by the time it reaches an evaluation position, the variable must have been substituted by a value. Thus, the evaluation rule only considers the form if v₀ then t₁ else t₂. The value v₀ must be a boolean value, otherwise evaluation gets stuck. The term trm_if (val_bool true) t₁ t₂ behaves like t₁, whereas the term trm_if (val_bool false) t₁ t₂ behaves like t₂. This behavior is described by a single rule, leveraging Coq's "if" constructor to factor out the two cases.

5. big for primitive stateless operations. For similar reasons, the behavior of applied primitive functions only needs to be described for the case of value arguments. An arithmetic operation expects integer arguments. The addition of val_int n₁ and val_int n₂ produces val_int (n₁ + n₂). The division operation, on the same arguments, produces the quotient n₁ / n₂, under the assumption that the divisor n₂ is non-zero. In other words, if a program performs a division by zero, then it cannot satisfy the big judgment. The random number generator val_rand n produces an integer n₁ in the range from 0 (inclusive) to n (exclusive).

6. big for primitive operations on memory. The term val_ref v allocates a fresh cell with contents v and returns the location, p, of the new cell. This location must not be previously in the domain of the store s. The term val_get (val_loc p) reads the value in the store s at location p. The location must be bound to a value in the store, otherwise evaluation is stuck. The term val_set (val_loc p) v updates the store at a location p assumed to be bound in the store s. The operation modifies the store and returns the unit value. The term val_free (val_loc p) deallocates the cell at location p.

Omni-Big-Step Semantics

A triple of the form triple t H Q aims to capture the property that, for any input state s satisfying the precondition H, any possible execution of the program starting from the initial configuration (s,t) will terminate and reach a final configuration satisfying the postcondition Q. However, the standard big-step judgment, big s t s' v, only describes one possible execution. Using this judgment, we can capture the property that "if a particular execution terminates, then it reaches a final configuration satisfying Q". But we do not capture the property that "all possible executions terminate". The omni-big-step judgment is a generalization of the standard big-step judgment that allows capturing properties of all possible executions. The judgment takes the form eval s t Q, where Q denotes a set of final configurations. It captures the fact that all possible executions starting on the configuration (s,t) terminate safely and reach a final configuration in the set Q. We can think of Q as a set of pairs made of values and a state. Equivalently, we can think of Q as a postcondition, of type val→state→Prop.

The inductive definition below defines the omni-big-step judgment, which has the form eval s t Q, where Q is a postcondition. The generalization from standard-big-step to omni-big-step follows a regular pattern, which should become apparent while stepping through the rules.

1. eval for values and function definitions. The judgment eval s v 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.

2. eval for function applications. Consider a function v₁ of the form val_fun x t₁. The term trm_app v₁ v₂ terminates with postcondition Q provided that the substituted term subst x v₂ t₁ terminates with postcondition Q. Hence, to prove eval s₁ (trm_app v₁ v₂) Q, we must establish eval s₁ (subst x v₂ t₁) Q.

3. eval for sequencing. Consider a sequence trm_seq t₁ t₂ in a state s. What is the requirement for this configuration to terminate with postcondition Q? First, we need the evaluation of t₁ in s to terminate. Let Q₁ be (an overapproximation of) the set of possible results for the execution of (s,t₁). Then, to prove that the sequence trm_seq t₁ t₂ terminates in Q, we need to show that, for any intermediate state s₂ satisfying Q₁, the evaluation of t₂ terminates with postcondition Q. The case of let-bindings is similar, only with an additional substitution.

4. eval for conditionals. The term (trm_if (val_bool b) t₁ t₂) has the same behaviors as the term t₁ when b is true, and as the term t₂ when b is false.

5. eval for primitive stateless operations. The judgment eval s (val_add n₁ n₂) Q asserts that the pair of the state s and the value n₁+n₂ produced by the addition operation satisfies the postcondition Q. Hence, the premise is Q (val_int (n₁ + n₂)) s. Nondeterministic constructs are more interesting. The rule eval_rand gives the condition under which the term val_rand n, evaluated in a state s, produces an output satisfying Q. 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. Formally: ∀ n₁, (0 ≤ n₁ < n) → (Q n₁ s).

6. eval for primitive operations on memory. The most interesting case here is that of allocation, which is nondeterministic. For val_ref v, evaluated in a state s, to produce a configuration in Q, we require that, for any location p that is "fresh" for the state s, the pair made of p and "s extended with a binding from p to v" satisfies Q.

Note that, given eval s t Q, it is *not* necessarily the case that Q is the exact set of configurations that are reachable from (s,t); it may rather be an overapproximation of that set. Trying to set up an inductive definition that relates (s,t) with exactly its set of reachable configurations would introduce unnecessary complications. Note, also, that eval s t Q will not hold if there exist one or more executions of (s,t) that run into an error, i.e., that reach a configuration that is stuck. To see why, consider a program of the form let n = rand 10 in (f n). When applying the rule eval_let to this program, the postcondition Q₁ associated with rand 10 must include all integers in the range 0..9. The second premise of the rule eval_let is of the form ∀ v₁ s₂, Q₁ v₁ s₂ → eval s₂ (subst x v₁ t₂) Q. In our specific example, this premise asserts that for any result in Q₁, which includes all integers n in the range 0..9, it is the case that the term f n terminates.

Definition of Triples

Now we come to the most important definition of the whole course! A triple triple t H Q asserts that, for any input state s satisfying the precondition H, any possible execution of (s,t) terminates and reaches a final configuration satisfying the postcondition Q. This statement is captured in terms of the omni-big-step semantics as follows.

Because the predicate eval s t Q captures termination, the predicate triple t H Q that we build on top of it also captures termination. It therefore yields a "total correctness" triple. If we had defined the predicate eval as CoInductive instead of Inductive, we would have allowed for infinite executions. With such a coinductive definition of eval, we would have obtained a "partial correctness" triple instead. Such a partial correctness triple would still capture the property that none of the possible executions can get stuck -- each possible execution either terminates safely with a result satisfying the postcondition, or else diverges. Throughout the development of program logics, most research has concentrated on "partial correctness" logics. Depending on the set up, capturing "total correctness" is often much more challenging. In particular, when considering nondeterministic small-step semantics, and in particular when targeting concurrent programs, it can be nonobvious how to account for termination. But as long as we are concerned with sequential programs (i.e., without concurrency), omni-big-step semantics simplify reasoning about nondeterministic termination.

Structural Rules

Now that triples are defined, we can state and prove reasoning rules of Separation Logic. This chapter focuses on structural rules; the other rules will be presented in the next chapter. We begin with the statements of the rules and present their proofs afterwards.

The frame rule asserts that an arbitrary heap predicate may be added to both the precondition and the postcondition of any triple.

The consequence rule asserts, as in Hoare Logic, that the validity of a triple is preserved if we strengthen its precondition or weaken its postcondition.

The "extraction rule for pure facts" asserts that a judgment of the form triple t (\[P] \* H) Q is derivable from P → triple t H Q. This structural rule captures the extraction of the pure facts out of the precondition of a triple, like himpl_hstar_hpure_l for entailments.

The "extraction rule for existentials" asserts that a judgment of the form triple t (\∃ x, J x) Q is derivable from ∀ x, triple t (J x) Q. Again, this rule is the counterpart of the corresponding rule on entailements, himpl_hexists_l.

Derived Structural Rules

Given a triple to be established, is is very unlikely for the frame rule to be applicable directly, because the precondition must be exactly of the form H \* H' and the postcondition exactly of the form Q \*+ H' for some H'. For example, the frame rule would not apply to a proof obligation of the form triple t (H' \* H) (Q \*+ H') because H' \* H does not match H \* H'. This limitation rule can be addressed by combining the frame rule and the rule of consequence into a single rule, called the "consequence-frame rule". This rule, shown below, enables deriving a triple from another triple, without syntactic restrictions on the shape of the precondition and postcondition of the two triples involved.

Exercise: 1 star, standard, especially useful (triple_conseq_frame)

Prove the combined consequence-frame rule.

The extraction rule triple_hpure assumes a precondition of the form \[P] \* H. The variant rule triple_hpure', stated below, assumes instead a precondition with only the pure part, i.e., of the form \[P].

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

Prove that triple_hpure' is indeed a corollary of triple_hpure.

More Details

Proof of the Consequence Rule

The proof of the consequence rule relies on establishing that the omni-big-step judgment is preserved under weakening its postcondition. Recall that in eval s t Q₁, the postcondition Q₁ is an overapproximation of the set of configurations reachable from (s,t). Thus, if Q₁ is included in a larger set Q₂, then Q₂ is also an overapproximation of the configurations reachable from (s,t). The formalization is a straightforward induction.

From there, it is straightforward to derive the consequence rule.

Proof of the Frame Rule

The second key property that we wish to establish is the "frame rule". The frame rule asserts that if a specification triple H t Q holds, then one may derive triple (H \* H') t (Q \*+ H') for any H'. Recall from chapter Hprop that the operator Q \*+ H' is a notation for fun x ⇒ (Q x \* H'). Intuitively, if the term t executes safely in a heap H, then this this term should behave similarly in any extension of H with a disjoint part H'. Moreover, its evaluation should leave this piece of state H' unmodified throughout the execution of t. The crux of the proof of the frame rule is to argue that eval is stable under extension with a disjoint piece of heap.

This proof goes by induction. The most interesting step is for allocation. In a derivation built using eval_ref, we are given as assumption a property that holds for any location p fresh from h₁, and we are requested to prove a property that holds for any location p fresh from h₁ \u h₂. We are thus restricting the set of p that can be considered for allocation, and so the result holds.

The frame rule is derived from eval_frame and eval_conseq.

Proof of the Extraction Rules

The extraction rules are proved by unfolding the definition of triple and inverting the hypothesis capturing the fact that the input state satisfies the precondition.

Exercise: 1 star, standard, especially useful (triple_hexists)

Prove triple_hexists.

Rule for Naming Heaps

To prove triple t H Q, it suffices to show that, for any heap h satisfying H, the triple triple t (= h) Q holds. In other words, even though the predicate triple abstracts away from the input heap, it remains technically possible to introduce an entity, namely h, that refers to the specific heap at hand during the evaluation of t. (An example use case will appear in a later chapter (WPsem, lemma wp_equiv_2).

Exercise: 1 star, standard, optional (triple_named_heap)

Prove the reasoning rule hoare_named_heap.

Optional Material

An Alternative Structural Rule for Existentials

Traditional papers on Separation Logic do not include triple_hexists, but instead include a rule called here triple_hexists2, which features an existential quantifier both in the precondition and in the postcondition. As we show next, in the presence of the consequence rule, the two rules are equivalent.

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

Using triple_hexists and triple_conseq, as well as the tactic xsimpl, prove that triple_hexists2 is derivable.

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

Reciprocally, using triple_hexists2 and triple_conseq, as well as the tactic xsimpl, prove that triple_hexists is derivable. Of course, you may not use triple_hexists in this proof.)

Compared with triple_hexists2, the formulation of triple_hexists is more concise, and is easier to exploit in practice.

Small-Step Semantics

Suppose we have a language with a formal semantics written not in big-step stype but in small-step style. What are the options for formalizing total correctness triples? We discuss two approaches. The first one consists of formally relating the small-step judgment with the omni-big-step judgment. The second consists of directly defining triples in terms of the small-step judgment. Before explaining the two approaches, let us present the formalization of the small-step semantics. 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 to reach the program configuration (s',t'). Its definition is standard.

The judgment steps s t s' t' corresponds to the reflexive and transitive closure of step. Concretely, it asserts that the configuration (s,t) can reduce in zero, one, or several steps to (s',t').

The predicate trm_is_val t asserts that t is a value.

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. Conversely, a configuration (s,t) that can take a step is said to be reducible.

Values are not reducible.

The predicate notstuck s t asserts that either t is a value or t is reducible.

Equivalence Between Small-Step and Omni-Big-Step

If we consider the omni-big-step semantics to be the starting point of a development, then the definition of triple is obviously sound with respect to that semantics, as it concludes eval s t Q. If, however, we consider the small-step semantics to be the starting point, then to establish soundness it is required to prove that triple t H Q ensures that all possible evaluations of t in a heap satisfying H are: (1) terminating, and (2) guaranteed to reach a value; moreover, (3) this value and the final state obtained must satisfy the postconditon Q. We begin by formalizing each of these properties. The judgment terminates s t is defined inductively. The execution starting from (s,t) terminates if any possible step leads to a configuration that terminates. Note that a configuration that has reached a value cannot take a step, hence is considered terminating.

The judgment safe s t asserts that no execution may reach a stuck term. In other words, for any configuration (s',t') reachable from (s,t), it is the case that the configuration (s',t') is either a value or is reducible.

The judgment correct s t Q asserts that if the execution of (s,t) reaches a final configuration, then this final configuration satisfies Q.

The conjunction of safe and correct corresponds to "partial correctness". The conjunction of safe, correct and terminates corresponds to "total correctness". The soundness theorem that we aim for establishes that triple t H Q entails total correctness.
    triple t H Q →
    ∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q. To prove soundness, we introduce an inductively predicate, named seval, which captures total correctness in small-step style. On the one hand, we prove that seval entails safe, correct, and terminates. On the other hand, we prove that seval is related to the omni-big-step judgment, eval. The judgment seval s t Q asserts that any execution of (s,t) terminates and reaches a configuration satisfying Q. In the "base" case, seval s v Q holds if the terminal configuration (s,v) satisfies Q. In the "step" case, seval s t Q holds if (1) the configuration (s,t) is reducible, and (2) if for any step that (s,t) may take to (s',t'), the predicate seval s' t' Q holds.

Exercise: 2 stars, standard, optional (seval_val_inv)

As a warm-up to get some familiary with seval, prove the following inversion lemma, which asserts that, given a value v, the property seval s v Q implies Q s v.

We begin with the three key properties of seval: termination, safety, and correctness.

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

Prove that seval captures termination.

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

Prove that seval captures safety.

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

Prove that seval captures correctness.

We can group the three results into a soundness theorem for seval.

We now establish that the omni-big-step evaluation judgment entails the small-step-based seval judgment. The proof is carried out by induction on the omni-big-step relation. It relies on a number of auxiliary results establishing that, for each term construct, the seval judgment admits an evaluation rule that mimics the omni-big-step evaluation rule. We begin with the statements of the auxiliary lemmas.