ADR-0057: Bounded persistent typed tail-state plan

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

Context

ADR-0056 proves that fixed process/startup work is essentially symmetric and that tail-transfer templates dominate the rejected policy-1.5 candidate. The next optimization cannot be another local byte rewrite. Repeated staging, home loads, home stores, and destructive argument shuffles are consequences of treating every tail edge as a complete machine-state boundary.

NAUX needs a proof object for the stronger alternative: retain typed logical state across a bounded connected tail region and materialize it only where semantics or finite proof limits require a boundary. This decision is about the plan and its independent replay only. It grants no encoding, execution, measurement, claim, or global policy authority.

Decision

Introduce a sovereign X64TailStatePlan derived only from an already verified R1-S7a target artifact. The plan is sealed to the exact target semantic, plan, and code identities and contains no candidate machine bytes.

For every canonical tail edge the planner expands arguments and parameters into exact typed 64-bit words. F64Array is represented as the ordered pair ArrayData and ArrayLength; Bool, I64, and F64 retain distinct word types; Unit contributes no word. A source and destination may be treated as an identity only when their physical frame-word location and word type are both equal.

Each non-frontier tail edge receives a canonical parallel-copy schedule. The scheduler snapshots all sources conceptually, emits acyclic moves when their destination is no longer a pending source, and breaks a cycle by saving the cycle destination in a typed scratch word before rewriting all matching sources to that scratch. One scratch word is sufficient at a time because a cycle is drained before another scratch save is admitted. The verifier independently executes the schedule over symbolic source tokens and compares the result with parallel snapshot semantics.

Persistent edges are grouped into deterministic weakly connected regions. The region is metadata for a future physical allocator; it is not permission to assume an unbounded hardware register file. Every region records its exact edge set, label set, maximum word width, scratch use, logical move bound, and conservative future machine-byte bound.

The following are forced materialization frontiers:

• entry ABI ingress;
• any target label with more than one canonical predecessor;
• a block containing a checked Bounds operation;
• every return transfer;
• any edge or region exceeding the frozen planner limits.

A malformed, ambiguous, irreducible, or over-budget state web is rejected as a whole. It is never partly selected with an ordinary encoder fallback hidden inside it. Frontier and refusal records are first-class sealed evidence.

Traffic accounting is deliberately conservative. The plan records current frame traffic, frontier materialization traffic, logical persistent moves, scratch saves, and a fixed maximum encoded-byte charge per future operation. These are structural upper bounds, not cycle estimates or performance claims.

Trust boundary

The constructor may use deterministic graph discovery and scheduling. The verifier must separately:

1. verify the source target artifact;
2. replay the plan seal;
3. reconstruct and compare the complete canonical plan;
4. check all limits and exact edge/frontier coverage;
5. replay every copy schedule using symbolic snapshot semantics;
6. reject type confusion, alias ambiguity, duplicate destinations, stale scratch reads, incomplete writes, arithmetic overflow, and locally resealed mutations.

The module must not import the raw encoder, native runner, standalone writer, profile measurement, or policy-selection paths. No public API converts a verified tail-state plan into executable bytes.

Frozen limits

• at most 4,096 canonical tail edges;
• at most 32 argument words per tail edge;
• at most 16,384 schedule steps in the complete plan;
• at most 4,096 persistent regions;
• at most 4,096 frontier records;
• at most 15 prospective bytes charged per logical machine operation.

The limits are policy identity. Raising one requires a successor ADR.

Consequences

• NAUX gains a representation-level path capable of removing repeated tail-state materialization rather than optimizing the copies one at a time.
• Alias and cycle correctness becomes independently checkable before a physical register assignment exists.
• Some edges will remain materialized or refused. This is explicit evidence, not a hidden performance fallback.
• Encoder policy remains exactly 1.4.0. A later ADR must introduce a bounded physical bank allocation, candidate byte encoding, independent decoding, finite correctness, isolated-process/standalone correspondence, and fresh matched measurement in that order.

Acceptance gates

1. Canonical plans and roots are deterministic for the lighthouse targets.
2. Exact tail-edge, word, identity, schedule, region, and frontier coverage reconciles with no omission or overlap.
3. Identity, acyclic permutation, two-cycle, longer cycle, duplicate source, immediate, and ordered array-pair cases replay exactly.
4. Wrong word types, duplicate destinations, stale scratch reads, missing writes, schedule reordering, wrong region membership, wrong frontier, limits, totals, source identities, and seals fail closed, including after local resealing.
5. Format, strict lint, focused tests, workspace tests, governance tests, and static authority audit pass.
6. X64_TARGET_ENCODER_POLICY_VERSION remains 1.4.0, and no encoder, executable, standalone, or claim path consumes the verified plan.

Accepted evidence

The canonical BranchMix policy-1.4 target produces plan root:

276ab1ed0ac7b692ed55275457db5a0356b0ca1e9ea1cd8fc33f30c5a21cf48a

Its exact structural ledger is:

tail edges                                      127
persistent edges                                108
forced-materialization edges                     19
refused edges                                      0
tail argument words                            1,289
identity words                                 1,100
logical moves                                    189
scratch saves                                      0
persistent regions                                26
forced frontiers                                  13
current frame-traffic upper bound              5,156
proposed frame-traffic upper bound             1,158
prospective machine-byte upper bound          20,840

The traffic figures are unweighted structural upper bounds. They prove that the representation exposes a bounded elimination opportunity; they do not predict cycles, code size, or Gate B performance. The zero scratch count is a property of this exact lighthouse artifact, not an unsupported claim that cycles cannot occur. Independent two-node and three-node cycle cases require and replay one typed scratch save.

Acceptance execution passed:

• seven focused unit tests covering identity, acyclic and duplicate-source copies, immediates, two/three cycles, ordered array words, stale scratch, type confusion, schedule reordering, Bounds/shared-join frontiers, both budget refusals, and locally resealed mutations;
• the public ADR-0057 integration boundary test;
• all workspace tests: 372 core/library tests passed with six deliberately ignored heavyweight evidence replays, followed by every integration and documentation test with zero failures;
• strict all-target/all-feature Clippy, format, and diff checks;
• all 22 governance script tests and all eight strict refinement closed-loop tests;
• a static authority audit showing the verified plan has no consumer in raw encoding, native execution, standalone packaging, measurement, claim, or global encoder-selection paths.

Global encoder policy remains exactly 1.4.0.

Correctness erratum — 2026-08-03

Typed homes at the same frame byte offset are one storage location even when their logical word types differ. The former scheduler keyed storage by (offset, type) and could therefore overwrite a still-live source through a typed alias. Policy 1.2.0 keys frame storage by byte offset, snapshots all sources before writes, rejects duplicate physical destinations and fails closed on cross-typed live-source ambiguity. The superseding BranchMix plan root is 576041d7747cf3d7e871307b04edf3b21bd3e87ddea0443cad8fea4b436bfa0b. It retains 127/108/19 accepted/persistent/materialized edges and 189 logical moves, now records two required scratch saves and a 20,870-byte conservative candidate upper bound. Earlier roots remain historical evidence only.