ADR-0050: Bounded Independent Shadow Machine-Semantic Decoder

Status: accepted for the bounded proof boundary; encoder policy 1.5 remains closed and no candidate bytes are selected or executed

Date: 2026-08-02

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

Related: ADR-0036, ADR-0037, ADR-0044, ADR-0048, ADR-0049

Extends: ADR-0049’s accepted proof-only physical realization with an implementation-diverse semantic check for cloned register instruction and register-tail bytes

Preserves: target-plan schema, lowering policy, encoder policy 1.4.0, every policy-1.4 executable identity, benchmark policy, ABI, Machine IR provenance, Bounds ordering, and all upstream semantic contracts; admits only target-profile/Gate B schema 1.6.0 and proof policy 1.5.0

Context

ADR-0049 proves that every prospective shadow byte has one atom, physical owner, semantic event, execution authority, label disposition, and fixup receipt. Its independent replay decodes rel32 displacements and verifies fused clones against normalized accepted bytes. It intentionally does not establish implementation-diverse machine semantics for the register-resident instruction and tail clones.

For the frozen BranchMix candidate, roots 106 and 116 each contain an accepted register-resident F64 instruction, a cloned target-121 I64 add, and a cloned tail-copy schedule. The machine sequence keeps values in XMM2 and R8, performs frame transfers, and falls through into the downstream fused target 48. Byte equality with the raw encoder would prove deterministic copying, not that those bytes implement the ordered target semantics.

Executing the candidate is also premature. It would place an unadmitted artifact inside the native correctness path, and a finite result comparison could miss malformed code outside the observed values. NAUX instead needs a small owned decoder with symbolic semantics, independent of raw emission.

Decision drivers

Do not call raw emission helpers from the semantic verifier.
Decode actual candidate bytes rather than trusting atom metadata.
Compare semantic state transitions, not opcode spellings alone.
Preserve typed GPR/XMM residency and simultaneous tail-assignment meaning.
Bind fallthrough or rel32 control to the exact continuation route.
Reject unknown opcodes, registers, addressing modes, padding, trailing bytes, type mismatches, ambiguous routes, and resource overflow.
Keep candidate bytes private, unselected, unexecuted, and untimed.
Add no third-party disassembler, SMT solver, assembler, or runtime.

Considered options

1. Re-emit expected bytes and compare

This catches mutation but shares the encoder’s templates and mistakes. It is retained as structural evidence under ADR-0049 and rejected as the new semantic authority.

2. Execute the shadow candidate on a finite corpus

This widens the executable trust boundary before policy admission and proves only the tested values. It is rejected for this stage.

3. Use an external x86 decoder or solver

An external decoder could diversify implementation, but it creates dependency debt in a production proof path and violates the sovereignty direction. It may be used only as optional research comparison and is rejected as canonical evidence.

4. Decode a bounded owned subset and compare symbolic transitions

This provides implementation diversity while keeping the proof surface small and fail-closed. Supporting only the exact current register-clone subset is an accepted initial restriction. This is the accepted option.

Decision

1. Separate decoder module

The verifier lives outside raw.rs and must not import or invoke RawEmitter, emit_planned_instruction, emit_value_tail_transfer, or any instruction-template helper. It receives only:

verified X64TargetProgram
accepted shared-join composition and routes
transient candidate bytes, atoms, labels, and fixups

The decoder remains private to target profiling. Only its bounded aggregate coverage receipt is public and seal-visible; expression graphs, registers, candidate bytes, and transient states are not serialized.

2. Exact admitted x86 subset

The first decoder admits the instruction forms needed by the bounded BranchMix register slices:

mov r64, [rsp + disp32]
mov [rsp + disp32], r64
movabs r64, imm64
mov r64, r64
add/sub/imul r64, r64
movsd xmm, [rsp + disp32]
movsd [rsp + disp32], xmm
movsd xmm, xmm
addsd/subsd xmm, xmm
optional terminal jmp rel32

Only canonical encodings, declared registers, stack-relative disp32 homes, and fully consumed byte slices are accepted. An unsupported planned instruction or machine form refuses the complete semantic proof; it never falls back to heuristic decoding.

3. Typed symbolic machine

The decoder executes into a bounded symbolic state. Physical stack offsets carry bit values rather than one global type because separate functions may legitimately reuse the same offset at different types. Type is resolved and checked at each target operation, XMM boundary, home write, tail parameter, and continuation comparison:

frame word(offset) -> delayed bit expression
typed boundary     -> canonical typed expression
GPR register       -> delayed or typed expression
XMM register       -> checked F64-bit expression
control            -> fallthrough or exact label

Expressions preserve operation identity and operand order. I64 arithmetic is wrapping; F64 expressions retain the accepted SSE2 operation and numeric contract without host evaluation. Loads read the current symbolic frame; stores update it. Reading an uninitialized register, crossing a frame home, using a register in the wrong bank, or producing an ill-typed expression refuses the proof.

4. Independent reference transition

The reference side starts from the same symbolic frame and reconstructs the logical path from target blocks and ADR-0048 routes:

start after the physical root instruction and apply the eliminated root-to-authority tail assignment when root and authority differ;
execute the authority-trigger instruction;
apply every ordered tail edge as a simultaneous typed assignment;
execute the selected register instruction;
continue through any no-op tail chain needed to reach the next physical selected atom; and
identify the exact continuation label and its live parameter homes.

Reference evaluation uses target operations and operands, not decoded instructions or raw template helpers. The candidate transition must match the reference expression at every continuation parameter word and must transfer control to the same label. Dead scratch homes are not compared.

5. Slice and coverage rules

Every register shared-join ingress owns exactly one checked slice. For the current composition the slice begins at the physical authority-trigger RegisterInstruction, includes the selected register instruction and its tail atom, and ends before the next semantic instruction atom. All included bytes are decoded once in atom order. The selected instruction and tail must have the exact ADR-0049 shared authority; the authority-trigger prefix must remain ordinary accepted policy-1.4 evidence.

The accepted BranchMix proof must cover exactly:

target 121 / root 106 / authority 107
target 121 / root 116 / authority 117

No label number is hard-coded into the decoder. These rows arise from the accepted composition and are asserted only as the frozen lighthouse vector.

6. Bounds and fail-closed behavior

The semantic decoder has checked ceilings for slices, decoded instructions, symbolic nodes, frame words, route events, and total work. Allocation is preflighted and fallible. One overflow, unknown form, route disagreement, semantic mismatch, or unused byte yields no partial semantic receipt and preserves the exact policy-1.4 selected artifact plus ADR-0049 structural evidence.

7. Accepted proof version boundary

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

The semantic receipt contains completeness, register-row, decoded-byte, decoded-instruction, symbolic-node, and reference-route-event totals. It is inside both the prospective realization hash and Gate B wrapper hash. Encoder policy 1.5 remains a separate later decision; proof acceptance does not authorize candidate selection.

Scope explicitly excluded

selecting, executing, loading, packaging, timing, or benchmarking the candidate;
a general x86-64 disassembler or formal ISA model;
fused-compare semantic migration beyond ADR-0049’s existing proof;
general register allocation, spilling, vectorization, or checked-array shared joins;
encoder policy 1.5, Gate B performance admission, Gate C, or P1; and
third-party proof or compilation dependencies.

Validation required before acceptance

deterministic discovery of both BranchMix target-121 register slices;
exact full-byte decode with no ignored prefix, suffix, or padding;
independent reconstruction of authority instruction, selected instruction, tail route, continuation, and live parameter homes;
typed symbolic equality for both F64-prefix variants and the shared I64 add/tail transition;
exact fallthrough into the downstream fused target;
semantics-changing opcode, immediate, displacement, ModRM register, load/store direction, operation, and instruction-order mutations fail closed; omitted, inserted, truncated, and trailing bytes fail exact decode;
wrong root, authority trigger, route event, continuation, parameter type, and atom-boundary evidence fail closed;
cap and arithmetic one-over cases yield no partial semantic evidence;
self-resealed candidate metadata cannot bypass fresh decoding;
policy-1.4 bytes and all target/native/process/standalone identities remain unchanged;
focused decoder/profile/raw tests plus full debug/release, strict, Clippy, format, and diff gates pass; and
an explicit ignored release-mode regenerative Gate B replay seals the migrated proof payload.

All twelve validation items are accepted for the bounded BranchMix proof. The frozen semantic receipt is:

register ingress rows              2
decoded candidate bytes          310
decoded machine instructions      42
canonical symbolic nodes          15
reference route events            25
candidate code hash       0e392caf51dbc65f9e36e08c678118e78b8f6aed90bf1df0edbf4b5c6a5f5173
Gate B realization hash   172b508e9648501162e28274afa3bcec0632f9cb3212e38f2b87b21ad7516198
Gate B schema-1.6 hash    ea0958fd4346c0a2a209b831633748709726e1ba23ee2712565f6d2be62722a5

Opcode/add-to-sub, immediate, live load/store direction, ModRM register, live instruction-order, and tail-destination mutations are rejected after the candidate code hash is recomputed. Unknown, truncated, and trailing machine forms, mistyped delayed values, budget one-over, and arithmetic overflow fail closed. Structural route, authority, partition, span, label, fixup, total, and hash adversaries inherited from ADR-0049 remain green.

Focused decoder 2/2, profile 5/5, Gate wrapper 1/1, debug and release workspace suites, strict refinement 8/8, 22 governance tests, Clippy with warnings denied, format, and diff checks pass. The explicit ignored release-mode regenerative Gate B seal passes 1/1 in 253.53 seconds. It regenerates the full 2,526,207,757-step profile and rejects a semantic counter mutation even after both nested hashes are recomputed.

Consequences

Positive

Register clone semantics become independent of encoder template identity.
Register residency and tail-copy schedules are checked as typed state transitions.
Candidate execution remains unnecessary before policy admission.
The proof stays NAUX-owned and narrowly bounded.

Negative

NAUX maintains a second small interpretation of selected x86 forms.
Symbolic routing duplicates some target semantic logic intentionally.
Unsupported but valid candidates fail closed until the decoder grows under a later decision.
Schema and heavy regenerative replay costs increase after acceptance.

Risks and mitigations

Decoder/encoder common bug: the decoder uses opcode parsing and symbolic execution rather than emission helpers or expected byte templates.
Dead-state false mismatch: only continuation parameter words and exact control are compared.
Hidden live state: continuation homes come from the verified target function signature, not a heuristic liveness pass.
Expression explosion: canonical nodes and hard work/node caps fail closed.
Premature policy admission: no decoded candidate becomes executable or selectable under this ADR.

Accepted implementation map

naux-lang/src/core/x64_target/prospective_semantics.rs: bounded decoder, typed symbolic machine, route reference, and unit/adversarial tests;
naux-lang/src/core/x64_target/profile.rs: invoke the independent gate while transient shadow bytes exist and require all register rows to pass;
naux-lang/src/core/x64_target.rs: private decoder module integration and public aggregate proof receipt export;
naux-lang/src/core/x64_gate_b_profile.rs: schema-1.6 canonical encoding, envelope validation, nested hashing, and regenerative seal.