ADR-0049: Proof-Only Shadow Prospective Shared-Join Realization

Status: accepted; proof-only implementation, schema migration, independent replay, adversarial corpus, and regenerative seal complete; encoder policy 1.5 remains unadmitted

Date: 2026-08-01

Visibility: private NAUX architecture/governance record. This ADR is not public roadmap material.

Related: ADR-0037, ADR-0041, ADR-0044, ADR-0045, ADR-0046, ADR-0047, ADR-0048

Extends: ADR-0048’s exact per-ingress ordered lineage into an accepted proof-only physical realization without superseding any accepted ADR

Preserves: target-plan schema, lowering policy, encoder policy 1.4.0, target-plan semantics, ABI, policy-1.4 raw code bytes, labels, fixups, target/native/process/standalone identities, benchmark workload, timing harness, Machine IR provenance, Bounds ordering, and every upstream semantic contract. Target-profile and Gate B wrapper schemas migrate to 1.5.0 and their proof policies migrate to 1.4.0 only for the accepted shadow evidence.

Context

ADR-0048 closes the logical route boundary needed by a future shared-join realization. Every ingress has an exact ordered route, an unambiguous dynamic count authority, and, for a fused comparison, exact per-ingress branch-arm counts. That evidence proves which logical executions a future clone may represent. It does not yet prove a physical byte layout.

Policy 1.4 has one RawRealizationAtom per emitted byte span. Its event can also provide the execution count because an accepted policy-1.4 semantic event normally owns one physical template site. Shared-join realization would clone one semantic event into multiple physical sites. Reusing the semantic event as the count authority would charge every clone the aggregate count and would double-count transitive paths. Fused-compare else-jump templates also need the per-ingress else cell rather than the aggregate branch count.

The current shared-join composition planner constructs prospective composed chains internally to prove feasibility, then deliberately discards those chains. It does not assign physical atom ownership, move labels to tombstones, assign fixups to atoms, or calculate a candidate code-growth receipt. Mutating the accepted policy-1.4 EmissionPlan to obtain those answers would make proof metadata silently control current code generation.

Exact byte ownership cannot be established from analytical size estimates alone. Variable tail-copy schedules, branch templates, label offsets, and rel32 displacements must be materialized by the owned raw templates. The candidate may therefore be encoded into a bounded private shadow buffer for verification, but it must not become the target artifact, executable input, or policy-1.5 output.

Decision drivers

• Keep the accepted policy-1.4 artifact as the only executable result.
• Separate logical semantic identity from physical execution-count authority.
• Bind every prospective byte, label, tombstone, and fixup to one owner.
• Include zero-count ingresses because workload evidence is not a semantic reachability proof.
• Obtain exact byte and rel32 receipts from NAUX-owned templates, not an estimate or third-party assembler.
• Bound work, replicas, atoms, fixups, memory, total code, and code growth.
• Refuse the whole prospective proof on one missing, ambiguous, overflowing, or non-canonical receipt.
• Independently reconstruct and seal the result before it can become evidence for any later encoder policy.

Considered options

1. Mutate EmissionPlan and emit policy 1.5 directly

This is the shortest implementation path, but it combines candidate planning, accepted code selection, and proof migration. A partially valid candidate could affect current bytes before ownership and fallback are independently checked. This option is rejected.

2. Predict candidate byte sizes without encoding

Analytical template sizes avoid a shadow buffer, but they do not prove exact copy schedules, atom boundaries, fixup offsets, displacements, or the final code hash. This option may be useful for an early heuristic but is rejected as realization evidence.

3. Encode, execute, and benchmark an unsealed candidate

This produces early measurements, but correctness and ownership would depend on bytes outside the accepted artifact boundary. A fast unsealed result is not admissible NAUX evidence. This option is rejected.

4. Build a proof-only shadow realization and discard its bytes

This preserves policy 1.4 while providing exact owned-template receipts for a future policy decision. The additional planner, verifier, schema payload, and test surface are accepted costs. This is the accepted option.

Decision

1. Separate prospective plan

The implementation introduces a ProspectiveSharedJoinPlan distinct from the accepted policy-1.4 EmissionPlan. It may reuse one pure composition builder, but it must own a separate copy of:

• final composed chains;
• policy-1.4 consumed labels plus selected shared targets;
• the exact physical root for each clone;
• the ADR-0048 ingress row that authorizes each clone; and
• the complete prospective refusal state.

The implementation must not add candidate chains to EmissionPlan, mutate its reachable, consumed, or chains fields, or let a Gate B profile label select encoder behavior. If one shared target, ingress, route, or dependency cannot be reconstructed exactly, no partial prospective plan is retained.

2. Private shadow emission

The policy-1.4 blob is encoded and retained first. A complete prospective plan may then be emitted into a separate bounded memory buffer using the existing owned instruction templates. The shadow buffer exists only long enough to:

1. patch and verify its internal rel32 transfers;
2. construct atom, label, tombstone, and fixup receipts;
3. compute a domain-separated prospective code hash; and
4. support independent replay.

The candidate bytes are never installed in X64TargetProgram, returned as the selected RawEncoding.code, loaded into executable memory, written into an ELF image, timed, or presented as policy 1.5. Public proof data carries the candidate hash and bounded receipts, not the candidate byte vector. The private vector is dropped after replay.

Generating exact bytes in this private verifier boundary is shadow emission, not encoder-policy admission. Exact byte and fixup ownership depend on this private generation step; removing it requires a superseding proof decision.

3. Exact prospective atom identity

Every non-empty shadow byte span belongs to exactly one prospective atom in strict physical order. An atom records independent fields for:

physical owner
semantic event
execution authority
template class
start offset
end offset

physical owner identifies the entry adapter, physical block root, return or Bounds epilogue, or exact tombstone label. It prevents an unlabelled inline clone from losing its placement identity.

semantic event remains the original logical event, such as Instruction { target, 0 }, Tail { target }, Branch { bridge }, or BranchElse { bridge }. Cloning never creates a new logical event.

execution authority is separate:

Semantic { event }
SharedJoin {
    target,
    root,
    authority_trigger,
    partition: All | Else,
}
Static

Ordinary atoms use their canonical semantic-event count. A cloned register instruction and its cloned tail use the exact ingress All count. A cloned fused-compare instruction and conditional branch template use All; its fall-through else-jump template uses the exact ingress Else cell. The current layout has no then-only template. A future inverted or then-only layout requires a new proof decision rather than silently reinterpreting this authority enum.

The profile verifier must prove that clone-authority sums conserve every logical event count. An authority row with zero executions still owns a structurally complete clone and all of its receipts.

4. Label and tombstone ownership

The first prospective boundary introduces no synthetic labels and does not change the declared label-id or label-owner set. Each declared label maps to exactly one candidate atom start. Each receipt is one of:

Live
Tombstone(Unreachable)
Tombstone(Policy14Consumed)
Tombstone(SharedJoinConsumed)

Every selected shared target must have exactly one SharedJoinConsumed one-byte NOP tombstone at its original label. Its clones are fall-through-only atoms within their exact physical ingress roots. No clone acquires an alias label, and no two declared labels may share a candidate offset.

Profile counts never decide whether a label is removed. In particular, a zero-count BranchMix ingress remains semantically live unless the ordinary target verifier proves otherwise.

5. Fixup ownership

Candidate fixups remain canonical internal rel32 fixups. Every fixup receipt binds:

fixup index
owning atom index
patch offset
target label
addend

The patch range must lie wholly inside exactly one non-tombstone atom. Fixups are strictly patch-offset ordered, reconstruct the exact encoded displacement, and resolve to one declared Live label. A fixup targeting any tombstone, selected shared body, unknown label, shared offset, or out-of-range patch refuses the complete prospective realization.

6. Exact byte accounting and caps

The receipt records policy-1.4 static bytes, candidate static bytes, bytes added, bytes removed, candidate atom count, label count, and fixup count. Added and removed bytes are separate checked non-negative values; signed or saturating arithmetic is not authority.

The existing shared-join caps remain inherited:

composition targets       <= 16
predecessors per target    <= 8
body replicas              <= 64
composition work           <= 32,000,000

The prospective boundary adds these fail-closed constraints:

• candidate labels equal the policy-1.4 declared label set exactly;
• candidate atoms do not exceed policy_1_4_atoms + 3 * body_replicas;
• candidate fixups do not exceed both the target global limit and policy_1_4_fixups + 2 * body_replicas;
• candidate code does not exceed the target global code-byte limit;
• positive candidate growth does not exceed min(policy_1_4_static_bytes / 4, 64 KiB); and
• all planning, receipt construction, multiplication, addition, conversion, and allocation lengths are checked before use.

These are admission ceilings, not profitability claims. An implementation may impose tighter limits; widening one requires a new ADR that supersedes this accepted boundary.

7. All-or-nothing fallback

Prospective failure has a different fallback tier from policy-1.4 failure. Policy 1.4 is encoded first and is the cached baseline. Any prospective planning, emission, patching, cap, ownership, hashing, or replay failure produces:

complete = false
candidate hash = zero
all prospective vectors and totals = empty/zero
selected artifact = exact cached policy-1.4 encoding

It must not fall through to the ordinary pre-policy-1.4 blob, and a successful prospective proof still returns policy-1.4 bytes while this ADR is the latest decision.

8. Independent replay and canonical seal

The raw prospective builder and profile verifier deliberately have separate responsibilities. The builder emits bytes and receipts. The verifier independently reconstructs from the verified target program, ADR-0048 routes, branch cells, and candidate bytes:

• clone placement and semantic event;
• All and Else authority selection;
• byte-span coverage and class;
• label disposition and one-byte tombstones;
• fixup ownership, decoded displacement, and live target;
• checked static and weighted totals; and
• the prospective code and realization hashes.

Canonical encoding follows physical atom order, label-id order, fixup patch order, and existing composition-step/ingress order. A self-resealed mutation must fail comparison with a freshly regenerated profile; recomputing a hash over malformed supplied metadata is not replay.

9. Proof schema is admitted; encoder boundary remains closed

The accepted proof versions are:

target-profile schema       1.5.0
target-profile proof policy 1.4.0
Gate B wrapper schema       1.5.0
Gate B proof policy         1.4.0
encoder policy              1.4.0

Schema 1.5.0 and proof policy 1.4.0 are admitted only for the prospective proof payload after implementation, independent verification, adversarial tests, full acceptance gates, and explicit regenerative release replay. Encoder policy remains 1.4.0; this ADR neither reserves nor authorizes policy-1.5 bytes.

Scope explicitly excluded

• selecting candidate bytes as an X64TargetArtifact;
• loading, executing, packaging, or benchmarking the candidate;
• encoder policy 1.5 or target-plan schema migration;
• native, isolated-process, startup, ELF, or standalone identity migration;
• a Gate B speed or cycle claim;
• independent semantic decoding of cloned register-instruction and register-tail machine bytes;
• general physical register allocation;
• checked-array shared joins; and
• broader target or ABI coverage.

Those remain separate later decisions after the prospective proof is accepted.

Validation required before acceptance

1. deterministic reconstruction of the complete BranchMix candidate from the accepted policy-1.4 baseline and ADR-0048 composition;
2. exact 11-replica semantic-event/authority mapping, including target 121 authorities 107/117 and target 48 authorities 38/107/117;
3. structural realization of the zero-count target-49 authority row;
4. contiguous non-overlapping atom coverage of every candidate byte;
5. one owner and canonical disposition for every declared label;
6. exact one-byte shared-target tombstones and no live fixup to any tombstone;
7. one in-range atom owner and independently decoded displacement for every fixup;
8. checked code, growth, atom, fixup, replica, work, and allocation caps;
9. deterministic candidate code and realization hashes across repeated builds;
10. conservation of logical instruction, tail, branch, and else-event counts across cloned atoms;
11. cap, cycle, route, authority, scheduling, patch, or arithmetic refusal yielding no partial prospective evidence and exact policy-1.4 fallback;
12. adversarial semantic-event, authority, All/Else, physical-root, atom span, label disposition, tombstone, fixup owner, target, displacement, byte-total, and hash mutations;
13. self-resealed prospective metadata rejected by regenerative replay;
14. unchanged policy-1.4 target, plan, code, label, fixup, native, process, startup, ELF, and standalone identities;
15. focused raw/profile tests, all debug and release workspace tests, strict refinement, Clippy with warnings denied, format, and diff gates; and
16. an explicit ignored release-mode regenerative profile replay before any schema-1.5 seal is accepted.

All sixteen items are accepted for the bounded BranchMix shadow. The sealed receipt is:

selected policy-1.4 bytes       3,097
candidate shadow bytes          3,214
bytes added / removed           117 / 0
selected / candidate atoms      179 / 199
labels / candidate fixups       142 / 51
body replicas                   11
shared-authority atoms          31
candidate weighted bytes        2,574,710,635
candidate code hash             0e392caf51dbc65f9e36e08c678118e78b8f6aed90bf1df0edbf4b5c6a5f5173
prospective realization hash    5f9b86ddb38f2b2a58f22cc4adb2bc4589f4f86ecf7d7fdae175204ae9266e15
Gate B schema-1.5 profile hash  2e7a1265e526d01697038fd7b0fac69258b9a17ce7362f063c3132551a78eb47

The target-49 zero-count root 30 owns complete fused-compare, conditional, and else-jump atoms with zero executions and zero weighted bytes. Root 31 owns the same three classes with one execution and exact weights 34/6/5. The candidate remains private, is independently replayed, and is discarded; the selected policy-1.4 code hash and every downstream executable identity remain unchanged.

Focused raw 36/36, profile 5/5, and Gate wrapper 1/1 tests pass. Full debug and release workspace suites, strict refinement 8/8, Clippy with warnings denied, format, and diff gates pass. The explicit ignored release-mode seal passes 1/1 in 319.21 seconds after complete emit, independent regeneration, and self-resealed mutation rejection.

This acceptance proves structural ownership, exact NAUX-template bytes, fixups, counts, and canonical identities. It does not independently decode the machine semantics of the cloned register instruction and register-tail templates. That stronger proof is required before any later encoder-policy admission may select or execute the candidate.

Consequences

Positive

• Physical cloning becomes auditable without risking accepted executable bytes.
• Semantic identity and dynamic count authority cannot be conflated.
• Label, tombstone, fixup, and byte growth receive one bounded ownership model.
• Zero-count rows cannot hide malformed code structure.
• A future encoder-policy proposal can start from exact sealed receipts rather than an optimizer prototype.

Negative

• The raw templates run once more into a private shadow buffer.
• Planning, emission, and independent verification retain intentionally duplicated checks.
• The profile-schema migration and regenerative replay are now permanent proof-surface costs even though executable bytes remain unchanged.
• The initial no-synthetic-label and growth caps may refuse otherwise valid layouts.
• Structural template replay alone is insufficient for encoder admission; a later independent machine-semantic decoder must close that stronger gate.

Risks and mitigations

• Circular proof: the verifier reconstructs ownership and decodes fixups independently instead of trusting the builder’s receipt map.
• Policy contamination: candidate chains live outside EmissionPlan, and selected output is always the cached policy-1.4 blob.
• Count multiplication: every cloned atom names one exact ingress row and partition; aggregate conservation is checked.
• Profile-directed miscompilation: zero-count rows remain structurally present and profile counts never control reachability.
• Logical/physical route confusion: ADR-0048 no-op bridge events remain logical evidence; they do not become byte atoms unless an owned template actually emits bytes.
• Tail to tombstone: every fixup target must have a Live label receipt.
• Resource explosion: independent target, predecessor, replica, work, atom, fixup, code, and growth caps fail closed.
• Premature performance claim: candidate hashes and weighted bytes are structural evidence only; Gate B timing remains open.
• Template-semantic circularity: this ADR deliberately does not claim an implementation-diverse decode of cloned register/tail bytes; candidate selection stays closed until a later verifier supplies it.

Implementation map

The accepted implementation is intentionally kept beside the policy-1.4 authorities it audits:

• naux-lang/src/core/x64_target/raw.rs: separate plan, shadow emission, receipts, caps, raw adversarial corpus, and the policy-1.4 fallback seam;
• naux-lang/src/core/x64_target/profile.rs: independent authority resolution, byte/fixup/label replay, conservation, bounded public projection, canonical realization hash, and adversarial reconstruction;
• naux-lang/src/core/x64_gate_b_profile.rs: canonical prospective encoding, exact allocation preflight, regenerative comparison, Gate mutations, and the accepted schema-1.5 seal; and
• naux-lang/src/core/x64_target.rs plus core/mod.rs: accepted public proof types and versioned re-exports. None exposes the candidate byte vector as a selectable artifact.