A stratified heap with two universes, enabling storing "small" heap predicates in the larger heap

[nikswamy]

This PR enriches the memory model of Pulse to use PulseCore.TwoLevelHeap

The underlying memory now contains the following:

• A small heap, storing objects in universe 1
• A large heap, storing objects in universe 2

A pair of a small heap and a large heap is called a TwoLevelHeap, or H2.heap.
The core Pulse.Lib.Core.vprop is now an affine H2.heap -> prop, where vprop : Type u#3

(We also have an invariant store in PulseCore.Memory, storing slprop as invariants, this is mostly unchanged, except for a universe level increase, and some other cleanup, notably, directly using PulseCore.MonotonicStateMonad in a universe-polymorphic way, rather than using FStar.MSTTotal, which fixes the state to be in universe 1.)

We also have two functions

• down : vprop -> small_slprop and
• up: small_slprop -> vprop, where small_slprop : Type u#2
  And a predicate is_small (p:vprop) = up (down p) == p
  That is, vprop validating is_small can be coerced to small_slprops without loss of information, and then coerced back.

Most familiar predicates are small, e.g, emp, pure, pts_to, ghost_pts_to etc.
The connectives ** and exists* form small vprops if their arguments are also small.

But, we now also have Pulse.Lib.BigReference.pts_to (#a:Type u#2) (x:ref a) (#p:perm) (v:a) : vprop that allows storing terms in universe 2 in the heap, including, notably small_slprop.

An example PulseExample.UseBigRef shows how it works, storing list of closures packed with small vprops denoting their pre and postconditions.

Note, we also have Pulse.Lib.BigGhostReference, for a ghost variant of a reference to store a universe 2 term.

I plan to add one more level to the heap, this one to turn any slprop into a resourceful invariant---so, expect one more universe bump.

[nikswamy]

Note, this commit gives a sense of the changes incurred in the Pulse checker and libraries for a universe bump:

e8c7e6d

It's relatively small. If F* had a way to declare top-level universe constants, e.g., let universe mem_level = u#3, then we could possibly isolate the edit to just changing this constant.