GitHub

ADR-0060: Owned tail-template byte capsule and independent decoder

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

Context

ADR-0059 accepts exact symbolic x86-64 template intent for persistent tail transitions, including register/frame operands, clobbers, instruction lengths, and retained rel32 fixups. It emits no bytes. The next boundary must establish that NAUX can own canonical machine encoding and independently recover its meaning without LLVM, an assembler, or a disassembler.

The transition slices are not yet embedded in a complete target image, so their target labels have no candidate code addresses. Leaving rel32 fields zero or unresolved would not prove the encoder. Reusing policy-1.4 label offsets would be misleading because the new slices have different lengths.

Machine bytes also erase logical word distinctions such as Bool, I64, and array data/length. A decoder cannot invent those types from identical mov opcodes. Typed correspondence must therefore bind independently decoded machine shape to the already verified ADR-0059 atom, never to an encoder receipt.

Decision drivers

  • The encoder must accept only the closed ADR-0059 instruction vocabulary.
  • Every byte, prefix, opcode, ModR/M, SIB, displacement, immediate, and rel32 field must have one canonical form.
  • Every rel32 must resolve to a finite in-capsule target.
  • The decoder must be structurally separate and must not call encoder helpers.
  • Decoder output must recover instruction boundaries, registers, frame offsets, immediates, control targets, and clobbers before comparison with typed ADR-0059 atoms.
  • Type-erased machine shapes must receive types only from exact predecessor correspondence, not from capsule metadata.
  • No byte buffer returned by this boundary may be mapped, executed, linked, timed, or globally selected.

Considered options

Patch against policy-1.4 label offsets

Rejected. Those offsets describe a different image and provide no proof that the new transition layout fits at the old sites.

Leave rel32 placeholders plus fixup receipts

Rejected. It would test opcode emission but defer the most layout-sensitive field.

Embed complete target blocks now

Rejected. That would mix transition encoding with native candidate selection, frontier integration, and whole-image control-flow authority before the closed vocabulary is independently decoded.

Synthetic finite transition capsule with trap anchors

Concatenate transitions in canonical edge order. Append one INT3 byte for each distinct target label in canonical label order. Resolve every final jmp rel32 to its target’s trap anchor. Accepted. The anchors are proof layout objects, not executable target blocks.

Decision

Introduce a sealed X64TailCandidateCapsule bound to the exact verified target, ADR-0057 logical plan, ADR-0058 allocation, and ADR-0059 realization.

Canonical machine grammar

GPR copy:       REX.W [R/B] 89 /r
GPR frame load: REX.W [R]   8B mod=10,r/m=100; SIB=00_100_100; disp32
GPR frame store:REX.W [R]   89 mod=10,r/m=100; SIB=00_100_100; disp32
XMM copy:       F2 0F 10 /r
XMM frame load: F2 0F 10 mod=10,r/m=100; SIB=00_100_100; disp32
XMM frame store:F2 0F 11 mod=10,r/m=100; SIB=00_100_100; disp32
GPR immediate:  REX.W [B] (B8+rd) imm64
GPR bits→XMM:   66 REX.W [B] 0F 6E /r
tail jump:      E9 rel32
target anchor:  CC

All integer fields are little-endian. Frame accesses always use disp32 and the exact RSP SIB above; disp8 contraction is forbidden. Redundant/unknown legacy prefixes, alternate mov directions, address-size override, non-RSP bases, and semantically equivalent encodings are noncanonical.

Finite capsule layout

Transitions are ordered by edge ordinal and placed contiguously from offset zero. Each receipt records exact start/end only as redundant sealed evidence. Distinct target labels are sorted and assigned consecutive one-byte INT3 anchors immediately after transition code. Every final rel32 is computed from the end of its own jump to the exact anchor using checked signed-32-bit arithmetic. No padding, alignment gap, trailing byte, or unresolved fixup is allowed.

The capsule records transition receipts, anchor receipts, resolved fixup receipts, code bytes, a domain-separated code hash, totals, and a capsule seal. These receipts are not decoder authority.

Independent decoder

The decoder lives in a separate module and shares no opcode emission helper. Starting only from verified ADR-0059 boundaries plus capsule bytes, it:

  1. independently reconstructs transition and anchor ranges;
  2. parses each instruction from prefixes/opcodes/ModR/M/SIB and exact remaining length;
  3. rejects unknown, redundant, truncated, overlapping, or trailing forms;
  4. computes each jump destination from signed rel32 and maps it to the unique derived anchor offset;
  5. emits untyped decoded machine operations, boundaries, operands, and independently derived clobbers;
  6. binds each decoded operation one-to-one with the exact ADR-0059 atom;
  7. takes logical word type only from that exact predecessor atom after machine shape matches, because the bytes deliberately erase it;
  8. reconstructs typed atoms and requires complete equality with ADR-0059;
  9. independently derives receipts, totals, code hash, and complete capsule identity.

Frozen limits

  • at most 4,096 transitions;
  • at most 65,536 decoded atoms;
  • at most 4,096 target anchors and resolved fixups;
  • at most 65 MiB capsule code;
  • at most 2,000,000 decoder-work units;
  • at most 64 MiB canonical capsule evidence.

All offsets, lengths, displacements, counters, and allocations use checked arithmetic. Any failure returns no verified capsule.

Consequences

  • NAUX owns canonical bytes for the persistent transition vocabulary and a separately written inverse parser.
  • The synthetic anchors make all fixups concrete while honestly withholding whole-image target-block authority.
  • Type erasure is explicit: byte decoding proves machine shape; the typed predecessor proves logical interpretation.
  • The capsule is not a replacement target image and grants no native, process, standalone, ELF, linker, timing, claim, or global policy authority.
  • A successor ADR must first bind every persistent-region body operand/result and every ingress/egress frontier to the ADR-0058 physical state. Merely splicing transition slices into policy-1.4 frame-based blocks would be semantically wrong. Only after that site/state proof may a later ADR compose and decode a whole image before any native correctness gate can begin.

Acceptance gates

  1. BranchMix and Bounds capsules are deterministic and source-bound through the complete ADR-0057/58/59 identity chain.
  2. Every ADR-0059 atom maps to one exact instruction range; every byte belongs to one transition atom or one derived target anchor.
  3. Every rel32 resolves exactly to its unique canonical anchor.
  4. Independent decode reconstructs all machine shapes, operands, boundaries, clobbers, and typed ADR-0059 correspondence.
  5. Single-byte exhaustive mutation for bounded fixtures plus targeted prefix, opcode, ModR/M, SIB, displacement, immediate, anchor, truncation, trailing, receipt, total, provenance, hash, and seal mutations fail closed.
  6. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
  7. Global encoder policy remains exactly 1.4.0; no executable consumer exists.

Accepted evidence

The exact policy-1.4 BranchMix predecessor chain deterministically produces:

  • capsule root 88654ac5fc21b6f142ca4c808e04846b11540f4a2a1ebf58665d026e2fae1de2;
  • code root 96c3daf0f3989fa81ea399cd079430ea2849d3e3df3b2f4192ca044a6c5af296;
  • 108 transitions, 318 decoded atoms, 108 anchors, and 108 resolved fixups;
  • 2,135 transition bytes plus 108 trap-anchor bytes, exactly 2,243 capsule bytes;
  • 2,669 encoder-work units and 2,561 independently derived decoder-work units.

Locked vectors cover every admitted instruction family. Exhaustively flipping one bit in each of all 2,243 BranchMix byte positions is rejected by the independent decoder. Truncation, trailing data, and locally resealed code, receipt, total, and predecessor-identity mutations also fail closed. The Bounds fixture and a public three-function cyclic-tail fixture establish the same proof-only boundary without changing their accepted target code.

On 2026-08-02, focused unit and public-boundary tests, strict Clippy, format, and the complete workspace suite passed. The core library reported 385 passed and 6 explicitly ignored research-cost tests; the isolated process corpus passed in 365.61 seconds; Gate A passed 3/3. Static authority inspection found no production mapping, native-call, process, standalone, ELF, timing, measurement, or encoder-helper dependency in the capsule decoder. Global encoder policy remained exactly 1.4.0.

Correctness erratum — 2026-08-03

Policy 1.1.0 encodes and independently decodes the reserved scratch and ordinary-temporary register distinction inherited from ADR-0059. The superseding capsule/code roots are bbaaf8a209b29194cdc19765b16b4c4ccc6108b3774e24d70d215979c8cf85f4 / abb57afc62f6de04a25ab1c97ef648a0975b6c0bde2fd2035337efbc55c474d6. The exact capsule has 108 transitions, 314 atoms, 108 anchors and fixups, 2,103 transition bytes, 108 anchor bytes, and 2,211 total bytes. Old roots may not authorize downstream artifacts.