Canonical Machine IR R1-S6 Contract

Status: implemented, bounded-validated, and source-replayed

Stage: Roadmap Stage 3 / pre-native P1 lighthouse

Decision: ADR-0036

1. Purpose

R1-S6 defines the first canonical, target-independent Machine IR trust boundary after the verified R1-S5 Core SSA handoff.

It gives Residual Core + Core SSA → Machine IR a closed admission envelope, deterministic lowering, canonical identity, ordinary verification, compositionally source-bound regenerative replay, reference evaluation, and exact resource limits before any target encoder is admitted.

R1-S6 is append-only. It does not alter R1-S5 Core SSA, Gate A evidence, Residual Core, or any earlier identity.

2. Claim boundaries

The package keeps three claims separate:

M1  deterministic source-bound Core/SSA to Machine IR lowering
M2  ordinary verification plus composed Core/SSA/Machine-IR replay
M3  bounded Core-SSA versus Machine-IR evaluator correspondence

Completing M1 cannot compensate for an M2 or M3 failure. Completing all three does not produce native code and cannot make Gate B, Gate C, performance, or Futamura P1 green.

M1, M2, and M3 are implemented and validated for the exact bounded R1-S6 envelope and frozen evidence below. This is a completed pre-native trust boundary, not completion of the P1 lighthouse.

The authoritative path is:

verified Residual Core
  → source-bound canonical Core SSA
  → canonical target-independent Machine IR

vm::ir, vm::ssa, trace operations, JIT guards, deoptimization, generic opcode handlers, and backend fallback are not authorities on this path.

2.1 Sealed Core SSA ↔ Machine IR correspondence

ADR-0040 turns M3 from a test-only comparison into its own 1.0.0, stage-separated evidence protocol. It carries exactly 51 canonical records, fixed execution limits, both workload source chains, and an order-sensitive aggregate root. Admission source-replays Core SSA and Machine IR and regenerates every observation.

The accepted ordered result root is:

3cc7cbd876531ea6f88c56f50c851eb168ac76afe2d9a05ae6835687bf411205

R1-S8 authority carries this root together with its manifest, schema, policy, limit vector, record count, and both profile identities. Copying the root without full replay grants no authority.

3. Source admission

The authoritative lowerer accepts both the Residual Core artifact and the Core SSA artifact. It first requires verify_core_ssa_source(source_ssa, source_core) to establish the R1-S5 Core-to-SSA source binding; ordinary verification of either artifact alone is insufficient. The admitted Core SSA must have:

schema             core-ssa@0.1.0
lowering policy    1.0.0
profile            P1V0

The additional closed R1-S6 envelope is:

types:
  Unit
  Bool
  I64
  F64
  read-only Array<F64, RegionId(0)>

effects:
  []
  [Error(Bounds)]

instructions:
  Copy
  Primitive
  direct Call

terminators:
  Return
  Branch
  TailCall

Only these primitives are admitted:

I64Add(Wrapping | Saturating)
I64Sub(Wrapping | Saturating)
I64Mul(Wrapping | Saturating)
F64Add
F64Sub
I64CmpLt
I64CmpGe
ArrayLenF64
ArrayGetF64

Checked I64, writable arrays, any region other than the admitted RegionId(0) array authority, Tuple/Sum, references, closures, handlers, arbitrary effects, and every future Core/SSA form reject with a bounded path-specific diagnostic.

4. Schema and provenance

The exact R1-S6 identity is:

MACHINE_IR_SCHEMA_NAME              = "naux-machine-ir"
MACHINE_IR_SCHEMA_VERSION           = (0, 1, 0)
MACHINE_IR_LOWERING_POLICY_VERSION  = (1, 0, 0)
MACHINE_IR_SEMANTIC_DOMAIN          =
  "NAUX:machine-ir:r1-s6:semantic:v1\0"

MachineIrProgram contains:

schema
lowering_policy_version
limits
source_core_hash
source_ssa_hash
entry
functions

source_core_hash must equal the supplied Residual Core semantic hash and the Core hash carried by the source-bound Core SSA. source_ssa_hash must equal the supplied Core SSA semantic hash. Both are non-zero and enter canonical Machine IR identity.

Provenance metadata is necessary but not sufficient. The authoritative source-bound verifier must first obtain the opaque R1-S5 Core/SSA source-bound view from verify_core_ssa_source, then rerun deterministic SSA-to-Machine-IR lowering and compare:

• exact canonical Machine IR semantic bytes;
• exact Machine IR semantic hash;
• the supplied source Core and SSA identities;
• exact schema, policy, limits, entry, signatures, and body.

A fully resealed Machine IR behavior mutation therefore remains independently well-formed only if ordinary verification permits it, but it must fail source-bound replay.

5. Target-independent model

5.1 Identifiers

MachineFunctionId(u32)
MachineBlockId(u32)
VirtualRegister(u32)

The lowerer preserves the corresponding Core SSA numeric identifiers and canonical vector order. Functions, blocks, parameters, and instruction results remain dense. A virtual register is not an x86-64 register, register class, stack slot, or spill location.

5.2 Types

MachineType =
    Unit
  | Bool
  | I64
  | F64
  | F64Array

F64Array denotes the logical immutable sequence admitted by the source type Array<F64, RegionId(0)>. R1-S6 specifies array length and checked indexed-read behavior, not descriptor layout, pointer representation, alignment, ownership, or calling convention.

5.3 Effects

MachineEffect = Bounds

Function effect vectors are canonical, ordered, and duplicate-free. A checked array read requires Bounds in the current function. A caller must admit every effect of a direct or tail callee.

5.4 Operands

MachineOperand =
    Unit
  | Bool(bool)
  | I64(i64)
  | F64Bits(u64)
  | Register(VirtualRegister)

F64Bits preserves signed zero. Every NaN is canonicalized to:

0x7ff8_0000_0000_0000

The verifier rejects a non-canonical NaN payload.

6. Instructions and control

The complete instruction schema is:

Move(operand)

I64Binary {
  operation: Add | Sub | Mul,
  mode: Wrapping | Saturating,
  left,
  right
}

F64Binary {
  operation: Add | Sub,
  left,
  right
}

I64Compare {
  operation: LessThan | GreaterOrEqual,
  left,
  right
}

ArrayLenF64 { array }
ArrayGetF64Checked { array, index }
Call { function, arguments }

The complete terminator schema is:

Return(operand)

Branch {
  condition,
  then_block,
  else_block
}

TailCall {
  function,
  arguments
}

The result rules are exact:

There is no phi node because the admitted R1-S5 CFG is a tree: block zero is entry, every non-entry block has exactly one incoming edge, and blocks are stored in then-first depth-first preorder.

7. Deterministic lowering

lower_machine_ir_r1_s6(source_ssa, source_core) performs:

1. verify_core_ssa_source(source_ssa, source_core);
2. checked lowering-work preflight;
3. ordered one-to-one function, parameter, block, instruction, operand, and terminator lowering;
4. canonical Machine IR sealing;
5. ordinary Machine IR verification of the emitted artifact.

The mapping is:

Core SSA Copy                    → Move
I64 Add/Sub/Mul Wrapping         → I64Binary Wrapping
I64 Add/Sub/Mul Saturating       → I64Binary Saturating
F64 Add/Sub                      → F64Binary
I64 CmpLt/CmpGe                  → I64Compare
ArrayLenF64                      → ArrayLenF64
ArrayGetF64                      → ArrayGetF64Checked
direct Call                      → direct Call
Return/Branch/TailCall           → Return/Branch/TailCall

Input iteration order is canonical source order. The lowerer performs no optimization, block joining, call folding, register allocation, instruction selection, or target legalization.

Any unsupported source form rejects the complete translation. It is never represented by a placeholder or redirected to the VM, interpreter, trace JIT, or generic runtime.

8. Canonical semantic encoding

Encoding is manual, domain-separated, length-delimited where required, and big-endian:

prefix:
  semantic domain bytes
  schema name length:u32 + UTF-8 bytes
  schema version:u16,u16,u16
  lowering policy:u16,u16,u16
  limits in the fixed order from section 9
  source_core_hash:32 bytes
  source_ssa_hash:32 bytes
  entry:u32

vectors:
  length:u32
  ordered elements

scalars:
  variant tags:u8
  ids:u32
  I64:i64 big-endian
  F64 bits:u64 big-endian
  resource values:u64 or u32 as declared

Instruction, operand, type, effect, and terminator variants use fixed explicit tags:

After the program envelope, each function encodes fields in this exact order:

function id
parameter sequence of (virtual register, type)
effect sequence
result type
entry block
block sequence

Each block is:

block id
instruction sequence
terminator

Each instruction is:

result virtual register
declared result type
tagged instruction and its ordered fields

Call and tail-call arguments are length-delimited operand sequences. A branch encodes its condition, then target, and else target in that order.

Semantic identity is:

SHA-256(canonical semantic bytes)

Rust layout, Debug, Serde defaults, pointer identity, host endian, hash-map order, target triple, CPU features, ABI, and native opcodes cannot enter these bytes.

9. Exact resource limits

MachineIrProgram.limits must equal MachineIrLimits::r1_s6():

Lowering work includes functions, parameters, effects, blocks, instructions, and every instruction/terminator operand. The lowerer uses checked arithmetic. Verifier saturation is a fail-closed overflow marker because every admitted cap is below u64::MAX. Verifier preflight completes before attacker-sized semantic traversal or encoding where possible.

Evaluation also receives a caller budget. max_steps names deterministic execution work units, not merely dispatched instructions. Entry-frame construction, direct Call, and TailCall charge their operand processing and frame-slot work before that work is performed; ordinary instruction and terminator dispatch also charges work. The effective work-unit and call-depth limits cannot exceed the R1-S6 hard caps. Exact-limit execution may succeed; the next charged unit fails with a typed budget result.

The diagnostic cap is a field of MachineIrLimits::r1_s6(), is encoded in the canonical limit vector, and therefore participates in Machine IR identity. The diagnostic vector is capped. Reaching the cap produces one bounded structural-limit diagnostic instead of unbounded error amplification.

10. Ordinary verification

verify_machine_ir checks at minimum:

• exact schema, policy, full limit record, non-zero provenance, semantic bytes, and semantic hash;
• non-empty program and a valid canonical entry;
• function IDs equal ordered vector positions;
• block IDs equal ordered vector positions and entry block is zero;
• parameter registers begin at zero and instruction results continue densely in canonical block order;
• all structural, edge, operand, register, CFG-depth, semantic-byte, and diagnostic limits;
• distinct valid branch targets, branch-tree incoming-edge counts, reachability, and then-first depth-first order;
• register definition before use along the active tree path;
• exact operand and instruction-result types;
• canonical F64 values;
• exact return and Boolean branch types;
• direct/tail-call target, arity, argument, result, and effect compatibility;
• Bounds authority for every ArrayGetF64Checked.

Success returns an opaque verified view. Consumers do not construct verified status themselves.

11. Source-bound verification and replay

verify_machine_ir_source(machine_ir, source_ssa, source_core):

1. calls verify_core_ssa_source(source_ssa, source_core) and retains its opaque source-bound view;
2. verifies the claimed Machine IR;
3. compares the supplied Core identity, source-bound SSA identity, source_core_hash, and source_ssa_hash;
4. reruns the same deterministic SSA-to-Machine-IR lowering over the verified source-bound SSA;
5. compares exact semantic bytes and semantic hash;
6. returns an opaque Core/SSA/Machine-IR source-bound verified view.

This relation rejects a forged source field and a behavior mutation even if a caller recomputes the outer Machine IR hash. A locally valid SSA paired with an arbitrary non-zero Core hash cannot enter this authoritative path.

Replay uses the same Rust seed implementation. It is deterministic translation validation, not implementation-diverse verification or a formal theorem.

12. Reference evaluation

Every evaluator verifies before execution. Evidence-producing paths require source-bound verification.

Execution uses:

• a dense virtual-register environment bounded by the exact live-slot cap;
• an explicit continuation stack bounded by 256 suspended direct callers, plus the active frame;
• frame replacement for proper TailCall;
• checked execution-work charging bounded by the caller declaration and 100,000,000-work-unit hard cap;
• pre-charging of entry, direct-call, and tail-call operand/frame work before argument traversal, register-frame allocation, or frame replacement;
• exact wrapping/saturating I64 semantics;
• canonical P1V0 F64 addition, subtraction, signed zero, and NaN behavior;
• immutable F64 array length and ordered checked access;
• an ordered Bounds effect followed by typed bounds failure.

The correspondence relation is:

evaluate_source_bound_core_ssa(
  verify_core_ssa_source(source_ssa, source_core),
  input
)
≈
evaluate_machine_ir(
  lower_machine_ir_r1_s6(source_ssa, source_core),
  input
)

The comparison preserves:

ReturnF64Bits(u64)  for every non-NaN value
ReturnNaN           for NaN
typed non-F64 values
ErrorBounds
ordered effect trace

Machine and SSA execution-work counters are non-semantic telemetry because the two evaluators charge work differently.

13. Validated positive evidence

The implemented and validated package establishes:

• the frozen R1-S4 residual and its exact source-bound R1-S5 SSA lower into deterministic verified Machine IR;
• two lowerings of an identical source-bound Core/SSA pair have identical structure, bytes, and hash;
• ordinary and source-bound verification accept the canonical result;
• all 46 branch-mix Gate A inputs produce Core-SSA/Machine-IR outcome and effect parity;
• the five ordered two-read Bounds cases preserve successful results, first/later failure behavior, signed zero, canonical NaN, infinity, and ordered effects;
• direct call, proper tail call, wrapping/saturating arithmetic, comparison, branch, array length/read, empty effect, and Bounds effect fixtures pass;
• representative structural, diagnostic, execution-work, and call-depth exhaustion paths are exercised directly;
• all frozen predecessor suites and repository quality gates remain green.

The verifier and lowerer enforce the applicable structural, CFG-depth, operand, lowering-work, semantic-byte, and diagnostic caps from section 9. The evaluator separately enforces live-register, execution-work, and direct-call-depth caps. The focused R1-S6 suite does not claim a separate one-over fixture for every individual cap; enforcement scope and directly exercised evidence are kept distinct.

14. Required rejection behavior

The verifier/lowerer contract requires rejection of:

• invalid source SSA and every unsupported source type, effect, mutability, region, primitive, or checked-I64 mode;
• altered schema, lowering policy, any limit, source Core hash, source SSA hash, entry, semantic hash, or canonical bytes;
• a fully resealed behavior mutation under source-bound replay;
• non-dense, duplicate, reordered, missing, or out-of-range function, block, or register identifiers;
• missing entry, unreachable block, CFG cycle, duplicate incoming edge, non-canonical block order, same-target branch, and invalid target;
• use before definition, result-type mutation, operand-type mutation, non-Boolean branch, and return mismatch;
• missing/extra call arguments, invalid callee, call-result mismatch, tail-result mismatch, and missing callee effects;
• checked array access without Bounds;
• F64 signed-zero substitution and non-canonical NaN payload;
• one-over hard limits, accounting overflow, oversized encoding, execution-work exhaustion, call-depth exhaustion, and live-register exhaustion;
• any attempt to encode a fallback, target opcode, physical register, ABI, or native address in the canonical schema.

The focused suite directly exercises representative mutations across provenance, identity, structure, types/effects/control, canonical F64, diagnostic saturation, execution work, and call depth. It does not represent a fixture-per-bullet proof of the entire rejection surface. Repeated emit and replay from identical inputs must produce identical bytes, hashes, results, effects, and rejection diagnostics.

15. Locked implementation vectors

The exact R1-S5 source boundary remains:

Residual Core  fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
Core SSA       f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d
SSA bytes      18750
shape          functions=121 blocks=139 instructions=23
control        branches=9 tail_calls=127 direct_calls=0

These immutable R1-S5 inputs feed the following locked R1-S6 outputs:

branch-mix Machine IR
  source Core      fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
  source SSA       f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d
  Machine IR       1b1e303af18630fb6249b8427f25ce9ce17b05718679f097fcf5afffd0782b0f
  bytes            16916
  shape            functions=121 blocks=139 instructions=23
  control          branches=9 tail_calls=127 direct_calls=0

ordered Bounds Machine IR
  Machine IR       758468a489dcd5ba2c55477a9d916530dd8c571e8dc4402194d73f3bdc6785e0
  bytes            872

The bounded evaluator-correspondence corpus contains:

branch_mix         46 cases
ordered Bounds      5 cases
total              51 cases

Every case compares Residual Core with source-bound Core SSA and Core SSA with source-bound Machine IR. The relation preserves exact outcomes, non-NaN F64 bits, canonical NaN, typed Bounds, and ordered effect traces. Engine-local step fields report execution-work counts and remain non-semantic telemetry.

Focused implementation evidence:

suite    naux-lang/tests/core_machine_ir_r1_s6.rs
tests    8 passed; 0 failed; 0 ignored

The suite covers deterministic lowering, composed Core/SSA/Machine-IR source binding, resealed behavior rejection, representative identifier/order/type/effect/control-flow/NaN/limit mutations, direct-call depth, constant-stack tail calls, ordered Bounds, execution-work exhaustion, locked structure and identity, and all 51 bounded parity cases. The complete limit vector is verifier-enforced; this focused evidence does not claim an independent boundary fixture for every cap.

16. Exit

R1-S6 has exited its bounded pre-native package because:

• M1, M2, and M3 all pass;
• exact Machine IR vectors are locked;
• positive, representative mutation/budget, and replay evidence is green;
• the implementation exports only verifier-gated public execution and source-binding paths;
• predecessor and repository gates remain green;
• documentation retains the pre-native claim boundary.

A later ADR may now separately propose target ABI lowering or reuse/extension of an x86-64 encoder. This exit does not itself admit either one.

17. Non-claims

R1-S6 does not establish physical registers, register allocation, stack frames, calling convention, target legalization, x86-64 instructions or bytes, executable memory, object/executable emission, relocation, linking, standalone viability, Gate B, Gate C, benchmark eligibility, performance leadership, Futamura P1/P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.