LibSepReferenceAppendix - The Full Construction

This file provides an end-to-end construction of a weakest-precondition style characteristic formula generator (the function named wpgen in chapter WPgen), for a core programming language with programs assumed to be in A-normal form, including support for records with up to 3 fields.

Set Implicit Arguments.
From SLF Require Export LibCore.
From SLF Require Export LibSepTLCbuffer LibSepVar LibSepFmap.
From SLF Require LibSepSimpl.
Module Fmap := LibSepFmap. (* Short name for Fmap module. *)

Imports

Extensionality Axioms

These standard extensionality axioms may also be found in the LibAxiom.v file associated with the TLC library.

Axiom functional_extensionality : ∀ A B (f g:A →B),
(∀ x, f x = g x ) →
f = g.

Axiom propositional_extensionality : ∀ (P Q:Prop),
(P ↔ Q ) →
P = Q.

Variables

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

Finite Maps

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

Source Language

Syntax

The grammar of primitive operations includes a number of operations.

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.

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.

A state, a.k.a. heap, 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 heap : Type := fmap loc val.

Coq Tweaks

h₁ \u h₂ is a notation for union of two heaps.

Notation "h₁ \u h₂" := (Fmap.union h₁ h₂)
(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 s : heap.

The types of values and terms are inhabited.

Global Instance Inhab_val : Inhab val.
Proof using. apply (Inhab_of_val val_unit). Qed.

Global Instance Inhab_trm : Inhab trm.
Proof using. apply (Inhab_of_val (trm_val val_unit)). Qed.

Coercions to improve conciseness in the statment of evaluation rules.

Coercion val_bool : bool >-> val.
Coercion val_int : Z >-> val.
Coercion val_loc : loc >-> val.
Coercion val_prim : prim >-> val.

Coercion trm_val : val >-> trm.
Coercion trm_var : var >-> trm.
Coercion trm_app : trm >-> Funclass.

Values and Substitutions

The predicate trm_is_val t asserts that t is a value.

Definition trm_is_val (t:trm) : Prop :=
match t with trm_val v ⇒ True | _ ⇒ False end.

The standard capture-avoiding substitution, written subst x v t.

Fixpoint subst (y:var) (v':val) (t:trm) : trm :=
  let aux t := subst y v' t in
  let if_y_eq x t₁ t₂ := if var_eq x y then t₁ else t₂ in
  match t with
  | trm_val v ⇒ trm_val v
  | trm_var x ⇒ if_y_eq x (trm_val v') t
  | trm_fun x t₁ ⇒ trm_fun x (if_y_eq x t₁ (aux t₁))
  | trm_fix f x t₁ ⇒ trm_fix f x (if_y_eq f t₁ (if_y_eq x t₁ (aux t₁)))
  | trm_app t₁ t₂ ⇒ trm_app (aux t₁) (aux t₂)
  | trm_seq t₁ t₂ ⇒ trm_seq (aux t₁) (aux t₂)
  | trm_let x t₁ t₂ ⇒ trm_let x (aux t₁) (if_y_eq x t₂ (aux t₂))
  | trm_if t₀ t₁ t₂ ⇒ trm_if (aux t₀) (aux t₁) (aux t₂)
  end.

Small-Step Semantics

The judgment step s t s' t' asserts that the configuration (s,t) can take one reduction step towards the program configuration (s',t').

Inductive step : heap → trm → heap → trm → Prop :=

  (* Context rules *)
  | step_seq_ctx : ∀ s₁ s₂ t₁ t₁' t₂,
      step s₁ t₁ s₂ t₁' →
      step s₁ (trm_seq t₁ t₂) s₂ (trm_seq t₁' t₂)
  | step_let_ctx : ∀ s₁ s₂ x t₁ t₁' t₂,
      step s₁ t₁ s₂ t₁' →
      step s₁ (trm_let x t₁ t₂) s₂ (trm_let x t₁' t₂)
  | step_app_arg1 : ∀ s₁ s₂ t₁ t₁' t₂,
      step s₁ t₁ s₂ t₁' →
      step s₁ (trm_app t₁ t₂) s₂ (trm_app t₁' t₂)
  | step_app_arg2 : ∀ s₁ s₂ v₁ t₂ t₂',
      step s₁ t₂ s₂ t₂' →
      step s₁ (trm_app v₁ t₂) s₂ (trm_app v₁ t₂')

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

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

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

  (* Heap operations *)
  | step_ref : ∀ s v p,
      ¬ Fmap.indom s p →
      step s (val_ref v) (Fmap.update s p v) (val_loc p)
  | step_get : ∀ s p,
      Fmap.indom s p →
      step s (val_get (val_loc p)) s (Fmap.read s p)
  | step_set : ∀ s p v,
      Fmap.indom s p →
      step s (val_set (val_loc p) v) (Fmap.update s p v) val_unit
  | step_free : ∀ s p,
      Fmap.indom s p →
      step s (val_free (val_loc p)) (Fmap.remove s p) val_unit.

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

Inductive steps : heap → trm → heap → trm → Prop :=
  | steps_refl : ∀ s t,
      steps s t s t
  | steps_step : ∀ s₁ s₂ s₃ t₁ t₂ t₃,
      step s₁ t₁ s₂ t₂ →
      steps s₂ t₂ s₃ t₃ →
      steps s₁ t₁ s₃ t₃.

Lemma steps_of_step : ∀ s₁ s₂ t₁ t₂,
step s₁ t₁ s₂ t₂ →
steps s₁ t₁ s₂ t₂.
Proof using. introv M. applys steps_step M. applys steps_refl. Qed.

Lemma steps_trans : ∀ s₁ s₂ s₃ t₁ t₂ t₃,
  steps s₁ t₁ s₂ t₂ →
  steps s₂ t₂ s₃ t₃ →
  steps s₁ t₁ s₃ t₃.
Proof using. introv M₁. induction M₁; introv M₂. { auto. } { constructors*. } Qed.

The predicate reducible s t asserts that the configuration (s,t) can take a step.

Definition reducible (s:heap) (t:trm) : Prop :=
∃ s' t', step s t s' t'.

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

Definition notstuck (s:heap) (t:trm) : Prop :=
trm_is_val t ∨ reducible s t.

Omni-Big-Step Semantics of primitive operations

Evaluation rules for unary operations are captured by the predicate evalunop op v₁ P, which asserts that op v₁ evaluates to a value v₂ satisfying P.

Inductive evalunop : prim → val → (val →Prop) → Prop :=
  | evalunop_neg : ∀ b₁,
      evalunop val_neg (val_bool b₁) (= val_bool (neg b₁))
  | evalunop_opp : ∀ n₁,
      evalunop val_opp (val_int n₁) (= val_int (- n₁))
  | evalunop_rand : ∀ n,
      n > 0 →
      evalunop val_rand (val_int n) (fun r ⇒ ∃ n₁ , r = val_int n₁ ∧ 0 ≤ n₁ < n).

Evaluation rules for binary operations are captured by the predicate redupop op v₁ v₂ P, which asserts that op v₁ v₂ evaluates to a value v₃ satisfying P.

Inductive evalbinop : val → val → val → (val →Prop) → Prop :=
  | evalbinop_eq : ∀ v₁ v₂,
      evalbinop val_eq v₁ v₂ (= val_bool (isTrue (v₁ = v₂)))
  | evalbinop_neq : ∀ v₁ v₂,
      evalbinop val_neq v₁ v₂ (= val_bool (isTrue (v₁ ≠ v₂)))
  | evalbinop_add : ∀ n₁ n₂,
      evalbinop val_add (val_int n₁) (val_int n₂) (= val_int (n₁ + n₂))
  | evalbinop_sub : ∀ n₁ n₂,
      evalbinop val_sub (val_int n₁) (val_int n₂) (= val_int (n₁ - n₂))
  | evalbinop_mul : ∀ n₁ n₂,
      evalbinop val_mul (val_int n₁) (val_int n₂) (= val_int (n₁ * n₂))
  | evalbinop_div : ∀ n₁ n₂,
      n₂ ≠ 0 →
      evalbinop val_div (val_int n₁) (val_int n₂) (= val_int (Z.quot n₁ n₂))
  | evalbinop_mod : ∀ n₁ n₂,
      n₂ ≠ 0 →
      evalbinop val_mod (val_int n₁) (val_int n₂) (= val_int (Z.rem n₁ n₂))
  | evalbinop_le : ∀ n₁ n₂,
      evalbinop val_le (val_int n₁) (val_int n₂) (= val_bool (isTrue (n₁ ≤ n₂)))
  | evalbinop_lt : ∀ n₁ n₂,
      evalbinop val_lt (val_int n₁) (val_int n₂) (= val_bool (isTrue (n₁ < n₂)))
  | evalbinop_ge : ∀ n₁ n₂,
      evalbinop val_ge (val_int n₁) (val_int n₂) (= val_bool (isTrue (n₁ ≥ n₂)))
  | evalbinop_gt : ∀ n₁ n₂,
      evalbinop val_gt (val_int n₁) (val_int n₂) (= val_bool (isTrue (n₁ > n₂)))
  | evalbinop_ptr_add : ∀ p₁ p₂ n,
      (p₂:int) = p₁ + n →
      evalbinop val_ptr_add (val_loc p₁) (val_int n) (= val_loc p₂).

Omni-Big-Step Semantics

Section Eval.

The predicate purepost s P converts a predicate P:val→Prop into a postcondition of type val→heap→Prop that holds in the state s.

Definition purepost (s:heap) (P:val →Prop) : val →heap →Prop :=
fun v s' ⇒ P v ∧ s' = s.

Definition purepostin (s:heap) (P:val →Prop) (Q:val →heap →Prop) : Prop :=
(* equivalent to purepost S P ===> Q *)
∀ v, P v → Q v s.

Omni-Big-step evaluation judgement, written eval s t Q.

Implicit Types Q : val →heap →Prop.

Inductive eval : heap → trm → (val →heap →Prop) → Prop :=
  | eval_val : ∀ s v Q,
      Q v s →
      eval s (trm_val v) Q
  | eval_fun : ∀ s x t₁ Q,
      Q (val_fun x t₁) s →
      eval s (trm_fun x t₁) Q
  | eval_fix : ∀ s f x t₁ Q,
      Q (val_fix f x t₁) s →
      eval s (trm_fix f x t₁) Q
  | eval_app_arg1 : ∀ s₁ t₁ t₂ Q₁ Q,
      ¬ trm_is_val t₁ →
      eval s₁ t₁ Q₁ →
      (∀ v₁ s₂, Q₁ v₁ s₂ → eval s₂ (trm_app v₁ t₂) Q ) →
      eval s₁ (trm_app t₁ t₂) Q
  | eval_app_arg2 : ∀ s₁ v₁ t₂ Q₁ Q,
      ¬ trm_is_val t₂ →
      eval s₁ t₂ Q₁ →
      (∀ v₂ s₂, Q₁ v₂ s₂ → eval s₂ (trm_app v₁ v₂) Q ) →
      eval s₁ (trm_app v₁ t₂) Q
  | eval_app_fun : ∀ s₁ v₁ v₂ x t₁ Q,
      v₁ = val_fun x t₁ →
      eval s₁ (subst x v₂ t₁) Q →
      eval s₁ (trm_app v₁ v₂) Q
  | eval_app_fix : ∀ s v₁ v₂ f x t₁ Q,
      v₁ = val_fix f x t₁ →
      eval s (subst x v₂ (subst f v₁ t₁)) Q →
      eval s (trm_app v₁ v₂) Q
  | eval_seq : ∀ Q₁ s t₁ t₂ Q,
      eval s t₁ Q₁ →
      (∀ v₁ s₂, Q₁ v₁ s₂ → eval s₂ t₂ Q ) →
      eval s (trm_seq t₁ t₂) Q
  | eval_let : ∀ Q₁ s x t₁ t₂ Q,
      eval s t₁ Q₁ →
      (∀ v₁ s₂, Q₁ v₁ s₂ → eval s₂ (subst x v₁ t₂) Q ) →
      eval s (trm_let x t₁ t₂) Q
  | eval_if : ∀ s (b:bool) t₁ t₂ Q,
      eval s (if b then t₁ else t₂) Q →
      eval s (trm_if (val_bool b) t₁ t₂) Q
  | eval_unop : ∀ op s v₁ P Q,
      evalunop op v₁ P →
      purepostin s P Q →
      eval s (op v₁) Q
  | eval_binop : ∀ op s v₁ v₂ P Q,
      evalbinop op v₁ v₂ P →
      purepostin s P Q →
      eval s (op v₁ v₂) Q
  | eval_ref : ∀ s v Q,
      (∀ p, ¬ Fmap.indom s p →
          Q (val_loc p) (Fmap.update s p v)) →
      eval s (val_ref v) Q
  | eval_get : ∀ s p Q,
      Fmap.indom s p →
      Q (Fmap.read s p) s →
      eval s (val_get (val_loc p)) Q
  | eval_set : ∀ s p v Q,
      Fmap.indom s p →
      Q val_unit (Fmap.update s p v) →
      eval s (val_set (val_loc p) v) Q
  | eval_free : ∀ s p Q,
      Fmap.indom s p →
      Q val_unit (Fmap.remove s p) →
      eval s (val_free (val_loc p)) Q.

Specialized rule for values, to instantiate the postcondition

Lemma eval_val_minimal : ∀ s v,
eval s (trm_val v) (fun v' s' ⇒ (v' = v ) ∧ (s' = s )).
Proof using. intros. applys* eval_val. Qed.

Specialized evaluation rules for selected operations, to avoid the indirection via eval_unop and eval_binop in the course.

Lemma eval_add : ∀ s n₁ n₂ Q,
  Q (val_int (n₁ + n₂)) s →
  eval s (val_add (val_int n₁) (val_int n₂)) Q.
Proof using.
  intros. applys* eval_binop.
  { applys* evalbinop_add. }
  { intros ? →. auto. }
Qed.

Lemma eval_div : ∀ s n₁ n₂ Q,
  n₂ ≠ 0 →
  Q (val_int (Z.quot n₁ n₂)) s →
  eval s (val_div (val_int n₁) (val_int n₂)) Q.
Proof using.
  intros. applys* eval_binop.
  { applys* evalbinop_div. }
  { intros ? →. auto. }
Qed.

Lemma eval_rand : ∀ s n Q,
  n > 0 →
  (∀ n₁, 0 ≤ n₁ < n → Q n₁ s ) →
  eval s (val_rand (val_int n)) Q.
Proof using.
  intros. applys* eval_unop.
  { applys* evalunop_rand. }
  { intros ? (?&->&?). auto. }
Qed.

Derived rule for reasoning about an applications, without need to perform a case analysis on whether the entities are already values.

Lemma eval_app_arg1' : ∀ s₁ t₁ t₂ Q₁ Q,
  eval s₁ t₁ Q₁ →
  (∀ v₁ s₂, Q₁ v₁ s₂ → eval s₂ (trm_app v₁ t₂) Q ) →
  eval s₁ (trm_app t₁ t₂) Q.
Proof using.
  introv M₁ M₂. tests C₁: (trm_is_val t₁).
  { destruct t₁; tryfalse. inverts M₁. applys* M₂. }
  { applys* eval_app_arg1. }
Qed.

Lemma eval_app_arg2' : ∀ s₁ v₁ t₂ Q₁ Q,
  eval s₁ t₂ Q₁ →
  (∀ v₂ s₂, eval s₂ (trm_app v₁ v₂) Q ) →
  eval s₁ (trm_app v₁ t₂) Q.
Proof using.
  introv M₁ M₂. tests C₁: (trm_is_val t₂).
  { destruct t₂; tryfalse. inverts M₁. applys* M₂. }
  { applys* eval_app_arg2. }
Qed.

eval_like t₁ t₂ asserts that t₂ evaluates like t₁. In particular, this relation hold whenever t₂ reduces in small-step to t₁.

Definition eval_like (t₁ t₂:trm) : Prop :=
∀ s Q, eval s t₁ Q → eval s t₂ Q.

End Eval.

Heap Predicates

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

Module SepSimplArgs.

Hprop and Entailment

Declare Scope hprop_scope.
Open Scope hprop_scope.

The type of heap predicates is named hprop.

Definition hprop := heap → Prop.

Implicit types for meta-variables.

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

Entailment for heap predicates, written H₁ ==> H₂. This entailment is linear.

Definition himpl (H₁ H₂:hprop) : Prop :=
∀ h, H₁ h → H₂ h.

Notation "H₁ ==> H₂" := (himpl H₁ H₂) (at level 55) : hprop_scope.

Entailment between postconditions, written Q₁ ===> Q₂.

Definition qimpl A (Q₁ Q₂:A →hprop) : Prop :=
∀ (v:A), Q₁ v ==> Q₂ v.

Notation "Q₁ ===> Q₂" := (qimpl Q₁ Q₂) (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
H₁ \* H₂ denotes the separating conjunction
Q₁ \*+ H₂ denotes the separating conjunction extending a postcondition
\∃ x, H denotes an existential quantifier
\∀ x, H denotes a universal quantifier
H₁ \−∗ H₂ denotes a magic wand between heap predicates
Q₁ \−−∗ Q₂ 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 (H₁ H₂ : hprop) : hprop :=
  fun h ⇒ ∃ h₁ h₂ , H₁ h₁
                              ∧ H₂ h₂
                              ∧ Fmap.disjoint h₁ h₂
                              ∧ h = Fmap.union h₁ h₂.

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 "H₁ '\*' H₂" := (hstar H₁ H₂)
(at level 41, right associativity) : hprop_scope.

Notation "'\exists' x₁ .. xn , H" :=
  (hexists (fun x₁ ⇒ .. (hexists (fun xn ⇒ H)) ..))
  (at level 39, x₁ binder, H at level 50, right associativity,
   format "'[' '\exists' '/ ' x₁ .. xn , '/ ' H ']'") : hprop_scope.

Notation "'\forall' x₁ .. xn , H" :=
  (hforall (fun x₁ ⇒ .. (hforall (fun xn ⇒ H)) ..))
  (at level 39, x₁ binder, H at level 50, right associativity,
   format "'[' '\forall' '/ ' x₁ .. 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 (H₁ H₂ : hprop) : hprop :=
\∃ H₀ , H₀ \* hpure ((H₁ \* H₀ ) ==> H₂).

Definition qwand A (Q₁ Q₂:A →hprop) : hprop :=
\∀ x , hwand (Q₁ x) (Q₂ 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 "H₁ \−∗ H₂" := (hwand H₁ H₂)
(at level 43, right associativity) : hprop_scope.

Notation "Q₁ \−−∗ Q₂" := (qwand Q₁ Q₂)
(at level 43) : hprop_scope.

Basic Properties of Separation Logic Operators

Tactic for Automation

We set up auto to process goals of the form h₁ = h₂ 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 h₁ h₂ 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 : ∀ H₂ H₁ H₃,
  (H₁ ==> H₂ ) →
  (H₂ ==> H₃ ) →
  (H₁ ==> H₃ ).
Proof using. introv M₁ M₂. unfolds* himpl. Qed.

Lemma himpl_trans_r : ∀ H₂ H₁ H₃,
   H₂ ==> H₃ →
   H₁ ==> H₂ →
   H₁ ==> H₃.
Proof using. introv M₁ M₂. applys* himpl_trans M₂ M₁. Qed.

Lemma himpl_antisym : ∀ H₁ H₂,
  (H₁ ==> H₂ ) →
  (H₂ ==> H₁ ) →
  (H₁ = H₂ ).
Proof using. introv M₁ M₂. applys pred_ext_1. intros h. iff*. Qed.

Lemma hprop_op_comm : ∀ (op:hprop →hprop →hprop),
(∀ H₁ H₂, op H₁ H₂ ==> op H₂ H₁ ) →
(∀ H₁ H₂, op H₁ H₂ = op H₂ H₁ ).
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 : ∀ H₁ H₂ h₁ h₂,
  H₁ h₁ →
  H₂ h₂ →
  Fmap.disjoint h₁ h₂ →
  (H₁ \* H₂ ) (Fmap.union h₁ h₂ ).
Proof using. intros. ∃¬h₁ h₂. Qed.

Lemma hstar_inv : ∀ H₁ H₂ h,
(H₁ \* H₂ ) h →
∃ h₁ h₂ , H₁ h₁ ∧ H₂ h₂ ∧ Fmap.disjoint h₁ h₂ ∧ h = Fmap.union h₁ h₂.
Proof using. introv M. applys M. Qed.

Lemma hstar_comm : ∀ H₁ H₂,
   H₁ \* H₂ = H₂ \* H₁.
Proof using.
  applys hprop_op_comm. unfold hprop, hstar. intros H₁ H₂.
  intros h (h₁&h₂&M₁&M₂&D&U). rewrite¬Fmap.union_comm_of_disjoint in U.
  ∃* h₂ h₁.
Qed.

Lemma hstar_assoc : ∀ H₁ H₂ H₃,
  (H₁ \* H₂ ) \* H₃ = H₁ \* (H₂ \* H₃ ).
Proof using.
  intros H₁ H₂ H₃. applys himpl_antisym; intros h.
  { intros (h'&h₃&(h₁&h₂&M₃&M₄&D'&U')&M₂&D&U). subst h'.
    ∃ h₁ (h₂ \+ h₃). splits¬. { applys* hstar_intro. } }
  { intros (h₁&h'&M₁&(h₂&h₃&M₃&M₄&D'&U')&D&U). subst h'.
    ∃ (h₁ \+ h₂) h₃. splits¬. { applys* hstar_intro. } }
Qed.

Lemma hstar_hempty_l : ∀ H,
  \[] \* H = H.
Proof using.
  intros. applys himpl_antisym; intros h.
  { intros (h₁&h₂&M₁&M₂&D&U). forwards E: hempty_inv M₁. 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 (h₁&h₂&(x&M₁)&M₂&D&U). ∃¬x h₁ h₂. }
  { intros (x&(h₁&h₂&M₁&M₂&D&U)). ∃ h₁ h₂. 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 (h₁&h₂&M₁&M₂&D&U). intros x. ∃¬h₁ h₂.
Qed.

Lemma himpl_frame_l : ∀ H₂ H₁ H₁',
H₁ ==> H₁' →
(H₁ \* H₂ ) ==> (H₁' \* H₂ ).
Proof using. introv W (h₁&h₂&?). ∃* h₁ h₂. Qed.

Lemma himpl_frame_r : ∀ H₁ H₂ H₂',
  H₂ ==> H₂' →
  (H₁ \* H₂ ) ==> (H₁ \* H₂').
Proof using.
  introv M. do 2 rewrite (@hstar_comm H₁). applys¬himpl_frame_l.
Qed.

Lemma himpl_frame_lr : ∀ H₁ H₁' H₂ H₂',
  H₁ ==> H₁' →
  H₂ ==> H₂' →
  (H₁ \* H₂ ) ==> (H₁' \* H₂').
Proof using.
  introv M₁ M₂. applys himpl_trans. applys¬himpl_frame_l M₁. applys¬himpl_frame_r.
Qed.

Lemma himpl_hstar_trans_l : ∀ H₁ H₂ H₃ H₄,
  H₁ ==> H₂ →
  H₂ \* H₃ ==> H₄ →
  H₁ \* H₃ ==> H₄.
Proof using.
  introv M₁ M₂. applys himpl_trans M₂. applys himpl_frame_l M₁.
Qed.

Lemma himpl_hstar_trans_r : ∀ H₁ H₂ H₃ H₄,
  H₁ ==> H₂ →
  H₃ \* H₂ ==> H₄ →
  H₃ \* H₁ ==> H₄.
Proof using.
  introv M₁ M₂. applys himpl_trans M₂. applys himpl_frame_r M₁.
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 (J₁ J₂:A →hprop),
  J₁ ===> J₂ →
  hexists J₁ ==> hexists J₂.
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 (J₁ J₂:A →hprop),
  J₁ ===> J₂ →
  hforall J₁ ==> hforall J₂.
Proof using.
  introv W. applys himpl_hforall_r. intros x. applys himpl_hforall_l W.
Qed.

Properties of hwand

Lemma hwand_equiv : ∀ H₀ H₁ H₂,
  (H₀ ==> H₁ \−∗ H₂ ) ↔ (H₁ \* H₀ ==> H₂ ).
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 H₁). applys¬himpl_hstar_hpure_l. }
  { applys himpl_hexists_r H₀.
    rewrite <- (hstar_hempty_r H₀) at 1.
    applys himpl_frame_r. applys himpl_hempty_hpure M. }
Qed.

Lemma himpl_hwand_r : ∀ H₁ H₂ H₃,
H₂ \* H₁ ==> H₃ →
H₁ ==> (H₂ \−∗ H₃ ).
Proof using. introv M. rewrite¬hwand_equiv. Qed.

Lemma himpl_hwand_r_inv : ∀ H₁ H₂ H₃,
H₁ ==> (H₂ \−∗ H₃ ) →
H₂ \* H₁ ==> H₃.
Proof using. introv M. rewrite¬<- hwand_equiv. Qed.

Lemma hwand_cancel : ∀ H₁ H₂,
H₁ \* (H₁ \−∗ H₂ ) ==> H₂.
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 : ∀ H₁ H₂ H₃,
  (H₁ \* H₂ ) \−∗ H₃ ==> H₁ \−∗ (H₂ \−∗ H₃ ).
Proof using.
  intros. apply himpl_hwand_r. apply himpl_hwand_r.
  rewrite <- hstar_assoc. rewrite (hstar_comm H₁ H₂).
  applys hwand_cancel.
Qed.

Lemma hwand_uncurry : ∀ H₁ H₂ H₃,
  H₁ \−∗ (H₂ \−∗ H₃ ) ==> (H₁ \* H₂ ) \−∗ H₃.
Proof using.
  intros. rewrite hwand_equiv. rewrite (hstar_comm H₁ H₂).
  rewrite hstar_assoc. applys himpl_hstar_trans_r.
  { applys hwand_cancel. } { applys hwand_cancel. }
Qed.

Lemma hwand_curry_eq : ∀ H₁ H₂ H₃,
  (H₁ \* H₂ ) \−∗ H₃ = H₁ \−∗ (H₂ \−∗ H₃ ).
Proof using.
  intros. applys himpl_antisym.
  { applys hwand_curry. }
  { applys hwand_uncurry. }
Qed.

Lemma hwand_inv : ∀ h₁ h₂ H₁ H₂,
  (H₁ \−∗ H₂ ) h₂ →
  H₁ h₁ →
  Fmap.disjoint h₁ h₂ →
  H₂ (h₁ \u h₂).
Proof using.
  introv M₂ M₁ D. unfolds hwand. lets (H₀&M₃): hexists_inv M₂.
  lets (h₀&h₃&P₁&P₃&D'&U): hstar_inv M₃. lets (P₄&E₃): hpure_inv P₃.
  subst h₂ h₃. rewrite union_empty_r in *. applys P₄. applys* hstar_intro.
Qed.

Properties of qwand

Lemma qwand_equiv : ∀ H A (Q₁ Q₂:A →hprop),
  H ==> (Q₁ \−−∗ Q₂ ) ↔ (Q₁ \*+ H ) ===> Q₂.
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 (Q₁ Q₂:A →hprop),
Q₁ \*+ (Q₁ \−−∗ Q₂ ) ===> Q₂.
Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.

Lemma himpl_qwand_r : ∀ A (Q₁ Q₂:A →hprop) H,
Q₁ \*+ H ===> Q₂ →
H ==> (Q₁ \−−∗ Q₂ ).
Proof using. introv M. rewrite¬qwand_equiv. Qed.

Arguments himpl_qwand_r [A].

Lemma qwand_specialize : ∀ A (x:A) (Q₁ Q₂:A →hprop),
(Q₁ \−−∗ Q₂ ) ==> (Q₁ x \−∗ Q₂ 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 w₁ w₂,
  (p ~~> w₁ ) \* (p ~~> w₂ ) ==> \[False ].
Proof using.
  intros. unfold hsingle. intros h (h₁&h₂&E₁&E₂&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 H₁ \* .. \* 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 H₁. Then, it cancels it out with the p ~~> v that occurs in HR. Otherwise, the tactic fails.

Ltac xsimpl_hook_hsingle p :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with (hsingle p ?v') ⇒
      constr:(true) end);
  apply xsimpl_lr_cancel_eq;
  [ xsimpl_lr_cancel_eq_repr_post tt | ].

The tactic xsimpl_hook handles cancellation of heap predicates of the form p ~~> v. It forces their cancellation against heap predicates of the form p ~~> w, by asserting the equality v = w. Note: this tactic is later refined to also handle records.

Ltac xsimpl_hook H ::=
  match H with
  | hsingle ?p ?v ⇒ xsimpl_hook_hsingle p
  end.

One last hack is to improve the math tactic so that it is able to handle the val_int coercion in goals and hypotheses of the form val_int ?n = val_int ?m, and so that it is able to process the well-founded relations dowto and upto for induction on integers.

Ltac math_0 ::=
  unfolds downto, upto;
  repeat match goal with
  | ⊢ val_int _ = val_int _ ⇒ fequal
  | H: val_int _ = val_int _ ⊢ _ ⇒ inverts H
  end.

Properties of haffine

The lemma haffine_any asserts that haffine H holds for any H. Nevertheless, let us state corollaries of haffine_any for specific heap predicates, to illustrate how the xaffine tactic works in chapter Affine.

Lemma haffine_hempty :
haffine \[].
Proof using. intros. applys haffine_hany. Qed.

Lemma haffine_hpure : ∀ P,
haffine \[P ].
Proof using. intros. applys haffine_hany. Qed.

Lemma haffine_hstar : ∀ H₁ H₂,
  haffine H₁ →
  haffine H₂ →
  haffine (H₁ \* H₂).
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.

Reasoning Rules

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

Definition of Separation Logic Triples.

The Separation Logic triple triple t H Q is defined in terms of the omni-big-step semantics predicate eval s t Q.

Definition triple (t:trm) (H:hprop) (Q:val →hprop) : Prop :=
∀ s, H s → eval s t Q.

We introduce a handy notation for postconditions of functions that return a pointer: funloc p ⇒ H is short for fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* H).

Notation "'funloc' p '=>' H" :=
(fun (r:val) ⇒ \∃ p , \[r = val_loc p] \* H)
(at level 200, p name, format "'funloc' p '=>' H") : hprop_scope.

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

If one considers the omni-big-step semantics to be the starting point of a development, then the definition of triple is obviously sound with respect to that semantics, as it concludes eval s t Q. If, however, one considers the small-step semantics to be the starting point, then to establish soundness it is required to prove that triple t H Q ensures that all possible evaluations of t in a heap satisfy H are: (1) terminating, (2) always reaching a value, and (3) this value and the final state obtained satisfy the postconditon Q.

The judgment terminates s t is defined inductively. The execution starting from (s,t) terminates if, for any possible step leads to a configuration that terminates. Note that a configuration that has reached a value cannot take a step, hence is considered terminating.

Inductive terminates : heap →trm →Prop :=
  | terminates_step : ∀ s t,
      (∀ s' t', step s t s' t' → terminates s' t') →
      terminates s t.

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

Definition safe (s:heap) (t:trm) : Prop :=
∀ s' t', steps s t s' t' → notstuck s' t'.

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

Definition correct (s:heap) (t:trm) (Q:val →hprop) : Prop :=
∀ s' v, steps s t s' v → Q v s'.

The aim is to show that triple t H Q entails that, for any s satisfying H, terminates s t and safe s t and correct s t Q holds.

The judgment seval s t Q asserts that any execution of (s,t) terminates and reaches a configuration satisfying Q. In the "base" case, seval s v Q holds if the terminal configuration (s,v) satisfies Q. In the "step" case, seval s t Q holds if (1) the configuration (s,t) is reducible, and (2) if for any step that (s,t) may take to (s',t'), the predicate seval s' t' Q holds.

Inductive seval : heap →trm ->(val →hprop )->Prop :=
  | seval_val : ∀ s v Q,
      Q v s →
      seval s v Q
  | seval_step : ∀ s t Q,
      reducible s t → (* (exists s' t', step s t s' t') *)
      (∀ s' t', step s t s' t' → seval s' t' Q ) →
      seval s t Q.

The judgment seval s t Q satisfies the 3 targeted soundness properties.

Lemma seval_terminates : ∀ s t Q,
  seval s t Q →
  terminates s t.
Proof using.
  introv M. induction M; constructors; introv R.
  { inverts R. }
  { eauto. }
Qed.

Lemma seval_safe : ∀ s t Q,
  seval s t Q →
  safe s t.
Proof using.
  introv M R. gen Q. induction R; intros.
  { inverts M. { left. hnfs*. } { right*. } }
  { rename H into S. inverts M. { inverts S. } { applys* IHR. } }
Qed.

Lemma seval_correct : ∀ s t Q,
  seval s t Q →
  correct s t Q.
Proof using.
  introv M. induction M; introv R.
  { inverts R as. { auto. } { introv S. inverts S. } }
  { rename H₁ into IH. inverts R. { lets (?&?&R): H. inverts R. } applys* IH. }
Qed.

false_step is a handy tactic to get rid of goals with assumptions of the form step s v s' t' or step s (op v) s' t' for a binary operator op.

Ltac false_step :=
  solve [ match goal with
  | K: step _ (trm_app (trm_val (val_prim _)) (trm_val _)) _ _ ⊢ _ ⇒
      inversion K; clear K; subst; false_step
  | K: step _ (trm_val _) _ _ ⊢ _ ⇒
      inversion K; clear K; subst
  | _ ⇒ false
  end ].

The proof that eval s t Q entails seval s t Q begins with a bunch of auxiliary lemmas.

Lemma seval_fun : ∀ s x t₁ Q,
  Q (val_fun x t₁) s →
  seval s (trm_fun x t₁) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructor. }
  { introv R. inverts R. { applys seval_val. applys M. } }
Qed.

Lemma seval_fix : ∀ s f x t₁ Q,
  Q (val_fix f x t₁) s →
  seval s (trm_fix f x t₁) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructor. }
  { introv R. inverts R. { applys seval_val. applys M. } }
Qed.

Lemma seval_app_fun : ∀ s x v₁ v₂ t₁ Q,
  v₁ = val_fun x t₁ →
  seval s (subst x v₂ t₁) Q →
  seval s (trm_app v₁ v₂) Q.
Proof using.
  introv E M. applys seval_step.
  { do 2 esplit. applys* step_app_fun. }
  { introv R. invert R; try solve [intros; false | introv R; inverts R]. introv → → → → → R. inverts E. applys M. }
Qed.

Lemma seval_app_fix : ∀ s f x v₁ v₂ t₁ Q,
  v₁ = val_fix f x t₁ →
  seval s (subst x v₂ (subst f v₁ t₁)) Q →
  seval s (trm_app v₁ v₂) Q.
Proof using.
  introv E M. applys seval_step.
  { do 2 esplit. applys* step_app_fix. }
  { introv R. invert R; try solve [intros; false | introv R; inverts R]. introv → → → → → R. inverts E. applys M. }
Qed.

Lemma seval_seq : ∀ s t₁ t₂ Q₁ Q,
  seval s t₁ Q₁ →
  (∀ s₁ v₁, Q₁ v₁ s₁ → seval s₁ t₂ Q ) →
  seval s (trm_seq t₁ t₂) Q.
Proof using.
  introv M₁ M₂. gen_eq Q₁': Q₁.
  induction M₁; intros; subst.
  { apply seval_step.
    { do 2 esplit. applys step_seq. }
    { introv R. inverts R as R'. { inverts R'. } applys* M₂. } }
  { rename t into t₁, H₁ into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. constructors. applys RE. }
    { introv R. inverts R as R'.
      { applys* IH R' M₂. }
      { false. inverts RE. } } }
Qed.

Lemma seval_let : ∀ s x t₁ t₂ Q₁ Q,
  seval s t₁ Q₁ →
  (∀ s₁ v₁, Q₁ v₁ s₁ → seval s₁ (subst x v₁ t₂) Q ) →
  seval s (trm_let x t₁ t₂) Q.
Proof using.
  introv M₁ M₂. gen_eq Q₁': Q₁.
  induction M₁; intros; subst.
  { apply seval_step.
    { do 2 esplit. applys step_let. }
    { introv R. inverts R as R'. { inverts R'. } applys* M₂. } }
  { rename t into t₁, H₁ into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. constructors. applys RE. }
    { introv R. inverts R as R'.
      { applys* IH R' M₂. }
      { false. inverts RE. } } }
Qed.

Lemma seval_app_arg1 : ∀ t₁ t₂ Q₁ s₁ Q,
  seval s₁ t₁ Q₁ →
  (∀ v₁ s₂, Q₁ v₁ s₂ → seval s₂ (v₁ t₂) Q ) →
  seval s₁ (t₁ t₂) Q.
Proof using.
  introv M₁ M₂. gen_eq Q₁': Q₁.
  induction M₁; intros; subst.
  { applys* M₂. }
  { rename t into t₁, H₁ into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. applys step_app_arg1. applys RE. }
    { introv R. inverts R as R'; try solve [inverts RE]; try false_step.
      { applys* IH R'. } } }
Qed.

Lemma seval_app_arg2 : ∀ v₁ t₂ Q₁ s₁ Q,
  seval s₁ t₂ Q₁ →
  (∀ v₂ s₂, Q₁ v₂ s₂ → seval s₂ (v₁ v₂) Q ) →
  seval s₁ (v₁ t₂) Q.
Proof using.
  introv M₁ M₂. gen_eq Q₁': Q₁.
  induction M₁; intros; subst.
  { applys* M₂. }
  { rename t into t₁, H₁ into IH.
    destruct H as (s'&t'&RE). applys seval_step.
    { do 2 esplit. applys step_app_arg2. applys RE. }
    { introv R. inverts R as R'; try solve [inverts RE]; try false_step.
      { applys* IH R'. } } }
Qed.

Lemma seval_if : ∀ s b t₁ t₂ Q,
  seval s (if b then t₁ else t₂) Q →
  seval s (trm_if b t₁ t₂) Q.
Proof using.
  introv M. applys seval_step.
  { do 2 esplit. constructors*. }
  { introv R. inverts R; tryfalse. { applys M. } }
Qed.

Lemma seval_of_eval : ∀ s t Q,
  eval s t Q →
  seval s t Q.
Proof using.
  introv M. induction M.
  { applys* seval_val. }
  { applys* seval_fun. }
  { applys* seval_fix. }
  { applys* seval_app_arg1. }
  { applys* seval_app_arg2. }
  { applys* seval_app_fun. }
  { applys* seval_app_fix. }
  { applys* seval_seq. }
  { applys* seval_let. }
  { applys* seval_if. }
  { rename H into HE, H₀ into K. unfolds purepostin.
    applys seval_step.
    { inverts HE; try solve [do 2 esplit; constructor; eauto].
      { ∃ s 0. applys step_rand. math. } }
    { introv R. inverts R; try false_step; inverts HE; applys* seval_val. } }
   { rename H into HE, H₀ into K. unfolds purepostin.
    applys seval_step.
    { inverts HE; try solve [do 2 esplit; constructor; eauto]. }
    { introv R. inverts R; do 2 (try inverts_if_head step); inverts HE; applys* seval_val.
      (* alternative: inverts HE; inverts R; try false_step; applys* seval_val. *)
      { math_rewrite (p₂ = p₃). { applys eq_nat_of_eq_int. math. } eauto. } } }
  { applys seval_step.
    { forwards¬(p&D&N): (exists_fresh null s).
      do 2 esplit. applys* step_ref. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_get. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_set. }
    { introv R. do 3 (try inverts_if_head step). applys* seval_val. } }
  { applys seval_step.
    { do 2 esplit. applys* step_free. }
    { introv R. do 2 (try inverts_if_head step). applys* seval_val. } }
Qed.

Final soundness theorem with respect to the small-step semantics.

Lemma triple_sound : ∀ t H Q,
  triple t H Q →
  ∀ s, H s → terminates s t ∧ safe s t ∧ correct s t Q.
Proof using.
  introv M Hs. specializes M Hs. lets M': seval_of_eval M. splits.
  { applys* seval_terminates. }
  { applys* seval_safe. }
  { applys* seval_correct. }
Qed.

Structural Properties of the eval Predicate

Section EvalProp.
Hint Constructors eval.

Covariance property

Lemma eval_conseq : ∀ s t Q₁ Q₂,
  eval s t Q₁ →
  Q₁ ===> Q₂ →
  eval s t Q₂.
Proof using.
  introv M W.
  asserts W': (∀ v h, Q₁ v h → Q₂ v h). { auto. } clear W.
  induction M; try solve [ constructors* ].
  { applys* eval_unop. unfolds* purepostin. }
  { applys* eval_binop. unfolds* purepostin. }
Qed.

Frame property

Lemma eval_frame : ∀ h₁ h₂ t Q,
  eval h₁ t Q →
  Fmap.disjoint h₁ h₂ →
  eval (h₁ \u h₂) t (Q \*+ (= h₂ )).
Proof using.
  introv M HD. gen h₂. induction M; intros;
    try solve [ hint hstar_intro; constructors* ].
  { rename M into M₁, H into M₂, IHM into IH₁, H₁ into IH₂.
    specializes IH₁ HD. applys* eval_app_arg1 IH₁. introv HK.
    lets (h₁'&h₂'&K₁'&K₂'&KD&KU): hstar_inv HK. subst. applys* IH₂. }
  { rename M into M₁, H into M₂, IHM into IH₁, H₁ into IH₂.
    specializes IH₁ HD. applys* eval_app_arg2 IH₁. introv HK.
    lets (h₁'&h₂'&K₁'&K₂'&KD&KU): hstar_inv HK. subst. applys* IH₂. }
  { rename M into M₁, H into M₂, IHM into IH₁, H₀ into IH₂.
    specializes IH₁ HD. applys eval_seq IH₁. introv HK.
    lets (h₁'&h₂'&K₁'&K₂'&KD&KU): hstar_inv HK. subst. applys* IH₂. }
  { rename M into M₁, H into M₂, IHM into IH₁, H₀ into IH₂.
    specializes IH₁ HD. applys eval_let IH₁. introv HK.
    lets (h₁'&h₂'&K₁'&K₂'&KD&KU): hstar_inv HK. subst. applys* IH₂. }
  { applys* eval_unop. unfolds* purepostin. introv Hv. applys* hstar_intro. }
  { applys* eval_binop. unfolds* purepostin. introv Hv. applys* hstar_intro. }
  { rename H into M. applys eval_ref. intros p Hp.
    rewrite Fmap.indom_union_eq in Hp. rew_logic in Hp. destruct Hp as [Hp₁ Hp₂].
    rewrite* Fmap.update_union_not_r. applys hstar_intro.
    { applys* M. } { auto. } { applys* Fmap.disjoint_update_not_r. } }
  { applys eval_get. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.read_union_l. applys* hstar_intro. } }
  { applys eval_set. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.update_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_update_l. } } }
  { applys eval_free. { rewrite* Fmap.indom_union_eq. }
    { rewrite* Fmap.remove_disjoint_union_l. applys hstar_intro.
      { auto. } { auto. } { applys* Fmap.disjoint_remove_l. } } }
Qed.

End EvalProp.

Structural Rules

Consequence and frame rule.

Lemma triple_conseq : ∀ t H' Q' H Q,
  triple t H' Q' →
  H ==> H' →
  Q' ===> Q →
  triple t H Q.
Proof using. unfolds triple. introv M MH MQ HF. applys* eval_conseq. Qed.

Lemma triple_frame : ∀ t H Q H',
  triple t H Q →
  triple t (H \* H') (Q \*+ H').
Proof.
  introv M. intros h HF. lets (h₁&h₂&M₁&M₂&MD&MU): hstar_inv (rm HF).
  subst. specializes M M₁. applys eval_conseq.
  { applys eval_frame M MD. } { xsimpl. intros h' →. applys M₂. }
Qed.

Extraction Rules

Lemma triple_hpure : ∀ t (P:Prop) H Q,
  (P → triple t H Q ) →
  triple t (\[P ] \* H) Q.
Proof using.
  introv M. intros h (h₁&h₂&M₁&M₂&D&U). destruct M₁ as (M₁&HP).
  lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.
Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A →hprop) Q,
(∀ (x:A), triple t (J x) Q ) →
triple t (hexists J) Q.
Proof using. introv M. intros h (x&Hh). applys M Hh. Qed.

Lemma triple_hforall : ∀ t (A:Type) (x:A) (J:A →hprop) Q,
triple t (J x) Q →
triple t (hforall J) Q.
Proof using. introv M. applys* triple_conseq M. applys hforall_specialize. Qed.

Lemma triple_hwand_hpure_l : ∀ t (P:Prop) H Q,
  P →
  triple t H Q →
  triple t (\[P ] \−∗ H) Q.
Proof using. introv HP M. applys* triple_conseq M. rewrite* hwand_hpure_l. Qed.

A corollary of triple_hpure useful for the course

Parameter triple_hpure' : ∀ t (P:Prop) Q,
(P → triple t \[] Q ) →
triple t \[P ] Q.

Heap-naming rule

Lemma triple_named_heap : ∀ t H Q,
(∀ h, H h → triple t (= h) Q ) →
triple t H Q.
Proof using. introv M Hs. applys M Hs. auto. Qed.

Combined and ramified rules.

Lemma triple_conseq_frame : ∀ H₂ H₁ Q₁ t H Q,
  triple t H₁ Q₁ →
  H ==> H₁ \* H₂ →
  Q₁ \*+ H₂ ===> 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 : ∀ H₁ Q₁ t H Q,
  triple t H₁ Q₁ →
  H ==> H₁ \* (Q₁ \−−∗ Q ) →
  triple t H Q.
Proof using.
  introv M W. applys triple_conseq_frame (Q₁ \−−∗ Q) M W.
  { rewrite¬<- qwand_equiv. }
Qed.

Rules for Terms

Lemma triple_eval_like : ∀ t₁ t₂ H Q,
  eval_like t₁ t₂ →
  triple t₁ H Q →
  triple t₂ H Q.
Proof using. introv E M₁ Hv. applys* E. Qed.

Lemma triple_val : ∀ v H Q,
H ==> Q v →
triple (trm_val v) H Q.
Proof using. introv M Hs. applys* eval_val. Qed.

Lemma triple_val_minimal : ∀ v,
triple (trm_val v) \[] (fun r ⇒ \[r = v ]).
Proof using. intros. applys triple_val. xsimpl*. Qed.

Lemma triple_fun : ∀ x t₁ H Q,
H ==> Q (val_fun x t₁) →
triple (trm_fun x t₁) H Q.
Proof using. introv M Hs. applys* eval_fun. Qed.

Lemma triple_fix : ∀ f x t₁ H Q,
H ==> Q (val_fix f x t₁) →
triple (trm_fix f x t₁) H Q.
Proof using. introv M Hs. applys* eval_fix. Qed.

Lemma triple_seq : ∀ t₁ t₂ H Q H₁,
  triple t₁ H (fun v ⇒ H₁) →
  triple t₂ H₁ Q →
  triple (trm_seq t₁ t₂) H Q.
Proof using. introv M₁ M₂ Hs. applys* eval_seq. Qed.

Lemma triple_let : ∀ x t₁ t₂ Q₁ H Q,
  triple t₁ H Q₁ →
  (∀ v₁, triple (subst x v₁ t₂) (Q₁ v₁) Q ) →
  triple (trm_let x t₁ t₂) H Q.
Proof using. introv M₁ M₂ Hs. applys* eval_let. Qed.

Lemma triple_let_val : ∀ x v₁ t₂ H Q,
  triple (subst x v₁ t₂) H Q →
  triple (trm_let x v₁ t₂) H Q.
Proof using.
  introv M. applys triple_let (fun v ⇒ \[v = v₁] \* H).
  { applys triple_val. xsimpl*. }
  { intros v. applys triple_hpure. intros →. applys M. }
Qed.

Lemma triple_if : ∀ (b:bool) t₁ t₂ H Q,
triple (if b then t₁ else t₂) H Q →
triple (trm_if b t₁ t₂) H Q.
Proof using. introv M Hs. applys* eval_if. Qed.

Lemma triple_app_fun : ∀ x v₁ v₂ t₁ H Q,
  v₁ = val_fun x t₁ →
  triple (subst x v₂ t₁) H Q →
  triple (trm_app v₁ v₂) H Q.
Proof using. introv E M Hs. applys* eval_app_fun. Qed.

Lemma triple_app_fun_direct : ∀ x v₂ t₁ H Q,
triple (subst x v₂ t₁) H Q →
triple (trm_app (val_fun x t₁) v₂) H Q.
Proof using. introv M. applys* triple_app_fun. Qed.

Lemma triple_app_fix : ∀ v₁ v₂ f x t₁ H Q,
  v₁ = val_fix f x t₁ →
  triple (subst x v₂ (subst f v₁ t₁)) H Q →
  triple (trm_app v₁ v₂) H Q.
Proof using. introv E M Hs. applys* eval_app_fix. Qed.

Lemma triple_app_fix_direct : ∀ v₂ f x t₁ H Q,
  f ≠ x →
  triple (subst x v₂ (subst f (val_fix f x t₁) t₁)) H Q →
  triple (trm_app (val_fix f x t₁) v₂) H Q.
Proof using. introv N M. applys* triple_app_fix. Qed.

Rules for Heap-Manipulating Primitive Operations

Lemma triple_ref : ∀ v,
  triple (val_ref v)
    \[]
    (fun r ⇒ \∃ p , \[r = val_loc p ] \* p ~~> v).
Proof using.
  intros. intros s₁ K. applys eval_ref. intros p D.
  lets ->: hempty_inv K. rewrite Fmap.update_empty.
  applys hexists_intro p. rewrite hstar_hpure_l. split*.
  applys hsingle_intro.
Qed.

Lemma triple_get : ∀ v p,
  triple (val_get p)
    (p ~~> v)
    (fun r ⇒ \[r = v ] \* (p ~~> v )).
Proof using.
  intros. intros s K. lets ->: hsingle_inv K.
  applys eval_get.
  { applys* Fmap.indom_single. }
  { rewrite hstar_hpure_l. split*. rewrite* Fmap.read_single. }
Qed.

Lemma triple_set : ∀ w p v,
  triple (val_set (val_loc p) v)
    (p ~~> w)
    (fun r ⇒ \[r = val_unit ] \* (p ~~> v )).
Proof using.
  intros. intros s₁ K. lets ->: hsingle_inv K. lets Hp: indom_single p v.
  applys eval_set.
  { applys* Fmap.indom_single. }
  { rewrite hstar_hpure_l. split*. rewrite Fmap.update_single. applys hsingle_intro. }
Qed.

Lemma triple_free' : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun r ⇒ \[r = val_unit ]).
Proof using.
  intros. intros s₁ K. lets ->: hsingle_inv K. lets Hp: indom_single p v.
  applys eval_free.
  { applys* Fmap.indom_single. }
  { rewrite* Fmap.remove_single. applys* hpure_intro. }
Qed.

Lemma triple_free : ∀ p v,
  triple (val_free (val_loc p))
    (p ~~> v)
    (fun r ⇒ \[]).
Proof using. intros. applys triple_conseq triple_free'; xsimpl*. Qed.

Rules for Other Primitive Operations

Lemma triple_unop' : ∀ op v₁ (P:val →Prop) Q, (* DEPRECATED? *)
  evalunop op v₁ P →
  (∀ v, P v → Q v Fmap.empty ) → (* purepostin heap_empty P Q ->*)
  triple (op v₁) \[] Q.
Proof using.
  introv M R Hs. lets ->: hempty_inv Hs. applys eval_unop M. hnfs*.
Qed.

Lemma triple_binop' : ∀ op v₁ v₂ (P:val →Prop) Q, (* DEPRECATED? *)
  evalbinop op v₁ v₂ P →
  (∀ v, P v → Q v Fmap.empty ) →
  triple (op v₁ v₂) \[] Q.
Proof using.
  introv M R Hs. lets ->: hempty_inv Hs. applys eval_binop M. hnfs*.
Qed.

Lemma triple_unop : ∀ op v₁ (P:val →Prop),
  evalunop op v₁ P →
  triple (op v₁) \[] (fun r ⇒ \[P r ]).
Proof using.
  introv M Hs. lets ->: hempty_inv Hs.
  applys eval_conseq (fun v s ⇒ P v ∧ s = Fmap.empty).
  { applys* eval_unop M. hnfs*. }
  { intros v s (?&->). applys* hpure_intro. }
Qed.

Lemma triple_binop : ∀ op v₁ v₂ (P:val →Prop),
  evalbinop op v₁ v₂ P →
  triple (op v₁ v₂) \[] (fun r ⇒ \[P r ]).
Proof using.
  introv M Hs. lets ->: hempty_inv Hs.
  applys eval_conseq (fun v s ⇒ P v ∧ s = Fmap.empty).
  { applys* eval_binop M. hnfs*. }
  { intros v s (?&->). applys* hpure_intro. }
Qed.

Lemma triple_add : ∀ n₁ n₂,
  triple (val_add n₁ n₂)
    \[]
    (fun r ⇒ \[r = val_int (n₁ + n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_add. Qed.

Lemma triple_div : ∀ n₁ n₂,
  n₂ ≠ 0 →
  triple (val_div n₁ n₂)
    \[]
    (fun r ⇒ \[r = val_int (Z.quot n₁ n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_div. Qed.

Lemma triple_rand : ∀ n,
  n > 0 →
  triple (val_rand n)
    \[]
    (fun r ⇒ \[∃ n₁ , r = val_int n₁ ∧ 0 ≤ n₁ < n ]).
Proof using. intros. applys* triple_unop. applys* evalunop_rand. Qed.

Lemma triple_neg : ∀ (b₁:bool),
  triple (val_neg b₁)
    \[]
    (fun r ⇒ \[r = val_bool (neg b₁)]).
Proof using. intros. applys* triple_unop. applys* evalunop_neg. Qed.

Lemma triple_opp : ∀ n₁,
  triple (val_opp n₁)
    \[]
    (fun r ⇒ \[r = val_int (- n₁)]).
Proof using. intros. applys* triple_unop. applys* evalunop_opp. Qed.

Lemma triple_eq : ∀ v₁ v₂,
  triple (val_eq v₁ v₂)
    \[]
    (fun r ⇒ \[r = isTrue (v₁ = v₂)]).
Proof using. intros. applys* triple_binop. applys evalbinop_eq. Qed.

Lemma triple_neq : ∀ v₁ v₂,
  triple (val_neq v₁ v₂)
    \[]
    (fun r ⇒ \[r = isTrue (v₁ ≠ v₂)]).
Proof using. intros. applys* triple_binop. applys evalbinop_neq. Qed.

Lemma triple_sub : ∀ n₁ n₂,
  triple (val_sub n₁ n₂)
    \[]
    (fun r ⇒ \[r = val_int (n₁ - n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_sub. Qed.

Lemma triple_mul : ∀ n₁ n₂,
  triple (val_mul n₁ n₂)
    \[]
    (fun r ⇒ \[r = val_int (n₁ * n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_mul. Qed.

Lemma triple_mod : ∀ n₁ n₂,
  n₂ ≠ 0 →
  triple (val_mod n₁ n₂)
    \[]
    (fun r ⇒ \[r = val_int (Z.rem n₁ n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_mod. Qed.

Lemma triple_le : ∀ n₁ n₂,
  triple (val_le n₁ n₂)
    \[]
    (fun r ⇒ \[r = isTrue (n₁ ≤ n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_le. Qed.

Lemma triple_lt : ∀ n₁ n₂,
  triple (val_lt n₁ n₂)
    \[]
    (fun r ⇒ \[r = isTrue (n₁ < n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_lt. Qed.

Lemma triple_ge : ∀ n₁ n₂,
  triple (val_ge n₁ n₂)
    \[]
    (fun r ⇒ \[r = isTrue (n₁ ≥ n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_ge. Qed.

Lemma triple_gt : ∀ n₁ n₂,
  triple (val_gt n₁ n₂)
    \[]
    (fun r ⇒ \[r = isTrue (n₁ > n₂)]).
Proof using. intros. applys* triple_binop. applys* evalbinop_gt. Qed.

Lemma triple_ptr_add : ∀ p n,
  p + n ≥ 0 →
  triple (val_ptr_add p n)
    \[]
    (fun r ⇒ \[r = val_loc (abs (p + n))]).
Proof using.
  intros. applys* triple_binop. applys* evalbinop_ptr_add.
  { rewrite¬abs_nonneg. }
Qed.

Lemma triple_ptr_add_nat : ∀ p (f:nat),
  triple (val_ptr_add p f)
    \[]
    (fun r ⇒ \[r = val_loc (p +f)%nat]).
Proof using.
  intros. applys triple_conseq triple_ptr_add. { math. } { xsimpl. }
  { xsimpl. intros. subst. fequals.
    applys eq_nat_of_eq_int. rewrite abs_nonneg; math. }
Qed.

Structural Rule for wp

Definition of wp

Definition wp (t:trm) (Q:val →hprop) : hprop :=
fun s ⇒ eval s t Q.

Equivalence between wp and triple

Lemma wp_equiv : ∀ t H Q,
(H ==> wp t Q ) ↔ (triple t H Q ).
Proof using. intros. unfold wp, triple. iff*. Qed.

Consequence rule for wp.

Lemma wp_conseq : ∀ t Q₁ Q₂,
Q₁ ===> Q₂ →
wp t Q₁ ==> wp t Q₂.
Proof using. unfold wp. introv M. intros s Hs. applys* eval_conseq. Qed.

Frame rule for wp.

Lemma wp_frame : ∀ t H Q,
  (wp t Q ) \* H ==> wp t (Q \*+ H).
Proof using.
  intros. unfold wp. intros h HF.
  lets (h₁&h₂&M₁&M₂&MD&MU): hstar_inv (rm HF).
  subst. applys eval_conseq.
  { applys eval_frame M₁ MD. }
  { xsimpl. intros h' →. applys M₂. }
Qed.

Corollaries, including ramified frame rule.

Lemma wp_ramified : ∀ t Q₁ Q₂,
  (wp t Q₁ ) \* (Q₁ \−−∗ Q₂ ) ==> (wp t Q₂ ).
Proof using.
  intros. applys himpl_trans.
  { applys wp_frame. }
  { applys wp_conseq. xsimpl. }
Qed.

Lemma wp_conseq_frame : ∀ t H Q₁ Q₂,
  Q₁ \*+ H ===> Q₂ →
  (wp t Q₁ ) \* H ==> (wp t Q₂ ).
Proof using.
  introv M. rewrite <- qwand_equiv in M. xchange M. applys wp_ramified.
Qed.

Lemma wp_ramified_trans : ∀ t H Q₁ Q₂,
H ==> (wp t Q₁ ) \* (Q₁ \−−∗ Q₂ ) →
H ==> (wp t Q₂ ).
Proof using. introv M. xchange M. applys wp_ramified. Qed.

Weakest-Precondition Style Reasoning Rules for Terms.

Lemma wp_eval_like : ∀ t₁ t₂ Q,
eval_like t₁ t₂ →
wp t₁ Q ==> wp t₂ Q.
Proof using. introv E Hs. applys* E Hs. Qed.

Lemma wp_val : ∀ v Q,
Q v ==> wp (trm_val v) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_val. Qed.

Lemma wp_fun : ∀ x t Q,
Q (val_fun x t) ==> wp (trm_fun x t) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_fun. Qed.

Lemma wp_fix : ∀ f x t Q,
Q (val_fix f x t) ==> wp (trm_fix f x t) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_fix. Qed.

Lemma wp_app_fun : ∀ x v₁ v₂ t₁ Q,
v₁ = val_fun x t₁ →
wp (subst x v₂ t₁) Q ==> wp (trm_app v₁ v₂) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_app_fun. Qed.

Lemma wp_app_fix : ∀ f x v₁ v₂ t₁ Q,
v₁ = val_fix f x t₁ →
wp (subst x v₂ (subst f v₁ t₁)) Q ==> wp (trm_app v₁ v₂) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_app_fix. Qed.

Lemma wp_seq : ∀ t₁ t₂ Q,
wp t₁ (fun r ⇒ wp t₂ Q) ==> wp (trm_seq t₁ t₂) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_seq. Qed.

Lemma wp_let : ∀ x t₁ t₂ Q,
wp t₁ (fun v ⇒ wp (subst x v t₂) Q) ==> wp (trm_let x t₁ t₂) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_let. Qed.

Lemma wp_if : ∀ b t₁ t₂ Q,
wp (if b then t₁ else t₂) Q ==> wp (trm_if b t₁ t₂) Q.
Proof using. unfold wp. intros. intros h K. applys* eval_if. Qed.

Lemma wp_if_case : ∀ b t₁ t₂ Q,
(if b then wp t₁ Q else wp t₂ Q ) ==> wp (trm_if b t₁ t₂) 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)::E₁ ⇒ if var_eq x y
                   then Some v
                   else lookup x E₁
  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)::E₁ ⇒
      let E₁' := rem x E₁ in
      if var_eq x y then E₁' else (y,v)::E₁'
  end.

ctx_disjoint E₁ E₂ asserts that the two contexts have disjoint domains.

Definition ctx_disjoint (E₁ E₂:ctx) : Prop :=
∀ x v₁ v₂, lookup x E₁ = Some v₁ → lookup x E₂ = Some v₂ → False.

ctx_equiv E₁ E₂ asserts that the two contexts bind same keys to same values.

Definition ctx_equiv (E₁ E₂:ctx) : Prop :=
∀ x, lookup x E₁ = lookup x E₂.

Basic properties of context operations follow.

Section CtxOps.

Lemma lookup_app : ∀ E₁ E₂ x,
  lookup x (E₁ ++ E₂) = match lookup x E₁ with
                         | None ⇒ lookup x E₂
                         | Some v ⇒ Some v
                         end.
Proof using.
  introv. induction E₁ as [|(y,w) E₁']; 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 E₁ E₂,
  rem x (E₁ ++ E₂) = rem x E₁ ++ rem x E₂.
Proof using.
  intros. induction E₁ as [|(y,w) E₁']; rew_list; simpl. { auto. }
  { case_var¬. { rew_list. fequals. } }
Qed.

Lemma ctx_equiv_rem : ∀ x E₁ E₂,
  ctx_equiv E₁ E₂ →
  ctx_equiv (rem x E₁) (rem x E₂).
Proof using.
  introv M. unfolds ctx_equiv. intros y.
  do 2 rewrite lookup_rem. case_var¬.
Qed.

Lemma ctx_disjoint_rem : ∀ x E₁ E₂,
  ctx_disjoint E₁ E₂ →
  ctx_disjoint (rem x E₁) (rem x E₂).
Proof using.
  introv D. intros y v₁ v₂ K₁ K₂. rewrite lookup_rem in *.
  case_var¬. applys* D K₁ K₂.
Qed.

Lemma ctx_disjoint_equiv_app : ∀ E₁ E₂,
  ctx_disjoint E₁ E₂ →
  ctx_equiv (E₁ ++ E₂) (E₂ ++ E₁).
Proof using.
  introv D. intros x. do 2 rewrite¬lookup_app.
  case_eq (lookup x E₁); case_eq (lookup x E₂); auto.
  { intros v₂ K₂ v₁ K₁. 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 t₁ ⇒
       trm_fun x (isubst (rem x E) t₁)
  | trm_fix f x t₁ ⇒
       trm_fix f x (isubst (rem x (rem f E)) t₁)
  | trm_if t₀ t₁ t₂ ⇒
       trm_if (isubst E t₀) (isubst E t₁) (isubst E t₂)
  | trm_seq t₁ t₂ ⇒
       trm_seq (isubst E t₁) (isubst E t₂)
  | trm_let x t₁ t₂ ⇒
       trm_let x (isubst E t₁) (isubst (rem x E) t₂)
  | trm_app t₁ t₂ ⇒
       trm_app (isubst E t₁) (isubst E t₂)
  end.

Properties of Multi-Substitution

The goal of this entire section is only to establish isubst_nil and isubst_rem, which assert:
        isubst nil t = t
    and
        isubst ((x,v)::E) t = subst x v (isubst (rem x E) t)

isubst_nil explains that the empty substitution is the identity.

Lemma isubst_nil : ∀ t,
isubst nil t = t.
Proof using. intros t. induction t; simpl; fequals. Qed.

subst_eq_isubst_one relates subst and isubst.

Lemma subst_eq_isubst_one : ∀ x v t,
  subst x v t = isubst ((x ,v )::nil) t.
Proof using.
  intros. induction t; simpl.
  { fequals. }
  { case_var¬. }
  { fequals. case_var¬. { rewrite¬isubst_nil. } }
  { fequals. case_var; try case_var; simpl; try case_var; try rewrite isubst_nil; auto. }
  { fequals*. }
  { fequals*. }
  { fequals*. case_var¬. { rewrite¬isubst_nil. } }
  { fequals*. }
Qed.

The next lemma shows that equivalent contexts produce equal results for isubst.

Lemma isubst_ctx_equiv : ∀ t E₁ E₂,
  ctx_equiv E₁ E₂ →
  isubst E₁ t = isubst E₂ t.
Proof using.
  hint ctx_equiv_rem.
  intros t. induction t; introv EQ; simpl; fequals¬.
  { rewrite¬EQ. }
Qed.

isubst_app asserts that isubst distribute over concatenation.

Lemma isubst_app : ∀ t E₁ E₂,
  isubst (E₁ ++ E₂) t = isubst E₂ (isubst E₁ 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 E₁); introv K₁; case_eq (lookup x E₂); introv K₂; auto.
    { simpl. rewrite¬K₂. }
    { simpl. rewrite¬K₂. } }
  { fequals. rewrite* rem_app. }
  { fequals. do 2 rewrite* rem_app. }
  { fequals*. }
  { fequals*. }
  { fequals*. { rewrite* rem_app. } }
  { fequals*. }
Qed.

isubst_cons is a corollary

Lemma isubst_cons : ∀ x v xvs t,
  isubst ((x ,v )::xvs) t = isubst xvs (subst x v t).
Proof using.
  intros. rewrite <- app_cons_one_r. rewrite isubst_app.
  rewrite* <- subst_eq_isubst_one.
Qed.

The next lemma asserts that the concatenation order is irrelevant in a substitution if the contexts have disjoint domains.

Lemma isubst_app_swap : ∀ t E₁ E₂,
  ctx_disjoint E₁ E₂ →
  isubst (E₁ ++ E₂) t = isubst (E₂ ++ E₁) 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 v₁ v₂ K₁ K₂. simpls. rewrite lookup_rem in K₁. 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 v₁ v₂ K₁ K₂. rew_listx in *. simpls. do 2 rewrite lookup_rem in K₁. 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 : ∀ Q₁ Q₂ F,
(mkstruct F Q₁ ) \* (Q₁ \−−∗ Q₂ ) ==> (mkstruct F Q₂ ).
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 Q₁ Q₂,
  Q₁ ===> Q₂ →
  mkstruct F Q₁ ==> mkstruct F Q₂.
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 : ∀ F₁ F₂ Q,
  (∀ Q, F₁ Q ==> F₂ Q ) →
  mkstruct F₁ Q ==> mkstruct F₂ 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 (F₁ F₂:formula) : formula := fun Q ⇒
F₁ (fun v ⇒ F₂ Q).

Definition wpgen_let (F₁:formula) (F2of:val →formula) : formula := fun Q ⇒
F₁ (fun v ⇒ F2of v Q).

Definition wpgen_if (t:trm) (F₁ F₂:formula) : formula := fun Q ⇒
\∃ (b:bool ), \[t = trm_val (val_bool b)] \* (if b then F₁ Q else F₂ Q ).

Definition wpgen_if_trm (F₀ F₁ F₂:formula) : formula :=
wpgen_let F₀ (fun v ⇒ mkstruct (wpgen_if v F₁ F₂)).

Definition wpgen_app (t:trm) : formula := fun Q ⇒
\∃ H , H \* \[triple t H Q ].

Recursive Definition of wpgen

wpgen E t is structurally recursive on t. Note that this function does not recurse through values. Note also that the context E gets extended when traversing bindings, in the let-binding and the function cases.

Fixpoint wpgen (E:ctx) (t:trm) : formula :=
  mkstruct match t with
  | trm_val v ⇒ wpgen_val v
  | trm_var x ⇒ wpgen_var E x
  | trm_fun x t₁ ⇒ wpgen_fun (fun v ⇒ wpgen ((x,v )::E) t₁)
  | trm_fix f x t₁ ⇒ wpgen_fix (fun vf v ⇒ wpgen ((f,vf )::(x,v )::E) t₁)
  | trm_if t₀ t₁ t₂ ⇒ wpgen_if (isubst E t₀) (wpgen E t₁) (wpgen E t₂)
  | trm_seq t₁ t₂ ⇒ wpgen_seq (wpgen E t₁) (wpgen E t₂)
  | trm_let x t₁ t₂ ⇒ wpgen_let (wpgen E t₁) (fun v ⇒ wpgen ((x,v )::E) t₂)
  | trm_app t₁ t₂ ⇒ wpgen_app (isubst E t)
  end.

Soundness of wpgen

formula_sound t F asserts that, for any Q, the Separation Logic judgment triple (F Q) t Q is valid. In other words, it states that F is a stronger formula than wp t.

The soundness theorem that we are ultimately interested in asserts that formula_sound (isubst E t) (wpgen E t) holds for any E and t.

Definition formula_sound (t:trm) (F:formula) : Prop :=
∀ Q, F Q ==> wp t Q.

Lemma wp_sound : ∀ t,
formula_sound t (wp t).
Proof using. intros. intros Q. applys himpl_refl. Qed.

One soundness lemma for mkstruct.

Lemma mkstruct_wp : ∀ t,
  mkstruct (wp t) = (wp t ).
Proof using.
  intros. applys fun_ext_1. intros Q. applys himpl_antisym.
  { unfold mkstruct. xpull. intros Q'. applys wp_ramified. }
  { applys mkstruct_erase. }
Qed.

Lemma mkstruct_sound : ∀ t F,
  formula_sound t F →
  formula_sound t (mkstruct F).
Proof using.
  introv M. unfolds formula_sound. intros Q'.
  rewrite <- mkstruct_wp. applys* mkstruct_monotone M.
Qed.

One soundness lemma for each term construct.

Lemma wpgen_fail_sound : ∀ t,
formula_sound t wpgen_fail.
Proof using. intros. intros Q. unfold wpgen_fail. xpull. Qed.

Lemma wpgen_val_sound : ∀ v,
formula_sound (trm_val v) (wpgen_val v).
Proof using. intros. intros Q. unfolds wpgen_val. applys wp_val. Qed.

Lemma wpgen_fun_sound : ∀ x t₁ Fof,
  (∀ vx, formula_sound (subst x vx t₁) (Fof vx)) →
  formula_sound (trm_fun x t₁) (wpgen_fun Fof).
Proof using.
  introv M. intros Q. unfolds wpgen_fun. applys himpl_hforall_l (val_fun x t₁).
  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 t₁ Fof,
  (∀ vf vx, formula_sound (subst x vx (subst f vf t₁)) (Fof vf vx)) →
  formula_sound (trm_fix f x t₁) (wpgen_fix Fof).
Proof using.
  introv M. intros Q. unfolds wpgen_fix.
  applys himpl_hforall_l (val_fix f x t₁). xchange hwand_hpure_l.
  { intros. applys himpl_trans_r. { applys* wp_app_fix. } { applys* M. } }
  { applys wp_fix. }
Qed.

Lemma wpgen_seq_sound : ∀ F₁ F₂ t₁ t₂,
  formula_sound t₁ F₁ →
  formula_sound t₂ F₂ →
  formula_sound (trm_seq t₁ t₂) (wpgen_seq F₁ F₂).
Proof using.
  introv S₁ S₂. intros Q. unfolds wpgen_seq. applys himpl_trans wp_seq.
  applys himpl_trans S₁. applys wp_conseq. intros v. applys S₂.
Qed.

Lemma wpgen_let_sound : ∀ F₁ F2of x t₁ t₂,
  formula_sound t₁ F₁ →
  (∀ v, formula_sound (subst x v t₂) (F2of v)) →
  formula_sound (trm_let x t₁ t₂) (wpgen_let F₁ F2of).
Proof using.
  introv S₁ S₂. intros Q. unfolds wpgen_let. applys himpl_trans wp_let.
  applys himpl_trans S₁. applys wp_conseq. intros v. applys S₂.
Qed.

Lemma wpgen_if_sound : ∀ F₁ F₂ t₀ t₁ t₂,
  formula_sound t₁ F₁ →
  formula_sound t₂ F₂ →
  formula_sound (trm_if t₀ t₁ t₂) (wpgen_if t₀ F₁ F₂).
Proof using.
  introv S₁ S₂. intros Q. unfold wpgen_if. xpull. intros b →.
  applys himpl_trans wp_if. case_if. { applys S₁. } { applys S₂. }
Qed.

Lemma wpgen_app_sound : ∀ t,
formula_sound t (wpgen_app t).
Proof using.
intros t Q. unfold wpgen_app. xpull. intros H M. rewrite wp_equiv. apply M.
Qed.

The main inductive proof for the soundness theorem.

Lemma wpgen_sound : ∀ E t,
  formula_sound (isubst E t) (wpgen E t).
Proof using.
  intros. gen E. induction t; intros; simpl;
   try applys mkstruct_sound.
  { applys wpgen_val_sound. }
  { rename v into x. unfold wpgen_var. case_eq (lookup x E).
    { intros v EQ. applys wpgen_val_sound. }
    { intros N. applys wpgen_fail_sound. } }
  { applys wpgen_fun_sound.
    { intros vx. rewrite* <- isubst_rem. } }
  { applys* wpgen_fix_sound.
    { fold isubst. intros vf vx. rewrite* <- isubst_rem_2. } }
  { applys wpgen_app_sound. }
  { applys* wpgen_seq_sound. }
  { rename v into x. applys* wpgen_let_sound.
    { intros v. rewrite* <- isubst_rem. } }
  { applys* wpgen_if_sound. }
Qed.

Lemma himpl_wpgen_wp : ∀ t Q,
wpgen nil t Q ==> wp t Q.
Proof using.
introv M. lets N: (wpgen_sound nil t). rewrite isubst_nil in N. applys* N.
Qed.

The final theorem for closed terms.

Lemma triple_of_wpgen : ∀ t H Q,
  H ==> wpgen nil t Q →
  triple t H Q.
Proof using.
  introv M. rewrite <- wp_equiv. xchange M. applys himpl_wpgen_wp.
Qed.

Practical Proofs

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

Lemmas for Tactics to Manipulate wpgen Formulae

Lemma xstruct_lemma : ∀ F H Q,
H ==> F Q →
H ==> mkstruct F Q.
Proof using. introv M. xchange M. applys mkstruct_erase. Qed.

Lemma xval_lemma : ∀ v H Q,
H ==> Q v →
H ==> wpgen_val v Q.
Proof using. introv M. applys M. Qed.

Lemma xlet_lemma : ∀ H F₁ F2of Q,
H ==> F₁ (fun v ⇒ F2of v Q) →
H ==> wpgen_let F₁ F2of Q.
Proof using. introv M. xchange M. Qed.

Lemma xseq_lemma : ∀ H F₁ F₂ Q,
H ==> F₁ (fun v ⇒ F₂ Q) →
H ==> wpgen_seq F₁ F₂ Q.
Proof using. introv M. xchange M. Qed.

Lemma xif_lemma : ∀ b H F₁ F₂ Q,
  (b = true → H ==> F₁ Q ) →
  (b = false → H ==> F₂ Q ) →
  H ==> wpgen_if b F₁ F₂ Q.
Proof using. introv M₁ M₂. unfold wpgen_if. xsimpl* b. case_if*. Qed.

Lemma xapp_lemma : ∀ t Q₁ H₁ H Q,
  triple t H₁ Q₁ →
  H ==> H₁ \* (Q₁ \−−∗ protect Q ) →
  H ==> wpgen_app t Q.
Proof using.
  introv M W. unfold wpgen_app. xsimpl.
  applys triple_ramified_frame M. applys W.
Qed.

Lemma xfun_spec_lemma : ∀ (S:val →Prop) H Q Fof,
  (∀ vf,
    (∀ vx H' Q', (H' ==> Fof vx Q') → triple (trm_app vf vx) H' Q') →
    S vf ) →
  (∀ vf, S vf → (H ==> Q vf )) →
  H ==> wpgen_fun Fof Q.
Proof using.
  introv M₁ M₂. unfold wpgen_fun. xsimpl. intros vf N.
  applys M₂. applys M₁. 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 xfix_spec_lemma : ∀ (S:val →Prop) H Q Fof,
  (∀ vf,
    (∀ vx H' Q', (H' ==> Fof vf vx Q') → triple (trm_app vf vx) H' Q') →
    S vf ) →
  (∀ vf, S vf → (H ==> Q vf )) →
  H ==> wpgen_fix Fof Q.
Proof using.
  introv M₁ M₂. unfold wpgen_fix. xsimpl. intros vf N.
  applys M₂. applys M₁. introv K. rewrite <- wp_equiv. xchange K. applys N.
Qed.

Lemma xfix_nospec_lemma : ∀ H Q Fof,
  (∀ vf,
     (∀ vx H' Q', (H' ==> Fof vf vx Q') → triple (trm_app vf vx) H' Q') →
     (H ==> Q vf )) →
  H ==> wpgen_fix Fof Q.
Proof using.
  introv M. unfold wpgen_fix. xsimpl. intros vf N. applys M.
  introv K. rewrite <- wp_equiv. xchange K. applys N.
Qed.

Lemma xwp_lemma_fun : ∀ v₁ v₂ x t H Q,
  v₁ = val_fun x t →
  H ==> wpgen ((x ,v₂ )::nil) t Q →
  triple (trm_app v₁ v₂) H Q.
Proof using.
  introv M₁ M₂. rewrite <- wp_equiv. xchange M₂.
  xchange (>> wpgen_sound ((x,v₂)::nil) t Q).
  rewrite <- subst_eq_isubst_one. applys* wp_app_fun.
Qed.

Lemma xwp_lemma_fix : ∀ v₁ v₂ f x t H Q,
  v₁ = val_fix f x t →
  f ≠ x →
  H ==> wpgen ((f ,v₁ )::(x ,v₂ )::nil) t Q →
  triple (trm_app v₁ v₂) H Q.
Proof using.
  introv M₁ N M₂. rewrite <- wp_equiv. xchange M₂.
  xchange (>> wpgen_sound (((f,v₁)::nil) ++ (x,v₂)::nil) t Q).
  rewrite isubst_app. do 2 rewrite <- subst_eq_isubst_one.
  applys* wp_app_fix.
Qed.

Lemma xtriple_lemma : ∀ t H (Q:val →hprop),
  H ==> mkstruct (wpgen_app t) Q →
  triple t H Q.
Proof using.
  introv M. rewrite <- wp_equiv. xchange M. unfold mkstruct, wpgen_app.
  xpull. intros Q' H' N. rewrite <- wp_equiv in N. xchange N.
  applys wp_ramified.
Qed.

Tactics to Manipulate wpgen Formulae

The tactic are presented in chapter WPgen.

Database of hints for xapp.

#[global] Hint Resolve triple_get triple_set triple_ref triple_free : triple.

#[global] Hint Resolve triple_add triple_div triple_neg triple_opp triple_eq
triple_neq triple_sub triple_mul triple_mod triple_le triple_lt
triple_ge triple_gt triple_ptr_add triple_ptr_add_nat : triple.

xstruct removes the leading mkstruct.

Tactic Notation "xstruct" :=
applys xstruct_lemma.

xstruct_if_needed removes the leading mkstruct if there is one.

Tactic Notation "xstruct_if_needed" :=
try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒ xstruct end.

Tactic Notation "xval" :=
xstruct_if_needed; applys xval_lemma.

Tactic Notation "xlet" :=
xstruct_if_needed; applys xlet_lemma.

Tactic Notation "xseq" :=
xstruct_if_needed; applys xseq_lemma.

Tactic Notation "xseq_xlet_if_needed" :=
  try match goal with ⊢ ?H ==> mkstruct ?F ?Q ⇒
  match F with
  | wpgen_seq ?F₁ ?F₂ ⇒ xseq
  | wpgen_let ?F₁ ?F2of ⇒ xlet
  end end.

Tactic Notation "xif" :=
xseq_xlet_if_needed; xstruct_if_needed;
applys xif_lemma; rew_bool_eq.

xapp_try_clear_unit_result implements some post-processing for cleaning up unused variables.

Tactic Notation "xapp_try_clear_unit_result" :=
try match goal with ⊢ val → _ ⇒ intros _ end.

Tactic Notation "xtriple" :=
intros; applys xtriple_lemma.

Tactic Notation "xtriple_if_needed" :=
try match goal with ⊢ triple ?t ?H ?Q ⇒ applys xtriple_lemma end.

xapp_simpl performs the final step of the tactic xapp. It leverages xsimpl_no_cancel_wand tt which is a restricted version of xsimpl that does not attempt to cancel out magic wands.

Lemma xapp_simpl_lemma : ∀ F H Q,
H ==> F Q →
H ==> F Q \* (Q \−−∗ protect Q ).
Proof using. introv M. xchange M. unfold protect. xsimpl. Qed.

Tactic Notation "xapp_simpl" :=
first [ applys xapp_simpl_lemma (* handles specification coming from xfun *)
| xsimpl_no_cancel_wand tt; unfold protect; xapp_try_clear_unit_result ].

Tactic Notation "xapp_pre" :=
xtriple_if_needed; xseq_xlet_if_needed; xstruct_if_needed.

xapp_nosubst E implements the heart of xapp E. If the argument E was always a triple, it would suffice to run applys xapp_lemma E; xapp_simpl. Yet, E might be an specification involving quantifiers. These quantifiers need to be first instantiated. This instantiation is achieved by means of the tactic forwards_nounfold_then offered by the TLC library.

Tactic Notation "xapp_nosubst" constr(E) :=
xapp_pre;
forwards_nounfold_then E ltac:(fun K ⇒ applys xapp_lemma K; xapp_simpl).

xapp_apply_spec implements the heart of xapp, when called without argument. If finds out the specification triple, either in the hint data base named triple, or in the context by looking for an induction hypothesis. Disclaimer: as explained in chapter WPgen, the simple implementation of xapp_apply_spec which we use here does not apply when the specification includes premises that cannot be solved by eauto; it such cases, the tactic xapp E must be called, providing the specification E explicitly. This limitation is overcome using more involved Hint Extern tricks in CFML 2.0.

Tactic Notation "xapp_apply_spec" :=
first [ solve [ eauto with triple ]
| match goal with H: _ ⊢ _ ⇒ eapply H end ].

xapp_nosubst_for_records is place holder for implementing xapp on records. It is implemented further on.

Ltac xapp_nosubst_for_records tt :=
fail.

xapp first calls xtriple if the goal is triple t H Q instead of H ==> wp t Q.

Tactic Notation "xapp_nosubst" :=
  xapp_pre;
  first [ applys xapp_lemma; [ xapp_apply_spec | xapp_simpl ]
        | xapp_nosubst_for_records tt ].

xapp_try_subst checks if the goal is of the form:

either ∀ (r:val), (r = ...) → ...
or ∀ (r:val), ∀ x, (r = ...) → ...

in which case it substitutes r away.

Tactic Notation "xapp_try_subst" :=
  try match goal with
  | ⊢ ∀ (r:val), (r = _) → _ ⇒ intros ? →
  | ⊢ ∀ (r:val), ∀ x, (r = _) → _ ⇒
      let y := fresh x in intros ? y ->; revert y
  end.

Tactic Notation "xapp" constr(E) :=
xapp_nosubst E; xapp_try_subst.

Tactic Notation "xapp" :=
xapp_nosubst; xapp_try_subst.

Tactic Notation "xapp_view" :=
xseq_xlet_if_needed; xstruct_if_needed; applys xapp_lemma.

xapp is essentially equivalent to xapp_view; [ xapp_apply_spec | xapp_simpl ] .

xfun handles local functions, only for functions of one argument.

Tactic Notation "xfun" constr(S) :=
  xseq_xlet_if_needed; xstruct_if_needed;
  first [ applys xfun_spec_lemma S
        | applys xfix_spec_lemma S ].

Tactic Notation "xfun" :=
  xseq_xlet_if_needed; xstruct_if_needed;
  first [ applys xfun_nospec_lemma
        | applys xfix_nospec_lemma ].

xvars may be called for unfolding "program variables as definitions", which take the form Vars.x, and revealing the underlying string.

Tactic Notation "xvars" :=
DefinitionsForVariables.libsepvar_unfold.

xwp_simpl is a specialized version of simpl to be used for getting the function wp to compute properly.

Ltac xwp_simpl :=
  xvars;
  cbn beta delta [
     LibListExec.combine List.combine
     wpgen wpgen_var isubst lookup var_eq
     string_dec string_rec string_rect
     sumbool_rec sumbool_rect
     Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
     Bool.bool_dec bool_rec bool_rect ] iota zeta;
  simpl.

xwp evaluates wpgen for the term appearing in the goal. This implementation of xwp is for functions of arity one only, refined further on for arbitrary arities.

Tactic Notation "xwp_arity_one_only" :=
  intros;
  first [ applys xwp_lemma_fun; [ reflexivity | ]
        | applys xwp_lemma_fix; [ reflexivity | ] ];
  xwp_simpl.

Additional Tooling for xapp

xapp* is a convenient notation for xapp; auto_star. xapp* E is a convenient notation for xapp E; auto_star.

Tactic Notation "xapp" "*" :=
xapp; auto_star.

Tactic Notation "xapp" "*" constr(E) :=
xapp E; auto_star.

xapp_debug is a tactic to help debugging a call to xapp.

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

Notations for Triples and wpgen

Declare Scope wp_scope.

Notation for printing proof obligations arising from wpgen.

Notation "'PRE' H 'CODE' F 'POST' Q" :=
  (H ==> (mkstruct F) Q)
  (at level 8, H at level 0, F, Q at level 0,
   format "'[v' 'PRE' H '/' 'CODE' F '/' 'POST' Q ']'") : wp_scope.

Notation "` F" :=
  (mkstruct F)
  (at level 10,
   format "` F") : wp_scope.

Custom grammar for the display of characteristic formulae.

Declare Custom Entry wp.

Notation "<[ e ]>" :=
e
(at level 0, e custom wp at level 99) : wp_scope.

Notation "` F" :=
  (mkstruct F)
  (in custom wp at level 10,
   format "` F") : wp_scope.

Notation "( x )" :=
  x
  (in custom wp,
   x at level 99) : wp_scope.

Notation "{ x }" :=
  x
  (in custom wp at level 0,
   x constr,
   only parsing) : wp_scope.

Notation "x" :=
  x
  (in custom wp at level 0,
   x constr at level 0) : wp_scope.

Notation "'Fail'" :=
((wpgen_fail))
(in custom wp at level 69) : wp_scope.

Notation "'Val' v" :=
((wpgen_val v))
(in custom wp at level 69) : wp_scope.

Notation "'Let' x ':=' F₁ 'in' F₂" :=
  ((wpgen_let F₁ (fun x ⇒ F₂)))
  (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. *)
   F₁ custom wp at level 99,
   F₂ custom wp at level 99,
   right associativity,
  format "'[v' '[' 'Let' x ':=' F₁ 'in' ']' '/' '[' F₂ ']' ']'") : wp_scope.

Notation "'Seq' F₁ ; F₂" :=
  ((wpgen_seq F₁ F₂))
  (in custom wp at level 68,
   F₁ custom wp at level 99,
   F₂ custom wp at level 99,
   right associativity,
   format "'[v' 'Seq' '[' F₁ ']' ; '/' '[' F₂ ']' ']'") : wp_scope.

Notation "'App' t₀ t₁ .. tn" :=
((wpgen_app (trm_app .. (trm_app t₀ t₁) .. tn)))
  (in custom wp at level 68,
   t₀ constr at level 0,
   t₁ constr at level 0,
   tn constr at level 0)
  : wp_scope.

Notation "'If_' v 'Then' F₁ 'Else' F₂" :=
  ((wpgen_if v F₁ F₂))
  (in custom wp at level 69,
   F₁ custom wp at level 99,
   F₂ custom wp at level 99,
   left associativity,
   format "'[v' '[' 'If_' v 'Then' ']' '/' '[' F₁ ']' '/' 'Else' '/' '[' F₂ ']' ']'") : wp_scope.

Notation "'Fun' x '=>' F₁" :=
  ((wpgen_fun (fun x ⇒ F₁)))
  (in custom wp at level 69,
   x name,
   F₁ custom wp at level 99,
   right associativity,
  format "'[v' '[' 'Fun' x '=>' F₁ ']' ']'") : wp_scope.

Notation "'Fix' vf x '=>' F₁" :=
  ((wpgen_fix (fun vf x ⇒ F₁)))
  (in custom wp at level 69,
   vf name, x name,
   F₁ custom wp at level 99,
   right associativity,
   format "'[v' '[' 'Fix' vf x '=>' F₁ ']' ']'") : 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 "t₁ t₂" := (trm_app t₁ t₂)
  (in custom trm at level 30,
   left associativity,
   only parsing) : trm_scope.

Notation "'if' t₀ 'then' t₁ 'else' t₂" :=
  (trm_if t₀ t₁ t₂)
  (in custom trm at level 69,
   t₀ custom trm at level 99,
   t₁ custom trm at level 99,
   t₂ custom trm at level 99,
   left associativity,
   format "'[v' '[' 'if' t₀ 'then' ']' '/' '[' t₁ ']' '/' 'else' '/' '[' t₂ ']' ']'") : trm_scope.

Notation "'if' t₀ 'then' t₁ 'end'" :=
  (trm_if t₀ t₁ (trm_val val_unit))
  (in custom trm at level 69,
   t₀ custom trm at level 99, (* at level 0 ? *)
   t₁ custom trm at level 99,
   left associativity,
   format "'[v' '[' 'if' t₀ 'then' ']' '/' '[' t₁ ']' '/' 'end' ']'") : trm_scope.

Notation "t₁ ';' t₂" :=
  (trm_seq t₁ t₂)
  (in custom trm at level 68,
   t₂ custom trm at level 99,
   right associativity,
   format "'[v' '[' t₁ ']' ';' '/' '[' t₂ ']' ']'") : trm_scope.

Notation "'let' x '=' t₁ 'in' t₂" :=
  (trm_let x t₁ t₂)
  (in custom trm at level 69,
   x at level 0,
   t₁ custom trm at level 99,
   t₂ custom trm at level 99,
   right associativity,
   format "'[v' '[' 'let' x '=' t₁ 'in' ']' '/' '[' t₂ ']' ']'") : trm_scope.

(* Let-functions *)

Notation "'let' f x₁ '=' t₁ 'in' t₂" :=
  (trm_let f (trm_fun x₁ t₁) t₂)
  (in custom trm at level 69,
   t₁ custom trm,
   t₂ custom trm,
   f, x₁ at level 0,
   format "'let' f x₁ '=' t₁ 'in' t₂") : val_scope.

Notation "'let' f x₁ .. xn '=' t₁ 'in' t₂" :=
  (trm_let f (trm_fun x₁ .. (trm_fun xn t₁) ..) t₂)
  (in custom trm at level 69,
   t₁ custom trm,
   t₂ custom trm,
   f, x₁, xn at level 0,
   format "'let' f x₁ .. xn '=' t₁ 'in' t₂") : val_scope.

Notation "'let' 'rec' f x₁ '=' t₁ 'in' t₂" :=
  (trm_let f (trm_fix f x₁ t₁) t₂)
  (in custom trm at level 69,
   t₁ custom trm,
   t₂ custom trm,
   f, x₁ at level 0,
   format "'let' 'rec' f x₁ '=' t₁ 'in' t₂") : val_scope.

Notation "'let' 'rec' f x₁ x₂ .. xn '=' t₁ 'in' t₂" :=
  (trm_let f (trm_fix f x₁ (trm_fun x₂ .. (trm_fun xn t₁) ..)) t₂)
  (in custom trm at level 69,
   t₁ custom trm,
   t₂ custom trm,
   f, x₁, x₂, xn at level 0,
   format "'let' 'rec' f x₁ x₂ .. xn '=' t₁ 'in' t₂") : val_scope.

(* On-the-fly functions, as values *)

Notation "'fun' x₁ '=>' t" :=
  (val_fun x₁ t)
  (in custom trm at level 69,
   x₁ at level 0,
   t custom trm at level 99,
   format "'fun' x₁ '=>' t") : val_scope.

Notation "'fun' x₁ x₂ .. xn '=>' t" :=
  (val_fun x₁ (trm_fun x₂ .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   x₁, x₂, xn at level 0,
   format "'fun' x₁ x₂ .. xn '=>' t") : val_scope.

Notation "'fix' f x₁ '=>' t" :=
  (val_fix f x₁ t)
  (in custom trm at level 69,
   f, x₁ at level 0,
   t custom trm at level 99,
   format "'fix' f x₁ '=>' t") : val_scope.

Notation "'fix' f x₁ x₂ .. xn '=>' t" :=
  (val_fix f x₁ (trm_fun x₂ .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   f, x₁, x₂, xn at level 0,
   format "'fix' f x₁ x₂ .. xn '=>' t") : val_scope.

(* On-the-fly functions, as terms *)

Notation "'fun_' x₁ '=>' t" :=
  (trm_fun x₁ t)
  (in custom trm at level 69,
   x₁ at level 0,
   t custom trm at level 99,
   format "'fun_' x₁ '=>' t") : trm_scope.

Notation "'fun_' x₁ .. xn '=>' t" :=
  (trm_fun x₁ .. (trm_fun xn t) ..)
  (in custom trm at level 69,
   t custom trm,
   x₁, xn at level 0,
   format "'fun_' x₁ .. xn '=>' t") : trm_scope.

Notation "'fix_' vf x₁ '=>' t" :=
  (trm_fix vf x₁ t)
  (in custom trm at level 69,
   vf, x₁ at level 0,
   t custom trm at level 99,
   format "'fix_' vf x₁ '=>' t") : trm_scope.

Notation "'fix_' vf x₁ x₂ .. xn '=>' t" :=
  (trm_fix vf x₁ (trm_fun x₂ .. (trm_fun xn t) ..))
  (in custom trm at level 69,
   t custom trm,
   vf, x₁, x₂, xn at level 0,
   format "'fix_' vf x₁ x₂ .. xn '=>' t") : trm_scope.

Notation "()" :=
(trm_val val_unit)
(in custom trm at level 0) : trm_scope.

Notation "()" :=
(val_unit)
(at level 0) : val_scope.

Notation for Primitive Operations.

Notation "'ref'" :=
(trm_val (val_prim val_ref))
(in custom trm at level 0, only parsing) : trm_scope.

Notation "'free'" :=
(trm_val (val_prim val_free))
(in custom trm at level 0, only parsing) : trm_scope.

Notation "'not'" :=
(trm_val (val_prim val_neg))
(in custom trm at level 0, only parsing) : trm_scope.

Notation "! t" :=
  (val_get t)
  (in custom trm at level 67,
   t custom trm at level 99) : trm_scope.

Notation "t₁ := t₂" :=
(val_set t₁ t₂)
(in custom trm at level 67) : trm_scope.

Notation "t₁ + t₂" :=
(val_add t₁ t₂)
(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 "t₁ - t₂" :=
(val_sub t₁ t₂)
(in custom trm at level 58) : trm_scope.

Notation "t₁ * t₂" :=
(val_mul t₁ t₂)
(in custom trm at level 57) : trm_scope.

Notation "t₁ / t₂" :=
(val_div t₁ t₂)
(in custom trm at level 57) : trm_scope.

Notation "t₁ 'mod' t₂" :=
(val_mod t₁ t₂)
(in custom trm at level 57) : trm_scope.

Notation "t₁ = t₂" :=
(val_eq t₁ t₂)
(in custom trm at level 58) : trm_scope.

Notation "t₁ <> t₂" :=
(val_neq t₁ t₂)
(in custom trm at level 58) : trm_scope.

Notation "t₁ <= t₂" :=
(val_le t₁ t₂)
(in custom trm at level 60) : trm_scope.

Notation "t₁ < t₂" :=
(val_lt t₁ t₂)
(in custom trm at level 60) : trm_scope.

Notation "t₁ >= t₂" :=
(val_ge t₁ t₂)
(in custom trm at level 60) : trm_scope.

Notation "t₁ > t₂" :=
(val_gt t₁ t₂)
(in custom trm at level 60) : trm_scope.

(* TESTING
Module TestingNotation.
Local Open Scope val_scope.
Local Open Scope trm_scope.

Definition test_app1 t₁ t₂ : trm :=
  <{ t₁ t₂ }>.

Definition test_app2 t₁ t₂ t₃ : trm :=
  <{ t₁ t₂ t₃ }>.

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

Definition test_fun2 x₁ x₂ t : val :=
  <{ fun x₁ x₂ => t }>.

Definition test_fun3 x₁ x₂ x₃ t : val :=
  <{ fun x₁ x₂ x₃ => t }>.

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

Definition test_fix2 f x₁ x₂ t : val :=
  <{ fun f x₁ x₂ => t }>.

Definition test_fix3 f x₁ x₂ x₃ t : val :=
  <{ fun f x₁ x₂ x₃ => t }>.

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

Definition test_trmfun_2 f x₁ x₂ : trm :=
  <{ fun_ f x₁ x₂ => x₁ }>.

Definition test_trmfun_3 f x₁ x₂ x₃ : trm :=
  <{ fun_ f x₁ x₂ x₃ => x₁ }>.

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

Definition test_trmfix2 f x₁ x₂ t : trm :=
  <{ fix_ f x₁ x₂ => t }>.

Definition test_trmfix3 f x₁ x₂ x₃ t : trm :=
  <{ fix_ f x₁ x₂ x₃ => t }>.

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

Definition test_letfun_2 f x₁ x₂ t : trm :=
  <{ let f x₁ x₂ = x₁ in t }>.

Definition test_letfun_3 f x₁ x₂ x₃ t : trm :=
  <{ let f x₁ x₂ x₃ = x₁ in t }>.

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

Definition test_letfix_2 f x₁ x₂ t : trm :=
  <{ let rec f x₁ x₂ = x₁ in t }>.

Definition test_letfix_3 f x₁ x₂ x₃ t : trm :=
  <{ let rec f x₁ x₂ x₃ = x₁ in t }>.

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

End TestingNotation.
*)

Scopes, Coercions and Notations for Concrete Programs

Module ProgramSyntax.

Export NotationForVariables.

Module Vars := DefinitionsForVariables.

Close Scope fmap_scope.
Open Scope string_scope.
Open Scope val_scope.
Open Scope trm_scope.
Open Scope wp_scope.
Coercion string_to_var (x:string) : var := x.

End ProgramSyntax.

Additional Separation Logic Operators

Disjunction: Definition and Properties of hor

Definition hor (H₁ H₂ : hprop) : hprop :=
\∃ (b:bool ), if b then H₁ else H₂.

Lemma hor_sym : ∀ H₁ H₂,
  hor H₁ H₂ = hor H₂ H₁.
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 : ∀ H₁ H₂,
H₁ ==> hor H₁ H₂.
Proof using. intros. unfolds hor. ∃* true. Qed.

Lemma himpl_hor_r_r : ∀ H₁ H₂,
H₂ ==> hor H₁ H₂.
Proof using. intros. unfolds hor. ∃* false. Qed.

Lemma himpl_hor_l : ∀ H₁ H₂ H₃,
  H₁ ==> H₃ →
  H₂ ==> H₃ →
  hor H₁ H₂ ==> H₃.
Proof using.
  introv M₁ M₂. unfolds hor. applys himpl_hexists_l. intros b. case_if*.
Qed.

Lemma triple_hor : ∀ t H₁ H₂ Q,
  triple t H₁ Q →
  triple t H₂ Q →
  triple t (hor H₁ H₂) Q.
Proof using.
  introv M₁ M₂. unfold hor. applys triple_hexists.
  intros b. destruct* b.
Qed.

Conjunction: Definition and Properties of hand

Definition hand (H₁ H₂ : hprop) : hprop :=
\∀ (b:bool ), if b then H₁ else H₂.

Lemma hand_sym : ∀ H₁ H₂,
  hand H₁ H₂ = hand H₂ H₁.
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 : ∀ H₁ H₂,
hand H₁ H₂ ==> H₁.
Proof using. intros. unfolds hand. applys* himpl_hforall_l true. Qed.

Lemma himpl_hand_l_l : ∀ H₁ H₂,
hand H₁ H₂ ==> H₂.
Proof using. intros. unfolds hand. applys* himpl_hforall_l false. Qed.

Lemma himpl_hand_r : ∀ H₁ H₂ H₃,
  H₁ ==> H₂ →
  H₁ ==> H₃ →
  H₁ ==> hand H₂ H₃.
Proof using.
  introv M₁ M₂. unfold hand. applys himpl_hforall_r. intros b. case_if*.
Qed.

Lemma triple_hand_l : ∀ t H₁ H₂ Q,
triple t H₁ Q →
triple t (hand H₁ H₂) Q.
Proof using. introv M₁. unfold hand. applys¬triple_hforall true. Qed.

Lemma triple_hand_r : ∀ t H₁ H₂ Q,
triple t H₂ Q →
triple t (hand H₁ H₂) Q.
Proof using. introv M₁. unfold hand. applys¬triple_hforall false. Qed.

Generalization to N-ary Functions

Smart Constructors for N-ary Functions and Applications

Definition vars : Type := list var.
Definition vals : Type := list val.
Definition trms : Type := list trm.

trm_apps f ts builds the application of the function f to the list of terms ts.

Fixpoint trm_apps (f:trm) (ts:trms) : trm :=
  match ts with
  | nil ⇒ f
  | ti::ts' ⇒ trm_apps (trm_app f ti) ts'
  end.

trm_funs xs t builds a term describing a function that expects arguments with names xs, and that has t for body.

Fixpoint trm_funs (xs:vars) (t:trm) : trm :=
  match xs with
  | nil ⇒ t
  | x₁::xs' ⇒ trm_fun x₁ (trm_funs xs' t)
  end.

val_funs xs t is similar to trm_funs xs t but produces a value.

Definition val_funs (xs:vars) (t:trm) : val :=
  match xs with
  | nil ⇒ arbitrary
  | x₁::xs' ⇒ val_fun x₁ (trm_funs xs' t)
  end.

trm_fixs f xs t builds a term describing a recursive function named f that expects arguments with names xs, and that has t for body.

Definition trm_fixs (f:var) (xs:vars) (t:trm) : trm :=
  match xs with
  | nil ⇒ arbitrary
  | x₁::xs' ⇒ trm_fix f x₁ (trm_funs xs' t)
  end.

val_fixs xs t is similar to trm_fixs xs t but produces a value.

Definition val_fixs (f:var) (xs:vars) (t:trm) : val :=
  match xs with
  | nil ⇒ arbitrary
  | x₁::xs' ⇒ val_fix f x₁ (trm_funs xs' t)
  end.

var_funs xs n asserts that xs is a nonempty list made of n distinct variable names.

Definition var_funs (xs:vars) (n:nat) : Prop :=
     LibList.noduplicates xs
  ∧ length xs = n
  ∧ xs ≠ nil.

trms_vals vs converts a list of values vs into a list of terms made of the corresponding values, each converted using trm_val.

Coercion trms_vals (vs:vals) : trms :=
LibList.map trm_val vs.

Lemma trms_vals_nil :
trms_vals nil = nil.
Proof using. auto. Qed.

Lemma trms_vals_cons : ∀ v vs,
trms_vals (v :: vs) = trm_val v :: trms_vals vs.
Proof using. intros. unfold trms_vals. rew_listx*. Qed.

#[local] Hint Rewrite trms_vals_nil trms_vals_cons : rew_listx.

Evaluation Rules for N-ary Constructs

subst_trm_funs distributes subst over trm_funs.

Lemma subst_trm_funs : ∀ xs x v t₁,
  ¬ mem x xs →
  subst x v (trm_funs xs t₁) = trm_funs xs (subst x v t₁).
Proof using.
  intros xs. induction xs as [|x xs']; introv N.
  { auto. }
  { rew_listx in N. rew_logic in N. destruct N. simpl. case_var. fequals*. }
Qed.

Evaluation rule for reducing trm_funs into val_funs

Lemma eval_like_trm_funs : ∀ xs t₁,
  xs ≠ nil →
  eval_like (val_funs xs t₁) (trm_funs xs t₁).
Proof using.
  introv N M. destruct xs; tryfalse. simpls. inverts M. applys* eval_fun.
Qed.

Auxiliary lemma: evaluation rule for reducing the first argument of a val_funs applied to an argument.

Lemma eval_like_app_val_funs_cons : ∀ x xs t₁ t₀ v,
  eval_like (val_funs (x :: xs) t₁) t₀ →
  ¬ mem x xs →
  xs ≠ nil →
  eval_like (val_funs xs (subst x v t₁)) (t₀ v).
Proof using.
  introv R Nx Hx M. unfolds eval_like. applys eval_app_arg1'.
  { applys R. applys eval_val_minimal. }
  { simpl. intros ? ? (->&->). applys* eval_app_fun.
    rewrite* subst_trm_funs. applys* eval_like_trm_funs. }
Qed.

Auxiliary lemma: evaluation rule for reducing a val_funs applied to its last argument.

Lemma eval_like_app_val_funs_one : ∀ x t₁ t₀ v,
  eval_like ((val_funs (x::nil) t₁)) t₀ →
  eval_like (subst x v t₁) (trm_app t₀ v).
Proof using.
  introv R N. applys eval_app_arg1'.
  { applys R. applys eval_val_minimal. }
  { simpl. intros ? ? (->&->). applys* eval_app_fun. }
Qed.

Evaluation rule for the application of a val_funs with n variables to a list of n values.

Lemma eval_like_trm_apps_funs : ∀ xs t₀ vs t₁,
  eval_like (val_funs xs t₁) t₀ →
  var_funs xs (length vs) →
  eval_like (isubst (combine xs vs) t₁) (trm_apps t₀ (trms_vals vs)).
Proof using.
  introv E (R₁&R₂&R₃). gen t₁ t₀ vs. induction xs; intros.
  { false*. }
  { inverts R₁. destruct vs as [|v vs]; rew_list in *; tryfalse.
    rew_listx. rewrite isubst_cons. simpl.
    tests: (xs = nil).
    { destruct vs as [|]; tryfalse.
      rew_listx. rewrite isubst_nil. simpl.
      applys* eval_like_app_val_funs_one. }
    { applys* IHxs. applys* eval_like_app_val_funs_cons. } }
Qed.

Evaluation rule for application of a recursive n-ary function of the form val_fix f (trm_funs xs t₁) to a list of values of the appropriate length.

Lemma eval_like_trm_apps_fixs : ∀ f xs vs t₁ v₀,
  v₀ = val_fixs f xs t₁ →
  var_funs xs (length vs) →
  ¬ mem f xs →
  xs ≠ nil →
  eval_like (isubst (combine (f::xs) (v₀::vs)) t₁) (trm_apps v₀ (trms_vals vs)).
Proof using.
  introv E F N₁ N₂. rew_listx. rewrite isubst_cons.
  destruct F as (F₁&F₂&F₃).
  destruct xs as [|x xs']; tryfalse.
  destruct vs as [|v vs']; tryfalse.
  tests C: (xs' = nil).
  { destruct vs' as [|]; tryfalse.
    rew_listx. rewrite isubst_cons, isubst_nil. simpl.
    introv M. applys* eval_app_fix. }
  { rew_listx. rewrite isubst_cons. simpl. rew_listx in N₁.
    rew_logic in N₁. destruct N₁ as (Nf&N₁). inverts F₁ as (Fx&F₁).
    applys eval_like_trm_apps_funs.
    { introv M. applys* eval_app_fix.
      inverts M. rewrite* subst_trm_funs. rewrite* subst_trm_funs.
      applys* eval_like_trm_funs. applys* eval_val. }
    { rew_list in F₂. splits*. } }
Qed.

Tooling for N-ary Functions and Applications

var_funs_exec xs n is a computable version of var_funs xs n.

Section Var_funs_exec.
Import LibListExec.RewListExec.

Definition var_funs_exec (xs:vars) (n:nat) : bool :=
     LibListExec.noduplicates var_eq xs
  && (LibNat.beq (LibListExec.length xs) n
  && LibListExec.is_not_nil xs).

Lemma var_funs_exec_eq : ∀ xs (n:nat),
  var_funs_exec xs n = isTrue (var_funs xs n).
Proof using.
  intros. hint var_eq_spec.
  unfold var_funs_exec, var_funs.
  rewrite LibNat.beq_eq. rew_list_exec; auto.
  extens; rew_istrue. splits*.
Qed.

End Var_funs_exec.

trms_to_vals is the reciprocal of trms_vals, in the sense that trms_to_vals ts = Some vs ensurse that ts = trms_vals vs.

Lemma trms_to_vals_spec : ∀ ts vs,
  trms_to_vals ts = Some vs →
  ts = trms_vals vs.
Proof using.
  intros ts. induction ts as [|t ts']; simpl; introv E.
  { inverts E. auto. }
  { destruct t; inverts E as E. cases (trms_to_vals ts') as C; inverts E.
    rename v₀ into vs'. rewrite* (IHts' vs'). }
Qed.

trm_apps_of_trm t is a tactic that takes a term t and returns a corresponding term in the form trm_apps f ts, assuming it is possible.

Ltac trm_apps_of_trm t :=
  let rec aux acc t :=
    match t with
    | trm_app ?t₀ ?t₁ ⇒
        let acc' := constr:(t₁::acc) in
        aux acc' t₀
    | _ ⇒ constr:(trm_apps t acc)
    end in
  aux (@nil trm) t.

Lemma trm_apps_of_trm_demo : ∀ (f x₁ x₂ x₃:trm) H Q,
  triple (f x₁ x₂ x₃) H Q.
Proof using.
  intros.
  match goal with ⊢ triple ?t _ _ ⇒
    let r := trm_apps_of_trm t in
    change t with r end.
Abort.

prove_eq_trm_apps applies to a goal of the form t = trm_apps ?f ?vs, and solve it by instantiating f and vs, assuming it is possible.

Ltac prove_eq_trm_apps :=
  match goal with ⊢ ?t = trm_apps _ _ ⇒
    let r := trm_apps_of_trm t in
    apply (refl_equal r) end.

Lemma prove_eq_trm_apps_demo : ∀ (f x₁ x₂ x₃:trm),
(∀ t ts, f x₁ x₂ x₃ = trm_apps t ts → (t ,ts ) = (t ,ts ) → True ) →
True.
Proof using. intros. eapply H. prove_eq_trm_apps. Abort.

trm_funs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form trm_funs xs t₁, assuming it is possible.

Ltac trm_funs_of_trm t :=
  let rec aux t :=
    match t with
    | trm_fun ?x ?t₁ ⇒
        match aux t₁ with
        | trm_funs ?xs ?t₀ ⇒ constr:(trm_funs (x::xs) t₀)
        | ?t₀ ⇒ constr:(trm_funs (x::nil) t₀)
        end
    | _ ⇒ constr:(t)
    end in
  let t := eval hnf in t in
  aux t.

val_funs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form val_funs xs t₁, assuming it is possible.

Ltac val_funs_of_trm t :=
  let t := eval hnf in t in
  match t with
  | val_fun ?x ?t₁ ⇒
      match trm_funs_of_trm t₁ with
      | trm_funs ?xs ?t₀ ⇒ constr:(val_funs (x::xs) t₀)
      | ?t₀ ⇒ constr:(val_funs (x::nil) t₀)
      end
  | _ ⇒ constr:(t)
  end.

prove_eq_val_funs applies to a goal of the form v = val_funs ?xs ?t₁ and solves it is possible by instantiating xs and t₁

Ltac prove_eq_val_funs :=
  match goal with ⊢ ?t = val_funs _ _ ⇒
    let r := val_funs_of_trm t in
    apply (refl_equal r) end.

Lemma prove_eq_val_funs_demo : ∀ (x₁ x₂:var) (t₀:trm),
(∀ xs t, val_fun x₁ (trm_fun x₂ t₀) = val_funs xs t → (xs ,t ) = (xs ,t ) → True ) →
True.
Proof using. intros. eapply H. prove_eq_val_funs. Abort.

val_fixs_of_trm t is a tactic that takes a term t and returns a corresponding term in the form val_fixs xs t₁, if possible.

Ltac val_fixs_of_trm t :=
  let t := eval hnf in t in
  match t with
  | val_fix ?f ?x ?t₁ ⇒
      match trm_funs_of_trm t₁ with
      | trm_funs ?xs ?t₀ ⇒ constr:(val_fixs f (x::xs) t₀)
      | _ ⇒ constr:(val_fixs f (x::nil) t₁)
      end
  | _ ⇒ constr:(t)
  end.

prove_eq_val_fix_trm_funs applies to a goal of the form v = val_fix ?f (trm_funs ?xs ?t₁) and solves it is possible.

Ltac prove_eq_val_fix_trm_funs :=
  match goal with ⊢ ?t = val_fixs _ _ _ ⇒
    let r := val_fixs_of_trm t in
    apply (refl_equal r) end.

Lemma prove_eq_val_fix_trm_funs_demo : ∀ (x₁ x₂:var) (t₀:trm),
(∀ f xs t, val_fix f x₁ (trm_fun x₂ t₀) = val_fixs f xs t → (f ,xs ,t ) = (f ,xs ,t ) → True ) →
True.
Proof using. intros. eapply H. prove_eq_val_fix_trm_funs. Abort.

Implementation of the Tactic xwp

Lemma xwp_lemma_funs : ∀ t v₀ ts vs xs t₁ H Q,
  t = trm_apps v₀ ts →
  v₀ = val_funs xs t₁ →
  trms_to_vals ts = Some vs →
  var_funs_exec xs (LibList.length vs) →
  H ==> (wpgen (LibListExec.combine xs vs) t₁) Q →
  triple t H Q.
Proof using.
  introv → E M₁ F M₂. rewrite var_funs_exec_eq in F. rew_bool_eq in F.
  lets HL: (proj32 F). rewrite* LibListExec.combine_eq in M₂.
  lets ->: trms_to_vals_spec (rm M₁).
  rewrite <- wp_equiv. xchange (rm M₂). xchange wpgen_sound.
  applys wp_eval_like. applys* eval_like_trm_apps_funs.
  { subst. introv M. applys M. }
Qed.

Lemma xwp_lemma_fixs : ∀ t v₀ ts vs f xs t₁ H Q,
  t = trm_apps v₀ ts →
  v₀ = val_fixs f xs t₁ →
  trms_to_vals ts = Some vs →
  var_funs_exec xs (LibList.length vs) →
  negb (LibListExec.mem var_eq f xs) →
  H ==> (wpgen (LibListExec.combine (f::xs) (v₀::vs)) t₁) Q →
  triple t H Q.
Proof using.
  introv → E M₁ F N₁ M₂. rewrite var_funs_exec_eq in F. rew_bool_eq in F.
  lets HL: (proj32 F). rewrite* LibListExec.combine_eq in M₂; [|rew_list*].
  lets Nxs: (proj33 F). lets ->: trms_to_vals_spec (rm M₁).
  rewrite LibListExec.mem_eq in N₁; [| applys var_eq_spec ]. rew_bool_eq in N₁.
  rewrite <- wp_equiv. xchange (rm M₂). xchange wpgen_sound.
  applys wp_eval_like. applys* eval_like_trm_apps_fixs.
Qed.

Specification of Array Operations

See chapter Array.

Specification of Record Operations

The chapter Struct shows how to these specifications may be realized.

Implicit Types k : nat.

Representation of Records

A field name is implemented as a natural number

Definition field : Type := nat.

A record field is described as the pair of a field and a value stored in that field.

Definition hrecord_field : Type := (field * val).

A record consists of a list of fields.

Definition hrecord_fields : Type := list hrecord_field.

Implicit Types kvs : hrecord_fields.

Record fields syntax, e.g., `{ head := x; tail := q }.

Notation "`{ k₁ := v₁ }" :=
  ((k₁,(v₁:val ))::nil)
  (at level 0, k₁ at level 0, only parsing)
  : val_scope.

Notation "`{ k₁ := v₁ ; k₂ := v₂ }" :=
  ((k₁,(v₁:val ))::(k₂,(v₂:val ))::nil)
  (at level 0, k₁, k₂ at level 0, only parsing)
  : val_scope.

Notation "`{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ }" :=
  ((k₁,(v₁:val ))::(k₂,(v₂:val ))::(k₃,(v₃:val ))::nil)
  (at level 0, k₁, k₂, k₃ at level 0, only parsing)
  : val_scope.

Notation "`{ k₁ := v₁ }" :=
  ((k₁,v₁)::nil)
  (at level 0, k₁ at level 0, only printing)
  : val_scope.

Notation "`{ k₁ := v₁ ; k₂ := v₂ }" :=
  ((k₁,v₁)::(k₂,v₂)::nil)
  (at level 0, k₁, k₂ at level 0, only printing)
  : val_scope.

Notation "`{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ }" :=
  ((k₁,v₁)::(k₂,v₂)::(k₃,v₃)::nil)
  (at level 0, k₁, k₂, k₃ 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 "t₁ '`.' k" :=
(val_get_field k t₁)
(in custom trm at level 56, k at level 0, format "t₁ '`.' 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 "t₁ '`.' k ':=' t₂" :=
  (val_set_field k t₁ t₂)
  (in custom trm at level 56,
   k at level 0, format "t₁ '`.' k ':=' t₂")
   : 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 k₁ k₂ v₁ v₂, written `{ k₁ := v₁ ; k₂ := v₂ }, allocates a record with two fields and initialize the fields.

Parameter val_new_hrecord_2 : ∀ (k₁:field) (k₂:field), val.

Notation "`{ k₁ := v₁ ; k₂ := v₂ }" :=
  (val_new_hrecord_2 k₁ k₂ v₁ v₂)
  (in custom trm at level 65,
   k₁, k₂ at level 0,
   v₁, v₂ at level 65) : trm_scope.

Open Scope trm_scope.

Parameter triple_new_hrecord_2 : ∀ k₁ k₂ v₁ v₂,
  k₁ = 0%nat →
  k₂ = 1%nat →
  triple <{ `{ k₁ := v₁ ; k₂ := v₂ } }>
    \[]
    (funloc p ⇒ p ~~~> `{ k₁ := v₁ ; k₂ := v₂ }).

#[global] Hint Resolve val_new_hrecord_2 : triple.

val_new_record_3 k₁ k₂ k₃ v₁ v₂ v₃, written `{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ }, allocates a record with three fields and initialize the fields.

Parameter val_new_hrecord_3 : ∀ (k₁:field) (k₂:field) (k₃:field), val.

Notation "`{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ }" :=
  (val_new_hrecord_3 k₁ k₂ k₃ v₁ v₂ v₃)
  (in custom trm at level 65,
   k₁, k₂, k₃ at level 0,
   v₁, v₂, v₃ at level 65) : trm_scope.

Parameter triple_new_hrecord_3 : ∀ k₁ k₂ k₃ v₁ v₂ v₃,
  k₁ = 0%nat →
  k₂ = 1%nat →
  k₃ = 2%nat →
  triple <{ `{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ } }>
    \[]
    (funloc p ⇒ p ~~~> `{ k₁ := v₁ ; k₂ := v₂ ; k₃ := v₃ }).

#[global] Hint Resolve val_new_hrecord_3 : triple.

Deallocation of Records

val_dealloc_hrecord p, written delete p, deallocates the record at location p.

Parameter val_dealloc_hrecord : val.

Notation "'delete'" :=
(trm_val val_dealloc_hrecord)
(in custom trm at level 0) : trm_scope.

Parameter triple_dealloc_hrecord : ∀ kvs p,
  triple (val_dealloc_hrecord p)
    (hrecord kvs p)
    (fun _ ⇒ \[]).

#[global] Hint Resolve triple_dealloc_hrecord : triple.

Extending xapp to Support Record Access Operations

The tactic xapp is refined to automatically invoke the lemmas triple_get_field_hrecord and triple_set_field_hrecord.

Parameter xapp_get_field_lemma : ∀ H k p Q,
  H ==> \∃ kvs , (hrecord kvs p ) \*
     match hfields_lookup k kvs with
     | None ⇒ \[False ]
     | Some v ⇒ ((fun r ⇒ \[r = v] \* hrecord kvs p ) \−−∗ protect Q) end →
  H ==> wpgen_app (val_get_field k p) Q.

Parameter xapp_set_field_lemma : ∀ H k p v Q,
  H ==> \∃ kvs , (hrecord kvs p ) \*
     match hfields_update k v kvs with
     | None ⇒ \[False ]
     | Some kvs' ⇒ ((fun _ ⇒ hrecord kvs' p ) \−−∗ protect Q) end →
  H ==> wpgen_app (val_set_field k p v) Q.

Ltac xapp_nosubst_for_records tt ::=
first [ applys xapp_set_field_lemma; xsimpl; simpl; xapp_simpl
| applys xapp_get_field_lemma; xsimpl; simpl; xapp_simpl ].

Extending xsimpl to Simplify Record Equalities

fequals_fields simplifies equalities between values of types hrecord_fields, i.e. list of pairs of field names and values.

Ltac fequals_fields :=
  match goal with
  | ⊢ nil = nil ⇒ reflexivity
  | ⊢ cons _ _ = cons _ _ ⇒ applys args_eq_2; [ fequals | fequals_fields ]
  end.

At this point, the tactic xsimpl is refined to take into account simplifications of predicates of the form p ~~~> kvs. The idea is to find a matching predicate of the form p ~~~> kvs' on the right-hand side of the entailment, then to simplify the list equality kvs = kvs'.

Ltac xsimpl_hook_hrecord p :=
  xsimpl_pick_st ltac:(fun H' ⇒
    match H' with hrecord ?kvs' p ⇒
      constr:(true) end);
  apply xsimpl_lr_cancel_eq;
  [ fequal; first [ reflexivity | try fequals_fields ] | ].

Ltac xsimpl_hook H ::=
  match H with
  | hsingle ?p ?v ⇒ xsimpl_hook_hsingle p
  | hrecord ?kvs ?p ⇒ xsimpl_hook_hrecord p
  end.

Demo Programs

Module DemoPrograms.
Export ProgramSyntax.

Definition and Verification of incr.

Here is an implementation of the increment function, written in A-normal form.

   let incr p =
       let n = !p in
       let m = n + 1 in
       p := m

The notation 'p stands for ("x":var). It is defined in LibSepVar.v.

Definition incr : val :=
  <{ fun 'p ⇒
     let 'n = ! 'p in
     let 'm = 'n + 1 in
     'p := 'm }>.

Here is the Separation Logic triple specifying increment. And the proof follows. Note that the script contains explicit references to the specification lemmas of the functions being called (e.g. triple_get for the get operation). The actual CFML2 setup is able to automatically infer those names.

Lemma triple_incr : ∀ (p:loc) (n:int),
  triple (incr p)
    (p ~~> n)
    (fun _ ⇒ (p ~~> (n +1))).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.

We register this specification so that it may be automatically invoked in further examples.

#[global] Hint Resolve triple_incr : triple.

Alternative definition using variable names without quotes, obtained by importing the module Vars from LibSepVar.v.

Module Export Def_incr. Import Vars.

Definition incr' : val :=
  <{ fun p ⇒
       let n = ! p in
       let m = n + 1 in
       p := m }>.

End Def_incr.

Lemma triple_incr' : ∀ (p:loc) (n:int),
  triple (incr' p)
    (p ~~> n)
    (fun _ ⇒ (p ~~> (n +1))).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.

The Decrement Function

Definition decr : val :=
  <{ fun 'p ⇒
       let 'n = ! 'p in
       let 'm = 'n - 1 in
       'p := 'm }>.

Module Export Def_decr. Import Vars.

Definition decr : val :=
  <{ fun p ⇒
       let n = !p in
       let m = n - 1 in
       p := m }>.

End Def_decr.

Lemma triple_decr : ∀ (p:loc) (n:int),
  triple (trm_app decr p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n -1)).
Proof using.
  xwp. xapp. xapp. xapp. xsimpl*.
Qed.

#[global] Hint Resolve triple_decr : triple.

Definition and Verification of mysucc.

Another example, involving a call to incr.

Module Export Def_mysucc. Import Vars.

Definition mysucc : val :=
  <{ fun n ⇒
       let r = ref n in
       incr r ;
       let x = !r in
       free r ;
       x }>.

End Def_mysucc.

Lemma triple_mysucc : ∀ n,
  triple (trm_app mysucc n)
    \[]
    (fun v ⇒ \[v = n +1]).
Proof using.
  xwp. xapp. intros r. xapp. xapp. xapp. xval. xsimpl. auto.
Qed.

Definition and Verification of myrec.

Another example, involving a function involving 3 arguments, as well as record operations.

let myrec r n₁ n₂ =
r.myfield := r.myfield + n₁ + n₂

Definition myfield : field := 0%nat.

Module Export Def_myrec. Import Vars.

Definition myrec : val :=
  <{ fun p n₁ n₂ ⇒
       let n = (p `.myfield ) in
       let m₁ = n + n₁ in
       let m₂ = m₁ + n₂ in
       p `.myfield := m₂ }>.

Lemma triple_myrec : ∀ (p:loc) (n n₁ n₂:int),
  triple (myrec p n₁ n₂)
    (p ~~~> `{ myfield := n })
    (fun _ ⇒ p ~~~> `{ myfield := (n +n₁ +n₂ ) }).
Proof using.
  xwp. xapp. xapp. xapp. xapp. xsimpl.
Qed.

End Def_myrec.

Definition and Verification of myfun.

Another example involving a local function definition.

Module Export Def_myfun. Import Vars.

Definition myfun : val :=
  <{ fun p ⇒
       let f = (fun_ u ⇒ incr p ) in
       f ();
       f () }>.

End Def_myfun.

Lemma triple_myfun : ∀ (p:loc) (n:int),
  triple (myfun p)
    (p ~~> n)
    (fun _ ⇒ p ~~> (n +2)).
Proof using.
  xwp.
  xfun (fun (f:val) ⇒ ∀ (m:int),
    triple (f ())
      (p ~~> m)
      (fun _ ⇒ p ~~> (m +1))); intros f Hf.
  { intros. applys Hf. clear Hf. xapp. xsimpl. }
  xapp.
  xapp.
  replace (n+1+1) with (n+2); [|math]. xsimpl.
Qed.

Demo of a Function with Multiple Arguments.

Definition project_32 : val :=
<{ fun 'a 'b 'c ⇒ 'b }>.

Lemma triple_project_32 : ∀ (a b c : int),
  triple (project_32 a b c)
    \[]
    (fun r ⇒ \[r = b ]).
Proof using. xwp. xval. xsimpl*. Qed.

Definition project_32_rec : val :=
<{ fix 'f 'a 'b 'c ⇒ if false then 'f 'b end }>.

Lemma triple_project_32_rec : ∀ (a b c : int),
  triple (project_32_rec a b c)
    \[]
    (fun _ ⇒ \[]).
Proof using. xwp. xif; auto_false. intros _. xval. xsimpl. Qed.

End DemoPrograms.

(* 2024-11-04 20:38 *)