ADR-0024: R0-B Evidence-Gated Static Evaluation

Status: accepted
Date: 2026-07-26

Context

R0-A admits canonical static values and dynamic holes under a verified B0 certificate. R0-B must begin executing static work without reusing bridge runtime values, speculatively running denied operations, or coupling evaluation correctness to the future Residual Core generator.

B0 evidence records two independent properties for every canonical node:

binding time: Static | Dynamic
static-evaluation eligibility: EligiblePure | Denied

Static alone is not permission to execute. Checked arithmetic and array indexing can be static while still producing an observable typed error, so B0 marks them Denied.

Options considered

Option	Benefit	Cost
Reuse the canonical bridge interpreter and `CoreValue`	Broad semantics already exist	Executes through host-oriented values and an API that permits effects
Fold constants directly while emitting Residual Core	Fewer intermediate APIs	Couples evaluation, code generation, and proof failures
Execute any node classified `Static`	Maximizes early folding	Confuses dependency with permission and can trigger typed effects
Dedicated evaluator gated by both B0 dimensions	Small independent trust boundary with explicit refusal	Initially supports less than the full P1V0 language

Decision

Implement a dedicated evaluator over SpecializationValue. It may be entered only with ValidatedSpecializationRequest, which retains the exact verified source artifact and B0 certificate.

Every term, rvalue, and operand is checked against the exact B0 node identity before execution:

Static + EligiblePure → consume one step, then execute
Dynamic              → ResidualRequired(DynamicDependency)
Static + Denied       → ResidualRequired(DeniedByCertificate)
missing/wrong evidence → fail closed

R0-B is split into bounded packages:

Package	Boundary
R0-B1	Intraprocedural all-or-frontier evaluation, exact executed-node trace, no calls
R0-B2	Interprocedural calls, tail calls, recursion, and mixed static-fact frontiers

R0-B1 supports verified P1V0 let, static if, static case, return, use, tuple, projection, sum construction, wrapping/saturating integer arithmetic, floating addition/subtraction, integer comparisons, and ArrayLenF64.

Direct calls and tail calls return ResidualRequired(InterproceduralDeferred). Checked integer arithmetic and ArrayGetF64 never execute in R0-B1 because their typed errors are observable. References, closures, handlers, operations, allocation, and mutation remain outside P1V0 and fail closed if reached.

The step budget counts each authorized canonical term, rvalue, and operand immediately before execution. Exhaustion returns a typed error and no StaticEvaluation artifact. Successful and residual outcomes include the request hash, exact step usage, and deterministic ordered executed-node trace.

Rationale

A separate evaluator keeps specialization semantics free of Arc, logical references, handlers, and bridge runtime representation.
Checking evidence at every node prevents a root-level permission check from becoming ambient authority.
All-or-frontier behavior establishes effect safety and deterministic budget semantics before mixed residualization adds control complexity.
Deferring calls avoids host-stack recursion and forces R0-B2 to define an explicit continuation machine.

Trade-offs

R0-B1 residualizes programs whose safe selected path could theoretically be evaluated when B0 conservatively denies the whole root.
Unused dynamic entry parameters are allowed only when the executed nodes remain independently certified static.
Direct and tail calls are deferred even when B0 certifies them pure.
Node lookup and trace storage add bridge-time overhead.

These costs are accepted because R0-B1 is a semantic/evidence gate, not the performance implementation or final partial evaluator.

Consequences

Positive: R0-B2 and R0-C gain a small, deterministic, effect-free execution kernel whose refusals are explicit and testable.

Negative: completing R0-B1 does not complete R0-B and produces no Residual Core.

Mitigation: R0-B2 must use an explicit continuation machine, preserve the same per-node authority checks, and retain fail-closed exhaustion.

Revisit trigger

Any capability to execute a Denied node, produce a typed effect at specialization time, admit another Core profile, or change step accounting requires a superseding ADR and policy version.