docs: W4-EFFECTS-1 — scope the admissible-effects recorded-product ABI

[gstoner]

The scope-before-build deliverable for the last open item of queue order 2 — "one physical packet family with admissible effects." No code; this is the plan you asked for before implementation, with every load-bearing claim measured rather than assumed.

The criterion, stated explicitly

A recorded product π(E) is sound iff:

• (R) Reproducibility — replay equals the recorded execution bit-for-bit, not merely in distribution;
• (C) Confinement — E's write-set is contained in values π names.

Both halves are load-bearing: (R) alone admits an op that reproduces its own value while corrupting a neighbour's state; (C) alone admits an op that touches nothing but returns different numbers on replay. And both must be verifier-checked, not producer-asserted.

Per-class verdicts, each with its enabling fact measured

Class	Verdict	Why
Keyed RNG	Admissible	The S4 generator is counter-based, so a draw is a pure function of its key — (R) holds by construction
Mutation	Admissible, reusing state_buffer_lineage.v1	It already content-addresses version + parents; do not invent a second schema (#31)
Ordered collectives	Admissible, identity only	The required property is a total order, which the schedule authority now derives (#625/#626)
I/O	Not admissible	An external read is not a function of any recorded value — no π satisfies (R)
Alias-sensitive	Conditional	Admissible exactly when alias facts are known (W2.1 + #625)

Measurements (§5)

RNG — the facts §3.1 rests on: bit-identical replay (max abs diff 0.0); child streams distinct with max |corr| 0.032 inside the 3/√n = 0.047 noise band; zero collisions over 800 split/fold_in derivations; per-rank disjoint across 8 ranks; KS vs N(0,1) on 200k draws p = 0.55.

Mutation — a precondition found while scoping: the lineage identity separates version, shape, access, parents, role (each verified individually) but hardcodes dtype="f32" with no caller override. Nothing collides today since every lineage is f32, but mixed-precision recorded state (bf16 master weights, fp8 optimizer state) would alias two materially different buffers. That's the same defect class as the MegaMoE schedule-digest fix in #625, so it's listed as a precondition of the slice, not a follow-up.

Five slices

E1 product ABI + verifier → E2 keyed RNG (dropout) → E3 mutation on the existing lineage → E4 collective identity → E5 one physical family end to end on x86 + gfx1151. Acceptance bars are set at bit-identity of replay, which a distributional check cannot establish.

§6 lists what the plan refuses to do — notably, no gate is weakened to make a family fit, and mock execution never stands in for a multi-rank numerical claim.

Registered in the compiler README authority chain; test_audit_docs.py green (it caught a missing map link, which is now fixed).

🤖 Generated with Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 69165611b7

ℹ️ 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".

[gstoner]

All four fixed in 6e6fbc6. Two of them are corrections to the plan's own criterion — I stated (R) and then failed to apply it rigorously in exactly two places.

P1 (mutation binds metadata, not contents) — correct, and it defeats the criterion. _buffer hashes name/role/shape/dtype/version/access/parents and not contents, so two buffers with identical metadata and different bytes share a lineage id. A replay binding "version N" can bind different bytes and produce a different gradient — silently, which is precisely the failure the gate exists to prevent. The product now binds a content digest (or an immutable snapshot; a (lineage_id, version)-keyed immutable store is the alternative if snapshot cost bites), and E3 gains a negative test: bytes changed under an unchanged id+version must be rejected. The plan now says plainly that metadata identity is necessary and not sufficient.

P1 (collective reduction tree) — correct, and I've made it measured rather than argued. Floating-point addition isn't associative, so the tree is part of the value. Same 1024 f32 values, identical inputs, identical issue order:

reduction	result
sequential	-50370.79
pairwise tree	-50370.76
ring (8 partials)	-50370.758

Three distinct bit patterns, max gap 3.1e-2, and the ring result changes again with rank count. You're right that LANGUAGE_AND_IR_SPEC.md §11 already required "fixed collective ordering and reduction trees" — my first draft bound only the first half. π now binds the reduction tree/algorithm and topology; E4 fails closed on a changed tree; and bit-identity of a collective result is explicitly deferred to native deterministic evidence, since the mock cannot establish it.

P2 (README) — my bug. The insertion matched the first occurrence of the FORGE anchor, which was in the routing table, splitting the epilogue-fusion row into two malformed cells and pointing that question at the wrong plan. Routing row restored verbatim; the inventory entry moved to the inventory table.

P1 (backends) — added. Sync key W4-EFFECTS-1-2026-08-25 in all four queues with distinct outcomes: rocm and x86 follow-up-required as the two named E5 acceptance hosts (rocm owns the hardest class — native RCCL determinism), nvidia and apple follow-up-on-adoption with what each inherits (NCCL deterministic-algorithm selection; Apple's no-third-representation constraint).

Still no code and no device claim in this PR — it remains the scope-before-build deliverable.

🤖 Generated with Claude Code