Static Evaluation R0-B1 Contract

Status: implemented and validated
Authority: ADR-0024
Scope: intraprocedural P1V0 all-or-frontier evaluation

1. Objective

R0-B1 establishes the first specialization-time execution kernel. It evaluates a verified, wholly static and effect-free intraprocedural path using canonical SpecializationValue.

It is deliberately not a residual generator. A computation outside this boundary returns an explicit frontier rather than being executed speculatively.

2. Trusted input

The only entry point accepts ValidatedSpecializationRequest. That wrapper retains:

exact verified P1V0 source artifact
independently verified B0 certificate
validated canonical R0 request and hash
static/dynamic entry slots
declared specialization-step budget

There is no evaluator entry point for a raw artifact, raw request, bridge CoreValue, trace-JIT guard, or profile value.

3. Per-node authority

Before executing a term, rvalue, or operand, R0-B1 resolves its exact FunctionId + structural path judgment in the verified certificate.

The check occurs at every executed node. Permission at a parent node is not ambient authority for its descendants.

4. Admitted execution

R0-B1 executes:

Term:
  Let
  If with a certified static Bool condition
  Case with a certified static Sum scrutinee
  Return

RValue:
  Use
  Tuple
  Project
  Construct
  admitted Primitive

Primitive:
  I64 Add/Sub/Mul in Wrapping or Saturating mode
  F64 Add/Sub
  I64 CmpLt/CmpGe
  ArrayLenF64

Integer and floating behavior is identical to the canonical P1V0 interpreter. Arrays remain immutable canonical values. Static if and case evaluate only the selected branch.

5. Explicit frontiers

R0-B1 never executes:

dynamic-dependent work
certificate-denied work
checked integer arithmetic
ArrayGetF64
direct calls
tail calls

Checked arithmetic and array access remain denied even with concrete arguments because overflow and bounds errors are observable typed effects. Calls return InterproceduralDeferred; R0-B2 must implement them with an explicit continuation machine rather than host recursion.

References, allocation, mutation, closures, handlers, and operations are not P1V0. Reaching any such node after validation is an internal fail-closed error.

6. Outcome and budget

A successful API result contains:

validated request hash
Complete(canonical value)
  or ResidualRequired(node, reason)
exact consumed steps
ordered executed-node trace

One step is consumed immediately before executing one authorized canonical term, rvalue, or operand. Evidence checks and refused frontiers consume no step. The trace contains exactly one node per consumed step in execution order.

The budget is checked before consumption. Exhaustion returns:

StepBudgetExceeded(limit, used, attempted node)

and emits no partial StaticEvaluation.

7. Locked execution vector

The vector entry accepts static I64::MAX, computes wrapping addition by one, then saturating subtraction by one, and returns the result:

result = I64::MIN
steps = 10

The exact trace is:

function[0].body
function[0].LetValue[0]
function[0].LetValue[0].PrimitiveArgument[0]
function[0].LetValue[0].PrimitiveArgument[1]
function[0].LetNext[0]
function[0].LetNext[0].LetValue[0]
function[0].LetNext[0].LetValue[0].PrimitiveArgument[0]
function[0].LetNext[0].LetValue[0].PrimitiveArgument[1]
function[0].LetNext[0].LetNext[0]
function[0].LetNext[0].LetNext[0].ReturnOperand[0]

Repeated construction and execution produces the same request identity, result, step count, and trace.

8. Validation evidence

The R0-B1 corpus covers:

• exact numeric result, step count, trace, and repeated-run determinism;
• every admitted numeric primitive family and mode;
• immutable array length, tuple construction/projection, and selected static branch behavior;
• sum construction, case selection, and field binding;
• unused dynamic input versus an actually dynamic result;
• checked-overflow and bounds-effect denial without execution;
• direct and tail-call frontiers;
• exact specialization-step exhaustion with no partial artifact;
• differential agreement with the canonical interpreter for numeric, aggregate/control, and sum/case programs.

9. Non-claims

R0-B1 does not implement interprocedural static evaluation, recursion, mixed static-fact collection, residual Core, a partial evaluator, CoreVM0, Futamura P1/P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis.