LibSepReferenceAppendix - The Full Construction

This file provides an end-to-end construction of a weakest-precondition style characteristic formula generator (the function named wpgen in chapter WPgen), for a core programming language with programs assumed to be in A-normal form, including support for records with up to 3 fields.
Set Implicit Arguments.
From SLF Require Export LibCore.
From SLF Require Export LibSepTLCbuffer LibSepVar LibSepFmap.
From SLF Require LibSepSimpl.
Module Fmap := LibSepFmap. (* Short name for Fmap module. *)

Imports

Extensionality Axioms

These standard extensionality axioms may also be found in the LibAxiom.v file associated with the TLC library.
Axiom functional_extensionality : ∀ A B (f g:A→B),
  (∀ x, f x = g x) →
  f = g.
Axiom propositional_extensionality : ∀ (P Q:Prop),
  (P ↔ Q) →
  P = Q.

Variables

The file LibSepVar.v, whoses definitions are imported in the header to the present file, defines the type var as an alias for string. It also provides the boolean function var_eq x y to compare two variables, and the tactic case_var to perform case analysis on expressions of the form if var_eq x y then .. else .. that appear in the goal.

Finite Maps

The file LibSepFmap.v, which is bound by the short name Fmap in the header, provides a formalization of finite maps. These maps are used to represent heaps in the semantics. The library provides a tactic called fmap_disjoint to automate disjointness proofs, and a tactic called fmap_eq for proving equalities between heaps modulo associativity and commutativity. Without these two tactics, proofs involving finite maps would be much more tedious and fragile.

Source Language

Syntax

The grammar of primitive operations includes a number of operations.
Inductive prim : Type :=
  | val_ref : prim
  | val_get : prim
  | val_set : prim
  | val_free : prim
  | val_neg : prim
  | val_opp : prim
  | val_eq : prim
  | val_add : prim
  | val_neq : prim
  | val_sub : prim
  | val_mul : prim
  | val_div : prim
  | val_mod : prim
  | val_rand : prim
  | val_le : prim
  | val_lt : prim
  | val_ge : prim
  | val_gt : prim
  | val_ptr_add : prim.
Locations are defined as natural numbers.
Definition loc : Type := nat.
The null location corresponds to address zero.
Definition null : loc := 0%nat.
The grammar of closed values includes includes basic values such as int and bool, but also locations, closures. It also includes two special values, val_uninit used in the formalization of arrays, and val_error used for stating semantics featuring error-propagation.
Inductive val : Type :=
  | val_unit : val
  | val_bool : bool → val
  | val_int : int → val
  | val_loc : loc → val
  | val_prim : prim → val
  | val_fun : var → trm → val
  | val_fix : var → var → trm → val
  | val_uninit : val
  | val_error : val

The grammar of terms includes values, variables, functions, applications, sequence, let-bindings, and conditions. Sequences are redundant with let-bindings, but are useful in practice to avoid binding dummy names, and serve on numerous occasion as a warm-up before proving results on let-bindings.

with trm : Type :=
  | trm_val : val → trm
  | trm_var : var → trm
  | trm_fun : var → trm → trm
  | trm_fix : var → var → trm → trm
  | trm_app : trm → trm → trm
  | trm_seq : trm → trm → trm
  | trm_let : var → trm → trm → trm
  | trm_if : trm → trm → trm → trm.
A state consists of a finite map from location to values. Records and arrays are represented as sets of consecutive cells, preceeded by a header field describing the length of the block.
Definition state : Type := fmap loc val.
The type heap, a.k.a. state. By convention, the "state" refers to the full memory state when describing the semantics, while the "heap" potentially refers to only a fraction of the memory state, when definining Separation Logic predicates.
Definition heap : Type := state.

Coq Tweaks

h1 \u h2 is a notation for union of two heaps.
Notation "h1 \u h2" := (Fmap.union h1 h2)
  (at level 37, right associativity).
Implicit types associated with meta-variables.
Implicit Types f : var.
Implicit Types b : bool.
Implicit Types p : loc.
Implicit Types n : int.
Implicit Types v w r vf vx : val.
Implicit Types t : trm.
Implicit Types h : heap.
Implicit Types s : state.
The types of values and terms are inhabited.
Global Instance Inhab_val : Inhab val.
Proof using. apply (Inhab_of_val val_unit). Qed.
Global Instance Inhab_trm : Inhab trm.
Proof using. apply (Inhab_of_val (trm_val val_unit)). Qed.
Coercions to improve conciseness in the statment of evaluation rules.
Coercion val_bool : bool >-> val.
Coercion val_int : Z >-> val.
Coercion val_loc : loc >-> val.
Coercion val_prim : prim >-> val.
Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.

Values and Substitutions

The predicate trm_is_val t asserts that t is a value.
Definition trm_is_val (t:trm) : Prop :=
  match t with trm_val v ⇒ True | _ ⇒ False end.
The standard capture-avoiding substitution, written subst x v t.
Fixpoint subst (y:var) (v':val) (t:trm) : trm :=
  let aux t := subst y v' t in
  let if_y_eq x t1 t2 := if var_eq x y then t1 else t2 in
  match t with
  | trm_val v ⇒ trm_val v
  | trm_var x ⇒ if_y_eq x (trm_val v') t
  | trm_fun x t1 ⇒ trm_fun x (if_y_eq x t1 (aux t1))
  | trm_fix f x t1 ⇒ trm_fix f x (if_y_eq f t1 (if_y_eq x t1 (aux t1)))
  | trm_app t1 t2 ⇒ trm_app (aux t1) (aux t2)
  | trm_seq t1 t2 ⇒ trm_seq (aux t1) (aux t2)
  | trm_let x t1 t2 ⇒ trm_let x (aux t1) (if_y_eq x t2 (aux t2))
  | trm_if t0 t1 t2 ⇒ trm_if (aux t0) (aux t1) (aux t2)
  end.

Small-Step Semantics

The judgment step s t s' t' asserts that the configuration (s,t) can take one reduction step towards the program configuration (s',t').
Inductive step : state → trm → state → trm → Prop :=

  (* Context rules *)
  | step_seq_ctx : ∀ s1 s2 t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_seq t1 t2) s2 (trm_seq t1' t2)
  | step_let_ctx : ∀ s1 s2 x t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_let x t1 t2) s2 (trm_let x t1' t2)
  | step_app_arg1 : ∀ s1 s2 t1 t1' t2,
      step s1 t1 s2 t1' →
      step s1 (trm_app t1 t2) s2 (trm_app t1' t2)
  | step_app_arg2 : ∀ s1 s2 v1 t2 t2',
      step s1 t2 s2 t2' →
      step s1 (trm_app v1 t2) s2 (trm_app v1 t2')

  (* Reductions *)
  | step_fun : ∀ s x t1,
      step s (trm_fun x t1) s (val_fun x t1)
  | step_fix : ∀ s f x t1,
      step s (trm_fix f x t1) s (val_fix f x t1)
  | step_app_fun : ∀ s v1 v2 x t1,
      v1 = val_fun x t1 →
      step s (trm_app v1 v2) s (subst x v2 t1)
  | step_app_fix : ∀ s v1 v2 f x t1,
      v1 = val_fix f x t1 →
      step s (trm_app v1 v2) s (subst x v2 (subst f v1 t1))
  | step_if : ∀ s b t1 t2,
      step s (trm_if (val_bool b) t1 t2) s (if b then t1 else t2)
  | step_seq : ∀ s t2 v1,
      step s (trm_seq v1 t2) s t2
  | step_let : ∀ s x t2 v1,
      step s (trm_let x v1 t2) s (subst x v1 t2)

  (* Unary operations *)
  | step_neg : ∀ s b,
      step s (val_neg (val_bool b)) s (val_bool (neg b))
  | step_opp : ∀ s n,
      step s (val_opp (val_int n)) s (val_int (- n))
  | step_rand : ∀ s n n1,
      0 ≤ n1 < n →
      step s (val_rand (val_int n)) s (val_int n1)

  (* Binary operations *)
  | step_eq : ∀ s v1 v2,
      step s (val_eq v1 v2) s (val_bool (isTrue (v1 = v2)))
  | step_neq : ∀ s v1 v2,
      step s (val_neq v1 v2) s (val_bool (isTrue (v1 ≠ v2)))
  | step_add : ∀ s n1 n2,
      step s (val_add (val_int n1) (val_int n2)) s (val_int (n1 + n2))
  | step_sub : ∀ s n1 n2,
      step s (val_sub (val_int n1) (val_int n2)) s (val_int (n1 - n2))
  | step_mul : ∀ s n1 n2,
      step s (val_mul (val_int n1) (val_int n2)) s (val_int (n1 * n2))
  | step_div : ∀ s n1 n2,
      n2 ≠ 0 →
      step s (val_div (val_int n1) (val_int n2)) s (Z.quot n1 n2)
  | step_mod : ∀ s n1 n2,
      n2 ≠ 0 →
      step s (val_mod (val_int n1) (val_int n2)) s (Z.rem n1 n2)
  | step_le : ∀ s n1 n2,
      step s (val_le (val_int n1) (val_int n2)) s (val_bool (isTrue (n1 ≤ n2)))
  | step_lt : ∀ s n1 n2,
      step s (val_lt (val_int n1) (val_int n2)) s (val_bool (isTrue (n1 < n2)))
  | step_ge : ∀ s n1 n2,
      step s (val_ge (val_int n1) (val_int n2)) s (val_bool (isTrue (n1 ≥ n2)))
  | step_gt : ∀ s n1 n2,
      step s (val_gt (val_int n1) (val_int n2)) s (val_bool (isTrue (n1 > n2)))
  | step_ptr_add : ∀ s p1 p2 n,
      (p2:int) = p1 + n →
      step s (val_ptr_add (val_loc p1) (val_int n)) s (val_loc p2)

  (* Heap operations *)
  | step_ref : ∀ s v p,
      ¬ Fmap.indom s p →
      step s (val_ref v) (Fmap.update s p v) (val_loc p)
  | step_get : ∀ s p,
      Fmap.indom s p →
      step s (val_get (val_loc p)) s (Fmap.read s p)
  | step_set : ∀ s p v,
      Fmap.indom s p →
      step s (val_set (val_loc p) v) (Fmap.update s p v) val_unit
  | step_free : ∀ s p,
      Fmap.indom s p →
      step s (val_free (val_loc p)) (Fmap.remove s p) val_unit.
The judgment steps 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 steps to (s',t').
Inductive steps : state → trm → state → trm → Prop :=
  | steps_refl : ∀ s t,
      steps s t s t
  | steps_step : ∀ s1 s2 s3 t1 t2 t3,
      step s1 t1 s2 t2 →
      steps s2 t2 s3 t3 →
      steps s1 t1 s3 t3.
Lemma steps_of_step : ∀ s1 s2 t1 t2,
  step s1 t1 s2 t2 →
  steps s1 t1 s2 t2.
Proof using. introv M. applys steps_step M. applys steps_refl. Qed.
Lemma steps_trans : ∀ s1 s2 s3 t1 t2 t3,
  steps s1 t1 s2 t2 →
  steps s2 t2 s3 t3 →
  steps s1 t1 s3 t3.
Proof using. introv M1. induction M1; introv M2. { auto. } { constructors*. } Qed.
The predicate reducible s t asserts that the configuration (s,t) can take a step.
Definition reducible (s:state) (t:trm) : Prop :=
  ∃ s' t', step s t s' t'.
The predicate notstuck s t asserts that t is a value or is reducible.
Definition notstuck (s:state) (t:trm) : Prop :=
  trm_is_val t ∨ reducible s t.

Omni-Big-Step Semantics of primitive operations

Evaluation rules for unary operations are captured by the predicate evalunop op v1 P, which asserts that op v1 evaluates to a value v2 satisfying P.
Inductive evalunop : prim → val → (val→Prop) → Prop :=
  | evalunop_neg : ∀ b1,
      evalunop val_neg (val_bool b1) (= val_bool (neg b1))
  | evalunop_opp : ∀ n1,
      evalunop val_opp (val_int n1) (= val_int (- n1))
  | evalunop_rand : ∀ n,
      n > 0 →
      evalunop val_rand (val_int n) (fun r ⇒ ∃ n1, r = val_int n1 ∧ 0 ≤ n1 < n).
Evaluation rules for binary operations are captured by the predicate redupop op v1 v2 P, which asserts that op v1 v2 evaluates to a value v3 satisfying P.
Inductive evalbinop : val → val → val → (val→Prop) → Prop :=
  | evalbinop_eq : ∀ v1 v2,
      evalbinop val_eq v1 v2 (= val_bool (isTrue (v1 = v2)))
  | evalbinop_neq : ∀ v1 v2,
      evalbinop val_neq v1 v2 (= val_bool (isTrue (v1 ≠ v2)))
  | evalbinop_add : ∀ n1 n2,
      evalbinop val_add (val_int n1) (val_int n2) (= val_int (n1 + n2))
  | evalbinop_sub : ∀ n1 n2,
      evalbinop val_sub (val_int n1) (val_int n2) (= val_int (n1 - n2))
  | evalbinop_mul : ∀ n1 n2,
      evalbinop val_mul (val_int n1) (val_int n2) (= val_int (n1 * n2))
  | evalbinop_div : ∀ n1 n2,
      n2 ≠ 0 →
      evalbinop val_div (val_int n1) (val_int n2) (= val_int (Z.quot n1 n2))
  | evalbinop_mod : ∀ n1 n2,
      n2 ≠ 0 →
      evalbinop val_mod (val_int n1) (val_int n2) (= val_int (Z.rem n1 n2))
  | evalbinop_le : ∀ n1 n2,
      evalbinop val_le (val_int n1) (val_int n2) (= val_bool (isTrue (n1 ≤ n2)))
  | evalbinop_lt : ∀ n1 n2,
      evalbinop val_lt (val_int n1) (val_int n2) (= val_bool (isTrue (n1 < n2)))
  | evalbinop_ge : ∀ n1 n2,
      evalbinop val_ge (val_int n1) (val_int n2) (= val_bool (isTrue (n1 ≥ n2)))
  | evalbinop_gt : ∀ n1 n2,
      evalbinop val_gt (val_int n1) (val_int n2) (= val_bool (isTrue (n1 > n2)))
  | evalbinop_ptr_add : ∀ p1 p2 n,
      (p2:int) = p1 + n →
      evalbinop val_ptr_add (val_loc p1) (val_int n) (= val_loc p2).

Omni-Big-Step Semantics

Section Eval.
The predicate purepost s P converts a predicate P:val→Prop into a postcondition of type val→state→Prop that holds in the state s.
Definition purepost (s:state) (P:val→Prop) : val→state→Prop :=
  fun v s' ⇒ P v ∧ s' = s.
Definition purepostin (s:state) (P:val→Prop) (Q:val→state→Prop) : Prop :=
  (* equivalent to purepost S P ===> Q *)
  ∀ v, P v → Q v s.
Omni-Big-step evaluation judgement, written eval s t Q.
Implicit Types Q : val→state→Prop.
Inductive eval : state → trm → (val→state→Prop) → Prop :=
  | eval_val : ∀ s v Q,
      Q v s →
      eval s (trm_val v) Q
  | eval_fun : ∀ s x t1 Q,
      Q (val_fun x t1) s →
      eval s (trm_fun x t1) Q
  | eval_fix : ∀ s f x t1 Q,
      Q (val_fix f x t1) s →
      eval s (trm_fix f x t1) Q
  | eval_app_arg1 : ∀ s1 t1 t2 Q1 Q,
      ¬ trm_is_val t1 →
      eval s1 t1 Q1 →
      (∀ v1 s2, Q1 v1 s2 → eval s2 (trm_app v1 t2) Q) →
      eval s1 (trm_app t1 t2) Q
  | eval_app_arg2 : ∀ s1 v1 t2 Q1 Q,
      ¬ trm_is_val t2 →
      eval s1 t2 Q1 →
      (∀ v2 s2, Q1 v2 s2 → eval s2 (trm_app v1 v2) Q) →
      eval s1 (trm_app v1 t2) Q
  | eval_app_fun : ∀ s1 v1 v2 x t1 Q,
      v1 = val_fun x t1 →
      eval s1 (subst x v2 t1) Q →
      eval s1 (trm_app v1 v2) Q
  | eval_app_fix : ∀ s v1 v2 f x t1 Q,
      v1 = val_fix f x t1 →
      eval s (subst x v2 (subst f v1 t1)) Q →
      eval s (trm_app v1 v2) Q
  | eval_seq : ∀ Q1 s t1 t2 Q,
      eval s t1 Q1 →
      (∀ v1 s2, Q1 v1 s2 → eval s2 t2 Q) →
      eval s (trm_seq t1 t2) Q
  | eval_let : ∀ Q1 s x t1 t2 Q,
      eval s t1 Q1 →
      (∀ v1 s2, Q1 v1 s2 → eval s2 (subst x v1 t2) Q) →
      eval s (trm_let x t1 t2) Q
  | eval_if : ∀ s (b:bool) t1 t2 Q,
      eval s (if b then t1 else t2) Q →
      eval s (trm_if (val_bool b) t1 t2) Q
  | eval_unop : ∀ op s v1 P Q,
      evalunop op v1 P →
      purepostin s P Q →
      eval s (op v1) Q
  | eval_binop : ∀ op s v1 v2 P Q,
      evalbinop op v1 v2 P →
      purepostin s P Q →
      eval s (op v1 v2) Q
  | eval_ref : ∀ s v Q,
      (∀ p, ¬ Fmap.indom s p →
          Q (val_loc p) (Fmap.update s p v)) →
      eval s (val_ref v) Q
  | eval_get : ∀ s p Q,
      Fmap.indom s p →
      Q (Fmap.read s p) s →
      eval s (val_get (val_loc p)) Q
  | eval_set : ∀ s p v Q,
      Fmap.indom s p →
      Q val_unit (Fmap.update s p v) →
      eval s (val_set (val_loc p) v) Q
  | eval_free : ∀ s p Q,
      Fmap.indom s p →
      Q val_unit (Fmap.remove s p) →
      eval s (val_free (val_loc p)) Q.
Specialized rule for values, to instantiate the postcondition
Lemma eval_val_minimal : ∀ s v,
  eval s (trm_val v) (fun v' s' ⇒ (v' = v) ∧ (s' = s)).
Proof using. intros. applys* eval_val. Qed.
Specialized evaluation rules for selected operations, to avoid the indirection via eval_unop and eval_binop in the course.
Lemma eval_add : ∀ s n1 n2 Q,
  Q (val_int (n1 + n2)) s →
  eval s (val_add (val_int n1) (val_int n2)) Q.
Proof using.
  intros. applys* eval_binop.
  { applys* evalbinop_add. }
  { intros ? →. auto. }
Qed.
Lemma eval_div : ∀ s n1 n2 Q,
  n2 ≠ 0 →
  Q (val_int (Z.quot n1 n2)) s →
  eval s (val_div (val_int n1) (val_int n2)) Q.
Proof using.
  intros. applys* eval_binop.
  { applys* evalbinop_div. }
  { intros ? →. auto. }
Qed.
Lemma eval_rand : ∀ s n Q,
  n > 0 →
  (∀ n1, 0 ≤ n1 < n → Q n1 s) →
  eval s (val_rand (val_int n)) Q.
Proof using.
  intros. applys* eval_unop.
  { applys* evalunop_rand. }
  { intros ? (?&->&?). auto. }
Qed.
Derived rule for reasoning about an applications, without need to perform a case analysis on whether the entities are already values.
Lemma eval_app_arg1' : ∀ s1 t1 t2 Q1 Q,
  eval s1 t1 Q1 →
  (∀ v1 s2, Q1 v1 s2 → eval s2 (trm_app v1 t2) Q) →
  eval s1 (trm_app t1 t2) Q.
Proof using.
  introv M1 M2. tests C1: (trm_is_val t1).
  { destruct t1; tryfalse. inverts M1. applys* M2. }
  { applys* eval_app_arg1. }
Qed.
Lemma eval_app_arg2' : ∀ s1 v1 t2 Q1 Q,
  eval s1 t2 Q1 →
  (∀ v2 s2, eval s2 (trm_app v1 v2) Q) →
  eval s1 (trm_app v1 t2) Q.
Proof using.
  introv M1 M2. tests C1: (trm_is_val t2).
  { destruct t2; tryfalse. inverts M1. applys* M2. }
  { applys* eval_app_arg2. }
Qed.
eval_like t1 t2 asserts that t2 evaluates like t1. In particular, this relation hold whenever t2 reduces in small-step to t1.
Definition eval_like (t1 t2:trm) : Prop :=
  ∀ s Q, eval s t1 Q → eval s t2 Q.
End Eval.

Heap Predicates

We next define heap predicates and establish their properties. All this material is wrapped in a module, allowing us to instantiate the functor from chapter LibSepSimpl that defines the tactic xsimpl.
Module SepSimplArgs.

Hprop and Entailment

Declare Scope hprop_scope.
Open Scope hprop_scope.
The type of heap predicates is named hprop.
Definition hprop := heap → Prop.
Implicit types for meta-variables.
Implicit Types P : Prop.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.
Entailment for heap predicates, written H1 ==> H2. This entailment is linear.
Definition himpl (H1 H2:hprop) : Prop :=
  ∀ h, H1 h → H2 h.
Notation "H1 ==> H2" := (himpl H1 H2) (at level 55) : hprop_scope.
Entailment between postconditions, written Q1 ===> Q2.
Definition qimpl A (Q1 Q2:A→hprop) : Prop :=
  ∀ (v:A), Q1 v ==> Q2 v.
Notation "Q1 ===> Q2" := (qimpl Q1 Q2) (at level 55) : hprop_scope.

Definition of Heap Predicates

The core heap predicates are defined next, together with the associated notation:
  • \[] denotes the empty heap predicate
  • \[P] denotes a pure fact
  • \Top denotes the true heap predicate (affine)
  • p ~~> v denotes a singleton heap
  • H1 \* H2 denotes the separating conjunction
  • Q1 \*+ H2 denotes the separating conjunction extending a postcondition
  • \∃ x, H denotes an existential quantifier
  • \∀ x, H denotes a universal quantifier
  • H1 \−∗ H2 denotes a magic wand between heap predicates
  • Q1 \−−∗ Q2 denotes a magic wand between postconditions.
Definition hempty : hprop :=
  fun h ⇒ (h = Fmap.empty).
Definition hsingle (p:loc) (v:val) : hprop :=
  fun h ⇒ (h = Fmap.single p v).
Definition hstar (H1 H2 : hprop) : hprop :=
  fun h ⇒ ∃ h1 h2, H1 h1
                              ∧ H2 h2
                              ∧ Fmap.disjoint h1 h2
                              ∧ h = Fmap.union h1 h2.
Definition hexists A (J:A→hprop) : hprop :=
  fun h ⇒ ∃ x, J x h.
Definition hforall (A : Type) (J : A → hprop) : hprop :=
  fun h ⇒ ∀ x, J x h.
Notation "\[]" := (hempty)
  (at level 0) : hprop_scope.
Notation "p '~~>' v" := (hsingle p v) (at level 32) : hprop_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
  (at level 41, right associativity) : hprop_scope.
Notation "'\exists' x1 .. xn , H" :=
  (hexists (fun x1 ⇒ .. (hexists (fun xn ⇒ H)) ..))
  (at level 39, x1 binder, H at level 50, right associativity,
   format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'") : hprop_scope.
Notation "'\forall' x1 .. xn , H" :=
  (hforall (fun x1 ⇒ .. (hforall (fun xn ⇒ H)) ..))
  (at level 39, x1 binder, H at level 50, right associativity,
   format "'[' '\forall' '/ ' x1 .. xn , '/ ' H ']'") : hprop_scope.
The remaining operators are defined in terms of the preivous above, rather than directly as functions over heaps. Doing so reduces the amount of proofs, by allowing to better leverage the tactic xsimpl.
Definition hpure (P:Prop) : hprop :=
  \∃ (p:P), \[].
Definition htop : hprop :=
  \∃ (H:hprop), H.
Definition hwand (H1 H2 : hprop) : hprop :=
  \∃ H0, H0 \* hpure ((H1 \* H0) ==> H2).
Definition qwand A (Q1 Q2:A→hprop) : hprop :=
  \∀ x, hwand (Q1 x) (Q2 x).
Notation "\[ P ]" := (hpure P)
  (at level 0, format "\[ P ]") : hprop_scope.
Notation "\Top" := (htop) : hprop_scope.
Notation "Q \*+ H" := (fun x ⇒ hstar (Q x) H)
  (at level 40) : hprop_scope.
Notation "H1 \−∗ H2" := (hwand H1 H2)
  (at level 43, right associativity) : hprop_scope.
Notation "Q1 \−−∗ Q2" := (qwand Q1 Q2)
  (at level 43) : hprop_scope.

Basic Properties of Separation Logic Operators

Tactic for Automation

We set up auto to process goals of the form h1 = h2 by calling fmap_eq, which proves equality modulo associativity and commutativity.
#[global] Hint Extern 1 (_ = _ :> heap) ⇒ fmap_eq.
We also set up auto to process goals of the form Fmap.disjoint h1 h2 by calling the tactic fmap_disjoint, which essentially normalizes all disjointness goals and hypotheses, split all conjunctions, and invokes proof search with a base of hints specified in LibSepFmap.v.
Import Fmap.DisjointHints.
Tactic Notation "fmap_disjoint_pre" :=
  subst; rew_disjoint; jauto_set.
#[global] Hint Extern 1 (Fmap.disjoint _ _) ⇒ fmap_disjoint_pre.

Properties of himpl and qimpl

Lemma himpl_refl : ∀ H,
  H ==> H.
Proof using. introv M. auto. Qed.
#[global] Hint Resolve himpl_refl.
Lemma himpl_trans : ∀ H2 H1 H3,
  (H1 ==> H2) →
  (H2 ==> H3) →
  (H1 ==> H3).
Proof using. introv M1 M2. unfolds* himpl. Qed.
Lemma himpl_trans_r : ∀ H2 H1 H3,
   H2 ==> H3 →
   H1 ==> H2 →
   H1 ==> H3.
Proof using. introv M1 M2. applys* himpl_trans M2 M1. Qed.
Lemma himpl_antisym : ∀ H1 H2,
  (H1 ==> H2) →
  (H2 ==> H1) →
  (H1 = H2).
Proof using. introv M1 M2. applys pred_ext_1. intros h. iff*. Qed.
Lemma hprop_op_comm : ∀ (op:hprop→hprop→hprop),
  (∀ H1 H2, op H1 H2 ==> op H2 H1) →
  (∀ H1 H2, op H1 H2 = op H2 H1).
Proof using. introv M. intros. applys himpl_antisym; applys M. Qed.
Lemma qimpl_refl : ∀ A (Q:A→hprop),
  Q ===> Q.
Proof using. intros. unfolds*. Qed.
#[global] Hint Resolve qimpl_refl.

Properties of hempty

Lemma hempty_intro :
  \[] Fmap.empty.
Proof using. unfolds*. Qed.
Lemma hempty_inv : ∀ h,
  \[] h →
  h = Fmap.empty.
Proof using. auto. Qed.

Properties of hstar

Lemma hstar_intro : ∀ H1 H2 h1 h2,
  H1 h1 →
  H2 h2 →
  Fmap.disjoint h1 h2 →
  (H1 \* H2) (Fmap.union h1 h2).
Proof using. intros. ∃¬h1 h2. Qed.
Lemma hstar_inv : ∀ H1 H2 h,
  (H1 \* H2) h →
  ∃ h1 h2, H1 h1 ∧ H2 h2 ∧ Fmap.disjoint h1 h2 ∧ h = Fmap.union h1 h2.
Proof using. introv M. applys M. Qed.
Lemma hstar_comm : ∀ H1 H2,
   H1 \* H2 = H2 \* H1.
Proof using.
  applys hprop_op_comm. unfold hprop, hstar. intros H1 H2.
  intros h (h1&h2&M1&M2&D&U). rewrite¬Fmap.union_comm_of_disjoint in U.
  ∃* h2 h1.
Qed.
Lemma hstar_assoc : ∀ H1 H2 H3,
  (H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Proof using.
  intros H1 H2 H3. applys himpl_antisym; intros h.
  { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
    ∃ h1 (h2 \+ h3). splits¬. { applys* hstar_intro. } }
  { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
    ∃ (h1 \+ h2) h3. splits¬. { applys* hstar_intro. } }
Qed.
Lemma hstar_hempty_l : ∀ H,
  \[] \* H = H.
Proof using.
  intros. applys himpl_antisym; intros h.
  { intros (h1&h2&M1&M2&D&U). forwards E: hempty_inv M1. subst.
    rewrite¬Fmap.union_empty_l. }
  { intros M. ∃ (Fmap.empty:heap) h. splits¬. { applys hempty_intro. } }
Qed.
Lemma hstar_hempty_r : ∀ H,
  H \* \[] = H.
Proof using.
  applys neutral_r_of_comm_neutral_l. applys¬hstar_comm. applys¬hstar_hempty_l.
Qed.
Lemma hstar_hexists : ∀ A (J:A→hprop) H,
  (hexists J) \* H = hexists (fun x ⇒ (J x) \* H).
Proof using.
  intros. applys himpl_antisym; intros h.
  { intros (h1&h2&(x&M1)&M2&D&U). ∃¬x h1 h2. }
  { intros (x&(h1&h2&M1&M2&D&U)). ∃ h1 h2. splits¬. { ∃¬x. } }
Qed.
Lemma hstar_hforall : ∀ H A (J:A→hprop),
  (hforall J) \* H ==> hforall (J \*+ H).
Proof using.
  intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. ∃¬h1 h2.
Qed.
Lemma himpl_frame_l : ∀ H2 H1 H1',
  H1 ==> H1' →
  (H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). ∃* h1 h2. Qed.
Lemma himpl_frame_r : ∀ H1 H2 H2',
  H2 ==> H2' →
  (H1 \* H2) ==> (H1 \* H2').
Proof using.
  introv M. do 2 rewrite (@hstar_comm H1). applys¬himpl_frame_l.
Qed.
Lemma himpl_frame_lr : ∀ H1 H1' H2 H2',
  H1 ==> H1' →
  H2 ==> H2' →
  (H1 \* H2) ==> (H1' \* H2').
Proof using.
  introv M1 M2. applys himpl_trans. applys¬himpl_frame_l M1. applys¬himpl_frame_r.
Qed.
Lemma himpl_hstar_trans_l : ∀ H1 H2 H3 H4,
  H1 ==> H2 →
  H2 \* H3 ==> H4 →
  H1 \* H3 ==> H4.
Proof using.
  introv M1 M2. applys himpl_trans M2. applys himpl_frame_l M1.
Qed.
Lemma himpl_hstar_trans_r : ∀ H1 H2 H3 H4,
  H1 ==> H2 →
  H3 \* H2 ==> H4 →
  H3 \* H1 ==> H4.
Proof using.
  introv M1 M2. applys himpl_trans M2. applys himpl_frame_r M1.
Qed.

Properties of hpure

Lemma hpure_intro : ∀ P,
  P →
  \[P] Fmap.empty.
Proof using. introv M. ∃ M. unfolds*. Qed.
Lemma hpure_inv : ∀ P h,
  \[P] h →
  P ∧ h = Fmap.empty.
Proof using. introv (p&M). split¬. Qed.
Lemma hstar_hpure_l : ∀ P H h,
  (\[P] \* H) h = (P ∧ H h).
Proof using.
  intros. apply prop_ext. unfold hpure.
  rewrite hstar_hexists. rewrite* hstar_hempty_l.
  iff (p&M) (p&M). { split¬. } { ∃¬p. }
Qed.
Lemma hstar_hpure_r : ∀ P H h,
  (H \* \[P]) h = (H h ∧ P).
Proof using.
  intros. rewrite hstar_comm. rewrite hstar_hpure_l. apply* prop_ext.
Qed.
Lemma himpl_hstar_hpure_r : ∀ P H H',
  P →
  (H ==> H') →
  H ==> (\[P] \* H').
Proof using. introv HP W. intros h K. rewrite* hstar_hpure_l. Qed.
Lemma hpure_inv_hempty : ∀ P h,
  \[P] h →
  P ∧ \[] h.
Proof using.
  introv M. rewrite <- hstar_hpure_l. rewrite¬hstar_hempty_r.
Qed.
Lemma hpure_intro_hempty : ∀ P h,
  \[] h →
  P →
  \[P] h.
Proof using.
  introv M N. rewrite <- (hstar_hempty_l \[P]). rewrite¬hstar_hpure_r.
Qed.
Lemma himpl_hempty_hpure : ∀ P,
  P →
  \[] ==> \[P].
Proof using. introv HP. intros h Hh. applys* hpure_intro_hempty. Qed.
Lemma himpl_hstar_hpure_l : ∀ P H H',
  (P → H ==> H') →
  (\[P] \* H) ==> H'.
Proof using.
  introv W Hh. rewrite hstar_hpure_l in Hh. applys* W.
Qed.
Lemma hempty_eq_hpure_true :
  \[] = \[True].
Proof using.
  applys himpl_antisym; intros h M.
  { applys* hpure_intro_hempty. }
  { forwards*: hpure_inv_hempty M. }
Qed.
Lemma hfalse_hstar_any : ∀ H,
  \[False] \* H = \[False].
Proof using.
  intros. applys himpl_antisym; intros h; rewrite hstar_hpure_l; intros M.
  { false*. } { lets: hpure_inv_hempty M. false*. }
Qed.

Properties of hexists

Lemma hexists_intro : ∀ A (x:A) (J:A→hprop) h,
  J x h →
  (hexists J) h.
Proof using. intros. ∃¬x. Qed.
Lemma hexists_inv : ∀ A (J:A→hprop) h,
  (hexists J) h →
  ∃ x, J x h.
Proof using. intros. destruct H as [x H]. ∃¬x. Qed.
Lemma himpl_hexists_l : ∀ A H (J:A→hprop),
  (∀ x, J x ==> H) →
  (hexists J) ==> H.
Proof using. introv W. intros h (x&Hh). applys* W. Qed.
Lemma himpl_hexists_r : ∀ A (x:A) H J,
  (H ==> J x) →
  H ==> (hexists J).
Proof using. introv W. intros h. ∃ x. apply¬W. Qed.
Lemma himpl_hexists : ∀ A (J1 J2:A→hprop),
  J1 ===> J2 →
  hexists J1 ==> hexists J2.
Proof using.
  introv W. applys himpl_hexists_l. intros x. applys himpl_hexists_r W.
Qed.

Properties of hforall

Lemma hforall_intro : ∀ A (J:A→hprop) h,
  (∀ x, J x h) →
  (hforall J) h.
Proof using. introv M. applys* M. Qed.
Lemma hforall_inv : ∀ A (J:A→hprop) h,
  (hforall J) h →
  ∀ x, J x h.
Proof using. introv M. applys* M. Qed.
Lemma himpl_hforall_r : ∀ A (J:A→hprop) H,
  (∀ x, H ==> J x) →
  H ==> (hforall J).
Proof using. introv M. intros h Hh x. apply¬M. Qed.
Lemma himpl_hforall_l : ∀ A x (J:A→hprop) H,
  (J x ==> H) →
  (hforall J) ==> H.
Proof using. introv M. intros h Hh. apply¬M. Qed.
Lemma hforall_specialize : ∀ A (x:A) (J:A→hprop),
  (hforall J) ==> (J x).
Proof using. intros. applys* himpl_hforall_l x. Qed.
Lemma himpl_hforall : ∀ A (J1 J2:A→hprop),
  J1 ===> J2 →
  hforall J1 ==> hforall J2.
Proof using.
  introv W. applys himpl_hforall_r. intros x. applys himpl_hforall_l W.
Qed.

Properties of hwand

Lemma hwand_equiv : ∀ H0 H1 H2,
  (H0 ==> H1 \−∗ H2) ↔ (H1 \* H0 ==> H2).
Proof using.
  unfold hwand. iff M.
  { rewrite hstar_comm. applys himpl_hstar_trans_l (rm M).
    rewrite hstar_hexists. applys himpl_hexists_l. intros H.
    rewrite (hstar_comm H). rewrite hstar_assoc.
    rewrite (hstar_comm H H1). applys¬himpl_hstar_hpure_l. }
  { applys himpl_hexists_r H0.
    rewrite <- (hstar_hempty_r H0) at 1.
    applys himpl_frame_r. applys himpl_hempty_hpure M. }
Qed.
Lemma himpl_hwand_r : ∀ H1 H2 H3,
  H2 \* H1 ==> H3 →
  H1 ==> (H2 \−∗ H3).
Proof using. introv M. rewrite¬hwand_equiv. Qed.
Lemma himpl_hwand_r_inv : ∀ H1 H2 H3,
  H1 ==> (H2 \−∗ H3) →
  H2 \* H1 ==> H3.
Proof using. introv M. rewrite¬<- hwand_equiv. Qed.
Lemma hwand_cancel : ∀ H1 H2,
  H1 \* (H1 \−∗ H2) ==> H2.
Proof using. intros. applys himpl_hwand_r_inv. applys himpl_refl. Qed.
Arguments hwand_cancel : clear implicits.
Lemma himpl_hempty_hwand_same : ∀ H,
  \[] ==> (H \−∗ H).
Proof using. intros. apply himpl_hwand_r. rewrite¬hstar_hempty_r. Qed.
Lemma hwand_hempty_l : ∀ H,
  (\[] \−∗ H) = H.
Proof using.
  intros. applys himpl_antisym.
  { rewrite <- hstar_hempty_l at 1. applys hwand_cancel. }
  { rewrite hwand_equiv. rewrite¬hstar_hempty_l. }
Qed.
Lemma hwand_hpure_l : ∀ P H,
  P →
  (\[P] \−∗ H) = H.
Proof using.
  introv HP. applys himpl_antisym.
  { lets K: hwand_cancel \[P] H. applys himpl_trans K.
    applys* himpl_hstar_hpure_r. }
  { rewrite hwand_equiv. applys* himpl_hstar_hpure_l. }
Qed.
Lemma hwand_curry : ∀ H1 H2 H3,
  (H1 \* H2) \−∗ H3 ==> H1 \−∗ (H2 \−∗ H3).
Proof using.
  intros. apply himpl_hwand_r. apply himpl_hwand_r.
  rewrite <- hstar_assoc. rewrite (hstar_comm H1 H2).
  applys hwand_cancel.
Qed.
Lemma hwand_uncurry : ∀ H1 H2 H3,
  H1 \−∗ (H2 \−∗ H3) ==> (H1 \* H2) \−∗ H3.
Proof using.
  intros. rewrite hwand_equiv. rewrite (hstar_comm H1 H2).
  rewrite hstar_assoc. applys himpl_hstar_trans_r.
  { applys hwand_cancel. } { applys hwand_cancel. }
Qed.
Lemma hwand_curry_eq : ∀ H1 H2 H3,
  (H1 \* H2) \−∗ H3 = H1 \−∗ (H2 \−∗ H3).
Proof using.
  intros. applys himpl_antisym.
  { applys hwand_curry. }
  { applys hwand_uncurry. }
Qed.
Lemma hwand_inv : ∀ h1 h2 H1 H2,
  (H1 \−∗ H2) h2 →
  H1 h1 →
  Fmap.disjoint h1 h2 →
  H2 (h1 \u h2).
Proof using.
  introv M2 M1 D. unfolds hwand. lets (H0&M3): hexists_inv M2.
  lets (h0&h3&P1&P3&D'&U): hstar_inv M3. lets (P4&E3): hpure_inv P3.
  subst h2 h3. rewrite union_empty_r in *. applys P4. applys* hstar_intro.
Qed.

Properties of qwand

Lemma qwand_equiv : ∀ H A (Q1 Q2:A→hprop),
  H ==> (Q1 \−−∗ Q2) ↔ (Q1 \*+ H) ===> Q2.
Proof using.
  unfold qwand. iff M.
  { intros x. rewrite hstar_comm. applys himpl_hstar_trans_l (rm M).
    applys himpl_trans. applys hstar_hforall. simpl.
    applys himpl_hforall_l x. rewrite hstar_comm. applys hwand_cancel. }
  { applys himpl_hforall_r. intros x. rewrite* hwand_equiv. }
Qed.
Lemma qwand_cancel : ∀ A (Q1 Q2:A→hprop),
  Q1 \*+ (Q1 \−−∗ Q2) ===> Q2.
Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.
Lemma himpl_qwand_r : ∀ A (Q1 Q2:A→hprop) H,
  Q1 \*+ H ===> Q2 →
  H ==> (Q1 \−−∗ Q2).
Proof using. introv M. rewrite¬qwand_equiv. Qed.
Arguments himpl_qwand_r [A].
Lemma qwand_specialize : ∀ A (x:A) (Q1 Q2:A→hprop),
  (Q1 \−−∗ Q2) ==> (Q1 x \−∗ Q2 x).
Proof using. intros. applys* himpl_hforall_l x. Qed.
Arguments qwand_specialize [ A ].

Properties of htop

Lemma htop_intro : ∀ h,
  \Top h.
Proof using. intros. ∃¬(=h). Qed.
Lemma himpl_htop_r : ∀ H,
  H ==> \Top.
Proof using. intros. intros h Hh. applys* htop_intro. Qed.
Lemma htop_eq :
  \Top = (\∃ H, H).
Proof using. auto. Qed.
Lemma hstar_htop_htop :
  \Top \* \Top = \Top.
Proof using.
  applys himpl_antisym.
  { applys himpl_htop_r. }
  { rewrite <- hstar_hempty_r at 1. applys himpl_frame_r. applys himpl_htop_r. }
Qed.

Properties of hsingle

Lemma hsingle_intro : ∀ p v,
  (p ~~> v) (Fmap.single p v).
Proof using. intros. hnfs*. Qed.
Lemma hsingle_inv: ∀ p v h,
  (p ~~> v) h →
  h = Fmap.single p v.
Proof using. auto. Qed.
Lemma hstar_hsingle_same_loc : ∀ p w1 w2,
  (p ~~> w1) \* (p ~~> w2) ==> \[False].
Proof using.
  intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
  subst. applys* Fmap.disjoint_single_single_same_inv.
Qed.
Arguments hstar_hsingle_same_loc : clear implicits.

Definition and Properties of haffine and hgc

Definition haffine (H:hprop) :=
  True.
Lemma haffine_hany : ∀ (H:hprop),
  haffine H.
Proof using. unfold haffine. auto. Qed.
Lemma haffine_hempty :
  haffine \[].
Proof using. applys haffine_hany. Qed.
Definition hgc := (* equivalent to \∃ H, \[haffine H] \* H *)
  htop.
Notation "\GC" := (hgc) : hprop_scope.
Lemma haffine_hgc :
  haffine \GC.
Proof using. applys haffine_hany. Qed.
Lemma himpl_hgc_r : ∀ H,
  haffine H →
  H ==> \GC.
Proof using. introv M. applys himpl_htop_r. Qed.
Lemma hstar_hgc_hgc :
  \GC \* \GC = \GC.
Proof using. applys hstar_htop_htop. Qed.

Functor Instantiation to Obtain xsimpl

End SepSimplArgs.
We are now ready to instantiate the functor that defines xsimpl. Demos of xsimpl are presented in chapter Himpl.v.
Module Export HS := LibSepSimpl.XsimplSetup(SepSimplArgs).
Export SepSimplArgs.
From now on, all operators have opaque definitions.
Global Opaque hempty hpure hstar hsingle hexists hforall
              hwand qwand htop hgc haffine.
At this point, the tactic xsimpl is defined. There remains to customize the tactic so that it recognizes the predicate p ~~> v in a special way when performing simplifications.
The tactic xsimpl_hook_hsingle p v operates as part of xsimpl. The specification that follows makes sense only in the context of the presentation of the invariants of xsimpl described in LibSepSimpl.v. This tactic is invoked on goals of the form Xsimpl (Hla, Hlw, Hlt) HR, where Hla is of the form H1 \* .. \* Hn \* \[]. The tactic xsimpl_hook_hsingle p v searches among the Hi for a heap predicate of the form p ~~> v'. If it finds one, it moves this Hi to the front, just before H1. Then, it cancels it out with the p ~~> v that occurs in HR. Otherwise, the tactic fails.
Ltac xsimpl_hook_hsingle p :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with (hsingle p ?v') ⇒
      constr:(true) end);
  apply xsimpl_lr_cancel_eq;
  [ xsimpl_lr_cancel_eq_repr_post tt | ].
The tactic xsimpl_hook handles cancellation of heap predicates of the form p ~~> v. It forces their cancellation against heap predicates of the form p ~~> w, by asserting the equality v = w. Note: this tactic is later refined to also handle records.
Ltac xsimpl_hook H ::=
  match H with
  | hsingle ?p ?v ⇒ xsimpl_hook_hsingle p
  end.
One last hack is to improve the math tactic so that it is able to handle the val_int coercion in goals and hypotheses of the form val_int ?n = val_int ?m, and so that it is able to process the well-founded relations dowto and upto for induction on integers.
Ltac math_0 ::=
  unfolds downto, upto;
  repeat match goal with
  | ⊢ val_int _ = val_int _ ⇒ fequal
  | H: val_int _ = val_int _ ⊢ _ ⇒ inverts H
  end.

Properties of haffine

The lemma haffine_any asserts that haffine H holds for any H. Nevertheless, let us state corollaries of haffine_any for specific heap predicates, to illustrate how the xaffine tactic works in chapter Affine.
Lemma haffine_hempty :
  haffine \[].
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hpure : ∀ P,
  haffine \[P].
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hstar : ∀ H1 H2,
  haffine H1 →
  haffine H2 →
  haffine (H1 \* H2).
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hexists : ∀ A (J:A→hprop),
  (∀ x, haffine (J x)) →
  haffine (\∃ x, (J x)).
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),
  (∀ x, haffine (J x)) →
  haffine (\∀ x, (J x)).
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hstar_hpure : ∀ (P:Prop) H,
  (P → haffine H) →
  haffine (\[P] \* H).
Proof using. intros. applys haffine_hany. Qed.
Lemma haffine_hgc :
  haffine \GC.
Proof using. intros. applys haffine_hany. Qed.
Using these lemmas, we are able to configure the xaffine tactic.
Ltac xaffine_core tt ::=
  repeat match goal with ⊢ haffine ?H ⇒
    match H with
    | (hempty) ⇒ apply haffine_hempty
    | (hpure _) ⇒ apply haffine_hpure
    | (hstar _ _) ⇒ apply haffine_hstar
    | (hexists _) ⇒ apply haffine_hexists
    | (hforall _) ⇒ apply haffine_hforall
    | (hgc) ⇒ apply haffine_hgc
    | _ ⇒ eauto with haffine
    end
  end.

Reasoning Rules

Implicit Types P : Prop.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.

Definition of Separation Logic Triples.

The Separation Logic triple triple t H Q is defined in terms of the omni-big-step semantics predicate eval s t Q.
Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
  ∀ s, H s → eval s t Q.
We introduce a handy notation for postconditions of functions that return a pointer: funloc p ⇒ H is short for fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* H).
Notation "'funloc' p '=>' H" :=
  (fun (r:val) ⇒ \∃ p, \[r = val_loc p] \* H)
  (at level 200, p name, format "'funloc' p '=>' H") : hprop_scope.

Soundness of Triples w.r.t. the Small-Step Semantics

If one considers 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, one considers 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 satisfy H are: (1) terminating, (2) always reaching a value, and (3) this value and the final state obtained satisfy the postconditon Q.
The judgment terminates s t is defined inductively. The execution starting from (s,t) terminates if, for 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.
Inductive terminates : state→trm→Prop :=
  | terminates_step : ∀ s t,
      (∀ s' t', step s t s' t' → terminates s' t') →
      terminates s t.
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.
Definition safe (s:state) (t:trm) : Prop :=
  ∀ s' t', steps s t s' t' → notstuck s' t'.
The judgment correct s t Q asserts that if the execution of (s,t) reaches a final configuration, then this final configuration satisfies Q.
Definition correct (s:state) (t:trm) (Q:val→hprop) : Prop :=
  ∀ s' v, steps s t s' v → Q v s'.
The aim is to show that triple t H Q entails that, for any s satisfying H, terminates s t and safe s t and correct s t Q holds.
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.
Inductive seval : state→trm->(val→hprop)->Prop :=
  | seval_val : ∀ s v Q,
      Q v s →
      seval s v Q
  | seval_step : ∀ s t Q,
      reducible s t → (* (exists s' t', step s t s' t') *)
      (∀ s' t', step s t s' t' → seval s' t' Q) →
      seval s t Q.
The judgment seval s t Q satisfies the 3 targeted soundness properties.
Lemma seval_terminates : ∀ s t Q,
  seval s t Q →
  terminates s t.
Proof using.
  introv M. induction M; constructors; introv R.
  { inverts R. }
  { eauto. }
Qed.
Lemma seval_safe : ∀ s t Q,
  seval s t Q →
  safe s t.
Proof using.
  introv M R. gen Q. induction R; intros.
  { inverts M. { left. hnfs*. } { right*. } }
  { rename H into S. inverts M. { inverts S. } { applys* IHR. } }
Qed.
Lemma seval_correct : ∀ s t Q,
  seval s t Q →
  correct s t Q.
Proof using.
  introv M. induction M; introv R.
  { inverts R as. { auto. } { introv S. inverts S. } }
  { rename H1 into IH. inverts R. { lets (?&?&R): H. inverts R. } applys* IH. }
Qed.
false_step is a handy tactic to get rid of goals with assumptions of the form step s v s' t' or step s (op v) s' t' for a binary operator op.
Ltac false_step :=
  solve [ match goal with
  | K: step _ (trm_app (trm_val (val_prim _)) (trm_val _)) _ _ ⊢ _ ⇒
      inversion K; clear K; subst; false_step
  | K: step _ (trm_val _) _ _ ⊢ _ ⇒
      inversion K; clear K; subst
  | _ ⇒ false
  end ].
The proof that eval s t Q entails seval s t Q begins with a bunch of auxiliary lemmas.
Lemma seval_fun : ∀ s x t1 Q,
  Q (val_fun x t1) s →
  seval s (trm_fun x t1) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructor. }
  { introv R. inverts R. { applys seval_val. applys M. } }
Qed.
Lemma seval_fix : ∀ s f x t1 Q,
  Q (val_fix f x t1) s →
  seval s (trm_fix f x t1) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructor. }
  { introv R. inverts R. { applys seval_val. applys M. } }
Qed.
Lemma seval_app_fun : ∀ s x v1 v2 t1 Q,
  v1 = val_fun x t1 →
  seval s (subst x v2 t1) Q →
  seval s (trm_app v1 v2) Q.
Proof using.
  introv E M. applys seval_step.
  { do 2 esplit. applys* step_app_fun. }
  { introv R. invert R; try solve [intros; false | introv R; inverts R]. introv → → → → → R. inverts E. applys M. }
Qed.
Lemma seval_app_fix : ∀ s f x v1 v2 t1 Q,
  v1 = val_fix f x t1 →
  seval s (subst x v2 (subst f v1 t1)) Q →
  seval s (trm_app v1 v2) Q.
Proof using.
  introv E M. applys seval_step.
  { do 2 esplit. applys* step_app_fix. }
  { introv R. invert R; try solve [intros; false | introv R; inverts R]. introv → → → → → R. inverts E. applys M. }
Qed.
Lemma seval_seq : ∀ s t1 t2 Q1 Q,
  seval s t1 Q1 →
  (∀ s1 v1, Q1 v1 s1 → seval s1 t2 Q) →
  seval s (trm_seq t1 t2) Q.
Proof using.
  introv M1 M2. gen_eq Q1': Q1.
  induction M1; intros; subst.
  { apply seval_step.
    { do 2 esplit. applys step_seq. }
    { introv R. inverts R as R'. { inverts R'. } applys* M2. } }
  { rename t into t1, H1 into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. constructors. applys RE. }
    { introv R. inverts R as R'.
      { applys* IH R' M2. }
      { false. inverts RE. } } }
Qed.
Lemma seval_let : ∀ s x t1 t2 Q1 Q,
  seval s t1 Q1 →
  (∀ s1 v1, Q1 v1 s1 → seval s1 (subst x v1 t2) Q) →
  seval s (trm_let x t1 t2) Q.
Proof using.
  introv M1 M2. gen_eq Q1': Q1.
  induction M1; intros; subst.
  { apply seval_step.
    { do 2 esplit. applys step_let. }
    { introv R. inverts R as R'. { inverts R'. } applys* M2. } }
  { rename t into t1, H1 into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. constructors. applys RE. }
    { introv R. inverts R as R'.
      { applys* IH R' M2. }
      { false. inverts RE. } } }
Qed.
Lemma seval_app_arg1 : ∀ t1 t2 Q1 s1 Q,
  seval s1 t1 Q1 →
  (∀ v1 s2, Q1 v1 s2 → seval s2 (v1 t2) Q) →
  seval s1 (t1 t2) Q.
Proof using.
  introv M1 M2. gen_eq Q1': Q1.
  induction M1; intros; subst.
  { applys* M2. }
  { rename t into t1, H1 into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. applys step_app_arg1. applys RE. }
    { introv R. inverts R as R'; try solve [inverts RE]; try false_step.
      { applys* IH R'. } } }
Qed.
Lemma seval_app_arg2 : ∀ v1 t2 Q1 s1 Q,
  seval s1 t2 Q1 →
  (∀ v2 s2, Q1 v2 s2 → seval s2 (v1 v2) Q) →
  seval s1 (v1 t2) Q.
Proof using.
  introv M1 M2. gen_eq Q1': Q1.
  induction M1; intros; subst.
  { applys* M2. }
  { rename t into t1, H1 into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. applys step_app_arg2. applys RE. }
    { introv R. inverts R as R'; try solve [inverts RE]; try false_step.
      { applys* IH R'. } } }
Qed.
Lemma seval_if : ∀ s b t1 t2 Q,
  seval s (if b then t1 else t2) Q →
  seval s (trm_if b t1 t2) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructors*. }
  { introv R. inverts R; tryfalse. { applys M. } }
Qed.
Lemma seval_of_eval : ∀ s t Q,
  eval s t Q →
  seval s t Q.
Proof using.
  introv M. induction M.
  { applys* seval_val. }
  { applys* seval_fun. }
  { applys* seval_fix. }
  { applys* seval_app_arg1. }
  { applys* seval_app_arg2. }
  { applys* seval_app_fun. }
  { applys* seval_app_fix. }
  { applys* seval_seq. }
  { applys* seval_let. }
  { applys* seval_if. }
  { rename H into HE, H0 into K. unfolds purepostin.
    applys seval_step.
    { inverts HE; try solve [do 2 esplit; constructor; eauto].
      { ∃ s 0. applys step_rand. math. } }
    { introv R. inverts R; try false_step; inverts HE; applys* seval_val. } }
   { rename H into HE, H0 into K. unfolds purepostin.
    applys seval_step.
    { inverts HE; try solve [do 2 esplit; constructor; eauto]. }
    { introv R. inverts R; do 2 (try inverts_if_head step); inverts HE; applys* seval_val.
      (* alternative: inverts HE; inverts R; try false_step; applys* seval_val. *)
      { math_rewrite (p2 = p3). { applys eq_nat_of_eq_int. math. } eauto. } } }
  { applys seval_step.
    { forwards¬(p&D&N): (exists_fresh null s).
      do 2 esplit. applys* step_ref. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_get. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_set. }
    { introv R. do 3 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_free. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
Qed.
Final soundness theorem with respect to the small-step semantics.
Lemma triple_sound : ∀ t H Q,
  triple t H Q →
  ∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.
Proof using.
  introv M Hs. specializes M Hs. lets M': seval_of_eval M. splits.
  { applys* seval_terminates. }
  { applys* seval_safe. }
  { applys* seval_correct. }
Qed.

Structural Properties of the eval Predicate

Section EvalProp.
Hint Constructors eval.
Covariance property
Lemma eval_conseq : ∀ s t Q1 Q2,
  eval s t Q1 →
  Q1 ===> Q2 →
  eval s t Q2.
Proof using.
  introv M W.
  asserts W': (∀ v h, Q1 v h → Q2 v h). { auto. } clear W.
  induction M; try solve [ constructors* ].
  { applys* eval_unop. unfolds* purepostin. }
  { applys* eval_binop. unfolds* purepostin. }
Qed.
Frame property
Lemma eval_frame : ∀ h1 h2 t Q,
  eval h1 t Q →
  Fmap.disjoint h1 h2 →
  eval (h1 \u h2) t (Q \*+ (= h2)).
Proof using.
  introv M HD. gen h2. induction M; intros;
    try solve [ hint hstar_intro; constructors* ].
  { rename M into M1, H into M2, IHM into IH1, H1 into IH2.
    specializes IH1 HD. applys* eval_app_arg1 IH1. introv HK.
    lets (h1'&h2'&K1'&K2'&KD&KU): hstar_inv HK. subst. applys* IH2. }
  { rename M into M1, H into M2, IHM into IH1, H1 into IH2.
    specializes IH1 HD. applys* eval_app_arg2 IH1. introv HK.
    lets (h1'&h2'&K1'&K2'&KD&KU): hstar_inv HK. subst. applys* IH2. }
  { rename M into M1, H into M2, IHM into IH1, H0 into IH2.
    specializes IH1 HD. applys eval_seq IH1. introv HK.
    lets (h1'&h2'&K1'&K2'&KD&KU): hstar_inv HK. subst. applys* IH2. }
  { rename M into M1, H into M2, IHM into IH1, H0 into IH2.
    specializes IH1 HD. applys eval_let IH1. introv HK.
    lets (h1'&h2'&K1'&K2'&KD&KU): hstar_inv HK. subst. applys* IH2. }
  { applys* eval_unop. unfolds* purepostin. introv Hv. applys* hstar_intro. }
  { applys* eval_binop. unfolds* purepostin. introv Hv. applys* hstar_intro. }
  { rename H into M. applys eval_ref. intros p Hp.
    rewrite Fmap.indom_union_eq in Hp. rew_logic in Hp. destruct Hp as [Hp1 Hp2].
    rewrite* Fmap.update_union_not_r. applys hstar_intro.
    { applys* M. } { auto. } { applys* Fmap.disjoint_update_not_r. } }
  { applys eval_get. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.read_union_l. applys* hstar_intro. } }
  { applys eval_set. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.update_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_update_l. } } }
  { applys eval_free. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.remove_disjoint_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_remove_l. } } }
Qed.
End EvalProp.

Structural Rules

Consequence and frame rule.
Lemma triple_conseq : ∀ t H' Q' H Q,
  triple t H' Q' →
  H ==> H' →
  Q' ===> Q →
  triple t H Q.
Proof using. unfolds triple. introv M MH MQ HF. applys* eval_conseq. Qed.
Lemma triple_frame : ∀ t H Q H',
  triple t H Q →
  triple t (H \* H') (Q \*+ H').
Proof.
  introv M. intros h HF. lets (h1&h2&M1&M2&MD&MU): hstar_inv (rm HF).
  subst. specializes M M1. applys eval_conseq.
  { applys eval_frame M MD. } { xsimpl. intros h' →. applys M2. }
Qed.
Extraction Rules
Lemma triple_hpure : ∀ t (P:Prop) H Q,
  (P → triple t H Q) →
  triple t (\[P] \* H) Q.
Proof using.
  introv M. intros h (h1&h2&M1&M2&D&U). destruct M1 as (M1&HP).
  lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.
Qed.
Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,
  (∀ (x:A), triple t (J x) Q) →
  triple t (hexists J) Q.
Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.
Lemma triple_hforall : ∀ t (A:Type) (x:A) (J:A→hprop) Q,
  triple t (J x) Q →
  triple t (hforall J) Q.
Proof using. introv M. applys* triple_conseq M. applys hforall_specialize. Qed.
Lemma triple_hwand_hpure_l : ∀ t (P:Prop) H Q,
  P →
  triple t H Q →
  triple t (\[P] \−∗ H) Q.
Proof using. introv HP M. applys* triple_conseq M. rewrite* hwand_hpure_l. Qed.
A corollary of triple_hpure useful for the course
Parameter triple_hpure' : ∀ t (P:Prop) Q,
  (P → triple t \[] Q) →
  triple t \[P] Q.
Heap-naming rule
Lemma triple_named_heap : ∀ t H Q,
  (∀ h, H h → triple t (= h) Q) →
  triple t H Q.
Proof using. introv M Hs. applys M Hs. auto. Qed.
Combined and ramified rules.
Lemma triple_conseq_frame : ∀ H2 H1 Q1 t H Q,
  triple t H1 Q1 →
  H ==> H1 \* H2 →
  Q1 \*+ H2 ===> Q →
  triple t H Q.
Proof using.
  introv M WH WQ. applys triple_conseq WH WQ. applys triple_frame M.
Qed.
Lemma triple_ramified_frame : ∀ H1 Q1 t H Q,
  triple t H1 Q1 →
  H ==> H1 \* (Q1 \−−∗ Q) →
  triple t H Q.
Proof using.
  introv M W. applys triple_conseq_frame (Q1 \−−∗ Q) M W.
  { rewrite¬<- qwand_equiv. }
Qed.

Rules for Terms

Lemma triple_eval_like : ∀ t1 t2 H Q,
  eval_like t1 t2 →
  triple t1 H Q →
  triple t2 H Q.
Proof using. introv E M1 Hv. applys* E. Qed.
Lemma triple_val : ∀ v H Q,
  H ==> Q v →
  triple (trm_val v) H Q.
Proof using. introv M Hs. applys* eval_val. Qed.
Lemma triple_val_minimal : ∀ v,
  triple (trm_val v) \[] (fun r ⇒ \[r = v]).
Proof using. intros. applys triple_val. xsimpl*. Qed.
Lemma triple_fun : ∀ x t1 H Q,
  H ==> Q (val_fun x t1) →
  triple (trm_fun x t1) H Q.
Proof using. introv M Hs. applys* eval_fun. Qed.
Lemma triple_fix : ∀ f x t1 H Q,
  H ==> Q (val_fix f x t1) →
  triple (trm_fix f x t1) H Q.
Proof using. introv M Hs. applys* eval_fix. Qed.
Lemma triple_seq : ∀ t1 t2 H Q H1,
  triple t1 H (fun v ⇒ H1) →
  triple t2 H1 Q →
  triple (trm_seq t1 t2) H Q.
Proof using. introv M1 M2 Hs. applys* eval_seq. Qed.
Lemma triple_let : ∀ x t1 t2 Q1 H Q,
  triple t1 H Q1 →
  (∀ v1, triple (subst x v1 t2) (Q1 v1) Q) →
  triple (trm_let x t1 t2) H Q.
Proof using. introv M1 M2 Hs. applys* eval_let. Qed.
Lemma triple_let_val : ∀ x v1 t2 H Q,
  triple (subst x v1 t2) H Q →
  triple (trm_let x v1 t2) H Q.
Proof using.
  introv M. applys triple_let (fun v ⇒ \[v = v1] \* H).
  { applys triple_val. xsimpl*. }
  { intros v. applys triple_hpure. intros →. applys M. }
Qed.
Lemma triple_if : ∀ (b:bool) t1 t2 H Q,
  triple (if b then t1 else t2) H Q →
  triple (trm_if b t1 t2) H Q.
Proof using. introv M Hs. applys* eval_if. Qed.
Lemma triple_app_fun : ∀ x v1 v2 t1 H Q,
  v1 = val_fun x t1 →
  triple (subst x v2 t1) H Q →
  triple (trm_app v1 v2) H Q.
Proof using. introv E M Hs. applys* eval_app_fun. Qed.
Lemma triple_app_fun_direct : ∀ x v2 t1 H Q,
  triple (subst x v2 t1) H Q →
  triple (trm_app (val_fun x t1) v2) H Q.
Proof using. introv M. applys* triple_app_fun. Qed.
Lemma triple_app_fix : ∀ v1 v2 f x t1 H Q,
  v1 = val_fix f x t1 →
  triple (subst x v2 (subst f v1 t1)) H Q →
  triple (trm_app v1 v2) H Q.
Proof using. introv E M Hs. applys* eval_app_fix. Qed.
Lemma triple_app_fix_direct : ∀ v2 f x t1 H Q,
  f ≠ x →
  triple (subst x v2 (subst f (val_fix f x t1) t1)) H Q →
  triple (trm_app (val_fix f x t1) v2) H Q.
Proof using. introv N M. applys* triple_app_fix. Qed.

Rules for Heap-Manipulating Primitive Operations

Lemma triple_ref : ∀ v,
  triple (val_ref v)
    \[]
    (fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).
Proof using.
  intros. intros s1 K. applys eval_ref. intros p D.
  lets ->: hempty_inv K. rewrite Fmap.update_empty.
  applys hexists_intro p. rewrite hstar_hpure_l. split*.
  applys hsingle_intro.
Qed.
Lemma triple_get : ∀ v p,
  triple (val_get p)
    (p ~~> v)
    (fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
  intros. intros s K. lets ->: hsingle_inv K.
  applys eval_get.
  { applys* Fmap.indom_single. }
  { rewrite hstar_hpure_l. split*. rewrite* Fmap.read_single. }
Qed.
Lemma triple_set : ∀ w p v,
  triple (val_set (val_loc p) v)
    (p ~~> w)
    (fun r ⇒ \[r = val_unit] \* (p ~~> v)).
Proof using.
  intros. intros s1 K. lets ->: hsingle_inv K. lets Hp: indom_single p v.
  applys eval_set.
  { applys* Fmap.indom_single. }
  { rewrite hstar_hpure_l. split*. rewrite Fmap.update_single. applys hsingle_intro. }
Qed.
Lemma triple_free' : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun r ⇒ \[r = val_unit]).
Proof using.
  intros. intros s1 K. lets ->: hsingle_inv K. lets Hp: indom_single p v.
  applys eval_free.
  { applys* Fmap.indom_single. }
  { rewrite* Fmap.remove_single. applys* hpure_intro. }
Qed.
Lemma triple_free : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun r ⇒ \[]).
Proof using. intros. applys triple_conseq triple_free'; xsimpl*. Qed.

Rules for Other Primitive Operations

Lemma triple_unop' : ∀ op v1 (P:val→Prop) Q, (* DEPRECATED? *)
  evalunop op v1 P →
  (∀ v, P v → Q v Fmap.empty) → (* purepostin heap_empty P Q ->*)
  triple (op v1) \[] Q.
Proof using.
  introv M R Hs. lets ->: hempty_inv Hs. applys eval_unop M. hnfs*.
Qed.
Lemma triple_binop' : ∀ op v1 v2 (P:val→Prop) Q, (* DEPRECATED? *)
  evalbinop op v1 v2 P →
  (∀ v, P v → Q v Fmap.empty) →
  triple (op v1 v2) \[] Q.
Proof using.
  introv M R Hs. lets ->: hempty_inv Hs. applys eval_binop M. hnfs*.
Qed.
Lemma triple_unop : ∀ op v1 (P:val→Prop),
  evalunop op v1 P →
  triple (op v1) \[] (fun r ⇒ \[P r]).
Proof using.
  introv M Hs. lets ->: hempty_inv Hs.
  applys eval_conseq (fun v s ⇒ P v ∧ s = Fmap.empty).
  { applys* eval_unop M. hnfs*. }
  { intros v s (?&->). applys* hpure_intro. }
Qed.
Lemma triple_binop : ∀ op v1 v2 (P:val→Prop),
  evalbinop op v1 v2 P →
  triple (op v1 v2) \[] (fun r ⇒ \[P r]).
Proof using.
  introv M Hs. lets ->: hempty_inv Hs.
  applys eval_conseq (fun v s ⇒ P v ∧ s = Fmap.empty).
  { applys* eval_binop M. hnfs*. }
  { intros v s (?&->). applys* hpure_intro. }
Qed.
Lemma triple_add : ∀ n1 n2,
  triple (val_add n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (n1 + n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_add. Qed.
Lemma triple_div : ∀ n1 n2,
  n2 ≠ 0 →
  triple (val_div n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (Z.quot n1 n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_div. Qed.
Lemma triple_rand : ∀ n,
  n > 0 →
  triple (val_rand n)
    \[]
    (fun r ⇒ \[∃ n1, r = val_int n1 ∧ 0 ≤ n1 < n]).
Proof using. intros. applys* triple_unop. applys* evalunop_rand. Qed.
Lemma triple_neg : ∀ (b1:bool),
  triple (val_neg b1)
    \[]
    (fun r ⇒ \[r = val_bool (neg b1)]).
Proof using. intros. applys* triple_unop. applys* evalunop_neg. Qed.
Lemma triple_opp : ∀ n1,
  triple (val_opp n1)
    \[]
    (fun r ⇒ \[r = val_int (- n1)]).
Proof using. intros. applys* triple_unop. applys* evalunop_opp. Qed.
Lemma triple_eq : ∀ v1 v2,
  triple (val_eq v1 v2)
    \[]
    (fun r ⇒ \[r = isTrue (v1 = v2)]).
Proof using. intros. applys* triple_binop. applys evalbinop_eq. Qed.
Lemma triple_neq : ∀ v1 v2,
  triple (val_neq v1 v2)
    \[]
    (fun r ⇒ \[r = isTrue (v1 ≠ v2)]).
Proof using. intros. applys* triple_binop. applys evalbinop_neq. Qed.
Lemma triple_sub : ∀ n1 n2,
  triple (val_sub n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (n1 - n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_sub. Qed.
Lemma triple_mul : ∀ n1 n2,
  triple (val_mul n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (n1 * n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_mul. Qed.
Lemma triple_mod : ∀ n1 n2,
  n2 ≠ 0 →
  triple (val_mod n1 n2)
    \[]
    (fun r ⇒ \[r = val_int (Z.rem n1 n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_mod. Qed.
Lemma triple_le : ∀ n1 n2,
  triple (val_le n1 n2)
    \[]
    (fun r ⇒ \[r = isTrue (n1 ≤ n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_le. Qed.
Lemma triple_lt : ∀ n1 n2,
  triple (val_lt n1 n2)
    \[]
    (fun r ⇒ \[r = isTrue (n1 < n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_lt. Qed.
Lemma triple_ge : ∀ n1 n2,
  triple (val_ge n1 n2)
    \[]
    (fun r ⇒ \[r = isTrue (n1 ≥ n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_ge. Qed.
Lemma triple_gt : ∀ n1 n2,
  triple (val_gt n1 n2)
    \[]
    (fun r ⇒ \[r = isTrue (n1 > n2)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_gt. Qed.
Lemma triple_ptr_add : ∀ p n,
  p + n ≥ 0 →
  triple (val_ptr_add p n)
    \[]
    (fun r ⇒ \[r = val_loc (abs (p + n))]).
Proof using.
  intros. applys* triple_binop. applys* evalbinop_ptr_add.
  { rewrite¬abs_nonneg. }
Qed.
Lemma triple_ptr_add_nat : ∀ p (f:nat),
  triple (val_ptr_add p f)
    \[]
    (fun r ⇒ \[r = val_loc (p+f)%nat]).
Proof using.
  intros. applys triple_conseq triple_ptr_add. { math. } { xsimpl. }
  { xsimpl. intros. subst. fequals.
    applys eq_nat_of_eq_int. rewrite abs_nonneg; math. }
Qed.

Structural Rule for wp

Definition of wp
Definition wp (t:trm) (Q:val→hprop) : hprop :=
  fun s ⇒ eval s t Q.
Equivalence between wp and triple
Lemma wp_equiv : ∀ t H Q,
  (H ==> wp t Q) ↔ (triple t H Q).
Proof using. intros. unfold wp, triple. iff*. Qed.
Consequence rule for wp.
Lemma wp_conseq : ∀ t Q1 Q2,
  Q1 ===> Q2 →
  wp t Q1 ==> wp t Q2.
Proof using. unfold wp. introv M. intros s Hs. applys* eval_conseq. Qed.
Frame rule for wp.
Lemma wp_frame : ∀ t H Q,
  (wp t Q) \* H ==> wp t (Q \*+ H).
Proof using.
  intros. unfold wp. intros h HF.
  lets (h1&h2&M1&M2&MD&MU): hstar_inv (rm HF).
  subst. applys eval_conseq.
  { applys eval_frame M1 MD. }
  { xsimpl. intros h' →. applys M2. }
Qed.
Corollaries, including ramified frame rule.
Lemma wp_ramified : ∀ t Q1 Q2,
  (wp t Q1) \* (Q1 \−−∗ Q2) ==> (wp t Q2).
Proof using.
  intros. applys himpl_trans.
  { applys wp_frame. }
  { applys wp_conseq. xsimpl. }
Qed.
Lemma wp_conseq_frame : ∀ t H Q1 Q2,
  Q1 \*+ H ===> Q2 →
  (wp t Q1) \* H ==> (wp t Q2).
Proof using.
  introv M. rewrite <- qwand_equiv in M. xchange M. applys wp_ramified.
Qed.
Lemma wp_ramified_trans : ∀ t H Q1 Q2,
  H ==> (wp t Q1) \* (Q1 \−−∗ Q2) →
  H ==> (wp t Q2).
Proof using. introv M. xchange M. applys wp_ramified. Qed.

Weakest-Precondition Style Reasoning Rules for Terms.

Lemma wp_eval_like : ∀ t1 t2 Q,
  eval_like t1 t2 →
  wp t1 Q ==> wp t2 Q.
Proof using. introv E Hs. applys* E Hs. Qed.
Lemma wp_val : ∀ v Q,
  Q v ==> wp (trm_val v) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_val. Qed.
Lemma wp_fun : ∀ x t Q,
  Q (val_fun x t) ==> wp (trm_fun x t) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_fun. Qed.
Lemma wp_fix : ∀ f x t Q,
  Q (val_fix f x t) ==> wp (trm_fix f x t) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_fix. Qed.
Lemma wp_app_fun : ∀ x v1 v2 t1 Q,
  v1 = val_fun x t1 →
  wp (subst x v2 t1) Q ==> wp (trm_app v1 v2) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_app_fun. Qed.
Lemma wp_app_fix : ∀ f x v1 v2 t1 Q,
  v1 = val_fix f x t1 →
  wp (subst x v2 (subst f v1 t1)) Q ==> wp (trm_app v1 v2) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_app_fix. Qed.
Lemma wp_seq : ∀ t1 t2 Q,
  wp t1 (fun r ⇒ wp t2 Q) ==> wp (trm_seq t1 t2) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_seq. Qed.
Lemma wp_let : ∀ x t1 t2 Q,
  wp t1 (fun v ⇒ wp (subst x v t2) Q) ==> wp (trm_let x t1 t2) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_let. Qed.
Lemma wp_if : ∀ b t1 t2 Q,
  wp (if b then t1 else t2) Q ==> wp (trm_if b t1 t2) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_if. Qed.
Lemma wp_if_case : ∀ b t1 t2 Q,
  (if b then wp t1 Q else wp t2 Q) ==> wp (trm_if b t1 t2) Q.
Proof using. intros. applys himpl_trans wp_if. case_if¬. Qed.

WP Generator

This section defines a "weakest-precondition style characteristic formula generator". This technology adapts the technique of "characteristic formulae" (originally developed in CFML 1.0) to produce weakest preconditions. (The formulae, their manipulation, and their correctness proofs are simpler in wp-style.)
The goal of the section is to define a function wpgen t, recursively over the structure of t, such that wpgen t Q entails wp t Q. Unlike wp t Q, which is defined semantically, wpgen t Q is defined following the syntax of t.
Technically, we define wpgen E t, where E is a list of bindings, to compute a formula that entails wp (isubst E t), where isubst E t denotes the iterated substitution of bindings from E inside t.

Definition of Context as List of Bindings

In order to define a structurally recursive and relatively efficient characteristic formula generator, we need to introduce contexts, that essentially serve to apply substitutions lazily.
Open Scope liblist_scope.
A context is an association list from variables to values.
Definition ctx : Type := list (var*val).
lookup x E returns Some v if x is bound to a value v, and None otherwise.
Fixpoint lookup (x:var) (E:ctx) : option val :=
  match E with
  | nil ⇒ None
  | (y,v)::E1 ⇒ if var_eq x y
                   then Some v
                   else lookup x E1
  end.
rem x E denotes the removal of bindings on x from E.
Fixpoint rem (x:var) (E:ctx) : ctx :=
  match E with
  | nil ⇒ nil
  | (y,v)::E1 ⇒
      let E1' := rem x E1 in
      if var_eq x y then E1' else (y,v)::E1'
  end.
ctx_disjoint E1 E2 asserts that the two contexts have disjoint domains.
Definition ctx_disjoint (E1 E2:ctx) : Prop :=
  ∀ x v1 v2, lookup x E1 = Some v1 → lookup x E2 = Some v2 → False.
ctx_equiv E1 E2 asserts that the two contexts bind same keys to same values.
Definition ctx_equiv (E1 E2:ctx) : Prop :=
  ∀ x, lookup x E1 = lookup x E2.
Basic properties of context operations follow.
Section CtxOps.
Lemma lookup_app : ∀ E1 E2 x,
  lookup x (E1 ++ E2) = match lookup x E1 with
                         | None ⇒ lookup x E2
                         | Some v ⇒ Some v
                         end.
Proof using.
  introv. induction E1 as [|(y,w) E1']; rew_list; simpl; intros.
  { auto. } { case_var¬. }
Qed.
Lemma lookup_rem : ∀ x y E,
  lookup x (rem y E) = If x = y then None else lookup x E.
Proof using.
  intros. induction E as [|(z,v) E'].
  { simpl. case_var¬. }
  { simpl. case_var~; simpl; case_var¬. }
Qed.
Lemma rem_app : ∀ x E1 E2,
  rem x (E1 ++ E2) = rem x E1 ++ rem x E2.
Proof using.
  intros. induction E1 as [|(y,w) E1']; rew_list; simpl. { auto. }
  { case_var¬. { rew_list. fequals. } }
Qed.
Lemma ctx_equiv_rem : ∀ x E1 E2,
  ctx_equiv E1 E2 →
  ctx_equiv (rem x E1) (rem x E2).
Proof using.
  introv M. unfolds ctx_equiv. intros y.
  do 2 rewrite lookup_rem. case_var¬.
Qed.
Lemma ctx_disjoint_rem : ∀ x E1 E2,
  ctx_disjoint E1 E2 →
  ctx_disjoint (rem x E1) (rem x E2).
Proof using.
  introv D. intros y v1 v2 K1 K2. rewrite lookup_rem in *.
  case_var¬. applys* D K1 K2.
Qed.
Lemma ctx_disjoint_equiv_app : ∀ E1 E2,
  ctx_disjoint E1 E2 →
  ctx_equiv (E1 ++ E2) (E2 ++ E1).
Proof using.
  introv D. intros x. do 2 rewrite¬lookup_app.
  case_eq (lookup x E1); case_eq (lookup x E2); auto.
  { intros v2 K2 v1 K1. false* D. }
Qed.
End CtxOps.

Multi-Substitution

Definition of Multi-Substitution

The specification of the characteristic formula generator is expressed using the multi-substitution function, which substitutes a list of bindings inside a term.
Fixpoint isubst (E:ctx) (t:trm) : trm :=
  match t with
  | trm_val v ⇒
       v
  | trm_var x ⇒
       match lookup x E with
       | None ⇒ t
       | Some v ⇒ v
       end
  | trm_fun x t1 ⇒
       trm_fun x (isubst (rem x E) t1)
  | trm_fix f x t1 ⇒
       trm_fix f x (isubst (rem x (rem f E)) t1)
  | trm_if t0 t1 t2 ⇒
       trm_if (isubst E t0) (isubst E t1) (isubst E t2)
  | trm_seq t1 t2 ⇒
       trm_seq (isubst E t1) (isubst E t2)
  | trm_let x t1 t2 ⇒
       trm_let x (isubst E t1) (isubst (rem x E) t2)
  | trm_app t1 t2 ⇒
       trm_app (isubst E t1) (isubst E t2)
  end.

Properties of Multi-Substitution

The goal of this entire section is only to establish isubst_nil and isubst_rem, which assert:
        isubst nil t = t
    and
        isubst ((x,v)::E) t = subst x v (isubst (rem x E) t)
isubst_nil explains that the empty substitution is the identity.
Lemma isubst_nil : ∀ t,
  isubst nil t = t.
Proof using. intros t. induction t; simpl; fequals. Qed.
subst_eq_isubst_one relates subst and isubst.
Lemma subst_eq_isubst_one : ∀ x v t,
  subst x v t = isubst ((x,v)::nil) t.
Proof using.
  intros. induction t; simpl.
  { fequals. }
  { case_var¬. }
  { fequals. case_var¬. { rewrite¬isubst_nil. } }
  { fequals. case_var; try case_var; simpl; try case_var; try rewrite isubst_nil; auto. }
  { fequals*. }
  { fequals*. }
  { fequals*. case_var¬. { rewrite¬isubst_nil. } }
  { fequals*. }
Qed.
The next lemma shows that equivalent contexts produce equal results for isubst.
Lemma isubst_ctx_equiv : ∀ t E1 E2,
  ctx_equiv E1 E2 →
  isubst E1 t = isubst E2 t.
Proof using.
  hint ctx_equiv_rem.
  intros t. induction t; introv EQ; simpl; fequals¬.
  { rewrite¬EQ. }
Qed.
isubst_app asserts that isubst distribute over concatenation.
Lemma isubst_app : ∀ t E1 E2,
  isubst (E1 ++ E2) t = isubst E2 (isubst E1 t).
Proof using.
  hint ctx_disjoint_rem.
  intros t. induction t; simpl; intros.
  { fequals. }
  { rename v into x. rewrite¬lookup_app.
    case_eq (lookup x E1); introv K1; case_eq (lookup x E2); introv K2; auto.
    { simpl. rewrite¬K2. }
    { simpl. rewrite¬K2. } }
  { fequals. rewrite* rem_app. }
  { fequals. do 2 rewrite* rem_app. }
  { fequals*. }
  { fequals*. }
  { fequals*. { rewrite* rem_app. } }
  { fequals*. }
Qed.
isubst_cons is a corollary
Lemma isubst_cons : ∀ x v xvs t,
  isubst ((x,v)::xvs) t = isubst xvs (subst x v t).
Proof using.
  intros. rewrite <- app_cons_one_r. rewrite isubst_app.
  rewrite* <- subst_eq_isubst_one.
Qed.
The next lemma asserts that the concatenation order is irrelevant in a substitution if the contexts have disjoint domains.
Lemma isubst_app_swap : ∀ t E1 E2,
  ctx_disjoint E1 E2 →
  isubst (E1 ++ E2) t = isubst (E2 ++ E1) t.
Proof using.
  introv D. applys isubst_ctx_equiv. applys¬ctx_disjoint_equiv_app.
Qed.
We are ready to derive the second targeted property of isubst.
Lemma isubst_rem : ∀ x v E t,
  isubst ((x, v)::E) t = subst x v (isubst (rem x E) t).
Proof using.
  intros. rewrite subst_eq_isubst_one. rewrite <- isubst_app.
  rewrite isubst_app_swap.
  { applys isubst_ctx_equiv. intros y. rew_list. simpl. rewrite lookup_rem. case_var¬. }
  { intros y v1 v2 K1 K2. simpls. rewrite lookup_rem in K1. case_var. }
Qed.
A variant useful for trm_fix is proved next.
Lemma isubst_rem_2 : ∀ f x vf vx E t,
  isubst ((f,vf)::(x,vx)::E) t = subst x vx (subst f vf (isubst (rem x (rem f E)) t)).
Proof using.
  intros. do 2 rewrite subst_eq_isubst_one. do 2 rewrite <- isubst_app.
  rewrite isubst_app_swap.
  { applys isubst_ctx_equiv. intros y. rew_list. simpl. do 2 rewrite lookup_rem. case_var¬. }
  { intros y v1 v2 K1 K2. rew_listx in *. simpls. do 2 rewrite lookup_rem in K1. case_var. }
Qed.

Definition of wpgen

The definition of wpgen E t comes next. It depends on a predicate called mkstruct for handling structural rules, and on one auxiliary definition for each term rule.

Definition of mkstruct

Let formula denote the type of wp t and wpgen t.
Definition formula := (val → hprop) → hprop.
Implicit Type F : formula.
mkstruct F transforms a formula F into one that satisfies structural rules of Separation Logic. This predicate transformer enables integrating support for the frame rule (and other structural rules), in characteristic formulae.
Definition mkstruct (F:formula) : formula :=
  fun Q ⇒ \∃ Q', F Q' \* (Q' \−−∗ Q).
Lemma mkstruct_ramified : ∀ Q1 Q2 F,
  (mkstruct F Q1) \* (Q1 \−−∗ Q2) ==> (mkstruct F Q2).
Proof using. unfold mkstruct. xsimpl. Qed.
Arguments mkstruct_ramified : clear implicits.
Lemma mkstruct_erase : ∀ Q F,
  F Q ==> mkstruct F Q.
Proof using. unfolds mkstruct. xsimpl. Qed.
Arguments mkstruct_erase : clear implicits.
Lemma mkstruct_conseq : ∀ F Q1 Q2,
  Q1 ===> Q2 →
  mkstruct F Q1 ==> mkstruct F Q2.
Proof using.
  introv WQ. unfolds mkstruct. xpull. intros Q. xsimpl Q. xchanges WQ.
Qed.
Lemma mkstruct_frame : ∀ F H Q,
  (mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).
Proof using.
  intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.
Qed.
Lemma mkstruct_monotone : ∀ F1 F2 Q,
  (∀ Q, F1 Q ==> F2 Q) →
  mkstruct F1 Q ==> mkstruct F2 Q.
Proof using.
  introv WF. unfolds mkstruct. xpull. intros Q'. xchange WF. xsimpl Q'.
Qed.

Definition of Auxiliary Definition for wpgen

we state auxiliary definitions for wpgen, one per term construct. For simplicity, we here assume the term t to be in A-normal form. If it is not, the formula generated will be incomplete, that is, useless to prove triples about the term t. Note that the actual generator in CFML2 does support terms that are not in A-normal form.
Definition wpgen_fail : formula := fun Q ⇒
  \[False].
Definition wpgen_val (v:val) : formula := fun Q ⇒
  Q v.
Definition wpgen_fun (Fof:val→formula) : formula := fun Q ⇒
  \∀ vf, \[∀ vx Q', Fof vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.
Definition wpgen_fix (Fof:val→val→formula) : formula := fun Q ⇒
  \∀ vf, \[∀ vx Q', Fof vf vx Q' ==> wp (trm_app vf vx) Q'] \−∗ Q vf.
Definition wpgen_var (E:ctx) (x:var) : formula :=
  match lookup x E with
  | None ⇒ wpgen_fail
  | Some v ⇒ wpgen_val v
  end.
Definition wpgen_seq (F1 F2:formula) : formula := fun Q ⇒
  F1 (fun v ⇒ F2 Q).
Definition wpgen_let (F1:formula) (F2of:val→formula) : formula := fun Q ⇒
  F1 (fun v ⇒ F2of v Q).
Definition wpgen_if (t:trm) (F1 F2:formula) : formula := fun Q ⇒
  \∃ (b:bool), \[t = trm_val (val_bool b)] \* (if b then F1 Q else F2 Q).
Definition wpgen_if_trm (F0 F1 F2:formula) : formula :=
  wpgen_let F0 (fun v ⇒ mkstruct (wpgen_if v F1 F2)).
Definition wpgen_app (t:trm) : formula := fun Q ⇒
  \∃ H, H \* \[triple t H Q].

Recursive Definition of wpgen

wpgen E t is structurally recursive on t. Note that this function does not recurse through values. Note also that the context E gets extended when traversing bindings, in the let-binding and the function cases.
Fixpoint wpgen (E:ctx) (t:trm) : formula :=
  mkstruct match t with
  | trm_val v ⇒ wpgen_val v
  | trm_var x ⇒ wpgen_var E x
  | trm_fun x t1 ⇒ wpgen_fun (fun v ⇒ wpgen ((x,v)::E) t1)
  | trm_fix f x t1 ⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf)::(x,v)::E) t1)
  | trm_if t0 t1 t2 ⇒ wpgen_if (isubst E t0) (wpgen E t1) (wpgen E t2)
  | trm_seq t1 t2 ⇒ wpgen_seq (wpgen E t1) (wpgen E t2)
  | trm_let x t1 t2 ⇒ wpgen_let (wpgen E t1) (fun v ⇒ wpgen ((x,v)::E) t2)
  | trm_app t1 t2 ⇒ wpgen_app (isubst E t)
  end.

Soundness of wpgen

formula_sound t F asserts that, for any Q, the Separation Logic judgment triple (F Q) t Q is valid. In other words, it states that F is a stronger formula than wp t.
The soundness theorem that we are ultimately interested in asserts that formula_sound (isubst E t) (wpgen E t) holds for any E and t.
Definition formula_sound (t:trm) (F:formula) : Prop :=
  ∀ Q, F Q ==> wp t Q.
Lemma wp_sound : ∀ t,
  formula_sound t (wp t).
Proof using. intros. intros Q. applys himpl_refl. Qed.
One soundness lemma for mkstruct.
Lemma mkstruct_wp : ∀ t,
  mkstruct (wp t) = (wp t).
Proof using.
  intros. applys fun_ext_1. intros Q. applys himpl_antisym.
  { unfold mkstruct. xpull. intros Q'. applys wp_ramified. }
  { applys mkstruct_erase. }
Qed.
Lemma mkstruct_sound : ∀ t F,
  formula_sound t F →
  formula_sound t (mkstruct F).
Proof using.
  introv M. unfolds formula_sound. intros Q'.
  rewrite <- mkstruct_wp. applys* mkstruct_monotone M.
Qed.
One soundness lemma for each term construct.
Lemma wpgen_fail_sound : ∀ t,
  formula_sound t wpgen_fail.
Proof using. intros. intros Q. unfold wpgen_fail. xpull. Qed.
Lemma wpgen_val_sound : ∀ v,
  formula_sound (trm_val v) (wpgen_val v).
Proof using. intros. intros Q. unfolds wpgen_val. applys wp_val. Qed.
Lemma wpgen_fun_sound : ∀ x t1 Fof,
  (∀ vx, formula_sound (subst x vx t1) (Fof vx)) →
  formula_sound (trm_fun x t1) (wpgen_fun Fof).
Proof using.
  introv M. intros Q. unfolds wpgen_fun. applys himpl_hforall_l (val_fun x t1).
  xchange hwand_hpure_l.
  { intros. applys himpl_trans_r. { applys* wp_app_fun. } { applys* M. } }
  { applys wp_fun. }
Qed.
Lemma wpgen_fix_sound : ∀ f x t1 Fof,
  (∀ vf vx, formula_sound (subst x vx (subst f vf t1)) (Fof vf vx)) →
  formula_sound (trm_fix f x t1) (wpgen_fix Fof).
Proof using.
  introv M. intros Q. unfolds wpgen_fix.
  applys himpl_hforall_l (val_fix f x t1). xchange hwand_hpure_l.
  { intros. applys himpl_trans_r. { applys* wp_app_fix. } { applys* M. } }
  { applys wp_fix. }
Qed.
Lemma wpgen_seq_sound : ∀ F1 F2 t1 t2,
  formula_sound t1 F1 →
  formula_sound t2 F2 →
  formula_sound (trm_seq t1 t2) (wpgen_seq F1 F2).
Proof using.
  introv S1 S2. intros Q. unfolds wpgen_seq. applys himpl_trans wp_seq.
  applys himpl_trans S1. applys wp_conseq. intros v. applys S2.
Qed.
Lemma wpgen_let_sound : ∀ F1 F2of x t1 t2,
  formula_sound t1 F1 →
  (∀ v, formula_sound (subst x v t2) (F2of v)) →
  formula_sound (trm_let x t1 t2) (wpgen_let F1 F2of).
Proof using.
  introv S1 S2. intros Q. unfolds wpgen_let. applys himpl_trans wp_let.
  applys himpl_trans S1. applys wp_conseq. intros v. applys S2.
Qed.
Lemma wpgen_if_sound : ∀ F1 F2 t0 t1 t2,
  formula_sound t1 F1 →
  formula_sound t2 F2 →
  formula_sound (trm_if t0 t1 t2) (wpgen_if t0 F1 F2).
Proof using.
  introv S1 S2. intros Q. unfold wpgen_if. xpull. intros b →.
  applys himpl_trans wp_if. case_if. { applys S1. } { applys S2. }
Qed.
Lemma wpgen_app_sound : ∀ t,
  formula_sound t (wpgen_app t).
Proof using.
  intros t Q. unfold wpgen_app. xpull. intros H M. rewrite wp_equiv. apply M.
Qed.
The main inductive proof for the soundness theorem.
Lemma wpgen_sound : ∀ E t,
  formula_sound (isubst E t) (wpgen E t).
Proof using.
  intros. gen E. induction t; intros; simpl;
   try applys mkstruct_sound.
  { applys wpgen_val_sound. }
  { rename v into x. unfold wpgen_var. case_eq (lookup x E).
    { intros v EQ. applys wpgen_val_sound. }
    { intros N. applys wpgen_fail_sound. } }
  { applys wpgen_fun_sound.
    { intros vx. rewrite* <- isubst_rem. } }
  { applys* wpgen_fix_sound.
    { fold isubst. intros vf vx. rewrite* <- isubst_rem_2. } }
  { applys wpgen_app_sound. }
  { applys* wpgen_seq_sound. }
  { rename v into x. applys* wpgen_let_sound.
    { intros v. rewrite* <- isubst_rem. } }
  { applys* wpgen_if_sound. }
Qed.
Lemma himpl_wpgen_wp : ∀ t Q,
  wpgen nil t Q ==> wp t Q.
Proof using.
  introv M. lets N: (wpgen_sound nil t). rewrite isubst_nil in N. applys* N.
Qed.
The final theorem for closed terms.
Lemma triple_of_wpgen : ∀ t H Q,
  H ==> wpgen nil t Q →
  triple t H Q.
Proof using.
  introv M. rewrite <- wp_equiv. xchange M. applys himpl_wpgen_wp.
Qed.

Practical Proofs

This last section shows the techniques involved in setting up the lemmas and tactics required to carry out verification in practice, through concise proof scripts.

Lemmas for Tactics to Manipulate wpgen Formulae

Lemma xstruct_lemma : ∀ F H Q,
  H ==> F Q →
  H ==> mkstruct F Q.
Proof using. introv M. xchange M. applys mkstruct_erase. Qed.
Lemma xval_lemma : ∀ v H Q,
  H ==> Q v →
  H ==> wpgen_val v Q.
Proof using. introv M. applys M. Qed.
Lemma xlet_lemma : ∀ H F1 F2of Q,
  H ==> F1 (fun v ⇒ F2of v Q) →
  H ==> wpgen_let F1 F2of Q.
Proof using. introv M. xchange M. Qed.
Lemma xseq_lemma : ∀ H F1 F2 Q,
  H ==> F1 (fun v ⇒ F2 Q) →
  H ==> wpgen_seq F1 F2 Q.
Proof using. introv M. xchange M. Qed.
Lemma xif_lemma : ∀ b H F1 F2 Q,
  (b = true → H ==> F1 Q) →
  (b = false → H ==> F2 Q) →
  H ==> wpgen_if b F1 F2 Q.
Proof using. introv M1 M2. unfold wpgen_if. xsimpl* b. case_if*. Qed.
Lemma xapp_lemma : ∀ t Q1 H1 H Q,
  triple t H1 Q1 →
  H ==> H1 \* (Q1 \−−∗ protect Q) →
  H ==> wpgen_app t Q.
Proof using.
  introv M W. unfold wpgen_app. xsimpl.
  applys triple_ramified_frame M. applys W.
Qed.
Lemma xfun_spec_lemma : ∀ (S:val→Prop) H Q Fof,
  (∀ vf,
    (∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →
    S vf) →
  (∀ vf, S vf → (H ==> Q vf)) →
  H ==> wpgen_fun Fof Q.
Proof using.
  introv M1 M2. unfold wpgen_fun. xsimpl. intros vf N.
  applys M2. applys M1. introv K. rewrite <- wp_equiv. xchange K. applys N.
Qed.
Lemma xfun_nospec_lemma : ∀ H Q Fof,
  (∀ vf,
     (∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →
     (H ==> Q vf)) →
  H ==> wpgen_fun Fof Q.
Proof using.
  introv M. unfold wpgen_fun. xsimpl. intros vf N. applys M.
  introv K. rewrite <- wp_equiv. xchange K. applys N.
Qed.
Lemma xwp_lemma_fun : ∀ v1 v2 x t H Q,
  v1 = val_fun x t →
  H ==> wpgen ((x,v2)::nil) t Q →
  triple (trm_app v1 v2) H Q.
Proof using.
  introv M1 M2. rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound ((x,v2)::nil) t Q).
  rewrite <- subst_eq_isubst_one. applys* wp_app_fun.
Qed.
Lemma xwp_lemma_fix : ∀ v1 v2 f x t H Q,
  v1 = val_fix f x t →
  f ≠ x →
  H ==> wpgen ((f,v1)::(x,v2)::nil) t Q →
  triple (trm_app v1 v2) H Q.
Proof using.
  introv M1 N M2. rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound (((f,v1)::nil) ++ (x,v2)::nil) t Q).
  rewrite isubst_app. do 2 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fix.
Qed.
Lemma xtriple_lemma : ∀ t H (Q:val→hprop),
  H ==> mkstruct (wpgen_app t) Q →
  triple t H Q.
Proof using.
  introv M. rewrite <- wp_equiv. xchange M. unfold mkstruct, wpgen_app.
  xpull. intros Q' H' N. rewrite <- wp_equiv in N. xchange N.
  applys wp_ramified.
Qed.

Tactics to Manipulate wpgen Formulae

The tactic are presented in chapter WPgen.
Database of hints for xapp.
#[global] Hint Resolve triple_get triple_set triple_ref triple_free : triple.
#[global] Hint Resolve triple_add triple_div triple_neg triple_opp triple_eq
   triple_neq triple_sub triple_mul triple_mod triple_le triple_lt
   triple_ge triple_gt triple_ptr_add triple_ptr_add_nat : triple.
xstruct removes the leading mkstruct.
Tactic Notation "xstruct" :=
  applys xstruct_lemma.
xstruct_if_needed removes the leading mkstruct if there is one.
Tactic Notation "xstruct_if_needed" :=
  try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.
Tactic Notation "xval" :=
  xstruct_if_needed; applys xval_lemma.
Tactic Notation "xlet" :=
  xstruct_if_needed; applys xlet_lemma.
Tactic Notation "xseq" :=
  xstruct_if_needed; applys xseq_lemma.
Tactic Notation "xseq_xlet_if_needed" :=
  try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒
  match F with
  | wpgen_seq ?F1 ?F2 ⇒ xseq
  | wpgen_let ?F1 ?F2of ⇒ xlet
  end end.
Tactic Notation "xif" :=
  xseq_xlet_if_needed; xstruct_if_needed;
  applys xif_lemma; rew_bool_eq.
xapp_try_clear_unit_result implements some post-processing for cleaning up unused variables.
Tactic Notation "xapp_try_clear_unit_result" :=
  try match goal with ⊢ val → _ ⇒ intros _ end.
Tactic Notation "xtriple" :=
  intros; applys xtriple_lemma.
Tactic Notation "xtriple_if_needed" :=
  try match goal with ⊢ triple ?t ?H ?Q ⇒ applys xtriple_lemma end.
xapp_simpl performs the final step of the tactic xapp. It leverages xsimpl_no_cancel_wand tt which is a restricted version of xsimpl that does not attempt to cancel out magic wands.
Lemma xapp_simpl_lemma : ∀ F H Q,
  H ==> F Q →
  H ==> F Q \* (Q \−−∗ protect Q).
Proof using. introv M. xchange M. unfold protect. xsimpl. Qed.
Tactic Notation "xapp_simpl" :=
  first [ applys xapp_simpl_lemma (* handles specification coming from xfun *)
        | xsimpl_no_cancel_wand tt; unfold protect; xapp_try_clear_unit_result ].
Tactic Notation "xapp_pre" :=
  xtriple_if_needed; xseq_xlet_if_needed; xstruct_if_needed.
xapp_nosubst E implements the heart of xapp E. If the argument E was always a triple, it would suffice to run applys xapp_lemma E; xapp_simpl. Yet, E might be an specification involving quantifiers. These quantifiers need to be first instantiated. This instantiation is achieved by means of the tactic forwards_nounfold_then offered by the TLC library.
Tactic Notation "xapp_nosubst" constr(E) :=
  xapp_pre;
  forwards_nounfold_then E ltac:(fun K ⇒ applys xapp_lemma K; xapp_simpl).
xapp_apply_spec implements the heart of xapp, when called without argument. If finds out the specification triple, either in the hint data base named triple, or in the context by looking for an induction hypothesis. Disclaimer: as explained in chapter WPgen, the simple implementation of xapp_apply_spec which we use here does not apply when the specification includes premises that cannot be solved by eauto; it such cases, the tactic xapp E must be called, providing the specification E explicitly. This limitation is overcome using more involved Hint Extern tricks in CFML 2.0.
Tactic Notation "xapp_apply_spec" :=
  first [ solve [ eauto with triple ]
        | match goal with H: _ ⊢ _ ⇒ eapply H end ].
xapp_nosubst_for_records is place holder for implementing xapp on records. It is implemented further on.
Ltac xapp_nosubst_for_records tt :=
 fail.
xapp first calls xtriple if the goal is triple t H Q instead of H ==> wp t Q.
Tactic Notation "xapp_nosubst" :=
  xapp_pre;
  first [ applys xapp_lemma; [ xapp_apply_spec | xapp_simpl ]
        | xapp_nosubst_for_records tt ].
xapp_try_subst checks if the goal is of the form:
  • either ∀ (r:val), (r = ...) → ...
  • or ∀ (r:val), ∀ x, (r = ...) → ...
in which case it substitutes r away.
Tactic Notation "xapp_try_subst" :=
  try match goal with
  | ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →
  | ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒
      let y := fresh x in intros ? y ->; revert y
  end.
Tactic Notation "xapp" constr(E) :=
  xapp_nosubst E; xapp_try_subst.
Tactic Notation "xapp" :=
  xapp_nosubst; xapp_try_subst.
Tactic Notation "xapp_view" :=
  xseq_xlet_if_needed; xstruct_if_needed; applys xapp_lemma.
xapp is essentially equivalent to xapp_view; [ xapp_apply_spec | xapp_simpl ] .
Tactic Notation "xfun" constr(S) :=
  xseq_xlet_if_needed; xstruct_if_needed; applys xfun_spec_lemma S.
Tactic Notation "xfun" :=
  xseq_xlet_if_needed; xstruct_if_needed; applys xfun_nospec_lemma.
xvars may be called for unfolding "program variables as definitions", which take the form Vars.x, and revealing the underlying string.
Tactic Notation "xvars" :=
  DefinitionsForVariables.libsepvar_unfold.
xwp_simpl is a specialized version of simpl to be used for getting the function wp to compute properly.
Ltac xwp_simpl :=
  xvars;
  cbn beta delta [
     LibListExec.combine List.combine
     wpgen wpgen_var isubst lookup var_eq
     string_dec string_rec string_rect
     sumbool_rec sumbool_rect
     Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
     Bool.bool_dec bool_rec bool_rect ] iota zeta;
  simpl.
xwp evaluates wpgen for the term appearing in the goal. This implementation of xwp is for functions of arity one only, refined further on for arbitrary arities.
Tactic Notation "xwp_arity_one_only" :=
  intros;
  first [ applys xwp_lemma_fun; [ reflexivity | ]
        | applys xwp_lemma_fix; [ reflexivity | ] ];
  xwp_simpl.

Additional Tooling for xapp

xapp* is a convenient notation for xapp; auto_star. xapp* E is a convenient notation for xapp E; auto_star.
Tactic Notation "xapp" "*" :=
  xapp; auto_star.
Tactic Notation "xapp" "*" constr(E) :=
  xapp E; auto_star.
xapp_debug is a tactic to help debugging a call to xapp.
Tactic Notation "xapp_debug" :=
  let step msg := (idtac msg; match goal with ⊢ ?H ⇒ idtac H end) in
  xapp_pre;
  step "============= goal after [xapp_pre] ==============";
  first
  [ applys xapp_lemma;
     [ step "============= triple for [xapp_apply_spec] ==============";
       first [ xapp_apply_spec; fail 1
             | idtac "=====================================================";
               idtac "===> [xapp_apply_spec] failed!";
               idtac "===> [eauto with triple] could not solve find a specification";
               idtac "===> try [xapp_view. eapply myspec.] or [xapp myspec]. ";
               idtac "===> if side-conditions are not solved by [eauto], [xapp] won't work."]
     | idtac ]
  | applys xapp_lemma;
    [ xapp_apply_spec
    | step "============= entailment for [xapp_simpl] ==============";
       xapp_simpl ] ].

Notations for Triples and wpgen

Declare Scope wp_scope.
Notation for printing proof obligations arising from wpgen.
Notation "'PRE' H 'CODE' F 'POST' Q" :=
  (H ==> (mkstruct F) Q)
  (at level 8, H at level 0, F, Q at level 0,
   format "'[v' 'PRE' H '/' 'CODE' F '/' 'POST' Q ']'") : wp_scope.
Notation "` F" :=
  (mkstruct F)
  (at level 10,
   format "` F") : wp_scope.
Custom grammar for the display of characteristic formulae.
Declare Custom Entry wp.
Notation "<[ e ]>" :=
  e
  (at level 0, e custom wp at level 99) : wp_scope.
Notation "` F" :=
  (mkstruct F)
  (in custom wp at level 10,
   format "` F") : wp_scope.
Notation "( x )" :=
  x
  (in custom wp,
   x at level 99) : wp_scope.
Notation "{ x }" :=
  x
  (in custom wp at level 0,
   x constr,
   only parsing) : wp_scope.
Notation "x" :=
  x
  (in custom wp at level 0,
   x constr at level 0) : wp_scope.
Notation "'Fail'" :=
  ((wpgen_fail))
  (in custom wp at level 69) : wp_scope.
Notation "'Val' v" :=
  ((wpgen_val v))
  (in custom wp at level 69) : wp_scope.
Notation "'Let' x ':=' F1 'in' F2" :=
  ((wpgen_let F1 (fun x ⇒ F2)))
  (in custom wp at level 69,
   x name, (* NOTE: For compilation with Coq 8.12, replace "name" with "ident",
               here and in the next 3 occurrences in the rest of the section. *)
   F1 custom wp at level 99,
   F2 custom wp at level 99,
   right associativity,
  format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : wp_scope.
Notation "'Seq' F1 ; F2" :=
  ((wpgen_seq F1 F2))
  (in custom wp at level 68,
   F1 custom wp at level 99,
   F2 custom wp at level 99,
   right associativity,
   format "'[v' 'Seq' '[' F1 ']' ; '/' '[' F2 ']' ']'") : wp_scope.
Notation "'App' t0 t1 .. tn" :=
 ((wpgen_app (trm_app .. (trm_app t0 t1) .. tn)))
  (in custom wp at level 68,
   t0 constr at level 0,
   t1 constr at level 0,
   tn constr at level 0)
  : wp_scope.
Notation "'If_' v 'Then' F1 'Else' F2" :=
  ((wpgen_if v F1 F2))
  (in custom wp at level 69,
   F1 custom wp at level 99,
   F2 custom wp at level 99,
   left associativity,
   format "'[v' '[' 'If_' v 'Then' ']' '/' '[' F1 ']' '/' 'Else' '/' '[' F2 ']' ']'") : wp_scope.
Notation "'Fun' x '=>' F1" :=
  ((wpgen_fun (fun x ⇒ F1)))
  (in custom wp at level 69,
   x name,
   F1 custom wp at level 99,
   right associativity,
  format "'[v' '[' 'Fun' x '=>' F1 ']' ']'") : wp_scope.
Notation "'Fix' f x '=>' F1" :=
  ((wpgen_fix (fun f x ⇒ F1)))
  (in custom wp at level 69,
   f name, x name,
   F1 custom wp at level 99,
   right associativity,
   format "'[v' '[' 'Fix' f x '=>' F1 ']' ']'") : wp_scope.

Notation for Concrete Terms

The custom grammar for trm is defined in LibSepVar.
Declare Scope val_scope.
Terms
Notation "<{ e }>" :=
  e
  (at level 0, e custom trm at level 99) : trm_scope.
Notation "( x )" :=
  x
  (in custom trm, x at level 99) : trm_scope.
Notation "'begin' e 'end'" :=
  e
  (in custom trm, e custom trm at level 99, only parsing) : trm_scope.
Notation "{ x }" :=
  x
  (in custom trm, x constr) : trm_scope.
Notation "x" := x
  (in custom trm at level 0,
   x constr at level 0) : trm_scope.
Notation "t1 t2" := (trm_app t1 t2)
  (in custom trm at level 30,
   left associativity,
   only parsing) : trm_scope.
Notation "'if' t0 'then' t1 'else' t2" :=
  (trm_if t0 t1 t2)
  (in custom trm at level 69,
   t0 custom trm at level 99,
   t1 custom trm at level 99,
   t2 custom trm at level 99,
   left associativity,
   format "'[v' '[' 'if' t0 'then' ']' '/' '[' t1 ']' '/' 'else' '/' '[' t2 ']' ']'") : trm_scope.
Notation "'if' t0 'then' t1 'end'" :=
  (trm_if t0 t1 (trm_val val_unit))
  (in custom trm at level 69,
   t0 custom trm at level 99, (* at level 0 ? *)
   t1 custom trm at level 99,
   left associativity,
   format "'[v' '[' 'if' t0 'then' ']' '/' '[' t1 ']' '/' 'end' ']'") : trm_scope.
Notation "t1 ';' t2" :=
  (trm_seq t1 t2)
  (in custom trm at level 68,
   t2 custom trm at level 99,
   right associativity,
   format "'[v' '[' t1 ']' ';' '/' '[' t2 ']' ']'") : trm_scope.
Notation "'let' x '=' t1 'in' t2" :=
  (trm_let x t1 t2)
  (in custom trm at level 69,
   x at level 0,
   t1 custom trm at level 99,
   t2 custom trm at level 99,
   right associativity,
   format "'[v' '[' 'let' x '=' t1 'in' ']' '/' '[' t2 ']' ']'") : trm_scope.
(* Let-functions *)
Notation "'let' f x1 '=' t1 'in' t2" :=
  (trm_let f (trm_fun x1 t1) t2)
  (in custom trm at level 69,
   t1 custom trm,
   t2 custom trm,
   f, x1 at level 0,
   format "'let' f x1 '=' t1 'in' t2") : val_scope.
Notation "'let' f x1 .. xn '=' t1 'in' t2" :=
  (trm_let f (trm_fun x1 .. (trm_fun xn t1) ..) t2)
  (in custom trm at level 69,
   t1 custom trm,
   t2 custom trm,
   f, x1, xn at level 0,
   format "'let' f x1 .. xn '=' t1 'in' t2") : val_scope.
Notation "'let' 'rec' f x1 '=' t1 'in' t2" :=
  (trm_let f (trm_fix f x1 t1) t2)
  (in custom trm at level 69,
   t1 custom trm,
   t2 custom trm,
   f, x1 at level 0,
   format "'let' 'rec' f x1 '=' t1 'in' t2") : val_scope.
Notation "'let' 'rec' f x1 x2 .. xn '=' t1 'in' t2" :=
  (trm_let f (trm_fix f x1 (trm_fun x2 .. (trm_fun xn t1) ..)) t2)
  (in custom trm at level 69,
   t1 custom trm,
   t2 custom trm,
   f, x1, x2, xn at level 0,
   format "'let' 'rec' f x1 x2 .. xn '=' t1 'in' t2") : val_scope.
(* On-the-fly functions, as values *)
Notation "'fun' x1 '=>' t" :=
  (val_fun x1 t)
  (in custom trm at level 69,
   x1 at level 0,
   t custom trm at level 99,
   format "'fun' x1 '=>' t") : val_scope.
Notation "'fun' x1 x2 .. xn '=>' t" :=
  (val_fun x1 (trm_fun x2 .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   x1, x2, xn at level 0,
   format "'fun' x1 x2 .. xn '=>' t") : val_scope.
Notation "'fix' f x1 '=>' t" :=
  (val_fix f x1 t)
  (in custom trm at level 69,
   f, x1 at level 0,
   t custom trm at level 99,
   format "'fix' f x1 '=>' t") : val_scope.
Notation "'fix' f x1 x2 .. xn '=>' t" :=
  (val_fix f x1 (trm_fun x2 .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   f, x1, x2, xn at level 0,
   format "'fix' f x1 x2 .. xn '=>' t") : val_scope.
(* On-the-fly functions, as terms *)
Notation "'fun_' x1 '=>' t" :=
  (trm_fun x1 t)
  (in custom trm at level 69,
   x1 at level 0,
   t custom trm at level 99,
   format "'fun_' x1 '=>' t") : trm_scope.
Notation "'fun_' x1 .. xn '=>' t" :=
  (trm_fun x1 .. (trm_fun xn t) ..)
  (in custom trm at level 69,
   t custom trm,
   x1, xn at level 0,
   format "'fun_' x1 .. xn '=>' t") : trm_scope.
Notation "'fix_' f x1 '=>' t" :=
  (trm_fix f x1 t)
  (in custom trm at level 69,
   f, x1 at level 0,
   t custom trm at level 99,
   format "'fix_' f x1 '=>' t") : trm_scope.
Notation "'fix_' f x1 x2 .. xn '=>' t" :=
  (trm_fix f x1 (trm_fun x2 .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   f, x1, x2, xn at level 0,
   format "'fix_' f x1 x2 .. xn '=>' t") : trm_scope.
Notation "()" :=
  (trm_val val_unit)
  (in custom trm at level 0) : trm_scope.
Notation "()" :=
  (val_unit)
  (at level 0) : val_scope.
Notation for Primitive Operations.
Notation "'ref'" :=
  (trm_val (val_prim val_ref))
  (in custom trm at level 0, only parsing) : trm_scope.
Notation "'free'" :=
  (trm_val (val_prim val_free))
  (in custom trm at level 0, only parsing) : trm_scope.
Notation "'not'" :=
  (trm_val (val_prim val_neg))
  (in custom trm at level 0, only parsing) : trm_scope.
Notation "! t" :=
  (val_get t)
  (in custom trm at level 67,
   t custom trm at level 99) : trm_scope.
Notation "t1 := t2" :=
  (val_set t1 t2)
  (in custom trm at level 67) : trm_scope.
Notation "t1 + t2" :=
  (val_add t1 t2)
  (in custom trm at level 58) : trm_scope.
Notation "'- t" :=
  (val_opp t)
  (in custom trm at level 57,
   t custom trm at level 99) : trm_scope.
Notation "t1 - t2" :=
  (val_sub t1 t2)
  (in custom trm at level 58) : trm_scope.
Notation "t1 * t2" :=
  (val_mul t1 t2)
  (in custom trm at level 57) : trm_scope.
Notation "t1 / t2" :=
  (val_div t1 t2)
  (in custom trm at level 57) : trm_scope.
Notation "t1 'mod' t2" :=
  (val_mod t1 t2)
  (in custom trm at level 57) : trm_scope.
Notation "t1 = t2" :=
  (val_eq t1 t2)
  (in custom trm at level 58) : trm_scope.
Notation "t1 <> t2" :=
  (val_neq t1 t2)
  (in custom trm at level 58) : trm_scope.
Notation "t1 <= t2" :=
  (val_le t1 t2)
  (in custom trm at level 60) : trm_scope.
Notation "t1 < t2" :=
  (val_lt t1 t2)
  (in custom trm at level 60) : trm_scope.
Notation "t1 >= t2" :=
  (val_ge t1 t2)
  (in custom trm at level 60) : trm_scope.
Notation "t1 > t2" :=
  (val_gt t1 t2)
  (in custom trm at level 60) : trm_scope.
(* TESTING
Module TestingNotation.
Local Open Scope val_scope.
Local Open Scope trm_scope.

Definition test_app1 t1 t2 : trm :=
  <{ t1 t2 }>.

Definition test_app2 t1 t2 t3 : trm :=
  <{ t1 t2 t3 }>.

Definition test_fun1 x1 t : val :=
  <{ fun x1 => t }>.

Definition test_fun2 x1 x2 t : val :=
  <{ fun x1 x2 => t }>.

Definition test_fun3 x1 x2 x3 t : val :=
  <{ fun x1 x2 x3 => t }>.

Definition test_fix1 f x1 t : val :=
  <{ fun f x1 => t }>.

Definition test_fix2 f x1 x2 t : val :=
  <{ fun f x1 x2 => t }>.

Definition test_fix3 f x1 x2 x3 t : val :=
  <{ fun f x1 x2 x3 => t }>.

Definition test_trmfun_1 f x1 : trm :=
  <{ fun_ f x1 => x1 }>.

Definition test_trmfun_2 f x1 x2 : trm :=
  <{ fun_ f x1 x2 => x1 }>.

Definition test_trmfun_3 f x1 x2 x3 : trm :=
  <{ fun_ f x1 x2 x3 => x1 }>.

Definition test_trmfix1 f x1 t : trm :=
  <{ fix_ f x1 => t }>.

Definition test_trmfix2 f x1 x2 t : trm :=
  <{ fix_ f x1 x2 => t }>.

Definition test_trmfix3 f x1 x2 x3 t : trm :=
  <{ fix_ f x1 x2 x3 => t }>.

Definition test_letfun_1 f x1 t : trm :=
  <{ let f x1 = x1 in t }>.

Definition test_letfun_2 f x1 x2 t : trm :=
  <{ let f x1 x2 = x1 in t }>.

Definition test_letfun_3 f x1 x2 x3 t : trm :=
  <{ let f x1 x2 x3 = x1 in t }>.

Definition test_letfix_1 f x1 t : trm :=
  <{ let rec f x1 = x1 in t }>.

Definition test_letfix_2 f x1 x2 t : trm :=
  <{ let rec f x1 x2 = x1 in t }>.

Definition test_letfix_3 f x1 x2 x3 t : trm :=
  <{ let rec f x1 x2 x3 = x1 in t }>.

Print test_app1.
Print test_app2.
Print test_trmfix3.
Print test_fun3.

End TestingNotation.
*)

Scopes, Coercions and Notations for Concrete Programs

Module ProgramSyntax.
Export NotationForVariables.
Module Vars := DefinitionsForVariables.
Close Scope fmap_scope.
Open Scope string_scope.
Open Scope val_scope.
Open Scope trm_scope.
Open Scope wp_scope.
Coercion string_to_var (x:string) : var := x.
End ProgramSyntax.

Additional Separation Logic Operators

Disjunction: Definition and Properties of hor

Definition hor (H1 H2 : hprop) : hprop :=
  \∃ (b:bool), if b then H1 else H2.
Lemma hor_sym : ∀ H1 H2,
  hor H1 H2 = hor H2 H1.
Proof using.
  intros. unfold hor. applys himpl_antisym.
  { applys himpl_hexists_l. intros b.
    applys himpl_hexists_r (neg b). destruct* b. }
  { applys himpl_hexists_l. intros b.
    applys himpl_hexists_r (neg b). destruct* b. }
Qed.
Lemma himpl_hor_r_l : ∀ H1 H2,
  H1 ==> hor H1 H2.
Proof using. intros. unfolds hor. ∃* true. Qed.
Lemma himpl_hor_r_r : ∀ H1 H2,
  H2 ==> hor H1 H2.
Proof using. intros. unfolds hor. ∃* false. Qed.
Lemma himpl_hor_l : ∀ H1 H2 H3,
  H1 ==> H3 →
  H2 ==> H3 →
  hor H1 H2 ==> H3.
Proof using.
  introv M1 M2. unfolds hor. applys himpl_hexists_l. intros b. case_if*.
Qed.
Lemma triple_hor : ∀ t H1 H2 Q,
  triple t H1 Q →
  triple t H2 Q →
  triple t (hor H1 H2) Q.
Proof using.
  introv M1 M2. unfold hor. applys triple_hexists.
  intros b. destruct* b.
Qed.

Conjunction: Definition and Properties of hand

Definition hand (H1 H2 : hprop) : hprop :=
  \∀ (b:bool), if b then H1 else H2.
Lemma hand_sym : ∀ H1 H2,
  hand H1 H2 = hand H2 H1.
Proof using.
  intros. unfold hand. applys himpl_antisym.
  { applys himpl_hforall_r. intros b.
    applys himpl_hforall_l (neg b). destruct* b. }
  { applys himpl_hforall_r. intros b.
    applys himpl_hforall_l (neg b). destruct* b. }
Qed.
Lemma himpl_hand_l_r : ∀ H1 H2,
  hand H1 H2 ==> H1.
Proof using. intros. unfolds hand. applys* himpl_hforall_l true. Qed.
Lemma himpl_hand_l_l : ∀ H1 H2,
  hand H1 H2 ==> H2.
Proof using. intros. unfolds hand. applys* himpl_hforall_l false. Qed.
Lemma himpl_hand_r : ∀ H1 H2 H3,
  H1 ==> H2 →
  H1 ==> H3 →
  H1 ==> hand H2 H3.
Proof using.
  introv M1 M2. unfold hand. applys himpl_hforall_r. intros b. case_if*.
Qed.
Lemma triple_hand_l : ∀ t H1 H2 Q,
  triple t H1 Q →
  triple t (hand H1 H2) Q.
Proof using. introv M1. unfold hand. applys¬triple_hforall true. Qed.
Lemma triple_hand_r : ∀ t H1 H2 Q,
  triple t H2 Q →
  triple t (hand H1 H2) Q.
Proof using. introv M1. unfold hand. applys¬triple_hforall false. Qed.

Generalization to N-ary Functions

Smart Constructors for N-ary Functions and Applications

Definition vars : Type := list var.
Definition vals : Type := list val.
Definition trms : Type := list trm.
trm_apps f ts builds the application of the function f to the list of terms ts.
Fixpoint trm_apps (f:trm) (ts:trms) : trm :=
  match ts with
  | nil ⇒ f
  | ti::ts' ⇒ trm_apps (trm_app f ti) ts'
  end.
trm_funs xs t builds a term describing a function that expects arguments with names xs, and that has t for body.
Fixpoint trm_funs (xs:vars) (t:trm) : trm :=
  match xs with
  | nil ⇒ t
  | x1::xs' ⇒ trm_fun x1 (trm_funs xs' t)
  end.
val_funs xs t is similar to trm_funs xs t but produces a value.
Definition val_funs (xs:vars) (t:trm) : val :=
  match xs with
  | nil ⇒ arbitrary
  | x1::xs' ⇒ val_fun x1 (trm_funs xs' t)
  end.
trm_fixs f xs t builds a term describing a recursive function named f that expects arguments with names xs, and that has t for body.
Definition trm_fixs (f:var) (xs:vars) (t:trm) : trm :=
  match xs with
  | nil ⇒ arbitrary
  | x1::xs' ⇒ trm_fix f x1 (trm_funs xs' t)
  end.
val_fixs xs t is similar to trm_fixs xs t but produces a value.
Definition val_fixs (f:var) (xs:vars) (t:trm) : val :=
  match xs with
  | nil ⇒ arbitrary
  | x1::xs' ⇒ val_fix f x1 (trm_funs xs' t)
  end.
var_funs xs n asserts that xs is a nonempty list made of n distinct variable names.
Definition var_funs (xs:vars) (n:nat) : Prop :=
     LibList.noduplicates xs
  ∧ length xs = n
  ∧ xs ≠ nil.
trms_vals vs converts a list of values vs into a list of terms made of the corresponding values, each converted using trm_val.
Coercion trms_vals (vs:vals) : trms :=
  LibList.map trm_val vs.
Lemma trms_vals_nil :
  trms_vals nil = nil.
Proof using. auto. Qed.
Lemma trms_vals_cons : ∀ v vs,
  trms_vals (v :: vs) = trm_val v :: trms_vals vs.
Proof using. intros. unfold trms_vals. rew_listx*. Qed.
#[local] Hint Rewrite trms_vals_nil trms_vals_cons : rew_listx.

Evaluation Rules for N-ary Constructs

subst_trm_funs distributes subst over trm_funs.
Lemma subst_trm_funs : ∀ xs x v t1,
  ¬ mem x xs →
  subst x v (trm_funs xs t1) = trm_funs xs (subst x v t1).
Proof using.
  intros xs. induction xs as [|x xs']; introv N.
  { auto. }
  { rew_listx in N. rew_logic in N. destruct N. simpl. case_var. fequals*. }
Qed.
Evaluation rule for reducing trm_funs into val_funs
Lemma eval_like_trm_funs : ∀ xs t1,
  xs ≠ nil →
  eval_like (val_funs xs t1) (trm_funs xs t1).
Proof using.
  introv N M. destruct xs; tryfalse. simpls. inverts M. applys* eval_fun.
Qed.
Auxiliary lemma: evaluation rule for reducing the first argument of a val_funs applied to an argument.
Lemma eval_like_app_val_funs_cons : ∀ x xs t1 t0 v,
  eval_like (val_funs (x :: xs) t1) t0 →
  ¬ mem x xs →
  xs ≠ nil →
  eval_like (val_funs xs (subst x v t1)) (t0 v).
Proof using.
  introv R Nx Hx M. unfolds eval_like. applys eval_app_arg1'.
  { applys R. applys eval_val_minimal. }
  { simpl. intros ? ? (->&->). applys* eval_app_fun.
    rewrite* subst_trm_funs. applys* eval_like_trm_funs. }
Qed.
Auxiliary lemma: evaluation rule for reducing a val_funs applied to its last argument.
Lemma eval_like_app_val_funs_one : ∀ x t1 t0 v,
  eval_like ((val_funs (x::nil) t1)) t0 →
  eval_like (subst x v t1) (trm_app t0 v).
Proof using.
  introv R N. applys eval_app_arg1'.
  { applys R. applys eval_val_minimal. }
  { simpl. intros ? ? (->&->). applys* eval_app_fun. }
Qed.
Evaluation rule for the application of a val_funs with n variables to a list of n values.
Lemma eval_like_trm_apps_funs : ∀ xs t0 vs t1,
  eval_like (val_funs xs t1) t0 →
  var_funs xs (length vs) →
  eval_like (isubst (combine xs vs) t1) (trm_apps t0 (trms_vals vs)).
Proof using.
  introv E (R1&R2&R3). gen t1 t0 vs. induction xs; intros.
  { false*. }
  { inverts R1. destruct vs as [|v vs]; rew_list in *; tryfalse.
    rew_listx. rewrite isubst_cons. simpl.
    tests: (xs = nil).
    { destruct vs as [|]; tryfalse.
      rew_listx. rewrite isubst_nil. simpl.
      applys* eval_like_app_val_funs_one. }
    { applys* IHxs. applys* eval_like_app_val_funs_cons. } }
Qed.
Evaluation rule for application of a recursive n-ary function of the form val_fix f (trm_funs xs t1) to a list of values of the appropriate length.
Lemma eval_like_trm_apps_fixs : ∀ f xs vs t1 v0,
  v0 = val_fixs f xs t1 →
  var_funs xs (length vs) →
  ¬ mem f xs →
  xs ≠ nil →
  eval_like (isubst (combine (f::xs) (v0::vs)) t1) (trm_apps v0 (trms_vals vs)).
Proof using.
  introv E F N1 N2. rew_listx. rewrite isubst_cons.
  destruct F as (F1&F2&F3).
  destruct xs as [|x xs']; tryfalse.
  destruct vs as [|v vs']; tryfalse.
  tests C: (xs' = nil).
  { destruct vs' as [|]; tryfalse.
    rew_listx. rewrite isubst_cons, isubst_nil. simpl.
    introv M. applys* eval_app_fix. }
  { rew_listx. rewrite isubst_cons. simpl. rew_listx in N1.
    rew_logic in N1. destruct N1 as (Nf&N1). inverts F1 as (Fx&F1).
    applys eval_like_trm_apps_funs.
    { introv M. applys* eval_app_fix.
      inverts M. rewrite* subst_trm_funs. rewrite* subst_trm_funs.
      applys* eval_like_trm_funs. applys* eval_val. }
    { rew_list in F2. splits*. } }
Qed.

Tooling for N-ary Functions and Applications

var_funs_exec xs n is a computable version of var_funs xs n.
Section Var_funs_exec.
Import LibListExec.RewListExec.
Definition var_funs_exec (xs:vars) (n:nat) : bool :=
     LibListExec.noduplicates var_eq xs
  && (LibNat.beq (LibListExec.length xs) n
  && LibListExec.is_not_nil xs).
Lemma var_funs_exec_eq : ∀ xs (n:nat),
  var_funs_exec xs n = isTrue (var_funs xs n).
Proof using.
  intros. hint var_eq_spec.
  unfold var_funs_exec, var_funs.
  rewrite LibNat.beq_eq. rew_list_exec; auto.
  extens; rew_istrue. splits*.
Qed.
End Var_funs_exec.
trms_to_vals is the reciprocal of trms_vals, in the sense that trms_to_vals ts = Some vs ensurse that ts = trms_vals vs.
Fixpoint trms_to_vals (ts:trms) : option vals :=
  match ts with
  | nil ⇒ Some nil
  | (trm_val v)::ts' ⇒
      match trms_to_vals ts' with
      | None ⇒ None
      | Some vs' ⇒ Some (v::vs')
      end
  | _ ⇒ None
  end.
Lemma trms_to_vals_spec : ∀ ts vs,
  trms_to_vals ts = Some vs →
  ts = trms_vals vs.
Proof using.
  intros ts. induction ts as [|t ts']; simpl; introv E.
  { inverts E. auto. }
  { destruct t; inverts E as E. cases (trms_to_vals ts') as C; inverts E.
    rename v0 into vs'. rewrite* (IHts' vs'). }
Qed.
trm_apps_of_trm t is a tactic that takes a term t and returns a corresponding term in the form trm_apps f ts, assuming it is possible.
Ltac trm_apps_of_trm t :=
  let rec aux acc t :=
    match t with
    | trm_app ?t0 ?t1 ⇒
        let acc' := constr:(t1::acc) in
        aux acc' t0
    | _ ⇒ constr:(trm_apps t acc)
    end in
  aux (@nil trm) t.
Lemma trm_apps_of_trm_demo : ∀ (f x1 x2 x3:trm) H Q,
  triple (f x1 x2 x3) H Q.
Proof using.
  intros.
  match goal with ⊢ triple ?t _ _ ⇒
    let r := trm_apps_of_trm t in
    change t with r end.
Abort.
prove_eq_trm_apps applies to a goal of the form t = trm_apps ?f ?vs, and solve it by instantiating f and vs, assuming it is possible.
Ltac prove_eq_trm_apps :=
  match goal with ⊢ ?t = trm_apps _ _ ⇒
    let r := trm_apps_of_trm t in
    apply (refl_equal r) end.
Lemma prove_eq_trm_apps_demo : ∀ (f x1 x2 x3:trm),
  (∀ t ts, f x1 x2 x3 = trm_apps t ts → (t,ts) = (t,ts) → True) →
  True.
Proof using. intros. eapply H. prove_eq_trm_apps. Abort.
trm_funs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form trm_funs xs t1, assuming it is possible.
Ltac trm_funs_of_trm t :=
  let rec aux t :=
    match t with
    | trm_fun ?x ?t1 ⇒
        match aux t1 with
        | trm_funs ?xs ?t0 ⇒ constr:(trm_funs (x::xs) t0)
        | ?t0 ⇒ constr:(trm_funs (x::nil) t0)
        end
    | _ ⇒ constr:(t)
    end in
  let t := eval hnf in t in
  aux t.
val_funs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form val_funs xs t1, assuming it is possible.
Ltac val_funs_of_trm t :=
  let t := eval hnf in t in
  match t with
  | val_fun ?x ?t1 ⇒
      match trm_funs_of_trm t1 with
      | trm_funs ?xs ?t0 ⇒ constr:(val_funs (x::xs) t0)
      | ?t0 ⇒ constr:(val_funs (x::nil) t0)
      end
  | _ ⇒ constr:(t)
  end.
prove_eq_val_funs applies to a goal of the form v = val_funs ?xs ?t1 and solves it is possible by instantiating xs and t1
Ltac prove_eq_val_funs :=
  match goal with ⊢ ?t = val_funs _ _ ⇒
    let r := val_funs_of_trm t in
    apply (refl_equal r) end.
Lemma prove_eq_val_funs_demo : ∀ (x1 x2:var) (t0:trm),
  (∀ xs t, val_fun x1 (trm_fun x2 t0) = val_funs xs t → (xs,t) = (xs,t) → True) →
  True.
Proof using. intros. eapply H. prove_eq_val_funs. Abort.
val_fixs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form val_fixs xs t1, if possible.
Ltac val_fixs_of_trm t :=
  let t := eval hnf in t in
  match t with
  | val_fix ?f ?x ?t1 ⇒
      match trm_funs_of_trm t1 with
      | trm_funs ?xs ?t0 ⇒ constr:(val_fixs f (x::xs) t0)
      | _ ⇒ constr:(val_fixs f (x::nil) t1)
      end
  | _ ⇒ constr:(t)
  end.
prove_eq_val_fix_trm_funs applies to a goal of the form v = val_fix ?f (trm_funs ?xs ?t1) and solves it is possible.
Ltac prove_eq_val_fix_trm_funs :=
  match goal with ⊢ ?t = val_fixs _ _ _ ⇒
    let r := val_fixs_of_trm t in
    apply (refl_equal r) end.
Lemma prove_eq_val_fix_trm_funs_demo : ∀ (x1 x2:var) (t0:trm),
  (∀ f xs t, val_fix f x1 (trm_fun x2 t0) = val_fixs f xs t → (f,xs,t) = (f,xs,t) → True) →
  True.
Proof using. intros. eapply H. prove_eq_val_fix_trm_funs. Abort.

Implementation of the Tactic xwp

Lemma xwp_lemma_funs : ∀ t v0 ts vs xs t1 H Q,
  t = trm_apps v0 ts →
  v0 = val_funs xs t1 →
  trms_to_vals ts = Some vs →
  var_funs_exec xs (LibList.length vs) →
  H ==> (wpgen (LibListExec.combine xs vs) t1) Q →
  triple t H Q.
Proof using.
  introv → E M1 F M2. rewrite var_funs_exec_eq in F. rew_bool_eq in F.
  lets HL: (proj32 F). rewrite* LibListExec.combine_eq in M2.
  lets ->: trms_to_vals_spec (rm M1).
  rewrite <- wp_equiv. xchange (rm M2). xchange wpgen_sound.
  applys wp_eval_like. applys* eval_like_trm_apps_funs.
  { subst. introv M. applys M. }
Qed.
Lemma xwp_lemma_fixs : ∀ t v0 ts vs f xs t1 H Q,
  t = trm_apps v0 ts →
  v0 = val_fixs f xs t1 →
  trms_to_vals ts = Some vs →
  var_funs_exec xs (LibList.length vs) →
  negb (LibListExec.mem var_eq f xs) →
  H ==> (wpgen (LibListExec.combine (f::xs) (v0::vs)) t1) Q →
  triple t H Q.
Proof using.
  introv → E M1 F N1 M2. rewrite var_funs_exec_eq in F. rew_bool_eq in F.
  lets HL: (proj32 F). rewrite* LibListExec.combine_eq in M2; [|rew_list*].
  lets Nxs: (proj33 F). lets ->: trms_to_vals_spec (rm M1).
  rewrite LibListExec.mem_eq in N1; [| applys var_eq_spec ]. rew_bool_eq in N1.
  rewrite <- wp_equiv. xchange (rm M2). xchange wpgen_sound.
  applys wp_eval_like. applys* eval_like_trm_apps_fixs.
Qed.
Tactic Notation "xwp" :=
  intros;
  first [ applys xwp_lemma_funs;
          [ prove_eq_trm_apps
          | prove_eq_val_funs
          | reflexivity
          | try reflexivity
          | ]
        | applys xwp_lemma_fixs;
          [ prove_eq_trm_apps
          | prove_eq_val_fix_trm_funs
          | reflexivity
          | try reflexivity
          | try reflexivity
          | ]
        | fail 1 "xwp only applies to functions defined using [val_fun] or [val_fix], with at most 3 arguments" ];
  xwp_simpl.

Specification of Array Operations

See chapter Array.

Specification of Record Operations

The chapter Struct shows how to these specifications may be realized.
Implicit Types k : nat.

Representation of Records

A field name is implemented as a natural number
Definition field : Type := nat.
A record field is described as the pair of a field and a value stored in that field.
Definition hrecord_field : Type := (field * val).
A record consists of a list of fields.
Definition hrecord_fields : Type := list hrecord_field.
Implicit Types kvs : hrecord_fields.
Record fields syntax, e.g., `{ head := x; tail := q }.
Notation "`{ k1 := v1 }" :=
  ((k1,(v1:val))::nil)
  (at level 0, k1 at level 0, only parsing)
  : val_scope.
Notation "`{ k1 := v1 ; k2 := v2 }" :=
  ((k1,(v1:val))::(k2,(v2:val))::nil)
  (at level 0, k1, k2 at level 0, only parsing)
  : val_scope.
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
  ((k1,(v1:val))::(k2,(v2:val))::(k3,(v3:val))::nil)
  (at level 0, k1, k2, k3 at level 0, only parsing)
  : val_scope.
Notation "`{ k1 := v1 }" :=
  ((k1,v1)::nil)
  (at level 0, k1 at level 0, only printing)
  : val_scope.
Notation "`{ k1 := v1 ; k2 := v2 }" :=
  ((k1,v1)::(k2,v2)::nil)
  (at level 0, k1, k2 at level 0, only printing)
  : val_scope.
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
  ((k1,v1)::(k2,v2)::(k3,v3)::nil)
  (at level 0, k1, k2, k3 at level 0, only printing)
  : val_scope.
Open Scope val_scope.
hrecord kvs p, written p ~~~> kvs, describes a record at location p, with fields described by the list kvs.
Parameter hrecord : ∀ (kvs:hrecord_fields) (p:loc), hprop.
Notation "p '~~~>' kvs" := (hrecord kvs p)
  (at level 32) : hprop_scope.
The heap predicate hrecord kvs p captures in particular the invariant that the location p is not null.
Parameter hrecord_not_null : ∀ p kvs,
  hrecord kvs p ==> hrecord kvs p \* \[p ≠ null].

Read Operation on Record Fields

val_get_field k p, written p'.k, reads field k from the record at location p.
Parameter val_get_field : field → val.
Notation "t1 '`.' k" :=
  (val_get_field k t1)
  (in custom trm at level 56, k at level 0, format "t1 '`.' k" ) : trm_scope.
Generator of specifications of val_get_field.
Fixpoint hfields_lookup (k:field) (kvs:hrecord_fields) : option val :=
  match kvs with
  | nil ⇒ None
  | (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
                       then Some vi
                       else hfields_lookup k kvs'
  end.
Specification of val_get_field in terms of hrecord.
Parameter triple_get_field_hrecord : ∀ kvs p k v,
  hfields_lookup k kvs = Some v →
  triple (val_get_field k p)
    (hrecord kvs p)
    (fun r ⇒ \[r = v] \* hrecord kvs p).

Write Operation on Record Fields

val_set_field k p v, written Set p'.k ':= v, update the contents of the field k from the record at location p, with the value v.
Parameter val_set_field : field → val.
Notation "t1 '`.' k ':=' t2" :=
  (val_set_field k t1 t2)
  (in custom trm at level 56,
   k at level 0, format "t1 '`.' k ':=' t2")
   : trm_scope.
Generator of specifications for val_set_field.
Fixpoint hfields_update (k:field) (v:val) (kvs:hrecord_fields)
                        : option hrecord_fields :=
  match kvs with
  | nil ⇒ None
  | (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
                   then Some ((k,v)::kvs')
                   else match hfields_update k v kvs' with
                        | None ⇒ None
                        | Some LR ⇒ Some ((ki,vi)::LR)
                        end
  end.
Specification of val_set_field in terms of hrecord.
Parameter triple_set_field_hrecord : ∀ kvs kvs' k p v,
  hfields_update k v kvs = Some kvs' →
  triple (val_set_field k p v)
    (hrecord kvs p)
    (fun _ ⇒ hrecord kvs' p).

Allocation of Records

val_alloc_hrecord ks allocates a record with fields ks, storing uninitialized contents.
Parameter val_alloc_hrecord : ∀ (ks:list field), trm.
Parameter triple_alloc_hrecord : ∀ ks,
  ks = nat_seq 0 (LibListExec.length ks) →
  triple (val_alloc_hrecord ks)
    \[]
    (funloc p ⇒ hrecord (LibListExec.map (fun k ⇒ (k,val_uninit)) ks) p).
An arity-generic version of the definition of allocation combined with initialization is beyond the scope of this course. We only include constructors for arity 2 and 3.
val_new_record_2 k1 k2 v1 v2, written `{ k1 := v1 ; k2 := v2 }, allocates a record with two fields and initialize the fields.
Parameter val_new_hrecord_2 : ∀ (k1:field) (k2:field), val.
Notation "`{ k1 := v1 ; k2 := v2 }" :=
  (val_new_hrecord_2 k1 k2 v1 v2)
  (in custom trm at level 65,
   k1, k2 at level 0,
   v1, v2 at level 65) : trm_scope.
Open Scope trm_scope.
Parameter triple_new_hrecord_2 : ∀ k1 k2 v1 v2,
  k1 = 0%nat →
  k2 = 1%nat →
  triple <{ `{ k1 := v1; k2 := v2 } }>
    \[]
    (funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 }).
#[global] Hint Resolve val_new_hrecord_2 : triple.
val_new_record_3 k1 k2 k3 v1 v2 v3, written `{ k1 := v1 ; k2 := v2 ; k3 := v3 }, allocates a record with three fields and initialize the fields.
Parameter val_new_hrecord_3 : ∀ (k1:field) (k2:field) (k3:field), val.
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
  (val_new_hrecord_3 k1 k2 k3 v1 v2 v3)
  (in custom trm at level 65,
   k1, k2, k3 at level 0,
   v1, v2, v3 at level 65) : trm_scope.
Parameter triple_new_hrecord_3 : ∀ k1 k2 k3 v1 v2 v3,
  k1 = 0%nat →
  k2 = 1%nat →
  k3 = 2%nat →
  triple <{ `{ k1 := v1; k2 := v2; k3 := v3 } }>
    \[]
    (funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 ; k3 := v3 }).
#[global] Hint Resolve val_new_hrecord_3 : triple.

Deallocation of Records

val_dealloc_hrecord p, written delete p, deallocates the record at location p.
Parameter val_dealloc_hrecord : val.
Notation "'delete'" :=
  (trm_val val_dealloc_hrecord)
  (in custom trm at level 0) : trm_scope.
Parameter triple_dealloc_hrecord : ∀ kvs p,
  triple (val_dealloc_hrecord p)
    (hrecord kvs p)
    (fun _ ⇒ \[]).
#[global] Hint Resolve triple_dealloc_hrecord : triple.

Extending xapp to Support Record Access Operations

The tactic xapp is refined to automatically invoke the lemmas triple_get_field_hrecord and triple_set_field_hrecord.
Parameter xapp_get_field_lemma : ∀ H k p Q,
  H ==> \∃ kvs, (hrecord kvs p) \*
     match hfields_lookup k kvs with
     | None ⇒ \[False]
     | Some v ⇒ ((fun r ⇒ \[r = v] \* hrecord kvs p) \−−∗ protect Q) end →
  H ==> wpgen_app (val_get_field k p) Q.
Parameter xapp_set_field_lemma : ∀ H k p v Q,
  H ==> \∃ kvs, (hrecord kvs p) \*
     match hfields_update k v kvs with
     | None ⇒ \[False]
     | Some kvs' ⇒ ((fun _ ⇒ hrecord kvs' p) \−−∗ protect Q) end →
  H ==> wpgen_app (val_set_field k p v) Q.
Ltac xapp_nosubst_for_records tt ::=
  first [ applys xapp_set_field_lemma; xsimpl; simpl; xapp_simpl
        | applys xapp_get_field_lemma; xsimpl; simpl; xapp_simpl ].

Extending xsimpl to Simplify Record Equalities

fequals_fields simplifies equalities between values of types hrecord_fields, i.e. list of pairs of field names and values.
Ltac fequals_fields :=
  match goal with
  | ⊢ nil = nil ⇒ reflexivity
  | ⊢ cons _ _ = cons _ _ ⇒ applys args_eq_2; [ fequals | fequals_fields ]
  end.
At this point, the tactic xsimpl is refined to take into account simplifications of predicates of the form p ~~~> kvs. The idea is to find a matching predicate of the form p ~~~> kvs' on the right-hand side of the entailment, then to simplify the list equality kvs = kvs'.
Ltac xsimpl_hook_hrecord p :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with hrecord ?kvs' p ⇒
      constr:(true) end);
  apply xsimpl_lr_cancel_eq;
  [ fequal; first [ reflexivity | try fequals_fields ] | ].
Ltac xsimpl_hook H ::=
  match H with
  | hsingle ?p ?v ⇒ xsimpl_hook_hsingle p
  | hrecord ?kvs ?p ⇒ xsimpl_hook_hrecord p
  end.

Demo Programs

Module DemoPrograms.
Export ProgramSyntax.

Definition and Verification of incr.

Here is an implementation of the increment function, written in A-normal form.
   let incr p =
       let n = !p in
       let m = n + 1 in
       p := m
The notation 'p stands for ("x":var). It is defined in LibSepVar.v.
Definition incr : val :=
  <{ fun 'p ⇒
     let 'n = ! 'p in
     let 'm = 'n + 1 in
     'p := 'm }>.
Here is the Separation Logic triple specifying increment. And the proof follows. Note that the script contains explicit references to the specification lemmas of the functions being called (e.g. triple_get for the get operation). The actual CFML2 setup is able to automatically infer those names.
Lemma triple_incr : ∀ (p:loc) (n:int),
  triple (incr p)
    (p ~~> n)
    (fun _ ⇒ (p ~~> (n+1))).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.
We register this specification so that it may be automatically invoked in further examples.
#[global] Hint Resolve triple_incr : triple.
Alternative definition using variable names without quotes, obtained by importing the module Vars from LibSepVar.v.
Module Export Def_incr. Import Vars.
Definition incr' : val :=
  <{ fun p ⇒
       let n = ! p in
       let m = n + 1 in
       p := m }>.
End Def_incr.
Lemma triple_incr' : ∀ (p:loc) (n:int),
  triple (incr' p)
    (p ~~> n)
    (fun _ ⇒ (p ~~> (n+1))).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.

The Decrement Function

Definition decr : val :=
  <{ fun 'p ⇒
       let 'n = ! 'p in
       let 'm = 'n - 1 in
       'p := 'm }>.
Module Export Def_decr. Import Vars.
Definition decr : val :=
  <{ fun p ⇒
       let n = !p in
       let m = n - 1 in
       p := m }>.
End Def_decr.
Lemma triple_decr : ∀ (p:loc) (n:int),
  triple (trm_app decr p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n-1)).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.
#[global] Hint Resolve triple_decr : triple.

Definition and Verification of mysucc.

Another example, involving a call to incr.
Module Export Def_mysucc. Import Vars.
Definition mysucc : val :=
  <{ fun n ⇒
       let r = ref n in
       incr r;
       let x = !r in
       free r;
       x }>.
End Def_mysucc.
Lemma triple_mysucc : ∀ n,
  triple (trm_app mysucc n)
    \[]
    (fun v ⇒ \[v = n+1]).
Proof using.
  xwp. xapp. intros r. xapp. xapp. xapp. xval. xsimpl. auto.
Qed.

Definition and Verification of myrec.

Another example, involving a function involving 3 arguments, as well as record operations.
   let myrec r n1 n2 =
      r.myfield := r.myfield + n1 + n2
Definition myfield : field := 0%nat.
Module Export Def_myrec. Import Vars.
Definition myrec : val :=
  <{ fun p n1 n2 ⇒
       let n = (p`.myfield) in
       let m1 = n + n1 in
       let m2 = m1 + n2 in
       p`.myfield := m2 }>.
Lemma triple_myrec : ∀ (p:loc) (n n1 n2:int),
  triple (myrec p n1 n2)
    (p ~~~> `{ myfield := n})
    (fun _ ⇒ p ~~~> `{ myfield := (n+n1+n2) }).
Proof using.
  xwp. xapp. xapp. xapp. xapp. xsimpl.
Qed.
End Def_myrec.

Definition and Verification of myfun.

Another example involving a local function definition.
Module Export Def_myfun. Import Vars.
Definition myfun : val :=
  <{ fun p ⇒
       let f = (fun_ u ⇒ incr p) in
       f();
       f() }>.
End Def_myfun.
Lemma triple_myfun : ∀ (p:loc) (n:int),
  triple (myfun p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n+2)).
Proof using.
  xwp.
  xfun (fun (f:val) ⇒ ∀ (m:int),
    triple (f())
      (p ~~> m)
      (fun _ ⇒ p ~~> (m+1))); intros f Hf.
  { intros. applys Hf. clear Hf. xapp. xsimpl. }
  xapp.
  xapp.
  replace (n+1+1) with (n+2); [|math]. xsimpl.
Qed.

Demo of a Function with Multiple Arguments.

Definition project_32 : val :=
  <{ fun 'a 'b 'c ⇒ 'b }>.
Lemma triple_project_32 : ∀ (a b c : int),
  triple (project_32 a b c)
    \[]
    (fun r ⇒ \[r = b]).
Proof using. xwp. xval. xsimpl*. Qed.
Definition project_32_rec : val :=
  <{ fix 'f 'a 'b 'c ⇒ if false then 'f 'b end }>.
Lemma triple_project_32_rec : ∀ (a b c : int),
  triple (project_32_rec a b c)
    \[]
    (fun _ ⇒ \[]).
Proof using. xwp. xif; auto_false. intros _. xval. xsimpl. Qed.
End DemoPrograms.
(* 2024-01-03 14:19 *)