Core-N0 Logical Store P1V1 Contract

Status: implemented and validated
Architecture decision: ADR-0013
Core profile: P1V1

1. Claim

For every verified P1V1 program and sufficient evaluation budget, the canonical interpreter evaluates store operations against an invocation-local logical store:

alloc(rho, v) = fresh opaque location l containing v
load(l)       = the most recent value stored through any alias of l
store(l, v)   = Unit and the cell at l becomes v

No host address, allocator choice, reference count, or reclamation time is part of this relation.

2. Admitted types and operations

Cell values:

Bool | I64 | F64

Reference type:

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

Operations:

Region { region, body }
RefAlloc { region, mutability: Shared, value }
RefLoad { reference }
RefStore { reference, value }

Use copies a logical reference and therefore creates an alias to the same cell. Local tuples and sums may temporarily contain references, but reference types are forbidden recursively in every function parameter and result.

3. Regions and lifetime

• Every reference region appears in the enclosing function’s strictly ordered region-parameter list.
• Every allocation, load, and store occurs inside an active lexical Region with the same region ID.
• Re-entering an already-active region ID is rejected.
• A region closes on normal return, typed error, tail transfer, or evaluation failure.
• Every ordinary or tail-called function invocation receives a new empty logical store.
• No reference can cross an invocation boundary in this profile.

Region IDs are proof names. They do not select a physical allocator or imply a stack/arena/heap placement.

4. Effects

The verifier requires exact declared effects:

The usual call rule propagates a callee’s effect row to its caller. Non-canonical effect order, duplicates, an undeclared region, or a missing required effect fails closed.

Store operations do not appear in the public effect_trace. Their observable ordering is behavioral: a later load must observe the latest preceding store through the same logical identity. Typed Error events retain their existing trace behavior.

5. Identity and freshness

Each successful allocation in one invocation produces a location distinct from every still-live location produced earlier in that invocation.

Observable:

• a write through an alias changes later reads through the original;
• a write to one fresh reference does not change another;
• store/load program order changes returned behavior;
• the lexical lifetime is explicit in Core structure.

Not observable:

• logical location numbers;
• physical addresses or placement;
• allocation count as a trace event;
• RC operations, movement, or reclamation timing.

There is no same_identity operation.

6. Fail-closed boundary

P1V1 rejects:

• every store construct in P1V0;
• Read or Unique allocation;
• non-scalar or reference-containing cells;
• store operations outside the matching active region;
• reference parameters or results, including nested tuple/sum positions;
• loads/stores through non-reference values;
• store values whose type differs from the cell type;
• missing Alloc<rho> or State<rho>;
• undeclared or recursively re-entered lexical regions.

The evaluator has no unchecked artifact entry point.

7. Canonical encoding

P1V1 uses profile tag 1 in Core-N0 semantic encoding v1. New RValue and Term tags are append-only. Existing P1V0 bytes and hashes remain unchanged.

The locked alias-program vector is:

semantic_hash = ac526f04cef5428c41b002f978ff52f7eab3752bbee98d564e67f84b5edde5a6

8. Evidence required

• alias-visible mutation;
• independent fresh allocations;
• load/store ordering;
• lexical-region close paths;
• invocation-local store behavior through ordinary and tail calls;
• exact type/effect/region negatives;
• P1V0 compatibility and rejection;
• deterministic semantic bytes/hash plus tamper rejection;
• deterministic step-budget failure;
• full workspace, strict lint, format, governance, and documentation-link gates.

9. Non-claims

This contract is not a physical allocator, ownership/borrow checker, affine typing, RC implementation, general region polymorphism, closure capture model, Surface mutation admission, P1 partial evaluation, native code generation, or dependency closure.