GitHub

ADR-0066: Sovereign ABI-envelope byte capsule

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

Context

ADR-0065 accepts one closed non-executable semantic image whose internal body, frontier, transition, relocation, ownership, and CFG evidence independently replay. Its entry adapter, return epilogue, and Bounds epilogue deliberately remain one-byte typed INT3 terminals. The internal image therefore has no complete calling-convention envelope and no execution authority.

The historical policy-1.4 raw encoder already contains working prologue and epilogue logic. Importing its helpers or copying its emitted spans as the new source of truth would preserve the dependency that this path exists to remove. Historical bytes may be compared in tests, but cannot own, encode, decode, or authorize this capsule.

Decision drivers

  • Own the entry, return, and Bounds machine bytes inside a new sovereign module that imports no raw/native/process/standalone helper.
  • Derive the ABI manifest, frame layout, entry homes, terminal labels, and entry successor only from verified target and ADR-0065 evidence.
  • Freeze every instruction and its symbolic ABI-state effect, including stack alignment, frame lifetime, caller MXCSR preservation, canonical MXCSR installation, hidden output-pointer custody, reserved-header initialization, input-lane materialization, output/status writes, and return.
  • Give the entry jump a concrete typed trap anchor inside the capsule while retaining its semantic target as ADR-0065’s exact entry successor.
  • Decode forward in a separately implemented module that imports no emitter helper and independently reconstructs instruction boundaries, operands, effects, rel32 destination, and totals.
  • Keep terminal replacement, native mapping, calling, process, ELF, timing, claim, and global policy authority closed. Encoder policy remains 1.4.0.

Considered options

Reuse historical raw prologue/epilogue helpers

Rejected. It would make the sovereign path depend on the legacy encoder and allow shared implementation defects to satisfy replay.

Replace ADR-0065 terminals while introducing the instruction grammar

Rejected. It would combine byte ownership, terminal substitution, whole-image relocation, and ABI proof in one decision.

Own a separate sealed ABI capsule with one typed entry-target anchor

Accepted for implementation. It isolates the new instruction vocabulary and lets a successor composition ADR copy exact accepted bytes and rewrite only the entry rel32 field.

Decision

Introduce X64TailAbiEnvelopeCapsule and a separately implemented x64_tail_abi_envelope_decode module.

Canonical capsule layout

The capsule contains exactly four owners in order:

  1. entry adapter;
  2. return epilogue;
  3. Bounds epilogue;
  4. one-byte typed entry-successor INT3 anchor.

The entry adapter uses the frozen Naux Lighthouse SysV1 convention. It creates the canonical aligned frame, saves the caller MXCSR, installs the canonical MXCSR, saves the hidden output pointer before any ABI register can be reused, zeroes the reserved header, materializes every typed input lane into its exact entry home, and jumps by checked rel32 to the typed anchor.

The return epilogue writes the two result words already produced in RAX and RDX, writes status zero, restores caller MXCSR, releases the exact frame, restores RBP, and returns. The Bounds epilogue writes two zero result words, writes status one, restores caller MXCSR, releases the same frame, restores RBP, and returns.

No shorter aliases, alternate addressing forms, optional prefixes, or host-selected encodings are admitted.

Symbolic ABI-state proof

Each decoded instruction owns one ordered symbolic effect. Independent replay starts from the frozen entry state and proves:

  • RSP mod 16 == 8 at call entry and the frame body sees canonical alignment;
  • the exact caller RBP, RSP, and MXCSR are restored on both exits;
  • the frame header owns offsets 0..32 exactly and all parameter writes remain inside verified canonical homes;
  • the hidden output pointer is captured before its register can be clobbered;
  • every entry lane appears exactly once in parameter/word order and no home word is missing or duplicated;
  • reserved header words are deterministically zero;
  • only return writes status zero and only Bounds writes status one;
  • the entry transfer resolves only to the typed anchor carrying ADR-0065’s exact semantic successor.

The state proof is structural. It does not assume that arbitrary output pointers are valid and does not execute the capsule.

Independent inverse proof

The decoder derives the expected ABI/frame/parameter manifest from the verified target and ADR-0065 image, consumes bytes forward, rejects noncanonical forms, and independently reconstructs all program ranges, instructions, effects, relocation evidence, anchor ownership, code hash, totals, and replay work. Exact comparison with capsule receipts happens only after decoding.

Authority boundary

The capsule is immutable data. It exposes no mapping, executable-memory, function-pointer, native runner, process, standalone, ELF, measurement, claim, or policy-selection API. RET bytes existing in a proof capsule do not grant authority to execute them.

Frozen limits

  • exactly three programs and one typed anchor;
  • at most five input lanes plus the hidden output-pointer lane, and 64 symbolic instructions/effects per program;
  • at most 4 KiB code and 1 MiB canonical evidence;
  • at most one relocation and 16,384 encoder/decoder/replay work units;
  • target frame and home limits remain those of verified R1-S7a;
  • every length, offset, displacement, reservation, and work charge uses checked arithmetic.

Limit exhaustion, noncanonical ABI/frame/header, missing or duplicate terminal owner, bad entry manifest, overlapping home, unknown instruction, alternate encoding, rel32 overflow, wrong anchor, state non-conservation, truncation, trailing byte, seal mismatch, or replay mismatch returns no capsule.

Consequences

  • NAUX gains a self-owned ABI instruction grammar without trusting the legacy raw encoder.
  • ADR-0065 remains unchanged and retains its three INT3 terminals.
  • A successor ADR can replace those terminals using exact ADR-0066 source spans and independently re-decode the fully enveloped image.
  • Capsule size and work are not native correctness, cycles, or performance evidence.

Acceptance gates

  1. BranchMix deterministically owns all three ABI programs and one typed anchor with exact instruction/effect/state replay.
  2. Public fixtures cover zero through five input lanes, Unit/scalar/F64Array homes, scalar/two-word returns, and Bounds behavior structurally.
  3. The independent decoder reconstructs every instruction, effect, program boundary, relocation, anchor, and total without emitter helpers or receipts.
  4. Every single-bit code mutation, truncation, trailing byte, and locally resealed program/instruction/effect/relocation/total/predecessor mutation fails closed.
  5. Historical raw bytes may match as redundant test evidence but are never a production dependency or authority input.
  6. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
  7. ADR-0065 code/hash and original target code/hash remain unchanged; no executable consumer exists and global encoder policy remains 1.4.0.

Accepted evidence

The exact BranchMix predecessor chain seals the capsule as:

  • capsule hash 7d059534c164396e3bf7175846c584ebfa7e8c651c77288450f2b7e62a064274;
  • code hash 5f83b79e74e85dc2d77eb30c0b6eacb63c100030feaf3a6107e0b50a7ba64bbb;
  • three programs, 30 canonical instructions, 30 ordered effects, three input lanes, one checked relocation, and one typed anchor;
  • 99 entry bytes, 37 return bytes, 42 Bounds bytes, and one anchor byte for exactly 179 owned code bytes;
  • 243 charged encode work units, 243 decode work units, and 36 symbolic replay work units.

The separately implemented decoder reconstructs the exact ABI manifest, program ranges, instruction/effect receipts, rel32 destination, typed anchor, code hash, totals, and state conservation. All 1,432 single-bit code mutations fail closed. Truncation, trailing bytes, and locally resealed program, instruction, effect, relocation, anchor, total, target-predecessor, image-predecessor, version, code, code-hash, and seal mutations also fail closed.

The public boundary covers zero through five input lanes, hidden-output-pointer placement through R9, Unit, Bool, I64, F64, F64Array, scalar and two-word return surfaces, and policy 1.4.0. Historical raw entry/exit bytes agree only as redundant cfg(test) evidence; production imports no raw/native/process/ standalone/measurement helper and no executable consumer exists.

Acceptance exposed and corrected one pre-existing manifest inconsistency: canonical home allocation reserves eight storage bytes for Unit while Unit contributes zero semantic tail/liveness words. ADR-0057 state-plan root 276ab1ed0ac7b692ed55275457db5a0356b0ca1e9ea1cd8fc33f30c5a21cf48a and its accepted evidence remain unchanged, and the corrected site-binding evidence replays.

The final exact-source workspace run exits zero: the core library discovers 397 tests (391 passed, 6 ignored), native-process correspondence passes 3/3, native parity passes 10/10, R1-S7a passes 9/9, and Gate A passes 3/3. Governance passes 22/22, refinement closed-loop passes 8/8, and workspace check, strict all-target Clippy, format, diff, and static authority gates pass. ADR-0065 image/code roots and the original target identities remain unchanged. These are byte-ownership and structural-replay facts, not execution, native-correctness, cycle, or performance evidence.

Correctness erratum — 2026-08-03

The ABI bytes remain byte-identical under code root 5f83b79e74e85dc2d77eb30c0b6eacb63c100030feaf3a6107e0b50a7ba64bbb, but the capsule binds the corrected entry-successor identity and therefore reseals under capsule root 6bdf9fd8d8221557728bb183877ebddbc954b4fa426393a1d98deddad51bf937. Its policy and exact 179-byte ABI vocabulary are unchanged. This dependency reseal is structural evidence only.