State invariants in WP and the dead of heap_ctx.
This merge request changes the WP construction so that it takes state interpretation as its parameter (part of the
irisG type class), instead of building in the authoritative ownership of the entire state. When instantiating WP with a concrete language, one can choose the state interpretation. For example, for
heap_lang we directly use
auth (gmap loc (frac * dec_agree val)), and avoid the indirection through an invariant managing ownership of the entire state.
As a result, we no longer have to carry around