F* Heap Model

Overview

We have recently implemented a new heap model in F*. The model introduces a few changes in the FStar.Heap interface. This page summarizes the heap model, and the differences from the previous interface.

Heap and refs

The model implements heap as a map from addresses of type nat to a sigma type a:Type0 & a. The heap also maintains a source of freshness, i.e. the next address to use when allocating a new reference.

A reference is an (abstract) record containing an address, and a couple of more fields. A function Heap.addr_of returns the address for a reference.

The heap interface provides (abstract) functions sel, upd, contains equal, and equal_dom as before (with the same signatures).

Differences from the previous heap model

• Modifies clauses

The signature of modifies is now: set nat -> heap -> heap. Specifically, the first argument is a set of addresses, and not a TSet Heap.aref as before. Each heap model FStar.Heap, FStar.HyperHeap, and FStar.HyperStack, exports functions to get addresses of corresponding refs: addr_of, addr_of, and as_addr (in the same spirit as as_aref) respectively.

• Use unused_in instead of ~ contains

In the new heap model, ~ contains does not indicate freshness. E.g. ~ contains r h0 h1 does not mean that r was not allocated in h0 (the intuition is that our heap model also supports strong updates (i.e. type changing updates), and ~ contains could also mean that the reference contains a value that is not consistent with the reference's type). Therefore avoid using ~ contains and instead use unused_in which has the signature: #a:Type -> ref a -> heap -> Tot bool.

All our libraries that defined their own contains version (such as HyperHeap, HyperStack, Buffer, etc.) also now define corresponding unused_in versions.

For new code, it would be better to write fresh r h0 h1 instead of unused_in r h0 /\ contains r h1, as fresh hides this inside a single predicate (which is easier to read).

• Injectivity of ref

Previously we had an axiom: forall (a:Type) (b:Type). ref a === ref b ==> a == b. This means that if we know a =!= b, then we can immediately derive ref a is not equal to ref b, and that gave us some form of framing. Specifically, if we know that modifies r h0 h1, and r: ref a, then for some reference s:ref b where a =!= b, sel h0 s == sel h1 s.

In the new heap model, we get ref injectivity but that does not give us the framing, because the heap is a map from addresses, and two refs not being equal does not mean their addresses are not equal.

However, we do get a distinctness lemma for addresses, if we can show that both the refs are contained in the heap, essentially:

let lemma_distinct_addrs_distinct_types
  (#a:Type) (#b:Type) (h:heap) (r1:ref a) (r2:ref b)
  :Lemma (requires (a =!= b /\ h `contains` r1 /\ h `contains` r2))
         (ensures  (addr_of r1 <> addr_of r2))
	 [SMTPatT (h `contains` r1); SMTPatT (h `contains` r2)]
  = ()

So if you would like to get framing in the new heap model based on the types of the references, make sure that you have contains for both the references in the context.