ADR-0016: Bounded Affine Unique Ownership for Core P1V4

Status: accepted
Date: 2026-07-25

Context

Core-N0 represents Mutability::Unique, but profiles through P1V3 reject unique references. Shared references prove alias-visible mutation but cannot justify no-alias optimization, destructive update, ownership transfer, or a future escaping closure/continuation policy.

Admitting Unique solely because the Rust seed holds a value in one variable would make host ownership accidental semantic evidence. Conversely, a general borrow checker with reborrowing, aggregate partial moves, region variance, and escaping ownership would be too large to introduce as one unchecked step.

Options considered

Decision

Core profile P1V4 is a strict admission superset of P1V3. Existing profile bytes, hashes, and rejection behavior remain unchanged.

P1V4 admits:

Ref<rho, Unique, Bool | I64 | F64>
RefAlloc<rho, Unique>(scalar)

A direct local of this type is an affine owner:

• it may be dropped without use;
• it may be borrowed any number of times by RefLoad and RefStore while live;
• it may be moved at most once;
• any later borrow or move through the source local fails verification.

The verifier owns a separate affine dataflow pass. Rust moves, Clone, reference counts, and host addresses are not evidence.

Move and borrow classification

Moves:

• Use(unique_local) into a new typed binder;
• a unique argument to a direct Call;
• a unique argument to a direct TailCall.

Borrows:

• the reference operand of RefLoad;
• the reference operand of RefStore;
• ordinary scalar operands.

Move transfer is positional and left-to-right. Passing one owner twice in one call fails on the second occurrence.

An internal function may accept a direct unique-reference parameter. Entry parameters and every function result remain reference-free. A call therefore transfers ownership into the callee; the caller cannot regain it implicitly. A unique tail transfer reuses the active logical store without creating an alias in the old frame.

Branch semantics

If and Case analyze each mutually exclusive branch from the same incoming ownership state. A move in one branch does not invalidate the other branch. Use-after-move within one reachable branch fails.

Core-N0 terms are terminal trees: there is no implicit post-branch join. A future block-parameter/CFG form must require exact ownership-state agreement at joins.

Bounded representation

P1V4 keeps unique ownership direct:

• tuples and sums containing Unique are rejected;
• unique values cannot be packed into closures;
• unique values cannot be captured by handlers;
• unique values cannot be passed to closure calls or effect operations;
• unique values cannot be stored inside logical cells;
• there is no Read reborrow or shared downgrade.

These restrictions avoid partial moves, repeated closure invocation, repeated handler clauses, and hidden alias creation before those mechanisms have accepted ownership rules.

Runtime semantics

The canonical interpreter removes a moved unique local from its environment. The logical cell and opaque location remain the same during transfer. RefLoad and RefStore use a temporary borrow and do not create a persistent Core alias.

The store admits both Shared and Unique scalar cells. Neither mode exposes physical placement, address, allocation count, or reclamation time.

Identity and observability

Observable:

• mutation through the current owner;
• move transfer and use-after-move rejection;
• left-to-right transfer order;
• branch-local ownership behavior;
• typed errors and evaluation budgets.

Not observable:

• host move/copy operations;
• addresses or reference counts;
• stack, arena, register, or heap placement;
• the numeric logical location.

Rationale

• A separate affine pass makes ownership independently checkable rather than entangled with host typing.
• Borrow-versus-move classification allows useful repeated mutation without sacrificing unique ownership.
• Direct call transfer is the smallest cross-frame ownership mechanism needed before safe escape can be designed.
• Affine dropping handles typed error, unhandled operation, and branch paths without mandatory destructor semantics.
• Rejecting captures prevents closure or handler reuse from duplicating an owner.

Trade-offs

• No nested unique ownership in tuples, sums, cells, closures, or handlers.
• No temporary Read borrow, reborrow, split borrow, or shared downgrade.
• No unique result or ownership return to a caller.
• A unique call is consuming even if the callee only reads.
• The first verifier is flow-sensitive over Core locals but not path-condition-sensitive.

Consequences

Positive: Core-N0 gains verifier-owned no-use-after-move evidence and sound unique mutation/transfer semantics suitable for later optimizer certificates.

Negative: P1V4 is not yet a general ownership/borrowing system.

Mitigation: unsupported aggregates, captures, entry/results, shared tail transfer, read borrows, and post-move use fail closed.

Revisit trigger

Add non-consuming Read borrows only with lexical loan scope and mutation exclusion. Add aggregate ownership only with field-sensitive partial-move and join rules. Add ownership return/escape only with explicit region transfer. Allow unique closure or continuation capture only when invocation/resumption multiplicity is verifier-proven affine.