Place Calculi, Partial Moves, and Field-Sensitive Borrowing

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

Let $x$ contain a pair of owned boxes. After moving its first component, the judgment must reject $x.0$ and $x$, yet still accept $x.1$. Rejecting all of $x$ is safe but imprecise; accepting $x$ is unsound. The unit of reasoning is therefore not merely a variable but a place: a root and a path into stored data.

Prefix overlap is necessary but does not determine how a move changes the context. Featherweight Rust answers with destructive reads and lexical lifetimes. Oxide v4 answers with loan sets, continuation-aware collection, and an ordered stack. Their signatures and proofs remain separate.

Places overlap by prefixes

For the field-sensitive presentation, let $$\pi ::=x\mid \pi .i,\rho ,\pi ::=\pi \mid \ast \rho .$$ $\pi$ is a projection path; $\rho$ may additionally dereference a borrow. The frozen Featherweight Rust core below uses only $w::=x\mid \ast w$. Numeric projections in this opening are a conservative artifact extension, not a premise of its theorems.

Thus $x.0{\mathrm{\#}}_{\mathsf{p}}x.1$, while $x{\bowtie }_{\mathsf{p}}x.0$ and $x.0{\bowtie }_{\mathsf{p}}x.0.1$. The relation is symmetric. Separation is not transitive: $x.0{\mathrm{\#}}_{\mathsf{p}}x.1$ and $x.1{\mathrm{\#}}_{\mathsf{p}}x.0.0$, but $x.0{\bowtie }_{\mathsf{p}}x.0.0$.

Featherweight Rust: one frozen ownership core

The core left values, types, and selected terms are $\partial T$ records an unavailable owner position. A mutable store maps variables to values or the undefined marker. A borrow value is a location; a box value is an owning location.

These operations are distinguishable even when they return equal integers: copy preserves future access; move consumes the owner.

Typing is flow-sensitive: $$\mathrm{\Gamma }⊢⟨t:T{⟩}_{\ell }^{\sigma }⊣{\mathrm{\Gamma }}^{\prime }.$$ The input and output environments describe the store before and after $t$; $\sigma$ and $\ell$ carry the stack and lifetime parameters of the frozen system. Lookup follows dereferences. The move rule replaces the target type by its partial form, the assignment rule restores its assigned type, and a declaration extends then removes a lexical binding.

The source core has no named fields, so the next trace belongs to the stated projection extension. It exposes the invariant without enlarging the Featherweight Rust theorem boundary: $${\mathrm{\Gamma }}_0=x:(◻A,◻B)\stackrel{\mathsf{move}x.0}{\to }{\mathrm{\Gamma }}_1=x:(\partial (◻A),◻B).$$ At ${\mathrm{\Gamma }}_1$, reading $x.0$ or the whole $x$ fails, while reading $x.1$ succeeds. A later assignment to $x.0$ restores the complete pair.

Proof of Lemma 48.4 — Projection-local invalidation

Proof. The environment update descends along the selected field path and replaces that leaf by $\partial T$. Lookup of a separated sibling diverges from the updated path at some projection and therefore reads an unchanged component. A prefix or extension of the moved path must traverse the partial marker and is rejected. ◻

The Featherweight Rust safety theorem

A runtime state $S▹t$ is valid when its locations and stack frames are well formed and every owning location is reached from at most one owner. Write $S\sim \mathrm{\Gamma }$ when $\mathrm{\Gamma }$ safely abstracts the store. Environment well-formedness adds the borrow invariant: every borrowed left value is live, well typed, and outlives the borrow that names it.

Proof of Lemma 48.5 — Borrow invariance

Imported proof. This is Lemma 4.9 on printed p. 29 of [Pea21], at the Featherweight Rust state, store-typing, lifetime, and flow-sensitive typing judgments frozen in this chapter. The source proof is the rule induction given in its Appendix 9.2. Its conclusion is exactly the well-formed extension by the fresh anonymous result binding displayed above; it does not assert well-formedness of ${\mathrm{\Gamma }}_2$ after discarding a borrowed result. ◻

The fresh binding is essential. A result can itself be a borrow; checking only ${\mathrm{\Gamma }}_2$ would forget the referent whose lifetime must be validated.

Proof of Theorem 48.6 — Featherweight Rust progress

Proof. The imported proof is induction on the typing derivation. For copy, move, and assignment, safe abstraction supplies the location demanded by lookup; borrow exclusion rules out the stuck aliasing configurations. A move cannot cross a borrow and therefore reaches an owned location. Congruence rules use the induction hypothesis, and completed blocks either return a value or drop their top frame. ◻

Flow sensitivity changes the form of preservation. The final environment is not intended to abstract every intermediate store.

Proof of Theorem 48.7 — Whole-term Featherweight Rust preservation

Proof. Induct over the complete evaluation derivation and the typing derivation. The move case removes one owner in both store and output environment. Assignment uses drop preservation before update preservation. Block exit drops the entire local frame and every transitively owned allocation. Borrow invariance, including the anonymous result binding, prevents a returned borrow from naming a dropped local. These cases establish the final abstraction; no claim is made that ${\mathrm{\Gamma }}_2$ abstracts every intermediate store. ◻

Proof of Theorem 48.8 — Featherweight Rust type and borrow safety

Proof. The finite core contains no loop or recursion. Repeated theorem 48.6 therefore reaches a terminal state, and theorem 48.7 types that state. Borrow safety is preserved by the only borrow-creation rules: a mutable borrow requires absence of every overlapping borrow, while a shared borrow requires absence of an overlapping mutable borrow. Move, assignment, and drop create no borrow alias. ◻

The termination premise in that proof concerns program evaluation in the finite calculus. A different problem remains: does the recursive borrow-checking algorithm itself terminate?

Repairing checker termination

The recursive function $\mathsf{type}(w,\tau )$ follows both syntactic dereferences and left values mentioned in borrow types. Without an invariant, makes lookup chase itself.

Equivalently, the dependency digraph $x\to v$ is acyclic. For , a correct ranking is $\varphi (x)=1$, $\varphi (y)=0$.

For a left value $w$, let $d(w)$ be its number of leading dereferences. Order recursive lookup obligations lexicographically by $${\mu }_{\tau }(w)=(\varphi (\mathsf{root}(w)),d(w)),$$ with the rank component primary.

Proof of Proposition 48.11 — Well-founded lookup measure

Proof. To inspect $\ast w$, lookup first removes one syntactic dereference while retaining the same root, so the second component decreases. If the resulting type is a borrow naming $w^{\prime }$, lookup continues at $w^{\prime }$. The root of $w^{\prime }$ occurs in the type of the current root; linearizability therefore strictly decreases the first component. Lexicographic order on $\mathbb{N}\times \mathbb{N}$ is well founded. ◻

Proof of Theorem 48.12 — Termination of recursive place operations

Proof. Use well-founded induction on ${\mu }_{\tau }$. Proposition 48.11 handles the recursive lookup calls. $\mathsf{mutable}$ and $\mathsf{write}$ have the same two ways to recurse: one structural dereference or one followed borrow. Their local update and strike clauses are nonrecursive. ◻

It remains to show that typing does not destroy the ranking invariant.

Proof of Lemma 48.13 — Linearizability is preserved

Proof. Rules that do not change $\tau$ reuse its rank. Move strikes type components and thus deletes dependency edges. Block exit drops vertices and incident edges. Declaration adds a fresh vertex above every variable in its result type. Assignment may rewrite the finite set of owner variables along its update path. None of those variables occurs in an old right-hand side, because the type system forbids modifying a borrowed variable. Nor can one occur in the assigned type: the root case is excluded by the assignment rule’s write-prohibition premise, and an interior case would require reading through a mutable borrow. Assign the rewritten variables fresh distinct ranks above all unchanged vertices. Every old edge between unchanged vertices retains its order and every new edge points downward. The resulting rank is injective. ◻

Proof of Corollary 48.14 — Borrow checking terminates

Proof. The empty typing is linearizable. Apply lemma 48.13 at each typing rule and theorem 48.12 at each recursive auxiliary call. The syntax-directed derivation has finitely many rule applications. ◻

Oxide v4 starts a new calculus

Oxide v4 is not a theorem-strengthening extension of Featherweight Rust. It has a different syntax, store, type system, and proof. Its non-dereferencing places $\pi$ use numeric projections; its place expressions $p$ may dereference. Reference types record a region and a qualifier: An abstract region is quantified. A concrete region $r$ is an entry in the stack typing and maps to a finite set of loans $\omega p$. Regions are static alias sets, not runtime allocation arenas.

The central typing judgment is $$\mathrm{\Sigma };\mathrm{\Delta };\mathrm{\Gamma };\mathrm{\Theta }⊢e:\tau \Rightarrow {\mathrm{\Gamma }}^{\prime }.$$ $\mathrm{\Sigma }$ holds global definitions, $\mathrm{\Delta }$ holds type and abstract-region variables, $\mathrm{\Gamma }$ is an ordered stack typing of frames, and $\mathrm{\Theta }$ types already-evaluated components waiting in the continuation. The output stack typing makes moves, drops, loan creation, and region rewriting explicit.

Consider $r_x\mapsto \{\mathsf{uniq}x\}$ and a reference . A reborrow of $\ast z$ into fresh $r_y$ adds $\mathsf{uniq}(\ast z)$ to $r_y$. While $r_y$ is live, the exclusion list prevents a unique use through $z$; after $r_y$’s loan is cleared, the use becomes admissible again.

Non-lexical loans need the continuation

Lexical scope still determines when a region binding exists, but a concrete region’s loan set may become empty earlier.

The $\mathrm{\Theta }$ test prevents a premature collection. While checking the second component of a tuple, the first component’s reference may exist only as an evaluated temporary. Its region is absent from ordinary variable types but present in $\mathrm{\Theta }$, so its loan must remain live.

Proof of Proposition 48.17 — Non-lexical release

Proof. The metafunction empties exactly the first class of region entries. Ownership safety quantifies over the loans remaining in the region map, so a removed loan contributes no conflict. In the second class the entry is unchanged, and its conflict premises remain available. ◻

Ordered frames and non-lexical loans coexist

Runtime stores and static stack typings are ordered sequences of frames. Closure values carry their captured frame. Two administrative expressions make the order operational: $\mathsf{shift}e$ delimits a lexical binding and $\mathsf{framed}e$ delimits a closure call. Each removes the most recent frame only.

Proof of Lemma 48.18 — Stack-pop alignment

Proof. The dynamic rule matches the final frame constructor of the ordered store. The typing rule matches the final frame constructor of $\mathrm{\Gamma }$. Store well-formedness relates these constructors pointwise, so both rules remove the same suffix. An unordered finite map would not supply this inversion. ◻

This lexical last-in–first-out discipline does not make loans lexical: $\mathsf{gc}\text{-}\mathsf{loans}$ can empty a region entry before its binding frame is popped.

The exact Oxide v4 safety result

The source proves a place-evaluation lemma between ownership safety and progress: a well-typed place expression evaluates to a location context containing a value of its computed type. This connects static loan reasoning to dynamic moves, copies, borrows, and assignment.

Proof of Theorem 48.19 — Oxide v4 progress

Proof. This is Oxide v4 Lemma 3.1. Induction on the typing derivation uses canonical forms. The separate place-evaluation lemma supplies the location and value for moves, copies, borrows, and assignments. Applications either expose a global function or a closure with its captured frame; the latter steps to $\mathsf{framed}e$. ◻

Preservation cannot say merely “the type and output environment are equal.” Evaluation may make a region more precise, and taking one branch may leave unused output information.

Proof of Theorem 48.20 — Oxide v4 preservation

Proof. This is Oxide v4 Lemma 3.3, with its region-rewriting judgment described rather than replaced by equality. The proof is induction on reduction. Region rewriting, drop and loan collection, well-typed extension, assignment, and safe loan updates each require a value-typing preservation family. Closure bodies make those families necessary: their captured frames must remain typable under every environment transformation. Branch reduction uses ${\mathrm{\Gamma }}_o$ to account for output information belonging to the branch not taken. Lemma 48.18 supplies the two administrative cases. ◻

Proof of Corollary 48.21 — Oxide v4 type safety

Proof. Interleave theorem 48.19, theorem 48.20. This is a safety theorem, not a termination theorem. ◻

Frozen boundary and seminar problems

Featherweight Rust contributes the core left-value calculus, safe abstraction, borrow invariance, whole-term preservation, and the finite-core type and borrow safety theorem. The separate termination repair proves totality of its recursive checking operations. Oxide v4 contributes its own place expressions, ordered stack, regions-as-loan-sets, continuation-aware loan collection, progress, preservation, and safety.

Named record fields are convenient sugar for stable numeric projections. They are supported by the chapter artifact, as are finite conflict diagnostics. They are not part of the frozen Featherweight Rust theorem and do not turn Oxide’s tested compiler into a formal equivalence with rustc. Arrays, raw pointers, unsafe code, concurrency, traits, and a production compiler remain outside both proved boundaries.

Suggested first pass.

Begin with exercise 48.1, exercise 48.2, exercise 48.3, exercise 48.4, exercise 48.6. Continue with exercise 48.7. The practical project is an optional second pass.

None of these problems is a prerequisite for a later chapter.

Exercise 48.7¶

★★★ Work through the move, mutable-borrow, and block-exit cases of the Featherweight Rust safety proof. For each case, state the input store abstraction, the output environment change, and the borrow-invariance obligation. Explain why this does not prove the named-field extension.

Referenced from 4 locations

• Place Calculi, Partial Moves, and Field-Sensitive Borrowing
• ch:ownership-borrowing: ch:ownership-borrowing

Exercise 48.8¶

★★★ Reconstruct the Oxide v4 sequencing preservation case. Show where ${\mathsf{gc}\text{-}\mathsf{loans}}_{\mathrm{\Theta }}$ is applied, why $\mathrm{\Theta }$ is held fixed by the step, and how the value-typing-after-loan-collection lemma is used.

Referenced from 3 locations

• Place Calculi, Partial Moves, and Field-Sensitive Borrowing
• ch:ownership-borrowing: ch:ownership-borrowing

Exercise 48.9¶

★★★ Practical project.place-loan-checker Implement in Kappa finite rooted paths, prefix overlap, partial-move availability, qualified loans, and continuation-aware loan collection. The observable corpus must separate sibling fields, block a read of the whole partially moved value, permit the live sibling, reject a unique use under an overlapping shared loan, permit a shared use under overlapping shared loans, and permit a formerly blocked use only after its region is absent from both variables and the continuation. Add a rank checker that rejects a two-node borrow cycle. Mutate prefix overlap into equality; an inline oracle must fail. State why the executions prove neither theorem 48.8 nor corollary 48.21.

Referenced from 4 locations

• Place Calculi, Partial Moves, and Field-Sensitive Borrowing
• Object calculus checker and evaluator
• ch:place-calculi: place and loan checking

Sources.

Featherweight Rust’s frozen core and metatheory are Definitions 3.1–4.8, Lemmas 4.9–4.11, Theorem 4.12, and Corollary 4.14 of [Pea21]. The linearizability repair and termination argument are Definitions 11–12, Propositions 1–2, and Lemmas 1–4 of [PPS22]; the rank reversal in its printed two-variable example is corrected explicitly above. The Oxide system is frozen to arXiv v4: its Lemmas 3.1–3.8 and Theorem E.70 own the Oxide claims [WGPA21]. The v4 tested-semantics corpus is implementation evidence, not a bidirectional theorem relating Oxide and Rust.