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, albeit with no way to predict what is going to be read. 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.