GitHub

ADR-0058: Bounded sovereign physical tail-bank allocation

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

Context

ADR-0057 proves logical parallel-copy semantics and exposes persistent typed tail-state regions, but deliberately assumes no physical register file. A future encoder cannot consume that plan until every retained word has a finite x86-64 residence, every conflict is derived from verified facts, and every spill or scratch transition refines the logical snapshot.

The allocation boundary must remain sovereign and proof-only. Importing an external register allocator, trusting trace-local liveness, or emitting bytes while allocation semantics are still ambiguous would move correctness into an unowned heuristic and violate the North Star admission rule.

Decision drivers

  • Persistent state must survive all currently admitted instruction templates.
  • Physical capacity must be finite, inspectable, and part of policy identity.
  • Distinct logical words that coexist in a tail snapshot must never alias one register.
  • Register reuse must follow only from verified non-interference.
  • Spill, immediate, register-copy, frame-copy, and cycle-scratch behavior must be explicit and symbolically replayable.
  • Any over-budget region must be refused as a whole, without partial allocation or ordinary-encoder fallback inside a selected region.
  • The artifact must contain no candidate code bytes and grant no execution or global encoder authority.

Considered options

Reuse the current temporary registers

RAX/RCX/RDX/R8 and XMM0..XMM2 already participate in arithmetic, checked array access, comparison, and policy-1.4 superblock templates. Keeping persistent state there would require trusting undocumented clobber behavior or simultaneously redesigning instruction lowering. Rejected for this boundary.

Use SysV callee-saved registers

RBX/R12..R15 provide a useful bank but require new prologue/epilogue save and restore semantics. That creates an ABI mutation before physical transition proof is established. Deferred; a successor policy may admit them with an explicit preservation proof.

Use an external or unconstrained allocator

LLVM-style coloring, caller-provided liveness, or an unbounded virtual bank could produce good allocations but would neither be sovereign nor finite. Rejected.

Frozen non-clobbered caller-saved bank

Use registers that the current admitted instruction templates do not modify after ABI ingress. This keeps allocation independent of candidate encoding while preserving a direct future lowering path. Accepted.

Decision

Introduce a sealed X64TailPhysicalAllocation derived from an independently verified R1-S7a target and accepted ADR-0057 logical plan.

The physical bank is exactly:

GPR persistent lanes: RDI, RSI, R9, R10, R11
XMM persistent lanes: XMM3, XMM4, XMM5, XMM6, XMM7
GPR cycle scratch:    RAX
XMM cycle scratch:    XMM0

Bool, I64, ArrayData, and ArrayLength inhabit the GPR bank. F64 inhabits the XMM bank. A physical location carries its logical word type even when the underlying register lane is reused at a disjoint point.

For each accepted ADR-0057 region, the allocator derives a conservative live set at every tail edge from all source locations and all destinations in that edge’s parallel snapshot. Every pair of distinct same-bank locations in that set interferes. This deliberately over-approximates liveness: it may spill an otherwise reusable word, but it cannot silently overlap values required by snapshot semantics.

Locations are ordered deterministically by descending interference degree, descending occurrence count, then canonical typed frame location. Each takes the lowest available bank lane not occupied by an already allocated neighbor; otherwise it retains its canonical frame location as an explicit spill. This is a reproducible bounded heuristic, not an optimal-coloring claim.

Every persistent logical edge is then lowered into a proof-only physical parallel assignment and scheduled with typed scratch cycle breaking. The independent verifier initializes physical locations with distinct symbolic logical tokens, executes the schedule, and requires every destination to equal the ADR-0057 snapshot result. Register/register, frame/register, register/frame, frame/frame, immediate/register, and immediate/frame paths are all explicit evidence.

Frozen limits

  • five persistent GPR lanes and five persistent XMM lanes;
  • one reserved scratch lane per bank;
  • at most 256 logical locations per region;
  • at most 32,768 interference pairs in the complete allocation;
  • at most 16,384 physical transition steps;
  • at most 1,000,000 checked allocation-work units;
  • at most 15 prospective bytes charged per physical operation;
  • at most 16 MiB canonical allocation evidence.

Limit exhaustion refuses the complete affected region or the complete artifact as specified by the field; it never returns a partial selected region.

Independent verification

The verifier must:

  1. independently verify the target and ADR-0057 plan;
  2. replay the allocation seal and reconstruct the complete canonical artifact;
  3. derive all region locations, occurrence counts, live sets, peak pressure, and same-bank interference without trusting allocator metadata;
  4. prove register-bank/type compatibility and reject any conflicting pair sharing a register;
  5. prove exact region/edge/location coverage and whole-region refusal;
  6. replay every physical transition against ADR-0057 parallel snapshot semantics with stale-scratch, duplicate-write, missing-write, and physical alias rejection;
  7. recompute traffic and conservative byte totals with checked arithmetic;
  8. reject all locally resealed provenance, allocation, pressure, interference, spill, transition, schedule, total, and seal mutations.

Consequences

  • NAUX owns an end-to-end logical-to-physical tail-state proof without an external allocator.
  • The chosen bank remains compatible with existing instruction clobbers, but the first candidate encoder must still prove that it preserves those lanes.
  • Conservative liveness may spill more than a future instruction-aware allocator. Exact pressure/spill evidence makes that cost visible.
  • No candidate bytes, decoder authority, native authority, standalone authority, performance claim, or global policy change is admitted.
  • A successor ADR may authorize a non-executable candidate byte capsule only after allocation evidence is accepted and independently replayable.

Acceptance gates

  1. BranchMix and Bounds allocations are deterministic and sealed to exact target plus ADR-0057 identities.
  2. All persistent logical edges are covered exactly once by an allocated region transition or by a whole-region refusal.
  3. Live-set/interference replay proves no physical register aliases a coexisting same-bank logical word.
  4. Register, spill, immediate, mixed-storage, two-cycle, longer-cycle, and both-bank scratch cases refine logical snapshot semantics.
  5. Adversarial and locally resealed mutations fail closed.
  6. Focused, public-boundary, workspace, strict lint, governance, format/diff, and static authority gates pass.
  7. Global encoder policy remains exactly 1.4.0 and no executable path consumes the verified allocation.

Accepted evidence

The exact BranchMix policy-1.4 allocation is sealed under root d3f88102d10b26160b1fca63dc427a8cfb22a3e263b916bfdc6ff56eab09f33e. It allocates all 26 accepted ADR-0057 regions and refuses none. Across those regions the verifier reconstructs 346 logical locations, 176 register locations, 170 canonical frame spills, 1,579 same-bank interference pairs, 108 physical transitions, 150 physical moves, 63 frame loads, 102 frame stores, 17 immediate materializations, and 7,173 allocation-work units. Its transition-only conservative machine-byte upper bound is 2,790 bytes. That bound excludes ADR-0057 materialization frontiers and is neither whole-image code size nor a performance claim.

BranchMix requires no cycle scratch after the frozen allocation. Independent artificial transition tests nevertheless force and replay both GPR (RAX) and XMM (XMM0) cycle breaking, so the zero BranchMix scratch count is an exact workload property rather than an untested scheduler assumption.

Acceptance validation passed:

  • five focused allocator/verifier unit tests and the public ADR-0058 boundary;
  • the complete workspace suite, including 377 core library tests with zero failures and six explicitly ignored heavyweight opt-in tests;
  • strict Clippy for every package target and feature;
  • 22 governance tests and eight strict refinement closed-loop tests;
  • format, diff, and static authority audits.

The authority audit finds the verified allocation only in its proof module, public re-export, and tests. No raw encoder, native runner, process worker, standalone image, measurement, or claim path consumes it. Global encoder policy remains exactly 1.4.0.

Correctness erratum — 2026-08-03

Physical replay now shares ADR-0057’s byte-storage identity: frame aliases are keyed by offset, sources are snapshotted before destinations, and ambiguous typed live aliases fail closed. A conservative region-wide same-bank clique prevents an allocation from depending on a weaker local interference fact. Policy 1.1.0 supersedes the historical allocation under root 7153bd9997b4d2af85149ba172f3cd2a0d3a2d20d3d42c765742b5f3294841ae: 31 regions, 346 locations, 176 registers, 170 spills, 1,675 interference pairs, 150 moves, 61 frame loads, 100 frame stores, 17 immediates, zero scratch saves, and 3,745 charged allocation-work units. These are structural facts, not native-performance evidence.