GitHub

CoreVM0 Gate A and Residual SSA R1-S5 Contract

Status: implemented, finite-validated, and independently replayed

Stage: Roadmap Stage 3 / pre-native P1 lighthouse

Decision: ADR-0035

1. Purpose

R1-S5 closes the finite Residual-Core correctness evidence required by Gate A for the frozen CoreVM0 branch-mix program and defines the first canonical, verifier-gated Residual Core to NAUX-owned typed SSA handoff.

R1-S5 is append-only. It does not alter any R0 or R1-S1 through R1-S4 policy, request, artifact, or evidence identity.

2. Claim boundaries

The package keeps three claims separate:

A1  raw-input regenerative artifact correspondence
A2  bounded three-engine behavioral correspondence
H1  verified Residual Core to canonical typed SSA handoff

A1 delegates exact source-to-residual regeneration to the frozen R1-S4 raw verifier. A2 supplies the missing finite semantic corpus. H1 establishes a new compiler validation boundary after Residual Core.

Completing H1 cannot compensate for an A1 or A2 failure. Completing all three does not imply Gate B, Gate C, native execution, performance graduation, or a Futamura projection.

2.1 Sealed Residual Core ↔ Core SSA correspondence

ADR-0040 adds a stage-owned 1.0.0 correspondence protocol over the same ordered 51-case Gate A manifest. Each record binds the canonical input, Residual Core identity, Core SSA identity, exact/canonicalized outcome, and ordered effect trace. Verification replays the source binding and regenerates all executions; a detached or fully resealed fabricated result is rejected.

The domain-separated ordered result root is:

18db0347094dfad000e7a6401cd1d989edd57f44bd0b31a9544d80f3803ba58b

This closes the previously test-only semantic identity at H1. It remains finite translation validation, not an infinite-domain theorem.

3. Canonical branch-mix workload

The frozen program has:

state : I64 = 0
sum   : F64 = +0.0

for each repetition:
    for each array value:
        state = wrapping(state + 17)
        if state >= 97:
            state = wrapping(state - 97)
        if state < 48:
            sum = sum + value
        else:
            sum = sum - value

return sum

state and sum are initialized once per kernel invocation and persist across repetitions. Resetting either value inside the repetition loop is a different workload and fails the Surface/VM workload-oracle prerequisite.

The verified CoreVM0 program, not a Surface or foreign-language copy, remains the semantic authority. Maintained Surface, C, C++, Rust, Go, and Zig copies are parity fixtures for later benchmark eligibility.

4. A1 artifact correspondence

R1-S5 consumes the raw R1-S4 replay boundary:

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

The verifier must rebuild the definitional artifact and B0 certificate, validate R0, rerun R1-S4 specialization and structural erasure, and compare:

  • canonical Residual Core semantic bytes;
  • exact Residual Core semantic hash;
  • exact sealed R1-S4 evidence.

Rust PartialEq, host pointer identity, and IEEE NaN equality are not artifact identity relations.

5. A2 corpus

The evidence emitter and verifier generate BoundedFiniteCorpusV1 internally. No public API accepts a caller-selected case list.

The ordered v1 corpus contains exactly 51 cases:

  1. 10 numeric and control edges, including empty and odd-length arrays, negative, zero, one, and multiple repetitions, signed zero, infinities, finite extremes, normal/subnormal boundaries, and distinct positive and negative NaN payload inputs;
  2. 20 bounded-exhaustive cases: every array of length zero through one over the exact alphabet [-1.0, -0.0, +0.0, +1.0], crossed with repetitions -1..=2;
  3. 16 generated cases from the frozen LCG seed, multiplier, increment, length, repetition, and value mappings;
  4. five fixed ordered two-read Bounds cases covering first-read failure, later-read failure, signed-zero return, NaN return, and infinity return.

The broader seed-only nucleus suites remain separate supporting evidence; the 51-case set is the corpus that crosses all three engines and is replayed by default repository gates. Its exact order, count, manifest hash, semantic result hash, and separate telemetry hash are locked. Adding, removing, reordering, or changing a case requires a new append-only corpus version.

6. Three-engine relation

Every primary case runs through:

evaluate_corevm0
evaluate_definitional_corevm0
evaluate verified R1-S4 Residual Core

All engines must complete inside their fixed budgets. A skipped case or budget failure invalidates the complete evidence object.

Results normalize only for cross-engine comparison:

ReturnF64Bits(u64)  for every non-NaN result
ReturnNaN           for every NaN result
ErrorBounds

ReturnF64Bits preserves +0.0 and -0.0 as distinct. Normalizing NaN outputs does not normalize raw corpus inputs: input F64 payload bits remain part of the case identity.

The ordered observable effect trace is semantic:

[]              for successful branch-mix results
[ErrorBounds]   for the admitted bounds failure

This slice observes the exact sequence of effect kinds, but Bounds carries no read-site label. First-read and later-read failures are exercised and have different deterministic work telemetry; that telemetry is supporting operational evidence, not a semantic proof of which read site raised the otherwise identical Bounds event.

Engine step counters and call-depth watermarks are not part of semantic equality. If recorded, they receive a separately labeled telemetry hash.

7. Resource bounds

The implementation fixes and hard-caps:

  • total case count;
  • cumulative array elements;
  • per-case CoreVM0 steps;
  • per-case Core steps and call depth;
  • checked cumulative execution usage;
  • R1-S4 specialization budgets inherited without widening.

All counts use checked arithmetic. Wall-clock time is an external CI/operator limit and does not enter deterministic semantic identity.

8. Gate A evidence and replay

Canonical encoding is manual, domain-separated, length-delimited where required, and big-endian. Debug output, Serde defaults, native layout, host map order, and encounter-dependent identifiers are forbidden.

Evidence binds:

  • schema, corpus, relation, replay, and evidence versions;
  • Core interpreter, definitional construction, artifact, program, and image identities;
  • B0 request/certificate and R0 request identities;
  • every S4 policy, request, control, table, residual, binding, erasure, and evidence identity;
  • execution budgets and checked usage;
  • exact ordered manifest, semantic-result, and optional telemetry hashes;
  • case/category counts;
  • the final evidence hash.

Replay order is:

  1. reject oversized case, input, record, or effect-trace shapes before attacker-controlled vectors are encoded;
  2. validate the top and nested evidence seals;
  3. regenerate the canonical manifest and reject structural disagreement;
  4. invoke R1-S4 raw replay;
  5. rerun every required engine and normalize its outcome and trace;
  6. regenerate every hash and compare the entire evidence object;
  7. return an opaque verified record.

This is same-seed deterministic translation validation over a bounded finite domain. Documentation, APIs, and diagnostics must not call it a theorem or proof of the infinite input domain.

9. H1 canonical typed SSA

The canonical SSA is a separate core artifact whose identity binds the source Residual Core semantic hash.

The first admitted schema contains:

Operand      Unit | Bool | I64 | F64Bits | Value
Instruction  Copy | Primitive | Call
Terminator   Return | Branch | TailCall

It preserves exact canonical Core function/type/effect/region/numeric metadata. Function, block, and value identifiers are deterministic and dense. F64 literal identity uses canonical bits, never host float equality.

The first lowerer accepts only:

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

Every input Core artifact passes the ordinary verifier before lowering. Anything outside the admitted slice fails closed; there is no fallback, Unsupported node, trace-JIT escape, or direct native bypass.

The SSA verifier checks:

  • schema and exact source provenance;
  • hard caps and canonical order;
  • dense IDs, valid targets, reachability, and dominance;
  • definition-before-use and exact operand/result types;
  • primitive arity, types, and numeric mode;
  • direct/tail-call arity, types, result, regions, and effects;
  • Bool branch conditions;
  • exact function returns;
  • Error<Bounds> authority for array access.

The evaluator verifies before execution, uses an explicit bounded call stack, replaces the current frame for proper tail calls, and preserves canonical Core wrapping/saturating numeric, typed-error, observable-effect, and array-read semantics. Checked I64 is outside the exact R1-S4 handoff and fails closed.

The initial handoff performs no optimization. Any future SSA optimization must be a separately identified checked pass and its output must pass the ordinary SSA verifier again.

10. Required negative evidence

At minimum, tests reject:

  • a one-bit mutation of every evidence identity class;
  • independently mutated version, lineage, count, budget, usage, manifest, result, telemetry, and top-seal classes;
  • a fully resealed raw-input mutation rejected by canonical manifest regeneration and a fully resealed backend-result/telemetry mutation rejected only after complete evidence regeneration;
  • omitted, duplicated, reordered, or reclassified corpus cases;
  • raw input F64 bit mutations, including signed zero and NaN payloads;
  • one-backend-only outcome or effect-trace mutation;
  • nested B0/R0/S4 evidence or budget mutation;
  • same-shape static program/image substitution;
  • forged or recomputed Residual Core identity;
  • forged SSA source hash or semantic hash;
  • non-dense IDs, invalid branch/tail targets, use-before-definition, type/arity/effect/numeric-mode changes, and F64 bit substitution;
  • exact execution step/call-depth boundaries, oversized preflight rejection, checked count/usage arithmetic, and bounded verifier diagnostics.

Repeated emit/replay from identical raw inputs must produce identical bytes and hashes.

11. Locked implementation vectors

Gate A:

corpus       edge=10 exhaustive=20 generated=16 bounds=5 total=51
manifest     0c4e4e796d60d571c874fd37b87e0418e1240f469a03672a6a4af4a4047b4e8f
results      bc755f8a99b6cbffaa7fee7d1e7cbc81de7787249a2dc5ba83458798a2366249
telemetry    f5d709e2713fac7f2268ad6da4855010dc7978a61529adfd74cf7b34b9ef1a29
evidence     5c2d81b3cd20ef72e41437b1426156642404a1c736faf7cace70ffe1e82c5f01
usage        seed=4665 definitional_core=509714 residual_core=7274

Frozen R1-S4 to canonical Core SSA:

source       fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
ssa          f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d
bytes        18750
shape        functions=121 blocks=139 instructions=23
control      branches=9 tail_calls=127 direct_calls=0

The Gate manifest crosses all three engines. Core-to-source-bound-SSA parity reuses the same 46 branch-mix cases plus the five ordered two-read Bounds cases. These vectors identify the finite Rust-seed evidence package; they are not native or performance identities.

12. Exit

R1-S5 exits only after:

  • the workload-oracle prerequisite is corrected and guarded;
  • A1 and A2 evidence emit, seal, mutate, and replay fail closed;
  • exact corpus and result vectors are locked;
  • canonical SSA lowers the exact R1-S4 branch-mix residual;
  • Core-vs-SSA edge, exhaustive, generated, numeric, bounds, and effect parity is green;
  • all frozen predecessor suites and repository quality gates remain green.

13. Non-claims

R1-S5 does not establish full node-origin R1-D, an infinite-domain theorem, implementation-diverse proof, optimized SSA, Machine IR, native/object/ executable emission, standalone viability, Gate B/C, benchmark eligibility, performance leadership, Futamura P1/P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.