GitHub

ADR-0067: Fully enveloped non-executable semantic image composition

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

Context

ADR-0065 owns one closed internal semantic image, but represents its entry, return, and Bounds labels with typed one-byte INT3 terminals. ADR-0066 separately owns the canonical entry adapter and both epilogues, with an independently decoded ABI-state proof, but its entry jump resolves only to a typed INT3 successor anchor. Neither artifact is a complete code image.

The next step is exact composition, not execution. Composition changes the address of the return and Bounds labels, removes the three ADR-0065 terminal bytes, removes the ADR-0066 proof anchor, and retargets the ABI entry jump to the real ADR-0065 entry successor. Existing body/frontier/transition rel32 fields that address a moved terminal must therefore be recomputed. Treating this as byte concatenation would leave stale control flow.

Decision drivers

  • Compose only already verified ADR-0065 and ADR-0066 artifacts.
  • Preserve every non-relocation source byte exactly and identify every authorized four-byte rel32 rewrite.
  • Give every label and ABI program one unambiguous final image range.
  • Recover the complete image from bytes in a separate decoder without trusting emitter receipts, copied displacements, or the final seal.
  • Prove that projecting the final image back to each predecessor recovers its exact accepted bytes and independently decoded semantics.
  • Keep mapping, invocation, process, ELF, timing, claim, and global policy authority closed. Encoder policy remains 1.4.0.

Considered options

Append ADR-0066 unchanged after ADR-0065

Rejected. ADR-0065 control flow would still land on traps, while ADR-0066’s entry jump would still land on its proof anchor.

Replace only the three terminal bytes

Rejected. Variable-length replacements move two terminal labels, so any rel32 targeting them must be rebased and repatched.

Compose and immediately execute the image

Rejected. Whole-image byte/state correctness and finite native correctness are separate authority decisions.

Compose exact source spans under a new sealed inverse proof

Accepted for implementation. The new artifact owns no novel instruction grammar; it owns final placement, the complete relocation set, predecessor projection, and the whole-image identity.

Decision

Introduce X64TailEnvelopedImage and a separately implemented x64_tail_enveloped_image_decode module.

Canonical layout

The final byte order is exact and gap-free:

  1. ADR-0065’s body/frontier/transition prefix, ending immediately before its first typed terminal;
  2. ADR-0066’s exact entry-adapter span;
  3. ADR-0066’s exact return-epilogue span;
  4. ADR-0066’s exact Bounds-epilogue span.

The three ADR-0065 terminal bytes and ADR-0066 entry-successor anchor are not copied. All internal labels keep their original offsets. The entry, return, and Bounds labels move to their corresponding ABI program starts. The public image entry point is exactly the entry-adapter start.

Authorized byte changes

The composer first copies exact predecessor spans. It may then change only:

  • the four displacement bytes of every accepted ADR-0065 relocation, with the same source identity and semantic target but a target offset derived from the final layout; and
  • the four displacement bytes of ADR-0066’s entry jump, retargeted from the omitted proof anchor to ADR-0065’s exact entry successor in the final image.

Patch ranges must be unique, non-overlapping, contained in their owning source instruction, and use checked signed rel32 arithmetic. No opcode, prefix, ModRM/SIB, immediate, frame offset, or non-patch byte may change.

Whole-image inverse proof

The separate decoder derives all boundaries from the independently verified predecessor manifests. It consumes the final bytes forward, reconstructs source-span ownership, rebased labels, ABI program/instruction/effect ranges, all rel32 destinations, the entry point, CFG edges, totals, and the code hash.

For the ADR-0065 projection it restores every accepted predecessor displacement and the three typed terminal bytes, then requires exact byte and independent-decode agreement with ADR-0065. For the ADR-0066 projection it restores the accepted entry displacement, appends the typed successor anchor, then requires exact byte and independent-decode agreement with ADR-0066. These projections are decoder-owned checks; emitter receipts cannot satisfy them by construction.

Authority boundary

The artifact is immutable byte data. It exposes no executable-memory mapping, function pointer, call, native runner, process, standalone, ELF, measurement, claim, or policy-selection API. A complete RET-terminated image is not by itself authority to execute.

Frozen limits

  • exactly one internal prefix and three ABI program source spans;
  • exactly the accepted ADR-0065 relocation cardinality plus one entry relocation;
  • at most 128 MiB code/evidence and 64,000,000 compose/decode work units;
  • at most the accepted ADR-0065 program, label, frontier, CFG, and source-range limits plus the three ABI programs and instructions;
  • every length, offset, displacement, count, reservation, and work charge uses checked arithmetic.

Missing or duplicate terminal ownership, predecessor mismatch, source gap or overlap, unauthorized byte difference, overlapping patch, noncanonical rel32, wrong entry successor, stale label, projection mismatch, CFG mismatch, truncation, trailing byte, limit exhaustion, or seal mismatch returns no verified image.

Consequences

  • NAUX gains its first self-owned complete entry-to-return code image on the sovereign path without reusing the historical raw encoder.
  • ADR-0065 and ADR-0066 remain immutable accepted predecessors.
  • A later ADR may consider finite native correctness for this exact identity; it cannot silently inherit historical execution authority.
  • Image bytes, byte count, and composition work are structural evidence, not cycles or performance evidence.

Acceptance gates

  1. BranchMix deterministically composes the exact accepted ADR-0065 and ADR-0066 identities into one gap-free image with exact entry/return/Bounds ranges and one public entry point.
  2. Independent decode recovers every source span, label, ABI instruction and effect, relocation, CFG edge, total, code hash, and both exact predecessor projections without emitter helpers or receipts.
  3. Only accepted rel32 patch windows differ from predecessor source bytes; every semantic target resolves to its final typed destination.
  4. Every single-bit code mutation, truncation, trailing byte, and locally resealed source/range/label/instruction/effect/relocation/CFG/total/ predecessor/code-hash/seal mutation fails closed.
  5. Public evidence proves the entry point, exact source coverage, terminal replacement, target-policy immutability, and absence of any executable consumer.
  6. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
  7. ADR-0065, ADR-0066, original target identities, and global encoder policy 1.4.0 remain unchanged; no native-correctness or performance claim is admitted.

Accepted evidence

The exact BranchMix predecessor chain seals the fully enveloped image as:

  • image hash 7341fe29c1474843e11cbd33dd49db059b30e30d4bf7a9e441e4438cd860d9bd;
  • code hash 966e116302dfd1bb1c2ef01032f36a1b994df4696792e41f55d224540c7d1ae9;
  • 7,079 exact internal-prefix bytes followed by 99 entry, 37 return, and 42 Bounds bytes, for one gap-free 7,257-byte image;
  • 310 closed programs, three ABI programs, 142 labels, 146 frontiers, 713 closed source ranges, four composition source spans, 30 ABI instructions and effects, 181 exact rel32 relocations, and 191 CFG edges;
  • entry point 7,079, exactly the replacement EntryAdapter label;
  • 8,728 compose work units, 8,728 independent decode work units, and 7,985 predecessor-projection work units.

The independent decoder validates every final displacement directly from the input bytes. It restores only the accepted patch windows and reconstructs the exact byte-identical ADR-0065 image, including its three typed terminals. It also reconstructs the exact byte-identical ADR-0066 capsule, including its typed successor anchor, and reruns the separately implemented ABI instruction and symbolic-state decoder on that projection.

All 58,056 single-bit code mutations fail closed. Truncation, trailing bytes, and locally resealed source-span, closed-program, label, frontier, closed-source, ABI-program, ABI-instruction/effect, relocation, CFG, entry, total, predecessor, version, code, code-hash, and seal mutations also fail closed. Public evidence covers zero through five input lanes, exact source coverage, terminal replacement, every rel32 destination, and policy 1.4.0.

The final exact-source workspace run exits zero. The core library discovers 399 tests (393 passed, 6 ignored); native-process correspondence passes 3/3, native parity 10/10, R1-S7a 9/9, Gate A 3/3, and the ADR-0067 public boundary 1/1. 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 2026967538a407340d92a8885d5d45c1afd82a1975fcaba2266340e0c55dcc4e / 5b6097a3e9816c0e9caf639409f22bdd8daf4f03f48b66ed05cdd84f1a0082c8 and ADR-0066 capsule/code roots 7d059534c164396e3bf7175846c584ebfa7e8c651c77288450f2b7e62a064274 / 5f83b79e74e85dc2d77eb30c0b6eacb63c100030feaf3a6107e0b50a7ba64bbb remain unchanged. Production imports no raw/native/process/standalone/ measurement helper, no executable consumer exists, and encoder policy remains 1.4.0. These are complete-image ownership and structural-replay facts, not native-correctness, cycle, or performance evidence.

Correctness erratum — 2026-08-03

The corrected predecessor vector composes under image/code roots 51f5498479257a50798e5c43ee0b46d9a656bff80a760701ab1fbccd535b31a8 / b363c66803c90b7cfe9d760df39e9051a0f93fd65a1857870ebfb72717866998. Independent replay recovers 319 closed and three ABI programs, 142 labels, 151 frontiers, 746 closed source ranges, four composition spans, 192 relocations and 209 CFG edges. The exact gap-free image has a 7,272-byte closed prefix plus 99/37/42 entry/return/Bounds bytes, 7,450 bytes total, with entry point 7,272. These complete-image structural facts supersede the prior root vector; they do not establish runtime performance.