GitHub

Residual Core R0-C2 Contract

Status: implemented and validated
Stage: Roadmap Stage 2 / Residualization R0-C
Decision: ADR-0027
Scope: bounded folding and aggregate Residual Core generation from an opaque R0-B2 evaluation record

1. Boundary

R0-C2 consumes exactly:

ValidatedSpecializationRequest
opaque MixedStaticEvaluation produced by evaluate_static_r0b2

The evaluation record exposes read-only observations. External Rust callers cannot construct or mutate its request hash, outcome, trace, steps, or skipped nodes. The generator also rejects a record whose request hash differs from the validated request.

This closes the in-process same-request mutation path present in the original R0-C1 API. It is not the independently serialized and replayed R0-D evidence boundary.

2. Deterministic transformation

R0-C2 leaves generate_residual_r0c frozen as the R0-C1 regression path and adds generate_residual_r0c2.

The R0-C2 generator:

  • narrows the entry signature to dynamic slots;
  • replaces an R0-B2 static Let fact when the residual still reads it;
  • removes a proven static binding when all residual reads disappear;
  • folds an If whose condition resolves to a static Bool;
  • folds a Case whose scrutinee resolves to a static Sum;
  • binds fields of the selected constructor before the selected arm;
  • eliminates a direct call when its result binder has an R0-B2 fact;
  • retains calls whose result remains dynamic;
  • walks the post-folding call graph from the entry and retains only reachable functions, preserving original FunctionId order.

No general syntactic inlining, alpha-renaming, speculative rewriting, trace guard, or profile feedback is used.

3. Aggregate materialization

Unit, Bool, I64, and F64 use canonical Core operands.

Live Tuple and Sum values are rebuilt as existing Core Let bindings:

nested children before parents
fields in source/type order
fresh LocalIds increasing from max(source entry LocalId) + 1

An existing parameter, Let, or selected Case-field LocalId is reused for the root value. A complete aggregate result receives a fresh root LocalId. LocalId exhaustion fails closed.

P1V0 has no array literal. A static Array<F64> is therefore accepted only when transformation removes every runtime read. If a residual return, primitive, call, aggregate, or other term still needs the value, generation fails with UnsupportedLiveStaticValue.

4. Effect and control preservation

Only values actually established by R0-B2 may erase their source binding. Dynamic, denied, unavailable, or otherwise skipped work is preserved.

A Complete result collapses to a constant only when R0-B2 reported no skipped nodes. When skipped work exists, R0-C2 retains that work and may only fold control justified by static entry slots. Function effect rows remain conservative declarations and are never narrowed by R0-C2.

5. Admission gates

Before an artifact is returned:

  1. the opaque evaluation record must match the validated request;
  2. every live static value must have an exact Core representation;
  3. fresh LocalId allocation must remain in the u32 namespace;
  4. the whole residual program must fit max_residual_nodes;
  5. canonical semantic bytes must fit max_residual_bytes;
  6. CoreArtifact::seal must succeed;
  7. the ordinary Core verifier must accept the artifact.

Any failure returns no residual artifact.

6. Evidence

naux-lang/tests/residual_r0c2.rs locks:

  • static If folding and removal of an unselected checked-effect branch;
  • static Case folding and selected-field materialization;
  • a live static Tuple rebuilt for a retained dynamic call;
  • deterministic child-first nested Tuple/Sum result materialization;
  • static-array elimination after ArrayLenF64 specialization;
  • fail-closed rejection of a live static array;
  • static-call elimination and unreachable-callee pruning;
  • preservation of skipped effectful work despite a complete static result;
  • exact LocalId exhaustion behavior;
  • residual node and byte budget rejection;
  • original-versus-residual result and effect-trace parity across dynamic input vectors.

The focused R0-B2/R0-C1/R0-C2 corpus and the complete workspace test suite pass after this boundary. Clippy with warnings denied passes for the affected library and integration targets.

7. Non-claims

R0-C2 is a verified-output generator, not independent residual evidence. It does not implement R0-D, CoreVM0, standalone native code, Futamura P1/P2, Projection Birth, dependency closure, or Nauxogenesis.

The next gate is R0-D: canonical residual evidence plus an independent validator that does not trust generator-owned transformation claims.