ADR-0037: Canonical x86-64 Target Plan and Checked Encoding

Status: accepted; R1-S7a implemented and validated; successor R1-S7b validated by ADR-0038

Date: 2026-07-28

Historical scope: the encoder rule and locked vectors in this record are the policy-1.0.0 acceptance state. ADR-0042 supersedes only that encoder policy with 1.3.0; it preserves the target schema, lowering semantics, ABI, and source-bound relation. Current identities live in the normative contract.

Extends: ADR-0036 without changing the frozen R1-S6 Machine IR schema, lowering policy, semantic identity, evaluator relation, or source-binding vectors

Context

ADR-0036 closes the target-independent trust boundary:

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

The frozen branch-mix artifact reaches that boundary with 121 functions, no direct calls, exact ordered Bounds, deterministic identity, and a 51-case finite correspondence corpus. It still has no physical representation, target operation, ABI, native byte, or executable entry.

The repository already contains an x86-64 trace-JIT encoder. It is bridge infrastructure, not a canonical backend:

• its input is VM bytecode or trace operations rather than source-bound Machine IR;
• its runtime contract contains guards, side exits, deoptimization, mutable profiles, host pointers, callbacks, and generic fallback;
• its physical register and value conventions are tied to the bridge VM;
• it may embed process addresses and resolve runtime helper calls;
• its emitted bytes do not carry the Core/SSA/Machine-IR provenance chain.

Individual instruction recipes, executable-memory tests, CPU detection, and rel32 patching techniques may be donated. The trace-JIT artifact and runtime contract cannot enter P1 evidence.

R1-S7 must therefore separate four questions:

1. What exact x86-64 target plan is the deterministic image of the admitted Machine IR?
2. What exact raw bytes and internal fixups encode that plan?
3. Can the plan be verified, replayed from its full source chain, and evaluated independently of native execution?
4. Can a later verifier-gated runner execute those exact bytes with native outcome correspondence?

Answering the first three questions is R1-S7a. The fourth is R1-S7b. Raw bytes belong to R1-S7a because a plan-only milestone would leave the instruction encoder outside the checked boundary. Executing those bytes belongs to R1-S7b because a code blob is not native correctness evidence merely because it has an x86-64 encoding.

Decision drivers

• Preserve the complete Residual Core → Core SSA → Machine IR provenance chain.
• Keep the first target package finite enough for adversarial verification.
• Preserve strict I64, F64, signed-zero, NaN, evaluation-order, and Bounds behavior.
• Preserve proper tail calls without growing the native stack.
• Give every target byte a deterministic, replayable explanation.
• Introduce no assembler, linker, runtime, or backend dependency.
• Keep target correctness separate from standalone viability and performance.
• Leave a versioned route to a later optimizing register allocator.

Options considered

Decision

R1-S7 package split

The R1-S7 umbrella is split into two non-interchangeable packages.

R1-S7a
  verified source chain
    → canonical x86-64 target plan
    → owned deterministic encoder
    → raw position-independent bytes + internal fixups
    → ordinary verification + source replay + target-plan evaluation

R1-S7b
  source-bound verified R1-S7a artifact
    → verifier-gated W^X runner
    → finite native execution correspondence

R1-S7a may be complete while R1-S7b remains open. R1-S7a must not report target-plan evaluation as native execution. R1-S7b must not accept a locally verified code artifact without the opaque source-bound R1-S7a view.

Target identity

The first target is exact:

ISA                 x86-64
environment         Linux userspace
host ABI            System V AMD64
byte order          little endian
pointer width       64
required feature    SSE2
forbidden features  x87 arithmetic, AVX, AVX2, FMA, BMI, target probing
numeric state       canonical MXCSR 0x0000_1f80
code model          one position-independent in-process code blob

Host ISA and operating-system ABI are platform contracts under the Charter. R1-S7a introduces no assembler, object writer, linker, libc routine, or third party backend into target realization. The current Rust/Cargo seed still builds the implementation and remains explicit dependency debt.

The target descriptor, ABI descriptor, feature set, numeric-state contract, lowering policy, encoder policy, and exact hard-limit vector participate in target artifact identity.

Closed source envelope

R1-S7a consumes only an artifact accepted by the authoritative R1-S6 source-bound verifier. It then admits this narrower target envelope:

types:
  Unit
  Bool
  I64
  F64
  F64Array

effects:
  []
  [Bounds]

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

terminators:
  Return
  Branch
  TailCall

Direct Call, every saturating I64 operation, checked I64, and every future Machine IR form fail closed. Wrapping multiplication is admitted only through its fixed target operation and encoder template; R1-S7a cannot exit until that path has focused evidence.

The frozen branch-mix artifact contains no direct call, so direct-call ABI, continuation frames, and error propagation across a returning callee are not needed to close this package.

Physical value representation

The physical representations are:

F64Array is read-only for the complete invocation. element_length counts F64 elements, not bytes. A target invocation admits an array descriptor only when:

• length is at most i64::MAX;
• length * 8 and the end address do not overflow;
• the data pointer is non-null when length is non-zero;
• the complete span is readable and immutable for the invocation;
• the output area is valid and does not overlap the input span.

These are typed host-admission preconditions. R1-S7a does not claim that raw x86-64 pointers prove their own validity.

ArrayGetF64Checked performs its signed-negative and upper-bound checks before the only element load. Failure transfers to the single terminal Bounds epilogue. No unchecked memory load, helper call, signal recovery, or fallback implements Bounds.

Entry and outcome ABI

The typed entry parameters are flattened into 64-bit lanes in source order:

Unit      → zero lanes
Bool      → one lane
I64       → one lane
F64       → one raw-bit lane
F64Array  → data-pointer lane, then element-length lane

At most five input lanes are admitted. They occupy the System V integer argument registers in this order:

RDI, RSI, RDX, RCX, R8

The hidden output pointer occupies the next integer argument register. No stack argument is admitted in v0.1. The entry ABI manifest records and hashes the exact lane assignment derived from the verified entry signature.

For the branch-mix lighthouse this is:

RDI  input.data
RSI  input.length
RDX  repetitions
RCX  output payload pointer

The output area is two writable 64-bit words. EAX returns the outcome tag:

0  Return
1  Bounds

On Return, payload words encode the declared result:

Unit      → {0, 0}
Bool      → {0 or 1, 0}
I64       → {two's-complement bits, 0}
F64       → {canonical F64 bits, 0}
F64Array  → {data_pointer, element_length}

On Bounds, both payload words are zero. Every other outcome tag is invalid. The runner must not expose a payload as a semantic value when the tag is Bounds.

Register and stack authority

R1-S7a uses a deterministic stack-home policy, not register allocation.

• RSP and RBP have frame-control authority only.
• RAX, RCX, RDX, R8, R9, R10, and R11 are fixed volatile integer scratch registers.
• XMM0 and XMM1 are fixed volatile scalar-F64 scratch registers.
• RDI and RSI are read only while entry lanes are copied to their homes and are not used afterward.
• No other physical register is writable by the target plan.
• The System V red zone is not used.

Every virtual register has one typed stack home. Homes are assigned in dense virtual-register order with eight-byte alignment; scalar homes use eight bytes and F64Array homes use sixteen bytes. Function home layouts overlay one maximum-size invocation home area because the admitted graph has no returning direct call.

The single invocation frame contains, in canonical order:

saved MXCSR
canonical MXCSR value
output pointer
maximum overlaid virtual-register home area
maximum outgoing tail-argument staging area
alignment padding

RSP is stable after the prologue. Every frame access uses a verified positive offset within the declared frame extent.

Under the historical encoder policy 1.0.0, a TailCall first copies every argument, left to right, into the non-aliasing outgoing area. Only after all source operands have been staged are they copied into the callee parameter homes. Control then transfers by internal jmp rel32. This is simultaneous assignment and proper constant-stack tail transfer, including cycles and overlapping caller/callee homes.

Strict numeric state

Target F64 operations use scalar SSE2 only. The entry prologue:

1. saves the caller MXCSR;
2. installs exactly 0x0000_1f80;
3. runs with round-to-nearest ties-to-even, masked exceptions, and FTZ/DAZ disabled;
4. restores the caller MXCSR on both Return and Bounds.

Signed zero and every non-NaN bit result are preserved. Observable NaN output is canonicalized to:

0x7ff8_0000_0000_0000

No fast-math substitution, reassociation, x87 extended precision, host MXCSR inheritance, or feature-selected alternate template is admitted.

Canonical target plan

The plan contains:

• the exact target and ABI descriptors;
• the exact limit vector;
• source Core, Core SSA, and Machine IR hashes;
• the entry ABI manifest;
• canonical frame and virtual-register home layouts;
• ordered functions and blocks;
• source-origin-tagged target operations and terminators;
• dense target labels;
• an entry offset fixed at byte zero.

The complete artifact additionally contains the ordered internal fixups, final raw code bytes, and separate plan, code, and complete-artifact hashes.

Target operations are physical macro operations with typed home locations and fixed scratch-register templates. There is no public arbitrary-byte operation, inline assembly node, external call, fallback node, deoptimization edge, or untyped memory operation.

Each macro operation expands through one encoder template. The encoder uses fixed-width choices:

• signed disp32 frame addressing;
• imm64 for semantic 64-bit constants where required;
• near rel32 conditional and unconditional control transfers;
• no short-branch relaxation;
• no alternative encoding selected from host features;
• no absolute code address.

Fixups and position independence

The only R1-S7a fixup kind is:

PcRel32 {
  patch_offset: u32,
  target_label: TargetLabelId,
  addend: 0
}

Fixups are stored in strictly increasing patch_offset order. The encoder:

1. emits a zero placeholder;
2. records the target label;
3. lays out every label and instruction deterministically;
4. computes target_offset - (patch_offset + 4);
5. rejects a value outside signed 32-bit range;
6. writes the little-endian displacement;
7. retains the ordered fixup table beside the final bytes.

All fixups target labels within the same artifact. External symbols, absolute addresses, loader relocations, GOT/PLT entries, TLS, data-section relocations, and process pointers are rejected.

Identity and deterministic encoding

Canonical metadata and plan encoding are handwritten, domain-separated, length-delimited, and big-endian. Raw x86-64 code bytes remain in their exact architectural little-endian form inside a length-delimited byte field.

The package uses separate identities:

plan_hash      = SHA-256(canonical target-plan bytes)
code_hash      = SHA-256(domain || length || final code bytes)
artifact_hash  = SHA-256(canonical complete-artifact bytes)

Canonical target-plan bytes end after the ordered labels. They exclude the fixup table, final code, and all three declared hashes, so no identity is circular. The complete-artifact encoding binds the plan hash, code hash, plan, home layouts, label/fixup tables, final bytes, source identities, policies, and limits. Rust layout, debug text, Serde defaults, hash-map order, allocation addresses, load addresses, CPU fingerprints, and executable-memory addresses cannot enter identity.

Verification and replay

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

• exact schema, target, ABI, feature, numeric, policy, and limit fields;
• non-zero source identities and exact plan/code/artifact hashes;
• source-envelope declarations;
• dense canonical function, block, virtual-register, origin, and label order;
• type widths, home alignment, non-overlap, frame authority, and exact frame extent;
• entry lane assignment and outcome representation;
• target-operation types and fixed scratch-register authority;
• Bounds checks before array loads;
• under policy 1.0.0, complete tail-argument staging before commit and jump;
• label uniqueness, target validity, instruction-boundary targets, and no fallthrough into data;
• fixup kind, order, patch range, target, displacement, and signed-rel32 fit;
• re-layout, re-encoding, re-patching, exact final byte equality, and the rule that every byte is explained by one admitted template;
• structural, work, byte, frame, fixup, and diagnostic caps.

The authoritative source-bound API accepts:

target artifact
source Machine IR
source Core SSA
source Residual Core

It first obtains the opaque R1-S6 source-bound Machine IR view through verify_machine_ir_source(machine_ir, source_ssa, source_core). It then verifies the supplied target artifact, compares all three source hashes, reruns deterministic target lowering and encoding, and compares exact plan bytes, fixups, code bytes, and all hashes.

A locally valid Machine IR plus copied provenance hashes is not authoritative. A fully resealed behavior mutation may pass ordinary local verification only when internally consistent, but must fail source-bound replay.

Target-plan evaluation

R1-S7a includes a bounded evaluator for the canonical target macro operations. It uses logical frame homes and immutable array descriptors; it does not mmap or execute the raw bytes.

The finite relation is:

eval_MachineIR(source-bound Machine IR, input)
≈
eval_X64TargetPlan(source-bound target plan, input)

It preserves exact non-NaN F64 bits, canonical NaN, typed return values, terminal Bounds, ordered effect traces, wrapping I64 semantics, branch behavior, and proper tail transfer. Engine work counters are non-semantic telemetry.

The same fixed 51-case manifest used at the R1-S6 handoff is required. This is target-plan correspondence, not native execution and not an infinite-domain theorem.

R1-S7b runner boundary

R1-S7b is a separate implementation and evidence gate. Its runner must:

• accept only an opaque source-bound R1-S7a artifact;
• allocate writable, non-executable memory;
• copy and re-hash the exact verified bytes;
• transition the mapping to read-execute before entry;
• never expose a writable-executable mapping;
• invoke only the declared entry offset and ABI;
• restore process numeric state on every normal semantic exit;
• record the executed code hash and reject fallback;
• compare native outcomes with source-bound Machine IR on the fixed corpus.

Crash containment, signal behavior, and malicious raw host pointers require a separate host-runner contract. R1-S7a does not gain native evidence from the existence of a future runner.

Resource limits

The accepted implementation encodes this exact identity-bound target limit vector:

The complete vector is part of target identity. Mutation and representative one-over evidence are green; an implementation cannot widen any field under the same schema and policy identities.

No producer may widen a locked limit while retaining the same schema or policy identity. Accounting is checked or fail-closed before attacker-sized allocation, plan traversal, encoding, or diagnostics.

Rationale

1. A target plan keeps physical placement and ABI decisions inspectable before byte encoding.
2. Including final bytes in R1-S7a closes the owned-encoder boundary without overclaiming that unexecuted bytes are native-correct.
3. A stack-home policy is deterministic and makes frame authority, aliasing, tail transfer, and bounds checks tractable for an ordinary verifier.
4. Whole-program tail transfer matches the frozen no-direct-call artifact and preserves constant stack without a general call convention.
5. Fixed SSE2 and MXCSR rules protect the strict numeric contract from host process state and feature-dependent code generation.
6. A single internal rel32 fixup form is enough for a position-independent lighthouse blob and avoids prematurely designing an object format.
7. Separate plan/code/artifact hashes distinguish semantic lowering, instruction encoding, and complete provenance.
8. A later optimizing register allocator can be compared against the same R1-S6 input under a new target policy rather than weakening this boundary.

Consequences

Positive:

• every admitted target byte has a source-bound plan and deterministic encoder explanation;
• VM/JIT fallback, host callbacks, and process addresses cannot enter the canonical artifact;
• proper tail calls remain constant-stack;
• checked array reads have a directly auditable physical representation;
• target realization is NAUX-owned and delegates no decision to third-party backend infrastructure, while the existing Rust seed debt remains explicit;
• target-plan evaluation can isolate lowering bugs before executable memory is involved.

Negative:

• every virtual register initially incurs a stack home;
• the first target policy is not expected to be performance-leading;
• direct calls and saturating arithmetic remain fail-closed;
• the ABI is deliberately narrow and admits no stack arguments;
• plan, verifier, evaluator, encoder, fixup replay, and later runner duplicate some concepts already present in bridge JIT code;
• Rust/Cargo still builds and runs this work, so sovereignty debt is unchanged.

Risks and mitigations:

• Risk: the encoder and re-encoder share the same implementation bug. Mitigation: fixed templates, byte golden vectors, target-plan evaluation, mutation tests, and later real native correspondence.
• Risk: a stack-home policy is too slow for Gate B. Mitigation: treat R1-S7 as a correctness boundary; introduce an evidence-gated allocation policy in a new ADR rather than hiding one here.
• Risk: raw pointer misuse causes a host fault. Mitigation: keep exact input-span preconditions and place host admission and crash containment in R1-S7b.
• Risk: host MXCSR changes numeric results. Mitigation: save, install, and restore the canonical MXCSR in the target entry/exit templates and test restoration in R1-S7b.

Acceptance

R1-S7a is implemented and validated because:

• the final locked schema, policies, target descriptor, ABI, numeric contract, and hard-limit vector are encoded and locked;
• the exact source-bound R1-S6 branch-mix artifact lowers deterministically;
• ordinary plan verification, owned encoding, fixup replay, byte verification, and full Core/SSA/Machine-IR/target source replay are implemented;
• all final bytes are explained by admitted target operations and templates;
• the fixed 51 cases pass Machine-IR versus target-plan correspondence;
• wrapping Add/Sub/Mul, F64 Add/Sub, comparisons, branches, array length, checked array access, return, and proper tail transfer have focused evidence;
• direct call, saturating arithmetic, forbidden register, unsafe memory, malformed frame, malformed fixup, byte, policy, ABI, feature, numeric-state, provenance, and cap mutations fail closed;
• a fully resealed behavior mutation fails source-bound replay;
• exact plan, code, and complete-artifact vectors are published;
• every predecessor suite and repository quality gate remains green;
• documentation continues to label native execution, standalone viability, performance, and P1 as open.

The historical policy-1.0.0 branch-mix plan/code/artifact identities are respectively 1f36987672e999523ef1a701a763a8bb5571e11fd8ddd1c7130bd68984f6eb02, cb113b0700d5b5bc7fda42e2ead5baceb6bb23444c56f19878cf963914dac97b, and cbde812f2306c1aa7439b3440eae76628eed7b92f03cdd571574e86d2d4c0c60. The ordered-Bounds plan/code/artifact identities are d1889577830314fe3bb62b139d910d81b75fc3a1d85b9b71a79c394ac89abf4f, 8e5a276de3baad3fe2a4c0fbbf8d7a0546a00d793804602ddda864fe2a31d984, and 86cb600ae30a5c211d3ece6cd981497cb102a73d3d8dbf65ae37b2884b90e67d. The normative contract publishes byte counts, physical shapes, frames, the independent 51-case result identity e04e6c508ba22ab052f71b2daec4692aa0572c4403ca26960cec191085551223, and the exact evidence boundary.

ADR-0042 and the normative target contract publish the current policy-1.3.0 tail rule and migrated identities; the historical values above are not current artifact authority.

R1-S7b requires its own implementation evidence before any native-execution claim:

• verifier-gated W^X loading;
• exact code-hash and entry binding;
• canonical ABI and MXCSR save/install/restore;
• the fixed native correspondence corpus;
• wrong ABI, changed byte, changed mapping state, invalid input admission, and fallback rejection.

Revisit trigger

A new ADR and append-only target schema or policy are required before adding:

• direct calls or returning call frames;
• saturating or checked I64 arithmetic;
• a physical register allocator, spills, coalescing, or alternate home policy;
• stack arguments, a changed entry/outcome ABI, or a general FFI ABI;
• AVX, FMA, feature-selected templates, or relaxed F64 semantics;
• writable arrays, allocation, external calls, additional effects, or effect handlers;
• external symbols, absolute relocations, object sections, an ELF writer, or a linker;
• another operating system, object format, ISA, or executable environment;
• a widened locked limit.

Related decisions

• ADR-0006 defines the strict numeric authority that the MXCSR and SSE2 rules preserve.
• ADR-0008 defines the no-third-party backend and release-path requirement.
• ADR-0035 establishes the canonical Residual Core to Core SSA handoff.
• ADR-0036 establishes the target-independent source consumed here.
• The finite implementation contract is docs/x86_64_target_r1_s7a_contract.md.

Non-claims

ADR-0037 does not establish a general R1-S6 backend, direct calls, an optimizing register allocator, standalone execution, ELF/object/executable writing, linking, symbol resolution, a libc-free runtime, raw-pointer memory safety, signal or unwind semantics, implementation-diverse or formally verified x86-64 semantics, Gate B, Gate C, benchmark eligibility, performance leadership, Futamura P1/P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.