Residual Core R0-C1 Contract

Status: implemented and validated
Authority: ADR-0026
Scope: bounded scalar-slot Residual Core generation from the R0-B2 record

1. Objective

R0-C1 produces the first verified Residual Core artifacts. It consumes a validated specialization request plus its R0-B2 evaluation record and emits an ordinary sealed P1V0 Core artifact whose behavior on every dynamic input equals the source program’s.

It is deliberately not a folding specializer: no branch is pruned, no call is inlined, and no dead function is removed. Those are R0-C2 scope.

2. Trusted input

The only entry point accepts ValidatedSpecializationRequest plus a MixedStaticEvaluation whose request hash must equal the validated request hash; any other record fails closed (RecordMismatch). There is no generator entry point for a raw artifact, raw request, or unverified evaluation record.

3. Admission boundary

every Static entry slot must be scalar: Unit, Bool, I64, F64
  (aggregate slots fail closed: UnsupportedStaticSlot);
a Complete outcome with no skipped nodes must carry a scalar
  result (otherwise UnsupportedCompleteResult).

4. Generation rules

Complete, no skips:
    residual entry = dynamic parameters only;
    body = Return(literal result); every reachable computation
    already executed statically, so no effect can be lost.
Complete, with skips:
    prologue + the original body verbatim; skipped work may carry
    observable typed effects and must survive.
MixedFrontier:
    residual entry = dynamic parameters only, original order;
    prologue: one Let per scalar static parameter, original order;
    body: the original entry body with every Let whose binder has
    a scalar static fact rewritten to Use(literal); everything
    else — skipped values, untaken branches, callees — preserved
    verbatim.

Substitution by binder is exact because the Core verifier rejects duplicate Let binders per function. Substituting a Static fact is behavior-preserving for all dynamic inputs because a Static judgment guarantees independence from every dynamic input. Non-scalar facts are not substituted; their computations remain in the body.

5. Budgets and verification

Checked in order, each failing closed:

residual nodes (one per term, rvalue, and operand across all
  functions) <= max_residual_nodes;
residual bytes (canonical Semantic Encoding v1 length)
  <= max_residual_bytes;
the sealed residual artifact passes the ordinary Core verifier.

A successful result binds the source semantic hash, the request hash, the residual artifact and its semantic hash, and the exact node and byte usage. Generation is deterministic: identical inputs produce identical artifacts and hashes.

6. Locked structure vectors

For the mixed spine a = 1 + 2; b = x * 2; c = a + 5; return b with dynamic x:

residual entry(x): a := Use(3); b = x * 2; c := Use(8); return b

For the R0-B2 locked vector (factorial call plus mixed spine):

residual entry(x): a := Use(6); b = a + x; c := Use(7); return b
callee f1 preserved unchanged

For r = s + x with static s = 5 and dynamic x:

residual entry(x): s := Use(5); r = s + x; return r

7. Validation evidence

The R0-C1 corpus covers:

• locked residual structure for the mixed spine, the interprocedural locked vector, and the static-parameter prologue, with exact term equality;
• original-versus-residual differential agreement over the canonical interpreter across dynamic input sweeps for every generated artifact;
• a Complete evaluation collapsing to Return(literal) with a narrowed empty signature;
• a skipped denied computation preserved verbatim, with both original and residual observing the same Overflow error outcome;
• repeated-generation determinism (equal artifacts and hashes);
• fail-closed rejection of a forged evaluation record, an aggregate static slot, a one-node residual budget, and an eight-byte residual budget.

8. Non-claims

R0-C1 does not implement static branch folding, call inlining, dead-function pruning, aggregate static slots, residual certificates (R0-D), CoreVM0, Futamura P1/P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis.