# SLFSummaryOverview of the ingredients

Set Implicit Arguments.

From SLF (* Sep *) Require SLFExtra SLFRules SLFWPgen SLFBasic.

Import SLFDirect.

# Motivation for Separation Logic in a proof assistant

We consider a lambda-calculus style programming language. Programs are
represented as terms of type trm, and terms evaluate to values of
type val.
Let us describe the grammar of terms and values, which correspond to
what is called a "deep embedding of the programming language".
The grammar of values includes:
The grammar of terms includes:

- basic values, such as unit, bool, or int,
- locations, of type loc, representing memory addresses as natural numbers,
- (closed) functions (written fun), and recursive functions (written fix),
- primitive operations, either for manipulating the memory state, or for performing arithmetic operations.

- closed values (i.e., values without free variables in them),
- variables, of type var, represented as strings,
- function definitions, which may include free variables in the source code,
- control structures: conditions, sequence, let-bindings,
- and function application.

Definition var : Type := string.

Definition loc : Type := nat.

Inductive val : Type :=

| val_unit : val

| val_bool : bool → val

| val_int : int → val

| val_loc : loc → val

| val_fun : var → trm → val

| val_fix : var → var → trm → val

| val_ref : val

| val_get : val

| val_set : val

| val_free : val

| val_add : val

with trm : Type :=

| trm_val : val → trm

| trm_var : var → trm

| trm_fun : var → trm → trm

| trm_fix : var → var → trm → trm

| trm_app : trm → trm → trm

| trm_seq : trm → trm → trm

| trm_let : var → trm → trm → trm

| trm_if : trm → trm → trm → trm.

End Language.

Consider the following program, which computes the length of a C-style
mutable list. If the pointer p is null, it returns zero, else it
returns one plus the length of the tail. In pseudo-Caml, this reads:

let rec mlength p =

if p == null

then 0

else 1 + mlength p.tail
The corresponding Coq definition using the grammar that we just defined
is as follows.

let rec mlength p =

if p == null

then 0

else 1 + mlength p.tail

Definition mlength : val :=

val_fix "f" "p" (

trm_if (trm_app (trm_app val_eq (trm_var "p")) (val_loc null))

(val_int 0)

(trm_app (trm_app val_add (val_int 1)) (trm_app (trm_var "f")

(trm_app (val_get_field tail) (trm_var "p"))))).

Obviously, we do not wish to manually write programs in this form.
One possibility is to use an external tool, namely a parser, to read
the pseudo-code above, and generate the Coq definition.
Another possibility is to exploit Coq notation and coercions facilities
for writing the program using an ad-hoc program syntax. For example,
the syntax that we consider features quote symbols everywhere to
distinguish between Coq keywords and program keywords, as shown below.

The result is arguably not very pretty, yet very convenient because it
enables presenting demos without a dependency on an external parser.

The semantics of an imperative programming language involves a
description of a memory state. A memory state is described as a finite
map location to values.

Remark: the file Fmap.v provides a formalization of finite maps.
The capture-avoiding substitution (not shown) is defined in a
standard way. subst x v t replaces all occurrences of the variable
x with the value v inside the term t.

The big-step evaluation judgement, written eval s t s' v, asserts
that from the initial state s, the evaluation of the term t
terminates in a final state s', and produces the result v.

A value evaluates to itself.

To evaluate a let-binding let x = t

_{1}in t_{2}in a state s_{1}, first evaluate t_{1}, which produces a state s_{2}and a value v_{1}, then evaluate the result of substituting v_{1}for x in t_{2}to obtain the final result.| eval_let : ∀ s

_{1}s

_{2}s

_{3}x t

_{1}t

_{2}v

_{1}r,

eval s

_{1}t

_{1}s

_{2}v

_{1}→

eval s

_{2}(subst x v

_{1}t

_{2}) s

_{3}r →

eval s

_{1}(trm_let x t

_{1}t

_{2}) s

_{3}r

To evaluate a read operation at a location p, first check that
p indeed belongs to the domain of the state s, then return
the value bound to p in the state s.

...
The other evaluation rules are standard. We omit them here.
Details may be found in SLFRules.v.

## Core Separation Logic predicates

Thereafter, we let H range over heap predicates, and we let
h range over pieces of state.

The 5 most important heap predicates are defined next.
The empty heap predicate, written \[], characterizes an empty
sate.

The pure heap predicate, written [\P], also characterizes an
empty state, but moreover asserts that the proposition P is
true. We will see example usage of this predicate further on.

Definition hpure (P:Prop) : hprop :=

fun h ⇒ (h = Fmap.empty) ∧ P.

Notation "\[ P ]" := (hpure P) (at level 0, format "\[ P ]").

The singleton heap predicate, written p ~~> v, characterizes
a singleton state, that is, a state made of a single memory cell,
at location p, and with contents v.

Definition hsingle (p:loc) (v:val) : hprop :=

fun h ⇒ (h = Fmap.single p v).

Notation "p '~~>' v" := (hsingle p v) (at level 32).

The key Separation Logic operator is the star, a.k.a, separating
conjunction, written H

_{1}\* H_{2}. This predicate characterizes a heap h that decomposes as the union of two disjoints parts: one that satisfies H_{1}, and one that satisfies H_{2}.Definition hstar (H

_{1}H

_{2}: hprop) : hprop :=

fun h ⇒ ∃ h

_{1}h

_{2}, H

_{1}h

_{1}

∧ H

_{2}h

_{2}

∧ Fmap.disjoint h

_{1}h

_{2}

∧ h = Fmap.union h

_{1}h

_{2}.

Notation "H

_{1}'\*' H

_{2}" := (hstar H

_{1}H

_{2}) (at level 41, right associativity).

Finally, the existential quantifier, written \∃ x, H, lifts
the existential quantifier on propositions into an existential
quantifier on predicates. The reader may skip over the technical details
of the corresponding definition, and simply read \∃ as the casual
existential quantifier, simply taking into account that it operates over
the type hprop instead of Prop.

Definition hexists A (J:A→hprop) : hprop :=

fun h ⇒ ∃ x, J x h.

Notation "'\exists' x

_{1}.. xn , H" :=

(hexists (fun x

_{1}⇒ .. (hexists (fun xn ⇒ H)) ..))

(at level 39, x

_{1}binder, H at level 50, right associativity,

format "'[' '\exists' '/ ' x

_{1}.. xn , '/ ' H ']'").

## Order relation on heap predicates: entailment

_{1}==> H

_{2}, asserts that the heap predicate H

_{2}is weaker than the heap predicate H

_{1}, in the sense that any heap h satisfying H

_{1}also satisfies H

_{2}.

Definition himpl (H

_{1}H

_{2}:hprop) : Prop :=

∀ h, H

_{1}h → H

_{2}h.

Notation "H

_{1}==> H

_{2}" := (himpl H

_{1}H

_{2}) (at level 55).

The entailment relation defines an order on the set of heap predicates.
It is reflexive, transitive, and antisymmetric.

Parameter himpl_refl : ∀ H,

H ==> H.

Parameter himpl_trans : ∀ H

_{2}H

_{1}H

_{3},

(H

_{1}==> H

_{2}) →

(H

_{2}==> H

_{3}) →

(H

_{1}==> H

_{3}).

Parameter himpl_antisym : ∀ H

_{1}H

_{2},

(H

_{1}==> H

_{2}) →

(H

_{2}==> H

_{1}) →

H

_{1}= H

_{2}.

The antisymmetry property asserts an equality between two predicates.
It is a direct consequence of a principle called "predicate
extensionality", which asserts that if two predicates yields equivalent
propositions when applied to any argument, then these two predicates
can be considered equal in the logic. The principle of predicate
extensionality comes builtin in several proof assistant. In Coq, it may
be safely added as an axiom.

The ability to write equalities between heap predicates is essential
to concisely state and efficiently exploit the properties of the
Separation Logic operators. These properties are presented next.

## Fundamental properties of the Separation Logic operators

(2) The star operator is commutative.

(3) The empty heap predicate is a neutral for the star.

(4) Existentials can be "extruded" out of stars, that is:
(\∃ x, H

_{1}) \* H_{2}= \∃ x, (H_{1}\* H_{2}). when x does not occur in H_{2}.
(5) The star operator is monotone with respect to entailment.
This rule can be read as follows: if you have to prove an
entailment from H

_{1}\* H_{2}to H_{1}' \* H_{2}, you can cancel out H_{2}on both sides, then there remains to prove that H_{1}entails H_{1}'.Parameter himpl_frame_l : ∀ H

_{2}H

_{1}H

_{1}',

H

_{1}==> H

_{1}' →

(H

_{1}\* H

_{2}) ==> (H

_{1}' \* H

_{2}).

End Hprop.

A precondition H describes an input state. It has type state
to Prop.

A postcondition Q describes not just an output state, but also an
output value. It is thus a binary relation, of type val to state
to Prop.

It is useful to generalize the star operator and the entailment
relation to operate over postconditions.
The operation Q \*+ H denotes the extension of a postcondition
with a heap predicate H.

The entailment relation Q

_{1}===> Q_{2}denotes the entailment between two postconditions, asserting that Q_{1}v entails Q_{2}v for any result value v.Definition qimpl (Q

_{1}Q

_{2}:val→hprop) : Prop :=

∀ (v:val), Q

_{1}v ==> Q

_{2}v.

Notation "Q

_{1}===> Q

_{2}" := (qimpl Q

_{1}Q

_{2}) (at level 55).

The generalization of these two operators to postconditions is
necessary to formally state reasoning rules in a concise way.
That said, in first approximation, one may read \*+ as \*
and read ===> as ==>, to get the intuition for the rules.

A Hoare triple, written hoare t H Q, describes the behavior of
a term t using a precondition H and a postcondition Q that
describe the whole memory state.
In total correctness, such a triple asserts that, for any initial
state s satisfying the precondition, there exists a final state
s' and an output value v such that the term t evaluates to
s' and v, and such that v and s' together satisfy the
postcondition.

Definition hoare (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (s:state), H s →

∃ (s':state) (v:val), eval s t s' v ∧ Q v s'.

A Separation Logic triple, written triple t H Q, describes the
behavior of a term t using a precondition H and a postcondition
Q that describe only a fragemnt of the memory state.
The notion of Separation Logic triple can be derived from that of
a Hoare triple by quantifying over the "rest of the state", described
by a heap predicate H'. This predicate H' appears universally
quantified in the definition shown below.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ (H':hprop), hoare t (H \* H') (Q \*+ H').

For example, using a Separation Logic triple, one may specify
the operation incr p, with a precondition that describes a
singleton heap p ~~> n, and a postcondition that describes
a result value that we ignore (it is unit), and a state
described by p ~~> (n+1).

To establish Separation Logic triples, the program logic includes
three kind of rules:
We next present these three kind of rules.

- structural rules, which do not depend on the programming language,
- one rule for each language construct,
- one rule for each primitive operation.

The rule of consequence is like in Hoare logic. It asserts that one
may strengthen the precondition, or weaken the postcondition.
Observe the use of an entailment between postconditions in the
third premise.

The frame rule is specific to Separation Logic. It asserts that the
precondition and the postcondition may be extended using the star
with an arbitrary heap predicate.
Observe the use of the star operator for postconditions \*+ in
the conclusion.

In addition, two extraction rules are also useful for extracting
pure facts and existential quantifiers out of preconditions.
We'll show further on an example use case.

Parameter triple_hpure : ∀ (P:Prop) t H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Parameter triple_hexists : ∀ (A:Type) (J:A→hprop) t Q,

(∀ (x:A), triple t (J x) Q) →

triple t (\∃ x, J x) Q.

## Reasoning rules for terms, e.g., the rule for sequences

_{1}; t

_{2}. To apply it, one needs to provide a heap predicate H' that describes the state between the evaluation of t

_{1}and that of t

_{2}.

{H} t

_{1}{fun v ⇒ H'} {H'} t

_{2}{Q}

------------------------------------

{H} (t

_{1};t

_{2}) {Q}

_{1}, which is ignored in the semantics.

Parameter hoare_seq : ∀ t

_{1}t

_{2}H Q H',

hoare t

_{1}H (fun v ⇒ H') →

hoare t

_{2}H' Q →

hoare (trm_seq t

_{1}t

_{2}) H Q.

The Separation Logic rule for sequence admits a similar statement,
only using the triple instead of hoare.

Parameter triple_seq : ∀ t

_{1}t

_{2}H Q H',

triple t

_{1}H (fun v ⇒ H') →

triple t

_{2}H' Q →

triple (trm_seq t

_{1}t

_{2}) H Q.

The Separation Logic rule can be proved as a direct consequence of
its Hoare Logic counterpart.
For every other language construct, we have a reasoning rule in
Separation Logic that mimics its counterpart in Hoare Logic.
For details, we refer to SLFRules.v.

Implicit Types p : loc.

Implicit Types v : val.

There remains to describe the rules specifying the behavior of the
primitive operations of the language. We focus here on the primitive
operations that act on the memory state.
The read operation assumes a singleton state described by p ~~> v.
It produces as result a value r, specified in the postcondition to
be equal to v by the pure predicate \[r = v]. The state remains
unchanged, as specified by the second part of the postcondition p ~~> v.

Consider now a write operation that updates a location p with a new
contents v. The precondition, like for a read, requires the location
p to be allocated, with some contents v', described by p ~~> v'.
The postcondition describes the final state as p ~~> v, reflecting the
update to the contents. Note that the postcondition needs not bind a name,
because the result value is unit.

Consider the operation that allocates a new cell with contents v.
The precondition consists of the empty heap predicate \[], reflecting
the fact that this allocation operation can be executed in an empty state.
The postcondition asserts that the result value r is of the form
val_loc p, for some location p, such that p ~~> v describes the
final state.
Observe how the location p is existentially quantified in the
postcondition.

Consider the free operation that deallocates the cell at a location p.
The precondition p ~~> v asserts that the cell is currently allocated,
with some contents v. The postcondition is empty, reflecting for the
fact that the cell is no longer accessible.

The rules presented so far suffice to carry out verification proofs.
To illustrate this claim, consider the increment function, which
augments by one unit the contents of a cell with integer contents.
In OCaml syntax, this function is written:

let incr p =

let n = !p in

let m = n+1 in

p := m
The same function can be defined in the embedded language as follows.

let incr p =

let n = !p in

let m = n+1 in

p := m

Definition incr : val :=

val_fun "p" (

trm_let "n" (trm_app val_get (trm_var "p")) (

trm_let "m" (trm_app (trm_app val_add

(trm_var "n")) (val_int 1)) (

trm_app (trm_app val_set (trm_var "p")) (trm_var "m")))).

Alternatively, it may be written using notations and coercions.

Let us check that the two definitions are indeed equivalent.

The specification of the function incr was presented previously,
as an illustration of a Separation Logic triple.

We next show a detailed proof for this specification. It exploits:

- the structural reasoning rules,
- the reasoning rules for terms,
- the specification of the primitive functions,
- the xsimpl tactic, which provides some degree of automation for simplifying entailments.

Proof using.

intros.

(* unfold the body of the function *)

applys triple_app_fun_direct. simpl.

(* reason about let n = .. *)

applys triple_let.

(* reason about !p *)

{ apply triple_get. }

(* name n' the result of !p *)

intros n'. simpl.

(* substitute away the equality n' = n *)

apply triple_hpure. intros →.

(* reason about let m = .. *)

applys triple_let.

(* apply the frame rule to put aside p ~~> n *)

{ applys triple_conseq_frame.

(* reason about n+1 in the empty state *)

{ applys triple_add. }

(* simplify the entailment *)

{ xsimpl. }

(* check the postcondition *)

{ xsimpl. } }

(* name m' the result of n+1 *)

intros m'. simpl.

(* substitute away the equality m' = m *)

apply triple_hpure. intros →.

(* reason about p := m *)

applys triple_conseq.

{ applys triple_set. }

{ xsimpl. }

{ xsimpl. }

Qed.

This proof script shows that a practical verification proof can
be conducted by applying the reasoning rule of the logic.
At the same time, it appears that manually invoking the rules
in such a way is fairly verbose.
To enhance the user experience and allow for more concise proof
scripts, we need to set up additional infrastructure.
Developing such an infrastructure is the matter of the remaining
of this presentation.

## Notion of characteristic formula

## Oveview of the characteristic formula generator

- First, wpgen should be a function that is recognized by Coq as structurally recursive, and that computes well within Coq.
- Second, the output of wpgen, i.e., the formulae that it produces, should be human readable. Indeed, the formulae are intended to be used in interactive proofs guided by the user.

- To cope with the lack of annotations in the source term, in particular for handling the case of function applications, wpgen leverages the notion of "semantic weakest precondition", a notion defined further on.
- To acccomodate for the frame rule, which is not syntax directed, wpgen integrates a predicate named mkstruct that is introduced at every node of the characteristic formula. This predicate may be used to invoke the frame rule if the user wishes to, otherwise it may be freely discarded from the formula.
- To appear as a structurally-recursive function, wpgen does not compute substitution eagerly using subst, but instead delay the substitutions by accumulating them in a context provided as extra argument to wpgen.
- To ensure a human-readable output, the definition of wpgen features auxiliary definitions, with a set of corresponding notation that enable to display the characteristic formula of a term t in a way that reads almost exactly like the source code of t. This feature will be illustrated through a demo.

The weakest precondition for a term t with respect to a postcondition
Q is written wp t Q. It consists of a heap predicate, of type hprop.

Definition wp (t:trm) (Q:val→hprop) : hprop := ...
The predicate wp t Q is called "weakest precondition" for a combination
of two reasons.
First, it is a valid precondition of a triple for the term t with
postcondition Q.

Definition wp (t:trm) (Q:val→hprop) : hprop := ...

Second, it is the weakest precondition H such that triple t H Q holds,
in the sense that any H satisfying this triple entails wp t Q.

An alternative, equivalent characterization of wp is captured by the
following equivalence, which asserts that H entails wp t Q if and
only if triple t H Q holds.

These two axiomatizations proposed above characterize without ambiguity
the weakest precondition predicate wp. However, they do not guarantee
the existence of such a predicate wp. To remedy the problem, let us
present a third, equivalent characterization of wp, as a direct
definition expressed using the operators of Separation Logic.

At this stage, the details of the definition do not matter much.
All that matters is that wp is well-defined and that one can prove
that this last definition satisfies the properties associated with
the other two characterizations.

## Separation Logic in weakest precondition style

_{1}and producing a postcondition from which I can execute t

_{2}and produce Q, then I have the resources for executing the sequence t

_{1}; t

_{2}and produce Q".

Using wp, the consequence rule reformulates as a monotony
property (a.k.a., covariance property) of the wp predicate.
The corresponding statement, shown below, reads as follows:
"If I have at hand the resources for executing t and producing
Q

_{1}, and besides I know that Q_{1}entails Q_{2}, then I have at hand the resouces for executing t and producing Q_{2}".
Using wp, the frame rule reformulates as an "absorption rule"
for the star. The corresponding statement, shown below, reads
as follows: "If I have on one hand the resources for executing t
and producing Q, and I have in my other hand the resource H,
then I have in my hands the resouces for executing t and
producing both Q and H".

Remark: in the wp presentation, no extraction rule is needed,
because the extraction rules are subsumed by the corresponding
rules on entailment. For example, recall the extraction rule for
pure facts:

This rule, when writing triple t H Q in the form H ==> wp t Q,
becomes a special instance of the rule for extracting pure facts
out of the right-hand side of an entailment:

As first approximation, wpgen t Q is defined as a recursive function
that pattern matches on its argument t, and produces the appropriate
heap predicate in each case. The definitions somewhat mimic the wp-style
reasoning rules. Let us show the first lines of the definition, and
comment them next.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒ \[False]

| trm_app v

| trm_let x t

...

end.
The weakest precondition of a value v with respect to a postcondition
Q is Q v.
The weakest precondition of a free variable x, which corresponds to
a stuck program, is \[False].
For computing wpgen of an application, because we have no specifications
at hand, we just fall back on the notion of semantics weakest precondition.
In other words, when t denotes an application, we define wpgen t just
as wp t. During the course of a proof, the corresponding proof obligation
can be discharged by the user by invoking a specification for the function
being applied.
Last, the weakest precondition of a let-binding mimics the corresponding
reasoning rule in weakest-precondition style. Consider the reasoning rule
wp_let for let-bindings, which generalizes wp_seq shown earlier on.

Fixpoint wpgen (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒ \[False]

| trm_app v

_{1}v_{2}⇒ wp t Q| trm_let x t

_{1}t_{2}⇒ wpgen t_{1}(fun v ⇒ wpgen (subst x v t_{2}) Q)...

end.

Parameter wp_seq : ∀ x t

_{1}t

_{2}Q,

wp t

_{1}(fun v ⇒ wp (subst x v t

_{2}) Q) ==> wp (trm_let x t

_{1}t

_{2}) Q.

The generator wpgen is such that wpgen (trm_let x t

_{1}t_{2}) Q is defined to be wpgen t_{1}(fun v ⇒ wpgen (subst x v t_{2}) Q).## Definition of the characteristic formula generator (2/5)

_{2}), which is not being made to a strict subterm of trm_let x t

_{1}t

_{2}. As a result, Coq would refuse the definition as it stands.

_{1}t

_{2}, we extend the context from E to (x,v)::E. When reaching a variable x, we perform a lookup for x in the context E, to find the value associated with x.

Fixpoint wpgen (E:ctx) (t:trm) (Q:val→hprop) : hprop :=

match t with

| trm_val v ⇒ Q v

| trm_var x ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v

_{2}⇒ wp t Q

| trm_let x t

_{1}t

_{2}⇒ wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

## Definition of the characteristic formula generator (3/5)

Fixpoint wpgen (E:ctx) (t:trm) : (val→hprop)->hprop :=

match t with

| trm_val v ⇒ fun Q ⇒ Q v

| trm_var x ⇒ fun Q ⇒

match lookup x E with

| Some v ⇒ Q v

| None ⇒ \[False]

end

| trm_app v

_{1}v

_{2}⇒ fun Q ⇒ wp (isubst E t) Q

| trm_let x t

_{1}t

_{2}⇒ fun Q ⇒

wpgen E t

_{1}(fun v ⇒ wpgen ((x,v)::E) t

_{2}Q)

...

end.

## Definition of the characteristic formula generator (4/5)

Fixpoint wpgen (E:ctx) (t:trm) : formula :=

match t with

| trm_val v ⇒ wpgen_val v

| trm_var x ⇒ wpgen_var E x

| trm_app t

_{1}t

_{2}⇒ wp t

| trm_let x t

_{1}t

_{2}⇒ wpgen_let (wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

end.

_{1}in F

_{2}be a notation for wpgen_let F

_{1}(fun v ⇒ F

_{2}).

_{1}t

_{2}) displays in the form Let x := F

_{1}in F

_{2}, where F

_{1}and F

_{2}correspond to the wpgen of t

_{1}and t

_{2}, respectively.

## Definition of the characteristic formula generator (5/5)

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

_{1}t

_{2}⇒ wp t

| trm_let x t

_{1}t

_{2}⇒ wpgen_let (wpgen E t

_{1}) (fun v ⇒ wpgen ((x,v)::E) t

_{2})

...

end).

Secondly, mkstruct should enable applying the frame rule and the
consequence rule, by validating the same structural rules as the wp
predicate (namely wp_frame and wp_conseq).

Parameter mkstruct_frame : ∀ (F:formula) H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Parameter mkstruct_conseq : ∀ (F:formula) Q

_{1}Q

_{2},

Q

_{1}===> Q

_{2}→

mkstruct F Q

_{1}==> mkstruct F Q

_{2}.

It really does not matter how mkstruct is defined. All that we care
about is that there exists a predicate mkstruct satisfying the above
three properties.
It turns out that we can exhibit such a predicate. One definition that
works appears below---at this stage, no need to undertand the details.

Definition mkstruct (F:formula) : formula :=

fun (Q:val→hprop) ⇒ \∃ H Q',(F Q') \* H \* \[Q' \*+ H ===> Q].

## Soundness of the characteristic formula generator

For another way to interpret the soundness theorem, recall the
equivalence that characterizes wp.

By exploiting this equivalence, the soundness theorem reformulates as
shown below: to establish a triple of the form triple t H Q, it
suffices to prove that H entails the result of wpgen applied to
t and Q, in the empty context.

The result above is the one that is invoked to begin the proof that
a particular term satisfies its specification. It introduces the
wpgen function, which may be evaluated using the Coq tactic simpl.

# Technical zoom: the magic wand

## Definition of magic wand

_{1}\-* H

_{2}, formalized as hwand H

_{1}H

_{2}.

Definition hwand (H

_{1}H

_{2}:hprop) : hprop := ...

_{1}wand H

_{2}" describes a heap predicate such that, if we augment it with H

_{1}, we obtain H

_{2}. This intuition is captured by the following simplification lemma.

There are several ways to define the magic wand. One possible
definition is the following: it describes some predicate H

_{0}, such that, if we star it with H_{1}, we obtain H_{2}.
It is useful to generalize the magic wand to postconditions,
through a predicate written Q

_{1}\--* Q_{2}. Again, there are several possible definitions. Here is one that is a simple generalization of the previous one.Definition qwand (Q

_{1}Q

_{2}:val→hprop) : hprop :=

\∃ H

_{0}, H

_{0}\* \[ Q

_{1}\*+ H

_{0}===> Q

_{2}].

## Structural rules revisited with the magic wand

Parameter triple_conseq_frame : ∀ H

_{2}H

_{1}Q

_{1}t H Q,

triple t H

_{1}Q

_{1}→

H ==> H

_{1}\* H

_{2}→

Q

_{1}\*+ H

_{2}===> Q →

triple t H Q.

One caveat with this rule is that it requires instantiating H
With the magic wand, we can bypass the problem altogether by
eliminating H
Substituting H

_{2}, the part of the heap being "framed out". Providing H_{2}by hand in the proofs would be way too tedious. Setting up a tactic that computes H_{2}as the difference between H and H_{1}(as suggested by the second premise) would work well in the simples cases, however it becomes very tricky to implement when H contains existential quantifiers. Indeed, one has to figure out which quantifiers should go into H_{1}, and which one should go into H_{2}._{2}. To that end, consider the third premise. It asserts that H_{2}is such that, when added to Q_{1}, yields Q. Thus H_{2}may be expressed as Q_{1}\--* Q, the magic wand between Q_{1}and Q._{2}with Q_{1}\--* Q leads to a more concise and more practical reasoning rule, called the "ramified frame rule".Parameter triple_ramified_frame : ∀ H

_{1}Q

_{1}t H Q,

triple t H

_{1}Q

_{1}→

H ==> H

_{1}\* (Q

_{1}\--* Q) →

triple t H Q.

The idea of the ramified frame rule can also be adapted to the
weakest-precondition style presentation. The resulting rule, shown
below, reads as follows: "If I have at in one hand the resources
for executing t and producing Q

_{1}, and I have in the other hand a resource such that, when adding Q_{1}to it I recover Q_{2}, then I have in my hands the resources for executing t and producing Q_{2}directly."
This rule alone captures, in a very concise statement, all the
structural properties of Separation Logic.

## Verification of the increment function, using x-tactics

- xwp introduces the characteristic formua.
- xapp reasons about an application; the application may be part of a let-binding or a sequence.
- xsimpl simplifies entailments, as already mentioned earlier.

Module ProveIncrWithTactics.

Import SLFExtra SLFProgramSyntax.

Definition incr : val :=

Fun 'p :=

Let 'n := '! 'p in

Let 'm := 'n '+ 1 in

'p ':= 'm.

Lemma triple_incr : ∀ (p:loc) (n:int),

triple (incr p)

(p ~~> n)

(fun _ ⇒ p ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. xsimpl.

Qed.

End ProveIncrWithTactics.

A mutable list cell is a two-cell record, featuring a head field and a
tail field. We define the field indices as follows.

A mutable list consists of a chain of cells, terminated by null.
The heap predicate MList L p describes a list whose head cell is
at location p, and whose elements are described by the list L.
This predicate is defined recursively on the structure of L:

- if L is empty, then p is the null pointer,
- if L is of the form x::L', then the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

Fixpoint MList (L:list val) (p:loc) : hprop :=

match L with

| nil ⇒ \[p = null]

| x::L' ⇒ \∃ q, (p ~~~>`{ head := x; tail := q})

\* (MList L' q)

end.

The following reformulations of the definition are helpful in proofs.

Lemma MList_cons : ∀ p x L',

MList (x::L') p =

\∃ q, (p ~~~>`{ head := x; tail := q}) \* MList L' q.

Proof using. auto. Qed.

Another characterization of MList L p is useful for proofs. Whereas
the original definition is by case analysis on whether L is empty,
the alternative one is by case analysis on whether p is null:
The lemma below is stated using an entailment. The reciprocal entailment
is also true, but we do not need it so we do not bother proving it here.

- if p is null, then L is empty,
- otherwise, L decomposes as x::L', the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

Parameter MList_if : ∀ (p:loc) (L:list val),

(MList L p)

==> (If p = null

then \[L = nil]

else \∃ x q L', \[L = x::L']

\* (p ~~~>`{ head := x; tail := q})

\* (MList L' q)).

(* Proof in SLFBasic. *)

## Verification of in-place concatenation of two mutable lists

_{1}and a list p

_{2}, and updates p

_{1}in place so that its tail gets extended by the cells from p

_{2}.

let rec append p

_{1}p

_{2}=

if p

_{1}.tail == null

then p

_{1}.tail <- p

_{2}

else append p

_{1}.tail p

_{2}

Definition append : val :=

Fix 'f 'p

_{1}'p

_{2}:=

Let 'q

_{1}:= 'p

_{1}'.tail in

Let 'b := ('q

_{1}'= null) in

If_ 'b

Then Set 'p

_{1}'.tail ':= 'p

_{2}

Else 'f 'q

_{1}'p

_{2}.

The append function is specified and verified as follows.

Lemma Triple_append : ∀ (L

_{1}L

_{2}:list val) (p

_{1}p

_{2}:loc),

p

_{1}≠ null →

triple (append p

_{1}p

_{2})

(MList L

_{1}p

_{1}\* MList L

_{2}p

_{2})

(fun _ ⇒ MList (L

_{1}++L

_{2}) p

_{1}).

Proof using.

(* The induction principle provides an hypothesis for the tail of L

_{1},

i.e., for the list L

_{1}' such that the relation list_sub L

_{1}' L

_{1}holds. *)

introv K. gen p

_{1}. induction_wf IH: (@list_sub val) L

_{1}. introv N. xwp.

(* To begin the proof, we reveal the head cell of p

_{1}.

We let q

_{1}denote the tail of p

_{1}, and L

_{1}' the tail of L

_{1}. *)

xchange (MList_if p

_{1}). case_if. xpull. intros x q

_{1}L

_{1}' →.

(* We then reason about the case analysis. *)

xapp. xapp. xif; intros Cq

_{1}.

{ (* If q

_{1}' is null, then L

_{1}' is empty. *)

xchange (MList_if q

_{1}). case_if. xpull. intros →.

(* In this case, we set the pointer, then we fold back the head cell. *)

xapp. xchange <- MList_cons. }

{ (* If q

_{1}' is not null, we reason about the recursive call using

the induction hypothesis, then we fold back the head cell. *)

xapp. xchange <- MList_cons. }

Qed.

End ProveAppend.

# Conclusion

(* 2020-09-03 15:43:11 (UTC+02) *)