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 value of some type, i.e., the sigma type a:Type0 & a, a pair of some type a (in universe 0) and a value of that type. In effect, the heap is a heterogeneous map from addresses to values, each of which may have a different type. This is important inasmuch as one clearly wants to store values of different types in the heap.

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.

• Decidable equality on ref

In the previous model, the type ref a came with an axiom for decidable equality on ref a, i.e. forall x. hasEq (ref a), where hasEq predicate says that the type ref a has decidable equality.

In the new heap model, we do not have decidable equality on the ref type. Instead one needs to use propositional equality or heterogeneous equality (see Different types of equalities in F*).

But also note that inequality of refs does not provide much in the new heap model. For example, in the previous model if we knew r1 =!= r2 then we could derive sel h r1 =!= sel h r2, not in the current heap model. Again, because the heap is a map from addresses and r1 =!= r2 does not mean that their addresses are different.

Instead in the new heap model, inequality of addresses is much more useful (i.e. addr_of r1 <> addr_of r2).