GitHub

ADR-0063: Frontier live-set narrowing and register injectivity

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

Context

ADR-0061 correctly proves physical injectivity at every body site, but its frontier adapter construction expands every register-assigned logical word in a persistent region. ADR-0058 intentionally permits non-interfering logical words to reuse one physical register. Those words are never simultaneously live at a body site, yet the region-wide adapter incorrectly requires the single register to contain all of them at once.

ADR-0062’s independent frontier token machine exposed this defect: the exact BranchMix artifact reaches a flush row where one register is associated with multiple logical tokens. The previous frontier counts and seal are internally replayable evidence of the old algorithm, but they are not safe authority for body/frontier realization.

Decision drivers

  • Preserve ADR-0061 as accepted historical evidence; supersede only its frontier-adapter construction through a new schema.
  • Derive every adapter from exact CFG/site/tail live state, never all values assigned anywhere in a region.
  • Prove register injectivity independently at each source and target frontier.
  • Bind source-live and target-live sets into each sealed frontier row so later consumers cannot infer or widen them.
  • Avoid duplicate declared Entry/Bounds/Return rows when concrete operational rows already own those boundaries.
  • Keep byte, native, process, timing, and global selection authority closed.

Considered options

Forbid register reuse across an entire region

Rejected. It would discard valid coloring, sharply increase spills, and hide the frontier modeling error instead of fixing it.

Flush every mapped register once using an arbitrary logical owner

Rejected. The owner depends on the exact program point; choosing globally can materialize a stale value.

Narrow adapters to exact frontier live sets

Accepted. This is the same liveness authority already independently replayed for body sites, applied at control boundaries.

Decision

Advance X64TailSiteBindingProof to schema 1.1.0 and domain v2. Every X64TailFrontierBindingRow gains exact ordered source_live and target_live physical bindings.

The canonical live sets are:

entry                         target block live-in
ordinary branch edge          target block live-in, bound in source and target maps
Bounds checked exit           live-before of the exact checked instruction
Return                        live-before of the exact return terminator
persistent tail               exact location sources and destinations of the tail assignments
materialized/refused tail      exact location sources and all assignment destinations
shared-join/budget ingress     represented by its concrete incoming CFG/tail rows

For a source live row, flush includes exactly those bindings physically held in persistent registers. For a target live row, hydrate includes exactly those bindings assigned to persistent registers. Frame-bound live words remain sealed in the live row but require no adapter atom.

The verifier requires each live row to be canonical and injective over physical locations. It also requires every adapter word to be the exact register projection of the corresponding live row, with no missing, stale, duplicate, or region-wide extra word. Same-region ordinary edges preserve only when source and target bindings are identical. Materialized tail scheduling remains owned by ADR-0057 and is not confused with an empty adapter list.

Concrete Entry, Bounds, and Return rows own those boundaries. Their duplicate logical declarations are not emitted. SharedJoin and Budget are enforced by the complete set of concrete incoming ordinary/tail edge rows; an uncovered ingress fails closed.

Consequences

  • ADR-0061 schema 1.0.0 frontier adapters are superseded and may not feed ADR-0062 or any encoder.
  • Body site binding, whole-CFG liveness, region readiness, and tail capsule identity from ADR-0061 remain conceptually unchanged and are regenerated under the new seal.
  • Adapter traffic should fall because dead mappings are no longer materialized; that is structural evidence, not a performance claim.
  • ADR-0062 may be accepted only after it passes against the corrected proof; that dependent gate is now satisfied.
  • Global encoder policy remains 1.4.0.

Acceptance gates

  1. BranchMix has no frontier row mapping two logical tokens to one physical register, and every adapter is the exact projection of its live row.
  2. A targeted region-wide reuse fixture fails the old construction but passes exact live-set narrowing without losing a live token.
  3. Entry, both branch arms, Bounds, persistent/materialized tail, and public cyclic-tail fixtures lock deterministic source/target live bindings.
  4. Locally resealed live-row, adapter, action, total, predecessor, and seal mutations fail closed.
  5. ADR-0062’s independent token machine accepts the corrected predecessor and rejects deliberate duplicate-register frontier mutations.
  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 corrected schema-1.1.0 BranchMix proof is accepted under root d2a44a525d9a5b1f64e5b69e82c6bbcd193a883c674b5c04a402b7a182ad6d6e. It retains all 26 ready regions, 164 sites, 1,318 reads, 21 definitions, 1,991 live-word rows, 145 CFG edges, two fixed-point rounds, zero destructive reuses, and zero alias conflicts. Its 146 concrete frontier rows bind 1,390 source-live and 1,476 target-live words, projecting exactly 209 flushes and 189 hydrations with no duplicate physical register in any adapter. Analysis uses 972 charged work units.

Relative to the superseded region-wide construction, concrete frontier rows fall from 152 to 146, flushes from 263 to 209, and hydrations from 246 to 189. This is a proof-shape reduction, not a runtime performance claim. Locally resealed live-set, adapter, duplicate-register, total, predecessor, and seal mutations fail closed. ADR-0062’s independent token machine accepts the corrected proof and rejects the original impossible token ownership.

The full workspace/all-target suite passes. The core library discovers 390 tests: 384 pass and six explicitly expensive release-only tests remain ignored. 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

The narrowed-frontier authority is now the schema-1.1.0, policy-1.2.0 site proof under root b463794482025164e936a6d88400e145d084bb0df7a7de33540eedb6c001bba2. It includes singleton regions for every remaining instruction-owning block and therefore supersedes the prior 26-region/146-frontier vector with the exact 31-region/151-frontier vector recorded by ADR-0061’s erratum. Register injectivity and fail-closed replay remain mandatory.