ADR-0036: Canonical Machine IR Trust Boundary

Status: accepted; implemented and validated

Date: 2026-07-28

Extends: ADR-0035 without changing the frozen R1-S5 Core SSA schema, lowering policy, semantic identity, Gate A evidence, or source-binding vectors

Context

ADR-0035 closes the fixed finite Gate A correspondence package and establishes a canonical, source-bound Residual Core to typed Core SSA handoff. The frozen branch-mix artifact reaches that boundary as verified P1V0 SSA with deterministic function, block, and value identifiers.

That handoff is not yet a backend trust boundary:

• Core SSA still carries canonical Core types, effects, and source provenance;
• the existing vm::ir, vm::ssa, and trace-JIT representations are bridge infrastructure with different fallback and deoptimization contracts;
• lowering verified SSA directly into x86-64 bytes would make an encoder responsible for type checking, control-flow validation, semantic lowering, target ABI selection, and byte encoding at once;
• physical registers, stack layout, calling convention, relocations, and target opcodes must not affect the identity of the target-independent transformation;
• a native result cannot be evidence unless the step immediately before target lowering has deterministic identity, independently replayable provenance, and executable reference semantics.

R1-S6 therefore freezes the semantic boundary between canonical Core SSA and all later target-specific work. It deliberately does not begin native encoding.

Options considered

Decision

R1-S6 adds a target-independent naux-machine-ir artifact under core/. Its authoritative API consumes both the exact R1-S5 Residual Core artifact and the P1V0 Core SSA artifact, and requires verify_core_ssa_source(source_ssa, source_core) before Machine IR lowering or source replay. A locally verified SSA plus a caller-supplied Core hash is not an admitted provenance chain. R1-S6 does not reuse a VM representation as semantic authority.

The implemented package now closes this bounded boundary with deterministic lowering, ordinary verification, source-bound regenerative replay, reference evaluation, canonical identity, hard resource limits, and focused mutation evidence. This status applies only to R1-S6; it does not admit a target backend or complete the P1 lighthouse.

Schema and identity

The first identities are:

schema name       naux-machine-ir
schema version    0.1.0
lowering policy   1.0.0
semantic domain   NAUX:machine-ir:r1-s6:semantic:v1\0
hash              SHA-256(canonical semantic bytes)

The semantic program binds:

schema
lowering_policy_version
exact R1-S6 limits
source_core_hash
source_ssa_hash
entry function
ordered functions, signatures, blocks, instructions, and terminators

source_core_hash continues the Residual Core provenance chain. source_ssa_hash names the exact verified Core SSA supplied to R1-S6. The exact limit vector includes the diagnostic cap, so changing max_diagnostics also changes the canonical bytes and semantic identity. Neither hash alone proves translation correspondence. Source-bound verification must first obtain the opaque R1-S5 Core/SSA source-bound view, then replay deterministic SSA-to-Machine-IR lowering and compare canonical bytes and the semantic hash.

Target-independent value model

The admitted types are exactly:

Unit
Bool
I64
F64
F64Array

F64Array is the Machine IR image of an immutable Array<F64, RegionId(0)>. Its physical address, descriptor layout, length representation, ownership convention, and ABI are not part of R1-S6. The verified source region authority is consumed by the closed lowering rule; R1-S6 introduces no physical memory model.

The only admitted observable effect is:

Bounds

An empty source effect row remains empty. Canonical Error<Bounds> becomes Bounds. Every other type, region form, mutability, or effect fails closed.

SSA values become target-independent virtual registers. Function, block, and register identifiers retain their deterministic dense source identifiers:

FunctionId  → MachineFunctionId
SsaBlockId  → MachineBlockId
SsaValueId  → VirtualRegister

Virtual registers are semantic names. They are not physical registers, register classes, spill slots, or allocation decisions.

Instruction envelope

The instruction set is closed:

Move
I64Binary(Add | Sub | Mul, Wrapping | Saturating)
F64Binary(Add | Sub)
I64Compare(LessThan | GreaterOrEqual)
ArrayLenF64
ArrayGetF64Checked
Call

The terminators are closed:

Return
Branch
TailCall

The deterministic lowering relation is:

There is no unsupported node, generic opcode, intrinsic escape, interpreter call, trace guard, deoptimization edge, or fallback instruction.

Numeric and error semantics

I64 arithmetic retains exact wrapping or saturating behavior. Checked I64 is outside the R1-S6 envelope.

F64 constants use canonical raw-bit identity. Signed zero remains distinct. Every NaN is represented by:

0x7ff8_0000_0000_0000

F64 addition and subtraction preserve the canonical P1V0 numeric contract. ArrayGetF64Checked evaluates the array before the index, performs an exact bounds check, and produces the ordered observable Bounds effect on failure.

Verification and evaluation

The ordinary Machine IR verifier is independent of emitter state. It checks:

• exact schema, lowering policy, limits, provenance fields, encoding, and semantic hash;
• non-empty program, exact entry, dense ordered function/block/register identifiers, and then-first depth-first block order;
• reachability, branch-tree shape, distinct and valid branch targets, and the declared CFG-depth bound;
• definition before use and exact operand, instruction-result, function-result, branch-condition, call, and tail-call types;
• direct/tail-call arity, result, and effect inclusion;
• canonical effect order and Bounds authority for checked array access;
• canonical F64 identity;
• all structural, operand, semantic-byte, and diagnostic caps.

The evaluator always verifies before execution. Direct calls use an explicit bounded call stack; proper tail calls replace the current frame. The caller-visible max_steps budget counts deterministic execution work units, not only instruction dispatches. Entry setup, direct Call, and TailCall pre-charge operand processing and register-frame work before traversing arguments, allocating a frame, or replacing one. Declarations above the R1-S6 hard caps reject. Work-unit or depth exhaustion is a typed failure and never falls back to another engine.

The semantic relation is:

eval_CoreSSA(verify_core_ssa_source(ssa, core), input)
≈
eval_MachineIR(lower_machine_ir_r1_s6(ssa, core), input)

≈ preserves exact non-NaN F64 bits, canonical NaN, typed outcomes, ordered effect traces, bounds behavior, evaluation order, and proper-tail-call behavior. Finite tests establish bounded translation validation, not an infinite-domain theorem.

Canonical encoding

Semantic encoding is handwritten, domain-separated, and big-endian:

• sequence and string lengths are checked u32;
• versions use big-endian u16;
• identifiers use big-endian u32;
• counts use checked u32; limits use their declared big-endian u64 or u32 width; I64 values and F64 bits use big-endian u64;
• variants use fixed explicit tags;
• hashes are their exact 32 bytes;
• vectors retain canonical stored order.

Serde defaults, Rust layout, debug text, pointers, host endianness, map iteration order, target triples, ABI choices, and target instruction encodings are forbidden from semantic identity.

Hard limits

The R1-S6 limits are part of the artifact and must equal these exact values:

Preflight accounting uses checked or fail-closed saturating arithmetic. A producer cannot widen a limit while retaining the R1-S6 schema, policy, or semantic identity. This applies to the verification-diagnostic cap as well as the structural, encoding, lowering, and execution caps.

Rationale

1. A source-bound Machine IR makes semantic lowering independently replayable before target-specific choices begin.
2. Virtual registers retain deterministic SSA identity without pretending that register allocation is semantic.
3. The closed type, effect, instruction, and control envelope is exactly large enough for the R1-S5 P1V0 handoff and no larger.
4. A reference evaluator isolates Machine IR correctness from any later x86-64 encoder bug.
5. Target-independent identity allows later encoders and ABIs to be compared against the same verified input.
6. Exact hard limits make hostile or accidentally explosive artifacts reject deterministically.

Trade-offs and consequences

Positive:

• the canonical compiler path gains a checkable boundary between Core SSA and target-specific lowering;
• later native encoders can be tested against a deterministic semantic source;
• provenance connects Machine IR to both Residual Core and canonical SSA;
• VM/JIT fallback semantics cannot enter P1 evidence through this boundary;
• no third-party backend dependency is introduced.

Negative:

• R1-S6 duplicates a small evaluator and verifier instead of trusting the eventual backend;
• the first form retains the tree-shaped CFG and potentially all 121 frozen branch-mix function variants;
• there are no phi nodes, joins, register allocation, ABI operations, or target addressing modes;
• F64Array is an abstract read-only sequence and still needs a separately decided physical representation;
• verification and source replay still execute under the Rust/Cargo seed and do not reduce sovereignty debt.

Acceptance

R1-S6 is implemented and validated against the accepted bounded package:

• the exact R1-S5 source-bound Residual Core/P1V0 SSA pair lowers deterministically;
• ordinary verification, source-bound regenerative replay, semantic encoding, hashing, and evaluator correspondence are implemented;
• authoritative replay composes the R1-S5 Core/SSA source verifier with the R1-S6 SSA/Machine-IR replay; a raw SSA plus arbitrary Core hash is rejected;
• the frozen branch-mix SSA and the ordered Bounds package pass Core-SSA versus Machine-IR parity;
• repeated lowering produces identical bytes and hashes;
• forged provenance, resealed behavior changes, malformed control flow, invalid types/effects/calls, non-canonical identifiers/F64 values, unsupported source features, and cap violations fail closed;
• representative structural, diagnostic, execution-work, and call-depth boundaries are exercised directly; the remaining members of the canonical limit vector are enforced by verifier/lowerer preflight without a claim that every cap has its own focused one-over fixture;
• locked Machine IR vectors are published in the R1-S6 contract;
• all frozen predecessor suites and repository quality gates remain green.

The locked implementation evidence is:

source Residual Core
  hash          fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9

source Core SSA
  hash          f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d

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

ordered Bounds Machine IR
  hash          758468a489dcd5ba2c55477a9d916530dd8c571e8dc4402194d73f3bdc6785e0
  bytes         872

bounded parity corpus
  branch_mix    46 cases
  Bounds        5 cases
  total         51 cases

focused suite
  tests         8 passed
  file          naux-lang/tests/core_machine_ir_r1_s6.rs

The 51-case evidence compares Residual Core with source-bound Core SSA and Core SSA with source-bound Machine IR for outcomes and ordered effect traces. It remains finite translation validation through the Rust seed, not an infinite-domain theorem or implementation-diverse proof.

Revisit trigger

A new ADR and append-only schema are required before adding any type, effect, instruction, control form, join/phi model, target property, physical layout, ABI concept, or widened limit. Target-specific lowering must receive its own decision after R1-S6 is implemented and validated.

Non-claims

ADR-0036 does not establish physical register allocation, stack layout, calling conventions, target opcodes, x86-64 bytes, executable memory, object or executable writing, linking, standalone execution, Gate B, Gate C, benchmark eligibility, performance leadership, Futamura P1/P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.