# BasicBasic Proofs in Separation Logic

Set Implicit Arguments.

From SLF Require Import LibSepReference.

Import ProgramSyntax DemoPrograms.

Implicit Types n m : int.

Implicit Types p q : loc.

From SLF Require Import LibSepReference.

Import ProgramSyntax DemoPrograms.

Implicit Types n m : int.

Implicit Types p q : loc.

# A First Taste

- "Heap predicates", which are used to describe memory states in Separation Logic.
- "Specification triples", of the form triple t H Q, which relate a term t, a precondition H, and a postcondition Q.
- "Entailment proof obligations", of the form H ==> H' or Q ===> Q', which assert that a pre- or post-condition is weaker than another one.
- "Verification proof obligations", of the form PRE H CODE F POST Q, which internally leverage a form of weakest-precondition.
- Custom proof tactics, called "x-tactics", which are specialized tactics for carrying out the verification proofs.

- p ~~> n, which describes a memory cell at location p with contents n,
- \[], which describes an empty state,
- \[P], which also describes an empty state, and moreover asserts that the proposition P is true,
- H
_{1}\* H_{2}, which describes a state made of two disjoint parts: H_{1}and H_{2}, - \∃ x, H, which is used to quantify variables in postconditions.

- xwp or xtriple to begin a proof,
- xapp to reason about an application,
- xval to reason about a return value,
- xif to reason about a conditional,
- xsimpl to simplify or prove entailments (H ==> H' or Q ===> Q').

- math, which is a variant of lia for proving mathematical goals,
- induction_wf, which sets up proofs by well-founded induction,
- gen, which is a shorthand for generalize dependent, a tactic also useful to set up induction principles.

## The Increment Function

let n = ! p in

let m = n + 1 in

p := m

Definition incr : val :=

<{ fun 'p ⇒

let 'n = ! 'p in

let 'm = 'n + 1 in

'p := 'm }>.

<{ fun 'p ⇒

let 'n = ! 'p in

let 'm = 'n + 1 in

'p := 'm }>.

The quotes that appear in the source code are used to disambiguate
between the keywords and variables associated with the source code,
and those from the corresponding Coq keywords and variables.
The fun keyword should be read like the fun keyword from OCaml.
The specification of incr p, shown below, is expressed using a
"Separation Logic triple". A triple is formally expressed by a proposition
of the form triple t H Q. By convention, we write the precondition H
and the postcondition Q on separate lines.

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

triple (incr p)

(p ~~> n)

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

triple (incr p)

(p ~~> n)

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

Here p denotes the address in memory of the reference cell provided
as argument to the increment function. In technical vocabulary, p
is the "location" of a reference cell. All locations have type loc,
thus the argument p of incr has type loc.
In Separation Logic, the "heap predicate" p ~~> n describes a memory
state in which the contents of the location p is the value n.
In the present example, n denotes an integer value.
The behavior of the operation incr p consists of updating the memory
state by incrementing the contents of the cell at location p, so that
its new contents are n+1. Thus, the memory state posterior to the
increment operation can be described by the heap predicate p ~~> (n+1).
The result value returned by incr p is the unit value, which does not
carry any useful information. In the specification of incr, the
postcondition is of the form fun _ ⇒ ... to indicate that there is
no need to bind a name for the result value.
The general pattern of a specification thus includes:
Note that we have to write p ~~> (n+1) using parentheses around n+1,
because p ~~> n+1 would get parsed as (p ~~> n) + 1.
Our next step is to prove the specification lemma triple_incr which
specifies the behavior of the function incr. We conduct the
verification proof using x-tactics.

- Quantification of the arguments of the functions---here, the variable p.
- Quantification of the "ghost variables" used to describe the input state---here, the variable n.
- The application of the predicate triple to the function application incr p, which is the term being specified by the triple.
- The precondition describing the input state---here, the predicate p ~~> n.
- The postcondition describing both the output value and the output state. The general pattern is fun r ⇒ H', where r names the result and H' describes the final state. Here, the final state is described by p ~~> (n+1).

Proof.

xwp begins the verification proof. The proof obligation is
displayed using the custom notation PRE H CODE F POST Q.
The CODE part does not look very nice, but one should
be able to somehow recognize the body of incr. Indeed,
if we ignore the details and perform the alpha-renaming
from v to n and v

Let' n := (App val_get p) in

Let' m := (App val_add n 1) in

App val_set p m
which is somewhat similar to the original source code.

_{0}to m, the CODE section reads like:Let' n := (App val_get p) in

Let' m := (App val_add n 1) in

App val_set p m

xwp.

The remainder of the proof performs some form of symbolic
execution. One should not attempt to read the full proof
obligation at each step, but instead only look at the current
state, described by the PRE part (here, p ~~> n), and at
the first line only of the CODE part, where one can read
the code of the next operation to reason about.
Each function call is handled using the tactic xapp.
We reason about the operation !p that reads into p;
this read operation returns the value n.

xapp.

We reason about the addition operation n+1.

xapp.

We reason about the update operation p := n+1,
thereby updating the state to p ~~> (n+1).

xapp.

At this stage, the proof obligation takes the form _ ==> _,
which require checking that the final state matches what
is claimed in the postcondition. We discharge it using
the tactic xsimpl.

xsimpl.

Qed.

Qed.

The command below associates the specification lemma triple_incr
with the function incr in a hint database, so that if we subsequently
verify a program that features a call to incr, the xapp tactic
is able to automatically invoke the lemma triple_incr.

Hint Resolve triple_incr : triple.

The proof framework can be used without any knowledge about the
implementation of the notation PRE H CODE F POST Q nor about the
implementation of the x-tactics. Readers with prior experience in
program verification may nevertheless be interested to know that
PRE H CODE F POST Q is defined as the entailment H ==> F Q,
where F is a form of weakest-precondition that describes the
behavior of the code.

## A Function with a Return Value

Definition example_let : val :=

<{ fun 'n ⇒

let 'a = 'n + 1 in

let 'b = 'n - 1 in

'a + 'b }>.

<{ fun 'n ⇒

let 'a = 'n + 1 in

let 'b = 'n - 1 in

'a + 'b }>.

We specify this function using the the triple notation, in the form
triple (example_let n) H (fun r ⇒ H'), where r, of type val,
denotes the output value.
To denote the fact that the input state is empty, we write \[]
in the precondition.
To denote the fact that the output state is empty, we could use \[].
Yet, if we write just fun r ⇒ \[] as postcondition, we would have
said nothing about the output value r produced by a call example_let.
Instead, we would like to specify that the result r is equal to 2*n.
To that end, we write the postcondition fun r ⇒ \[r = 2*n], which
actually stands for fun (r:val) ⇒ [r = val_int (2*n)], where the
coercion [val_int] translates the integer value [2*n] into the
corresponding value of type [val] from the programming language.

Lemma triple_example_let : ∀ (n:int),

triple (example_let n)

\[]

(fun r ⇒ \[r = 2*n]).

triple (example_let n)

\[]

(fun r ⇒ \[r = 2*n]).

The verification proof script is very similar to the previous one.
The x-tactics xapp performs symbolic execution of the code.
Ultimately, we need to check that the expression computed,
(n + 1) + (n - 1), is equal to the specified result, that is, 2*n.
We exploit the TLC tactics math to prove this mathematical result.

Proof.

xwp. xapp. xapp. xapp. xsimpl. math.

Qed.

xwp. xapp. xapp. xapp. xsimpl. math.

Qed.

## The Function quadruple

Definition quadruple : val :=

<{ fun 'n ⇒

let 'm = 'n + 'n in

'm + 'm }>.

<{ fun 'n ⇒

let 'm = 'n + 'n in

'm + 'm }>.

#### Exercise: 1 star, standard, especially useful (triple_quadruple)

Specify and verify the function quadruple to express that it returns 4*n, following the template of triple_example_let.
(* FILL IN HERE *)

☐

☐

## The Function inplace_double

Definition inplace_double : val :=

<{ fun 'p ⇒

let 'n = !'p in

let 'm = 'n + 'n in

'p := 'm }>.

<{ fun 'p ⇒

let 'n = !'p in

let 'm = 'n + 'n in

'p := 'm }>.

#### Exercise: 1 star, standard, especially useful (triple_inplace_double)

Specify and verify the function inplace_double, following the template of triple_incr.
(* FILL IN HERE *)

☐

☐

## Increment of Two References

Definition incr_two : val :=

<{ fun 'p 'q ⇒

incr 'p;

incr 'q }>.

<{ fun 'p 'q ⇒

incr 'p;

incr 'q }>.

The specification of this function takes the form
triple (incr_two p q) H (fun _ ⇒ H'),
where r denotes the result value of type unit.
The precondition describes two references cells: p ~~> n
and q ~~> m. To assert that the two cells are distinct from
each other, we separate their description with the operator \*.
This operator called "separating conjunction" in Separation Logic,
and is also known as the "star" operator. Thus, the precondition
is (p ~~> n) \* (q ~~> m), or simply p ~~> n \* q ~~> m.
The postcondition describes the final state as
is p ~~> (n+1) \* q ~~> (m+1), where the contents of both
cells is increased by one unit compared with the precondition.
The specification triple for incr_two is thus as follows.

Lemma triple_incr_two : ∀ (p q:loc) (n m:int),

triple (incr_two p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> (m+1)).

triple (incr_two p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> (m+1)).

The verification proof follows the usual pattern. Note that,
from here on, we use the command Proof using. instead of
just Proof., to enable asynchronous proof checking, a feature
that allows for faster navigation in scripts when using CoqIDE.

Proof using.

xwp. xapp. xapp. xsimpl.

Qed.

xwp. xapp. xapp. xsimpl.

Qed.

We register the specification triple_incr_two in the
database, to enable reasoning about calls to incr_two.

Hint Resolve triple_incr_two : triple.

## Aliased Arguments

Definition aliased_call : val :=

<{ fun 'p ⇒

incr_two 'p 'p }>.

<{ fun 'p ⇒

incr_two 'p 'p }>.

A call to aliased_call p should increase the contents of p by 2.
This property can be specified as follows.

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

triple (aliased_call p)

(p ~~> n)

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

triple (aliased_call p)

(p ~~> n)

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

If we attempt the proof, we get stuck. Observe how xapp reports its
failure to make progress.

Proof using.

xwp. xapp.

Abort.

xwp. xapp.

Abort.

In the above proof, we get stuck with a proof obligation of the form:
\[] ==> (p ~~> ?m) \* _, which requires showing that
from an empty state one can extract a reference p ~~> ?m
for some integer ?m.
What happened is that when matching the current state p ~~> n
against p ~~> ?n \* p ~~> ?m (which corresponds to the precondition
of triple_incr_two with q = p), the internal simplification tactic
was able to cancel out p ~~> n in both expressions, but then got
stuck with matching the empty state against p ~~> ?m.
The issue here is that the specification triple_incr_two is
specialized for the case of non-aliased references.
It is possible to state and prove an alternative specification for
the function incr_two, to cover the case of aliased arguments.
Its precondition mentions only one reference, p ~~> n, and its
postcondition asserts that its contents gets increased by two units.
This alternative specification can be stated and proved as follows.

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

triple (incr_two p p)

(p ~~> n)

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

Proof using.

xwp. xapp. xapp. xsimpl. math.

Qed.

triple (incr_two p p)

(p ~~> n)

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

Proof using.

xwp. xapp. xapp. xsimpl. math.

Qed.

By exploiting the alternative specification, we are able to verify
the specification of aliased_call p, which invokes incr_two p p.
In order to indicate to the xapp tactic that it should invoke the
lemma triple_incr_two_aliased and not triple_incr_two, we provide that
lemma as argument to xapp, by writing xapp triple_incr_two_aliased.

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

triple (aliased_call p)

(p ~~> n)

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

Proof using.

xwp. xapp triple_incr_two_aliased. xsimpl.

Qed.

triple (aliased_call p)

(p ~~> n)

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

Proof using.

xwp. xapp triple_incr_two_aliased. xsimpl.

Qed.

## A Function that Takes Two References and Increments One

Definition incr_first : val :=

<{ fun 'p 'q ⇒

incr 'p }>.

<{ fun 'p 'q ⇒

incr 'p }>.

We can specify this function by describing its input state
as p ~~> n \* q ~~> m, and describing its output state
as p ~~> (n+1) \* q ~~> m. Formally:

Lemma triple_incr_first : ∀ (p q:loc) (n m:int),

triple (incr_first p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> m).

Proof using.

xwp. xapp. xsimpl.

Qed.

triple (incr_first p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> m).

Proof using.

xwp. xapp. xsimpl.

Qed.

Observe, however, that the second reference plays absolutely
no role in the execution of the function. In fact, we might
equally well have described in the specification only the
existence of the reference that the code actually manipulates.

Lemma triple_incr_first' : ∀ (p q:loc) (n:int),

triple (incr_first p q)

(p ~~> n)

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

Proof using.

xwp. xapp. xsimpl.

Qed.

triple (incr_first p q)

(p ~~> n)

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

Proof using.

xwp. xapp. xsimpl.

Qed.

Interestingly, the specification triple_incr_first, which
mentions the two references, is derivable from the specification
triple_incr_first', which mentions only the first reference.
The proof of this fact uses the tactic xtriple, which turns a
specification triple of the form triple t H Q into the form PRE
H CODE t POST Q, thereby enabling this proof obligation to be
processed by xapp.
Here, we invoke the tactic xapp triple_incr_first', to exploit
the specification triple_incr_first'.

Lemma triple_incr_first_derived : ∀ (p q:loc) (n m:int),

triple (incr_first p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> m).

Proof using.

xtriple. xapp triple_incr_first'. xsimpl.

Qed.

triple (incr_first p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n+1) \* q ~~> m).

Proof using.

xtriple. xapp triple_incr_first'. xsimpl.

Qed.

More generally, in Separation Logic, if a specification triple
holds, then this triple remains valid when we add the same heap
predicate to both the precondition and the postcondition. This is
the "frame" principle, a key modularity feature that we'll come
back to later on in the course.

Definition transfer : val :=

<{ fun 'p 'q ⇒

let 'n = !'p in

let 'm = !'q in

let 's = 'n + 'm in

'p := 's;

'q := 0 }>.

<{ fun 'p 'q ⇒

let 'n = !'p in

let 'm = !'q in

let 's = 'n + 'm in

'p := 's;

'q := 0 }>.

#### Exercise: 1 star, standard, especially useful (triple_transfer)

State and prove a lemma called triple_transfer specifying the behavior of transfer p q in the case where p and q denote two distinct references.
(* FILL IN HERE *)

☐

☐

#### Exercise: 1 star, standard, especially useful (triple_transfer_aliased)

State and prove a lemma called triple_transfer_aliased specifying the behavior of transfer when it is applied twice to the same argument. It should take the form triple (transfer p p) H Q.
(* FILL IN HERE *)

☐

☐

## Specification of Allocation

(* TODO: explain the notation triple <{ vs triple (). *)

Parameter triple_ref : ∀ (v:val),

triple <{ ref v }>

\[]

(fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).

Parameter triple_ref : ∀ (v:val),

triple <{ ref v }>

\[]

(fun r ⇒ \∃ p, \[r = val_loc p] \* p ~~> v).

The pattern fun r ⇒ \∃ p, \[r = val_loc p] \* H) occurs
whenever a function returns a pointer. Thus, this pattern appears
pervasively. To improve concision, we introduce a specific
notation for this pattern, shortening it to funloc p ⇒ H.

Notation "'funloc' p '=>' H" :=

(fun r ⇒ \∃ p, \[r = val_loc p] \* H)

(at level 200, p ident, format "'funloc' p '=>' H").

(fun r ⇒ \∃ p, \[r = val_loc p] \* H)

(at level 200, p ident, format "'funloc' p '=>' H").

Using this notation, the specification triple_ref can be reformulated
more concisely, as follows.

Parameter triple_ref' : ∀ (v:val),

triple <{ ref v }>

\[]

(funloc p ⇒ p ~~> v).

triple <{ ref v }>

\[]

(funloc p ⇒ p ~~> v).

Remark: the CFML tool features a technique that generalizes the
notation funloc to all return types, by leveraging type-classes.
Unfortunately, the use of type-classes involves a number of
technicalities that we wish to avoid in this course. For that
reason, we employ only the funloc notation, and use existential
quantifiers explicitly for other types.

## Allocation of a Reference with Greater Contents

Definition ref_greater : val :=

<{ fun 'p ⇒

let 'n = !'p in

let 'm = 'n + 1 in

ref 'm }>.

<{ fun 'p ⇒

let 'n = !'p in

let 'm = 'n + 1 in

ref 'm }>.

The precondition of ref_greater needs to assert the existence of a cell
p ~~> n. The postcondition of ref_greater should asserts the existence
of two cells, p ~~> n and q ~~> (n+1), where q denotes the
location returned by the function. The postcondition is thus written
funloc q ⇒ p ~~> n \* q ~~> (n+1), which is a shorthand for
fun (r:val) ⇒ \∃ q, \[r = val_loc q] \* p ~~> n \* q ~~> (n+1).
The complete specification of ref_greater is:

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

triple (ref_greater p)

(p ~~> n)

(funloc q ⇒ p ~~> n \* q ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. intros q. xsimpl. auto.

Qed.

☐

triple (ref_greater p)

(p ~~> n)

(funloc q ⇒ p ~~> n \* q ~~> (n+1)).

Proof using.

xwp. xapp. xapp. xapp. intros q. xsimpl. auto.

Qed.

☐

#### Exercise: 2 stars, standard, especially useful (triple_ref_greater_abstract)

State another specification for the function ref_greater, called triple_ref_greater_abstract, with a postcondition that does not reveal the contents of the fresh reference q, but instead only asserts that it is greater than the contents of p. To that end, introduce in the postcondition an existentially quantified variable called m, with m > n.
(* FILL IN HERE *)

☐

☐

## Deallocation in Separation Logic

Definition succ_using_incr_attempt :=

<{ fun 'n ⇒

let 'p = ref 'n in

incr 'p;

! 'p }>.

<{ fun 'n ⇒

let 'p = ref 'n in

incr 'p;

! 'p }>.

The operation succ_using_incr_attempt n admits an empty
precondition, and a postcondition asserting that the final
result is n+1. Yet, if we try to prove this specification,
we get stuck.

Lemma triple_succ_using_incr_attempt : ∀ (n:int),

triple (succ_using_incr_attempt n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. }

Abort.

triple (succ_using_incr_attempt n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. }

Abort.

In the above proof script, we get stuck with the entailment
p ~~> (n+1) ==> \[], which indicates that the current state contains
a reference, whereas the postcondition describes an empty state.
We could attempt to patch the specification to account for the left-over
reference. This yields a provable specification.

Lemma triple_succ_using_incr_attempt' : ∀ (n:int),

triple (succ_using_incr_attempt n)

\[]

(fun r ⇒ \[r = n+1] \* \∃ p, (p ~~> (n+1))).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. }

Qed.

triple (succ_using_incr_attempt n)

\[]

(fun r ⇒ \[r = n+1] \* \∃ p, (p ~~> (n+1))).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. }

Qed.

However, while the above specification is provable, it is not
especially useful, since the piece of postcondition
\∃ p, p ~~> (n+1) is of absolutely no use to the caller
of the function. Worse, the caller will have its
The right solution is to alter the code to free the reference once
it is no longer needed, as shown below. We assume the source language
includes a deallocation operation written free p. (This operation
does not exist in OCaml, but let us nevertheless continue using OCaml
syntax for writing programs.)

*own*state polluted with \∃ p, p ~~> (n+1) and will have no way to get rid of it apart from incorporating it into its own postcondition.
Definition succ_using_incr :=

<{ fun 'n ⇒

let 'p = ref 'n in

incr 'p;

let 'x = ! 'p in

free 'p;

'x }>.

<{ fun 'n ⇒

let 'p = ref 'n in

incr 'p;

let 'x = ! 'p in

free 'p;

'x }>.

This program may now be proved correct with respect to the intended
specification. Observe in particular the last call to xapp below,
which corresponds to the free operation.
The final result is the value of the variable x. To reason about it,
we exploit the tactic xval, as illustrated below.

Lemma triple_succ_using_incr : ∀ n,

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xapp. xval. xsimpl. auto.

Qed.

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xapp. xval. xsimpl. auto.

Qed.

Remark: if we verify programs written in a language equipped with
a garbage collector (like, e.g., OCaml), we need to tweak the
Separation Logic to account for the fact that some heap predicates
can be freely discarded from postconditions. This variant of
Separation Logic will be described in the chapter Affine.

## Combined Reading and Freeing of a Reference

Definition get_and_free : val :=

<{ fun 'p ⇒

let 'v = ! 'p in

free 'p;

'v }>.

<{ fun 'p ⇒

let 'v = ! 'p in

free 'p;

'v }>.

#### Exercise: 2 stars, standard, especially useful (triple_get_and_free)

Prove the correctness of the function get_and_free.
Lemma triple_get_and_free : ∀ p v,

triple (get_and_free p)

(p ~~> v)

(fun r ⇒ \[r = v]).

Proof using. (* FILL IN HERE *) Admitted.

☐

triple (get_and_free p)

(p ~~> v)

(fun r ⇒ \[r = v]).

Proof using. (* FILL IN HERE *) Admitted.

☐

Hint Resolve triple_get_and_free : triple.

## Axiomatization of the Mathematical Factorial Function

Module Import Facto.

Parameter facto : int → int.

Parameter facto_init : ∀ n,

0 ≤ n ≤ 1 →

facto n = 1.

Parameter facto_step : ∀ n,

n > 1 →

facto n = n * (facto (n-1)).

End Facto.

Parameter facto : int → int.

Parameter facto_init : ∀ n,

0 ≤ n ≤ 1 →

facto n = 1.

Parameter facto_step : ∀ n,

n > 1 →

facto n = n * (facto (n-1)).

End Facto.

Note that we have purposely not specified the value of facto on
negative arguments.

## A Partial Recursive Function, Without State

if n ≤ 1 then 1 else n * factorec (n-1)

Definition factorec : val :=

<{ fix 'f 'n ⇒

let 'b = 'n ≤ 1 in

if 'b

then 1

else let 'x = 'n - 1 in

let 'y = 'f 'x in

'n * 'y }>.

<{ fix 'f 'n ⇒

let 'b = 'n ≤ 1 in

if 'b

then 1

else let 'x = 'n - 1 in

let 'y = 'f 'x in

'n * 'y }>.

A call factorec n can be specified as follows:
In case the argument is negative (i.e., n < 0), we have two choices:
Let us follow the second approach, in order to illustrate the
specification of partial functions.
There are two possibilities for expressing the constraint n ≥ 0:
The two presentations are totally equivalent. By convention, we follow
the second presentation, which tends to improve both the readability of
specifications and the conciseness of proof scripts.
The specification of factorec is thus stated as follows.

- the initial state is empty,
- the final state is empty,
- the result value r is such that r = facto n, when n ≥ 0.

- either we explicitly specify that the result is 1 in this case,
- or we rule out this possibility by requiring n ≥ 0.

- either we use as precondition \[n ≥ 0],
- or we place an assumption (n ≥ 0) → _ to the front of the triple, and use an empty precondition, that is, \[].

Lemma triple_factorec : ∀ n,

n ≥ 0 →

triple (factorec n)

\[]

(fun r ⇒ \[r = facto n]).

n ≥ 0 →

triple (factorec n)

\[]

(fun r ⇒ \[r = facto n]).

Let's walk through the proof script in detail, to see in particular
how to set up the induction, how to reason about the recursive call,
and how to deal with the precondition n ≥ 0.

Proof using. unfold factorec.

We set up a proof by induction on n to obtain an induction
hypothesis for the recursive calls. Recursive calls are made
each time on smaller values, and the last recursive call is
made on n = 1. The well-founded relation downto 1 captures
this recursion pattern. The tactic induction_wf is provided
by the TLC library to assist in setting up well-founded inductions.
It is exploited as follows.

intros n. induction_wf IH: (downto 1) n.

Observe the induction hypothesis IH. By unfolding downto
as done in the next step, this hypothesis asserts that the
specification that we are trying to prove already holds for
arguments that are smaller than the current argument n,
and that are greater than or equal to 1.

unfold downto in IH.

We may then begin the interactive verification proof.

intros Hn. xwp.

We reason about the evaluation of the boolean condition n ≤ 1.

xapp.

The result of the evaluation of n ≤ 1 in the source program
is described by the boolean value isTrue (n ≤ 1), which appears
in the CODE section after Ifval. The operation isTrue is
provided by the TLC library as a conversion function from Prop
to bool. The use of such a conversion function (which leverages
classical logic) greatly simplifies the process of automatically
performing substitutions after calls to xapp. We next perform the case analysis on the test n ≤ 1.

xif.

Doing so gives two cases.
In the "then" branch, we can assume n ≤ 1.

{ intros C.

Here, the return value is 1.

xval. xsimpl.

We check that 1 = facto n when n ≤ 1.

rewrite facto_init; math. }

In the "else" branch, we can assume n > 1.

{ intros C.

We reason about the evaluation of n-1

xapp.

We reason about the recursive call, implicitly exploiting
the induction hypothesis IH with n-1.

xapp.

We justify that the recursive call is indeed made on a smaller
argument than the current one, that is, n.

{ math. }

We justify that the recursive call is made to a nonnegative argument,
as required by the specification.

{ math. }

We reason about the multiplication n * facto(n-1).

xapp.

We check that n * facto (n-1) matches facto n.

xsimpl. rewrite (@facto_step n); math. }

Qed.

Qed.

## A Recursive Function with State

if m > 0 then (

incr p;

repeat_incr p (m - 1)

)

_{1}then t

_{2}end. The keyword end avoids ambiguities in cases where this construct is followed by a semi-column.

Definition repeat_incr : val :=

<{ fix 'f 'p 'm ⇒

let 'b = 'm > 0 in

if 'b then

incr 'p;

let 'x = 'm - 1 in

'f 'p 'x

end }>.

<{ fix 'f 'p 'm ⇒

let 'b = 'm > 0 in

if 'b then

incr 'p;

let 'x = 'm - 1 in

'f 'p 'x

end }>.

The specification for repeat_incr p requires that the initial
state contains a reference p with some integer contents n,
that is, p ~~> n. Its postcondition asserts that the resulting
state is p ~~> (n+m), which is the result after incrementing
m times the reference p. Observe that this postcondition is
only valid under the assumption that m ≥ 0.

Lemma triple_repeat_incr : ∀ (m n:int) (p:loc),

m ≥ 0 →

triple (repeat_incr p m)

(p ~~> n)

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

m ≥ 0 →

triple (repeat_incr p m)

(p ~~> n)

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

#### Exercise: 2 stars, standard, especially useful (triple_repeat_incr)

Prove the specification of the function repeat_incr. Hint: the structure of the proof resembles that of triple_factorec'.
Proof using. unfold repeat_incr. (* FILL IN HERE *) Admitted.

☐

☐

Lemma triple_repeat_incr' : ∀ (p:loc) (n m:int),

m ≥ 0 →

triple (repeat_incr p m)

(p ~~> n)

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

Proof using.

(* First, introduces all variables and hypotheses. *)

intros n m Hm.

(* Next, generalize those that are not constant during the recursion. *)

gen n Hm.

(* Then, set up the induction. *)

induction_wf IH: (downto 0) m. unfold downto in IH.

(* Finally, re-introduce the generalized hypotheses. *)

intros.

Abort.

m ≥ 0 →

triple (repeat_incr p m)

(p ~~> n)

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

Proof using.

(* First, introduces all variables and hypotheses. *)

intros n m Hm.

(* Next, generalize those that are not constant during the recursion. *)

gen n Hm.

(* Then, set up the induction. *)

induction_wf IH: (downto 0) m. unfold downto in IH.

(* Finally, re-introduce the generalized hypotheses. *)

intros.

Abort.

## Trying to Prove Incorrect Specifications

Lemma triple_repeat_incr_incorrect : ∀ (p:loc) (n m:int),

triple (repeat_incr p m)

(p ~~> n)

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

Proof using.

intros. revert n. induction_wf IH: (downto 0) m. unfold downto in IH.

intros. xwp. xapp. xif; intros C.

{ (* In the 'then' branch: m > 0 *)

xapp. xapp. xapp. { math. } xsimpl. math. }

{ (* In the 'else' branch: m ≤ 0 *)

xval.

triple (repeat_incr p m)

(p ~~> n)

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

Proof using.

intros. revert n. induction_wf IH: (downto 0) m. unfold downto in IH.

intros. xwp. xapp. xif; intros C.

{ (* In the 'then' branch: m > 0 *)

xapp. xapp. xapp. { math. } xsimpl. math. }

{ (* In the 'else' branch: m ≤ 0 *)

xval.

At this point, we are requested to justify that the current state
p ~~> n matches the postcondition p ~~> (n + m), which
amounts to proving n = n + m.

xsimpl.

Abort.

Abort.

When the specification features the assumption m ≥ 0,
we can prove this equality because the fact that we are
in the else branch means that m ≤ 0, thus m = 0.
However, without the assumption m ≥ 0, the value of
m could very well be negative.
Note that there exists a valid specification for repeat_incr
that does not constrain m but instead specifies that the state
always evolves from p ~~> n to p ~~> (n + max 0 m).
The corresponding proof scripts exploits two properties of the
max function.

Lemma max_l : ∀ n m,

n ≥ m →

max n m = n.

Proof using. introv M. unfold max. case_if; math. Qed.

Lemma max_r : ∀ n m,

n ≤ m →

max n m = m.

Proof using. introv M. unfold max. case_if; math. Qed.

n ≥ m →

max n m = n.

Proof using. introv M. unfold max. case_if; math. Qed.

Lemma max_r : ∀ n m,

n ≤ m →

max n m = m.

Proof using. introv M. unfold max. case_if; math. Qed.

Here is the most general specification for the function
repeat_incr.

Lemma triple_repeat_incr' : ∀ (p:loc) (n m:int),

triple (repeat_incr p m)

(p ~~> n)

(fun _ ⇒ p ~~> (n + max 0 m)).

Proof using.

intros. gen n. induction_wf IH: (downto 0) m.

xwp. xapp. xif; intros C.

{ xapp. xapp. xapp. { math. }

xsimpl. repeat rewrite max_r; math. }

{ xval. xsimpl. rewrite max_l; math. }

Qed.

triple (repeat_incr p m)

(p ~~> n)

(fun _ ⇒ p ~~> (n + max 0 m)).

Proof using.

intros. gen n. induction_wf IH: (downto 0) m.

xwp. xapp. xif; intros C.

{ xapp. xapp. xapp. { math. }

xsimpl. repeat rewrite max_r; math. }

{ xval. xsimpl. rewrite max_l; math. }

Qed.

## A Recursive Function Involving two References

if !q > 0 then (

incr p;

decr q;

step_transfer p q

)

Definition step_transfer :=

<{ fix 'f 'p 'q ⇒

let 'm = !'q in

let 'b = 'm > 0 in

if 'b then

incr 'p;

decr 'q;

'f 'p 'q

end }>.

<{ fix 'f 'p 'q ⇒

let 'm = !'q in

let 'b = 'm > 0 in

if 'b then

incr 'p;

decr 'q;

'f 'p 'q

end }>.

The specification of step_transfer is essentially the same as
that of the function transfer presented previously, the
only difference being that we here assume the contents of q to be
nonnegative.

Lemma triple_step_transfer : ∀ p q n m,

m ≥ 0 →

triple (step_transfer p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n + m) \* q ~~> 0).

m ≥ 0 →

triple (step_transfer p q)

(p ~~> n \* q ~~> m)

(fun _ ⇒ p ~~> (n + m) \* q ~~> 0).

#### Exercise: 2 stars, standard, especially useful (triple_step_transfer)

Verify the function step_transfer. Hint: to set up the induction, follow the pattern shown in the proof of triple_repeat_incr'.
Proof using. (* FILL IN HERE *) Admitted.

☐

☐

# Historical Notes

(* 2021-01-25 13:22 *)