Oxide: The Essence of Rust

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked quotations and pages, the 208 of 615 test counts (89 + 119 = 208, 407 excluded, Fig. 10), rules and steps in Sec. 2-3, Verus forms; changed the claim that region rewriting makes provenance more precise (it unions loan sets), lets requiring regions reborrowable (paper: not reborrowed), an invented exception to automatic fresh regions, an unsupported reason for ordered stacks and dead markers, closure frame timing, the omitted test adaptations, and marked own inferences.

scope and contribution

Weiss, Gierczak, Patterson, and Ahmed define Oxide, a source-level formal language intended to capture safe Rust’s ownership and borrow checker. Oxide is a model and metatheory, not a Verus verification workflow. It gives VL a semantic vocabulary for moves, shared and unique borrows, non-lexical lifetimes, regions, reborrowing, closures, and type safety. The paper includes an OCaml typechecker (OxideTC), a Rust-to-Oxide reducer, and tests against rustc.

The abstract says: “We capture the essence of this model of ownership by developing a type systems account of Rust’s borrow checker.” (abstract, p. 1) It also states: “Our type system is able to automatically compute this information through a control-flow-based substructural typing judgment.” (abstract, p. 1)

The formalism deliberately omits type inference, traits, concurrency, most unsafe behavior, and many libraries. Claims below about using Oxide ideas in Verus are my inference.

technique 1: ownership as use-once variables

what it is and when to use it

Treat a noncopyable value as a linear/use-once binding. Moving a value transfers ownership and marks the old binding dead. Use this as the base rule for reasoning about resource consumption and to detect use-after-move before adding borrowing.

how to apply it

1. Bind a value, such as pt = Point(6, 9).
2. On x = pt, transfer the value to x and mark pt dead.
3. Reject any later use of pt; using x is valid.
4. Permit repeated use only for copyable types under the copy rule.
5. Preserve dead bindings in ordered environments so scope/drop behavior remains explicit.

The paper’s example says: “Moving the value out of pt, invalidates this old name. Subsequently, when we attempt to use it again at line 4, we encounter an error because pt was already moved in the previous line.” (Sec. 2.1, p. 3)

Verus form (inference)

Verus and Rust already enforce much of this for ordinary values. The useful addition is a tracked ghost token for external resources, raw allocations, or protocol states: consuming the token models a move, and no later proof can reopen it. Copyable ghost facts should be explicitly marked duplicable.

Evidence and limits

This is an explanatory rule, not an independent benchmark. The paper marks a moved place with a dagger (dead) and keeps the name in scope until T-Let drops it (Sec. 3.5, p. 17); it says stack typings are ordered, “which makes it easier to state invariants like outlives” (Sec. 3.3, p. 11). Inference: this is why ordering and the dead marker matter; the paper does not argue that lexical linearity is insufficient.

technique 2: shared and unique loans

what it is and when to use it

Borrowing softens use-once ownership. A shared loan allows multiple read-only references; a unique loan is the only usable name and allows mutation. Use the choice at each borrow site to express whether aliasing or mutation is intended.

how to apply it

1. Introduce a region scope with letrgn<'x, 'y>.
2. For read sharing, create &'x shrd pt and &'y shrd pt; accept both because shared loans do not permit mutation.
3. For mutation, create &'x uniq pt; reject another unique borrow while the first remains live.
4. Reject a shared borrow while a unique loan is live.
5. Use later-use information to determine whether a loan actually remains live; if a unique reference is never used, non-lexical lifetime analysis may end it early.

The paper explains: “As a consequence of allowing this sharing, the type systems of both Oxide and Rust prevent mutation through these references. To mutate through a reference, you must instead have a unique reference (i.e., it is the only usable name for the underlying data).” (Sec. 2.2, p. 4)

Verus form (inference)

Use ordinary &T and &mut T where Rust’s checker suffices. For raw pointers or ghost models, encode shrd and uniq capabilities as tracked tokens and require a unique token for mutation lemmas. A Verus requires clause can state the token, and ensures can return it after a borrow’s modeled end.

Evidence and limits

The examples establish intended acceptance/rejection patterns, including NLL and mixed-borrow rejection. Oxide does not model concurrency, and its shared-reference story is about safe Rust; interior mutability is discussed only as a guarded exception.

technique 3: regions as static alias provenance

what it is and when to use it

Oxide regions are sets of loans that approximate where a reference may point. They are not allocation regions and do not control memory reclamation. Use them to reason about alias origins, NLL, and reborrowing without tying a lifetime to lexical scope.

how to apply it

1. Bind abstract regions in letrgn.
2. When borrowing x as &'y uniq, record 'y -> { uniq x } in the environment.
3. When reborrowing through y as z, record a chain such as 'z -> { uniq x, uniq *y }.
4. Use the loan set to decide whether a new unique/shared borrow overlaps a live conflicting loan.
5. Clear unused concrete-region loans at sequencing points when continuation typing shows no future use.

The paper says: “In this way, we can think of our regions as a sort of static grouping of distinct objects in memory, and by associating a reference with a region, we identify that the objects in memory that reference could point to must be from the collection of loans we’ve associated with it.” (Sec. 2.2, p. 5)

Verus form (inference)

Represent a region as a ghost set/map of allocation identities and borrow paths. Functions can quantify over region-like ghost parameters and require outlives relations as predicates. Verus lifetimes remain Rust compiler artifacts; the ghost region is a semantic layer for raw-pointer provenance and proof automation.

Evidence and limits

Oxide’s region design specifically targets non-lexical lifetimes. It requires explicit region annotations in the calculus, adding annotation burden absent from surface Rust. The authors report that the implementation reduces this burden by “automatically generating a fresh local region for borrow expressions without an annotation. This suffices for the majority of expressions without change.” (Sec. 3.8, p. 23)

technique 4: ownership-safety judgment and reborrow exclusions

what it is and when to use it

The core judgment Δ; Γ; Θ ⊢ω p ⇒ {ω p'} proves that place p is safe to use uniquely (uniq) or sharedly (shrd) and returns a borrow chain. A unique use conflicts with any overlapping loan; a shared use conflicts only with overlapping unique loans. Reborrow exclusion lists prevent a reference from conflicting with loans inherited from the reference it reborrows.

how to apply it

1. Inspect every concrete region in the stack typing Γ.
2. Define overlap as equal places or a prefix relation (a field/element lies inside a larger place).
3. For uniq, reject any overlapping loan; for shrd, reject only overlapping unique loans.
4. When dereferencing a reference, decompose the place into a context and recurse through its region’s loan set.
5. Add the reborrow origins to an exclusion list so inherited loans do not falsely conflict.
6. Add the new reborrow loan to the borrow chain and store that chain in the region environment.

The paper states: “Since it is precisely this ownership safety judgment that captures the essence of Rust’s ownership semantics, we understand Rust’s borrow checking system as ultimately being a system for statically building a proof that data in memory is either uniquely owned (and thus able to allow unguarded mutation) or collectively shared, but not both.” (Sec. 3.4, p. 12)

Verus form (inference)

Implement ownership_safe as ghost lemmas over paths and loan sets. A path can be a root allocation plus field/index projections; a prefix relation captures overlap. Reborrow proof functions add an exclusion set and return a chain token. This is most relevant to unsafe Rust, where compiler borrow checking no longer validates raw-pointer-derived aliases.

Evidence and limits

Inference: the paper gives formal rules and a pen-and-paper type-safety proof for Oxide, not for rustc itself. Its overlap abstraction is at the level of places, and unsafe pointer provenance, layout, and concurrency are outside scope.

technique 5: control-flow substructural typing and environments

Oxide’s main typing judgment is Σ; Δ; Γ; Θ ⊢ e : τ ⇒ Γ': global definitions Σ, type/region environment Δ, ordered stack typing Γ, and temporary/continuation typing Θ produce a type and updated environment. Γ records bindings, dead markers, regions, and loan sets; Θ retains already-checked parts of tuples or continuations so a later component cannot incorrectly forget an earlier live borrow. Branches typecheck both paths and reconcile output environments; sequencing garbage-collects loans not needed by Θ; lets require that free regions of the bound type are not reborrowed (rnrb); assignments require unique safety.

Closures are handled by moving captured values into a frame carried by the closure type. When the closure body is typechecked, the captured frame is appended to the stack typing with ♮ (Sec. 3.3, p. 11). This makes captured ownership and regions explicit and allows preservation to reason about suspended computations.

Verus form (inference)

Verus proof functions can mirror Γ updates as ghost state, while executable Rust remains ordinary. For agent-generated proofs, record branch-local invariants and merge them explicitly at if joins; use continuation-like ghost parameters for partially constructed tuples and closures. The exact Oxide judgments are a semantic blueprint, not syntax that Verus accepts.

technique 6: region rewriting and outlives

Oxide distinguishes concrete regions (loan sets) from abstract regions in polymorphic function types. Outlives judgments relate them, and region rewriting rewrites the regions of one type into those of another, for example so both branches of an if get one type, by combining loan sets conservatively (Sec. 3.5, p. 15). Function signatures can carry where-bounds such as abstract region 'a outliving 'b; calls check these bounds and reborrow restrictions. Use this for generic functions that return a reference from one of several reference parameters.

The paper says: “These where bounds come directly from Rust, and are useful in making functions that, e.g., reborrow from one of several reference-typed parameters.” (Sec. 3.2, p. 9)

Verus form (inference)

Use lifetime-parameterized Rust signatures for compiler-checked outlives and add ghost predicates for semantic region inclusion. A verified wrapper can require that a returned reference’s provenance is included in an input region. Region rewriting corresponds to weakening: the paper unions the loan sets (the rules OL-CombineConcrete set the output to the union of both regions’ loans, Fig. 6), so a ghost set would grow, not shrink.

technique 7: operational semantics and type safety

Oxide defines small-step semantics for moves, copies, borrows, assignment, sequencing, lets, closures, calls, and loops. The metatheory proves progress and preservation. Progress says a well-typed expression is a value, an abort, or can step. Preservation maintains stack validity, expression typing, and aliasing invariants after a step, allowing region rewriting and environment changes. The combined result is a conventional syntactic type-safety theorem.

The paper states: “With Lemma 3.1 and Lemma 3.3 in hand, we also prove a conventional type safety theorem as a corollary.” (Sec. 3.7, p. 22)

The difficult part is preserving well-typed closures and values across region rewriting, drop/garbage collection of loans, assignment, and safe loan updates. Inference: this proof decomposition is a technique for building a Rust semantics: isolate preservation lemmas for each environment mutation, then compose them.

Verus form (inference)

Verus projects usually prove function-level specifications rather than a full language metatheory. For a verified Rust runtime or unsafe abstraction, the analogous evidence is a library invariant preserved by every public operation. Oxide’s progress/preservation structure can guide a future semantic model of Verus-checked Rust, but cannot itself prove a particular Verus program.

technique 8: tested semantics against rustc

The authors implement OxideTC and Reducer and compare results with official borrowck and NLL tests. Of 615 tests considered, 208 were in scope and all 208 either typechecked when rustc did or produced a corresponding error. 407 were excluded as out of scope; the largest categories include heap allocation, libraries, enums, statics/constants, traits, and uninitialized variables. This is validation evidence, not a completeness theorem.

The paper reports: “All 208 tests either type check when rustc does so, or produce an error corresponding to the error produced by rustc.” (Sec. 3.8, p. 22)

The tested subset omits unsafe, two-phase borrows, multithreading, macros, and other categories. The authors also adapted the tests: they translated methods into functions, manually introduced temporaries, and split files with several errors into one file per error (Sec. 3.8, p. 23). Thus an agent using Oxide ideas must not claim all-Rust coverage from these numbers.

what is proved, trusted, and relevant to VL

Proved: Oxide’s formal typing and operational semantics satisfy progress and preservation, with supporting lemmas for region rewriting, drops, closures, assignment, and loan updates. Measured: 208/208 in-scope official tests matched rustc. Inference (not stated in the paper): not proved are equivalence to all rustc behavior, unsafe aliasing soundness, trait/library semantics, or Verus solver correctness. Trusted elements include the formal rules, reducer, typechecker implementation, test oracle, and the selected safe-Rust subset.

Threat to VL (inference) is foundational rather than a direct product exploit. If VL generates safe Rust, the compiler supplies much of the ownership discipline; if it generates unsafe code or reasons about raw pointers, Oxide exposes missing semantic obligations. VL should borrow the region/loan vocabulary, branch-sensitive environment tracking, closure preservation, and explicit distinction between static alias safety and functional postconditions. It should not redo Oxide’s already-developed core semantics, but must extend evidence to Verus annotations, unsafe operations, concurrency, and actual product libraries.

techniques for the catalog

• use-once ownership — consume noncopyable bindings on move and reject later use of dead names
• shared and unique loans — permit many read-only aliases or one mutable alias, with mixed-borrow rejection
• region-based alias management — represent reference provenance as static sets of loans rather than allocation regions
• ownership-safety judgment — check place overlap and permissions, with reborrow exclusion lists and borrow chains
• continuation-aware environments — track ordered stack frames, dead bindings, closures, and partially evaluated values
• outlives and region rewriting — relate abstract/concrete regions and merge loan sets so values of differently annotated types get one type
• progress-preservation metatheory — prove every well-typed step remains well typed and cannot get stuck
• tested semantics — compare a reducer/typechecker against rustc’s in-scope borrow-checker and NLL tests

Last edited: 2026-10-13