Ownership, borrowing, and affine protocols

The finite calculus has owned, unavailable, shared-set, and exclusive-stack states; lexically nested begin/end commands; move, drop, read, write, and sequencing. Runtime agreement includes the current lifetime stack. The locally proved results are one-command preservation with a unique realized step, finite-sequence progress and preservation, and the no-use-after-move and empty-stack no-dangling corollary (lemma 46.4, theorem 46.5, corollary 46.6). The token elaboration simulates each protocol command at the signatures in proposition 46.7.

Affe has constrained unrestricted, affine, and linear kinds, ordered environment splitting, suspended and active borrow bindings, explicit region levels, and a fuel-bounded definitional evaluator. The imported endpoint is Radanne–Saffrich–Thiemann Theorem 5.1, expanded as Theorem G.6: successful evaluation preserves the typed store, permissions, frame, shared reachable cells, active-borrow liveness, resource accounting, and fresh-allocation boundary. The chapter attributes no separate small-step progress or preservation theorem to this source.

The simplified monomorphic call-by-need uniqueness calculus owns imported progress and preservation (paper Theorems 1–2) and the technical report’s shared_function proof lemma. The source supplies a detailed Coq-oriented proof report, not a recovered mechanization. Futhark’s consuming pure update and alias restriction are compiler-design evidence, not an end-to-end correctness theorem.

At the extended paper’s call-by-need Linear Haskell signature with two executions and association, the published results are denotational strong confluence, well-typedness implies initial association, and safe-final mutative configuration implies empty global memory (theorem 46.14).

Safe progress for both executions and association bisimulation are conjectures (definition 46.15). Preservation of safety is conditional on bisimulation. Mutative behavior uniqueness is conditional on bisimulation and the proved denotational diamond. No unconditional complete safety, mutative confluence, purity, or behavior-uniqueness theorem is recorded.

Oxide v4 owns progress (Lemma 3.1), preservation (Lemma 3.3), and closed type safety (Theorem E.70) at its region/loan/store signature. Borrow Logic owns the BoCa Fundamental Property (Lemma 3.1), weakest-precondition adequacy (Theorem 3.2), and closed-unit termination with empty memory (Corollary 3.3). Neither card transfers to Pure Borrow or Affe.

The Kappa companion checks six finite protocol traces. It does not execute memory updates or imported implementations and proves none of the results in this ledger. The archived Pure Borrow records preserve the version-one scheduler defect and its fixed history; that engineering record proves no metatheoretic conjecture.