ADR-0025: R0-B2 Interprocedural Continuation Machine

Status: accepted
Date: 2026-07-26

Context

R0-B1 (ADR-0024) executes only the intraprocedural, wholly static and eligible path and defers every direct and tail call as an explicit frontier. The roadmap requires R0-B2 to add calls, tail calls, and recursion through an explicit continuation machine and to expose mixed static facts without executing dynamic or denied work. Host-stack recursion is forbidden.

Two verified B0 properties shape the design:

call/tail-call eligibility chains every argument eligibility
  and the callee summary, so an EligiblePure call implies an
  entirely EligiblePure callee body;
a Let term carries its continuation binding time, so a dynamic
  or denied bound value does not make the remaining static
  spine unreachable.

Options considered

Option	Benefit	Cost
Extend R0-B1 host recursion to calls	Smallest diff	Uses the host call stack; forbidden by the roadmap
Inline callee bodies before evaluation	No frames	Destroys exact B0 node identity and grows code before residualization exists
Interprocedural all-or-frontier	Simple outcome	A single dynamic value hides every static fact behind a root frontier
Explicit frame machine, value-plane skip, control-plane frontier	Mixed facts with exact per-node authority	More machine states to specify

Decision

Implement evaluate_static_r0b2 as an explicit continuation machine entered only through ValidatedSpecializationRequest.

Machine shape:

frames: Vec<Frame { function, environment, pending }>
pending: Option<{ binder, continuation term, continuation node }>
R0B2_MAX_FRAMES = 256 (aligned with the canonical interpreter
  MAX_SAFE_CALL_DEPTH)
tail calls replace the top frame and never grow the stack

Per-node authority is unchanged from ADR-0024: an executed node must resolve its exact FunctionId + structural path judgment with the expected kind; missing or kind-mismatched evidence fails closed. No Dynamic or Denied node is ever executed.

Value plane (an RValue bound by Let):

Static + EligiblePure, all read locals 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)

A skip executes nothing, consumes no step, and is appended to a deterministic ordered skipped-node list.

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

Calls: an EligiblePure call consumes one step for the call node and one per argument operand, records the caller continuation as pending, and pushes (or, for tail calls, replaces) a frame. Recursion is admitted; termination is enforced by the exact specialization-step budget and the frame cap. Exceeding either fails closed with a typed error and no partial artifact.

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. On a fully static, eligible, call-free program the R0-B2 step count and executed-node trace equal R0-B1’s exactly.

Mixed-fact identity:

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

A frontier can only surface in the entry frame: an EligiblePure call implies a fully eligible callee, so frames deeper than the entry never halt. The machine verifies this invariant and fails closed if it breaks.

Rationale

Explicit frames satisfy the no-host-recursion requirement and make call/tail-call accounting observable and testable.
Skipping at the value plane exposes exactly the static facts the R0-C residual generator needs, while the double-gate from ADR-0024 still guarantees no dynamic or denied execution.
Halting at the control plane keeps evaluation deterministic: the machine never guesses a branch, an arm, or a result it cannot prove.
The UnavailableStaticValue skip keeps static-but-denied poison sound: a value withheld by an earlier skip can never be silently recomputed.

Trade-offs

Context-insensitive B0 summaries mean a call that is static at this site but dynamic at another is skipped, not executed.
A static-but-denied value poisons its dependents into skips even though their judgments are Static + EligiblePure.
Entry-frame facts are the only facts; no partial callee entry exists.
The fixed 256-frame cap rejects deep non-tail static recursion that the step budget alone could have afforded.

These costs preserve fail-closed behavior and exact evidence; R0-C may motivate refinements through a superseding ADR.

Consequences

Positive: R0-C receives, for every halted specialization, the exact halt node, reason, ordered skips, and canonical static facts needed to generate Residual Core without re-analysis.

Negative: completing R0-B2 still produces no Residual Core, no residual verifier, and no certificate; R0-C and R0-D remain closed.

Revisit trigger

Executing any Denied node, entering a non-eligible callee, changing step or skip accounting, altering mixed-fact ordering, or changing R0B2_MAX_FRAMES requires a superseding ADR and policy version.