Ownership, Borrowing, and Affine Resource Protocols

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Let $b$ be the sole handle of an allocated buffer. Affine typing accepts the transfer $$\mathsf{send}b$$ because the continuation does not use $b$. It rejects $$\mathsf{let}n=\mathsf{length}b\mathsf{in}\mathsf{send}b,$$ because the call to $\mathsf{length}$ consumes the handle before $\mathsf{send}$ receives it. Copying $b$ would make the second call typable, but would also create two handles with deallocation authority. The missing operation must expose less authority for a bounded interval and then restore the sole owner.

A finite ownership protocol

The first calculus isolates that interval. It is small enough that every transition and every metatheoretic case can be written on the page. Its progress argument identifies the exact invariant needed by the larger language comparison.

The word owner denotes the handle in state $\mathsf{O}(A)$; it is the only handle permitted to transfer or destroy its payload. A shared borrow is read authority indexed by one member of $B$. An exclusive borrow is read–write authority indexed by the top of $\overline{\alpha }$. These names describe static authority, not the number of machine pointers. The picture breaks if raw pointer equality is taken to be ownership: several shared views may contain the same address while none may deallocate it.

Commands change protocol environments. We write $\mathcal{L};\mathrm{\Omega }⊢c\Rightarrow {\mathcal{L}}^{\prime };{\mathrm{\Omega }}^{\prime }$. In $\mathsf{move}h\mathsf{as}k$, the handle $k$ is fresh. In every begin command, the lifetime is fresh for $\mathcal{L}$; in every end command, it is the top of $\mathcal{L}$.

The set and the stack in definition 46.1 perform different work. Shared scopes may be nested while the same read authority remains available. Exclusive reborrowing suspends the outer exclusive view; only the top lifetime may act.

For shared access, the rejected affine program becomes Its state calculation is The third step, not the read, returns transfer authority.

An exclusive reborrow uses a stack: The middle action may write through $\beta$. The outer view for $\alpha$ is suspended at that point because $\beta$ is the top lifetime.

Dynamics and safety

A runtime resource map $R$ sends a handle to a payload together with one of the same four modes. A moved payload is installed under the fresh destination handle before the source becomes unavailable; dropping destroys the payload. Borrow-begin and borrow-end change only the mode. Reads return the payload and writes replace it. We write $(\mathcal{L},R;c){⟼}_{\mathsf{own}}({\mathcal{L}}^{\prime },R^{\prime };\mathsf{skip})$ for one command transition.

The empty-stack hypothesis is substantive. Stopping after ${\mathsf{beginS}}_{\alpha }h$ leaves a well-typed prefix with an active borrow. It is not a completed scope and does not satisfy the corollary’s final-state premise.

Token-passing elaboration

The protocol states can be made explicit as affine values. Let ${\mathsf{Cap}}_h(q)$ be an affine token for handle $h$ in state $q$, and let $\mathsf{Life}(\mathcal{L})$ be an affine token for the current lifetime stack. If the ordered domain of $\mathrm{\Omega }$ is $h_1,\dots ,h_m$, define $$\mathcal{R}(\mathcal{L};\mathrm{\Omega })=\mathsf{Life}(\mathcal{L})\otimes {\mathsf{Cap}}_{h_1}(\mathrm{\Omega }(h_1))\otimes \cdots \otimes {\mathsf{Cap}}_{h_m}(\mathrm{\Omega }(h_m)).$$ The target has one proof-indexed affine primitive for each non-sequencing rule of definition 46.2. Representative signatures are Each primitive exists only when the corresponding source premises hold. Thus there is no move constant without a fresh destination and no end constant for a lifetime other than the stack top. Read and write constants preserve the state token; drop, the two shared end rules, and the two exclusive end rules have exactly the source conclusions. Their target reduction contracts $\hat{c}r$ to the canonical representation of the conclusion. The proof-directed translation $\mathcal{E}$ maps a primitive source derivation to its indexed constant and maps Seq to affine composition.

This is an explicit elaboration of the finite protocol derivation into affine state tokens. It does not erase the protocol indices and is not a compiler-correctness theorem for Affe, Rust, or Pure Borrow.

The Affe foundation

Affe is an impure, strict ML-like language with unrestricted, affine, and linear kinds and both shared and exclusive borrowing. Its internal language uses explicit regions. The book freezes the part of that signature needed to explain the opening program; it does not replace Affe’s full constrained polymorphism by the finite protocol calculus.

The region and borrow rules are

The auxiliary relation $C{⊢}_x\mathrm{\Gamma }{⇝}_{\mathsf{reg}}{\mathrm{\Gamma }}^{\prime }$ replaces the selected suspended binding by a borrow binding whose kind is confined to level $n$. The result-kind premise excludes that level, so neither the borrow nor a closure containing it can leave the region.

The opening application is typed by splitting the environment so that its left side contains $[b:\mathsf{Buffer}{]}_{\mathsf{S}}^1$ and its right side contains $b:\mathsf{Buffer}$. Rule Region activates the suspended binding only around . After that region returns an integer, the right subexpression sends the owner.

Affe states soundness for a fuel-bounded definitional evaluator rather than a small-step progress–preservation pair. The distinction matters.

The theorem implies the precise no-use-after-free property recorded by its permission clauses: evaluation can access an address only while its permission is present, and the result clauses keep borrowed reachable cells live. The Region result-kind premise gives the no-dangling property. The source does not state a separate small-step progress theorem or preservation theorem, so neither is attributed to Affe here. A timeout is the evaluator’s fuel result, not a stuck well-typed term. Affe’s inference soundness, completeness, and principality are separate Theorems 4.1, 4.4 and Appendix E; they are not needed for the borrowing argument.

Uniqueness is not temporary authority

Let ${\mathsf{replace}}_i(a,v)$ denote the pure array that equals $a$ except at index $i$. If $a$ has no aliases, a compiler may implement this value by overwriting $a[i]$. If $b=a$ remains observable, the same machine choice changes $b[i]$ and fails to implement the pure operation. The required fact is absence of aliases, not permission to ignore a variable.

No mutable store occurs in this theorem. It therefore does not prove that the destructive array implementation is correct, and it does not give a lifetime, a lender, or reclamation. Affinity says at most one use of a handle; uniqueness says that a value has no aliases at the relevant program point; ownership grants a distinguished authority; borrowing suspends part of that authority temporarily. Clean’s full mutable language contains further rules and is not the calculus of theorem 46.11.

Futhark makes the compiler-facing distinction concrete. Its expression $$a\mathsf{with}[i]=v$$ is semantically a pure array update. The operation consumes $a$; neither $a$ nor a variable that aliases it may be used on the continuation path. The compiler may then choose an in-place write. The rejected program $$\mathsf{let}b=a\mathsf{in}\mathsf{let}{a}^{\prime }=a\mathsf{with}[i]=v\mathsf{in}(a^{\prime },b[i])$$ keeps an alias observable after consuming $a$. This is the uniqueness and alias-analysis contract documented in §3 of the PLDI 2017 paper and the “In-Place Updates” section of the pinned Futhark book [HSE^+17]. It is not an end-to-end compiler-correctness theorem and transfers no borrowing result.

Pure Borrow: theorem, conjecture, and artifact

Pure Borrow is a 2026 Linear Haskell library and formal calculus. Its status is part of the mathematics: three results are published as theorems, two load-bearing claims are conjectures, and two further results are conditional on one conjecture.

The library interface

A lifetime is atomic, static, or an intersection: $$\alpha ,\beta ::=\mathsf{Al}\iota \mid \mathsf{Static}\mid \alpha \wedge \beta .$$ Lifetime inclusion $\alpha ⊑\beta$ has intersection as meet and $\mathsf{Static}$ as top. The paper-facing core signatures are The final evaluated implementation’s lower layer exposes $\mathsf{newLifetime}:\mathsf{Linearly}⊸\mathsf{SomeNow}$, $\mathsf{endLifetime}:{\mathsf{Now}}^{\alpha }⊸\mathsf{Ur}({\mathsf{EndToken}}^{\alpha })$, and $\mathsf{execBO}:{\mathsf{BO}}^{\alpha }a⊸{\mathsf{Now}}^{\alpha }⊸({\mathsf{Now}}^{\alpha }\otimes a)$. Here $\mathsf{SomeNow}$ existentially packages a fresh atomic lifetime; the persistent end token implements the paper-facing ${\mathsf{End}}^{\alpha }$ evidence. These are two interface layers, not interchangeable signatures. Mutable borrowers and live lifetime tokens are linear. A shared borrower is movable and may be duplicated. A lender is linear; reclamation also needs persistent evidence that its lifetime ended. Hence ownership returns without collecting each borrower as a runtime value.

For the vector $[0,1,2]$, borrow once, perform the updates $0+=3$, $2+=5$, and $0\ast =4$, share the mutable borrower to copy position $0$, end the lifetime, and reclaim. The pure result is $(12,[12,1,7])$. The lender cannot be reclaimed before the ${\mathsf{End}}^{\alpha }$ evidence exists; the mutable borrower cannot be used after $\mathsf{share}$ consumes it.

The typing trace keeps each linear handoff visible: The body therefore has type ${\mathsf{BO}}^{\alpha }({\mathsf{End}}^{\alpha }\to (\mathsf{Int}\otimes \mathsf{Vector}\mathsf{Int}))$, which is exactly the input expected by $\mathsf{runBO}$. This is a typing/evaluation trace for the published example, not a replay of its Haskell implementation.

Reborrowing is derived by borrowing a mutable borrower and flattening: $${\mathsf{Mut}}^{\alpha }a⊸{\mathsf{Mut}}^{\alpha \wedge \beta }a\otimes {\mathsf{Lend}}^{\beta }({\mathsf{Mut}}^{\alpha }a).$$ The inner borrower is confined to $\alpha \wedge \beta$. Reclaiming its lender with ${\mathsf{End}}^{\beta }$ returns the outer mutable borrower.

Parallel quicksort splits a mutable vector borrower into disjoint slice borrowers, partitions in $\mathsf{BO}$, and evaluates the recursive calls with $\mathsf{parBO}$. Each base case consumes its slice borrower; after both branches finish, the outer lender from the initial whole-vector borrow is reclaimed. The work-stealing version changes the scheduler, not these public types. This is a case study in implementability, not a theorem about scheduler correctness.

The formal calculus and its two executions

The mutative semantics has configurations $M=(H;\mu ;x)$: a lazy binding heap $H$, global memory $\mu$, and result variable $x$. Representative rules allocate a fresh location, update $\mu (\ell )$, and free $\ell$. We write $M{⟼}_{\mathsf{m}}{M}^{\prime }$.

The denotational semantics has configurations $D=(G;x)$, with no global memory. A borrow receives a fresh identifier $\iota$. Each update appends or replaces the entry for its borrow path in a finite history $\eta$. Ending a lifetime moves $\eta$ to its dead token, and reclamation restores the lender’s value by replaying the final history. We write $D{⟼}_{\mathsf{d}}{D}^{\prime }$. Thus the two rule tables differ exactly at state: The table records the state-changing clauses; the complete calculus also has the shared call-by-need context and operator rules.

The dependency boundary is The last two implications are conditional corollaries. The diamond theorem alone says nothing about a mutative execution, and association alone is not left-unique. There is therefore no unconditional complete safety, purity, or behavior-uniqueness theorem to import.

The version-one scheduler failure

The first public Zenodo record reported a race in the work-stealing API. Its scheduler assumed an invalid timing invariant and could, with low probability, return a partially unsorted array. The repaired source used a global atomic counter to decide completion. That repair changed only Control.Concurrent.DivideConquer.Linear and its submodules; it did not change the core borrowing interface. It also reduced performance. The record contains the original source and images, fixed source and images, and a replacement benchmark plot. The later PLDI and final Zenodo revisions contain the repair.

This history separates four claims. A type-correct client can be written with the API. The original scheduler had a race. The atomic-counter revision fixes the reported completion condition in the evaluated artifact. None of these facts proves the conjectured bisimulation or purity of the unsafe internals.

Two exact neighboring boundaries

Oxide v4 uses regions, loans, non-lexical stacks, numeric paths, and an imperative store. Its Lemmas 3.1 and 3.3 establish progress and preservation, and Theorem E.70 gives closed-program type safety at that exact signature [WGPA21]. Oxide’s region/loan invariant is mature evidence for an imperative Rust-shaped calculus. It does not prove Pure Borrow’s association conjectures, and its store theorem is not a theorem about Affe’s fuel-bounded evaluator.

The Borrow Calculus of Wagner–Gierczak–Marshall–Li–Ahmed begins with a linear language and derives immutable borrows, lexical lifetimes, reborrowing, and mutable borrows without adding runtime borrowing operations. Its exact endpoints are the Fundamental Property (Lemma 3.1), weakest-precondition adequacy (Theorem 3.2), and closed-unit termination with empty final memory (Corollary 3.3) [WGM^+25]. Borrow Logic proves those results for BoCa through a semantic model. It is neither an elaboration of Pure Borrow nor a proof of the conjectures in definition 46.15.

Fractional permissions divide access quantitatively; separation logic divides heap assertions; regions delimit validity. A translation from any of these systems would have to map its states, typing rules, and dynamics and then prove preservation or simulation. No such map is assumed here. Full Rust, unsafe code, concurrency libraries, and arbitrary mutation lie outside this chapter’s theorem boundary.

Source boundary.

Affe’s exact full theorem is Theorem 5.1 and Appendix G of [RST20]. The uniqueness results are bounded to the monomorphic calculus and proof report of [dVPA08]. The Futhark comparison is a language/compiler design claim from [HSE^+17], not a compiler proof. The Pure Borrow theorem/conjecture split and the association proof sketches are from the extended v4 source of [MI26]; the final evaluated artifact is recorded separately in subsubappendix E.3.21. The BoCa and Oxide comparisons retain the signatures of [WGM^+25, WGPA21]. No result transfers between these calculi without an explicit translation theorem.

All 7 Chapter 46 corpus cases passed.