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

Implicit Types x : val.

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.

Implicit Types x : val.

# First Pass

- The
*First Pass*section presents the most important ideas only. - The
*More Details*section presents additional material explaining in more depth the meaning and the consequences of the key results. By default, readers would eventually read all this material. - The
*Optional Material*section contains more advanced material, for readers who can afford to invest more time in the topic.

## Formalization of the List Representation Predicate

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. The arrow ~~~> is provided by the framework for describing
records. The notation `{...} is a handy notation for a list of pairs of
field names and values of arbitrary types. (Further details on the
formalization of records are presented in chapter Struct.)
A mutable list consists of a chain of cells. Each cell stores a tail pointer
that gives the location of the next cell in the chain. The last cell stores
the null value in its tail field.
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:
This definition is formalized as follows.

- if L is empty, then p is the null pointer,
- if L is of the form x::L', then p is not null, and 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.

In addition, it is also very useful in proofs to reformulate the definition
of MList L p in the form of a case analysis on whether the pointer p is
null or not. This corresponds to the programming pattern
if p == null then ... else. This alternative characterization of
MList L p asserts that:
The corresponding lemma, shown below, is stated using the
If P then X else Y construction, which generalizes Coq's construction
if b then X else Y to discriminate over a proposition P as opposed to a
boolean value b. The If construct leverages (strong) classical logic. It
is provided by the TLC library, just like the tactic case_if which is
convenient for performing the case analysis on whether P is true or false.

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

(MList L p)

==> (If p = null

then \[L = nil]

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

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

The proof is a bit technical, it may be skipped for a first reading.

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.

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.

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.

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.

To conclude, it suffices to correctly instantiate the existential
quantifiers. The tactic xsimpl is able to guess the appropriate
instantiations.

xsimpl. auto. }

Qed.

Qed.

Note that the reciprocal entailment to the one stated in MList_if is also
true, but we do not need it so we do not bother proving it here. In the rest
of the course, we will never unfold the definition MList, but only work
using MList_nil, MList_cons, and MList_if. So, we can make MList
opaque, thereby avoiding undesired simplifications.

## In-place Concatenation of Two Mutable Lists

_{1}on a nonempty list, and a pointer p

_{2}on another list (possibly empty). The function updates the last cell from the first list in such a way that its tail points to the head cell of p

_{2}. After this operation, the pointer p

_{1}points to a list that corresponds to the concatenation of the two input lists.

_{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 shown below. The proof
pattern is representative of that of many list-manipulating functions, so it
is essential that the reader follow through every step of this 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}.
We then reason about the case analysis.

xapp. xapp. xif; intros Cq

_{1}.
If q

_{1}' is null, then L_{1}' is empty.
In this case, we set the pointer, then we fold back the head cell.

Otherwise, if q

_{1}' is not null, we reason about the recursive call using the induction hypothesis, then we fold back the head cell.## Smart Constructors for Linked Lists

Definition mnil : val :=

<{ fun 'u ⇒

null }>.

Lemma triple_mnil :

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

<{ fun 'u ⇒

null }>.

Lemma triple_mnil :

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

The proof uses the tactic xchanges*, which is a shorthand for xchange
followed with xsimpl*.

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 creates a fresh list cell, with x in the head
field and q in the tail field. Its implementation allocates and
initializes a fresh record made of two fields. The allocation operation
leverages the allocation construct written `{ head := 'x; tail := 'q } in
the code. This construct is in fact a notation for an operation called
val_new_hrecord_2, which we here view as a primitive operation.

The operation mcons admits two specifications. The first one describes
only the production of a heap predicate for the freshly allocated record.

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 assumes that the argument q comes with a list
representation of the form Mlist q L, and it specifies that the function
mcons produces the representation predicate Mlist p (x::L). This second
specification is derivable from the first one, by folding the representation
predicate MList using the tactic xchange.

Lemma triple_mcons' : ∀ L x q,

triple (mcons x q)

(MList L q)

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

Proof using.

intros. xapp triple_mcons.

intros p. xchange <- MList_cons. xsimpl*.

Qed.

triple (mcons x q)

(MList L q)

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

Proof using.

intros. xapp triple_mcons.

intros p. xchange <- MList_cons. xsimpl*.

Qed.

In practice, this second specification is more often useful than the first
one, hence we register it in the database for xapp. It remains possible to
invoke xapp triple_mcons for exploiting the first specification, where
needed.

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 described as MList L p.
The postcondition asserts that the function returns a pointer p' and a
list described as 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).

The proof is structure is like 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. Make sure to generalize the appropriate variables before applying the well-founded induction tactic. Then, complete the proof of the specification triple_mlength', using xapp triple_acclength to reason about the call to the auxiliary function.
(* 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. Hint: here again, start by stating a lemma mtriple_rev_aux expressing the specification of the recursive function mrev_aux. Make sure to generalize the appropriate variables before applying the well-founded induction tactic. Then, complete the proof of triple_mrev, using xapp triple_mrev_aux.
(* 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.

☐

In this section, we consider the implementation of a mutable stack featuring
a constant-time access to the size of the stack. This 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 implementation includes
a function create to allocate an empty stack, a function sizeof for
reading the size, and three functions push, top and pop 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 top s =

let p = s.data in

p.head

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 top s =

let p = s.data in

p.head

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 location of the
mutable list; this location is existentially quantified in the definition.
The predicate Stack also does not expose the size of the stack, as this
value can be deduced by computing length L. Let's start with the
specification and verification of create and sizeof.

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.

☐

#### Exercise: 2 stars, standard, optional (triple_top)

Prove the following specification for the top operation.
Lemma triple_top : ∀ L s,

L ≠ nil →

triple (top s)

(Stack L s)

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

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

☐

L ≠ nil →

triple (top s)

(Stack L s)

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

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

☐

## Formalization of the Tree Representation Predicate

_{1}T

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

_{1}and T

_{2}denote the two subtrees.

In a program manipulating a mutable tree, an empty tree is represented using
the null pointer, and a node is represented in memory using a three-cell
record. The first field, named "item", stores an integer. The other two
fields, named "left" and "right", store 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, storing the integer n and the two pointers p_{1}and p_{2}.- 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 that operates 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

_{1}T asserts that the tree T

_{1}is either the left or the right subtree of the tree T. This order may be exploited for verifying recursive functions over trees using the tactic induction_wf IH: tree_sub T.

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

A 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. Compared with the first specification, this second specification is said to perform "ownership transfer".#### 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 Coq function
treesum, which computes the sum of the node items stored in a logical
tree. This operation is defined by recursion over the tree.

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: to begin with, state and prove the specification lemma triple_treeacc.
(* 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

let p = ref 0 in

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

In this section, we present two specifications for counter functions. The
first specification is the most direct, however it exposes the existence of
the reference cell, revealing implementation details about the counter
function. The second specification is more abstract: it hides from the
client the internal representation of the counter, by means of using an
abstract representation predicate.
Let us begin with the simple, direct specification. The proposition
CounterSpec f p asserts that f is a counter function f whose internal
state is stored in a reference cell at location p. Thus, 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)).

Implicit Type f : val.

∀ m, triple (f ())

(p ~~> m)

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

Implicit Type f : val.

The function create_counter creates a fresh counter. Its precondition is
empty. Its postcondition asserts that the function f being returned
satisfies CounterSpec f p, and the output state contains a cell p ~~> 0
for some existentially quantified location p.

Lemma triple_create_counter :

triple (create_counter ())

\[]

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

Proof using.

xwp. xapp. intros p.

triple (create_counter ())

\[]

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

Proof using.

xwp. xapp. intros p.

The proof involves the use of a new tactic, called xfun, for reasoning
about local function definitions. Here, xfun gives us the hypothesis Hf
that specifies the code of f

xfun. intros f Hf.

xsimpl.

{ intros m.

xsimpl.

{ intros m.

To reason about the call to the function f, we can exploit Hf, either
explicitly by calling applys Hf, or automatically by simply calling xapp
.

xapp.

xapp. xapp. xsimpl. auto. }

Qed.

xapp. xapp. xsimpl. auto. }

Qed.

Consider now a call to a counter function f, under the assumption
CounterSpec f p. Assume the input state to be of the form p ~~> n for
some n. Then, the call produces a state p ~~> (n+1), and returns the
value n+1. The specification shown below captures this logic, for any f.

Lemma triple_apply_counter : ∀ f p n,

CounterSpec f p →

triple (f ())

(p ~~> n)

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

CounterSpec f p →

triple (f ())

(p ~~> n)

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

The specification above is in fact nothing but a reformulation of the
definition of CounterSpec. Thus, its proof is straightforwards. (The proof
may actually be reduced to just auto, however in general one needs to use
xapp for reasoning about an abstract function.)

Proof using. introv Hf. unfolds in Hf. xapp. xsimpl*. Qed.

## Verification of a Counter Function with Local State, With Abstraction

Using IsCounter, we can reformulate the specification of create_counter
with a postcondition asserting that the output function f is described by
the heap predicate IsCounter f 0.

This lemma is the same as the previous specification triple_create_counter
, except that the reference cell p is no longer visible.

We can also reformulate the specification of a call to a counter function. A
call to f(), in a state satisfying IsCounter f n, produces a state
satisfying IsCounter f (n+1), and returns n+1.

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

Prove the abstract specification for a counter function. You will need to begin the proof using the tactic xtriple, for turning goal into a form on which xpull can be invoked to extract facts from the precondition.
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.

☐

## 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 can be expressed in terms of an invariant, named I,
describing the state in between every two calls to f. We assume that the
initial state satisfies I 0. Moreover, we assume that, for every index i
in the range from 0 (inclusive) to n (exclusive), a call f() can
execute in a state that satisfies I i and produce a state that satisfies
I (i+1). The specification below asserts that, under these two
assumptions, after the n calls to f(), the final state satisfies I n.
The specification takes the form:

n ≥ 0 →

Hypothesis_on_f →

triple (repeat f n)

(I 0)

(fun u ⇒ I n) where Hypothesis_on_f is a proposition that captures the following specification:

∀ i,

0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1)) The complete specification of repeat n f is thus as shown below.

n ≥ 0 →

Hypothesis_on_f →

triple (repeat f n)

(I 0)

(fun u ⇒ I n) where Hypothesis_on_f is a proposition that captures the following specification:

∀ i,

0 ≤ i < n →

triple (f ())

(I i)

(fun u ⇒ I (i+1)) The complete specification of repeat n f is thus as shown below.

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

Proof using.

introv Hn Hf.

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

Proof using.

introv Hn Hf.

To establish this specification, we carry out a proof by induction over a
generalized specification, covering the case where there remains m
iterations to perform, for any value of m between 0 and n inclusive.

∀ m, 0 ≤ m ≤ n →

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)) We use the TLC tactics cuts, a variant of cut, to state show that the generalized specification entails the statement of triple_repeat.

∀ m, 0 ≤ m ≤ n →

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)) We use the TLC tactics cuts, a variant of cut, to state show that the generalized specification entails the statement of triple_repeat.

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

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

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

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

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

We then carry a proof by induction: during the execution, the value of m
decreases step by step down to 0.

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

xwp. xapp. xif; intros C.

xwp. xapp. xif; intros C.

We reason about the call to f

{ xapp. { math. } xapp.

We next reason about the recursive call.

Finally, when m reaches zero, we check that we obtain I n.

## 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. This prefix ranges 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 the
fact that the iteration process does not alter the contents of 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: as explained earlier, use xfun; intros f Hf for reasoning about the function definition, then use xapp for reasoning about a call to f.
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. In the general case, p

_{3}is equal to p

_{1}, but if p

_{1}is the null pointer, meaning that the first list is empty, then p

_{3}is equal to p

_{2}.

_{1}p

_{2}k, which invokes the continuation function k on the result of concatenating the lists at locations p

_{1}and p

_{2}. Its code appears at first quite puzzling, because the recursive call is performed inside the continuation. It takes a good drawing and at least several minutes to figure out how the function works.

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

Lemma triple_cps_append : ∀ (L

triple (cps_append p

(MList L

(funloc p

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

☐

Lemma triple_cps_append : ∀ (L

_{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-08-11 15:24 *)