GitHub

Core-N0 Ownership Return P1V5 Contract

Status: implemented and validated
Architecture decision: ADR-0017
Core profile: P1V5

1. Admitted result

An internal function may return:

UniqueRef<T> = Ref<rho, Unique, T>
T = Bool | I64 | F64

No entry function or aggregate result may contain a reference.

2. Liveness anchor

An ownership-returning function must have exactly one parameter containing any reference. That parameter must be a direct UniqueRef<T> exactly equal to the result type.

f(owner: UniqueRef<T>, scalar_args...) -> UniqueRef<T>

The anchor proves that rho is active in the caller’s logical store throughout the call.

3. Return move

return owner

consumes the direct unique local. Returning an already-moved owner is an OwnershipViolation.

A successful Call binds the returned owner to its ANF result binder. The source argument remains moved:

let owner2 = call f(owner1)
use owner1  // rejected
use owner2  // valid

4. Success cardinality

One owner enters and one owner returns on every successful value path.

The result may be:

  • the original owner;
  • a local move of that owner;
  • an owner returned by a valid tail call;
  • a fresh replacement allocated in the same anchored region.

Typed error, unhandled operation, or evaluation failure returns no owner. Affine dropping is valid.

5. Region safety

  • result region and element type equal the anchor;
  • the anchored region is active at function entry;
  • the anchored region cannot be reopened;
  • a different nested region cannot satisfy the result type;
  • a function without an anchor cannot return an owner.

P1V5 does not transfer or escape the region itself.

6. Tail return

An ownership-returning function may tail-call another function with the same unique result type. The owner moves into the tail callee, the borrowed invocation retains the logical store, and the final owner returns to the original direct caller.

7. Fail-closed boundary

P1V5 rejects:

  • ownership results in P1V0–P1V4;
  • entry reference results or parameters;
  • shared, tuple, sum, closure, or nested-reference results;
  • no anchor, a shared anchor, a mismatched anchor, or multiple reference-bearing parameters;
  • use-after-call of the consumed source;
  • return-after-move and duplicate call arguments;
  • aggregate, closure, handler, operation, or cell containment;
  • closed-region and unanchored owner escape.

8. Canonical encoding

Semantic encoding v1 uses:

profile P1V5 = 5

No new type, mutability, rvalue, term, or effect tag is required. Existing P1V0–P1V4 vectors remain unchanged.

The locked P1V5 mutate-and-return vector is:

09006d69756a52fd1fe1dfc36cd198d1a40122a5201fbcfe73ccd6d538a9290a

9. Evidence required

  • direct mutate-and-return followed by caller borrow/move;
  • consumed caller source rejection;
  • local move then return and return-after-move rejection;
  • branch-local and tail-call ownership return;
  • fresh same-region replacement;
  • no/shared/multiple/mismatched anchor negatives;
  • entry, aggregate, capture, operation, and closed-region negatives;
  • typed error and exact budget behavior;
  • deterministic semantic bytes/hash and tamper rejection;
  • unchanged P1V0–P1V4 and T2 vectors;
  • full workspace, strict lint, formatting, governance, shell, and link gates.

The executable corpus is core_ownership_return_p1v5.rs.

10. Non-claims

P1V5 is not aggregate ownership, multi-value return, identity-preserving ownership, owner creation without an input anchor, general region transfer, escaping ownership, general borrowing, partial moves, ownership through closures/handlers, P1/P2, native lowering, or dependency closure.