Residualization R0 Contract

Status: implemented and validated through R0-D
Stage: Roadmap Stage 2
Prerequisite: complete verified Binding-Time B0 certificate

1. Objective

R0 turns a verified P1V0 Core artifact, a verified B0 certificate, and concrete static inputs into a verified Residual Core artifact without performing observable effects or silently widening budgets.

R0 is the first real partial-evaluation path. It must not reuse trace-JIT guards, bridge profiling, or existing bytecode specialization as proof.

Implementation slices:

R0-B packages:

R0-C packages:

2. R0-A implemented boundary

An R0-A request binds:

verified P1V0 source artifact
validated B0 request
verified B0 certificate
ordered entry specialization slots
specialization policy version and hash
max specialization steps
max residual nodes
max residual bytes
max static-value nodes
max static-array elements

Each entry slot is exactly one of:

Static(canonical P1V0 value)
Dynamic(expected P1V0 type)

Requirements:

• every Static slot corresponds to a Static B0 entry classification;
• every Dynamic slot corresponds to a Dynamic B0 entry classification;
• each static value matches the exact verified Core parameter type;
• dynamic slots contain no hidden example or profile value;
• the request binds the source, interpreter semantics, B0 policy/request, and verified B0 certificate hash;
• values and policy use separate identity domains, while every budget is included in the domain-separated request identity;
• unknown, missing, reordered, mistyped, over-budget, or forged input fails closed.

R0-A performs no Core evaluation and produces no Residual Core.

Its byte-level format, hard caps, admission rules, and locked vectors are specified by Specialization R0-A Encoding v1.

3. Static-value scope

The target value domain is the immutable, reference-free P1V0 value subset:

Unit
Bool
I64
F64
Tuple
Sum
read-only Array<F64>

Canonical value identity must preserve observable P1V0 semantics:

• all NaN payloads normalize exactly as Core Semantic Encoding v1;
• signed zero remains distinct;
• tuple and constructor fields preserve canonical order;
• sum type/constructor identity is explicit;
• array length and element order are explicit;
• value and aggregate sizes consume declared request budgets.

References, closures, handlers, external handles, host pointers, bridge runtime objects, and opaque Rust layout are not admitted.

4. R0-A validation evidence

The Rust seed implements:

• a dedicated specialization-value representation separate from interpreter runtime values;
• canonical value, policy, and request encodings and SHA-256 identities;
• exact verification of source, interpreter, B0 request/policy/certificate, R0 policy, entry, slot, type, and budget fields;
• recursive tuple, sum, and read-only Array<F64> type checking;
• static-value node, static-array element, specialization-step, residual-node, and residual-byte budgets with fixed hard caps;
• golden vectors plus provenance, certificate, arity, slot-kind, recursive type, zero-budget, over-cap, and identity mutation tests.

Passing R0-A validation admits a request boundary only. No API in R0-A evaluates Core or emits a residual artifact.

5. Later R0 slices

R0-B may execute only work whose exact node is certified both Static and EligiblePure. Denied, dynamic, or unknown work residualizes or fails under an explicit policy; it never executes by default. The evaluator uses only canonical SpecializationValue, not bridge interpreter values.

R0-B1 is all-or-frontier and intraprocedural. It either produces one complete canonical result or an explicit dynamic/denied/call frontier. R0-B2 adds direct calls, tail calls, and recursion through an explicit continuation machine that does not rely on the host call stack, and collects mixed static facts at every frontier.

The implemented R0-B1 semantics, locked trace, and evidence corpus are specified by Static Evaluation R0-B1 Contract. The implemented R0-B2 machine, mixed-fact identity, locked vector, and evidence corpus are specified by Static Evaluation R0-B2 Contract.

R0-C must emit verified canonical Core rather than bridge bytecode or a trace. Every residual artifact must pass the ordinary Core verifier before it becomes evidence.

R0-C1 provides scalar fact substitution and static-parameter prologues. R0-C2 adds Tuple/Sum materialization, static If/Case folding, elimination of calls whose results were established by R0-B2, deterministic reachability pruning, and an eliminate-or-refuse policy for static arrays. The precise boundary and validation corpus are specified by Residual Core R0-C2 Contract.

R0-D must bind source, request, B0 certificate, residual artifact, budgets, and structural correspondence. An independent validator must reject forged or incomplete residual evidence and differential tests must compare original and residual behavior over dynamic inputs.

R0-D implements that admission boundary with canonical evaluation/evidence hashes and exact bounded regeneration from raw public inputs. Its format, locked vectors, mutation corpus, and explicit non-claim of algorithmic diversity are specified by Residual Evidence R0-D Contract.

6. Acceptance direction

R0 is not complete until:

• static-value/request encodings have locked vectors;
• mistyped or B0-inconsistent slots fail closed;
• specialization executes no denied effect;
• exhaustion is deterministic and returns no falsely complete artifact;
• residual Core is deterministic and verifies;
• original/residual differential behavior agrees for the admitted corpus;
• forged residual certificates fail independent validation;
• code growth and specialization cost remain within declared budgets.

7. Non-claims

Completing R0-B1 does not implement interprocedural or mixed static evaluation, a partial evaluator, Residual Core, CoreVM0, Futamura P1/P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis.