ADR-0064: Owned non-executable body/frontier byte capsule

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

Context

ADR-0062 accepts one bounded typed-token realization for every ready body site and concrete frontier obligation. It freezes exact x86-64 instruction shapes, prospective lengths, clobbers, fixup intents, adapter order, and references to the already-owned ADR-0060 transition capsule, but deliberately owns no new machine byte.

The next boundary must prove that the closed symbolic vocabulary has one canonical byte representation. Encoding it directly into a whole image would prematurely combine program placement, CFG composition, transition ownership, relocation, and execution authority. Trusting encoder receipts would also make the encoder its own verifier.

ADR-0060 already owns 2,135 transition bytes. Copying them into another capsule would create ambiguous byte ownership and two sources of truth.

Decision drivers

• Own exactly the new body/frontier bytes admitted by ADR-0062.
• Retain every CapsuleTransition as an exact external ADR-0060 reference; never copy or re-encode its bytes.
• Give every symbolic atom one canonical x86-64/SSE2 representation with no shorter alias, alternate prefix, or host-dependent encoding.
• Resolve every new rel32 only against a typed trap anchor, never a real target block or executable address.
• Decode forward with a separately implemented parser that shares no opcode emission helper and does not trust receipts.
• Recover exact instruction boundaries, registers, frame displacements, immediates, compound-atom ordering, branch targets, clobbers, and fixups.
• Bind code, predecessor identities, receipts, totals, and limits into domain-separated seals.
• Keep whole-image, native, process, standalone, timing, claim, and policy authority closed. Global encoder policy remains 1.4.0.

Considered options

Compose a complete candidate image now

Rejected. It would collapse byte ownership, program layout, CFG recovery, and native correctness into one unauditable authority jump.

Reuse policy-1.4 raw encoder helpers

Rejected. The new path must own its grammar and remain statically independent from raw/native/process/standalone/measurement code.

Copy ADR-0060 transition bytes into every tail site

Rejected. Those bytes already have an owner and independent decoder. The new capsule records exact source spans and the predecessor capsule hash instead.

Serialize symbolic atoms instead of machine instructions

Rejected. ADR-0062 already owns symbolic evidence. This boundary exists to prove a canonical machine-byte representation.

Encode isolated program slices with typed trap anchors

Accepted. Site slices precede frontier slices in canonical ordinal order. All control targets resolve to one canonical typed INT3 anchor table appended after the slices. The anchors are proof objects and cannot perform target semantics.

Decision

Introduce X64TailBodyFrontierCapsule and a separate x64_tail_body_frontier_decode module.

Byte ownership

The capsule owns only bytes emitted for non-CapsuleTransition atoms. Every site and frontier receives a canonical program receipt containing its typed kind, ordinal, byte range, encoded atom count, and external-reference count. Zero-byte no-op and capsule-reference programs remain present in the receipt stream, so coverage cannot disappear through omission.

Each external reference binds site ordinal, atom ordinal, edge ordinal, ADR-0060 start/end, and retained length. Its source capsule hash is sealed in the envelope. No referenced byte appears in the new code vector.

Closed canonical grammar

The encoder admits only the exact ADR-0062 vocabulary:

movabs and typed GPR/XMM acquire/define forms
wrapping add/sub/imul and signed cmp/setcc normalization
SSE2 addsd/subsd
test plus canonical rel32 conditional/unconditional branches
ordered Bounds negative/upper checks and checked F64 element load
typed frame↔persistent flush/hydrate
typed frame scratch save and materialized parallel-copy moves
external ADR-0060 transition reference with zero new bytes

Frame access always uses [rsp+disp32]. F64 immediates enter XMM scratch via movabs rax then movq; materialized F64 immediate-to-frame moves store the exact bits through GPR scratch. Every symbolic atom emits exactly its frozen prospective length except CapsuleTransition, which emits zero bytes and one external reference.

Typed proof anchors and fixups

The encoder collects unique (Label, id) and (Frontier, ordinal) targets from non-external fixups, orders them by typed key, and appends one 0xcc byte per target. Every rel32 is resolved with checked signed arithmetic to exactly one anchor. Anchors are not labels in a whole-image CFG and grant no execution authority.

Independent decoding

The decoder derives program ranges and external references from the verified ADR-0062 realization, not capsule receipts. It parses machine bytes forward, rejects unknown/redundant prefixes and noncanonical register or addressing forms, reconstructs primitive machine instructions, groups them by exact symbolic atom boundary, and binds each group to the expected typed atom.

It independently derives the typed anchor table, resolves every rel32, and reconstructs clobbers and fixup receipts. Only after decoding does the capsule verifier compare decoded receipts, external references, totals, code hash, and the complete canonical regeneration.

Frozen limits

• at most 1,000,000 site and 32,000 frontier programs;
• at most 8,000,000 encoded atoms and 2,000,000 resolved fixups;
• at most 4,096 external ADR-0060 transition references;
• at most 2,032,000 typed proof anchors;
• at most 64 MiB owned code and 64 MiB canonical evidence;
• at most 32,000,000 encoder and 32,000,000 decoder work units;
• at most 18 owned bytes per symbolic atom and 15 bytes per primitive x86-64 instruction;
• all lengths, displacements, counts, reservations, and work charges use checked arithmetic.

Limit exhaustion, unknown symbolic form, missing/duplicate program ownership, bad external span, rel32 overflow, noncanonical byte, truncation, trailing byte, receipt mismatch, or replay mismatch returns no capsule.

Consequences

• NAUX gains independent evidence that every accepted body/frontier intent has one owned canonical byte representation.
• ADR-0060 remains the sole owner of persistent transition bytes.
• Program slices and trap anchors are deliberately not executable semantics.
• Owned byte count is not whole-image size, runtime performance, or policy selection evidence.
• A successor ADR may compose the two accepted byte owners into one finite non-executable whole-image candidate with independent full-CFG recovery.

Acceptance gates

1. BranchMix deterministically covers all 164 sites and 146 frontiers, with every ADR-0062 atom encoded or retained exactly once.
2. Every machine family has locked positive vectors and rejects alternate, malformed, truncated, and trailing encodings.
3. The decoder reconstructs program boundaries, typed anchors, clobbers, fixups, external references, and exact ADR-0062 atom bindings without consulting encoder receipts.
4. Every single-bit mutation in the owned code fails closed; locally resealed program, fixup, reference, total, predecessor, code-hash, and capsule-seal mutations fail closed.
5. Bounds and the public finite cyclic-tail fixture pass without changing the original target bytes/hash.
6. Focused, public-boundary, 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 capsule root 0d9d856a4486a74a61560a8c7dff39d1a02da6b653eef62c860a8e0722e59010 and owned-code root 1b582e7645397c0bdeafcfdaa47144558ff3227aceb3d503c119b0a77d400085. All 164 sites and 146 frontiers remain present as 310 canonical program receipts. Of ADR-0062’s 713 atoms, 605 encode into 662 primitive instructions and 108 become exact external ADR-0060 references. No transition byte is copied.

The capsule owns 853 site bytes and 4,091 frontier bytes. Sixty-five typed trap anchors make 72 new rel32 fixups concrete, producing exactly 5,009 owned capsule bytes. The external references retain all 2,135 ADR-0060 transition bytes under their original owner. Encoder and decoder each charge 5,722 work units. These counts are proof-capsule structure, not whole-image size, cycles, or a performance claim.

Locked vectors cover every admitted machine family. Exhaustively flipping each of eight bits at every one of the 5,009 byte positions produces 40,072 rejected decodes. Truncation, trailing bytes, and locally resealed program, anchor, fixup, external-reference, total, predecessor, code-hash, and seal mutations fail closed. The public finite cyclic-tail fixture passes and the original target code/hash remain unchanged.

The full workspace/all-target suite passes. The core library discovers 393 tests: 387 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. Strict Clippy, formatting, diff hygiene, and static authority scans are clean. The decoder contains no emitter helper; no raw/native/process/standalone/measurement consumer exists, and global encoder policy remains 1.4.0.

Correctness erratum — 2026-08-03

Policy 1.2.0 reserves live scratch registers in the concrete body/frontier encoder and requires the independent decoder to recover the same clobbers. The superseding capsule/code roots are 64f470d5b7a7d1536c2100f104e606fb5a9313b8c21685ee08a333c273d1364a / 80de9349e0abd8604147ca1b8b3495eaa9139c58840d19eba541461e40a44c13. The exact artifact has 319 programs, 638 atoms, 703 primitive instructions, 108 external references, 71 typed anchors, 83 resolved fixups, 970 site bytes, 4,199 frontier bytes, 71 anchor bytes and 5,240 owned bytes. These are byte ownership facts, not native-performance evidence.