appendix sectionsignatures

Uniqueness and ownership signatures

Barendsen–Smetsers graph uniqueness

Signature and semantics.: The frozen 1996 signature has fixed-arity constructors and functions, variables, sharing lets, simultaneous recursive lets, and left-linear constructor cases. Expressions denote finite rooted equation graphs, including retained garbage equations; source reduction is defined through graph rewriting. Attributed types carry $u$ or $m$ , correction is partial, and graph typing inspects incoming reference counts.
Exact imported results.: The term–graph conventional correspondence, conventional preservation, uniqueness soundness, completeness modulo graph denotation, graph-rewrite typing, source preservation modulo graph equivalence, conventional principal typing, and principal attribution relative to a fixed conventional solution are the results identified in the source paragraph of chapter 47. The chapter reconstructs their decisive sharing, correction, root-rewrite, and factorization cases.
Locally proved boundary.: Theorem 47.19 proves only that an eligible layout-compatible overwrite has the same typed graph interface as allocation and redirection. The 1994 quicksort application supplies the update pattern but not preservation; the 1996 system owns that metatheorem.
Not claimed.: There is no global principal uniqueness theorem, compiler-correctness theorem, cost theorem, concurrent semantics, or result for arbitrary mutation. The later simplified uniqueness calculus is comparison evidence only.

Signature and semantics.: The frozen core has $w ::= x ∣ * w$ , integers, boxes, shared and mutable borrows, partial types, move, copy, assignment, declarations, and blocks. The store semantics uses destructive read and recursive drop. Typing is flow-sensitive and carries store and lifetime parameters.
Exact imported results.: Borrow invariance, progress, whole-term preservation, finite-core type and borrow safety, and the strengthened core borrow-safety corollary have exactly the hypotheses summarized in section 48.3. The terminal preservation theorem does not say that one output environment abstracts every intermediate store.
Termination repair.: The separate simplified termination source supplies linearizable typings, well-founded recursive lookup, and preservation of linearizability by move, drop, declaration, and assignment. The chapter corrects the source’s reversed two-variable ranking example and makes its lexicographic measure explicit. This proves checker termination from the empty typing, not termination of programs after adding loops or recursion.
Not claimed.: Numeric projections and named-field partial moves are a finite extension and artifact model. They are not cases of the frozen core safety proof.

Signature and semantics.: The frozen arXiv-v4 signature has numeric places, dereferencing place expressions, qualified region references, abstract and concrete regions, loan sets, closures, ordered static and runtime frames, temporary continuations, region rewriting, branch union, and administrative $shift$ and $framed$ terms.
Exact imported results.: The chapter states v4 progress, place-expression reduction, preservation, the value-preservation lemma families on which it depends, and type safety. Preservation includes a post-step stack typing, preserved temporaries, a retyped residual expression, region rewriting, and residual output union. Closures and their captured frames are essential proof cases.
Non-lexical and lexical discipline.: ${gc - loans}_{Θ}$ may empty a loan set before its region binding leaves scope, but ordered frames are still popped last-in–first-out. The continuation test prevents collection while an evaluated component still holds the region.
Not claimed.: Oxide v1 and v4 are not interchangeable. V4 has no named-record former. The compiler and differential corpus are tested semantics, not a theorem of equivalence with Rust. The type-safety conclusion permits value, abort, or divergence.