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)]
  = ()

Just something to keep in mind.