ADR-0017: Bounded Ownership Return for Core P1V5

Status: accepted
Date: 2026-07-25

Context

P1V4 can move a direct Unique owner into an internal function, but every function result is reference-free. A callee may mutate the owner, yet a successful call cannot return ownership to its caller. This makes unique calls terminal from the caller’s perspective and prevents ordinary ownership threading through reusable functions.

Allowing arbitrary reference results would be unsound. A callee could allocate inside a lexical region, close that region, and return a dead logical reference. Allowing aggregate results would also require partial moves and ownership-aware joins that P1V4 deliberately excludes.

ADR-0016 reserved ownership escape for explicit region transfer. This decision does not create such an escape: the region remains caller-owned and active, while only its direct owner is threaded through the callee and back.

Options considered

Decision

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

An internal function may have a direct unique result:

Ref<rho, Unique, Bool | I64 | F64>

only when all of these conditions hold:

1. the function is not the program entry;
2. exactly one parameter contains any reference;
3. that parameter is itself a direct Unique reference;
4. its type exactly equals the function result type.

That parameter is the function’s liveness anchor. Passing it proves that rho belongs to an already-active caller store for the whole invocation. Other parameters remain reference-free.

Return(unique_local) moves the owner out of the callee. A later use of that local is invalid even though the frame terminates. A successful direct call binds the returned owner to its result local. The caller’s source argument was already consumed when entering the call and is not revived.

Replacement versus identity

P1V5 guarantees one direct owner enters and one direct owner returns on a successful value path. It does not require the returned logical cell to be the same cell.

The callee may:

• mutate and return the input owner;
• move it through local binders or tail calls;
• drop it, allocate a fresh unique cell in the anchored region, and return the replacement.

No persistent alias to either unique cell exists, and physical addresses, allocation counts, and reclamation timing are unobservable. Cell identity therefore need not be conserved. The returned scalar value and subsequent mutation remain observable.

Lifetime rule

The result region and element type exactly match the liveness anchor. The callee cannot return an owner from a different nested region because its type would differ. It cannot reopen the anchored region because active-region re-entry is already rejected.

A function with no matching anchor, a shared anchor, multiple reference-bearing parameters, an aggregate reference parameter, or an entry result fails closed.

This is ownership threading within a caller-owned region, not escaping ownership or region transfer.

Call and tail-call behavior

A direct call:

let owner2 = call f(owner1, scalar_args...)

moves owner1 left-to-right with the other arguments. On successful return, owner2 is the sole returned owner. Typed error, unhandled operation, or budget failure returns no owner and drops the consumed path.

A function whose own result is the same unique type may tail-call another valid ownership-returning function. The borrowed invocation loop retains the same logical store and returns the final owner to the original caller.

Bounded exclusions

P1V5 still rejects:

• reference-bearing entry parameters or entry results;
• Shared, aggregate, closure, or function results containing references;
• multiple reference-bearing parameters on an ownership-returning function;
• unique owners in tuples, sums, cells, closures, handlers, or operations;
• closure-call or handler-based ownership return;
• Read borrows, reborrowing, shared downgrade, partial moves, and joins;
• owners returned from a lexical region that is not anchored by the input.

Runtime semantics

The canonical interpreter moves a direct unique operand when executing Return. The same opaque logical reference, or a fresh replacement in the same active region, becomes the call result. The caller binds that result only for a successful value outcome.

No host-language move, clone, address, or destructor is semantic evidence.

Rationale

• The anchor makes store liveness explicit in existing Core types.
• Exactly one reference-bearing parameter avoids hidden shared context and keeps the proof cardinality small.
• A direct unique result composes with existing ANF Call and TailCall without new term or rvalue tags.
• Moving on Return completes the P1V4 affine story across both directions of an internal call.
• Replacement freedom preserves optimization latitude without weakening observable uniqueness.

Trade-offs

• No function can create and return the first owner without receiving an anchor.
• No method-like call may combine a unique owner with shared reference parameters.
• No scalar value can be returned alongside the owner.
• Ownership return remains unavailable through closures and handlers.
• The rule proves liveness and uniqueness, not logical-cell identity conservation.

Consequences

Positive: Core-N0 gains compositional state threading and a stronger foundation for no-alias specialization certificates.

Negative: the one-in/one-out shape is intentionally narrower than a general ownership type system.

Mitigation: unsupported shapes fail closed and can be widened only with a new ADR and proof boundary.

Revisit trigger

Add multiple or aggregate ownership results only with field-sensitive move state and exact join rules. Add owner creation without an input anchor only with explicit region capability transfer. Add shared context only when the verifier can prove it cannot alias the returned unique owner.