GitHub

Core-N0 Affine Unique P1V4 Contract

Status: implemented and validated
Architecture decision: ADR-0016
Core profile: P1V4

1. Admitted owner

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

RefAlloc<rho, Unique>(value) creates one direct affine owner of one fresh opaque logical cell.

2. Affine rule

For every control-flow path:

moves(owner) <= 1

Dropping an owner is valid. Borrowing does not consume it. Borrowing or moving an already-moved local is an OwnershipViolation.

3. Moves

The following consume a direct unique local:

let new_owner = use old_owner
call f(old_owner)
tailcall f(old_owner)

The destination binder or callee parameter becomes the sole owner. Arguments move left-to-right, so duplicate use in one argument vector fails deterministically.

4. Borrows

RefLoad(unique_owner)
RefStore(unique_owner, scalar)

borrow without consuming. Multiple sequential loads/stores are valid while the owner remains live.

There is no first-class borrow value, Read conversion, shared downgrade, or loan escape in P1V4.

5. Function boundary

  • entry parameters contain no references;
  • internal direct parameters may be direct unique references;
  • all function results contain no references;
  • a unique direct call consumes the caller owner;
  • a unique tail call transfers ownership in the same logical store;
  • shared or aggregate reference tail transfer remains rejected.

6. Branches

If and Case clone the incoming affine state for mutually exclusive arms. Each arm is checked independently. Core-N0 has no post-branch continuation or implicit ownership join.

7. Rejected containment

Unique cannot occur recursively in:

  • tuples or sums;
  • arrays or logical-store cell values;
  • closure captures or closure behavioral types;
  • handler captures;
  • operation signatures;
  • function results or entry parameters.

This keeps the owner a direct local and prevents hidden duplication.

8. Runtime relation

  • a move removes the unique source local from the interpreter environment;
  • destination/callee receives the same opaque logical reference;
  • load/store borrow the current owner;
  • region close destroys all remaining cells regardless of normal return, typed error, unhandled operation, or budget failure;
  • physical placement and host copying are unobservable.

9. Fail-closed boundary

P1V4 rejects:

  • Unique in older profiles;
  • use-after-move by borrow or second move;
  • duplicate owner arguments;
  • aggregate, closure, or handler containment;
  • entry/result escape;
  • shared-reference tail transfer;
  • Read allocation or reference types;
  • unique logical-cell values and nested references;
  • missing region or State/Alloc effects.

10. Canonical encoding

Semantic encoding v1 uses:

profile P1V4 = 4
Mutability Unique = 1

No new type, rvalue, term, or effect tag is required. Existing profile vectors remain unchanged.

The locked P1V4 repeated-borrow vector is:

f314f6e72535bf12b6b42aa962a4a34c70845a7eefa709e7242b190b95fa27a9

11. Evidence required

  • repeated unique load/store before move;
  • Use move parity and source invalidation;
  • direct and tail-call ownership transfer;
  • duplicate argument and use-after-move rejection;
  • independent branch ownership states;
  • aggregate, closure, handler, entry, result, and shared-tail negatives;
  • alias-visible mutation without persistent alias creation;
  • region/error/unhandled/budget cleanup behavior;
  • deterministic semantic bytes/hash and tamper rejection;
  • unchanged P1V0–P1V3 and T2 vectors;
  • full workspace, strict lint, formatting, governance, shell, and link gates.

The executable corpus is core_unique_p1v4.rs.

12. Non-claims

P1V4 is not general borrowing, partial moves, aggregate ownership, shared downgrade, escaping ownership, ownership-returning functions, unique closure capture, first-class affine continuations, physical placement, P1/P2, native lowering, or dependency closure.