gstoner · gstoner · Aug 25, 2026 · Aug 25, 2026 · Aug 25, 2026 · Aug 25, 2026
diff --git a/docs/audit/backend/apple/todo.md b/docs/audit/backend/apple/todo.md
@@ -7,6 +7,29 @@ last_updated: 2026-08-25
 ---
 
 # Apple compiler, exact-device, and performance plan
+Cross-backend sync `W4-EFFECTS-1-E5-2026-08-25` — **one physical family carrying an admissible effect, end to end; Apple outcome: not applicable — no row claimed.** As with NVIDIA: no M1 Max row was run and none is implied. The keyed-RNG class rests on counter-based purity, which holds on any target, so an Apple row is a matter of running it rather than of new design.
+
+
+Cross-backend sync `W4-EFFECTS-1-E4-2026-08-25` — **ordered-collective
+recorded products (identity only); Apple outcome: not applicable today.** The product
+binds communicator, issue order, reduction algorithm and topology; the
+verifier rejects a permuted order and a changed tree under an identical
+order. Order evidence comes from the deterministic mock-mesh executor.
+No Metal collective surface consumes this; no M1 Max evidence is implied.
+
+
+Cross-backend sync `W4-EFFECTS-1-E3-2026-08-25` — **shared state-lineage
+identity change; Apple outcome: not applicable today, inherited on
+adoption.** Same reason as the nvidia entry — host-side package identity, no
+Metal surface consumes it, no M1 Max evidence implied.
+
+
+Cross-backend sync `W4-EFFECTS-1-E2-2026-08-25` — **shared autodiff gate
+change (AutodiffPairedPass); Apple outcome: not applicable, no behaviour
+change.** Same reason as the nvidia entry — a target-neutral diagnostic split
+over a fail-closed gate. No Metal surface changes and no M1 Max evidence is
+implied.
+
 
 Cross-backend sync `W4-EFFECTS-1-2026-08-25` — **UPDATED 2026-08-25 (slice E1
 landed): shared recorded-product carrier + verifier implemented in Python;

diff --git a/docs/audit/backend/nvidia/todo.md b/docs/audit/backend/nvidia/todo.md
@@ -7,6 +7,33 @@ last_updated: 2026-08-25
 ---
 
 # NVIDIA compiler test-suite evaluation and rearchitecture
+Cross-backend sync `W4-EFFECTS-1-E5-2026-08-25` — **one physical family carrying an admissible effect, end to end; NVIDIA outcome: not applicable — no row claimed.** E5's physical acceptance was scoped to x86 + gfx1151 and executed there. No sm_120 evidence exists or is implied; an NVIDIA row would need its own exact-device replay on NR2 Pro, since no result transfers between architectures.
+
+
+Cross-backend sync `W4-EFFECTS-1-E4-2026-08-25` — **ordered-collective
+recorded products (identity only); NVIDIA outcome: not applicable today, inherited on adoption.** The product
+binds communicator, issue order, reduction algorithm and topology; the
+verifier rejects a permuted order and a changed tree under an identical
+order. Order evidence comes from the deterministic mock-mesh executor.
+When an NVIDIA collective family adopts recorded products it inherits the same requirement, and NCCL deterministic-algorithm selection becomes the gating evidence for any result claim.
+
+
+Cross-backend sync `W4-EFFECTS-1-E3-2026-08-25` — **shared state-lineage
+identity change; NVIDIA outcome: not applicable today, inherited on
+adoption.** The lineage is host-side package identity, not target codegen; no
+sm_120 artifact changes. Worth knowing when NVIDIA stateful packages adopt
+recorded products: the dtype field is now real, so a bf16 or fp8 optimizer
+state gets its own identity rather than aliasing the f32 one.
+
+
+Cross-backend sync `W4-EFFECTS-1-E2-2026-08-25` — **shared autodiff gate
+change (AutodiffPairedPass); NVIDIA outcome: not applicable, no behaviour
+change.** The pass is target-neutral and the change is a diagnostic split
+over a fail-closed check, so no sm_120 artifact or numerical result moves and
+no NVIDIA-owned surface needs revalidation. What NVIDIA inherits when a
+stochastic family is admitted on its lane: the same product requirement, and
+its own exact-device replay evidence.
+
 
 Cross-backend sync `W4-EFFECTS-1-2026-08-25` — **UPDATED 2026-08-25 (slice E1
 landed): shared recorded-product carrier + verifier implemented in Python;

diff --git a/docs/audit/backend/rocm/todo.md b/docs/audit/backend/rocm/todo.md
@@ -6,6 +6,41 @@ scope: ROCm backend implementation and exact-device proof
 ---
 
 # ROCm backend TODO
+Cross-backend sync `W4-EFFECTS-1-E5-2026-08-25` — **one physical family carrying an admissible effect, end to end; ROCm outcome: **parity VALIDATED, exact-device (gfx1151)**.** The keyed Philox RNG family executes its recorded product on the WSL-visible Radeon 8060S through `rocm_rng_compiled` with `execution_kind=native_gpu` asserted exactly, so the row cannot pass by falling through to a CPU lane. Replay from the product alone is BIT-IDENTICAL on device, a changed counter changes the draw (non-vacuous), and the same product matches the x86 result and the algorithm reference bit-for-bit. Correctness only — no timing is claimed on WSL, and the collective class's native-RCCL evidence remains separately open under the E4 key.
+
+
+Cross-backend sync `W4-EFFECTS-1-E4-2026-08-25` — **ordered-collective
+recorded products (identity only); ROCm outcome: follow-up required (owns the native evidence).** The product
+binds communicator, issue order, reduction algorithm and topology; the
+verifier rejects a permuted order and a changed tree under an identical
+order. Order evidence comes from the deterministic mock-mesh executor.
+STATED LIMIT: the mock establishes ORDER only. Bit-identity of a collective RESULT needs native RCCL deterministic-algorithm evidence on gfx1151, because floating-point addition is not associative and the reduction tree is part of the value (measured: identical inputs and identical issue order give three different bit patterns for sequential, pairwise and ring). No such claim is made here.
+
+
+Cross-backend sync `W4-EFFECTS-1-E3-2026-08-25` — **shared state-lineage
+identity change; ROCm outcome: parity validated, no behaviour change.**
+`state_buffer_lineage`'s `dtype` becomes a real parameter instead of a
+hardcoded "f32", so mixed-precision recorded state can no longer alias two
+materially different buffers under one lineage id. The default is "f32", so
+every lineage id built today is byte-identical and no package digest moves —
+verified by the existing stateful/optimizer suites (81 tests). Mutation
+products now additionally bind a content digest, which is new surface rather
+than a change to an existing one. No gfx1151 kernel or numerical result
+changes.
+
+
+Cross-backend sync `W4-EFFECTS-1-E2-2026-08-25` — **shared autodiff gate
+change (AutodiffPairedPass); ROCm outcome: parity validated, no behaviour
+change on this backend.** The blanket `AUTODIFF_STOCHASTIC_EFFECT` refusal is
+split into the two questions it conflated: REPLAYABILITY (does the op carry a
+`keyed_rng` recorded product?) and DIFFERENTIABILITY (does it have an
+adjoint?). The gate stays fail-closed — an op with no product is refused, and
+absence is not permission — so every program that compiled before still
+compiles and every program refused before is still refused, only with a
+diagnostic that names which question failed. Validated here: full IR lit
+suite 357 passed / 0 failed, autodiff paired + law suites 230 passed. No
+gfx1151 kernel, artifact, or numerical result changes.
+
 
 Cross-backend sync `W4-EFFECTS-1-2026-08-25` — **UPDATED 2026-08-25 (slice E1
 landed): shared recorded-product carrier + verifier implemented in Python;

diff --git a/docs/audit/backend/x86/todo.md b/docs/audit/backend/x86/todo.md
@@ -8,6 +8,34 @@ scope: x86 AVX-512 implementation/proof and AMX access planning
 ---
 
 # x86 backend TODO
+Cross-backend sync `W4-EFFECTS-1-E5-2026-08-25` — **one physical family carrying an admissible effect, end to end; x86 outcome: **parity VALIDATED (AVX-512 host)**.** Same family through `x86_rng_compiled` with `execution_kind=native_cpu` asserted exactly. Replay from the recorded product is bit-identical, and the cross-target row shows this host and gfx1151 produce the same bits from the same product.
+
+
+Cross-backend sync `W4-EFFECTS-1-E4-2026-08-25` — **ordered-collective
+recorded products (identity only); x86 outcome: parity validated (host-side analysis only).** The product
+binds communicator, issue order, reduction algorithm and topology; the
+verifier rejects a permuted order and a changed tree under an identical
+order. Order evidence comes from the deterministic mock-mesh executor.
+Nothing in the AVX-512 lane changes: this slice is host-side recording and verification with no kernel or numerical effect. The mock-mesh order evidence runs here.
+
+
+Cross-backend sync `W4-EFFECTS-1-E3-2026-08-25` — **shared state-lineage
+identity change; x86 outcome: parity validated, no behaviour change.** Same
+change as the rocm entry, and the same evidence: the f32 default keeps every
+existing lineage id byte-stable, so the AVX-512 stateful packages
+(Lion/Adafactor/sequence-mixer) keep their digests. The E3 content-digest
+binding is additive.
+
+
+Cross-backend sync `W4-EFFECTS-1-E2-2026-08-25` — **shared autodiff gate
+change (AutodiffPairedPass); x86 outcome: parity validated, no behaviour
+change on this backend.** Same gate split as the rocm entry; it is a
+diagnostic refinement over a fail-closed check, not a relaxation. Validated
+on the AVX-512 host with the same lit and autodiff suites. The Python-side
+call-form classifier that decides which draws may carry a product lives here
+too (`stochastic_product_for_call`), and its verdicts are pinned against the
+op's MEASURED behaviour rather than a convention.
+
 
 Cross-backend sync `W4-EFFECTS-1-2026-08-25` — **UPDATED 2026-08-25 (slice E1
 landed): shared recorded-product carrier + verifier implemented in Python;

diff --git a/docs/audit/compiler/W4_ADMISSIBLE_EFFECTS_PLAN.md b/docs/audit/compiler/W4_ADMISSIBLE_EFFECTS_PLAN.md
@@ -17,7 +17,26 @@ design and acceptance detail only.
 (`python/tessera/compiler/recorded_product.py`, tests in
 `tests/unit/test_recorded_product.py`): the carrier, its per-class (R)
 requirements, the (C) confinement checks, region-level totality, and the
-content address. E2–E5 remain open. Every claim below that could have been
+content address. **E2's gate half is landed too**: the blanket
+`AUTODIFF_STOCHASTIC_EFFECT` refusal is split into replayability
+(`AUTODIFF_STOCHASTIC_NO_PRODUCT` / `AUTODIFF_STOCHASTIC_UNKEYED`) and
+differentiability (`AUTODIFF_OP_NOT_DIFFERENTIABLE`), and
+`stochastic_product_for_call` admits only call forms whose replay is a
+function of recorded data — measured, not assumed: `dropout(x, p,
+seed=N)` replays bit-identically while the ambient and
+caller-generator forms do not. **E2b** (the dropout `AdjointInterface` that replays the mask from the
+product) is landed too: the Jacobian is `diag(m/(1-p))`, diagonal and
+hence its own transpose, so `dx = dropout(dout, same key)`. **E3 is
+landed**: `dtype` is a real parameter of the lineage identity (the
+measured precondition — the default keeps every existing lineage id
+byte-stable), and a mutation product binds lineage id + version + a
+**content digest**, with `verify_recorded_state` rejecting BOTH
+directions: changed bytes under an unchanged identity, and — since the
+PR #630 review — the right bytes under the wrong identity, because
+zero-initialised optimizer state makes distinct lineages byte-identical
+and a content-only check would call that replay faithful. The caller
+must name the lineage and version it is replaying; there is no default
+(#21a). **E4 is landed**: the product binds communicator + order + reduction tree + topology, the verifier rejects a permuted order AND a changed tree under an identical order, and the recorded order is taken from the real W5.4 mock-mesh executor rather than a synthetic list — with the scope boundary explicit in code and tests, that this establishes ORDER and that result bit-identity still requires native deterministic evidence. **E5 is landed**: the keyed Philox RNG family carries its recorded product to real hardware. Exact-device rows on BOTH hosts — replay from the product alone is bit-identical on gfx1151 and on AVX-512, and the SAME product gives identical bits on both targets and matches the algorithm's independent reference, so a recorded product is portable evidence rather than a per-target coincidence. Rows assert the exact `execution_kind` per target, so a ROCm row cannot pass by falling through to a CPU lane. Correctness only (WSL, Decision #26a); no timing claimed. **With E5, queue order 2's remaining item is closed.** The PR #630 review additionally moved recorded-product admission into one shared verifier (`recordedProductFailure` in `SemanticEffects.cpp`) called by the paired pass, the structured region replayability walk, and the structurized-CFG walk, so an admitted keyed draw stays admitted inside `scf.if`/`scf.for`/`scf.while` instead of failing `AUTODIFF_REGION_ADJOINT` — the family was previously admissible only in straight-line code (#31). Every claim below that could have been
 assumed was measured instead; the measurements are in §5.
 
 ---
@@ -176,10 +195,10 @@ first is deliberately the smallest one that exercises the whole ABI.
 | # | Slice | Deliverable | Acceptance |
 |---|---|---|---|
 | E1 | **Product ABI + verifier — LANDED 2026-08-25** | One `tessera.recorded_product.v1` carrier: effect class, content-addressed `π`, declared write-set. A boundary verifier checks (R)-inputs are present and (C) write-set ⊆ declared, failing closed with a named diagnostic per class. | Positive and negative fixtures per class; a product whose write-set exceeds its declaration is rejected; **no** class is admitted without a `π`. |
-| E2 | **Keyed RNG (dropout family)** | Split `AUTODIFF_STOCHASTIC_EFFECT` into *unkeyed* vs *no adjoint rule*; admit keyed draws with a registered rule; carry the key as `π`. | Replay of a recorded dropout region is **bit-identical** (not distributional); unkeyed still fails; the two diagnostics are distinguishable. Gradient checked against the analytic pathwise rule. |
-| E3 | **Mutation, on the existing lineage** | `dtype` becomes real in `state_buffer_lineage`; the product binds lineage id + version **+ content digest**; region replay reads the recorded version and the verifier checks the digest. | Bit-identical replay of a stateful step; a tampered version fails closed; **a buffer whose bytes changed under an unchanged lineage id + version is REJECTED** (the §3.2 correction, with a negative test); a mixed-precision lineage no longer aliases (§5.2). |
-| E4 | **Ordered collectives (identity only)** | Communicator + sequence digest **+ reduction tree/algorithm and topology** as `π`; replay issues the recorded order under the recorded tree. | Mock-mesh replay reproduces the recorded order exactly; a reordered sequence fails closed; **a changed reduction tree fails closed** even when order and inputs match. Bit-identity of a collective RESULT additionally requires native deterministic evidence on real transport (RCCL/NCCL) — the mock check cannot establish it, so E4 claims identity only and the numerical claim moves to E5/DIST-NATIVE-1. |
-| E5 | **One physical packet family end to end** | The queue row's actual ask: one family carrying an admissible effect through Schedule→Tile→target on x86 and gfx1151. | Exact-device rows on both hosts, bit-identical to the recorded execution; digests bound; no reference-lane fallback. |
+| E2 | **Keyed RNG (dropout family)** — gate split LANDED 2026-08-25; the adjoint (E2b) remains | Split `AUTODIFF_STOCHASTIC_EFFECT` into *unkeyed* vs *no adjoint rule*; admit keyed draws with a registered rule; carry the key as `π`. | Replay of a recorded dropout region is **bit-identical** (not distributional); unkeyed still fails; the two diagnostics are distinguishable. Gradient checked against the analytic pathwise rule. |
+| E3 | **Mutation, on the existing lineage** — LANDED 2026-08-25 | `dtype` becomes real in `state_buffer_lineage`; the product binds lineage id + version **+ content digest**; region replay reads the recorded version and the verifier checks the digest. | Bit-identical replay of a stateful step; a tampered version fails closed; **a buffer whose bytes changed under an unchanged lineage id + version is REJECTED** (the §3.2 correction, with a negative test); a mixed-precision lineage no longer aliases (§5.2). |
+| E4 | **Ordered collectives (identity only)** — LANDED 2026-08-25 | Communicator + sequence digest **+ reduction tree/algorithm and topology** as `π`; replay issues the recorded order under the recorded tree. | Mock-mesh replay reproduces the recorded order exactly; a reordered sequence fails closed; **a changed reduction tree fails closed** even when order and inputs match. Bit-identity of a collective RESULT additionally requires native deterministic evidence on real transport (RCCL/NCCL) — the mock check cannot establish it, so E4 claims identity only and the numerical claim moves to E5/DIST-NATIVE-1. |
+| E5 | **One physical packet family end to end** — LANDED 2026-08-25 | The queue row's actual ask: one family carrying an admissible effect through Schedule→Tile→target on x86 and gfx1151. | Exact-device rows on both hosts, bit-identical to the recorded execution; digests bound; no reference-lane fallback. |
 
 Estimated shape: E1 is the load-bearing one; E2 is the cheapest real proof;
 E5 is the row that lets queue order 2 close.

diff --git a/docs/audit/generated/autodiff_connection_ledger.csv b/docs/audit/generated/autodiff_connection_ledger.csv
@@ -87,7 +87,7 @@ dequantize_nvfp4,quantize,yes,none,none,,,,,,,,python_reference=python-unit-regi
 det,linalg_function,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,
 digamma,elementwise,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,
 div,elementwise,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,
-dropout,random_mask,yes,none,native,,,,,,,,python_reference=python-unit-registry;ir_tangent=llvm23-core,,,
+dropout,random_mask,yes,native,native,,,,,,,,python_reference=python-unit-registry;ir_adjoint=llvm23-core;ir_tangent=llvm23-core,native compiler adjoint,,
 dynamic_slice,indexing,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,
 dynamic_update_slice,indexing,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,
 ebm_energy_quadratic,ebm,yes,none,none,,,,,,,,python_reference=python-unit-registry,,,