appendix sectionnotation

Concurrent separation logic and Iris notation

$P ⊢_{I} Q$ , $P ⊣ ⊢_{I} Q$ .: Internal Iris entailment and equivalence. They are used only for Iris propositions and are distinct from the model entailment of chapter 44.
$⟨ aff ⟩ P$ , $◻ P$ .: The affinely and persistently modalities. The box means duplicable Iris ownership here, not a modal necessity in an object language.
${inv}_{N} (P)$ .: The invariant named in namespace $N$ . The name controls opening; it is not a program variable.
$| = E_{1}, E_{2} = > P$ .: A fancy update from mask $E_{1}$ to mask $E_{2}$ . Masks list enabled invariant names; $↑ N$ is the set belonging to namespace $N$ .
${WP}_{E} e {v . Φ (v)}$ .: HeapLang weakest precondition at mask $E$ . It asserts partial correctness and non-stuckness, not termination.
${own}_{γ} (a)$ .: Ghost ownership at name $γ$ . This is a logical resource; it adds no physical HeapLang cell.
${saved}_{γ}^{d} (P)$ .: Share $d$ of a saved Iris proposition. Its payload is guarded by a logical later step; a discarded share is persistent.
$∙ m$ , $\circ n$ .: An authoritative counter and a lower-bound fragment. The bullets are resource constructors, not term syntax.
$a ⇝_{fp} b$ .: A frame-preserving ghost update. It preserves compatibility with every frame and is not a machine step.
$ℓ \mapsto_{h} v$ .: Exclusive physical HeapLang points-to, separate from the atomic-heap interface’s points-to predicate.
$⟶_{p}$ , $⟶_{a}$ .: Physical and abstract one-step transitions. The first changes a machine configuration; the second records a selected logical operation.
$⟨ ⟨ P ⟩ ⟩ e @ E ⟨ ⟨ Q ⟩ ⟩$ .: A logically atomic specification. The double angles package abort and commit continuations; they do not assert that $e$ is one physical step.