Perennial is using gen_heap for purely ghost state, and IMO the library does not work very well for that, in particular since it is a "singleton library" -- the gname is hidden in a typeclass, and if you have more than one instance around you need to always explicitly pass an implicit argument to make it pick the right one. This is not a problem for the intended usecase where there is only one instance.
I was surprised how this even came to be, but to be fair, the comments in gen_heap are not really clear about this -- we tacitly assumed that "heap" could only ever mean "physical heap" since we never used that term for ghost state, but if people think of "ghost state of type gmap" as a "ghost heap", then trying to use this library makes perfect sense. So this extends the comment in gen_heap to clarify the intended use of this library.
The proper replacement for gen_heap is described in #358 (closed), but until then I propose we point users to the gmap_view RA.
While at it, I also renamed gen_heap_ctx, which I think got its name way back when this was still put into an invariant because there was not yet a state interpretation. This use of the _ctx suffix is in conflict with e.g. lft_ctx in the lifetime logic, where it means "persistent assertion that everything assumes is in the context everywhere".
@tchajed I'd be interested in your feedback here.