First Pass

A representation predicate is a heap predicate that describes a mutable data structure. For example, the heap predicate MList L p describes a mutable linked list whose head cell is at location p, and whose elements are described by the Coq list L. In this chapter, we'll see how to define MList, and to use this predicate for specifying and verifying functions that operate on mutable linked lists. We will also study representation predicates for mutable trees, as well as for counter functions, which feature an internal state. As explained in the Preface, this chapter, like all the following ones, is decomposed in three parts:

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

In the proofs, we will make use of a few additional tactics:

• xpull to extract pure facts and quantifiers from the LHS of ==>.
• xchange for exploiting transitivity of ==>.
• xfun to reason about a function definition.
• xtriple to establish a specification for an abstract function.
• rew_list is a TLC tactic used to normalize list expressions.

Formalization of the List Representation Predicate

The implementation of mutable lists and trees involves the use of records. For simplicity, field names are represented as natural numbers. For example, to represent a list cell with a head and a tail field, we define head as the constant zero, and tail as the constant one.

The heap predicate p ~~~>`{ head := x; tail := q } describes a record allocated at location p, with a head field storing x and a tail field storing q. The arrow ~~~> is provided by the framework for describing records. The notation `{...} is a handy notation for a list of pairs of field names and values of arbitrary types. (Further details on the formalization of records are presented in chapter Struct.) A mutable list consists of a chain of cells. Each cell stores a tail pointer that gives the location of the next cell in the chain. The last cell stores the null value in its tail field. The heap predicate MList L p describes a list whose head cell is at location p, and whose elements are described by the list L. This predicate is defined recursively on the structure of L:

• if L is empty, then p is the null pointer,
• if L is of the form x::L', then p is not null, and the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

This definition is formalized as follows.

Alternative Characterizations of MList

Carrying out proofs directly with MList can be slightly cumbersome, mainly due to Coq's limited support for folding back definitions. We find it more practical to explicitly state equalities that paraphrase the definition of MList. There is one equality for the nil case, and one for the cons case.

In addition, it is also very useful in proofs to reformulate the definition of MList L p in the form of a case analysis on whether the pointer p is null or not. This corresponds to the programming pattern if p == null then ... else. This alternative characterization of MList L p asserts that:

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

The corresponding lemma, shown below, is stated using the If P then X else Y construction, which generalizes Coq's construction if b then X else Y to discriminate over a proposition P as opposed to a boolean value b. The If construct leverages (strong) classical logic. It is provided by the TLC library, just like the tactic case_if which is convenient for performing the case analysis on whether P is true or false.

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

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

Case L = nil. By definition of MList, we have p = null. To exploit this property, we can execute rewrite MList_nil, then invoke the CFML 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 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 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.

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

In-place Concatenation of Two Mutable Lists

The function append expects two arguments: a pointer p₁ on a nonempty list, and a pointer p₂ on another list (possibly empty). The function updates the last cell from the first list in such a way that its tail points to the head cell of p₂. After this operation, the pointer p₁ points to a list that corresponds to the concatenation of the two input lists.     let rec append p₁ p₂ =
      if p₁.tail == null
        then p₁.tail <- p₂
        else append p₁.tail p₂

The append function is specified and verified as shown below. The proof pattern is representative of that of many list-manipulating functions, so it is essential that the reader follow through every step of this proof.

The induction principle provides an hypothesis for the tail of L₁, i.e., for the list L₁', such that the relation list_sub L₁' L₁ holds.

To begin the proof, we reveal the head cell of p₁. We let q₁ denote the tail of p₁, and L₁' the tail of L₁.

We then reason about the case analysis.

If q₁' is null, then L₁' is empty.

In this case, we set the pointer, then we fold back the head cell.

Otherwise, if q₁' is not null, we reason about the recursive call using the induction hypothesis, then we fold back the head cell.

Smart Constructors for Linked Lists

We next introduce two smart constructors for linked lists, called mnil and mcons. The operation mnil() creates an empty list. Its implementation simply returns the value null. Its specification asserts that the return value is a pointer p such that MList nil p holds.

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

Observe that the specification triple_mnil does not mention the null pointer anywhere. This specification may thus be used to specify the behavior of operations on mutable lists without having to reveal low-level implementation details that involve the null pointer. The operation mcons x q creates a fresh list cell, with x in the head field and q in the tail field. Its implementation allocates and initializes a fresh record made of two fields. The allocation operation leverages the allocation construct written `{ head := 'x; tail := 'q } in the code. This construct is in fact a notation for an operation called val_new_hrecord_2, which we here view as a primitive operation.

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

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

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

Copy Function for Lists

The function mcopy takes a mutable linked list and builds an independent copy of it, with help of the functions mnil and mcons.     let rec mcopy p =
      if p == null
        then mnil ()
        else mcons (p.head) (mcopy p.tail)

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

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

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

When entering the first branch of the proof after the case analysis, Coq reports on two hypotheses p = null. Actually, these two hypotheses are slightly different. Using Set Printing Coercions. (or Shift+Alt+C in CoqIDE) 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

The function mlength computes the length of a mutable linked list.     let rec mlength p =
      if p == null
        then 0
        else 1 + mlength p.tail

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

Alternative Length Function for Lists

In this section, we consider an alternative implementation of mlength that uses an auxiliary reference cell, called c, to keep track of the number of cells traversed so far. The list is traversed recursively, incrementing the contents of the reference once for every cell.     let rec listacc c p =
      if p == null
        then ()
        else (incr c; listacc c p.tail)

    let mlength' p =
      let c = ref 0 in
      listacc c p;
      !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.

In-Place Reversal Function for Lists

The function mrev takes as argument a pointer on a mutable list, and returns a pointer on the reverse list, that is, a list with elements in the reverse order. The cells from the input list are reused for constructing the output list. The operation is said to be "in place".     let rec mrev_aux p₁ p₂ =
      if p₂ == null
        then p₁
        else (let p₃ = p₂.tail in
              p₂.tail <- p₁;
              mrev_aux p₂ p₃)

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

More Details

Sized Stack

In this section, we consider the implementation of a mutable stack featuring a constant-time access to the size of the stack. This stack structure consists of a 2-field record, storing a pointer on a mutable linked list, and an integer storing the length of that list. The implementation includes a function create to allocate an empty stack, a function sizeof for reading the size, and three functions push, top and pop for operating at the top of the stack.     type 'a stack = {
      data : 'a list;
      size : int }

    let create () =
      { data = 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.

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.

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

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

Exercise: 3 stars, standard, especially useful (triple_push)

Prove the following specification for the push operation.

The pop operation extracts the element at the head of the list, updates the data field to the tail of the list, and decrements the size field.

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

Prove the following specification for the pop operation.

The top operation extracts the element at the head of the list.

Exercise: 2 stars, standard, optional (triple_top)

Prove the following specification for the top operation.

Formalization of the Tree Representation Predicate

In this section, we generalize the ideas presented for linked lists to binary trees. For simplicity, let us consider binary trees that store integer values in the nodes. Just like mutable lists are specified with respect to Coq's purely functional lists, mutable binary trees are specified with respect to Coq trees. Consider the following inductive definition of the type tree. A leaf is represented by the constructor Leaf, and a node takes the form Node n T₁ T₂, where n is an integer and T₁ and T₂ 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.

The heap predicate p ~~~>`{ item := n; left := p₁; right := p₂ } describes a record allocated at location p, storing the integer n and the two pointers p₁ and 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:

• if T is a Leaf, then p is the null pointer,
• if T is a node Node n T₁ T₂, then p is not null, and at location p one finds a record with field contents n, p₁ and p₂, with MTree T₁ p₁ and MTree T₂ p₂ describing the two subtrees.

Alternative Characterization of MTree

Just like for MList, it is very useful for proofs to state three lemmas that paraphrase the definition of MTree. The first two lemmas correspond to the folding/unfolding rules for leaves and nodes.

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.

Additional Tooling for MTree

For reasoning about recursive functions over trees, it is useful to exploit the well-founded order associated with "immediate subtrees". Concretely, tree_sub T₁ T asserts that the tree T₁ 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.

For allocating fresh tree nodes as a 3-field record, we introduce the operation mnode n p₁ p₂, defined and specified as follows.

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

A second specification, derived from the first, asserts that, if provided the description of two subtrees T₁ and T₂ at locations p₁ and p₂, the operation mnode n p₁ p₂ builds, at a fresh location p, a tree described by Mtree [Node n T₁ T₂] 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.

Tree Copy

The operation tree_copy takes as argument a pointer p on a mutable tree and returns a fresh copy of that tree. It is defined in a similar way to the function mcopy for lists.     let rec tree_copy p =
      if p = null
        then null
        else mnode p.item (tree_copy p.left) (tree_copy p.right)

Exercise: 3 stars, standard, optional (triple_tree_copy)

Prove the specification of tree_copy.

Computing the Sum of the Items in a Tree

The operation mtreesum takes as argument the location p of a mutable tree, and it returns the sum of all the integers stored in the nodes of that tree. Consider the implementation that traverses the tree, using an auxiliary reference cell to maintain the sum of all the items visited so far.     let rec treeacc c p =
      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

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.

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.

Verification of a Counter Function with Local State

This section is concerned with the verification of counter functions, which feature internal, mutable state. A counter function f is a function that, each time it is called, returns the next integer. Concretely, the first call to f() returns 1, the second call to f() returns 2, the third call to f() returns 3, and so on. A counter function can be implemented using a reference cell, named p, that stores the integer last returned by the counter. Initially, the contents of the reference p is zero. Each time the counter function is called, the contents of p is increased by one unit, and the new value of the contents is returned to the caller. The function create_counter produces a fresh counter function. Concretely, create_counter() returns a counter function f independent from any other previously existing counter function.     let create_counter () =
       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.

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. Most importantly, 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 comes as a direct 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

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.

Let us move on to the presentation of more abstract specifications. The goal 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.

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

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

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

Finally, let us illustrate how a client might work with counter functions.     let test_counter () =
       let c₁ = create_counter () in
       let c₂ = create_counter () in
       let n₁ = c₁() in
       let n₂ = c₂() in
       let n₃ = c₁() in
       n₂ + n₃

Exercise: 2 stars, standard, optional (triple_test_counter)

Prove the example function manipulating abstract counters. In the specification below, the \∃ H, H part corresponds to the two counters, which we currently have no way of deallocating. The necessary mechanism for garbage collection will be introduced later in Affine. Hint: use xapp triple_create_counter_abstract and xapp triple_apply_counter_abstract to invoke the specifications.

Optional Material

Specification of a Higher-Order Repeat Operator

Consider the higher-order iterator repeat: a call to repeat f n executes n times the call f().     let rec repeat f n =
      if n > 0 then (f(); repeat f (n-1))

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.

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.

The above line can be made more concise using the TLC tactics applys_eq, a variant of apply that automatically introduces the necessary equalities: applys_eq G. { f_equal. math. } { math. }. We then carry a proof by induction: during the execution, the value of m decreases step by step down to 0.

We reason about the call to f

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

The operation miter takes as argument a function f and a pointer p on a mutable list, and invokes f on each of the items stored in that list.     let rec miter f p =
      if p ≠ null then (f p.head; miter f p.tail)

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.

For exploiting the specification triple_miter to reason about a call to miter, it is necessary to provide an invariant I of type list val → hprop, that is, of the form fun (K:list val) ⇒ .... This invariant, which cannot be inferred automatically, should describe the state at the point where the iteration has traversed a prefix K of the list L. Concretely, for reasoning about a call to miter, one should exploit the tactic xapp (triple_miter (fun K ⇒ ...)). An example appears next.

Computing the Length of a Mutable List using an Iterator

The function mlength_using_miter computes the length of a mutable list by iterating over that list a function that increments a reference cell once for every item.     let mlength_using_miter p =
      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.

A Continuation-Passing-Style, Factorial Function

This section and the next one present examples of functions involving "continuations". As a warm-up, we first consider consider a function that does not involve any mutable state. The function cps_facto_aux n k performs a call of the function k on the value facto n. The function cps_facto n computes the value of facto n by applying cps_facto_aux to the identity function.     let rec cps_facto_aux n k =
      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)

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, use the syntax xapp (>> IH F₂) to specify the function F₂ that describes the behavior of the continuation k₂. 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).

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.

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

This section presents an example verification of a function involving "continuations". The function cps_append is similar to the function append presented previously: it also performs in-place concatenation of two lists. The main difference is that it is implemented using an auxiliary recursive function in "continuation-passing style" (CPS). The presentation of cps_append p₁ p₂ is also slightly different: this operation returns a pointer p₃ that describes the head of the result of the concatenation. In the general case, p₃ is equal to p₁, but if p₁ is the null pointer, meaning that the first list is empty, then p₃ is equal to p₂. The code of cps_append involves the auxiliary function cps_append_aux p₁ p₂ k, which invokes the continuation function k on the result of concatenating the lists at locations p₁ and p₂. Its code appears at first quite puzzling, because the recursive call is performed inside the continuation. It takes a good drawing and at least several minutes to figure out how the function works.     let rec cps_append_aux p₁ p₂ k =
      if p₁ == null
        then k p₂
        else cps_append_aux p₁.tail p₂ (fun r ⇒ (p₁.tail <- r); k p₁)

    let cps_append p₁ p₂ =
      cps_append_aux p₁ p₂ (fun r ⇒ r)

The goal is to establish the following specification for cps_append.
  Lemma triple_cps_append : ∀ (L₁ L₂:list val) (p₁ p₂:loc),
    triple (cps_append p₁ p₂)
      (MList L₁ p₁ \* MList L₂ p₂)
      (funloc p₃ ⇒ MList (L₁++L₂) 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.

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