Add ghost data to locations

This MR makes it possible to attach "meta" or "ghost" data to locations. This is achieved by adding the following connectives to heap_lang and the gen_heap construction:

• When you allocate a location, in addition to the point-to connective l ↦ v, you also get the token meta_token ⊤ l. This token is an exclusive resource that denotes that no meta data has been associated with the namespaces in the mask ⊤ for the location l.
• Meta data tokens can be split w.r.t. namespace masks, i.e. meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2 if E1 ## E2.
• Meta data can be set using the update meta_token l E ==∗ meta l N x (provided ↑ N ⊆ E, and x : A for any countable A). The meta l N x connective is persistent and denotes the knowledge that the meta data x has been associated with namespace N to the location l.

The advantage of this MR is that we can get much cleaner specs for ADTs. Currently, most specs expose some ghost name γ (or big tuple of ghost names) that is used for naming the ghost state used in the definition of the representation predicates. Using this MR, these ghost names γ can he hidden entirely, by associating them as meta data to the location l.

To make the system as flexible as possible, the x : A in meta l N x can be of any countable type A. This means that you can associate single ghost names, but also tuples of ghost names, or any arbitrary stuff you like to a location l.

Moreover, to further increase flexibility, instead of directly requiring the user to give an associated meta value when allocating an location, I have introduced the connective meta_token. This way, one could allocate the location, use some additional abstractions that may create ghost variables, and then change meta_token into meta.

To further extend that, I've indexed the meta l N x and meta_token l E predicates with a namespace N and mask E. That way, one basically has a linked-list of meta connectives. So, when building abstractions, one can gradually assign more ghost information to a location instead of having to do all of this at once.

This MR is much inspired by ghost record fields in tools like Verifast.

An example of an application of this MR is the spin/ticket lock spec, whose spec has become:

{{{ R }}} newlock #() {{{ lk, RET lk; is_lock lk R }}}
{{{ is_lock lk R }}} acquire lk {{{ RET #(); locked lk ∗ R }}}
{{{ is_lock lk R ∗ locked lk ∗ R }}} release lk {{{ RET #(); True }}}

Note that is_lock and locked no longer have a γ as argument. This γ is hidden using meta l nroot γ.