ADR-0026: R0-C1 Scalar-Slot Residual Core Generation

Status: accepted
Date: 2026-07-26

Context

R0-B2 (ADR-0025) produces, for every specialization, either a complete canonical value or a mixed static-fact frontier: the halt node, an ordered skipped-node list, and the entry frame’s canonical static facts. R0-C must turn that record into the first real Residual Core artifact — verified canonical Core, not bridge bytecode or a trace — while enforcing the declared residual node and byte budgets and refusing anything it cannot prove.

Two verified properties make a simple, sound generator possible:

the Core verifier rejects duplicate Let binders (DuplicateId), so a
  LocalId names exactly one binding site per function;
a Static judgment means the bound value is independent of every
  dynamic input, so substituting its canonical value is behavior-
  preserving for all dynamic inputs.

Options considered

Decision

Implement generate_residual_r0c as a bounded R0-C1 package over the validated request plus its R0-B2 evaluation record.

Admission (fail closed):

the record's request hash must equal the validated request hash;
every Static entry slot must be a scalar (Unit, Bool, I64, F64);
a Complete outcome must carry a scalar result.

Aggregate static slots (Tuple, Sum, Array<F64>) and aggregate complete results are refused with typed errors; they are R0-C2 scope.

Generation:

Complete(scalar v):
    residual entry = dynamic parameters only,
    body = Return(literal v); only the entry function is emitted.
MixedFrontier:
    residual entry = dynamic parameters only, in original order;
    prologue: one Let per static parameter binding its LocalId to
      its literal slot value, in original parameter order;
    body: the original entry body with every Let whose binder has a
      scalar static fact rewritten to Use(literal fact); all other
      terms, rvalues, and functions are preserved unchanged.

Non-scalar facts are not substituted; their original computations remain in the residual body, which is still behavior-preserving. Skipped dynamic and denied work is preserved verbatim for runtime execution.

Budgets and verification (fail closed, in this order):

residual nodes = terms + rvalues + operands of the residual program,
  checked against max_residual_nodes;
residual bytes = canonical Semantic Encoding v1 length, checked
  against max_residual_bytes;
the sealed residual artifact must pass the ordinary Core verifier.

The result binds the source hash, request hash, residual semantic hash, and exact node/byte usage. Generation is deterministic: identical inputs produce byte-identical residual artifacts and hashes.

Rationale

• Substitution keyed by Let binder is exact because the verifier enforces binder uniqueness per function.
• Static facts are dynamic-input-independent by the B0 Static judgment, so substitution preserves behavior on every dynamic input, not just observed ones.
• Preserving untaken branches and skipped work keeps the residual total: it is an ordinary verified P1V0 artifact with no dependence on the evaluator, the certificate, or the trace.
• Refusing aggregates keeps the v1 encoding surface identical to existing scalar literal operands; no new Core constructs are introduced.

Trade-offs

• No static branch folding, call inlining, or dead-function pruning yet: the residual keeps the original control skeleton and possibly dead callees.
• Static aggregate inputs (for example a static Array<F64> program) cannot be residualized in R0-C1.
• The residual entry re-evaluates substituted constants at runtime instead of collapsing them transitively; downstream folding is R0-C2/R0-D scope.

These costs keep R0-C1 small enough to be exhaustively evidenced while the differential story (original versus residual over dynamic inputs) is established.

Consequences

Positive: the first verified Residual Core artifacts exist, with locked structure vectors, deterministic hashes, budget enforcement, and original-versus-residual differential evidence over the canonical interpreter.

Negative: R0-C1 alone does not deliver the folding specializer the P1 lighthouse needs; R0-C2 (aggregates, branch folding, pruning) and R0-D (residual certificates) remain closed.

Revisit trigger

Admitting aggregate slots, folding static control flow, pruning functions, changing the node-count or byte-count rule, or emitting anything that bypasses the ordinary Core verifier requires a superseding ADR and policy version.