ADR-0062: Bounded symbolic body/frontier realization

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

Implementation note: independent token replay exposed the region-wide adapter defect documented by ADR-0063. The accepted artifact consumes only ADR-0063’s corrected schema-1.1.0 frontier proof; the superseded schema-1.0.0 proof grants it no authority.

Context

ADR-0061 proves that every admitted persistent-region body site has an exact typed physical binding. ADR-0063’s schema-1.1.0 correction binds every ingress, egress, checked side exit, and tail boundary to its exact live-set state obligation. They deliberately emit no instruction intent. Consequently, the corrected proof does not yet establish that an x86-64 template can consume those bindings, preserve every unrelated live token, define the right result, and discharge each flush/hydration obligation in the required order.

ADR-0060 owns bytes only for the already proven persistent tail transitions. Those slices cannot be composed with the current frame-based body templates. Whole-image work therefore remains unsound until the complete body and frontier state machine exists at a non-byte boundary.

Decision drivers

• Consume only the exact verified ADR-0061 predecessor chain regenerated under ADR-0063 schema 1.1.0.
• Admit only regions whose corrected site-binding status is Ready.
• Lower every admitted instruction/control site exactly once into a closed, typed symbolic x86-64 vocabulary.
• Represent entry, branch stubs, checked Bounds exits, materialized tails, shared joins, Return, and budget barriers as explicit ordered adapter programs rather than implicit frame/register assumptions.
• Reference ADR-0060 persistent transitions by exact edge and capsule span; do not copy, decode, patch, or select their bytes.
• Prove local live-token preservation and whole-CFG state continuity with an independent symbolic machine.
• Freeze exact prospective lengths, clobbers, and rel32 intent without granting byte, layout, native, process, timing, or selection authority.

Considered options

Encode body bytes immediately

Rejected. A decoder can validate instruction shape after encoding, but it cannot repair a missing state-transfer or incorrect scratch schedule chosen before encoding.

Reuse policy-1.4 raw templates as the proof source

Rejected. Those templates are frame-based and would make the new proof dependent on the authority it is intended to replace. ADR-0062 owns a small symbolic vocabulary and imports no raw/native/process path.

Treat every ADR-0061 frontier row as an independent emitted block

Rejected. Declared frontiers can overlap concrete CFG edges or checked exits. The realizer must assign one canonical operational owner and retain duplicate rows only as evidence aliases, preventing double hydration or double counting.

Emit and replay a sealed symbolic realization

Accepted. Byte encoding remains a later independently authorized boundary.

Decision

Introduce X64TailBodyFrontierRealization, sealed to the exact target, ADR-0057 logical plan, ADR-0058 physical allocation, ADR-0059 transition realization, ADR-0060 capsule, and ADR-0063-corrected site-binding proof.

Closed symbolic vocabulary

The vocabulary contains only typed operations needed by the accepted target:

acquire immediate/frame/persistent GPR or XMM word into a fixed scratch
define one logical word from a fixed scratch into frame/persistent storage
I64 add/sub/mul, signed compare/setcc, F64 add/sub
boolean test, signed-negative and unsigned-upper-bound checks
checked F64 element load
frame↔persistent adapter transfer
logical frame parallel-copy scratch save/move
rel32 branch/jump intent
exact ADR-0060 transition reference

Every atom records ordinal, prospective start/end, typed operands, exact definitions, ordered clobbers, and any retained fixup. Lengths are exact for the frozen instruction shape but remain prospective until a later owned byte encoder reproduces them.

Site programs

Each corrected site is regenerated from the source target operation and its ordered bound reads/definitions. Loads use only the frozen scratch bank RAX/RCX/RDX and XMM0/XMM1; computation atoms define an explicit logical result token; stores move that token to the corrected physical definition. Array checks target the exact operational Bounds frontier so flushes occur only on the exceptional path. Branches target either the target label directly for a preserving edge or its exact adapter stub. Persistent tails reference the exact ADR-0060 receipt. Refused tails and unsupported destructive aliases fail closed.

Frontier programs and ownership

Operational frontier programs have one of these placements:

before-label   entry/shared-join/budget hydration barriers
edge-stub      branch and materialized-tail adapters
checked-exit   Bounds flush before the Bounds epilogue
exit-stub      Return flush before observation
capsule-ref    persistent transition already owned by ADR-0060
evidence-alias duplicate declared row covered by an operational owner

FlushThenHydrate always stores the complete source adapter in canonical logical order before loading the complete target adapter. A materialized tail performs source flush, the ADR-0057 logical parallel-copy schedule over frame homes, target hydration, then control transfer. Each row is consumed exactly once as an owner or a sealed alias.

Independent symbolic replay

The verifier rebuilds the target/site/frontier lookup independently and runs a typed token machine over every declared atom. At each site it seeds the exact corrected live-before mapping, verifies each scratch read before use, applies the source operation, checks every definition, and requires the exact live-after mapping at exit. Adapter replay proves frame/register token correspondence and strict flush-before-hydrate ordering. Persistent transition references must match one unique ADR-0060 receipt and logical edge.

The verifier also reconstructs block order and CFG links. Adjacent site states, ordinary branch edges, adapter continuations, and tail destinations must agree on every live logical word. No declared receipt, prospective length, clobber list, fixup, frontier owner, total, or seal is trusted.

Frozen limits

• at most 1,000,000 site programs and 32,000 frontier programs;
• at most 8,000,000 symbolic atoms and 2,000,000 retained fixups;
• at most 64 words per adapter and 16,384 logical tail-copy steps;
• at most 64 atoms per site and 512 atoms per frontier;
• at most 64 MiB canonical evidence;
• at most 32,000,000 symbolic replay work units;
• every prospective x86-64 instruction is at most 15 bytes;
• all counts, cursors, lengths, and work charges use checked arithmetic.

Limit exhaustion, unknown template shape, missing frontier owner, ambiguous aliasing, unsupported tail disposition, or token mismatch returns no artifact.

Consequences

• ADR-0062 is the first artifact that proves the body, adapters, and retained tail transitions form one symbolic state machine.
• It still owns no new machine byte and cannot enter executable selection.
• Exact symbolic length is not whole-image size because label placement, alignment, concrete rel32 displacement, and byte ownership remain closed.
• A successor ADR may encode only the accepted body/frontier vocabulary and must use a separately implemented decoder.
• Whole-image composition, relocation, W^X/native correctness, process isolation, standalone packaging, measurement, claims, and global policy selection remain separate gates. Encoder policy stays 1.4.0.

Acceptance gates

1. BranchMix deterministically realizes every ready corrected site and consumes every frontier row exactly once as an operational owner or evidence alias.
2. Bounds exits flush only on the exceptional path and target the exact Bounds epilogue intent.
3. All persistent tails bind one-to-one to exact ADR-0060 receipt spans; materialized tails replay the exact ADR-0057 frame schedule.
4. Independent token replay covers all site atoms, adapters, CFG links, and tail destinations with no uninitialized scratch read or live-token loss.
5. Targeted unsupported, alias, missing-owner, bad-order, stale predecessor, atom/fixup/length/clobber/total, and seal mutations fail closed.
6. Bounds and the public finite cyclic-tail fixture pass without changing the original target bytes/hash.
7. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
8. 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 realization root 97358e4b859ef31d92eebe4b71282adf85190c785bc00f55859d4a80a8325552. It realizes all 164 body/control sites and 146 frontier programs: 38 operational adapters and 108 exact ADR-0060 capsule references, with zero no-op, evidence-alias, or refused programs. Independent replay covers 713 symbolic atoms, 180 fixup intents, 209 flushes, 189 hydrations, 39 materialized-tail steps, and 1,023 charged work units.

The frozen prospective layout accounts for 2,988 body bytes and 4,091 frontier bytes. The body total includes all 2,135 already-owned ADR-0060 transition bytes; neither total is a whole image, newly executable code, or a performance claim. Atom layout, clobber, fixup, frontier order, source hash, total, and seal mutations fail closed. The public finite cyclic-tail fixture passes, and the original target code and hash remain unchanged.

The full workspace/all-target suite passes. The core library discovers 390 tests: 384 pass and six explicitly expensive release-only tests remain ignored. Process isolation, native parity, S7a, and Gate A pass. Governance is 22/22 and strict refinement is 8/8. Strict Clippy, formatting, diff hygiene, and static authority scans are clean. 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 carries byte-storage aliasing and live-scratch reservation into the independent body/frontier token machine. The superseding realization root is 93e281cba92c985043dc2401167f4a051eb9a6f322bda032362846ec0250ffff: 168 site programs, 151 frontier programs, 43 operational adapters, 108 capsule frontiers, 746 atoms, 191 fixups, 207 flushes, 189 hydrations and 41 materialized-tail steps. Its 3,073 body and 4,199 frontier prospective-byte facts are structural bounds, not execution or performance measurements.