LibSepReferenceAppendix - The Full Construction

This file provides a pretty-much end-to-end construction of a weakest-precondition style characteristic formula generator (the function named wpgen in WPgen), for a core programming language with programs assumed to be in A-normal form.
This file is included by the chapters from the course.
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_rand : 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_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 heap values are inhabited.
Global Instance Inhab_val : Inhab val.
Proof using. apply (Inhab_of_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.

Substitution

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.

Semantics

Evaluation rules for unary operations are captured by the predicate redupop op v1 v2, which asserts that op v1 evaluates to v2.
Inductive evalunop : prim → val → val → 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)).
Evaluation rules for binary operations are captured by the predicate redupop op v1 v2 v3, which asserts that op v1 v2 evaluates to v3.
Inductive evalbinop : val → val → val → val → 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).
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.
Big-step evaluation judgement, written eval s t s' v.
Inductive eval : heap → trm → heap → val → Prop :=
  | eval_val : ∀ s v,
      eval s (trm_val v) s v
  | eval_fun : ∀ s x t1,
      eval s (trm_fun x t1) s (val_fun x t1)
  | eval_fix : ∀ s f x t1,
      eval s (trm_fix f x t1) s (val_fix f x t1)
  | eval_app_args : ∀ s1 s2 s3 s4 t1 t2 v1 v2 r,
      (¬ trm_is_val t1 ∨ ¬ trm_is_val t2) →
      eval s1 t1 s2 v1 →
      eval s2 t2 s3 v2 →
      eval s3 (trm_app v1 v2) s4 r →
      eval s1 (trm_app t1 t2) s4 r
  | eval_app_fun : ∀ s1 s2 v1 v2 x t1 v,
      v1 = val_fun x t1 →
      eval s1 (subst x v2 t1) s2 v →
      eval s1 (trm_app v1 v2) s2 v
  | eval_app_fix : ∀ s1 s2 v1 v2 f x t1 v,
      v1 = val_fix f x t1 →
      eval s1 (subst x v2 (subst f v1 t1)) s2 v →
      eval s1 (trm_app v1 v2) s2 v
  | eval_seq : ∀ s1 s2 s3 t1 t2 v1 v,
      eval s1 t1 s2 v1 →
      eval s2 t2 s3 v →
      eval s1 (trm_seq t1 t2) s3 v
  | eval_let : ∀ s1 s2 s3 x t1 t2 v1 r,
      eval s1 t1 s2 v1 →
      eval s2 (subst x v1 t2) s3 r →
      eval s1 (trm_let x t1 t2) s3 r
  | eval_if : ∀ s1 s2 b v t1 t2,
      eval s1 (if b then t1 else t2) s2 v →
      eval s1 (trm_if (val_bool b) t1 t2) s2 v
  | eval_unop : ∀ op m v1 v,
      evalunop op v1 v →
      eval m (op v1) m v
  | eval_binop : ∀ op m v1 v2 v,
      evalbinop op v1 v2 v →
      eval m (op v1 v2) m v
  | eval_ref : ∀ s v p,
      ¬ Fmap.indom s p →
      eval s (val_ref v) (Fmap.update s p v) (val_loc p)
  | eval_get : ∀ s p v,
      Fmap.indom s p →
      v = Fmap.read s p →
      eval s (val_get (val_loc p)) s v
  | eval_set : ∀ s p v,
      Fmap.indom s p →
      eval s (val_set (val_loc p) v) (Fmap.update s p v) val_unit
  | eval_free : ∀ s p,
      Fmap.indom s p →
      eval s (val_free (val_loc p)) (Fmap.remove s p) val_unit.
Specialized evaluation rules for addition and division, for avoiding the indirection via eval_binop in the course.
Lemma eval_add : ∀ s n1 n2,
  eval s (val_add (val_int n1) (val_int n2)) s (val_int (n1 + n2)).
Proof using. intros. applys eval_binop. applys evalbinop_add. Qed.
Lemma eval_div : ∀ s n1 n2,
  n2 ≠ 0 →
  eval s (val_div (val_int n1) (val_int n2)) s (val_int (Z.quot n1 n2)).
Proof using. intros. applys eval_binop. applys* evalbinop_div. 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 s' v, eval s t1 s' v → eval s t2 s' v.

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

In this file, we set up an affine logic. 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.

Evaluation Rules for Primitives in Separation Style

These lemmas reformulated the big-step evaluation rule in a Separation-Logic friendly presentation, that is, by using disjoint unions as much as possible.
Lemma eval_ref_sep : ∀ s1 s2 v p,
  s2 = Fmap.single p v →
  Fmap.disjoint s2 s1 →
  eval s1 (val_ref v) (Fmap.union s2 s1) (val_loc p).
Proof using.
  introv → D. forwards Dv: Fmap.indom_single p v.
  rewrite <- Fmap.update_eq_union_single. applys¬eval_ref.
  { intros N. applys¬Fmap.disjoint_inv_not_indom_both D N. }
Qed.
Lemma eval_get_sep : ∀ s s2 p v,
  s = Fmap.union (Fmap.single p v) s2 →
  eval s (val_get (val_loc p)) s v.
Proof using.
  introv →. forwards Dv: Fmap.indom_single p v.
  applys eval_get.
  { applys¬Fmap.indom_union_l. }
  { rewrite¬Fmap.read_union_l. rewrite¬Fmap.read_single. }
Qed.
Lemma eval_set_sep : ∀ s1 s2 h2 p w v,
  s1 = Fmap.union (Fmap.single p w) h2 →
  s2 = Fmap.union (Fmap.single p v) h2 →
  Fmap.disjoint (Fmap.single p w) h2 →
  eval s1 (val_set (val_loc p) v) s2 val_unit.
Proof using.
  introv → → D. forwards Dv: Fmap.indom_single p w.
  applys_eq eval_set.
  { rewrite¬Fmap.update_union_l. fequals.
    rewrite¬Fmap.update_single. }
  { applys¬Fmap.indom_union_l. }
Qed.
Lemma eval_free_sep : ∀ s1 s2 v p,
  s1 = Fmap.union (Fmap.single p v) s2 →
  Fmap.disjoint (Fmap.single p v) s2 →
  eval s1 (val_free p) s2 val_unit.
Proof using.
  introv → D. forwards Dv: Fmap.indom_single p v.
  applys_eq eval_free.
  { rewrite¬Fmap.remove_union_single_l.
    intros Dl. applys Fmap.disjoint_inv_not_indom_both D Dl.
    applys Fmap.indom_single. }
  { applys¬Fmap.indom_union_l. }
Qed.

Hoare Reasoning Rules

Definition of total correctness Hoare Triples.

Definition hoare (t:trm) (H:hprop) (Q:val→hprop) :=
  ∀ h, H h → ∃ h' v, eval h t h' v ∧ Q v h'.
Structural rules for hoare triples.
Lemma hoare_conseq : ∀ t H' Q' H Q,
  hoare t H' Q' →
  H ==> H' →
  Q' ===> Q →
  hoare t H Q.
Proof using.
  introv M MH MQ HF. forwards (h'&v&R&K): M h. { applys* MH. }
  ∃ h' v. splits¬. { applys* MQ. }
Qed.
Lemma hoare_hexists : ∀ t (A:Type) (J:A→hprop) Q,
  (∀ x, hoare t (J x) Q) →
  hoare t (hexists J) Q.
Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.
Lemma hoare_hpure : ∀ t (P:Prop) H Q,
  (P → hoare t H Q) →
  hoare 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.
Other structural rules, not required for setting up wpgen.
Lemma hoare_hforall : ∀ t (A:Type) (J:A→hprop) Q,
  (∃ x, hoare t (J x) Q) →
  hoare t (hforall J) Q.
Proof using.
  introv (x&M) Hh. applys* hoare_conseq (hforall J) Q M.
  applys* himpl_hforall_l.
Qed.
Lemma hoare_hwand_hpure_l : ∀ t (P:Prop) H Q,
  P →
  hoare t H Q →
  hoare t (\[P] \−∗ H) Q.
Proof using. introv HP M. rewrite* hwand_hpure_l. Qed.
Reasoning rules for hoare triples. These rules follow directly from the big-step evaluation rules.
Lemma hoare_eval_like : ∀ t1 t2 H Q,
  eval_like t1 t2 →
  hoare t1 H Q →
  hoare t2 H Q.
Proof using.
  introv E M1 K0. forwards (s'&v&R1&K1): M1 K0.
  ∃ s' v. split. { applys E R1. } { applys K1. }
Qed.
Lemma hoare_val : ∀ v H Q,
  H ==> Q v →
  hoare (trm_val v) H Q.
Proof using.
  introv M. intros h K. ∃ h v. splits.
  { applys eval_val. }
  { applys* M. }
Qed.
Lemma hoare_fun : ∀ x t1 H Q,
  H ==> Q (val_fun x t1) →
  hoare (trm_fun x t1) H Q.
Proof using.
  introv M. intros h K. ∃ h __. splits.
  { applys¬eval_fun. }
  { applys* M. }
Qed.
Lemma hoare_fix : ∀ f x t1 H Q,
  H ==> Q (val_fix f x t1) →
  hoare (trm_fix f x t1) H Q.
Proof using.
  introv M. intros h K. ∃ h __. splits.
  { applys¬eval_fix. }
  { applys* M. }
Qed.
Lemma hoare_app_fun : ∀ v1 v2 x t1 H Q,
  v1 = val_fun x t1 →
  hoare (subst x v2 t1) H Q →
  hoare (trm_app v1 v2) H Q.
Proof using.
  introv E M. intros s K0. forwards (s'&v&R1&K1): (rm M) K0.
  ∃ s' v. splits. { applys eval_app_fun E R1. } { applys K1. }
Qed.
Lemma hoare_app_fix : ∀ v1 v2 f x t1 H Q,
  v1 = val_fix f x t1 →
  hoare (subst x v2 (subst f v1 t1)) H Q →
  hoare (trm_app v1 v2) H Q.
Proof using.
  introv E M. intros s K0. forwards (s'&v&R1&K1): (rm M) K0.
  ∃ s' v. splits. { applys eval_app_fix E R1. } { applys K1. }
Qed.
Lemma hoare_seq : ∀ t1 t2 H Q H1,
  hoare t1 H (fun r ⇒ H1) →
  hoare t2 H1 Q →
  hoare (trm_seq t1 t2) H Q.
Proof using.
  introv M1 M2 Hh.
  forwards* (h1'&v1&R1&K1): (rm M1).
  forwards* (h2'&v2&R2&K2): (rm M2).
  ∃ h2' v2. splits¬. { applys¬eval_seq R1 R2. }
Qed.
Lemma hoare_let : ∀ x t1 t2 H Q Q1,
  hoare t1 H Q1 →
  (∀ v1, hoare (subst x v1 t2) (Q1 v1) Q) →
  hoare (trm_let x t1 t2) H Q.
Proof using.
  introv M1 M2 Hh.
  forwards* (h1'&v1&R1&K1): (rm M1).
  forwards* (h2'&v2&R2&K2): (rm M2).
  ∃ h2' v2. splits¬. { applys¬eval_let R2. }
Qed.
Lemma hoare_if : ∀ (b:bool) t1 t2 H Q,
  hoare (if b then t1 else t2) H Q →
  hoare (trm_if b t1 t2) H Q.
Proof using.
  introv M1. intros h Hh. forwards* (h1'&v1&R1&K1): (rm M1).
  ∃ h1' v1. splits¬. { applys* eval_if. }
Qed.
Operations on the state.
Lemma hoare_ref : ∀ H v,
  hoare (val_ref v)
    H
    (fun r ⇒ (\∃ p, \[r = val_loc p] \* p ~~> v) \* H).
Proof using.
  intros. intros s1 K0.
  forwards¬(p&D&N): (Fmap.single_fresh 0%nat s1 v).
  ∃ (Fmap.union (Fmap.single p v) s1) (val_loc p). split.
  { applys¬eval_ref_sep D. }
  { applys¬hstar_intro.
    { ∃ p. rewrite¬hstar_hpure_l. split¬. { applys¬hsingle_intro. } } }
Qed.
Lemma hoare_get : ∀ H v p,
  hoare (val_get p)
    ((p ~~> v) \* H)
    (fun r ⇒ \[r = v] \* (p ~~> v) \* H).
Proof using.
  intros. intros s K0. ∃ s v. split.
  { destruct K0 as (s1&s2&P1&P2&D&U).
    lets E1: hsingle_inv P1. subst s1. applys eval_get_sep U. }
  { rewrite¬hstar_hpure_l. }
Qed.
Lemma hoare_set : ∀ H w p v,
  hoare (val_set (val_loc p) v)
    ((p ~~> w) \* H)
    (fun r ⇒ \[r = val_unit] \* (p ~~> v) \* H).
Proof using.
  intros. intros s1 K0.
  destruct K0 as (h1&h2&P1&P2&D&U).
  lets E1: hsingle_inv P1.
  ∃ (Fmap.union (Fmap.single p v) h2) val_unit. split.
  { subst h1. applys eval_set_sep U D. auto. }
  { rewrite hstar_hpure_l. split¬.
    { applys¬hstar_intro.
      { applys¬hsingle_intro. }
      { subst h1. applys Fmap.disjoint_single_set D. } } }
Qed.
Lemma hoare_free : ∀ H p v,
  hoare (val_free (val_loc p))
    ((p ~~> v) \* H)
    (fun r ⇒ \[r = val_unit] \* H).
Proof using.
  intros. intros s1 K0.
  destruct K0 as (h1&h2&P1&P2&D&U).
  lets E1: hsingle_inv P1.
  ∃ h2 val_unit. split.
  { subst h1. applys eval_free_sep U D. }
  { rewrite hstar_hpure_l. split¬. }
Qed.
Other operations.
Lemma hoare_unop : ∀ v H op v1,
  evalunop op v1 v →
  hoare (op v1)
    H
    (fun r ⇒ \[r = v] \* H).
Proof using.
  introv R. intros h Hh. ∃ h v. splits.
  { applys* eval_unop. }
  { rewrite* hstar_hpure_l. }
Qed.
Lemma hoare_binop : ∀ v H op v1 v2,
  evalbinop op v1 v2 v →
  hoare (op v1 v2)
    H
    (fun r ⇒ \[r = v] \* H).
Proof using.
  introv R. intros h Hh. ∃ h v. splits.
  { applys* eval_binop. }
  { rewrite* hstar_hpure_l. }
Qed.
Bonus: example of proofs for a specific primitive operation.
Lemma hoare_add : ∀ H n1 n2,
  hoare (val_add n1 n2)
    H
    (fun r ⇒ \[r = val_int (n1 + n2)] \* H).
Proof.
  dup.
  { intros. applys hoare_binop. applys evalbinop_add. }
  { intros. intros s K0. ∃ s (val_int (n1 + n2)). split.
    { applys eval_binop. applys evalbinop_add. }
    { rewrite* hstar_hpure_l. } }
Qed.

Definition of Separation Logic Triples.

A Separation Logic triple triple t H Q may be defined either in terms of Hoare triples, or in terms of wp, as H ==> wp t Q. We prefer the former route, which we find more elementary.
Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=
  ∀ (H':hprop), hoare t (H \* H') (Q \*+ H').
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.

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.
  introv M MH MQ. intros HF. applys hoare_conseq M.
  { xchanges MH. }
  { intros x. xchanges (MQ x). }
Qed.
Lemma triple_frame : ∀ t H Q H',
  triple t H Q →
  triple t (H \* H') (Q \*+ H').
Proof using.
  introv M. intros HF. applys hoare_conseq (M (HF \* H')); xsimpl.
Qed.
Details for the proof of the frame rule.
Lemma triple_frame' : ∀ t H Q H',
  triple t H Q →
  triple t (H \* H') (Q \*+ H').
Proof using.
  introv M. unfold triple in *. rename H' into H1. intros H2.
  applys hoare_conseq. applys M (H1 \* H2).
  { rewrite hstar_assoc. auto. }
  { intros v. rewrite hstar_assoc. auto. }
Qed.
Extraction rules.
Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,
  (∀ x, triple t (J x) Q) →
  triple t (hexists J) Q.
Proof using.
  introv M. intros HF. rewrite hstar_hexists.
  applys hoare_hexists. intros. applys* M.
Qed.
Lemma triple_hpure : ∀ t (P:Prop) H Q,
  (P → triple t H Q) →
  triple t (\[P] \* H) Q.
Proof using.
  introv M. intros HF. rewrite hstar_assoc.
  applys hoare_hpure. intros. applys* M.
Qed. (* Note: can also be proved from triple_hexists *)
Lemma triple_hforall : ∀ A (x:A) t (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.
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.
Named heaps.
Lemma hexists_named_eq : ∀ H,
  H = (\∃ h, \[H h] \* (= h)).
Proof using.
  intros. apply himpl_antisym.
  { intros h K. applys hexists_intro h.
    rewrite* hstar_hpure_l. }
  { xpull. intros h K. intros ? →. auto. }
Qed.
Lemma triple_named_heap : ∀ t H Q,
  (∀ h, H h → triple t (= h) Q) →
  triple t H Q.
Proof using.
  introv M. rewrite (hexists_named_eq H).
  applys triple_hexists. intros h.
  applys* triple_hpure.
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. intros H'. applys hoare_eval_like E. applys M1.
Qed.
Lemma triple_val : ∀ v H Q,
  H ==> Q v →
  triple (trm_val v) H Q.
Proof using.
  introv M. intros HF. applys hoare_val. { xchanges M. }
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. intros HF. applys¬hoare_fun. { xchanges M. }
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. intros HF. applys¬hoare_fix. { xchanges M. }
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. intros HF. applys hoare_seq.
  { applys M1. }
  { applys hoare_conseq M2; xsimpl. }
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. intros HF. applys hoare_let.
  { applys M1. }
  { intros v. applys hoare_conseq M2; xsimpl. }
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 M1. intros HF. applys hoare_if. applys M1.
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.
  (* can also be proved using triple_eval_like *)
  unfold triple. introv E M1. intros H'.
  applys hoare_app_fun E. applys M1.
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.
  (* can also be proved using triple_eval_like *)
  unfold triple. introv E M1. intros H'.
  applys hoare_app_fix E. applys M1.
Qed.
Lemma triple_app_fix_direct : ∀ v2 f x t1 H Q,
  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 M. applys* triple_app_fix. Qed.

Triple-Style Specification for Primitive Functions

Operations on the state.
Lemma triple_ref : ∀ v,
  triple (val_ref v)
    \[]
    (funloc p ⇒ p ~~> v).
Proof using.
  intros. unfold triple. intros H'. applys hoare_conseq hoare_ref; xsimpl¬.
Qed.
Lemma triple_get : ∀ v p,
  triple (val_get p)
    (p ~~> v)
    (fun r ⇒ \[r = v] \* (p ~~> v)).
Proof using.
  intros. unfold triple. intros H'. applys hoare_conseq hoare_get; xsimpl¬.
Qed.
Lemma triple_set : ∀ w p v,
  triple (val_set (val_loc p) v)
    (p ~~> w)
    (fun _ ⇒ p ~~> v).
Proof using.
  intros. unfold triple. intros H'. applys hoare_conseq hoare_set; xsimpl¬.
Qed.
Lemma triple_free : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun _ ⇒ \[]).
Proof using.
  intros. unfold triple. intros H'. applys hoare_conseq hoare_free; xsimpl¬.
Qed.
Other operations.
Lemma triple_unop : ∀ v op v1,
  evalunop op v1 v →
  triple (op v1) \[] (fun r ⇒ \[r = v]).
Proof using.
  introv R. unfold triple. intros H'.
  applys* hoare_conseq hoare_unop. xsimpl*.
Qed.
Lemma triple_binop : ∀ v op v1 v2,
  evalbinop op v1 v2 v →
  triple (op v1 v2) \[] (fun r ⇒ \[r = v]).
Proof using.
  introv R. unfold triple. intros H'.
  applys* hoare_conseq hoare_binop. xsimpl*.
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_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.

Alternative Definition of wp

Definition of the Weakest-Precondition Judgment.

wp is defined on top of hoare triples. More precisely wp t Q is a heap predicate such that H ==> wp t Q if and only if triple t H Q, where triple t H Q is defined as ∀ H', hoare t (H \* H') (Q \*+ H').
Definition wp (t:trm) := fun (Q:val→hprop) ⇒
  \∃ H, H \* \[∀ H', hoare t (H \* H') (Q \*+ H')].
Equivalence with triples.
Lemma wp_equiv : ∀ t H Q,
  (H ==> wp t Q) ↔ (triple t H Q).
Proof using.
  unfold wp, triple. iff M.
  { intros H'. applys hoare_conseq. 2:{ applys himpl_frame_l M. }
     { clear M. rewrite hstar_hexists. applys hoare_hexists. intros H''.
       rewrite (hstar_comm H''). rewrite hstar_assoc.
       applys hoare_hpure. intros N. applys N. }
     { auto. } }
  { xsimpl H. apply M. }
Qed.

Structural Rule for wp

The ramified frame rule.
Lemma wp_ramified : ∀ Q1 Q2 t,
  (wp t Q1) \* (Q1 \−−∗ Q2) ==> (wp t Q2).
Proof using.
  intros. unfold wp. xpull. intros H M.
  xsimpl (H \* (Q1 \−−∗ Q2)). intros H'.
  applys hoare_conseq M; xsimpl.
Qed.
Arguments wp_ramified : clear implicits.
Corollaries.
Lemma wp_conseq : ∀ t Q1 Q2,
  Q1 ===> Q2 →
  wp t Q1 ==> wp t Q2.
Proof using.
  introv M. applys himpl_trans_r (wp_ramified Q1 Q2). xsimpl. xchanges M.
Qed.
Lemma wp_frame : ∀ t H Q,
  (wp t Q) \* H ==> wp t (Q \*+ H).
Proof using. intros. applys himpl_trans_r wp_ramified. xsimpl. Qed.
Lemma wp_ramified_frame : ∀ t Q1 Q2,
  (wp t Q1) \* (Q1 \−−∗ Q2) ==> (wp t Q2).
Proof using. intros. applys himpl_trans_r wp_ramified. xsimpl. 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. unfold wp. xpull. intros H M. xsimpl H.
  intros H'. applys hoare_eval_like E M.
Qed.
Lemma wp_val : ∀ v Q,
  Q v ==> wp (trm_val v) Q.
Proof using. intros. unfold wp. xsimpl; intros H'. applys hoare_val. xsimpl. Qed.
Lemma wp_fun : ∀ x t Q,
  Q (val_fun x t) ==> wp (trm_fun x t) Q.
Proof using. intros. unfold wp. xsimpl; intros H'. applys hoare_fun. xsimpl. Qed.
Lemma wp_fix : ∀ f x t Q,
  Q (val_fix f x t) ==> wp (trm_fix f x t) Q.
Proof using. intros. unfold wp. xsimpl; intros H'. applys hoare_fix. xsimpl. 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. introv EQ1. unfold wp. xsimpl; intros. applys* hoare_app_fun. Qed.
(* variant: introv EQ1. applys wp_eval_like. introv R. applys* eval_app_fun. *)
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. introv EQ1. unfold wp. xsimpl; intros. applys* hoare_app_fix. Qed.
(* variant: introv EQ1. applys wp_eval_like. introv R. applys* eval_app_fix. *)
Lemma wp_seq : ∀ t1 t2 Q,
  wp t1 (fun r ⇒ wp t2 Q) ==> wp (trm_seq t1 t2) Q.
Proof using.
  intros. unfold wp at 1. xsimpl. intros H' M1.
  unfold wp at 1. xsimpl. intros H''.
  applys hoare_seq. applys (rm M1). unfold wp.
  repeat rewrite hstar_hexists. applys hoare_hexists; intros H'''.
  rewrite (hstar_comm H'''); repeat rewrite hstar_assoc.
  applys hoare_hpure; intros M2. applys hoare_conseq M2; xsimpl.
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.
  intros. unfold wp at 1. xsimpl. intros H' M1.
  unfold wp at 1. xsimpl. intros H''.
  applys hoare_let. applys (rm M1). intros v. simpl. unfold wp.
  repeat rewrite hstar_hexists. applys hoare_hexists; intros H'''.
  rewrite (hstar_comm H'''). rewrite hstar_assoc.
  applys hoare_hpure; intros M2. applys hoare_conseq M2; xsimpl.
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.
  intros. repeat unfold wp. xsimpl; intros H M H'.
  applys hoare_if. applys M.
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)
The first targeted lemma.
Lemma isubst_nil : ∀ t,
  isubst nil t = t.
Proof using. intros t. induction t; simpl; fequals. Qed.
The next lemma 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.
The next lemma 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.
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)).

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 ⇒ wp (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.
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;
   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. } }
  { rename v into x. applys wpgen_fun_sound.
    { intros vx. rewrite* <- isubst_rem. } }
  { rename v into f, v0 into x. applys wpgen_fix_sound.
    { intros vf vx. rewrite* <- isubst_rem_2. } }
  { applys wp_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 ==> wp t Q.
Proof using.
  introv M W. rewrite <- wp_equiv in M. xchange W. xchange M.
  applys wp_ramified_frame.
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 →
  H ==> wpgen ((f,v1)::(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 (((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 (wp t) Q →
  triple t H Q.
Proof using.
  introv M. rewrite <- wp_equiv. xchange M. unfold mkstruct.
  xpull. intros Q'. applys wp_ramified_frame.
Qed.

Tactics to Manipulate wpgen Formulae

The tactic are presented in 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.
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; 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 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_debug" :=
  xseq_xlet_if_needed; xstruct_if_needed; applys xapp_lemma.
xapp is essentially equivalent to xapp_debug; [ 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 [
     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.
Tactic Notation "xwp" :=
  intros;
  first [ applys xwp_lemma_fun; [ reflexivity | ]
        | applys xwp_lemma_fix; [ reflexivity | ] ];
  xwp_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' f v1" :=
  ((wp (trm_app f v1)))
  (in custom wp at level 68, f, v1 at level 0) : wp_scope.
Notation "'App' f v1 v2" :=
  ((wp (trm_app (trm_app f v1) v2)))
  (in custom wp at level 68, f, v1, v2 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.
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 '=>' 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 "'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 '=>' 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 "()" :=
  (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) : trm_scope.
Notation "'free'" :=
  (trm_val (val_prim val_free))
  (in custom trm at level 0) : trm_scope.
Notation "'not'" :=
  (trm_val (val_prim val_neg))
  (in custom trm at level 0) : 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.

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.

Bonus

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.

Treatment of Functions of 2 and 3 Arguments

As explained in chapter Struct, there are different ways to support functions of several arguments: curried functions, n-ary functions, or functions expecting a tuple as argument.
For simplicity, we here follow the approach based on curried function, specialized for arity 2 and 3. It is possible to state arity-generic definitions and lemmas, but the definitions become much more technical.
From an engineering point of view, it is easier and more efficient to follow the approach using n-ary functions, as the CFML tool does.

Syntax for Functions of 2 or 3 Arguments.

Notation "'fun' x1 x2 '=>' t" :=
  (val_fun x1 (trm_fun x2 t))
  (in custom trm at level 69,
   x1, x2 at level 0,
   format "'fun' x1 x2 '=>' t") : val_scope.
Notation "'fix' f x1 x2 '=>' t" :=
  (val_fix f x1 (trm_fun x2 t))
  (in custom trm at level 69,
   f, x1, x2 at level 0,
   format "'fix' f x1 x2 '=>' t") : val_scope.
Notation "'fun_' x1 x2 '=>' t" :=
  (trm_fun x1 (trm_fun x2 t))
  (in custom trm at level 69,
   x1, x2 at level 0,
   format "'fun_' x1 x2 '=>' t") : trm_scope.
Notation "'fix_' f x1 x2 '=>' t" :=
  (trm_fix f x1 (trm_fun x2 t))
  (in custom trm at level 69,
   f, x1, x2 at level 0,
   format "'fix_' f x1 x2 '=>' t") : trm_scope.
Notation "'fun' x1 x2 x3 '=>' t" :=
  (val_fun x1 (trm_fun x2 (trm_fun x3 t)))
  (in custom trm at level 69,
   x1, x2, x3 at level 0,
   format "'fun' x1 x2 x3 '=>' t") : val_scope.
Notation "'fix' f x1 x2 x3 '=>' t" :=
  (val_fix f x1 (trm_fun x2 (trm_fun x3 t)))
  (in custom trm at level 69,
   f, x1, x2, x3 at level 0,
   format "'fix' f x1 x2 x3 '=>' t") : val_scope.
Notation "'fun_' x1 x2 x3 '=>' t" :=
  (trm_fun x1 (trm_fun x2 (trm_fun x3 t)))
  (in custom trm at level 69,
   x1, x2, x3 at level 0, format "'fun_' x1 x2 x3 '=>' t") : trm_scope.
Notation "'fix_' f x1 x2 x3 '=>' t" :=
  (trm_fix f x1 (trm_fun x2 (trm_fun x3 t)))
  (in custom trm at level 69,
   f, x1, x2, x3 at level 0, format "'fix_' f x1 x2 x3 '=>' t") : trm_scope.

Evaluation Rules for Applications to 2 or 3 Arguments.

eval_like judgment for applications to several arguments.
Lemma eval_like_app_fun2 : ∀ v0 v1 v2 x1 x2 t1,
  v0 = val_fun x1 (trm_fun x2 t1) →
  x1 ≠ x2 →
  eval_like (subst x2 v2 (subst x1 v1 t1)) (v0 v1 v2).
Proof using.
  introv E N. introv R. applys* eval_app_args.
  { applys eval_app_fun E. simpl. rewrite var_eq_spec. case_if. applys eval_fun. }
  { applys* eval_val. }
  { applys* eval_app_fun. }
Qed.
Lemma eval_like_app_fix2 : ∀ v0 v1 v2 f x1 x2 t1,
  v0 = val_fix f x1 (trm_fun x2 t1) →
  (x1 ≠ x2 ∧ f ≠ x2) →
  eval_like (subst x2 v2 (subst x1 v1 (subst f v0 t1))) (v0 v1 v2).
Proof using.
  introv E (N1&N2). introv R. applys* eval_app_args.
  { applys eval_app_fix E. simpl. do 2 (rewrite var_eq_spec; case_if). applys eval_fun. }
  { applys* eval_val. }
  { applys* eval_app_fun. }
Qed.
Lemma eval_like_app_fun3 : ∀ v0 v1 v2 v3 x1 x2 x3 t1,
  v0 = val_fun x1 (trm_fun x2 (trm_fun x3 t1)) →
  (x1 ≠ x2 ∧ x1 ≠ x3 ∧ x2 ≠ x3) →
  eval_like (subst x3 v3 (subst x2 v2 (subst x1 v1 t1))) (v0 v1 v2 v3).
Proof using.
  introv E (N1&N2&N3). introv R. applys* eval_app_args.
  { applys* eval_like_app_fun2 E. simpl. do 2 (rewrite var_eq_spec; case_if). applys eval_fun. }
  { applys eval_val. }
  { applys* eval_app_fun. }
Qed.
Lemma eval_like_app_fix3 : ∀ v0 v1 v2 v3 f x1 x2 x3 t1,
  v0 = val_fix f x1 (trm_fun x2 (trm_fun x3 t1)) →
  (x1 ≠ x2 ∧ f ≠ x2 ∧ f ≠ x3 ∧ x1 ≠ x3 ∧ x2 ≠ x3) →
  eval_like (subst x3 v3 (subst x2 v2 (subst x1 v1 (subst f v0 t1)))) (v0 v1 v2 v3).
Proof using.
  introv E (N1&N2&N3&N4&N5). introv R. applys* eval_app_args.
  { applys* eval_like_app_fix2 E. simpl. do 3 (rewrite var_eq_spec; case_if). applys eval_fun. }
  { applys eval_val. }
  { applys* eval_app_fun. }
Qed.

Reasoning Rules for Applications to 2 or 3 Arguments

Weakest preconditions for applications to several arguments.
Lemma wp_app_fun2 : ∀ x1 x2 v0 v1 v2 t1 Q,
  v0 = val_fun x1 (trm_fun x2 t1) →
  x1 ≠ x2 →
  wp (subst x2 v2 (subst x1 v1 t1)) Q ==> wp (trm_app v0 v1 v2) Q.
Proof using. introv EQ1 N. applys wp_eval_like. applys* eval_like_app_fun2. Qed.
Lemma wp_app_fix2 : ∀ f x1 x2 v0 v1 v2 t1 Q,
  v0 = val_fix f x1 (trm_fun x2 t1) →
  (x1 ≠ x2 ∧ f ≠ x2) →
  wp (subst x2 v2 (subst x1 v1 (subst f v0 t1))) Q ==> wp (trm_app v0 v1 v2) Q.
Proof using. introv EQ1 N. applys wp_eval_like. applys* eval_like_app_fix2. Qed.
Lemma wp_app_fun3 : ∀ x1 x2 x3 v0 v1 v2 v3 t1 Q,
  v0 = val_fun x1 (trm_fun x2 (trm_fun x3 t1)) →
  (x1 ≠ x2 ∧ x1 ≠ x3 ∧ x2 ≠ x3) →
  wp (subst x3 v3 (subst x2 v2 (subst x1 v1 t1))) Q ==> wp (trm_app v0 v1 v2 v3) Q.
Proof using. introv EQ1 N. applys wp_eval_like. applys* eval_like_app_fun3. Qed.
Lemma wp_app_fix3 : ∀ f x1 x2 x3 v0 v1 v2 v3 t1 Q,
  v0 = val_fix f x1 (trm_fun x2 (trm_fun x3 t1)) →
  (x1 ≠ x2 ∧ f ≠ x2 ∧ f ≠ x3 ∧ x1 ≠ x3 ∧ x2 ≠ x3) →
  wp (subst x3 v3 (subst x2 v2 (subst x1 v1 (subst f v0 t1)))) Q ==> wp (trm_app v0 v1 v2 v3) Q.
Proof using. introv EQ1 N. applys wp_eval_like. applys* eval_like_app_fix3. Qed.

Generalization of xwp to Handle Functions of Two Arguments

Generalization of xwp to handle functions of arity 2 and 3, and to handle weakening of an existing specification.
Lemma xwp_lemma_fun2 : ∀ v0 v1 v2 x1 x2 t H Q,
  v0 = val_fun x1 (trm_fun x2 t) →
  var_eq x1 x2 = false →
  H ==> wpgen ((x1,v1)::(x2,v2)::nil) t Q →
  triple (v0 v1 v2) H Q.
Proof using.
  introv M1 N M2. rewrite var_eq_spec in N. rew_bool_eq in *.
  rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound (((x1,v1)::nil) ++ ((x2,v2)::nil)) t Q).
  rewrite isubst_app. do 2 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fun2.
Qed.
Lemma xwp_lemma_fix2 : ∀ f v0 v1 v2 x1 x2 t H Q,
  v0 = val_fix f x1 (trm_fun x2 t) →
  (var_eq x1 x2 = false ∧ var_eq f x2 = false) →
  H ==> wpgen ((f,v0)::(x1,v1)::(x2,v2)::nil) t Q →
  triple (v0 v1 v2) H Q.
Proof using.
  introv M1 N M2. repeat rewrite var_eq_spec in N. rew_bool_eq in *.
  rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound (((f,v0)::nil) ++ ((x1,v1)::nil) ++ ((x2,v2)::nil)) t Q).
  do 2 rewrite isubst_app. do 3 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fix2.
Qed.
Lemma xwp_lemma_fun3 : ∀ v0 v1 v2 v3 x1 x2 x3 t H Q,
  v0 = val_fun x1 (trm_fun x2 (trm_fun x3 t)) →
  (var_eq x1 x2 = false ∧ var_eq x1 x3 = false ∧ var_eq x2 x3 = false) →
  H ==> wpgen ((x1,v1)::(x2,v2)::(x3,v3)::nil) t Q →
  triple (v0 v1 v2 v3) H Q.
Proof using.
  introv M1 N M2. repeat rewrite var_eq_spec in N. rew_bool_eq in *.
  rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound (((x1,v1)::nil) ++ ((x2,v2)::nil) ++ ((x3,v3)::nil)) t Q).
  do 2 rewrite isubst_app. do 3 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fun3.
Qed.
Lemma xwp_lemma_fix3 : ∀ f v0 v1 v2 v3 x1 x2 x3 t H Q,
  v0 = val_fix f x1 (trm_fun x2 (trm_fun x3 t)) →
  ( var_eq x1 x2 = false ∧ var_eq f x2 = false ∧ var_eq f x3 = false
   ∧ var_eq x1 x3 = false ∧ var_eq x2 x3 = false) →
  H ==> wpgen ((f,v0)::(x1,v1)::(x2,v2)::(x3,v3)::nil) t Q →
  triple (v0 v1 v2 v3) H Q.
Proof using.
  introv M1 N M2. repeat rewrite var_eq_spec in N. rew_bool_eq in *.
  rewrite <- wp_equiv. xchange M2.
  xchange (>> wpgen_sound (((f,v0)::nil) ++ ((x1,v1)::nil) ++ ((x2,v2)::nil) ++ ((x3,v3)::nil)) t Q).
  do 3 rewrite isubst_app. do 4 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fix3.
Qed.
Tactic Notation "xwp" :=
  intros;
  first [ applys xwp_lemma_fun; [ reflexivity | ]
        | applys xwp_lemma_fix; [ reflexivity | ]
        | applys xwp_lemma_fun2; [ reflexivity | reflexivity | ]
        | applys xwp_lemma_fix2; [ reflexivity | splits; reflexivity | ]
        | applys xwp_lemma_fun3; [ reflexivity | splits; reflexivity | ]
        | applys xwp_lemma_fix3; [ reflexivity | splits; reflexivity | ]
        | fail 1 "xwp only applies to functions defined using [val_fun] or [val_fix], with at most 3 arguments" ];
  xwp_simpl.

Bonus: Triples for Applications to Several Arguments

Triples for applications to 2 arguments. Similar rules can be stated and proved for 3 arguments. These rules are not needed for the verification framework.
Lemma triple_app_fun2 : ∀ v0 v1 v2 x1 x2 t1 H Q,
  v0 = val_fun x1 (trm_fun x2 t1) →
  x1 ≠ x2 →
  triple (subst x2 v2 (subst x1 v1 t1)) H Q →
  triple (v0 v1 v2) H Q.
Proof using.
  introv E N M1. applys triple_eval_like M1. applys* eval_like_app_fun2.
Qed.
Lemma triple_app_fix2 : ∀ f x1 x2 v0 v1 v2 t1 H Q,
  v0 = val_fix f x1 (trm_fun x2 t1) →
  (x1 ≠ x2 ∧ f ≠ x2) →
  triple (subst x2 v2 (subst x1 v1 (subst f v0 t1))) H Q →
  triple (v0 v1 v2) H Q.
Proof using.
  introv E N M1. applys triple_eval_like M1. applys* eval_like_app_fix2.
Qed.

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 ==> wp (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 ==> wp (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.
End DemoPrograms.
(* 2023-10-01 07:24 *)