# ReprRepresentation Predicates

Set Implicit Arguments.

From SLF Require Import LibSepReference.

Import ProgramSyntax DemoPrograms.

From SLF Require Import Basic.

Open Scope liblist_scope.

Implicit Types n m : int.

Implicit Types p q s c : loc.

From SLF Require Import LibSepReference.

Import ProgramSyntax DemoPrograms.

From SLF Require Import Basic.

Open Scope liblist_scope.

Implicit Types n m : int.

Implicit Types p q s c : loc.

# First Pass

- xfun to reason about a function definition.
- xchange for exploiting transitivity of ==>.

## Formalization of the List Representation Predicate

Definition head : field := 0%nat.

Definition tail : field := 1%nat.

Definition tail : field := 1%nat.

The heap predicate p ~~~>`{ head := x; tail := q} describes a
record allocated at location p, with a head field storing x
and a tail field storing q.
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 p is not null, 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.

match L with

| nil ⇒ \[p = null]

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

end.

## Alternative Characterizations of MList

Lemma MList_nil : ∀ p,

(MList nil p) = \[p = null].

Proof using. auto. Qed.

Lemma MList_cons : ∀ p x L',

MList (x::L') p =

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

Proof using. auto. Qed.

(MList nil p) = \[p = null].

Proof using. auto. Qed.

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.

Lemma 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 using.

(* Let's prove this result by case analysis on L. *)

intros. destruct L as [|x L'].

{ (* Case L = nil. By definition of MList, we have p = null. *)

xchange MList_nil. intros M.

(* We have to justify L = nil, which is trivial.

The TLC case_if tactic performs a case analysis on the argument

of the first visible if conditional. *)

case_if. xsimpl. auto. }

{ (* Case L = x::L'. *)

(* One possibility is to perform a rewrite operation using MList_cons

on its first occurrence. Then using CFML the tactic xpull to extract

the existential quantifiers out from the precondition:

rewrite MList_cons. xpull. intros q.

A more efficient approach is to use the dedicated CFML tactic xchange,

which is specialized for performing updates in the current state. *)

xchange MList_cons. intros q.

(* Because a record is allocated at location p, the pointer p

cannot be null. The lemma hrecord_not_null allows us to exploit

this property, extracting the hypothesis p ≠ null. We use again

the tactic case_if to simplify the case analysis. *)

xchange hrecord_not_null. intros N. case_if.

(* To conclude, it suffices to correctly instantiate the existential

quantifiers. The tactic xsimpl is able to guess the appropriate

instantiations. *)

xsimpl. auto. }

Qed.

Global Opaque MList.

(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 using.

(* Let's prove this result by case analysis on L. *)

intros. destruct L as [|x L'].

{ (* Case L = nil. By definition of MList, we have p = null. *)

xchange MList_nil. intros M.

(* We have to justify L = nil, which is trivial.

The TLC case_if tactic performs a case analysis on the argument

of the first visible if conditional. *)

case_if. xsimpl. auto. }

{ (* Case L = x::L'. *)

(* One possibility is to perform a rewrite operation using MList_cons

on its first occurrence. Then using CFML the tactic xpull to extract

the existential quantifiers out from the precondition:

rewrite MList_cons. xpull. intros q.

A more efficient approach is to use the dedicated CFML tactic xchange,

which is specialized for performing updates in the current state. *)

xchange MList_cons. intros q.

(* Because a record is allocated at location p, the pointer p

cannot be null. The lemma hrecord_not_null allows us to exploit

this property, extracting the hypothesis p ≠ null. We use again

the tactic case_if to simplify the case analysis. *)

xchange hrecord_not_null. intros N. case_if.

(* To conclude, it suffices to correctly instantiate the existential

quantifiers. The tactic xsimpl is able to guess the appropriate

instantiations. *)

xsimpl. auto. }

Qed.

Global Opaque MList.

## In-place Concatenation of Two Mutable Lists

_{1}and a list p

_{2}, and it updates p

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

_{2}.

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

let 'q

let 'b = ('q

if 'b

then 'p

else 'f 'q

<{ fix 'f 'p

_{1}'p_{2}⇒let 'q

_{1}= 'p_{1}`.tail inlet 'b = ('q

_{1}= null) inif 'b

then 'p

_{1}`.tail := 'p_{2}else 'f 'q

_{1}'p_{2}}>.
The append function is specified and verified as follows. The
proof pattern is representative of that of many list-manipulating
functions, so it is essential that the reader follow through every
step of the proof.

Lemma Triple_append : ∀ (L

p

triple (append p

(MList L

(fun _ ⇒ MList (L

Proof using.

_{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 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. }

Otherwise, 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.

Qed.

Implicit Types x : val.

This section introduces two smart constructors for linked lists,
called mnil and mcons.
The operation mnil() is intended to create an empty list.
Its implementation simply returns the value null. Its
specification asserts that the return value is a pointer p
such that MList nil p holds.

Definition mnil : val :=

<{ fun 'u ⇒

null }>.

Lemma triple_mnil :

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

Proof using. xwp. xval. xchanges* <- (MList_nil null). Qed.

Hint Resolve triple_mnil : triple.

<{ fun 'u ⇒

null }>.

Lemma triple_mnil :

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

Proof using. xwp. xval. xchanges* <- (MList_nil null). Qed.

Hint Resolve triple_mnil : triple.

Observe that the specification triple_mnil does not mention
the null pointer anywhere. This specification may thus be
used to specify the behavior of operations on mutable lists
without having to reveal low-level implementation details that
involve the null pointer.
The operation mcons x q is intended to allocate a fresh list cell,
with x in the head field and q in the tail field. The implementation
of this operation allocates and initializes a fresh record made of
two fields. The allocation operation leverages the New construct, which
is notation for a operation called val_new_hrecord_2, which we here view
as a primitive operation. (The chapter Struct describes an encoding
of this function in terms of the allocation and write operations.)

Definition mcons : val :=

<{ fun 'x 'q ⇒

`{ head := 'x; tail := 'q } }>.

<{ fun 'x 'q ⇒

`{ head := 'x; tail := 'q } }>.

The operation mcons admits two specifications: one that describes only
the fresh record allocated, and one that combines it with a list
representation of the form Mlist q L to produce as postcondition
an extended list of the form Mlist p (x::L).
The first specification is as follows.

Lemma triple_mcons : ∀ x q,

triple (mcons x q)

\[]

(funloc p ⇒ p ~~~> `{ head := x ; tail := q }).

Proof using. xwp. xapp triple_new_hrecord_2; auto. xsimpl*. Qed.

triple (mcons x q)

\[]

(funloc p ⇒ p ~~~> `{ head := x ; tail := q }).

Proof using. xwp. xapp triple_new_hrecord_2; auto. xsimpl*. Qed.

The second specification is derived from the first.

Lemma triple_mcons' : ∀ L x q,

triple (mcons x q)

(MList L q)

(funloc p ⇒ MList (x::L) p).

Proof using.

intros. xtriple. xapp triple_mcons.

intros p. xchange <- MList_cons. xsimpl*.

Qed.

Hint Resolve triple_mcons' : triple.

triple (mcons x q)

(MList L q)

(funloc p ⇒ MList (x::L) p).

Proof using.

intros. xtriple. xapp triple_mcons.

intros p. xchange <- MList_cons. xsimpl*.

Qed.

Hint Resolve triple_mcons' : triple.

## Copy Function for Lists

if p == null

then mnil ()

else mcons (p.head) (mcopy p.tail)

Definition mcopy : val :=

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b

then mnil ()

else

let 'x = 'p`.head in

let 'q = 'p`.tail in

let 'q

mcons 'x 'q

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b

then mnil ()

else

let 'x = 'p`.head in

let 'q = 'p`.tail in

let 'q

_{2}= ('f 'q) inmcons 'x 'q

_{2}}>.
The precondition of mcopy requires a linked list MList L p.
Its postcondition asserts that the function returns a pointer p'
and a list MList L p', in addition to the original list MList L p.
The two lists are totally disjoint and independent, as captured by
the separating conjunction symbol (the star).

Lemma triple_mcopy : ∀ L p,

triple (mcopy p)

(MList L p)

(funloc p' ⇒ (MList L p) \* (MList L p')).

triple (mcopy p)

(MList L p)

(funloc p' ⇒ (MList L p) \* (MList L p')).

The proof script is very similar in structure to the previous ones.
While playing the script, try to spot the places where:

- mnil produces an empty list of the form MList nil p',
- the recursive call produces a list of the form MList L' q',
- mcons produces a list of the form MList (x::L') p'.

Proof using.

intros. gen p. induction_wf IH: list_sub L.

xwp. xapp. xchange MList_if. xif; intros C; case_if; xpull.

{ intros →. xapp. xsimpl*. subst. xchange* <- MList_nil. }

{ intros x q L' →. xapp. xapp. xapp. intros q'.

xapp. intros p'. xchange <- MList_cons. xsimpl*. }

Qed.

intros. gen p. induction_wf IH: list_sub L.

xwp. xapp. xchange MList_if. xif; intros C; case_if; xpull.

{ intros →. xapp. xsimpl*. subst. xchange* <- MList_nil. }

{ intros x q L' →. xapp. xapp. xapp. intros q'.

xapp. intros p'. xchange <- MList_cons. xsimpl*. }

Qed.

## Length Function for Lists

if p == null

then 0

else 1 + mlength p.tail

Definition mlength : val :=

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b

then 0

else (let 'q = 'p`.tail in

let 'n = 'f 'q in

'n + 1) }>.

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b

then 0

else (let 'q = 'p`.tail in

let 'n = 'f 'q in

'n + 1) }>.

#### Exercise: 3 stars, standard, especially useful (triple_mlength)

Prove the correctness of the function mlength.
Lemma triple_mlength : ∀ L p,

triple (mlength p)

(MList L p)

(fun r ⇒ \[r = val_int (length L)] \* (MList L p)).

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

☐

triple (mlength p)

(MList L p)

(fun r ⇒ \[r = val_int (length L)] \* (MList L p)).

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

☐

## Alternative Length Function for Lists

if p == null

then ()

else (incr c; listacc c p.tail)

let mlength' p =

let c = ref 0 in

listacc c p;

!c

Definition acclength : val :=

<{ fix 'f 'c 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

incr 'c;

let 'q = 'p`.tail in

'f 'c 'q

end }>.

Definition mlength' : val :=

<{ fun 'p ⇒

let 'c = ref 0 in

acclength 'c 'p;

get_and_free 'c }>.

<{ fix 'f 'c 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

incr 'c;

let 'q = 'p`.tail in

'f 'c 'q

end }>.

Definition mlength' : val :=

<{ fun 'p ⇒

let 'c = ref 0 in

acclength 'c 'p;

get_and_free 'c }>.

#### Exercise: 3 stars, standard, especially useful (triple_mlength')

Prove the correctness of the function mlength'. Hint: start by stating a lemma triple_acclength expressing the specification of the recursive function acclength. Then, register that specification for subsequent use by xapp using the command Hint Resolve triple_acclength : triple. Finally, complete the proof of the specification triple_mlength'.
(* FILL IN HERE *)

Lemma triple_mlength' : ∀ L p,

triple (mlength' p)

(MList L p)

(fun r ⇒ \[r = val_int (length L)] \* (MList L p)).

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

☐

Lemma triple_mlength' : ∀ L p,

triple (mlength' p)

(MList L p)

(fun r ⇒ \[r = val_int (length L)] \* (MList L p)).

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

☐

## In-Place Reversal Function for Lists

_{1}p

_{2}=

if p

_{2}== null

then p

_{1}

else (let p

_{3}= p

_{2}.tail in

p

_{2}.tail <- p

_{1};

mrev_aux p

_{2}p

_{3})

let mrev p =

mrev_aux p null

Definition mrev_aux : val :=

<{ fix 'f 'p

let 'b = ('p

if 'b

then 'p

else (

let 'p

'p

'f 'p

Definition mrev : val :=

<{ fun 'p ⇒

mrev_aux null 'p }>.

<{ fix 'f 'p

_{1}'p_{2}⇒let 'b = ('p

_{2}= null) inif 'b

then 'p

_{1}else (

let 'p

_{3}= 'p_{2}`.tail in'p

_{2}`.tail := 'p_{1};'f 'p

_{2}'p_{3}) }>.Definition mrev : val :=

<{ fun 'p ⇒

mrev_aux null 'p }>.

#### Exercise: 5 stars, standard, optional (triple_mrev)

Prove the correctness of the functions mrev_aux and mrev.
(* FILL IN HERE *)

Lemma triple_mrev : ∀ L p,

triple (mrev p)

(MList L p)

(funloc q ⇒ MList (rev L) q).

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

☐

Lemma triple_mrev : ∀ L p,

triple (mrev p)

(MList L p)

(funloc q ⇒ MList (rev L) q).

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

☐

Module SizedStack.

In this section, we consider the implementation of a mutable stack with
constant-time access to its size, i.e., to the number of items it stores.
The stack structure consists of a 2-field record, storing a pointer on a
mutable linked list, and an integer storing the length of that list.
The stack implementation exposes a function to create an empty stack, a
function for reading the size, and push and pop methods for operating
at the top of the stack.
type 'a stack = { data : 'a list; size : int }

let create () =

{ data = nil; size = 0 }

let sizeof s =

s.size

let push p x =

s.data <- mcons x s.data;

s.size <- s.size + 1

let pop s =

let p = s.data in

let x = p.head in

let q = p.tail in

delete p;

s.data <- q in

s.size <- s.size - 1;

x
The representation predicate for the stack takes the form Stack L s, where
s denotes the location of the record describing the stack, and where L
denotes the list of items stored in the stack. The underlying mutable list
is described as MList L p, where p is the location p stored in the
first field of the record. The definition of Stack is as follows.

let create () =

{ data = nil; size = 0 }

let sizeof s =

s.size

let push p x =

s.data <- mcons x s.data;

s.size <- s.size + 1

let pop s =

let p = s.data in

let x = p.head in

let q = p.tail in

delete p;

s.data <- q in

s.size <- s.size - 1;

x

Definition data : field := 0%nat.

Definition size : field := 1%nat.

Definition Stack (L:list val) (s:loc) : hprop :=

\∃ p, s ~~~>`{ data := p; size := length L } \* (MList L p).

Definition size : field := 1%nat.

Definition Stack (L:list val) (s:loc) : hprop :=

\∃ p, s ~~~>`{ data := p; size := length L } \* (MList L p).

Observe that the predicate Stack does not expose the address of the
mutable list; this adress is existentially quantified in the definition.
The predicate Stack also does not expose the size of the stack, as this
value can be deduced as length L.

Definition create : val :=

<{ fun 'u ⇒

`{ data := null; size := 0 } }>.

Lemma triple_create :

triple (create ())

\[]

(funloc s ⇒ Stack nil s).

Proof using.

xwp. xapp triple_new_hrecord_2; auto. intros s.

unfold Stack. xsimpl*. xchange* <- (MList_nil null).

Qed.

<{ fun 'u ⇒

`{ data := null; size := 0 } }>.

Lemma triple_create :

triple (create ())

\[]

(funloc s ⇒ Stack nil s).

Proof using.

xwp. xapp triple_new_hrecord_2; auto. intros s.

unfold Stack. xsimpl*. xchange* <- (MList_nil null).

Qed.

The sizeof operation returns the contents of the size field of a
stack.

Definition sizeof : val :=

<{ fun 'p ⇒

'p`.size }>.

Lemma triple_sizeof : ∀ L s,

triple (sizeof s)

(Stack L s)

(fun r ⇒ \[r = length L] \* Stack L s).

Proof using.

xwp. unfold Stack. xpull. intros p. xapp. xsimpl*.

Qed.

<{ fun 'p ⇒

'p`.size }>.

Lemma triple_sizeof : ∀ L s,

triple (sizeof s)

(Stack L s)

(fun r ⇒ \[r = length L] \* Stack L s).

Proof using.

xwp. unfold Stack. xpull. intros p. xapp. xsimpl*.

Qed.

The push operation extends the head of the list, and increments the size
field.

Definition push : val :=

<{ fun 's 'x ⇒

let 'p = 's`.data in

let 'p

's`.data := 'p

let 'n = 's`.size in

let 'n

's`.size := 'n

<{ fun 's 'x ⇒

let 'p = 's`.data in

let 'p

_{2}= mcons 'x 'p in's`.data := 'p

_{2};let 'n = 's`.size in

let 'n

_{2}= 'n + 1 in's`.size := 'n

_{2}}>.#### Exercise: 3 stars, standard, especially useful (triple_push)

Prove the following specification for the push operation.
Lemma triple_push : ∀ L s x,

triple (push s x)

(Stack L s)

(fun u ⇒ Stack (x::L) s).

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

☐

triple (push s x)

(Stack L s)

(fun u ⇒ Stack (x::L) s).

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

☐

Definition pop : val :=

<{ fun 's ⇒

let 'p = 's`.data in

let 'x = 'p`.head in

let 'p

delete 'p;

's`.data := 'p

let 'n = 's`.size in

let 'n

's`.size := 'n

'x }>.

<{ fun 's ⇒

let 'p = 's`.data in

let 'x = 'p`.head in

let 'p

_{2}= 'p`.tail indelete 'p;

's`.data := 'p

_{2};let 'n = 's`.size in

let 'n

_{2}= 'n - 1 in's`.size := 'n

_{2};'x }>.

#### Exercise: 4 stars, standard, especially useful (triple_pop)

Prove the following specification for the pop operation.
Lemma triple_pop : ∀ L s,

L ≠ nil →

triple (pop s)

(Stack L s)

(fun x ⇒ \∃ L', \[L = x::L'] \* Stack L' s).

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

☐

L ≠ nil →

triple (pop s)

(Stack L s)

(fun x ⇒ \∃ L', \[L = x::L'] \* Stack L' s).

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

☐

End SizedStack.

## Formalization of the Tree Representation Predicate

_{1}T

_{2}, where n is an integer and T

_{1}and T

_{2}denote the two subtrees. A leaf is represented by the constructor Leaf.

Inductive tree : Type :=

| Leaf : tree

| Node : int → tree → tree → tree.

Implicit Types T : tree.

| Leaf : tree

| Node : int → tree → tree → tree.

Implicit Types T : tree.

A mutable tree node consists of a three-cell record, featuring an field
storing an integer named "item", and two pointers named "left" and "right",
denoting the pointers to the left and right subtrees, respectively.

Definition item : field := 0%nat.

Definition left : field := 1%nat.

Definition right : field := 2%nat.

Definition left : field := 1%nat.

Definition right : field := 2%nat.

The heap predicate p ~~~>`{ item := n; left := p
The representation predicate MTree T p, of type hprop, asserts that
the mutable tree structure with root at location p describes the logical
tree T. The predicate is defined recursively on the structure of T:

_{1}; right := p_{2}} describes a record allocated at location p, describing a node storing the integer n, with its two subtrees at locations p_{1}and p_{2}. An empty tree is represented using the null pointer.- if T is a Leaf, then p is the null pointer,
- if T is a node Node n T
_{1}T_{2}, then p is not null, and at location p one finds a record with field contents n, p_{1}and p_{2}, with MTree T_{1}p_{1}and MTree T_{2}p_{2}describing the two subtrees.

Fixpoint MTree (T:tree) (p:loc) : hprop :=

match T with

| Leaf ⇒ \[p = null]

| Node n T

(p ~~~>`{ item := n; left := p

\* (MTree T

\* (MTree T

end.

match T with

| Leaf ⇒ \[p = null]

| Node n T

_{1}T_{2}⇒ \∃ p_{1}p_{2},(p ~~~>`{ item := n; left := p

_{1}; right := p_{2}})\* (MTree T

_{1}p_{1})\* (MTree T

_{2}p_{2})end.

## Alternative Characterization of MTree

Lemma MTree_Leaf : ∀ p,

(MTree Leaf p) = \[p = null].

Proof using. auto. Qed.

Lemma MTree_Node : ∀ p n T

(MTree (Node n T

\∃ p

(p ~~~>`{ item := n; left := p

\* (MTree T

Proof using. auto. Qed.

(MTree Leaf p) = \[p = null].

Proof using. auto. Qed.

Lemma MTree_Node : ∀ p n T

_{1}T_{2},(MTree (Node n T

_{1}T_{2}) p) =\∃ p

_{1}p_{2},(p ~~~>`{ item := n; left := p

_{1}; right := p_{2}})\* (MTree T

_{1}p_{1}) \* (MTree T_{2}p_{2}).Proof using. auto. Qed.

The third lemma reformulates MTree T p using a case analysis on whether
p is the null pointer. This formulation matches the case analysis
typically perform in the code of functions operating on trees.

Lemma MTree_if : ∀ (p:loc) (T:tree),

(MTree T p)

==> (If p = null

then \[T = Leaf]

else \∃ n p

\* (p ~~~>`{ item := n; left := p

\* (MTree T

Proof using.

intros. destruct T as [|n T

{ xchange MTree_Leaf. intros M. case_if. xsimpl*. }

{ xchange MTree_Node. intros p

xchange hrecord_not_null. intros N. case_if. xsimpl*. }

Qed.

Opaque MTree.

(MTree T p)

==> (If p = null

then \[T = Leaf]

else \∃ n p

_{1}p_{2}T_{1}T_{2}, \[T = Node n T_{1}T_{2}]\* (p ~~~>`{ item := n; left := p

_{1}; right := p_{2}})\* (MTree T

_{1}p_{1}) \* (MTree T_{2}p_{2})).Proof using.

intros. destruct T as [|n T

_{1}T_{2}].{ xchange MTree_Leaf. intros M. case_if. xsimpl*. }

{ xchange MTree_Node. intros p

_{1}p_{2}.xchange hrecord_not_null. intros N. case_if. xsimpl*. }

Qed.

Opaque MTree.

## Additional Tooling for MTree

Inductive tree_sub : binary (tree) :=

| tree_sub_1 : ∀ n T

tree_sub T

| tree_sub_2 : ∀ n T

tree_sub T

Lemma tree_sub_wf : wf tree_sub.

Proof using.

intros T. induction T; constructor; intros t' H; inversions¬H.

Qed.

Hint Resolve tree_sub_wf : wf.

| tree_sub_1 : ∀ n T

_{1}T_{2},tree_sub T

_{1}(Node n T_{1}T_{2})| tree_sub_2 : ∀ n T

_{1}T_{2},tree_sub T

_{2}(Node n T_{1}T_{2}).Lemma tree_sub_wf : wf tree_sub.

Proof using.

intros T. induction T; constructor; intros t' H; inversions¬H.

Qed.

Hint Resolve tree_sub_wf : wf.

For allocating fresh tree nodes as a 3-field record, we introduce the
operation mnode n p

_{1}p_{2}, defined and specified as follows.
Definition mnode : val :=

val_new_hrecord_3 item left right.

val_new_hrecord_3 item left right.

The first specification of mnode describes the allocation of a record.

Lemma triple_mnode : ∀ n p

triple (mnode n p

\[]

(funloc p ⇒ p ~~~> `{ item := n ; left := p

Proof using. intros. applys* triple_new_hrecord_3. Qed.

_{1}p_{2},triple (mnode n p

_{1}p_{2})\[]

(funloc p ⇒ p ~~~> `{ item := n ; left := p

_{1}; right := p_{2}}).Proof using. intros. applys* triple_new_hrecord_3. Qed.

The second specification, derived from the first, asserts that, if provided
the description of two subtrees T

_{1}and T_{2}at locations p_{1}and p_{2}, the operation mnode n p_{1}p_{2}builds, at a fresh location p, a tree described by Mtree [Node n T_{1}T_{2}] p.#### Exercise: 2 stars, standard, optional (triple_mnode')

Prove the specification triple_mnode' for node allocation.
Lemma triple_mnode' : ∀ T

triple (mnode n p

(MTree T

(funloc p ⇒ MTree (Node n T

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

Hint Resolve triple_mnode' : triple.

☐

_{1}T_{2}n p_{1}p_{2},triple (mnode n p

_{1}p_{2})(MTree T

_{1}p_{1}\* MTree T_{2}p_{2})(funloc p ⇒ MTree (Node n T

_{1}T_{2}) p).Proof using. (* FILL IN HERE *) Admitted.

Hint Resolve triple_mnode' : triple.

☐

## Tree Copy

if p = null

then null

else mnode p.item (tree_copy p.left) (tree_copy p.right)

Definition tree_copy :=

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b then null else (

let 'n = 'p`.item in

let 'p

let 'p

let 'q

let 'q

mnode 'n 'q

) }>.

<{ fix 'f 'p ⇒

let 'b = ('p = null) in

if 'b then null else (

let 'n = 'p`.item in

let 'p

_{1}= 'p`.left inlet 'p

_{2}= 'p`.right inlet 'q

_{1}= 'f 'p_{1}inlet 'q

_{2}= 'f 'p_{2}inmnode 'n 'q

_{1}'q_{2}) }>.

Lemma triple_tree_copy : ∀ p T,

triple (tree_copy p)

(MTree T p)

(funloc q ⇒ (MTree T p) \* (MTree T q)).

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

☐

triple (tree_copy p)

(MTree T p)

(funloc q ⇒ (MTree T p) \* (MTree T q)).

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

☐

## Computing the Sum of the Items in a Tree

if p ≠ null then (

c := !c + p.item;

treeacc c p.left;

treeacc c p.right)

let mtreesum p =

let c = ref 0 in

treeacc c p;

!c

Definition treeacc : val :=

<{ fix 'f 'c 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'm = ! 'c in

let 'x = 'p`.item in

let 'm

'c := 'm

let 'p

'f 'c 'p

let 'p

'f 'c 'p

end }>.

Definition mtreesum : val :=

<{ fun 'p ⇒

let 'c = ref 0 in

treeacc 'c 'p;

get_and_free 'c }>.

<{ fix 'f 'c 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'm = ! 'c in

let 'x = 'p`.item in

let 'm

_{2}= 'm + 'x in'c := 'm

_{2};let 'p

_{1}= 'p`.left in'f 'c 'p

_{1};let 'p

_{2}= 'p`.right in'f 'c 'p

_{2}end }>.

Definition mtreesum : val :=

<{ fun 'p ⇒

let 'c = ref 0 in

treeacc 'c 'p;

get_and_free 'c }>.

The specification of mtreesum is expressed in terms of the logical
operation treesum which computes the sum of the node items stored
in a logical tree. This operation is defined in Coq as a fixed point.

Fixpoint treesum (T:tree) : int :=

match T with

| Leaf ⇒ 0

| Node n T

end.

match T with

| Leaf ⇒ 0

| Node n T

_{1}T_{2}⇒ n + treesum T_{1}+ treesum T_{2}end.

#### Exercise: 4 stars, standard, optional (triple_mtreesum)

Prove the correctness of the function mlength'. Hint: start by stating a lemma triple_treeacc, then register it using the command Hint Resolve triple_treeacc : triple.. Finally, complete the proof of the specification triple_mtreesum.
(* FILL IN HERE *)

Lemma triple_mtreesum : ∀ T p,

triple (mtreesum p)

(MTree T p)

(fun r ⇒ \[r = treesum T] \* (MTree T p)).

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

☐

Lemma triple_mtreesum : ∀ T p,

triple (mtreesum p)

(MTree T p)

(fun r ⇒ \[r = treesum T] \* (MTree T p)).

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

☐

## Verification of a Counter Function with Local State

Implicit Type f : val.

A counter function is a function f such that, each time it
is invoked, returns the next integer, starting from 1.
The function create_counter produces a fresh counter function.
Concretely, if create_counter() produces the counter f,
then the first call to f() returns 1, the second call to
f() returns 2, the third call to f() returns 3, and so on.
The counter function can be implemented using a reference cell,
named p, that stores the integer last returned by the counter.
Initially, the contents of the reference p is zero. Each time
the counter is queried, the contents of p is increased by one
unit, and the new value of the contents is returned to the caller.
let create_counter () =

let p = ref 0 in

(fun () → (incr p; !p))

let p = ref 0 in

(fun () → (incr p; !p))

Definition create_counter : val :=

<{ fun 'u ⇒

let 'p = ref 0 in

(fun_ 'u ⇒ (incr 'p; !'p)) }>.

<{ fun 'u ⇒

let 'p = ref 0 in

(fun_ 'u ⇒ (incr 'p; !'p)) }>.

The remaining of this section presents two set of specifications,
each covering both the specification of a counter function and
the specification of a function that creates a fresh counter function.
The first specification is the most direct: it exposes the existence
of a reference p. Doing so, however, reveals implementation details
about the counter function.
The second specification is more abstract: it successfully hides
the description of the internal representation of the counter,
and states specification only in terms of a representation predicate,
called IsCounter f n, that exposes only the identity of the
counter function and its current value, but not the existence of
the reference p.
Let's begin with the simple, direct specification. The proposition
CounterSpec f p asserts that the counter function f has its
internal state stored in a reference cell at location p, in the
sense that invoking f in a state p ~~> m updates the state to
p ~~> (m+1) and produces the output value m+1.

Definition CounterSpec (f:val) (p:loc) : Prop :=

∀ m, triple (f ())

(p ~~> m)

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

∀ m, triple (f ())

(p ~~> m)

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

The function create_counter creates a fresh counter. Its precondition
is empty. Its postcondition describes the existence of a reference
cell p ~~> 0, for an existentially quantified location p, and such
that the proposition CounterSpec f p holds. Observe the use of the
tactic xfun for reasoning about a function definition.

Lemma triple_create_counter :

triple (create_counter ())

\[]

(fun f ⇒ \∃ p, (p ~~> 0) \* \[CounterSpec f p]).

Proof using.

xwp. xapp. intros p. xfun. intros f Hf. xsimpl.

{ intros m. applys Hf. xapp. xapp. xsimpl. auto. }

Qed.

triple (create_counter ())

\[]

(fun f ⇒ \∃ p, (p ~~> 0) \* \[CounterSpec f p]).

Proof using.

xwp. xapp. intros p. xfun. intros f Hf. xsimpl.

{ intros m. applys Hf. xapp. xapp. xsimpl. auto. }

Qed.

Given a counter function described by CounterSpec f p, a call to the
function f on a unit argument, in an input state of the form p ~~> n
for some n, produces the state p ~~> (n+1) and the output value n+1.
Observe how this specification applies to any function f satisfying
CounterSpec f p.

Lemma triple_apply_counter : ∀ f p n,

CounterSpec f p →

triple (f ())

(p ~~> n)

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

Proof using. introv Hf. applys Hf. Qed.

CounterSpec f p →

triple (f ())

(p ~~> n)

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

Proof using. introv Hf. applys Hf. Qed.

In the proof above, we were able to directly apply the assumption Hf.
In general, however, for reasoning about a call to an abstract function
f, it is generally needed to first invoke the tactic xwp.

Lemma triple_apply_counter_alternative_proof : ∀ f p n,

CounterSpec f p →

triple (f ())

(p ~~> n)

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

Proof using.

introv Hf. xtriple. lets H: Hf n. xapp. xsimpl. auto.

Qed.

CounterSpec f p →

triple (f ())

(p ~~> n)

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

Proof using.

introv Hf. xtriple. lets H: Hf n. xapp. xsimpl. auto.

Qed.

Let's now make the specifications more abstract, by hiding away the
description of the reference cells from the client of the specifications.
To that end, we introduce the heap predicate IsCounter f n, which
relates a function f, its current value n, and the piece of memory
state involved in the implementation of this function. This piece of
memory is of the form p ~~> n for some location p, such that
CounterSpec f p holds. Here, p gets quantified existentially.

Definition IsCounter (f:val) (n:int) : hprop :=

\∃ p, p ~~> n \* \[CounterSpec f p].

\∃ p, p ~~> n \* \[CounterSpec f p].

Using IsCounter, we can reformulate the specification of
create_counter is a more abstract and more concise manner,
with a postcondition simply asserting that the fresh counter
function f initialized at zero is described by the heap
predicate IsCounter f 0.

Lemma triple_create_counter_abstract :

triple (create_counter ())

\[]

(fun f ⇒ IsCounter f 0).

Proof using. unfold IsCounter. applys triple_create_counter. Qed.

triple (create_counter ())

\[]

(fun f ⇒ IsCounter f 0).

Proof using. unfold IsCounter. applys triple_create_counter. Qed.

Likewise, we can reformulate the specification of a call to a counter
function f. Such a call, under precondition IsCounter f n for some
n, admits the precondition IsCounter f (n+1), and returns n+1.

#### Exercise: 3 stars, standard, especially useful (triple_apply_counter_abstract)

Prove the abstract specification for a counter function. Hint: use xtriple at some point.
Lemma triple_apply_counter_abstract : ∀ f n,

triple (f ())

(IsCounter f n)

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

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

☐

triple (f ())

(IsCounter f n)

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

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

☐

Opaque IsCounter.

## Specification of a Higher-Order Repeat Operator

if n > 0 then (f(); repeat f (n-1))

Definition repeat : val :=

<{ fix 'g 'f 'n ⇒

let 'b = ('n > 0) in

if 'b then

'f ();

let 'n

'g 'f 'n

end }>.

<{ fix 'g 'f 'n ⇒

let 'b = ('n > 0) in

if 'b then

'f ();

let 'n

_{2}= 'n - 1 in'g 'f 'n

_{2}end }>.

For simplicity, let us assume for now n ≥ 0. The specification of
repeat n f is expressed in terms of an invariant, named I,
describing the state in-between every two calls to f. Initially, we
assume the state to satisfy f 0. We assume that, for every index i
in the range from 0 (inclusive) to n (exclusive), a call f() takes
the state from one satisfying f i to one satisfying f (i+1). The
specification below asserts that, under these assumptions, after the n
calls to f(), the final state satisfies f n.
The specification takes the form:

n ≥ 0 →

Hypothesis_on_f →

triple (repeat f n)

(I 0)

(fun u ⇒ I n).
where the hypothesis of f captures the following specification:

0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1))
The complete specification of repeat n f appears below.

n ≥ 0 →

Hypothesis_on_f →

triple (repeat f n)

(I 0)

(fun u ⇒ I n).

0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1))

Lemma triple_repeat : ∀ (I:int→hprop) (f:val) (n:int),

n ≥ 0 →

(∀ i, 0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1))) →

triple (repeat f n)

(I 0)

(fun u ⇒ I n).

n ≥ 0 →

(∀ i, 0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1))) →

triple (repeat f n)

(I 0)

(fun u ⇒ I n).

To establish that specification, we carry out a proof by induction over the
judgment:

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).
which asserts that, when there remains m calls to perform, the current
state is described by I (n-m), that is, the current index i is equal
to n-m.

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

Proof using.

introv Hn Hf.

cuts G: (∀ m, 0 ≤ m ≤ n →

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

{ applys_eq G. { fequals. math. } { math. } }

intros m. induction_wf IH: (downto 0) m. intros Hm.

xwp. xapp. xif; intros C.

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

math_rewrite ((n - m) + 1 = n - (m - 1)). xsimpl. }

{ xval. math_rewrite (n - m = n). xsimpl. }

Qed.

introv Hn Hf.

cuts G: (∀ m, 0 ≤ m ≤ n →

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

{ applys_eq G. { fequals. math. } { math. } }

intros m. induction_wf IH: (downto 0) m. intros Hm.

xwp. xapp. xif; intros C.

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

math_rewrite ((n - m) + 1 = n - (m - 1)). xsimpl. }

{ xval. math_rewrite (n - m = n). xsimpl. }

Qed.

## Specification of an Iterator on Mutable Lists

if p ≠ null then (f p.head; miter f p.tail)

Definition miter : val :=

<{ fix 'g 'f 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'x = 'p`.head in

'f 'x;

let 'q = 'p`.tail in

'g 'f 'q

end }>.

<{ fix 'g 'f 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'x = 'p`.head in

'f 'x;

let 'q = 'p`.tail in

'g 'f 'q

end }>.

The specification of miter follows the same structure as that of the
function repeat from the previous section, with two main differences.
The first difference is that the invariant is expressed not in terms of
an index i ranging from 0 to n, but in terms of a prefix of the
list L being traversed, ranging from nil to the full list L.
The second difference is that the operation miter f p requires in its
precondition, in addition to I nil, the description of the mutable list
MList L p. This predicate is returned in the postcondition, unchanged,
reflecting on the fact that the iteration does not alter the list.

#### Exercise: 5 stars, standard, especially useful (triple_miter)

Prove the correctness of triple_miter.
Lemma triple_miter : ∀ (I:list val→hprop) L (f:val) p,

(∀ x L

triple (f x)

(I L

(fun u ⇒ I (L

triple (miter f p)

(MList L p \* I nil)

(fun u ⇒ MList L p \* I L).

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

☐

(∀ x L

_{1}L_{2}, L = L_{1}++x::L_{2}→triple (f x)

(I L

_{1})(fun u ⇒ I (L

_{1}++(x::nil)))) →triple (miter f p)

(MList L p \* I nil)

(fun u ⇒ MList L p \* I L).

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

☐

## Computing the Length of a Mutable List using an Iterator

let c = ref 0 in

miter (fun x → incr c) p;

!c

#### Exercise: 4 stars, standard, especially useful (triple_mlength_using_miter)

Prove the correctness of mlength_using_iter. Hint: use xfun. intros f Hf for reasoning about the function definition, then use xapp for reasoning about a call to f by inlining its code.
Definition mlength_using_miter : val :=

<{ fun 'p ⇒

let 'c = ref 0 in

let 'f = (fun_ 'x ⇒ incr 'c) in

miter 'f 'p;

get_and_free 'c }>.

Lemma triple_mlength_using_miter : ∀ p L,

triple (mlength_using_miter p)

(MList L p)

(fun r ⇒ \[r = length L] \* MList L p).

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

☐

<{ fun 'p ⇒

let 'c = ref 0 in

let 'f = (fun_ 'x ⇒ incr 'c) in

miter 'f 'p;

get_and_free 'c }>.

Lemma triple_mlength_using_miter : ∀ p L,

triple (mlength_using_miter p)

(MList L p)

(fun r ⇒ \[r = length L] \* MList L p).

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

☐

## A Continuation-Passing-Style, In-Place Concatenation Function

_{1}p

_{2}is also slightly different: this operation returns a pointer p

_{3}that describes the head of the result of the concatenation, and it works even if p

_{1}corresponds to an empty list.

_{1}p

_{2}k =

if p

_{1}== null

then k p

_{2}

else cps_append_aux p

_{1}.tail p

_{2}(fun r ⇒ (p

_{1}.tail <- r); k p

_{1})

let cps_append p

_{1}p

_{2}=

cps_append_aux p

_{1}p

_{2}(fun r ⇒ r)

Definition cps_append_aux : val :=

<{ fix 'f 'p

let 'b = ('p

if 'b

then 'k 'p

else

let 'q

let 'k

'f 'q

Definition cps_append : val :=

<{ fun 'p

let 'f = (fun_ 'r ⇒ 'r) in

cps_append_aux 'p

<{ fix 'f 'p

_{1}'p_{2}'k ⇒let 'b = ('p

_{1}= null) inif 'b

then 'k 'p

_{2}else

let 'q

_{1}= 'p_{1}`.tail inlet 'k

_{2}= (fun_ 'r ⇒ ('p_{1}`.tail := 'r; 'k 'p_{1})) in'f 'q

_{1}'p_{2}'k_{2}}>.Definition cps_append : val :=

<{ fun 'p

_{1}'p_{2}⇒let 'f = (fun_ 'r ⇒ 'r) in

cps_append_aux 'p

_{1}'p_{2}'f }>.#### Exercise: 5 stars, standard, optional (triple_cps_append)

Specify and verify cps_append_aux, then verify cps_append.
(* FILL IN HERE *)

The main function cps_append simply invokes cps_append_aux
with a trivial continuation.

Lemma triple_cps_append : ∀ (L

triple (cps_append p

(MList L

(funloc p

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

☐

_{1}L_{2}:list val) (p_{1}p_{2}:loc),triple (cps_append p

_{1}p_{2})(MList L

_{1}p_{1}\* MList L_{2}p_{2})(funloc p

_{3}⇒ MList (L_{1}++L_{2}) p_{3}).Proof using. (* FILL IN HERE *) Admitted.

☐

## Historical Notes

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