ADR-0035: Gate A Translation Validation and Canonical Residual SSA

Status: accepted; implemented and validated

Date: 2026-07-28

Extends: ADR-0034 without changing any frozen R0 or R1-S1 through R1-S4 identity

Context

R1-S4 produces and regeneratively replays an ordinary-verifier-accepted Residual Core artifact for the frozen CoreVM0 branch-mix package. It also proves the interpreter structures forbidden by the lighthouse contract are absent. That result is necessary but does not by itself close Gate A:

• replay regenerates the artifact through the same Rust seed implementation;
• only a small branch-mix sample currently crosses the definitional Core to Residual Core boundary;
• no versioned, sealed three-engine corpus binds CoreVM0 seed, definitional CoreVM0, and Residual Core outcomes;
• the existing vm::ssa module is a surface/VM optimization prototype and cannot be the semantic handoff from canonical Core;
• the Surface and native branch_mix workload copies currently reset state on every repetition, while the frozen CoreVM0 program keeps state and sum alive across repetitions.

Gate A must therefore distinguish artifact provenance, finite behavioral validation, and the later SSA handoff. A hash is identity evidence, not a substitute for semantic validation.

Options considered

Decision

R1-S5 has three separately named obligations.

A1 — regenerative artifact correspondence

The existing R1-S4 raw-input verifier remains the artifact-correspondence authority. R1-S5 invokes it from:

CoreVM0 program
B0 request and certificate
R0 request
R1-S4 budget
claimed Residual Core
R1-S4 evidence

It must regenerate the exact canonical Residual Core and the exact sealed R1-S4 evidence. R1-S5 does not edit or reinterpret frozen S4 identities.

A2 — bounded three-engine translation validation

R1-S5 defines a versioned BoundedFiniteCorpusV1 generated internally from a fixed manifest. Callers cannot select, omit, reorder, or duplicate cases.

Every primary branch-mix case is evaluated by:

verified CoreVM0 seed
verified definitional CoreVM0
verified R1-S4 Residual Core

The relation compares:

• exact non-NaN F64 bits, including signed zero;
• one canonical NaN result class;
• typed Bounds outcomes;
• the exact ordered effect trace.

The admitted trace records effect kinds, not ArrayGet source sites. The first-read and later-read failures exercise operational ordering and bind separate step telemetry, but identical [Bounds] traces do not constitute a semantic proof of which read site failed.

Engine step counts are recorded only as non-semantic telemetry. Their different counting schedules cannot change the semantic result hash.

The corpus contains a frozen numeric/control edge list, bounded exhaustive small arrays and repetition counts, a deterministic generated corpus, and an auxiliary ordered two-read Bounds package. Every case must complete within fixed hard caps. A skipped, timed-out, or budget-exhausted case fails the whole validation.

The Surface/VM workload oracle comparison required by the lighthouse contract is a prerequisite. All maintained branch_mix workload copies must implement the canonical persistent-state repetition semantics before A2 can be green. Cross-language files are workload fixtures, not semantic authorities.

Evidence uses manual domain-separated, big-endian encoding. It binds:

• corpus, relation, replay, and evidence versions;
• interpreter, artifact, program, image, B0, R0, S4, residual, binding, and erasure identities;
• fixed execution limits and checked usage;
• ordered corpus-manifest, semantic-result, and optional telemetry hashes;
• the nested R1-S4 evidence hash;
• its own final evidence hash.

Replay verifies the cheap outer seal first, regenerates the manifest, invokes the R1-S4 raw verifier, reruns all three engines, and compares the fully regenerated evidence. This is deterministic finite translation validation through the Rust seed, not an infinite-domain theorem or an implementation-diverse proof.

H1 — canonical Residual Core to typed SSA handoff

R1-S5 adds a new NAUX-owned Core SSA under core/. It does not reuse vm::ssa as a semantic authority.

The first schema is deliberately minimal:

• deterministic function, block, and value identifiers;
• typed parameters, instructions, operands, and terminators;
• exact Core FunctionId, Type, EffectRow, Primitive, NumericMode, region parameters, entry function, and source semantic hash;
• F64 constants represented by canonical raw-bit identity;
• Copy, Primitive, and direct Call instructions;
• Return, Branch, and proper TailCall terminators.

The admitted R1-S5 lowering slice is exactly the verified S4 residual form:

Term:   Let | If | TailCall | Return
RValue: Use | Primitive | Call

There is no fallback node, unsupported placeholder, bytecode dispatch, or trace-JIT escape. Unsupported verified Core fails closed. The current tree-shaped ANF control flow has no join after If, so the first schema does not add Phi nodes.

The SSA verifier checks schema/source identity, hard caps, canonical dense identifiers, function and block order, reachability, dominance, operand availability, exact instruction and terminator types, call arity and result, effect inclusion, numeric mode, region authority, and Error<Bounds> for array access.

The SSA evaluator always verifies first. Proper tail calls replace the active frame, direct calls use a bounded explicit call stack, and primitive behavior matches the exact R1-S4 envelope: wrapping/saturating I64, signed zero, NaN, and observable Bounds. Checked I64 remains outside this handoff and is rejected fail closed.

The SSA artifact has a separate canonical encoding and semantic hash bound to the exact Residual Core source hash. Residual-to-SSA parity is a separately sealed handoff result. It strengthens the compiler pipeline but cannot make Gate B, Gate C, native closure, or a P1 performance claim green.

Rationale

1. Separate A1 and A2 claims prevent artifact regeneration from masquerading as semantic correspondence.
2. A generated fixed corpus is reproducible, mutation-testable, and honest about its finite scope.
3. Normalized semantic results keep NaN comparable while preserving every non-NaN bit pattern and ordered typed effects.
4. A canonical typed SSA creates the validation boundary needed before optimization and machine encoding.
5. The minimal tree-shaped schema covers the frozen S4 output without importing speculative generality.
6. Append-only versions preserve all prior locked vectors.

Trade-offs and consequences

Positive:

• Gate A acquires an explicit, replayable evidence object rather than a transitive collection of tests;
• a same-shape program, altered corpus, signed-zero substitution, backend-only result mutation, or forged source hash can be rejected;
• SSA can later host checked optimizations without weakening Core semantics;
• the old VM SSA remains free to evolve as a non-canonical bridge.

Negative:

• the first corpus is strong finite evidence, not a proof for arbitrary arrays and repetition counts;
• replay cost includes specialization and 51 three-engine cases;
• the first SSA form retains the 121 S4 function variants and performs no joining or optimization;
• the implementation still runs under Rust/Cargo and therefore does not reduce sovereignty debt.

Acceptance

R1-S5 is complete only when:

• canonical persistent-state branch_mix semantics are guarded across the maintained workload copies;
• A1 raw-input replay is invoked and mutation-tested from the R1-S5 boundary;
• A2 manifest and result vectors are locked and independently replayable;
• edge, exhaustive, generated, signed-zero, NaN, infinity, negative/zero repetition, and first/later Bounds cases pass all three engines;
• missing, reordered, duplicated, mutated, or budget-incomplete corpora fail closed;
• canonical SSA lowering, verification, encoding, evaluation, source binding, and mutation tests are green;
• all earlier frozen suites, full workspace tests, strict Clippy, formatting, whitespace, and Markdown links remain green.

Non-claims

ADR-0035 does not establish an infinite-domain theorem, full node-origin R1-D, implementation-diverse verification, an optimizing SSA, Machine IR, native encoding, standalone execution, Gate B/C, performance leadership, Futamura P1 or P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.