compiler: W4-EFFECTS-1 slices E2–E5 — admissible effects, from the gate to real hardware - #630
Conversation
…keyed dropout its pathwise adjoint E2a, the gate. The blanket AUTODIFF_STOCHASTIC_EFFECT refusal conflated two independent questions: can the draw be REPLAYED, and can it be DIFFERENTIATED. They are now separate and each refusal names which failed — demonstrable on one op: the same dropout without a recorded product reports AUTODIFF_STOCHASTIC_NO_PRODUCT, and with one passes that gate to be judged on its adjoint instead. The gate stays fail-closed: absence of a product is refusal, not permission, so every program refused before is still refused. Admissibility is a property of the CALL FORM, not the op name — measured on tessera.dropout, whose three forms differ: `seed=N` replays bit-identically, ambient entropy does not, and a caller-owned generator does not because it ADVANCES per call and its position is not in the product. That third form is the one worth naming: it looks keyed and is not. `stochastic_product_for_call` admits the first and refuses the others by name, and a test pins those verdicts against the op's measured behaviour so the table cannot drift from reality. E2b, the adjoint. Under the declared constant_noise estimator the forward is y = x * m/(1-p), so the Jacobian is diag(m/(1-p)) — DIAGONAL, hence its own transpose — and the adjoint is the same operation applied to the cotangent: dx = dropout(dout, same key). It therefore mirrors DropoutOp::buildTangent rather than introducing a second formula (#31), and carries the same guard: an unkeyed training draw emits no adjoint, because the backward would otherwise apply a DIFFERENT mask than the forward and produce a plausible but wrong gradient. Verified exactly where exactness is the claim: J v == diag(m) v bitwise, the forward is exactly elementwise scaling by the mask, and the emitted adjoint equals the analytic pathwise rule bitwise. The pairing identity <Jv,u> = <v,Ju> is checked in float64, since two dot products over different vectors accumulate in different orders and bit equality there would be a statement about summation rather than about the operator. Two drift gates caught real omissions, which is what they exist for: the new diagnostics needed diagnostic_codes.py entries, and dropout had to be recorded in the native-adjoint ledger. Gates: IR lit 61/61 (E2a's obsolete no-adjoint case retired into the new adjoint fixture, so each file states one thing); 27 unit tests; full suite at the recorded environmental baseline with no new failure site; mypy 0; ruff clean; dashboards regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…lue; collectives bind order AND tree
E3, mutation. The precondition first: `state_buffer_lineage`'s `dtype` was a
hardcoded "f32", so the identity could not EXPRESS a bf16 or fp8 buffer and
mixed-precision recorded state would have aliased two materially different
buffers under one lineage id — which a mutation product binds, so the
aliasing would have reached replay. It is now a real parameter; f32/bf16/
fp8_e4m3/f64 give four distinct ids, and the "f32" default keeps every
lineage id built today byte-identical (81 existing stateful/optimizer tests
unchanged, so no package digest moves).
Then the core: a mutation product binds identity AND value — lineage id,
version, and a content digest — with `verify_recorded_state` rejecting the
case metadata identity is blind to, an unchanged id and version over CHANGED
bytes. The digest covers dtype and shape as well as bytes, so it separates a
reshape over identical bytes, an f32-viewed-as-int32 reinterpretation, and
+0.0 vs -0.0 — numerically equal, different bits, and (R) is bit-identity.
E4, ordered collectives. The product binds communicator, issue order,
reduction algorithm and topology. Order alone would not give (R): floating-
point addition is not associative, so the tree is part of the value, and the
test measures it — identical inputs under an identical issue order give three
different bit patterns for sequential, pairwise and ring reduction, with the
ring result changing again with rank count. LANGUAGE_AND_IR_SPEC section 11
requires exactly this ("fixed collective ordering and reduction trees"). The
verifier therefore rejects a permuted order AND a changed tree under an
identical order.
The order evidence comes from the real W5.4 mock-mesh executor rather than a
synthetic list, and the scope boundary is explicit in both code and tests:
this establishes ORDER. Bit-identity of a collective RESULT still requires
native deterministic evidence on real transport, which a mock mesh cannot
provide and which this slice does not claim.
Gates: 37 unit tests; full suite at the recorded environmental baseline with
no new failure site; mypy 0; ruff clean; audit-doc gate green; dashboards
regenerated. Plan updated (E1-E4 landed, E5 open) and all four backend queues
carry both sync keys, with ROCm's stating the native-RCCL limit explicitly.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…corded product to real hardware
The queue row's actual ask: one physical family carrying an admissible effect
end to end, with exact-device rows rather than a reference lane. The family is
keyed Philox RNG — the physical form of E1's keyed_rng class, and the reason
that class is admissible: a counter-based generator is a pure function of its
key, so the key IS the product.
Rows, on both hosts of this fleet:
* replay from the recorded product ALONE is bit-identical on gfx1151, and
separately on AVX-512;
* the SAME product gives identical bits on both targets AND matches the
algorithm's independent reference — so a recorded product is portable
evidence, not a per-target coincidence. If that ever diverges, every
cross-target replay claim built on this ABI is void, which is why the row
exists;
* non-vacuous: a product differing only in its counter produces a different
draw on both targets;
* confinement holds on the real artifact: the draw writes its declared result
and nothing else.
The launch is rebuilt FROM THE PRODUCT — key words and counter become the op's
operands — so a replay cannot smuggle in state the product does not carry.
Claim-integrity fix to my own row while writing it: the first version asserted
`execution_kind in ("native_gpu", "native_cpu")`, which would let a ROCm row
pass by falling through to a CPU lane and still report green. Each row now
asserts its EXACT kind per target; the ROCm path was confirmed reporting
native_gpu on the Radeon 8060S.
Scope, stated in code, plan and queues: correctness only (WSL, Decision #26a),
no timing claimed, and no NVIDIA or Apple row run or implied.
Gates: 5 exact-device rows; full unit suite at the recorded environmental
baseline with no new failure site; audit-doc gate green; ruff clean;
dashboards regenerated. Plan marks E1-E5 landed, closing queue order 2's
remaining item.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 59e5404bee
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…eck identity Four findings, all real. The first two were the same defect seen from two sides: admission was too weak, and it was implemented twice. P1 — the gate admitted an unverified carrier. `carriesKeyedRngProduct` checked only the class string and that the digest was 64 hex characters, so the fixture's own placeholder digest passed. The recorded product is supposed to be *evidence*, and evidence nobody checks is decoration. It is now a hash chain: supported schema, lowercase 64-hex digest, `sha256(payload) == digest`, and a payload that names THIS op and THIS effect class — so a fabricated digest, a payload-less digest, and a valid product copied from another operation are each refused with their own reason. The positive fixture now carries a payload generated by the real E1 carrier rather than a placeholder, which is what made the weakness visible in the first place. P2 — admission inside regions. `RegionAdjointInterface::isReplayable` rejected every non-pure op, so the same keyed dropout that E2 admitted at the top level failed with AUTODIFF_REGION_ADJOINT the moment it appeared in an `scf.if` body. The newly admitted family was admissible only in straight-line code, which is not a useful family. Rather than write a second check, the verifier moved into `SemanticEffects.cpp` and all three call sites — the paired pass, the structured region walk, and the structurized-CFG body walk — call it (#31). A nested-region fixture proves both directions: a verified draw differentiates and saves the predicate rather than redrawing it; the same nesting with a product naming another op is still refused, which is the teeth for the sharing claim. P2 — mutation identity. `verify_recorded_state` compared only the content digest, answering "do these bytes match" rather than "is this the same state at the same version". Zero-initialised optimizer state is the everyday counterexample: every lineage's first moment is the same bytes, so a replay reattached to the wrong buffer verified clean. Lineage and version are now required keyword arguments — no default, because a defaulted identity is the permissive answer to a semantic question (#21a) — and the two failure directions get separate messages. P2 — the paired pass no longer emits AUTODIFF_STOCHASTIC_EFFECT, so its metadata stops listing it and names the two codes it does emit. A listed code the pass cannot emit is a declaration with no producer, and it reads as "this family is still refused wholesale" (#29). The in-place `tessera-autodiff` pass still emits the old code and keeps it. Evidence, this box (Strix Halo, gfx1151 + Zen 5 AVX-512): lit tests/tessera-ir/ 414/414 phase_f4 (incl. the new fixture) 62/62 test_recorded_product.py 38 passed test_w4_effects_physical_family.py 5 passed, native_gpu/native_cpu unit -m "not slow" failure profile unchanged from the recorded baseline (fp8 20, apple 17, scheduled_matmul 3, wmma 1 = 41) scripts/check_generated_docs.sh 26 in sync Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
All four addressed in P1 — validate the payload before admission. You were right that the check was structural only, and the demonstration is embarrassing: my own fixture's placeholder digest passed it. P2 — admission inside regions. This one had more teeth than the finding suggested. P2 — mutation identity. Content-only comparison answered "do these bytes match", not "is this the same state at the same version". Zero-initialised optimizer state is the everyday counterexample — every lineage's first moment is byte-identical, so a replay reattached to the wrong buffer verified clean. P2 — pass metadata. Removed Evidence on this box (Strix Halo, gfx1151 + Zen 5 AVX-512): |
1 participant
Completes the admissible-effects plan (#628) on top of E1 (#629). Three commits, one per slice — reviewable independently in that order, or as the arc.
With E5, queue order 2's remaining item closes: mutation, keyed RNG and ordered collectives can now enter a differentiated region through a verified recorded product, while I/O and unkeyed draws stay closed by argument rather than by omission.
E2 — split the gate, and give keyed dropout its adjoint (
480f590d)The blanket
AUTODIFF_STOCHASTIC_EFFECTrefusal conflated two unrelated questions. They're now separate, and the compiler demonstrates it on one op: the same dropout without a product reportsAUTODIFF_STOCHASTIC_NO_PRODUCT(replayability), and with one passes that gate to be judged on its adjoint instead. The gate stays fail-closed — absence is refusal, not permission — so nothing that was refused before is admitted now.Admissibility turned out to be a property of the call form, not the op. Measured on
tessera.dropout:dropout(x, p, seed=N)dropout(x, p)dropout(x, p, rng=<generator>)The third is the one worth naming: it looks keyed and isn't. A test pins all three verdicts against the op's measured behaviour so the table can't drift from reality.
The adjoint (E2b): under
constant_noise,y = x·m/(1−p), so the Jacobian isdiag(m/(1−p))— diagonal, hence its own transpose — givingdx = dropout(dout, same key). It mirrors the existingbuildTangentrather than introducing a second formula (#31), and carries the same guard: an unkeyed training draw emits no adjoint, because the backward would otherwise apply a different mask and produce a plausible-but-wrong gradient. Verified exactly:J v == diag(m) vbitwise, and the emitted adjoint equals the analytic rule bitwise.⟨Jv,u⟩ = ⟨v,Ju⟩is checked in float64 — bit equality there would be a claim about summation order, not about the operator.E3 + E4 — bind the value, not the name (
bd58880a)E3, mutation. The precondition first:
state_buffer_lineage'sdtypewas hardcoded"f32", so the identity couldn't express a bf16 or fp8 buffer and mixed-precision state would have aliased. Now a real parameter — four dtypes, four ids — with thef32default keeping every existing lineage id byte-identical (81 existing stateful tests unchanged, no package digest moved).Then the core: a product binds identity and value, and
verify_recorded_staterejects unchanged-id + unchanged-version over changed bytes. The digest covers dtype and shape as well as bytes, so it separates a reshape over identical bytes, anf32-viewed-as-int32reinterpretation, and +0.0 vs −0.0 — numerically equal, different bits, and (R) is bit-identity.E4, collectives. Order alone doesn't give (R), and the test measures why: identical inputs under an identical issue order give three different bit patterns for sequential / pairwise / ring reduction, with the ring result changing again with rank count. So the product binds order and tree and topology. The order evidence comes from the real W5.4 mock-mesh executor, not a synthetic list — and the scope boundary is in the code: this establishes order; result bit-identity needs native transport.
E5 — the family reaches hardware (
59e5404b)Keyed Philox RNG, on both hosts of this fleet:
Claim-integrity fix to my own row: the first version asserted
execution_kind in ("native_gpu","native_cpu"), which would let a ROCm row pass by falling through to a CPU lane and still look green. Each row now asserts its exact kind; I confirmed the ROCm path reportsnative_gpuon the Radeon 8060S.Evidence
Exact-device rows on gfx1151 + AVX-512 · IR lit 61/61 · unit tests 37 for the ABI plus 5 device rows · full suite at the recorded environmental baseline with no new failure site across all four slices · mypy 0 · ruff clean · dashboards regenerated.
Two drift gates caught real omissions along the way, which is what they're for: the new diagnostics needed
diagnostic_codes.pyentries, anddropouthad to be recorded in the native-adjoint ledger.Not claimed
Correctness only (WSL, Decision #26a) — no timing. Collective result bit-identity still needs native RCCL evidence and is recorded as ROCm's open item. No NVIDIA or Apple row was run or implied; all four backend queues carry the E2/E3/E4/E5 sync keys with per-architecture outcomes.
🤖 Generated with Claude Code