GitHub

Core-N0 Existential Closure P1V2 Contract

Status: implemented and validated
Architecture decision: ADR-0014
Core profile: P1V2

1. Semantic representation

For ordered captures c0:C0 ... cn:Cn and code function:

f : (Tuple<C0 ... Cn>, A0 ... Am) ! E -> R

packing produces:

PackClosure(f, c0 ... cn)
    : Closure<(A0 ... Am), E, R>

Calling:

CallClosure(pack, a0 ... am)

is behaviorally equivalent to:

Call(f, Tuple(c0 ... cn), a0 ... am)

under the same logical store, effects, and evaluation budget whenever the environment contains a reference. For value-only environments, a fresh invocation store is observationally equivalent.

2. Capture ordering

  • Capture sequence order is semantic and encoded.
  • The hidden environment is exactly a tuple in that order.
  • Source names, hash-map iteration, host addresses, and discovery order are absent from Core.
  • Empty capture lists use Tuple<>, not a special null environment.
  • Reordering captures without changing the code function’s environment type may change behavior and always changes semantic bytes.

3. Environment typing

The verifier requires:

  • an existing code FunctionId;
  • at least one code parameter;
  • first code parameter exactly Tuple<capture operand types...>;
  • remaining code parameters exactly the behavioral closure parameters;
  • code effects exactly the behavioral closure effects;
  • code result exactly the behavioral closure result;
  • every captured reference region declared by both creator and code function;
  • every captured reference region active at the pack site.

There is no dynamic environment cast and no unchecked closure-call path.

4. Calls and effects

  • The closure operand is evaluated before explicit arguments.
  • Arguments retain Core left-to-right order.
  • Arity and types match exactly; no coercion or Any.
  • The caller effect row contains every closure effect.
  • Typed errors propagate exactly as direct-call errors.
  • Calls and recursive environment calls consume the normal deterministic evaluation budget.

P1V2 has no tail-closure term. A direct tail call containing a reference anywhere in its argument types fails verification.

5. Lifetime and aliasing

  • Closure types cannot occur recursively in function parameters or results.
  • Entry parameters and all function results cannot contain references.
  • Nested closure captures are rejected.
  • A reference capture must be live in an active lexical region.
  • Reference-containing closure calls borrow that invocation’s logical store.
  • A write through the captured alias is visible through the creator’s original reference after the call.
  • The borrowed region cannot be reopened by closure code.
  • Closure values cannot enter scalar-only store cells.

The environment is a semantic value. No physical allocation, address, RC operation, or reclamation time is observable.

6. Recursive closure behavior

Closure code may call itself directly by passing its hidden environment tuple as the first argument. If the environment contains references, the recursive call borrows the same store. Non-tail recursion is bounded by call depth; all recursion is bounded by the global step budget.

This is not a cyclic self-containing closure environment.

7. Fail-closed boundary

P1V2 rejects:

  • closure constructs in P1V0 or P1V1;
  • missing code function or hidden environment parameter;
  • non-tuple or mismatched hidden environment;
  • wrong closure-call arity or argument type;
  • call of a non-closure value;
  • missing propagated effect;
  • inactive/undeclared captured reference region;
  • closure parameter/result escape, including nested tuple/sum positions;
  • reference entry/result escape;
  • nested closure capture;
  • reference-containing tail transfer.

8. Canonical encoding

Semantic encoding v1 assigns:

profile P1V2 = 2
RValue PackClosure = 9
RValue CallClosure = 10

The tags are append-only. Existing P1V0 and P1V1 semantic bytes and hashes remain unchanged.

The canonical value-closure vector locked by the implementation has semantic hash:

ba1613399e67b828b1e629ace2236d492ae86b01d7a2c8ecd7304d27ae763e75

9. Evidence required

  • closure call versus explicit-environment direct-call parity;
  • capture ordering and empty environment;
  • exact environment, argument, result, and effect checks;
  • captured-reference alias-visible mutation;
  • finite recursive environment behavior;
  • call-depth and step-budget failures;
  • lifetime, escape, nested closure, and borrowed-tail negatives;
  • repeated-run and semantic-hash stability;
  • tamper rejection;
  • unchanged P1V0/P1V1/T2A/T2B vectors;
  • full workspace, strict lint, formatting, governance, and documentation-link gates.

10. Non-claims

P1V2 is not Surface closure admission, arbitrary first-class closure escape, heap closure allocation, RC, general region polymorphism, cyclic recursive closures, handler semantics, partial evaluation, P1/P2, native lowering, or dependency closure.