GitHub

ADR-0059: Bounded physical-template preservation realization

Status: accepted
Date: 2026-08-02
Decision owners: NAUX architecture and x86-64 proof boundary

Context

ADR-0058 assigns persistent logical tail state to a sovereign finite GPR/XMM bank and independently replays physical parallel copies. It intentionally does not say how those copies become x86-64 instructions, whether surrounding instruction templates preserve the bank, or whether a template’s hidden temporary can destroy a still-live cycle scratch value.

That missing boundary is correctness-critical. In particular, materializing an F64 immediate requires a GPR temporary even though the destination belongs to the XMM bank. Treating GPR and XMM scratch lifetimes as unrelated would therefore be unsound. Emitting candidate bytes before this interaction is explicit would transfer authority to accidental encoder behavior.

Decision drivers

  • Every target-plan instruction site inside an accepted persistent region must have a finite, source-derived clobber contract.
  • The persistent GPR/XMM lanes must be disjoint from all non-frontier template clobbers.
  • Every ADR-0058 physical step must lower to a closed symbolic x86-64 template vocabulary with exact prospective lengths.
  • Frame addressing, immediate materialization, scratch use, branch layout, and retained fixups must be explicit evidence.
  • Replay must model cross-bank temporary clobbers and reject stale scratch.
  • No arbitrary instruction, raw byte, executable mapping, or external assembler may enter the proof boundary.
  • Limit exhaustion must return no partial realization.

Considered options

Extend the current raw encoder immediately

This would produce runnable bytes quickly, but byte emission would become the first specification of preservation and scratch semantics. Rejected: the proof boundary must precede executable authority.

Trust ABI caller-saved conventions

The ABI says which registers a call may destroy; it does not prove the exact templates inside a persistent region or intentional writes during tail-state transition. Rejected.

Inspect emitted bytes and infer clobbers afterward

Post-hoc disassembly is valuable later, but it cannot own the source-level decision about which templates are admitted. Deferred to the independent candidate decoder gate.

Closed symbolic instruction vocabulary plus independent replay

Derive a conservative clobber census from the verified target plan, lower only ADR-0058 steps into sealed symbolic templates, retain exact layout/fixups, and replay their state effects without emitting bytes. Accepted.

Decision

Introduce a sealed X64TailTemplateRealization bound to the exact verified R1-S7a target, ADR-0057 plan, and ADR-0058 allocation.

Preservation census

Every instruction and control site whose label belongs to an allocated persistent region is classified from the target-plan enum, not from caller metadata. The frozen conservative clobber catalog is:

move scalar/unit:       RAX, R8
move F64:               RAX, R8, XMM2
move array pair:        RAX, RDX
I64 wrapping:           RAX, RCX, R8, FLAGS
SSE2 F64:               RAX, RCX, XMM0, XMM1, XMM2
I64 setcc:              RAX, RCX, R8, FLAGS
array length:           RAX, R8
checked array get:      RAX, RCX, RDX, XMM0, FLAGS
branch condition:       RAX, FLAGS
branch-else rel32:      no data-register clobber
materialized/refused
tail frontier:          RAX, RDX, R8, XMM2

Entry, Bounds, Return, shared-join, budget, and ADR-0057 materialization boundaries remain explicit frontiers; they do not silently promise persistent state. A persistent tail terminator is realized by the transition vocabulary below rather than the legacy frame-transfer template.

The persistent bank remains exactly RDI/RSI/R9/R10/R11 and XMM3..XMM7. Any census site whose clobber set intersects this bank rejects the whole artifact.

Symbolic transition vocabulary

Only these typed operations are admitted:

GPR register copy             3 bytes
GPR disp32 frame load/store   8 bytes
XMM register copy             4 bytes
XMM disp32 frame load/store   9 bytes
movabs GPR immediate         10 bytes
GPR bits to XMM               5 bytes
near rel32 tail jump          5 bytes + one retained fixup

Frame-to-frame movement expands through the typed scratch lane. An F64 immediate expands through RAX, including when its final destination is an XMM register. Every atom records a contiguous start/end interval; no short displacement, immediate-width contraction, instruction fusion, or hidden temporary is inferred.

The final atom of every persistent transition is exactly one symbolic rel32 jump to the ADR-0057 target label. The artifact retains its patch offset, target, width, and addend but contains no displacement bytes.

Independent replay

The verifier independently:

  1. verifies the target, logical plan, and physical allocation;
  2. rebuilds the complete site census and frozen clobber sets;
  3. proves every non-frontier site preserves all persistent lanes;
  4. reconstructs transition templates from ADR-0058 schedules without trusting declared atoms, lengths, or fixups;
  5. checks contiguous layout, exact per-template length, one final rel32 jump, and exact fixup coverage;
  6. executes templates over distinct typed symbolic tokens, including RAX and XMM0 scratch contents, and compares every destination with the original parallel snapshot;
  7. rejects cross-bank scratch destruction, type confusion, undeclared clobbers, partial writes, unsupported offsets, overflow, and every locally resealed mutation;
  8. compares the complete regenerated artifact exactly.

Frozen limits

  • at most 1,000,000 preservation sites;
  • at most 4,096 persistent transitions;
  • at most 65,536 symbolic template atoms;
  • at most 4,096 retained fixups;
  • at most 64 MiB prospective transition layout;
  • at most 2,000,000 replay-work units;
  • at most 32 MiB canonical evidence.

Every counter uses checked arithmetic. Exceeding any limit returns no realization.

Consequences

  • NAUX owns the path from logical parallel copy through physical allocation to exact non-executable instruction intent without LLVM, an assembler, or a third-party register allocator.
  • Hidden scratch coupling becomes a verified state effect rather than an encoder accident.
  • The clobber catalog deliberately over-approximates policy-1.4 ordinary and register-superblock forms; it may reject a future template until that template receives a new proof.
  • The artifact grants no raw encoding, decode, native, process, standalone, measurement, claim, or global policy authority.
  • A successor ADR may propose an owned byte encoder only after this artifact is accepted and independently replayable.

Acceptance gates

  1. BranchMix and Bounds site censuses and transition realizations are deterministic and sealed to exact predecessor identities.
  2. Every allocated-region instruction/control site and every ADR-0058 transition is covered exactly once.
  3. All persistent lanes survive every non-frontier site.
  4. Register, frame, immediate, cross-bank immediate, spill, GPR cycle, XMM cycle, and mixed-bank schedules refine ADR-0058 snapshots.
  5. Layout, fixup, clobber, scratch, provenance, total, and seal mutations fail closed even when locally resealed.
  6. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and authority audits pass.
  7. Encoder policy remains exactly 1.4.0; no executable consumer exists.

Accepted evidence

The exact BranchMix policy-1.4 realization is sealed under root 078b1b0c98e5369bd621f8b1364f0b2d74d719a0ac06879867dc24c9111e67c9. Its source-derived census contains 164 persistent-region instruction/control sites. All persistent GPR/XMM lanes are absent from every non-transition clobber set; persistent transitions own their intentional destination writes through separate symbolic replay.

All 108 ADR-0058 transitions lower to 318 exact symbolic atoms with 108 retained rel32 fixups: 190 GPR atoms, 20 XMM atoms, 17 immediate atoms, 63 frame loads, and 102 frame stores. Their prospective transition-only layout is 2,135 bytes, with a 92-byte largest transition and 1,566 replay-work units. This is 655 bytes below ADR-0058’s conservative 2,790-byte transition upper bound because ADR-0059 charges exact fixed template lengths. It excludes ADR-0057 frontiers and the rest of the target image, and is neither executable code size nor a performance claim.

An adversarial mixed-bank schedule saves an I64 cycle token in RAX, then materializes an F64 immediate through RAX before consuming the token. The symbolic instruction replay rejects that structurally lowerable schedule, while accepting the canonical ordering that consumes the GPR scratch first. This freezes cross-bank scratch coupling as a checked semantic effect.

Acceptance validation passed:

  • five focused preservation/realization/verifier tests and the public ADR-0059 boundary;
  • the complete workspace suite, including 382 core library tests with zero failures and six explicitly ignored heavyweight opt-in tests;
  • strict Clippy for every package target and feature;
  • 22 governance tests and eight strict refinement closed-loop tests;
  • format, diff, and static authority audits.

The authority audit finds the verified realization only in its proof module, public re-export, and tests. No raw encoder, native runner, process worker, standalone image, measurement, or claim path consumes it. Global encoder policy remains exactly 1.4.0.

Correctness erratum — 2026-08-03

A saved cycle token in RAX/XMM0 must remain live until its scratch read; ordinary frame moves may not reuse that register in the interval. Policy 1.2.0 reserves RAX/XMM0 for live scratch and uses RCX/XMM1 for ordinary temporaries. Independent clobber replay rejects a locally resealed violation. The superseding realization root is d976fd91769b210b4e13a28ebd57a8ffa238d71d5285b62fff781fa74995b266: 168 sites, 108 transitions, 314 atoms, 186 GPR atoms, 20 XMM atoms, 17 immediates, 61 loads, 100 stores, 108 fixups, and 2,103 prospective bytes.