Static Evaluation R0-B2 Contract

Status: implemented and validated
Authority: ADR-0025
Scope: interprocedural P1V0 continuation machine and mixed static-fact frontiers

1. Objective

R0-B2 extends the R0-B1 execution kernel with direct calls, tail calls, and recursion through an explicit continuation machine, and exposes mixed static facts at every frontier so the R0-C residual generator can consume them without re-analysis.

It does not rely on the host call stack, and it never executes a Dynamic or Denied node.

2. Trusted input

The only entry point accepts ValidatedSpecializationRequest, exactly as R0-B1. There is no evaluator entry point for a raw artifact, raw request, bridge CoreValue, trace-JIT guard, or profile value.

3. Continuation machine

frames: explicit Vec of { environment, pending caller continuation }
R0B2_MAX_FRAMES = 256 (aligned with the canonical interpreter
  MAX_SAFE_CALL_DEPTH)
tail calls replace the top frame and never grow the stack
recursion is admitted; termination is enforced by the exact
  specialization-step budget and the frame cap

Exceeding the frame cap fails closed with FrameBudgetExceeded; exceeding the step budget fails closed with StepBudgetExceeded. Neither emits a partial artifact.

4. Per-node authority and the two planes

Per-node authority is unchanged from R0-B1: every executed node resolves its exact FunctionId + structural path judgment with the expected kind; missing or kind-mismatched evidence fails closed.

Value plane (an RValue bound by Let):

Judgment / state	Behavior
`Static + EligiblePure`, reads available	consume steps and execute (calls included)
`Dynamic`	skip, bind a hole (`DynamicDependency`)
`Static + Denied`	skip, bind a hole (`DeniedByCertificate`)
authorized but a read local is a hole	skip, bind a hole (`UnavailableStaticValue`)

Control plane (If condition, Case scrutinee, Return operand, TailCall): a dynamic, denied, or unavailable node halts the machine with a mixed static-fact frontier instead of skipping.

Term plane: a term node consumes one step only when it is itself Static + EligiblePure; walking a non-eligible Let spine is structural traversal, not execution.

An EligiblePure call implies an entirely EligiblePure callee body, so a frontier can only surface in the entry frame. The machine verifies this invariant and fails closed if it breaks.

5. Calls and step accounting

An eligible call consumes one step for the call node and one per argument operand, records the caller continuation, and pushes a frame; an eligible tail call consumes one step for its term node and one per argument operand and replaces the top frame. Skips, refused frontiers, frame pushes, pops, and caller resumption consume no step.

On a fully static, eligible, call-free program the R0-B2 step count and executed-node trace equal R0-B1’s exactly.

6. Outcome and mixed-fact identity

A successful API result contains:

validated request hash
Complete(canonical value)
  or MixedFrontier(halt node + reason,
                   static facts of the entry frame)
exact consumed steps
ordered executed-node trace (one node per consumed step)
ordered skipped-node list (encounter order, with reasons)

Mixed-fact identity is locked as:

static facts: (LocalId, canonical SpecializationValue) pairs of the
  halted entry frame, ascending LocalId
executed trace: execution order
skipped list: encounter order
halt: exact node identity plus reason

7. Locked execution vector

The vector entry takes one dynamic I64 input x and computes:

a = f1(3, 1)      f1 = proper-tail-call factorial (a = 6)
b = a + x         dynamic → skipped
c = a + 1         static  → 7
return b          dynamic → mixed frontier

The locked result is:

outcome  = MixedFrontier
halt     = function[0].LetNext[0].LetNext[0].LetNext[0].ReturnOperand[0]
           (DynamicDependency)
facts    = [Local 1 = I64 6, Local 3 = I64 7]
skipped  = [function[0].LetNext[0].LetValue[0] (DynamicDependency)]
steps    = 65
trace    = begins at the eligible call node
           function[0].LetValue[0]; one node per step

Repeated construction and execution produces the same request identity, outcome, facts, skips, step count, and trace. The full 65-node trace is locked by tests/static_evaluate_r0b2.rs:: the_locked_interprocedural_mixed_vector_is_stable.

8. Validation evidence

The R0-B2 corpus covers:

exact call and tail-call execution with locked step counts and full executed-node traces;
R0-B1 equality of result, steps, and trace on fully static call-free programs, including Use and Project operand children;
terminating tail recursion (factorial) and terminating non-tail recursion (summation) with canonical-interpreter differential agreement;
fail-closed frame-cap exhaustion for deep non-tail recursion;
fail-closed step exhaustion for an unbounded eligible tail loop;
mixed static-fact collection past skipped dynamic values, with locked facts, skips, halt, steps, and trace;
static-but-denied poison: a skipped denied value forces dependents to skip as UnavailableStaticValue without execution;
a dynamic call skipped without entering its callee;
an unused dynamic parameter still completing statically;
repeated-run determinism of every locked outcome.

9. Non-claims

R0-B2 does not implement Residual Core generation, a residual verifier, a residual certificate, partial callee entry, context-sensitive binding times, CoreVM0, Futamura P1/P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis. R0-C and R0-D remain closed.