GitHub

Residual Evidence R0-D Contract

Status: implemented and validated
Stage: Roadmap Stage 2 / Residualization R0-D
Decision: ADR-0028
Scope: canonical sealed evidence and regenerative admission for R0-C2 Residual Core

1. Evidence payload

ResidualEvidence schema v1 binds:

evidence schema version
replay policy version
source semantic hash
interpreter-semantics hash
B0 request hash
B0 certificate hash
R0 specialization request hash
R0-B2 evaluation hash
R0-B2 exact step count
residual semantic hash
residual node count
residual canonical-byte count

The payload uses the domain NAUX:core-n0:residual-evidence:r0d:v1\0. The declared evidence_hash is excluded from its own canonical bytes.

2. Evaluation identity

The R0-B2 identity uses a separate domain and covers:

  • specialization request hash;
  • complete value or mixed-frontier halt node/reason;
  • ordered static facts and their canonical specialization values;
  • exact specialization step count;
  • ordered executed-node trace;
  • ordered skipped-node trace and reasons.

Specialization values and B0 structural nodes retain their existing domain-separated encodings inside the evaluation payload.

3. Emission

emit_residual_evidence_r0d accepts a validated request, its opaque R0-B2 record, and an R0-C2 ResidualCore. It refuses:

  • a record from another request;
  • mismatched source/request provenance;
  • an artifact rejected by the ordinary Core verifier;
  • non-canonical wrapper node/byte metrics;
  • a residual that differs from deterministic R0-C2 regeneration.

Only then is the evidence hash sealed.

4. Independent admission boundary

verify_residual_evidence_r0d accepts raw public inputs:

source CoreArtifact
B0 BindingTimeRequest
B0 BindingTimeCertificate
R0 SpecializationRequest
residual CoreArtifact
ResidualEvidence

It does not accept the emitter’s validated request, evaluation record, or ResidualCore wrapper.

Admission runs:

  1. ordinary source verification and complete B0/R0 request validation;
  2. exact provenance, schema, policy, and evidence-hash checks;
  3. ordinary residual verification plus independent node/byte recount;
  4. fresh R0-B2 replay and exact evaluation hash/step comparison;
  5. deterministic R0-C2 regeneration;
  6. exact residual program/hash/metric comparison.

Regeneration is bounded by the already validated specialization and residual budgets. Any error returns no verified evidence.

This is an independent admission/provenance boundary, not an implementation-diverse proof checker. The validator deliberately reuses the versioned R0-B2 and R0-C2 semantic kernels, as recorded by ADR-0028.

5. Locked evidence

The canonical mixed R0-D vector locks:

evaluation_hash =
35fe28eebf550682e4abb45d7bc7baa1c2a8f80e18239442465da777c3f85295

evidence_hash =
98121ecc99f317a046a35a8b313d608d26ff6a909934a22d36b77434f4e0c683

The vector contains a statically executed direct call, a static comparison, static branch selection, a dynamic frontier, skipped-node evidence, two static facts, R0-C2 call/control erasure, and dead-callee pruning.

6. Validation corpus

naux-lang/tests/residual_evidence_r0d.rs covers:

  • deterministic emission and successful raw-input verification;
  • exact locked evaluation/evidence hash vectors;
  • declaration-hash exclusion from canonical payload bytes;
  • mutation of every evidence field, including mutations resealed by the caller;
  • a forged but valid Core artifact with a recomputed evidence hash, rejected by exact regeneration;
  • forged ResidualCore provenance and metrics rejected by the emitter;
  • complete evaluation outcomes with skipped effectful work;
  • raw R0 request and B0 certificate mutation rejection;
  • source/residual result and effect-trace differential parity.

Focused R0-B2 through R0-D tests, formatting, and clippy with warnings denied pass. The complete workspace suite is the final integration gate.

7. Non-claims

R0-D establishes sealed residual provenance and regenerative validation only. It does not provide implementation-diverse formal proof, a tiny standalone checker, CoreVM0, native code generation, Futamura P1/P2, Projection Birth, dependency closure, or Nauxogenesis.

ADR-0029/ADR-0030 subsequently add the Stage 3 CoreVM0 seed and generic Core artifact, and the R1 line subsequently adds evidence-gated interpreter-loop specialization. Current status is governed only by ../ROADMAP.md. The P1 claim remains closed until all lighthouse erasure, standalone-native, correctness, and performance gates pass.