Concurrent separation logic and Iris metatheory

Frozen signatures.

The physical machine is HeapLang at pinned Iris commit 832a5cd28048a8af53a7eddb1f4d4bb5c002efe0. A configuration contains a thread pool and a finite heap. Its primitive compare-and-swap performs the comparison and conditional write in one physical reduction. The logical signature contains Iris propositions, separating conjunction, later, affinely, persistently, named invariants, fancy updates, weakest preconditions, and ownership of resource-algebra elements. Only the mask-changing invariant and atomic-expression rules displayed in subappendix A.45 are used. O’Hearn’s disjoint-concurrency and resource rules are fixed by Sections 3–5 of [O'H07]; Brookes’s trace semantics, soundness, and race-freedom results are Sections 4, 8, 12, and 13 of [Bro07]. They justify the foundational ownership-transfer obstruction but are not theorem premises for HeapLang.

Verified theorem signatures.

Physical increment.

$⟨⟨\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⟩⟩$. This is mechanized as incr_phy_spec in iris_heap_lang/lib/increment.v:22–41.

Atomic-heap increment.

$\mathsf{heap}\mathsf{\_}\mathsf{inv}$ entails the corresponding atomic-heap contract at $\mathsf{atomic}\mathsf{\_}\mathsf{heapN}$. This is mechanized as incr_spec in the same file at lines 104–127.

Concrete client.

$\mathsf{heap}\mathsf{\_}\mathsf{inv}-\ast {\mathsf{WP}}_{\mathrm{\top }}\mathsf{incr}\mathsf{\_}\mathsf{client}x\{u.\mathsf{True}\}$. This is mechanized as incr_client_safe in the same file at lines 175–196. The client calls incr, not incr_phy.

Higher-order ghost payload.

Compatible shares of ${\mathsf{saved}}_{\gamma }^d(P)$ agree on their proposition one logical step later. Discarded ownership is persistent, and full ownership can be updated. These are saved_prop_agree, saved_prop_dis­carded_persistent, and saved_prop_update in iris/base_logic/lib/saved_prop.v:148–218.

HeapLang adequacy.

Completed main values satisfy the selected postcondition. At $\mathsf{NotStuck}$, every expression in every reachable thread pool is a value or reducible. In iris/program_logic/adequacy.v, the exact locators are adequate at lines 181–189 and adequate_tp_safe at lines 202–215. The declaration heap_adequacy is at iris_heap_lang/adequacy.v:25–48.

Proof dependencies.

The increment proof uses Löb induction, exclusive points-to, physical load and CAS rules, and the abort/commit interface of atomic updates. The client proof additionally uses allocation, a client invariant, persistence, the atomic-heap increment specification, and parallel composition. Adequacy is a separate semantic theorem; the Kappa trace checker does not prove it. The invariant interface is pinned separately at iris/base_logic/lib/invariants.v:97–133.

Excluded conclusions.

No displayed theorem establishes termination, fairness, starvation freedom, weak-memory correctness, a final counter value for the $\mathsf{True}$-postcondition client, or generalized compositional linearizability. The exchanger proposition is a finite impossibility result for independent unary deterministic functions, not a transfer of a theorem from another linearizability logic.