Concurrent separation logic and Iris

The interface of chapter 45 uses Iris propositions, internal entailment ${⊢}_{\mathsf{I}}$, separating conjunction, the later modality, masks $E$, and namespace-indexed invariants. Its complete selected update fragment uses the closing token The selected laws are The final law requires $\uparrow N\subseteq E$. A physically atomic expression admits the following mask change:

For the authoritative counter, validity and its selected update are $$\bullet m\cdot \circ n\text{ valid}⟺n\le m,\bullet m\cdot \circ n{⇝}_{\mathsf{fp}}\bullet (m+1)\cdot \circ (n+1).$$ Saved proposition ownership satisfies $${\mathsf{saved}}_{\gamma }^{d_1}(P)\ast {\mathsf{saved}}_{\gamma }^{d_2}(Q){⊢}_{\mathsf{I}}▹(P⊣{⊢}_{\mathsf{I}}Q)$$ when the shares are compatible. The later guards the higher-order payload. The exact physical increment contract is $$⟨⟨\mathrm{\forall }v\in \mathbb{Z}.\ell {\mapsto }_{\mathsf{h}}v⟩⟩{\mathsf{incr}}_{\mathsf{phy}}\ell @\varnothing ⟨⟨\ell {\mapsto }_{\mathsf{h}}(v+1)\mid \mathsf{RET}v⟩⟩.$$ Load and failed CAS take the abort continuation. Successful CAS takes the commit continuation and witnesses $v{⟶}_{\mathsf{a}}v+1$.