WIP-0028: Deterministic ownership, borrowing, regions, and no implicit tracing GC

Summary

Wheeler uses deterministic ownership and region-based storage as its normal memory model. The language doesn't require or silently provide a tracing garbage collector.

A dynamic mutable value has one owner unless code uses an explicit sharing type. The compiler checks copying, moves, borrows, mutation, destruction, and escape, and verified bytecode records those choices. The core access rule is simple:

one exclusive mutable borrow
or
any number of shared immutable borrows

The referenced value must stay alive and unmoved for the full loan. Wheeler adopts this safety rule and Rust-like move behavior without copying Rust's syntax, full lifetime system, auto traits, interior-mutation patterns, broad unsafe, or effectful destructors.

Normal storage includes inline values, unique dynamic owners, bounded lexical or dynamic regions, phase arenas with typed IDs, and nonescaping loans. An explicit immutable Shared<T> may later be a library type. Host capabilities and foreign resources follow separate effect rules.

Memory release is deterministic. Automatic destruction may free Wheeler-owned memory and update internal accounting. It cannot perform file, network, process, target, provider, clock, random, or other outside effects. Those actions finish through explicit typed operations.

Quantum resources use the same ownership base with stricter must-consume rules. Qubits and registers cannot be copied, dropped without an operation, reference counted, serialized, or stored in a normal shared graph.

Motivation

The current machine already supports bounded affine regions, move and drop state, mutable buffer and map borrows, and immutable UTF-8 borrows. It also supports owner-returning calls, disjoint slices, affine quantum resources, exact ownership rewind, and hard byte and object limits.

The next profile needs compiler-sized arenas, owners that cross calls, borrowed results, package and runtime resources, and the generic collections from WIP-0029. A general object heap would make reachability an implicit lifetime rule. It would also tie VM and native behavior to collector policy, complicate rewind and FFI pinning, invite finalizers, and make compiler limits depend on collector behavior.

Wheeler uses a smaller contract: ownership modes, places, origins, loans, regions, deterministic memory release, explicit external cleanup, and bounded compiler and verifier analysis. VM rewind stays separate from source inverse. Quantum values remain affine semantic resources. The compiler and package manager are the full acceptance programs.

Representative source

This proposal fixes the source spelling borrow T for a shared loan and borrow mut T for an exclusive loan. Public borrowed results use returns borrow from name when the origin is not otherwise unique. WIP-0005 and WIP-0006 own grammar placement and formatting, not alternate ownership dialects.

Unique owner and loans

Vec<Token> tokens = new Vec<Token>(borrow mut arena, capacity);
tokens.push(token);
consumeTokens(tokens);              // moves tokens

long countKinds(borrow Slice<Token> tokens) {
  ...
}

void normalize(borrow mut Vec<Token> tokens) {
  ...
}

borrow Token first(borrow Slice<Token> tokens)
  returns borrow from tokens;

Using tokens after the move fails. Shared loans may coexist. An exclusive loan suspends overlapping owner and loan access. The returned token cannot outlive the slice origin.

Arena graph

Arena<SyntaxRegion> syntax = new Arena<SyntaxRegion>(limits);
NodeId root = parse(source, borrow mut syntax);
check(root, borrow syntax);
drop(syntax);

Nodes form graphs or cycles through typed IDs. The arena owns the graph and releases it without tracing individual reachability.

External and quantum resources

Result<File, OpenError> opened = files.open(path);
File file = opened.value();
Result<Done, CloseError> closed = file.close();

borrow mut Qubit left = q.borrowMut(0);
borrow mut Qubit right = q.borrowMut(1);
CNOT(left, right);

File must close, move, or return on every successful path. Scope exit cannot invent a successful host close. Close releases the resource and provides no WIP-0032 durability receipt. Quantum loans must be disjoint and end before measurement or register movement.

Native pinning

A bounded Pin<T> may stabilize storage for one exact WIP-0025 call scope. Pinning is explicit, creates no portable pointer identity, and is not the representation of ordinary loans.

Goals

• Define copy, move, shared/exclusive borrow, reborrow, drop, must-consume, region, arena, and pin semantics.
• Make mutable dynamic ownership unique by default and derive aggregate ownership structurally.
• Infer deterministic local last-use loan scopes and encode public borrow origins.
• Move owned values across function and module boundaries and return safe owner-tied loans.
• Provide bounded lexical/dynamic regions, unique allocation, and arena graphs with typed IDs.
• Reclaim memory deterministically without an implicit collector, finalizer, or hidden host cleanup.
• Specify optional immutable sharing without making it ambient object semantics.
• Integrate ownership with VM rewind, commit, proof evidence, native lowering, FFI, packages, closures, and quantum resources.
• Give .wbc verification enough canonical metadata to reject aliasing, escape, use after move, double drop, and leaked must-consume resources.
• Keep diagnostics source-located, bounded, and useful to somebody who did not write the checker yesterday.

Non-goals

The first profile leaves out:

• the full Rust lifetime, coercion, trait, and unsafe model.
• tracing collection, reference counting, or a fallback GC.
• Java object identity, reflection, finalizers, resurrection, and weak-finalization queues.
• exposed pointers, addresses, or arbitrary pointer arithmetic.
• user code during automatic destruction.
• hidden failure during resource cleanup.
• intrinsically reversible allocation or drop.
• persisted raw loans.
• shared-memory concurrency.
• copying or implicit dropping of quantum resources through generic containers.

General self-referential owners remain rejected. Cycles use one region or graph owner plus typed IDs. Advanced abstractions may retain bounded checks. The design does not require zero runtime checks.

Semantic model

Value modes

Every closed type has compiler-derived canonical properties:

• Copy means duplication preserves both value and ownership. Bounded scalars, small immutable enums, admitted proof-irrelevant evidence, and immutable records whose fields are all Copy qualify.
• Owned means one binding or aggregate place owns the value. Assignment, passing, and return move it unless Copy applies.
• Affine values may be consumed at most once, so copying is forbidden. Ordinary unique allocations are affine but may be droppable.
• Must-consume values must be moved, returned, transformed, or explicitly consumed on every successful path. Live qubits, registers, capabilities, transactions, and external handles may use this mode.
• Droppable values permit deterministic memory-only destruction under the sealed Drop contract. A must-consume type may deliberately lack this property.
• Borrowed values are scoped permissions that refer to an owner or shorter reborrow. They own nothing.

Copy, Drop, and must-consume status are compiler-derived or admitted by sealed evidence. An ordinary WIP-0030 instance cannot make a socket copyable or teach a dirty qubit to disappear.

Places, origins, and loans

A place is a statically identified location: local, state or record field, checked array element, buffer/slice range, region handle, or quantum subrange. Operations apply to places, not untyped addresses.

A loan records canonical owner origin, shared/exclusive mode, start, deterministic last use or lexical end, allowed projections, region relation, and optional disjointness evidence. Reborrowing preserves the origin and narrows lifetime/permission. A parent exclusive loan is suspended while a child reborrow lives.

moved(o) => no read, borrow, drop, or second move of o

exclusiveLoan(p) =>
    no overlapping loan and no overlapping owner access

sharedLoans(p) =>
    no overlapping exclusive loan or mutation

lifetime(b) <= lifetime(origin(b))

drop(o) =>
    no live originating loan and no unconsumed must-consume child

Simultaneous exclusive loans to p and q require static proof or a checked prepublication test of disjoint(p, q). A failed dynamic range test publishes neither loan.

Initial loans are second-class. They cannot enter ordinary owned aggregates, persisted state, package archives, certificates, workflow events, retained FFI state, escaping closures, an unrelated task, target submission, measurement transition, or commit. A public return or borrowed ABI names its origin explicitly. WIP-0041 result slots do not weaken this rule. A returned loan keeps its origin-bearing ABI and Slot<borrow T> remains invalid.

WIP-0032 supplies the one suspension exception: an affine operation may own a verifier-visible loan across asynchronous suspension while the continuation cannot access the overlapping place. That loan still cannot enter persisted continuation state. Process suspension first completes, cancels and reconciles, or converts the operation to canonical owned resumable state.

Partial moves and captures

Complete locals and statically representable aggregate fields may move independently. A dynamically indexed element moves only through a collection operation that updates initialized-element state.

A closure copies Copy captures, moves owned captures, and may borrow only within the origin lifetime. Exclusive capture is exclusive. A must-consume capture makes the closure must-consume. Closure drop is legal only when every capture is droppable. WIP-0031 adds callable characteristics and effects.

Allocation and reclamation

Inline and unique storage

Scalars and bounded aggregates may live in frames or inline aggregate storage. Native layout is derived and is never source identity.

A Box<T>-like owner stores one T in allocator-owned memory. Moving moves ownership. Borrowing reaches the contained place. Drop destroys T under its sealed contract and releases storage.

Owned Vec<T>, String, builders, maps, sets, and queues expose mutation through unique ownership or exclusive loans. Capacity, allocator, and hard bounds are explicit values or declared execution policy.

Regions and arenas

A lexical region belongs to one scope. A dynamic region is an affine owner that may cross calls. Both carry unique identity, byte/object limits, allocation policy, child relation, allocation table, and open/closed state.

A region closes only with no live loan, escaped allocation, unfinished child owner, or outstanding explicit resource transition. Successful lexical exit satisfies those rules statically. Trap cleanup follows the separate failure contract below instead of treating an unfinished external cleanup as complete.

Compiler/package phases allocate immutable or phase-owned nodes in arenas and refer to them through nominal NodeId, TypeId, or SymbolId. IDs are meaningful only with access to their arena and are never persisted as addresses.

Explicit immutable sharing

Shared<T> is an optional library owner, not universal representation. Its accepted profile requires immutable fully constructed T, no interior mutation, no external resource/finalizer, deterministic bookkeeping, memory-only release, and an API unable to construct strong cycles. Reference-count changes and allocation remain visible effects. General mutable reference-counted graphs are out of scope.

A future traced GcRegion requires its own WIP. A runtime may privately trace host implementation objects only when they are not Wheeler values and cannot affect semantics, diagnostics, limits, bytes, finalization, or FFI stability.

Deterministic destruction

At normal scope exit, memory-only droppable owners are destroyed in canonical order:

1. inner scopes before outer scopes.
2. reverse declaration order within one scope.
3. aggregate fields and collection elements in their declared deterministic order.
4. never allocation-address or hash-bucket order.

Automatic Drop is bounded, infallible, nonblocking, nontrapping for valid input, address-blind, and free of host, network, process, target, provider, clock, random, FFI, or user callback effects. External owners use explicit consuming operations such as close, finish, commit, abort, or releaseTarget, usually returning Result.

On a trap, the runtime deterministically reclaims private frame/region memory without invoking arbitrary user code. External resources follow their declared host/runtime failure contract. Committed effects remain committed. Must-consume obligations are required on successful paths, not retroactively declared successful after a trap.

Reversibility, history, and commit

Move marking and loan lifetime changes are often compile-time facts and may appear in rev code when the ownership relation remains invertible. Swapping or permuting complete owners may be intrinsically reversible.

Allocation and deallocation are ordinary effects. A rev body may use caller-owned clean workspace or a certified reversible allocator protocol. It may not allocate and discard. Drop is valid during intrinsic reversal only for statically clean/empty values or when exact owned evidence recreates them. Logged history makes rollback possible, not intrinsic inverse.

The VM records allocation, mutation, move, loan, and drop state above the commit horizon and can restore it during rewind. WIP-0001 rewind still does not make allocation/drop legal in a generated inverse. Commit permanently discards older history and permits source-unreachable memory reclamation. No loan spans that horizon.

Quantum ownership

Qubit, Qreg, quantum views, ancillas, and target-session resources are must-consume affine values. They implement neither Copy nor Shared and cannot be serialized as ordinary data.

Shared borrows permit metadata operations only. Gates use disjoint exclusive borrows or an owning register operation. Split creates disjoint affine views with origin/index maps. Join checks common origin, nonoverlap, required coverage, and absence of child loans. Measurement consumes or transitions the old quantum identity. Ancillas return clean, transition under an accepted measurement/reset contract, or return to the caller. Scope exit does not sweep dirty state under the amplitude rug.

An ordinary Vec<Qubit> is valid only if every operation preserves affinity, origin, and consumption. It is not automatically a Qreg.

Capabilities, concurrency, and native calls

Capabilities and external resources are affine or scoped. Importing a package grants no capability. Automatic wrapper-memory release cannot claim an external operation succeeded.

This WIP defines no shared-memory synchronization. Moving immutable owners between structured tasks and sharing immutable values require future Send/Share evidence. borrow mut is not a memory model.

WIP-0025 may lower a loan to one bounded native span when the exact descriptor permits it, storage is pinned or copied for the call, mutability/aliasing agree, and callbacks or retention cannot outlive the scope. Retention requires transfer to an affine foreign owner.

Asynchronous I/O loans

WIP-0032 requests capture owners or loans without submitting an effect. Submission moves those obligations into an affine Operation<T>: reads hold an exclusive destination loan, writes hold a shared source loan, and moved buffers return through terminal results. The loan ends only at final resource-release completion, not at a convenient earlier transport notification.

Provided-buffer leases, registered regions, remote advertisements, tier allocations, and target sessions are bounded affine resources. A live operation is must-consume. Scope exit must cancel or complete, reconcile uncertainty, release every held loan, and reap exactly once.

Reversible IR, proof, bytecode, and packages

Ownership is part of Wheeler's reversible typed IR instead of a source-only lint. Every move, initialization, mutation, loan boundary that survives lowering, release, and resource transition has an exact forward state rule plus its WIP-0001 inverse, logged-rewind, or barrier classification. rev bodies may contain only ownership transitions whose inverse relation is checked. Coherent and unitary bodies must also satisfy WIP-0002/WIP-0031 affine resource rules. Native lowering consumes these facts and cannot rediscover weaker alias rules from machine pointers.

Compiler/verifier evidence covers use-after-move, double drop, borrow escape, shared/exclusive compatibility, disjoint split, must-consume completion, region nonescape, and no live loan at destruction. WIP-0011 may expose stronger propositions, but a theorem never disables verifier safety.

Canonical function/type metadata records value mode, structural properties, passing mode, result origin, region/outlives relations, place layout/projections, captures, and disposal obligations. Ownership dataflow assigns each place a state such as:

uninitialized | owned | partially moved | shared borrowed
exclusive borrowed | moved | dropped

The verifier derives compatibility across branches and loops and need not keep runtime counts for statically bounded shared loans. Metadata is source-order-independent. Native lowering may not weaken verified alias assumptions.

Public ownership is package API. Changes from copy to move, droppable to must-consume, shared to exclusive borrow, result origin, lifetime, disposal, allocator/region requirement, or quantum consumption are compatibility changes.

Limits and failures

Compiler limits cover owners, regions, loans, projections, control-flow states, disjointness tests, lifetime relations, captures, generic ownership derivations, diagnostics, memory, and total checking work. Runtime limits cover bytes, objects, pins, shared owners, call depth, and cleanup work.

Exhaustion is a deterministic diagnostic, never permission to compile unsafely. Forged ownership metadata, invalid state joins, escape, overlap, or cleanup obligations fail before execution and before any partial artifact is published.

Migration and deletion

1. Define value modes and canonical ownership metadata.
2. Extend current local owner/borrow checks through call parameters and results.
3. Add deterministic last-use inference and public origin declarations.
4. Add unique allocation and dynamic region owners.
5. Add arena/typed-ID substrate and port compiler syntax and semantic graphs.
6. Add WIP-0029 generic owned collections.
7. Add canonical memory-only destruction and explicit must-consume disposal.
8. Add quantum split/join and ancilla obligations.
9. Add optional acyclic immutable Shared<T>.
10. Add WIP-0025 pinning and native conformance.
11. Delete host-GC-backed source values, hidden finalizers, duplicate manual owner flags, and pointer-like bootstrap shortcuts instead of keeping obsolete ownership paths.

Progress

• [x] Function-local affine regions and owned buffers execute.
• [x] Nonescaping shared and exclusive parameter borrows execute for bootstrap storage.
• [x] VM snapshots and rewind preserve current owner/drop state.
• [ ] Canonical value modes and public metadata are accepted.
• [x] Primitive region, words, bytes, utf8, and longmap owners return across calls through canonical typed result metadata. The callee consumes the returned local, every other callee owner must be dead, and storage factories allocate through a nonescaping caller-region borrow. The stage-0 VM and Wheeler-written verifier/interpreter agree and rewind the transfer exactly. OwnedReturns.w exercises all five owner kinds. The caller gets one owner, not two handles and a motivational poster.
• [x] Unqualified primitive owner parameters transfer region, words, bytes, utf8, or longmap ownership into the callee. Definite-ownership flow rejects caller use after the call and requires the callee to drop, forward, or return the owner. Bytecode verification, stage-0 execution, Wheeler-native interpretation, and exact rewind agree.
• [ ] Public borrowed results with explicit origins execute.
• [ ] Local last-use inference is deterministic.
• [ ] Unique dynamic allocation executes.
• [ ] Generic arenas and typed IDs support compiler-scale graphs.
• [ ] Deterministic destruction executes without finalizers.
• [ ] Effectful disposal is explicit and must-consume.
• [ ] Quantum split/join and ancilla obligations execute.
• [ ] Optional immutable sharing satisfies acyclicity.
• [ ] Native lowering and FFI preserve ownership.
• [ ] No source-level traced path remains or is required.

Testing and acceptance

• [ ] Copy values duplicate. Owned values move. Use after move, double move/drop, and forgotten must-consume values fail.
• [ ] Shared loans coexist and block mutation. Exclusive loans reject overlap. Reborrows suspend and restore parent permissions.
• [ ] Local loans end at deterministic last use. Returned loans cannot outlive owners. Ambiguous public origins require metadata.
• [ ] Dynamic split rejects overlap before publishing loans.
• [ ] Region drop rejects live loans and escapes. Cyclic arena graphs release without tracing.
• [ ] Box<T> and collections derive element ownership correctly.
• [ ] Trap cleanup invokes no user finalizer and external failure remains explicit.
• [ ] VM rewind restores ownership/storage above the horizon. Generated inverse rejects arbitrary allocation/drop.
• [ ] Qubit/register copy, implicit drop, sharing, and serialization fail. Split/join/ancilla obligations pass.
• [ ] Shared<T> cannot form a strong cycle through its accepted API.
• [ ] Pinning is bounded and creates no portable address identity.
• [ ] Forged lifetime, loan, move, and drop metadata fails verification.
• [ ] VM and native execution agree on successful and failing ownership transitions.
• [ ] Self-hosted compiler and package-manager acceptance programs run without a tracing collector.

Alternatives

Adopt Rust wholesale

Rejected as a specification shortcut. Wheeler keeps the central alias/lifetime laws but has different source ergonomics, rewind, quantum resources, bounded execution, proof boundaries, and explicit effects.

Use tracing collection or universal reference counting

Rejected as ordinary semantics. Tracing adds implicit liveness, pauses, root/pinning policy, finalization temptation, and VM/native parity work. Universal reference counting adds hidden mutations, cycle policy, and awkward reversible behavior. Explicit future library/region types may propose either without becoming ambient.

Require manual free

Rejected. Static moves, must-consume rules, and regions preserve control without admitting leaks, use-after-free, and double-free as an API style.

C++-style effectful destructors

Rejected. Hidden fallible I/O during unwinding composes badly with traps, rewind, proofs, and deterministic builds. External cleanup remains source-visible.

Keep every compiler value forever

Useful for a milestone, not a language contract. Long-lived applications and reusable libraries need bounded nested release.

Add unsafe now

Rejected. WIP-0025 already names the native trust boundary. An unnamed escape hatch is not a substitute for finishing the checker.

Open questions

• Is Shared<T> required for this WIP's first acceptance or its immediate library milestone (owner: runtime and library maintainers. Decision point: standard collection stabilization)?
• Which must-consume resources receive runtime-managed abort on trap, if any (owner: runtime and workflow maintainers. Decision point: external resource type states)?
• Are named regions visible in ordinary collection types or only ambiguous public signatures (owner: type-system and library maintainers. Decision point: cross-function borrow support)?
• Which ownership facts are stored in .wbc and which are rederived (owner: bytecode and verifier maintainers. Decision point: ownership section freeze)?

Integration with reversible concurrency

Task transfer and scoped sharing

WIP-0039 defines sealed compiler-derived task-transfer properties. Copy values may copy into a child. An owner may move into one child. Immutable sharing needs compiler evidence. Ordinary loans do not cross spawn. AtomicRef stays inside its TaskScope. JoinHandle is affine and scope-owned.

WIP-0032 keeps its verifier-visible operation loan across external suspension. Quantum owners move to one task or split into proven-disjoint affine views.

Normal WIP-0030 instances cannot grant task transfer, atomic sharing, or quantum sharing authority.

References

• WIP-0039
• WIP-0040

• WIP-0001
• WIP-0002
• WIP-0005
• WIP-0011
• WIP-0012
• WIP-0013
• WIP-0025
• WIP-0029
• WIP-0030
• WIP-0031
• WIP-0032
• Rust ownership and borrowing
• Linear Haskell
• Region-Based Memory Management in Cyclone
• Safe and Flexible Memory Management in Cyclone