compiler: W4-EFFECTS-1 slice E1 — the recorded-product carrier and its verifier

[gstoner]

First slice of the merged admissible-effects plan (#628): the carrier every later slice builds on. No pass is wired to it yet — that's E2.

The module encodes the criterion, it doesn't describe it

Each effect class declares the fields that make replay a function of the product, and both review corrections from the plan are required fields, not advice:

• recorded_mutation without a content_digest is rejected. The existing state_buffer_lineage identity hashes metadata and not contents, so binding "version N" alone lets a replay bind different bytes and produce a different gradient — silently.
• ordered_collective without a reduction_algorithm (+ topology) is rejected. Floating-point addition isn't associative, so the tree is part of the value; LANGUAGE_AND_IR_SPEC §11 already required fixed ordering and fixed trees.

io is not a reachable class — constructing one fails with the argument for why, so the closure lives in the code rather than only in prose.

Confinement is checked both directions: over-declaring is allowed (conservative, can't hide a stray write); writing something undeclared is rejected; classes that write nothing may not declare a write-set. Region-level totality keeps "admissible" from meaning "unchecked" — an effectful op with no product stays fail-closed, and a product naming an op that isn't on the path is equally rejected.

Verification beyond the unit assertions

Digest injectivity, combinatorially. 120 distinct objects across the three value-bearing classes → 120 distinct digests, zero collisions. This repo has now hit the shared-content-address failure twice (the MegaMoE schedule digest; the f32-only lineage), so I confirmed every field reaches the digest rather than trusting SHA-256 to be handed everything.

(R) demonstrated against the live S4 generator. Record a key, discard the values, rebuild the draw from the product alone, require bit identity — plus a negative showing a different product does not reproduce it, so the test can't pass vacuously. That's the acceptance bar the plan sets and one a distributional check cannot meet.

Gates

19/19 new tests · governance + audit-doc gates green · ruff clean · mypy 0 (476 files) · generated docs in sync · full unit suite 16,448 passed, environmental baseline unchanged — same four files as before (fp8 20, apple 17, scheduled_matmul 3, wmma 1), no new failure site. E1 is additive: one new module, one new test file.

Plan status updated: E1 landed, E2–E5 open.

🤖 Generated with Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2a3ccf95d1

ℹ️ 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 af909e9. The first is a real hole in the totality guarantee, and it fails in the more dangerous direction.

P1 (occurrence keying) — correct, and it breaks both ways. Keying by op name meant a region with two tessera.dropout calls rejected the second product as a duplicate; worse, set(effectful_ops) collapses the repetition, so one product satisfied both occurrences and an effect went unchecked — precisely what the totality check exists to prevent. Products now carry a required occurrence_id — reusing the region carrier's existing StructuredOperation.operation_id shape rather than inventing an identity — and the verifier keys by it. A repeated occurrence id in the requested set is itself rejected, since totality can't be checked against an ambiguous key. Pinned by a test with two dropout occurrences that asserts both failure directions.

P2 (deep immutability) — correct. A frozen dataclass only stops rebinding the field. product and its nested values are now MappingProxyType + tuples (the pattern schedule_object.py already uses), and — belt and braces — the digest is computed once at construction, so the content address cannot drift even if the freeze were somehow defeated. canonical_payload() thaws into fresh plain containers, so the copy a caller receives can't alias the carrier either. The test mutates at three depths and asserts the digest is unmoved.

P2 (scalar draw) — correct, including the inconsistency you spotted. () is the canonical scalar shape and rng.normal defaults to it, but the check tested membership in (None, "", ()) and so read a legitimate value as absent — while the JSON-equivalent [] passed. The check now tests absence (key missing / None / ""), and fields whose emptiness is meaningless (key, lineage_id, content_digest, communicator, sequence_digest, reduction_algorithm, topology) are listed per class and fail closed separately. () and [] now produce the same digest.

P1 (backend queues) — fair. All four said "plan only, no code", which went stale the moment E1 landed. Each now records its E1 outcome, and the honest one is no evidence: E1 is host-neutral Python that no backend surface consumes until E2, so rocm/x86 stay follow-up-required with that reason rather than claiming a parity they haven't earned; nvidia/apple are not-applicable-at-this-slice with what each inherits on adoption.

Gates: 23/23 · ruff clean · mypy 0 (476 files) · governance + audit-doc green · dashboards in sync.

🤖 Generated with Claude Code