Remove predicative invariants

[gebner]

This PR contains a number of cleanings that bring the PulseCore formalization closer to our written account.

• Predicative invariants are removed, including the meta flag on cells.
• The high water mark sinks to Heap.heap (as described in Section 3.1)
• The free_above predicates are removed (made possible by sinking the high water mark)
• Actions no longer have allocation flags and pure pre/postconditions (also made possible by the sinking)
• BaseHeapSig.mem no longer needs to add counters and is defined directly as Heap2.heap
• The heap extension mechanism is removed, instead we use Heap2.heap u#3 as the timeless heap and store small values using Pulse.Lib.PCM.Raise
• Heap signatures are removed too (they didn't fit the impredicative heap anyhow)

In total, the PulseCore LOC count shrinks by 35%. The CI runtime decreases by roughly 10%.

Removing predicative invariants does not significantly reduce the expressivity of PulseCore: impredicative invariants storing timeless predicates offer the same API as the predicative invariants on the lowest level. I expect most nested invariants can be encoded with flags (like cancellable invariants).