WIP: Add heap_lang lib for "GC locations": locations that can never be deallocated
A "GC" location is a location that can never be deallocated explicitly by the program. It provides a persistent witness that will always allow reading the location. The location is moreover associated with a (pure, Coq-level) invariant determining which values are allowed to be stored in that location. The persistent witness cannot know the exact value that will be read, but it can know that the value satisfies the invariant.
This is useful for data structures like RDCSS that need to read locations long after their ownership has been passed back to the client, but do not care what it is that they are reading in that case.
Note that heap_lang does not actually have explicit dealloaction. However, the proof rules we provide for heap operations currently are conservative in the sense that they do not expose this fact. By making "GC" locations a separate assertion, we can keep all the other proofs that do not need it conservative.