# 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

*representation predicates*.

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

- xpull to extract pure facts and quantifiers from the LHS of ==>.
- xchange for exploiting transitivity of ==>.
- xfun to reason about function definitions.
- xtriple to establish specifications for abstract functions.
- rew_list (a TLC tactic) to normalize list expressions.

## 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 Records.)
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, 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 the following.
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. The tactic case_if 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 on 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. To exploit
this fact, we can execute rewrite MList_nil, then invoke the tactic
xpull to extract the pure heap predicate \[p = null] from the LHS. A
more efficient approach is to leverage the CFML tactic xchange, as
follows.

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'. To simplify MList (x :: L') p, we could execute the tactics
rewrite MList_cons. xpull., but, here again, using xchange leads to a
more concise script.

Because a record is allocated at location p, the pointer p cannot be
null. The library 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
with MList_nil, MList_cons, and MList_if. We therefore make the
definition of MList opaque to prevent Coq from performing undesired
simplifications.

## In-place Concatenation of Two Mutable Lists

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

_{2}to 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 you 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 a hypothesis for the tail of L

_{1}. The predicate list_sub L_{1}' L_{1}asserts that L_{1}decomposes as x::L_{1}' for some x.
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 if-statement.

xapp. xapp. xif; intros Cq

_{1}.
If q

_{1}' is null, then L_{1}' is empty.
In this case, we reason about the assignement, 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 re-fold 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*.

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

#[global] Hint Resolve triple_mnil : triple.

#[global] Hint Resolve triple_mnil : triple.

An important aspect of the specification triple_mnil is that it 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. 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 a primitive operation called
val_new_hrecord_2.

The operation mcons admits two specifications. The first one says that it
produces a record described with a record heap predicate.

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 asserts that mcons can be used to extend a
mutable list. It 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 to exploit the first specification, where
needed.

#[global] 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 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', and
- 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.

When entering the first branch of the proof after the case analysis, Coq
reports two hypotheses p = null. Actually, these two hypotheses are
slightly different. Using Set Printing Coercions. reveals their true type:
val_loc p = val_loc null and p = null. Thus, only the second hypothesis
can be used for a substitution or rewrite operation.

## 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. Hint: use the TLC tactic rew_list to normalize list expressions -- in particular, to prove length L' + 1 = length (x :: L').
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.

☐

## Free Function for Lists

if p != null then begin

let q = p.tail in

delete p;

mfree q

end

Definition mfree : val :=

<{ fix 'f 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'q = 'p`.tail in

delete 'p;

'f 'q

end }>.

<{ fix 'f 'p ⇒

let 'b = ('p ≠ null) in

if 'b then

let 'q = 'p`.tail in

delete 'p;

'f 'q

end }>.

The precondition of mfreep requires a full list MList L p. The
postcondition is empty: the entire list is destroyed.

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

Verify the function mfree.
Lemma triple_mfree : ∀ L p,

triple (mfree p)

(MList L p)

(fun _ ⇒ \[]).

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

☐

triple (mfree p)

(MList L p)

(fun _ ⇒ \[]).

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 null p

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 triple_mrev_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 the functions push, top and pop for operating at
the top of the stack.
type 'a stack = {

data : 'a list;

size : int }

let create () =

{ data = null;

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 constants data and size are introduced as identifiers for the record
fields of the type 'a stack.

data : 'a list;

size : int }

let create () =

{ data = null;

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.

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

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

\∃ 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 performed 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.

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

Beyond this point, the definition of Mtree not longer needs to be
unfolded. Thus, we make it opaque.

## 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. The relation tree_sub is defined as follows.

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.

#[global] 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.

#[global] 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. apply triple_new_hrecord_3; auto. 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. apply triple_new_hrecord_3; auto. 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.

#[global] 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.

#[global] 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}) }>.

#### Exercise: 3 stars, standard, optional (triple_tree_copy)

Prove the specification of tree_copy. Hint: you'll need to use xchange <- (MTree_Leaf null) twice.
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 mtreesum. 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]).

triple (create_counter ())

\[]

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

Observe how the postcondition that appears in the triple below refers to
CounterSpec, which itself involves a triple. In other words, a triple
appears nested inside another triple. In technical terms, we are leveraging
the "imprecativity of triples", which holds as a consequence of the
"impredicativity of predicates" in the logic of Coq.
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.

Proof using.

xwp. xapp. intros p.

xfun. intros f Hf.

xsimpl.

{ intros m.

xwp. xapp. intros p.

xfun. intros f Hf.

xsimpl.

{ intros m.

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

xapp.

xapp. xapp. xsimpl. auto. }

Qed.

xapp. xapp. xsimpl. auto. }

Qed.

Let us move on to the presentation of more abstract specifications. Their
purpose is to hide from the client the existence of the reference cell used
to represent the internal state of the counter functions. 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.

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.

Next, we 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 other x-tactics can be invoked. Then, use xpull 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.

☐

Finally, let us illustrate how a client might work with counter functions.
let test_counter () =

let c

let c

let n

let n

let n

n

let c

_{1}= create_counter () inlet c

_{2}= create_counter () inlet n

_{1}= c_{1}() inlet n

_{2}= c_{2}() inlet n

_{3}= c_{1}() inn

_{2}+ n_{3}
Definition test_counter : val :=

<{ fun 'u ⇒

let 'c

let 'c

let 'n

let 'n

let 'n

'n

<{ fun 'u ⇒

let 'c

_{1}= create_counter () inlet 'c

_{2}= create_counter () inlet 'n

_{1}= 'c_{1}() inlet 'n

_{2}= 'c_{2}() inlet 'n

_{3}= 'c_{1}() in'n

_{2}+ 'n_{3}}>.#### Exercise: 2 stars, standard, optional (triple_test_counter)

Prove the example function manipulating abstract counters. In the specification below, the heap predicate \∃ H, H corresponds to the two counters, which we currently have no way of deallocating. The necessary mechanism for garbage collection will be introduced later in chapter Affine.
Lemma triple_test_counter :

triple (test_counter ())

\[]

(fun r ⇒ \[r = 3] \* (\∃ H, H)).

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

☐

triple (test_counter ())

\[]

(fun r ⇒ \[r = 3] \* (\∃ H, H)).

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

☐

# Optional Material

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

{ replace 0 with (n - n). { eapply G. math. } { math. } }

triple (repeat f m)

(I (n-m))

(fun u ⇒ I n)).

{ replace 0 with (n - n). { eapply G. 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. Use of xlet is optional.
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 Factorial Function in Continuation-Passing Style

if n ≤ 1

then k 1

else cps_facto_aux (n-1) (fun r → k (n * r))

let cps_facto n =

cps_facto_aux n (fun r → r)

Definition cps_facto_aux : val :=

<{ fix 'f 'n 'k ⇒

let 'b = 'n ≤ 1 in

if 'b

then 'k 1

else let 'k

let 'n

'f 'n

Definition cps_facto : val :=

<{ fun 'n ⇒

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

cps_facto_aux 'n 'k }>.

Import Facto.

<{ fix 'f 'n 'k ⇒

let 'b = 'n ≤ 1 in

if 'b

then 'k 1

else let 'k

_{2}= (fun_ 'r ⇒ let 'r_{2}= 'n * 'r in 'k 'r_{2}) inlet 'n

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

_{2}'k_{2}}>.Definition cps_facto : val :=

<{ fun 'n ⇒

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

cps_facto_aux 'n 'k }>.

Import Facto.

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

Verify cps_facto_aux. Hints: To set up the induction, use the usual pattern induction_wf IH: (downto 0) n. To reason about the function definition, use xfun. To reason about the recursive call, you'll need to exploit the induction hypothesis, called IH, which universally quantifies over a function F of type int→int. To do so, use the syntax xapp (>> IH (fun a ⇒ ..)). The function provided should describe the behavior of the continuation k_{2}that appears in the code. For the mathematical reasoning, use the same pattern as in the proof of factorec, applying the tactics rewrite facto_init and rewrite (@facto_step n).

Lemma triple_cps_facto_aux : ∀ (n:int) (k:val) (F:int→int),

n ≥ 0 →

(∀ (a:int), triple (k a) \[] (fun r ⇒ \[r = F a])) →

triple (cps_facto_aux n k)

\[]

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

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

☐

n ≥ 0 →

(∀ (a:int), triple (k a) \[] (fun r ⇒ \[r = F a])) →

triple (cps_facto_aux n k)

\[]

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

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

☐

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

Verify cps_facto. Hint: use the syntax xapp (>> triple_cps_append_aux F) to provide the function F that describes the behavior of the identity continuation.
Lemma triple_cps_facto : ∀ n,

n ≥ 0 →

triple (cps_facto n)

\[]

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

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

☐

n ≥ 0 →

triple (cps_facto n)

\[]

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

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

☐

## An In-Place Concatenation Function in Continuation-Passing Style

_{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 a couple 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 }>.
The goal is to establish the following specification for cps_append.

Lemma triple_cps_append : ∀ (L

triple (cps_append p

(MList L

(funloc p
If you are interested in the challenge of solving a 6-star exercise, then try
to prove the above specification without reading any further. If, however,
you are only looking for a 5-star exercise, keep reading.

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}).#### Exercise: 5 stars, standard, optional (triple_cps_append_aux)

The specification of cps_append_aux involves an hypothesis describing the behavior of the continuation k. For this function, and more generally for code in CPS form, we cannot easily leverage the frame property, thus we need to quantify explicitly over a heap predicate H for describing the "rest of the state". Prove that specification. Hint: you can use the syntax xapp (>> IH H') to instantiate the induction hypothesis IH on a specific heap predicate H'.
Lemma triple_cps_append_aux : ∀ H Q (L

(∀ (p

triple (cps_append_aux p

(MList L

Q.

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

☐

_{1}L_{2}:list val) (p_{1}p_{2}:loc) (k:val),(∀ (p

_{3}:loc), triple (k p_{3}) (MList (L_{1}++ L_{2}) p_{3}\* H) Q) →triple (cps_append_aux p

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

_{1}p_{1}\* MList L_{2}p_{2}\* H)Q.

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

☐

#### Exercise: 3 stars, standard, optional (triple_cps_append)

Verify cps_append. Hint: use the syntax @triple_cps_append_aux H' Q' to specialize the specification of the auxiliary function to specific pre- and post-conditions.
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

(* 2024-01-03 14:46 *)