# 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 E for exploiting a lemma E with a conclusion of the
form H
_{1}==> H_{2}or H_{1}= H_{2}. - xchange <- E for exploiting an entailment H
_{2}==> H_{1}in the case E is a lemma with a conclusion of the form H_{1}= H_{2}. - xchanges is a shorthand for xchange followed with xsimpl.
- xfun to reason about function definitions.
- xtriple to establish specifications for abstract functions.
- introv (a TLC tactic) like intros but takes as arguments only the name of the hypotheses, not of all variables.
- 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 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. (* FILL IN HERE *) Admitted.

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 take the time to play through every step of this
proof. Several exercises will require a very similar proof pattern.

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 TLC tactic introv is very convenient for providing explicit names for
hypotheses without having to provide names for the variables already named
in the lemma statement.

introv N.

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

_{1}. induction_wf IH: list_sub L_{1}. intros. xwp.
To begin the proof, we reveal the head cell of p

_{1}, exploiting the assumption that p_{1}≠ null.
Using xpull, we extract the existentially quantified variables: we let
q

_{1}denote the tail of p_{1}, x the head element of L_{1}, and L_{1}' the tail of L_{1}.
xpull.

The tactic intros → is a shorthand for intros E; rewrite E; clear E.

intros x q

_{1}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 assignment, then we fold back the head
cell. To that end, we exploit the tactic xchange <- MList_cons, which is
similar to xchange MList_cons but exploits the equality asserted by
MList_cons in the reverse direction.

Above, the tactic xchange discharges the goal because the LHS, after the
operation, matches the RHS. To see the details, change the line of script
to: xapp. eapply himpl_trans. xchange <- MList_cons. apply himpl_refl.

}

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

Note: in theory, we could present mnil as a constant rather than as a
function that takes unit as argument. However, viewing it as a function like
all the other example programs helps keep the framework minimal.

We are requested to prove that, under the empty precondition, the value
null satisfies the postcondition
fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* (MList nil p). As the
tactic xval shows, this is equivalent to proving that the precondition
\[] entails ∃ p, \[null = val_loc p] \* (MList nil p)).

xval.

To conclude the proof, it suffices to instantiate p with null, and to
argue that MList nil null can created out of thin air. This is indeed true
because MList nil null is equivalent to \[]. The first step is to obtain
an explicit statement of this equivalence, in the form of an hypothesis
named E. By instantiating the lemma MList_nil, which asserts that
∀ p, MList nil p = \[p = null], we obtain the equality
MList nil null = \[null = null].

Then, we invoke xchange <- E. In exchange for proving null = null, this
tactic replaces the empty heap predicate \[] with MList nil null.

xchange <- E. { auto. }

At this stage, the tactic xsimpl is able to automatically instantiate p
with null, and auto checks that null = null.

xsimpl. auto.

Qed.

Qed.

The proof above can be greatly shortened by using the tactic xchanges,
which is a shorthand for xchange <- E followed by xsimpl. In fact, we
even use xchanges* <- E, to invoke xchanges <- E followed by eauto.

Lemma triple_mnil' :

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

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

#[global] Hint Resolve triple_mnil : triple.

triple (mnil ())

\[]

(funloc p ⇒ MList nil p).

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

#[global] Hint Resolve triple_mnil : triple.

Observe that the specification triple_mnil does not mention the null
pointer anywhere. Hence, this specification abstracts away from the
implementation details of how mutable lists are represented internally.
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 details of record constructions are explained in
the chapter Record. There is no need to understand the details at
this stage.

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

To prove this lemma, we need to know that the record allocation operation is
in fact a notation for a call to val_new_hrecord_2, hence we need to
invoke a library lemma called triple_new_hrecord_2 for reasoning about
this call. (Don't worry: this proof pattern will not appear in exercises!)

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.

In what follows, we consider several classic operations on mutable lists,
each illustrating an idiomatic proof pattern.

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

intros. gen p. induction_wf IH: list_sub L.

xwp. xapp. xchange MList_if. xif.

{ intros C.

Note that C is actually val_loc p = val_loc null, and not simply
p = null. This explains why a call to subst does nothing. If needed, use
the TLC tactic, inverts C or invert C to exploit the equality. In this
specific proof, though, we don't need that.

case_if. (* automatically rules out the case p ≠ null *)

xpull. intros E. subst L.

xapp. xsimpl. { auto. }

subst. xchange <- MList_nil. auto. }

{ intros C. case_if. (* automatically rules out p = null *)

xpull. intros x q L' E. subst L.

xapp. xapp. xapp. intros q'.

xapp. intros p'.

xchange <- MList_cons. xsimpl. auto. }

Qed.

xpull. intros E. subst L.

xapp. xsimpl. { auto. }

subst. xchange <- MList_nil. auto. }

{ intros C. case_if. (* automatically rules out p = null *)

xpull. intros x q L' E. subst L.

xapp. xapp. xapp. intros q'.

xapp. intros p'.

xchange <- MList_cons. xsimpl. auto. }

Qed.

A Coq expert would typically write the same proof script in a more compact
fashion, as follows. Recall that the token → can be provided instead of a
fresh name to indicate on-the-fly substitution, and that the star token
after a tactic indicates a call to eauto.

Lemma triple_mcopy' : ∀ L p,

triple (mcopy p)

(MList L p)

(funloc p' ⇒ (MList L p) \* (MList 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.

triple (mcopy p)

(MList L p)

(funloc p' ⇒ (MList L p) \* (MList 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.

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

(Recall that get_and_free was defined in chapter Basic.

#### 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. Recall that rew_list can be used to simplify length (x :: L') into length L' + 1 and that math can be used to prove arithmetic equalities such as (n + 1) + m = n + (m + 1).
(* 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 mfree 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: 4 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._{1}==> (\∃ x, H

_{2}).

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

☐

# More Details

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 to a mutable linked list plus
an integer recording the length of that list. The implementation includes a
function create to allocate an empty stack, a function sizeof for
reading the size, and functions push, top, and pop for manipulating
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 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.
It also does not expose the size of the stack, as this value can be obtained
from 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. Hint: You'll need to unfold the definition of Stack as in the proofs above, and at some point you'll want to destruct L.
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 MTree

_{1}T

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

_{1}and T

_{2}are its 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, "item", stores an integer. The other two fields,
"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: 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, when provided
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 "transfer ownership" of the two subtrees.#### Exercise: 2 stars, standard, optional (triple_mnode')

Prove the specification triple_mnode' for node allocation. Because this specification refines the previous specification triple_mnode, the proof should begin with xapp triple_mnode.
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.

☐

## Deep-Copy of a Tree

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, especially useful (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, but it exposes the existence of the
reference cell, revealing implementation details about the counter function.
The second specification is more abstract, hiding from the client the
internal representation of the counter 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 above 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 "impredicativity 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. This hypothesis is of the form:
∀ v H' Q', (PRE H' CODE B POST Q') → triple (f v) H' Q', where B
denotes the code of the body of the function f instantiated on the
argument v, and where H' and Q' denote arbitrary pre- and
postconditions. Exploiting this assumption enables the user to subsequently
derive triples about the local function f, by reasoning about the code of
the f, just in the same way as when the user invokes xwp for reasoning
about a top-level function.

Proof using.

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 calling xapp. *)

xapp.

xapp. xapp. xsimpl. auto. }

Qed.

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 calling xapp. *)

xapp.

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 triple_create_counter, except that the reference
cell p is no longer explicitly mentioned in the postcondition. In other
words, the address of the reference cell p used internally by the counter
becomes hidden from the user.

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.

xapp. { math. } { math. }

We need to exploit an arithmetic equality. We do so using math_rewrite,
which is a convenient TLC tactic to assert an equality proved by the math
tactic, then immediately invoke rewrite with this equality.

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.

☐

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

☐

## 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-08-25 14:53 *)