ADR-0013: Bounded Logical Store for Core P1V1

Status: accepted
Date: 2026-07-25

Context

Core-N0 already represents logical regions, Ref types, and State<rho>/Alloc<rho> effects, but profile P1V0 deliberately rejects references and has no allocation, load, store, or explicit region-lifetime term. Stage 1 cannot claim mutation or identity semantics until the verifier and canonical interpreter agree on those operations.

The first implementation must preserve the optimizer freedom accepted by ADR-0003 and ADR-0004. It must not make host pointers, physical placement, reference counts, or reclamation timing observable. It also cannot pretend that Unique is sound before affine-use verification exists.

Options considered

Decision

Core profile P1V1 is a strict admission superset of P1V0. P1V0 keeps its existing byte representation, semantic hashes, and rejection behavior.

P1V1 adds:

Region(region, body)
RefAlloc(region, Shared, initial_value)
RefLoad(reference)
RefStore(reference, value)

The semantic store maps fresh opaque logical locations to typed scalar cells. The location allocator is deterministic inside the canonical interpreter, but location numbers and physical addresses are not Core observations.

The first admitted cell types are exactly Bool, I64, and F64. Ref<rho, Shared, T> is the only admitted reference type. Read conversion, Unique, nested references, reference-containing cells, and cycles remain outside this profile.

Every store operation must occur inside an active lexical Region for its declared region:

• RefAlloc<rho> requires the function effect Alloc<rho>;
• RefLoad<rho> requires State<rho>;
• RefStore<rho> requires State<rho>;
• the lexical scope ends on return, error, tail transfer, or evaluator failure.

References may be copied through Use, tuples, sums, and projections inside a function, so aliases observe the same cell. A reference may not occur recursively in a function parameter or result type. Therefore references cannot enter or leave a function invocation in P1V1. Each invocation owns a fresh logical store, and all its locations die before control crosses that boundary.

Function region parameters are the bounded profile’s declared logical region names. Region makes an owned lexical lifetime explicit; it does not select stack, arena, heap, RC, or any other physical placement.

Store actions do not add public evaluator trace events. Their observable order is the order reflected by subsequent loads and returned/error behavior. Making logical allocation counts observable would incorrectly forbid dead allocation removal. Effect rows remain mandatory static ordering evidence.

The semantic encoding v1 assigns a new profile tag and append-only tags for the new constructs. No existing tag, field order, domain separator, or P1V0 byte sequence changes. A decoder that does not recognize P1V1 must reject it rather than interpret it as P1V0.

Rationale

• Opaque locations preserve alias behavior without exposing representation.
• Lexical scope provides an explicit lifecycle and a verifier boundary for no-escape.
• Shared is honest about copying; Unique waits for a proof mechanism.
• Scalar cells are enough to prove freshness, mutation, and effect ordering without admitting cycles or recursive store structure.
• A new profile keeps existing golden artifacts stable while allowing the schema to advance monotonically.

Trade-offs

• References cannot yet be arguments, results, closure captures, array elements, or stored values.
• Region arguments and general region polymorphism remain absent.
• Function-local effects are conservatively visible in the function effect row even though the invocation reclaims its store.
• The canonical interpreter uses a map and monotonic logical IDs for clarity, not as a performance implementation.

Consequences

Positive: Core-N0 gains independently verified freshness, alias-visible mutation, explicit lifetime, and effect requirements without importing the bridge runtime or committing to physical allocation.

Negative: this profile is intentionally too narrow for general systems programming and does not yet prove ownership transfer or zero-cost placement.

Mitigation: unsupported mutability, escaping references, undeclared regions, missing effects, and cross-boundary references fail closed with typed verification errors.

Revisit trigger

Admit Unique only with affine-use evidence. Add reference arguments/results only with explicit region arguments, variance and no-escape rules. Add reference-containing cells or cycles only after the accepted cycle policy has a checked representation. A Surface syntax is admitted only after it can elaborate to this contract without importing bridge identity semantics.