Semantic Invariants

This merge request adds an additional version of invariants to Iris. In proofs, it is sometimes useful to have an invariant which contains for example knowledge of multiple locations, say a ↦ 3 * b ↦ 5. When opening this invariant in a proof, for example to read from a, we have to reason about both a and b instead of just a. Furthermore, if we have already verified some code which expects a ↦ 3 as an invariant, we cannot reuse that proof because our invariant guarantees more. The semantic invariants included in this MR allow the weakening of an invariant P to accessors of P. In the above example, this means we can obtain an invariant a ↦ 3. The semantic invariant P and an accessor Q which has been derived from P cannot be opened at the same time, as this would lead to inconsistencies.

In essence, the definition of a semantic invariant requires that the lemma that is used to open standard invariants holds persistently. The standard lemmas concerning invariants still hold for semantic invariants, they can be created from traditional invariants, and weakening, as described above, holds.