ADR-0061: Bounded persistent-site binding and frontier-state proof

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

Supersession note

This ADR remains accepted as the historical schema-1.0.0 whole-body binding and CFG-liveness proof. Its region-wide frontier-adapter construction is unsound when two non-interfering logical words reuse one physical register; ADR-0063 supersedes that construction with schema 1.1.0 exact live-set narrowing. The root and frontier totals below are retained for audit history only and may not feed ADR-0062, a byte encoder, or any later authority.

Context

ADR-0057 selects persistent tail regions, ADR-0058 maps tail-live logical words to a finite GPR/XMM/frame bank, ADR-0059 proves the surrounding policy-1.4 template clobbers preserve that bank, and ADR-0060 owns/decodes bytes for the persistent tail transitions.

That chain is not yet sufficient for a whole image. Policy-1.4 block bodies still read operands and write results through canonical frame homes. If only the tail-transfer bytes were replaced, a successor block could receive a word in a persistent register and then read the stale frame slot. Conversely, a body result written only to a frame slot would leave the persistent register stale for the next transition.

ADR-0058 also builds interference from tail-edge snapshots. Two logical words that never coexist at a tail may still be simultaneous operands inside a body instruction or live across a branch. Assuming the tail-only graph is enough would turn an allocation heuristic into unproved semantics.

Finally, entry, shared join, Bounds, Return, budget, materialized-tail, and cross-region control edges require explicit frame↔persistent state adapters. Neither a clobber census nor a tail capsule defines those adapters.

Decision drivers

• No ADR-0060 byte may enter a whole image until every body use/definition is bound to an exact typed physical location.
• Whole-body liveness must be derived from the verified target CFG, not from tail receipts or occurrence counts.
• Distinct simultaneously live logical words may not alias one physical location unless a later explicit destructive-template proof admits it.
• Every control ingress and egress must be classified as a persistent transition or an explicit hydration/flush frontier obligation.
• Cross-region branches, mixed persistent/materialized predecessors, checked side exits, entry, return, and budget boundaries must fail closed rather than inherit implicit register state.
• The analysis must be finite, deterministic, sealed, and independently replayable without emitting or decoding new machine bytes.

Considered options

Splice ADR-0060 transitions into policy 1.4 now

Rejected. The target bodies retain frame semantics, so transition registers would not be the operands those bodies consume.

Treat ADR-0059 preservation as body adaptation

Rejected. “Does not clobber a register” is weaker than “reads and defines the logical value in that register.”

Assume tail-edge interference covers instruction sites

Rejected. Body operands, results, and branch-live values can coexist even when they never coexist in one tail snapshot.

Emit a bounded site/frontier readiness proof first

Accepted. The artifact exposes exactly where the accepted allocation is sufficient, where adapters are required, and where a region must be refused before any body encoding is attempted.

Decision

Introduce a sealed X64TailSiteBindingProof bound to the exact verified target, ADR-0057 logical plan, ADR-0058 allocation, ADR-0059 realization, and ADR-0060 capsule.

Typed physical binding

For every target block whose label belongs to an allocated persistent region, expand each scalar home to one typed word and each F64-array home to ordered ArrayData/ArrayLength words. Each word is bound through the region’s exact ADR-0058 mapping; a word outside that mapping remains at its canonical typed frame location. Immediate operands remain exact typed values.

Each site receipt records the source function/block/label/position, operation kind, ordered bound reads, ordered bound definitions, template clobbers, and the exact logical live-before/live-after sets from which alias safety is derived. Receipts are evidence, not authority for a later encoder.

CFG liveness and interference refinement

The analyzer constructs the complete label/block CFG from the verified target and computes a deterministic backward least fixed point using explicit work and iteration caps. Branch successors contribute their live-in sets. Return has no successor state. Tail terminators consume their explicit ordered arguments; inter-function state transfer remains owned by the edge/frontier classification rather than ordinary fallthrough liveness.

At every instruction/control boundary:

1. every typed logical read must contain its symbolic token in the bound physical location;
2. distinct live logical words must map injectively;
3. a definition may reuse a source location only when the source is dead after the site and the receipt marks the reuse as requiring a later explicit destructive-template proof;
4. no other live-out token may be destroyed by the definition;
5. ADR-0059’s non-intentional clobbers remain disjoint from all live physical persistent registers;
6. any failure refuses the complete region, never an individual site in isolation.

The initial policy is conservative: an unproved destructive reuse is recorded but does not become byte-encoding authority.

Frontier-state obligations

Every incoming/outgoing control edge touching a persistent region is classified exactly once:

accepted same-region persistent tail  -> bind ADR-0060 transition
entry or non-persistent ingress        -> hydrate mapped words from frame
materialized/cross-region egress       -> flush mapped words to frame
shared join or mixed predecessor       -> flush/hydrate boundary
Bounds/Return/budget side boundary     -> flush before observable exit
same-region ordinary branch            -> preserve one identical mapping
cross-region ordinary branch           -> explicit flush/hydrate obligation

Hydration and flush rows contain exact typed frame/register pairs in canonical order. ADR-0061 does not lower them to instructions. A label with ambiguous or unclassified ingress/egress refuses its region.

Independent replay

The verifier independently rebuilds target CFG successors/predecessors, region ownership, typed word expansion, liveness fixed point, physical bindings, alias checks, clobber checks, frontier classification, totals, and the complete artifact. It does not trust declared site/frontier receipts and does not call any raw encoder, ADR-0060 encoder helper, native runner, process, or external solver.

Frozen limits

• at most 4,096 persistent regions;
• at most 1,000,000 body/control sites;
• at most 8,000,000 bound words across site rows;
• at most 2,000,000 CFG edges;
• at most 4,096 liveness fixed-point rounds;
• at most 64 mapped words per region and 64 words per frontier row;
• at most 32,000 frontier rows;
• at most 16,000,000 analysis-work units;
• at most 64 MiB canonical evidence.

All counts, set growth, offsets, and work charges use checked arithmetic. Limit exhaustion returns no proof artifact.

Consequences

• A tail-only whole-image splice is normatively forbidden.
• The accepted allocation may be narrowed by evidence if whole-body liveness reveals interference absent from ADR-0058’s tail snapshots.
• The result is a precise input to a later symbolic body/frontier realization, not itself an encoder or performance claim.
• ADR-0060 remains valid as an isolated transition encoding proof even when a region is refused by this stronger readiness boundary.
• Raw whole-image composition, native correctness, process isolation, standalone packaging, measurement, claims, and global selection remain closed.

Acceptance gates

1. BranchMix and Bounds proofs deterministically bind the complete accepted predecessor identity chain.
2. Every allocated-region instruction/control site is covered exactly once.
3. CFG liveness and physical injectivity are independently replayed; targeted tail-only interference counterexamples fail closed.
4. Every control edge touching a persistent region receives exactly one persistent or frontier classification.
5. Entry, mixed join, same/cross-region branch, materialized tail, Bounds, Return, and budget fixtures lock positive and negative behavior.
6. Locally resealed liveness, binding, alias, clobber, frontier, total, predecessor, and seal mutations fail closed.
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 historical schema-1.0.0 BranchMix predecessor chain was accepted under proof root ef2248289423fd7690fd52289178a9e32bad8b3b111745ba6c1786e4ae0eb14b. Independent replay covers all 26 persistent regions and all 164 derived instruction/control sites. All 26 regions are ready; none requires a later destructive-reuse proof and none is refused. The sealed artifact contains 1,318 bound reads, 21 bound definitions, 1,991 live-word rows, 145 CFG edges, 152 frontier rows, 263 flush words, and 246 hydration words. Backward liveness reaches its least fixed point in two rounds using 972 charged work units. It records zero destructive reuses and zero alias conflicts.

A targeted counterexample in which two logical values do not conflict at a tail but do alias at a body site is refused. Locally resealed site liveness, frontier action, predecessor capsule identity, region status, totals, and seal mutations fail closed. Bounds and the public three-function cyclic-tail fixture pass while preserving the original target identity.

The full workspace reports 388 core tests passed, zero failed, and six ignored; process isolation and all three Gate A cases pass. Governance reports 22/22 and strict refinement 8/8. Strict Clippy, formatting, diff hygiene, and the static authority audit are clean. No raw/native/process/standalone/ measurement consumer exists, and the global encoder policy remains 1.4.0.

Subsequent independent token replay exposed that the 152 historical frontier rows could associate one reused physical register with multiple logical tokens. ADR-0063 records the counterexample and the accepted schema-1.1.0 replacement. This does not erase the evidence above; it revokes only its use as downstream frontier authority.

Correctness erratum — 2026-08-03

The complete instruction-owning region census plus exact empty-adapter cross-region classification is sealed by schema 1.1.0, policy 1.2.0, root b463794482025164e936a6d88400e145d084bb0df7a7de33540eedb6c001bba2. It contains 31 ready regions, 168 sites, 1,346 reads, 23 definitions, 2,059 live-word rows, 151 frontiers, 1,417/1,476 source/target live words, 207 flushes, 189 hydrations, zero alias conflicts and zero destructive reuse. Historical schema-1.0 evidence remains revoked as downstream authority.