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 heap_ctx.