GitHub

ADR-0065: Closed non-executable semantic image composition

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

Context

ADR-0060 owns and independently decodes the persistent tail-transition byte capsule. ADR-0064 separately owns and independently decodes every admitted body/frontier byte while retaining each transition as an exact ADR-0060 reference. Both capsules deliberately resolve control transfers to typed trap anchors rather than to one another.

The next trust boundary must prove that those two accepted byte owners can be placed into one deterministic address space, that every rel32 can be relocated to its real semantic destination, and that the resulting control-flow graph is recoverable without trusting the composer. The accepted predecessors do not yet own an ABI entry prologue, return epilogue, or Bounds epilogue. Calling the result an executable whole image would therefore be false.

Decision drivers

  • Compose only bytes already owned by ADR-0060 and ADR-0064; introduce no new executable instruction vocabulary.
  • Give every retained source byte exactly one typed owner and reject gaps, overlap, duplication, or orphan bytes.
  • Place every block, site, operational frontier, and persistent transition in one canonical bounded layout.
  • Relocate every accepted rel32 with checked signed arithmetic to one exact block, frontier, or typed terminal boundary.
  • Keep entry ABI, return, and Bounds as explicit INT3 terminal anchors until successor ADRs own their real byte sequences.
  • Recover layout, byte provenance, relocation, and the full internal CFG in a separate decoder that imports no composer helper and trusts no composer receipt.
  • Keep native mapping, calling, process, ELF, timing, claim, and encoder-policy authority closed. Global encoder policy remains 1.4.0.

Considered options

Reuse the existing raw policy-1.4 image

Rejected. It would bypass the newly proven persistent-register representation and make historical raw/native authority the source of truth for this path.

Add real prologue and epilogues in the same change

Rejected. That would mix composition proof with a new ABI instruction grammar and prematurely open execution authority.

Trust ADR-0060/0064 receipts while patching their bytes

Rejected. Predecessor receipts are useful redundant evidence, but the new decoder must derive placement and parse both accepted grammars independently.

Compose one closed semantic image with typed terminal anchors

Accepted. It proves the complete internal body CFG and makes the remaining ABI envelope explicit rather than hiding it.

Decision

Introduce X64TailClosedImage and a separately implemented x64_tail_closed_image_decode module.

Canonical layout

Target blocks retain canonical target function/block order. For each block:

  1. operational BeforeLabel frontiers are placed in frontier ordinal order;
  2. the block label is marked;
  3. all site programs for that block are placed in site ordinal order, with every CapsuleTransition expanded from its exact ADR-0060 source span;
  4. operational ExitStub frontiers owned by that source block follow by fallthrough.

Operational EdgeStub and CheckedExit frontiers then form an ordinal stub pool. Three typed one-byte terminal anchors follow in canonical owner order: entry adapter, return epilogue, and Bounds epilogue. No-op, capsule-reference, and evidence-alias frontier rows remain explicit zero-byte aliases; they cannot silently acquire ownership.

The external entry boundary records one semantic successor: the operational entry frontier when present, otherwise the entry block label. The entry anchor itself is a proof terminal and is not executable startup code.

Byte provenance and relocation

Every non-transition atom copies its exact ADR-0064 program bytes. Every transition atom copies its exact ADR-0060 transition span. Only the four-byte rel32 fields may differ from their source capsules. For each copied range the image records source capsule, source program/edge, source interval, image interval, and relocated patch ownership.

All copied non-patch bytes must remain byte-identical. Relocations are resolved only to canonical block offsets, operational frontier offsets, or typed terminal anchors. A frontier target that denotes a zero-byte or aliased row is invalid unless its disposition canonically resolves to an admitted owner.

Independent inverse proof

The decoder derives the layout from the verified target and ADR-0062 realization, not from image receipts. It independently decodes the ADR-0060 and ADR-0064 predecessor bytes, consumes the composed image forward, proves every non-patch byte against its unique source owner, and reconstructs every rel32 destination.

It then rebuilds block/site/frontier ranges, source-byte ownership, relocation receipts, entry successor, terminal anchors, fallthrough edges, conditional edges, unconditional edges, and terminal edges. Exact replay compares this independent result with the sealed image envelope only after decoding.

Authority boundary

The image is immutable data. It has no mapping, executable-memory, function pointer, native runner, process, standalone, ELF, measurement, claim, or policy selection API. Reaching a terminal INT3 is proof of an unfinished ABI boundary, not target semantics.

Frozen limits

  • at most 1,000,000 sites, 32,000 frontiers, and 2,032,000 labels/anchors;
  • at most 8,000,000 atoms and 2,004,096 relocations;
  • at most 128 MiB image bytes and 128 MiB canonical evidence;
  • at most 64,000,000 composer and 64,000,000 decoder work units;
  • every extent, offset, displacement, count, reservation, and work charge uses checked arithmetic.

Limit exhaustion, unsupported frontier placement, missing/duplicate ownership, bad predecessor span, source-byte mismatch, rel32 overflow, unknown target, CFG escape, gap, overlap, orphan byte, truncation, trailing byte, seal mismatch, or replay mismatch returns no image.

Consequences

  • NAUX gains one finite address space for all accepted body, frontier, and persistent-transition bytes.
  • The remaining distance to executable authority is made exact: the ABI entry, return, and Bounds terminal envelopes still need sovereign bytes and proof.
  • Image size and construction work are structural evidence, not runtime speed or a Gate B claim.
  • A successor ADR may own the three ABI envelope templates, then seek finite native correctness without changing policy merely because bytes exist.

Acceptance gates

  1. BranchMix composes every admitted ADR-0064 atom and all referenced ADR-0060 transitions exactly once with zero non-patch byte drift.
  2. Independent decode recovers every block/site/frontier range, source owner, relocation, terminal anchor, and full internal CFG without composer helpers or receipts.
  3. Every CFG edge resolves to an exact instruction boundary, operational frontier, block label, or typed terminal; no byte is unowned or multiply owned.
  4. Exhaustive single-bit mutation, truncation, trailing byte, and locally resealed provenance/layout/relocation/CFG/total/predecessor mutations fail closed.
  5. A public finite cyclic-tail fixture passes without changing original target code/hash and exposes no executable API.
  6. Focused, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
  7. No raw/native/process/standalone/measurement consumer exists and global encoder policy remains exactly 1.4.0.

Accepted evidence

The exact BranchMix predecessor chain is accepted under image root 2026967538a407340d92a8885d5d45c1afd82a1975fcaba2266340e0c55dcc4e and code root 5b6097a3e9816c0e9caf639409f22bdd8daf4f03f48b66ed05cdd84f1a0082c8. The canonical image contains 310 programs, 142 block labels, 146 operational frontiers, three typed ABI terminals, 713 source ranges, 180 relocations, and 191 independently reconstructed CFG edges. Of the source ranges, 605 own ADR-0064 body/frontier bytes and 108 own exact ADR-0060 transition spans.

The image contains exactly 4,944 body/frontier bytes, 2,135 transition bytes, and three terminal bytes, for 7,082 uniquely owned bytes. Composer and decoder each charge 7,795 work units. Every relocation patch is contained by one exact typed source atom, and every CFG destination independently resolves to a block label, operational frontier, or exact program instruction boundary. The original target bytes and code hash remain unchanged.

Exhaustively flipping each of eight bits at every image position produces 56,656 rejected independent decodes. Truncation, trailing bytes, and locally resealed program, label, frontier, terminal, source, relocation, CFG, total, predecessor, code-hash, and image-seal mutations fail closed. The public finite cyclic-tail fixture also passes without acquiring execution authority.

The full workspace/all-target suite passes. The core library discovers 395 tests: 389 pass and six explicitly expensive release-only tests remain ignored. Process isolation passes 3/3, native parity 10/10, S7a 9/9, and Gate A 3/3. Governance is 22/22 and strict refinement is 8/8. Workspace check, strict Clippy, formatting, diff hygiene, and static authority scans are clean. The production composer/decoder has no raw, native, process, standalone, measurement, mapping, ELF, or execution consumer; the sole native-lighthouse reference is test-only. Global encoder policy remains exactly 1.4.0.

These roots and counts prove deterministic composition, ownership, relocation, and independent replay. They are not native-correctness or performance evidence. The three INT3 terminals keep entry, return, and Bounds ABI authority explicitly closed for a successor decision.

Correctness erratum — 2026-08-03

The corrected predecessor chain reseals policy 1.1.0 under image/code roots 44d504cddf12cc7f9766f3f33b90968cca9b1fb46f65aaa2d8aa02c1e1e960aa / c0b7aa0d92401e9b98e26adc4aa28d3d8f52dc29695820aa895ce53d9e09abd5. It owns 319 programs, 142 labels, 151 frontiers, 746 source ranges, 638 body ranges, 108 transition ranges, 191 relocations and 209 CFG edges. The exact image contains 5,169 body, 2,103 transition and three terminal bytes: 7,275 bytes total. Prior roots are preserved only as superseded audit history.