feat(engine): PR-6.75 — C0-full+C1 read/write conflict profiler; sound CR 603.3b same-event trigger ordering

[lgray]

🤖 AI text below 🤖

Summary

PR-6.75 of the combo-detector series: C0-full + C1 precision pass — a typed read/write conflict-profile module (ability_rw.rs) and a CR 603.3b same-event trigger-ordering gate that is fail-closed over the profiled read/write sets (sound modulo two documented profile-invisible symmetric residuals — §8-R4), replacing the shipped fail-open allowlist with a fail-closed classifier. 13 commits, engine-only — 7 original, 5 review-response commits (all review findings from the 2026-07-04 rounds, §8), 1 rebase-adaptation (v0.15.0 new-variant exhaustiveness):

1. commit 1 — ability_rw read/write conflict profiler: per-ability typed read/write span extraction with a fail-closed dual-walk (every new enum variant/field must be explicitly classified per-axis or the build breaks — no wildcards).
2. commit 2 — C0-full + C1: the profiler becomes the trigger-ordering gate (CR 603.3b). Same-event path is monotone-safe: the old code unconditionally auto-ordered, so C1 can only ADD prompts, never remove one.
3. commit 3 — position-agnostic D5 legacy-ref visitor (CR 603.10a): typed, compiler-exhaustive visitor closing the fail-open hole where legacy event refs in effect TARGET/COUNT positions were missed (50 cards would have silently auto-ordered).
4. commit 4 — cheap read/write conflict levers (10 precision refinements; sweep 64→27).
5. same_controller — ControllerUniformity typed group property ({Mixed, Uniform, UniformAligned}; CR 805.7 team pools are the sole mixer; 27→24).
6. batch-hard — Batch-T1 uniformity theorem: controller-uniform + source-independent + no member-bound storage + no live-event read + no event-object write ⇒ f∘f idempotent ⇒ order-independent. Dodecapod is the counterexample proving mixed-controller batches are unclearable (executable negative test). 24→19.
7. sweep-green — full-DB parity sweep allowlist: 18 documented-conservative over-prompts + 1 genuine (Day of the Dragons), floors mutation-proven non-vacuous.
8. HIGH-1 fix (b4ec14aa9) — same-event member-bound discriminator (review finding 1; §8).
9. HIGH-2 fix (5f109132b) — non-phase delayed triggers routed through begin_trigger_ordering (review finding 2; §8).
10. rebase adaptation (41843f974) — v0.15.0 new-variant exhaustiveness classification for the dual-walk (§8).
11. R4 fix (53838b08b) — same-event event-object read/write feed closed (review round-4 finding; §8-R4).
12. R5 caller-level regression test (83bb4084a) — production-path group_is_order_independent pin for the R4 discriminator (review round-5 finding; §8-R5).
13. C2-ungating adoption + soundness conjunct (01580f3bf) — adopts perf(engine): batch identical self-counter triggers #5084's loop-detection ungating of C2 finite ordering and closes the Dodecapod under-prompt the ungating surfaced (§8-R5).

Files changed

• crates/engine/src/game/ability_rw.rs (new module, +7448)
• crates/engine/src/game/ability_scan.rs (+17)
• crates/engine/src/game/engine_priority.rs (+9)
• crates/engine/src/game/mod.rs (+1)
• crates/engine/src/game/triggers.rs (+414/−189)
• crates/engine/src/game/triggers_ordering_parity_tests.rs (new test module, +2138)
• crates/engine/tests/integration/daretti_emblem_simultaneous_death.rs (+11/−8 — updated to the new OrderTriggers contract, §8)

Track

Developer

LLM

Model: claude-opus-4-8
Thinking: high
Tier: Frontier

Implementation method (required)

• Produced via the /engine-implementer pipeline (plan → review-plan → implement → review-impl → commit)

Every commit in the series ran the full pipeline: signed-off plan (PR-6.75-C0FULL-C1-PLAN.md, 4-round plan review R1→R4-clean), per-commit implementer, per-commit adversarial /review-impl (each round's REQUIRED fixes applied before commit), plus one final cumulative adversarial review over the whole 7-commit diff (verdict: SHIP).

CR references

69 unique CR annotations in the series diff, every one grep-verified against docs/MagicCompRules.txt before writing. Load-bearing: CR 603.3b (APNAP trigger ordering — the seam this PR fixes), CR 603.4 (intervening-if re-check), CR 603.10a (delayed/legacy refs), CR 805.7 (team trigger pools = the sole controller-mixer), CR 701.21a (sacrifice → owner's graveyard, the osseous/skyfisher class), CR 303.4d + CR 301.5c (Aura/Equipment can't attach to itself — §L6), CR 120.4a (excess damage → PlayerLife write), CR 608.2h, CR 704.5a/g/j, CR 904.3. One wrong pre-existing citation found by the cumulative review was fixed in-series (§L6: 701.3d/704.5j → 303.4d/301.5c).

Verification

Developer-track checklist for this head (01580f3, rebased onto upstream/main cf7cd7c):

• cargo fmt --all — clean
• cargo clippy --workspace --exclude phase-tauri --all-targets --features engine/proptest -- -D warnings — clean, 0 lints (re-run at 01580f3)
• ./scripts/check-parser-combinators.sh — clean (no parser files in the diff)
• cargo test -p engine --features proptest — 0 failures at 01580f3 (engine lib 15103 pass / 0 fail + all integration binaries pass)
• Corpus regenerated at 01580f3 (provenance client/public/card-data-meta.json); 0 new Unimplemented entries (this PR adds no parser surface)
• FORGE_TEST_FULL_DB=1 cargo test -p engine ordering_parity_sweep — GREEN: 0 unexplained at the rebased head (details below)

Commands run at this head (01580f3) — three rebases during review-response, each verified by range-diff: onto 1badc19 (9/9 = modulo one benign use-line 3-way with #4625) + one adaptation commit (§8); onto 4c0ac54 (11/11 =, pure base-move); onto cf7cd7c (conflict resolution with #5084 — 10/12 =; commit-2 ! = the C1 conflict resolution keeps the commit's own gated form, re-applied as the tail ungating commit so HEAD adopts #5084; HIGH-2 ! = context-line only from #5084's visibility bump; §8-R5). No dual-walk exhaustiveness breaks in any rebase after the adaptation commit (#5090 adds no enum variant):

Command	Result
FORGE_TEST_FULL_DB=1 cargo test -p engine ordering_parity_sweep (corpus regenerated at 01580f3, incl. #5080/#5090 parser changes)	GREEN: 0 unexplained over swept=13556 / compared=6208; over_prompt_hit=18, batch_genuine_hit=1 (Day of the Dragons), cat1_hit=6, se_mb_genuine=6 (§8 exact-set assert), se_member_bound_class=43 (predicate-derived, floor ≥35), se_event_object_class=13 + SAME_EVENT_EVENT_OBJECT_GENUINE={} (§8-R4, empty exact-set asserted, floor ≥9, disjointness vs member-bound asserted); all floors pass, t1_source_indep=2820 (assert ≥2727). Zero movement across all three rebases — both upstream parser changes measured corpus-neutral; the C2-ungating is off the sweep's profiles_conflict path (predicted AND measured)
Mutation probe matrix M1–M9 (flip one classifier conjunct → full-DB sweep → confirm the named floor/assert trips → revert; run at the pre-review-fix tree)	every surviving floor and ledger assert has ≥1 discriminating mutation; M4 surfaced 50 under-prompt-direction rows, 0 suppressible — the direction gate cannot be masked by the allowlist. §8's new class floor has its own mutation proof: deleting the HIGH-1 discriminator collapses se_member_bound_class 43→0 and trips the floor + the genuine exact-set assert
cargo clippy --workspace --exclude phase-tauri --all-targets --features engine/proptest -- -D warnings	0 lints (at 01580f3)
cargo test -p engine --features proptest	0 failures (at 01580f3: engine lib 15103/0 + all integration binaries)
cargo fmt --all / parser-combinator gate vs true base	clean / no parser files in the diff

Behavioral trace of the trigger-ordering seam: begin_trigger_ordering collects the same-event batch → partitions by controller (CR 805.7 team pools are the only path that mixes controllers; condition1_dodecapod_mixed_controller_still_prompts pins that mixed groups always prompt) → group_is_order_independent consults the ability_rw read/write profiles → any read/write span conflict ⇒ prompt (player orders, CR 603.3b); provably-disjoint spans ⇒ auto-order. Monotone safety: the pre-C1 path unconditionally auto-ordered same-event groups, so C1 can only ADD prompts — it cannot remove one.

Under-prompt proof (the #1 risk): the sweep's direction gate flags decision_old && !decision_new (previously-prompted → now-auto) rows into unexplained, which is asserted empty — an allowlist entry cannot hide an under-prompt by construction. The 7 newly-prompting category-1 cards are each measured genuinely order-dependent (table below); the 18 conservative over-prompts are documented with per-card reasons and completeness-asserted at full-DB. Discriminating runtime pins: b2_dotd_member_bound_pin, b1_mindslicer_uniformity_gate, the Dodecapod executable negative, freeze-auto discriminators N-A/N-B, and a mechanical 12-tag×position exhaustiveness matrix for the D5 visitor.

Rules correctness (CR 603.3b)

Per the 2026-07-03 maintainer/user ruling: C1 ships UNGATED — it is a bug fix on the always-on legacy ordering path (the gated feature remains C2 from #4904/#4603). Rationale: rules correctness is the project's primary concern; the pre-C1 path could silently auto-order genuinely order-dependent same-event triggers (under-prompt = rules-wrong). C1 is a strict tightening: the direction gate in the parity sweep (decision_old && !decision_new) proves no card auto-orders under C1 that prompted before, and the 6 newly-prompting cards (+1 parse-blocked, table below) are measured genuinely order-dependent.

§7 Full-DB parity sweep: final accounting (sweep GREEN)

Honesty correction: step-4 found 0 genuine at SAME-EVENT depth; commit-6's deeper BATCH analysis reclassified Day of the Dragons as genuinely order-dependent. The earlier "0 genuine among the 64" statement was correct for the same-event analysis it was made under and is superseded — not silently revised — by the batch-depth result. D3's zero-widening premise did not hold at full-corpus scale.

Arithmetic: the pre-allowlist full-DB sweep panicked at exactly 19 unexplained rows: 19 = 18 documented-conservative (17 same-event + 1 batch [Skyfisher Spider]) + 1 GENUINE (Day of the Dragons, batch). Skyfisher Spider and Day of the Dragons are both batch-arm diffs but land in DIFFERENT categories: skyfisher's prompt is conservative (owner-misalignment / osseous-class — its owner-ALIGNED co-departure is genuinely auto-safe via sum-symmetry [both the total 2N−1 and the per-copy multiset {1..N} are order-invariant, so even an intermediate "whenever you gain life" observer is order-blind], while the owner-MISaligned case IS order-observable but is correctly prompted by production — see the ledger), DotD's prompt is correct (order genuinely observable even when fully aligned). After allowlisting, the sweep reports 0 unexplained and is GREEN.

Measured at the pre-fold series tip (FORGE_TEST_FULL_DB=1): swept=13543 compared=6206; the four surviving floor metrics plus the removed srcread's measurement {srcread=0, obs=494, hadcounters=1, retained=285, t1=2871}. Re-measured after rebase onto current main with a corpus regenerated at the rebased tip (provenance: client/public/card-data-meta.json, generator-stamped): zero drift on every gated metric (swept +4 benign corpus growth, t1 −1 with 143 floor margin).

Intended prompts (category 1) — same-event genuine (6 measured flips + 1 parse-blocked) + batch genuine (1):

Card	Depth	Order-dependence proof (one line)
ouroboroid	same-event	each copy's Power{Source} read is fed by the other's PutCounterAll
docent of perfection	same-event	token write feeds the shared census threshold — which copy transforms depends on order
sidequest: hunt the mark	same-event	token write feeds the shared census threshold
promise of tomorrow	same-event	first copy's mass return flips the second's CR 603.4 re-check
spawn of mayhem	same-event	damage order across the 10-life threshold decides which copy gets the counter
complex automaton	same-event	ObjectCount{Permanent} intervening-if read × self-Bounce census overlap
your inescapable doom	same-event (parse-blocked)	proven order-dependent in-plan; current parse degrades its counter feed to Any so the sweep never forms its group (expected-UNHIT, asserted)
day of the dragons	batch	LTB Sacrifice{Dragons, count: ObjectCount} → ChangeZone{TrackedSet(0) → battlefield}: each member returns its OWN tracked set and the returned creatures can be Dragons the other member's re-sacrifice consumes (CR 603.3b) — pinned at runtime by b2_dotd_member_bound_pin

Documented-conservative over-prompt ledger (18) — mirrors DOCUMENTED_OVER_PROMPT in triggers_ordering_parity_tests.rs (the source of truth; every entry completeness-asserted at full-DB):

• L8-held (12), monotone/self-limiting intervening-if (CR 603.4): chorale of the void, deathbonnet sprout, death of a thousand stings, exile into darkness, glimmer seeker, graf rats, mirror-sigil sergeant, persistent marshstalker, reclusive wight, reveille squad, stensia uprising, stillness in motion. The L8 idempotence recognizer is deliberately NOT built: a wrong recognizer under-prompts (rules-wrong); a conservative prompt is fail-closed (rules-correct).
• Owner-keyed read × owner-misaligned write (1): osseous sticktwister (CR 701.21a: sacrifice goes to the OWNER's graveyard; a control-changed permanent you own makes the write-span Any).
• Context-free-unclassifiable singletons (2): paroxysm (revealed-card read indistinguishable from a board read in the AST), flamewake phoenix (commutes only via runtime source power 2 < 4).
• Parse-blocked commutes (2): deep-sea kraken, ichorplate golem (both commute underneath; the mis-parse hides the structure).
• Owner-misalignment / osseous-class, batch (1): skyfisher spider — the owner-ALIGNED co-departure is auto-safe via sum-symmetry (total AND per-copy multiset {1..N} order-invariant); the owner-MISaligned case is order-observable (an opp-owned copy dies to its OWNER's graveyard, CR 701.21a/404, so its self-exile no-ops on your gy count) but is correctly prompted by the same count-read × graveyard-write conflict — no under-prompt. Same owner-misalignment meta-class as osseous; the aligned-safety sub-mechanism (sum-symmetry) is distinct from osseous's write-doesn't-feed-read.

Floors: re-tuned to full-DB measured values minus 5% corpus-churn tolerance (batch_obs 494 → ≥469, retained_prompt 285 → ≥271, t1_source_indep 2871 → ≥2727, hadcounters_batch_self ≥1 witnessed by Promising Duskmage); batch_self_srcread REMOVED — its cell is empty in-corpus (its old ≥40 population was an artifact of the D5 fail-open hole that commit 3 closed; that freeze-auto class is now counted by retained_prompt, and the freeze-auto behavior is pinned by unit discriminators N-A/N-B). Every surviving floor and every ledger entry is mutation-proven non-vacuous (review probe matrix M1–M9: each mutation flips one classifier conjunct → full-DB sweep → the named floor trips or the named assert fails; M4 additionally proved the direction gate — 50 under-prompt rows surfaced, 0 suppressible).

§8 Review-response (maintainer CHANGES_REQUESTED, 2026-07-04) — two HIGH findings closed + rebase onto v0.15.0

Two [HIGH] maintainer findings were addressed as new commits, then the whole 9-commit series was rebased onto the current upstream/main (v0.15.0+, 1badc1920). The full-DB parity sweep was regenerated and re-run at the rebased head and is GREEN (0 unexplained).

HIGH-1 — same-event member-bound trigger-ordering discriminator (commit b4ec14aa9, CR 603.3b / 603.10a)

profiles_conflict's same-event fast path auto-ordered any source_independent group, but a group of DISTINCT sources whose identical resolution reads per-source bound storage (CR 603.10a look-back — TrackedSet / ExiledBySource / ChosenCard, via member_bound_target_filter) is NOT one shared f(state): member A reads A's storage, member B reads B's, so the identical-function commutation proof breaks and the order can be observable. Since same-event order-independence is decided solely by !same_event_conflict (no c2 backstop), this auto-ordered genuinely order-dependent groups. Fix mirrors the batch path's !reads_member_bound conjunct at same-event depth: exclude member-bound from the fast-path disjunct + add the fail-closed discriminator if s.same_event && p.reads_member_bound { return true }. all_same_source stays auto-ordered (shared storage ⇒ f_A = f_B); the batch path is byte-inert.

NOT latent — the sweep caught it. The fix flips 48 same-event cards auto→prompt (all over-prompt direction — the base engine auto-ordered every same-event group unconditionally, so these can never be under-prompts). Split:

• 6 GENUINE same-event order-dependence (a NEW honesty category, SAME_EVENT_MEMBER_BOUND_GENUINE, exact-set asserted): mimic vat, mirror of life trapping (imprint-contention — two copies race to imprint the ONE shared triggering creature into their per-source pile, CR 603.10a); moonring mirror, duplicity (hand-swap re-capture — each copy exiles the shared hand into its own pile then returns its prior pile, A feeds B); world queller (shared-pool consumption under per-copy-divergent chosen types, CR 701.21 — genuine on rules grounds; its reads_member_bound bit comes from a non-obvious AST carrier, not the surface IsChosenCreatureType); blood tyrant (genuine via a DIFFERENT axis — a PutCounter{SelfRef} self-write whose per-copy split is order-observable when a player hits 0 life between resolutions, CR 704.5a/800.4a; caught incidentally by the member-bound discriminator).
• Conservative over-prompt CLASS (member-bound but order-immaterial: disjoint per-source referents, same controller optimizes both). Documented as a predicate-keyed class in the sweep (se_member_bound_class, keyed same_event ∧ reads_member_bound ∧ auto→prompt — the discriminator's own gate), NOT a per-card allowlist: membership is DERIVED + emitted as an evidence artifact, so it is robust to corpus churn. Measured 43 at the rebased corpus (was 42 pre-rebase; the +1 is ichormoon gauntlet, a ChooseCounterKind/PutChosenCounter card the v0.15.0 parser newly surfaced — a conservative counter-add, order-immaterial). A predicate-keyed class was chosen precisely so a corpus-churn member-bound card auto-absorbs without a manual allowlist edit; a 48-name allowlist would have broken the completeness assert at exactly this rebase.

Class floor se_member_bound_class ≥ 35 (mutation-proof: deleting the discriminator collapses it to 0). t1_source_indep measured 2871→2830→2831 (the source-independent slice of the class now prompts instead of auto-ordering; assert ≥2727 unchanged, still passes — an accounted movement, not a floor bump).

HIGH-2 — non-phase delayed triggers routed through the CR 603.3b ordering gate (commit 5f109132b, CR 603.3b / 603.7)

check_delayed_triggers (CR 603.7) APNAP-sorted its firing batch then DIRECTLY dispatched, bypassing begin_trigger_ordering — so two+ simultaneous same-controller order-dependent non-phase delayed triggered abilities reached the stack in fixed order with no CR 603.3b ordering choice. Pre-existing (byte-identical base↔HEAD); this PR made begin_trigger_ordering the sound authority but never wired this path. Fix routes the to_fire batch through begin_trigger_ordering (the phase-delayed path is the template), preserving every delayed-specific disposition (Good King Mog, Breeches reflexive pause, epic, multi-fire) via the shared Delayed-origin dispatcher, plus one engine_priority guard to surface the OrderTriggers prompt. Pure tightening: singletons and provably-commuting identical no-input groups still auto-order. One integration test (daretti_emblem_simultaneous_death) asserted the old direct-dispatch contract for two distinct-target simultaneous returns and is updated to a positive OrderTriggers pin.

Issue #4809 (Braids/Spinal Embrace) is a DISTINCT phase-path seam, not this bug — AtNextPhase{End} is phase-classified and already merged+ordered by the phase path (proven by the existing #5048 test); HIGH-2 neither closes nor regresses it. (Separate empirical follow-up.)

Rebase onto v0.15.0 — new-variant exhaustiveness (single adaptation commit 41843f974)

The rebase surfaced 6 new upstream enum variants in the wildcard-free ability_rw dual-walk, all classified per rw-axis with grep-verified CRs (full table in the adaptation commit body): FilterProp::InTrackedSet (member-bound — chain tracked-set membership), Effect::EachSourceDealsDamage (CR 120), ChooseCounterKind/PutChosenCounter (member-bound, per-source chosen counter, CR 122.1/122.6), CreatePlaneswalkReplacement (deferred body), ChaosEnsues (CR 311.7). Corpus regenerated at the rebased head; sweep re-run GREEN.

Convention note (vs the pre-PR rebase): the earlier pre-PR rebase folded its 15 new-variant arms into their owning profiler commits (per-commit-compiles). This rebase's arms could NOT be folded that way — three of them depend on engine features born LATER in the series (CreatePlaneswalkReplacement uses pscope/chain_move_owner/the 4-arg rw_effect signature from the same_controller commit; ChooseCounterKind/PutChosenCounter set reads_member_bound from the batch-hard commit), so folding would require deliberately-wrong evolving stub arms across three commits. They ship as one honest adaptation commit instead. Per-commit-compiles for c1–c8 was already forfeited by the rebase itself (non-exhaustive vs the new base by construction); the sound bisect build points are the base and HEAD. This is measured necessity, not a convention lapse.

Corrected arithmetic at the rebased corpus (b76c53274962cbf0): the same-event member-bound bucket = 43 conservative + 6 genuine; the original batch/same-event ledger (18 over-prompt + 6 cat-1 + 1 DotD genuine) is unchanged. Sweep: swept=13556 compared=6208 unexplained=0.

§8-R4 Review-response (round 4) — same-event event-object feed CLOSED

The round-4 [HIGH] — the same-event gate was not fail-closed for the event-object read/write feed — was accepted (option 1: close the feed) and fixed as commit 53838b08b, then the full series was rebased onto 4c0ac54f5.

The gap: read_object_scope maps EventSource/EventTarget reads to reads_event_live, a bare bool with no KindSet, so the feeds() kind×kind matrix was structurally blind to a writes_event_object mutation feeding an event-object live read (CR 608.2h — the read uses the object's current information). Same-event members share ONE live event object, so a member's write is observed by a sibling's live read ⇒ order-observable. The batch path was NOT holed (asymmetry, not a symmetric miss): a co-departure batch event object has DEPARTED and is frozen LKI (CR 603.10a) — a write no-ops or trips the freeze-invalidation row.

The fix (CR 603.3b / 608.2h): new shared predicate reads_and_writes_event_object() = reads_event_live && writes_event_object.any() — a conjunction, derived not copied (the batch guard is a disjunction-of-negations because refusing a fast path only defers; a prompt-returning discriminator must witness a real feed = both endpoints). Same-event T1 fast-path source_independent branch gains the exclusion; new discriminator if s.same_event && s.event_object_present && reads_and_writes_event_object() { return true } after the member-bound row. Gated on event_object_present (mirrors effective_external: a write to a non-present event object no-ops per targeting.rs, so Phase-mode triggers stay auto — the gate can only drop vacuous prompts, zero under-prompt risk). all_same_source stays auto (identical f over one shared object); both edits s.same_event-guarded ⇒ batch byte-inert.

Sweep: +13 same-event flips, all over-prompt direction, 0 GENUINE (SAME_EVENT_EVENT_OBJECT_GENUINE ships EMPTY, exact-set asserted; se_event_object_class=13, predicate-keyed, membership derived + emitted, floor ≥9 mutation-proof, disjointness vs se_member_bound_class asserted). Governing theorem (why R4 has 0 genuine where R3 had 6): every R4 write targets the SHARED event object — k identical fs on one shared object compose to the same final state under every permutation (relabel-invariant) — while R3's genuine members wrote to PER-SOURCE storage (imprint pile A ≠ pile B), an order-divergent destination. The 13: 7 frozen-context reads (EventContextAmount/EventOutcomeWon — a write cannot feed a frozen amount), idempotent shared-object writes (untap/exile/destroy, CR 701.26a/26b/608.2b), additive-commutative counters. Per-card both-orders traces in the classification artifact. sidequest: catch a fish sits OUTSIDE the class by the event_object_present conjunct (Phase-mode, no live event object, write provably no-ops) — excluded, not missed.

Claims-consistency (the R4 failure mode was a doc-vs-code gap): the module doc now records the direct event-object feed as CLOSED at both depths, and enumerates the two residuals that REMAIN — the source-actor granted-state channel and a board-wide writes_external × event-live-read channel — both SYMMETRIC across batch and same-event depths. The group_is_order_independent contract comment now states exactly this: never auto-orders order-dependence visible in the profiled read/write sets; sound modulo two profile-invisible symmetric residuals.

Second rebase (onto 4c0ac54f5): pure base-move, all 11 commits = in the range-diff; no new enum variants ⇒ no dual-walk breaks. #5088 (World-rule SBA, CR 704.5k) implements the rule cited for winter's night's practical unreachability — explicitly re-verified: the sweep uses structural reachability, winter's night remains a class member. Sweep at the fresh corpus: zero movement on every count vs pre-rebase.

§8-R5 Review-response (round 5) — caller-level regression test + C2-ungating adoption

R5-1 (the round-5 [HIGH], commit 83bb4084a, test-only): a production-path regression test now pins the R4 discriminator at the group_is_order_independent CALLER level (where event_object_present is threaded from the real pending trigger event) — distinct sources on one shared event object with an EventSource/EventTarget live read + a TriggeringSource event-object write ⇒ NOT order-independent; guard cases (read-only ⇒ auto, write-only/no-event-object ⇒ auto, all-same-source ⇒ auto) prove the discriminator rather than a blanket prompt. Revert-to-red measured at the caller level: disabling the discriminator reds the positive case.

R5-2 (commit 01580f3bf): adopting upstream #5084's C2-ungating surfaced a LATENT SERIES BUG, now fixed. #5084 removed the loop-detection gate from the C2 finite-ordering term (maintainer rationale: loop detection governs infinite-combo shortcutting, not finite CR 603.3b ordering UX). Applying it verbatim turned two of this series' own discriminating NEGs red (condition1_dodecapod_mixed_controller_still_prompts, b1_mindslicer_uniformity_gate): the coarse ability_scan-computed C2 term is structurally blind to the source-actor residual, and as a disjunct it could OVERRIDE the precise batch/uniformity prompt for a Mixed-controller co-departure — a genuine under-prompt (the Dodecapod cause-source-controller channel). This was latent in the series all along (reachable only under loop-ON, which the NEGs never exercised); the ungating made it default-path. Fix: the C2 term becomes c2_order_independent && !batch_conflict — a precision-dominance rule (the coarse walker may auto-order only when the precise profiler agrees). This is NOT a revert of #5084: the loop-ungating stands, and #5084's own pr625_c2 fan-out behavior is preserved (its group has batch_conflict=false); review-impl confirmed the conjunct is sound everywhere (a real co-departure batch never reaches the C2 term; for non-co-departure groups the conjunct is strictly more conservative). Revert-to-red: the bare c2 form re-reds both NEGs; the conjunct form is 5/5 green.

Third rebase (onto cf7cd7cb9, resolving the #5084 conflict): range-diff 10/12 =; commit-2 ! = the C1 conflict resolution retains that commit's own gated form with the ungating applied at the tail commit (HEAD adopts #5084); HIGH-2 ! = context-line only (visibility bump). #5084's stack.rs self-counter batching was classified orthogonal to the gate (resolution-time, same-source, checkpoint-proven sequential-equivalent — triggers are already ordered before they reach the stack). #5090 adds no enum variant; corpus regenerated; sweep zero-movement (table above).

Review summary

• Cumulative adversarial review over the whole series diff: SHIP — no new under-prompt exists (direction gate provably routes any under-prompt to the asserted-empty unexplained); ~50 CR annotations grep-verified in review; one CR-citation nit fixed in-series (§L6 now cites CR 303.4d "an Aura can't enchant itself" + CR 301.5c "an Equipment can't equip itself").
• R3 review-response (§8): both HIGH fixes ran the full pipeline (HIGH-1: classification verdicts → impl → adversarial review-impl APPROVE, both edits independently revert-to-red; HIGH-2: plan → plan verification → impl → review-impl APPROVE, Paused/Breeches idempotence proven by construction + 4 named discriminating tests; §F runtime revert-to-red pins prompt AND post-order resolution).
• R4 review-response (§8-R4): full pipeline (derived-shape checkpoint → impl → sweep + per-card classification → adversarial review-impl APPROVE 13/13 with claims-consistency as an explicit checklist item; discriminator revert-to-red measured).
• Follow-up filed: ci: wire the FORGE_TEST_FULL_DB trigger-ordering parity sweep into a CI/release gate #5073 — wire the FORGE_TEST_FULL_DB sweep into a CI/release gate (default CI runs the fixture subset only).

Combo-detector series

Pos	PR	Delivers
PR-0	#4092	ResourceVector + modulo-resource loop equality (additive).
PR-1	#4097	Analysis sim harness feeding ResourceVector.
PR-2	#4119	Net-progress detect_loop → LoopCertificate + corpus harness.
PR-3	#4480	Live mandatory-loop winner shortcut (drain-cascade, CR 704.5a).
PR-4a	#4493	Engine B static ability-graph extractor (scaffold + 5 families + SCC).
PR-4b	#4534	Engine B effect/trigger breadth + life-symmetry cost.
PR-5	#4547	cargo combo-verify CLI over the 53-row corpus.
PR-6	#4603	∞ unbounded-resource display — generalize infinite-mana to the whole ResourceAxis class (engine-owned DerivedViews projection).
PR-6.25	(deferred R3)	Order-independence soundness fix for group_is_order_independent (latent CR 603.3b). Notes: PR-6.25-DEFERRED-FINDINGS.md.
PR-6.5	#4904	Growing-cascade detector for multiplayer win-acceleration (ω-coverability modulo growth) + C0 fail-closed walker + C2 gated order-independent auto-resolve. Notes: PR-6.5-EPIC-GROWING-CASCADE.md.
PR-6.75 (this PR)	—	C0-full + C1 precision pass — ability_rw read/write conflict-profile module, latent CR 603.3b same-event fix, ungated per maintainer ruling.

Predecessor: PR-6.5 — #4904 — #4904 — delivered the C0 fail-closed walker skeleton and the C2 gated auto-resolve; this PR completes C0 to full read/write profiling and ships C1, turning the walker's classifications into the sound same-event ordering gate.

Related: #4603 (C2 gating policy), #4990 (S07 series whose subject_slot field is classified member-bound here).

Scope Expansion

None.

Validation Failures

None.

CI Failures

None.

🤖 Generated with Claude Code

[gemini-code-assist]

Warning

You have reached your daily quota limit. Please wait up to 24 hours and I will start processing your requests again!

[matthewevans]

Holding this head for required review evidence before any approval/enqueue decision.

This is a large hot-path engine change (ability_rw + trigger ordering), the current-head CI/card-data evidence is still pending, and the PR packet currently has proof_gap=true because the AI-contributor proof/template sections are missing. Please add the concrete proof for this head: commands/checks run, the behavioral trace for the trigger-ordering seam, and the discriminating tests/sweep evidence that prove the new gate does not under-prompt. I will not enqueue from this sweep until that evidence is present and current-head checks/parse-diff evidence have had a chance to populate.

[lgray]

🤖 AI text below 🤖

@matthewevans Evidence added for this head — the PR body now carries the required template sections:

• Implementation method: full /engine-implementer-pipeline per commit (plan → 4-round plan review → implement → per-commit adversarial review-impl) + one cumulative adversarial review over the whole series (verdict: SHIP).
• Verification: the exact commands + results table for HEAD 17c8aa9 — full-DB parity sweep GREEN (0 unexplained, swept=13547), the M1–M9 mutation matrix proving every floor/ledger assert discriminating (M4: 50 under-prompt-direction rows surfaced, 0 suppressible), workspace clippy 0, cargo test -p engine --features proptest 17301/0 re-run after the final rebase.
• Behavioral trace of the ordering seam (batch → CR 805.7 controller partition → ability_rw conflict consult → prompt/auto) incl. the monotone-safety argument: the pre-C1 path unconditionally auto-ordered, so C1 can only add prompts.
• Under-prompt proof: the sweep's direction gate routes any decision_old && !decision_new row to the asserted-empty unexplained — an allowlist entry cannot mask an under-prompt by construction.

Current-head checks have also populated since your comment: all required checks green, including Card data (generate, validate, coverage) (9m9s) and the parser gate; the branch base is the current main tip (c89f99c), so the parse-diff evidence is stale-base-free. Happy to add anything further you need for the enqueue decision.

[matthewevans]

Thanks for the follow-up. I rechecked the current packet for head 17c8aa90f5a66b9ec8e90e18eadb247dcdc824ff; checks are now green, but I still cannot approve/enqueue from the sweep because the local proof gate still reports proof_gap=true.

The remaining machine-visible gaps are:

• missing required AI-contributor template sections: summary, files changed, track, llm
• an unchecked implementation-method item remains visible: - [ ] **Not** /engine-implementer — explain why below

For this large hot-path engine trigger-ordering change, please update the PR body so the required sections and implementation-method checklist are unambiguous on the current head. I’ll hold this until that proof gate clears.

[lgray]

🤖 AI text below 🤖

@matthewevans Body restructured to the docs/AI-CONTRIBUTOR.md template so the proof gate has its machine-visible sections on this head (17c8aa9): ## Summary, ## Files changed (5 paths, measured from git diff --stat c89f99c37..HEAD), ## Track (Developer), ## LLM (Model/Thinking/Tier canonical lines), ## Verification (developer-track checklist: fmt/clippy-strict/parser-gate/test-engine 17301-0/card-data/full-DB sweep), and ## Scope Expansion / ## Validation Failures / ## CI Failures = None.. The unchecked implementation-method item is removed — only the checked /engine-implementer-pipeline box remains. The behavioral trace, under-prompt proof, and §7 sweep accounting from the previous revision are retained below the template sections. pr_review.py inspect 5072 should now report proof_gap == false; ping me if any section still reads as missing to the gate.

[matthewevans]

[HIGH] Same-event member-bound triggers can still auto-order. Evidence: crates/engine/src/game/ability_rw.rs:960 uses the same-event fast path when source_independent() is true, while source_independent() at crates/engine/src/game/ability_rw.rs:745 ignores reads_member_bound; member-bound targets are explicitly flagged at crates/engine/src/game/ability_rw.rs:1547 from carriers such as TrackedSet and ExiledBySource listed at crates/engine/src/game/ability_rw.rs:2254. Why it matters: same-event triggers whose resolution reads per-source storage can be treated as one source-independent function and skip the ordering choice even though the order can change the result. Suggested fix: make member-bound profiles refuse the same-event source_independent fast path and add a same-event tracked/exiled-by-source discriminator.

[HIGH] Non-phase delayed triggers bypass the CR 603.3b ordering gate. Evidence: crates/engine/src/game/triggers.rs:5242 APNAP-sorts delayed triggers, then crates/engine/src/game/triggers.rs:5256 iterates and crates/engine/src/game/triggers.rs:5275 dispatches each trigger directly; the phase-delayed path routes its pending batch through begin_trigger_ordering at crates/engine/src/game/triggers.rs:5547. Why it matters: simultaneous same-controller delayed triggers can reach the stack without the required ordering choice. Suggested fix: convert the non-phase delayed to_fire batch into PendingTriggerContexts and run it through begin_trigger_ordering before dispatching.

[lgray]

🤖 AI text below 🤖

@matthewevans Both [HIGH] findings are fixed, and the first one was a better catch than "plausible hole": the sweep measured it as live, not latent — 48 same-event cards were silently auto-ordering, and 6 of them are genuinely order-observable (real under-prompts): Mimic Vat + Mirror of Life Trapping (imprint-contention for the one shared triggering creature), Moonring Mirror + Duplicity (hand-swap re-capture, A feeds B), World Queller (shared-pool consumption under divergent chosen types), Blood Tyrant (self-write × CR 704.5a/800.4a elimination edge, caught incidentally). Thank you — the review directly removed reachable rules-wrong behavior.

HIGH-1 (d52b1ee38): your exact two shapes — !reads_member_bound in the fast-path disjunct + the fail-closed same_event ∧ reads_member_bound discriminator row (all_same_source stays auto-ordered: shared storage ⇒ f_A=f_B; batch path byte-inert). All 48 flips are over-prompt-direction by construction (the old path auto-ordered every same-event group), classified per-card with CR evidence: 6 genuine (exact-set asserted as SAME_EVENT_MEMBER_BOUND_GENUINE) + a predicate-keyed conservative class (se_member_bound_class, keyed on the discriminator's own gate, membership derived + emitted — not a 48-name allowlist). We considered narrowing the discriminator to the storage carriers you named (TrackedSet/ExiledBySource) and rejected it: it would leave the same-event guard weaker than the batch guard for AttachedTo/Chosen carriers (two Auras on the same creature are order-observable), and the full predicate is what you asked for. The class design paid for itself at the rebase: v0.15.0's parser surfaced Ichormoon Gauntlet as a new member-bound card and the class absorbed it (42→43) with zero allowlist edits; a name-enumerated assert would have broken.

HIGH-2 (69f012f8c): check_delayed_triggers' to_fire batch now converts to PendingTriggerContexts and routes through begin_trigger_ordering (phase-delayed path as template), with one engine_priority guard so the OrderTriggers prompt survives to the client. All delayed-specific dispositions preserved (Good King Mog, Breeches reflexive pause, epic, multi-fire) — the Paused reconciliation is idempotent by construction and pinned by the 4 Breeches/coin-flip tests. Runtime revert-to-red: two same-controller WhenDies delayed triggers off one death → prompt (RED pre-fix) AND correct post-order resolution. One pre-existing test (daretti_emblem_simultaneous_death) asserted the old direct-dispatch order for two distinct-target returns; it's updated to a positive OrderTriggers pin (CR 603.3b requires the controller's choice there).

Related issue triage: #4809 (Braids/Spinal) is a DISTINCT seam — AtNextPhase{End} is phase-classified and already merges+orders via the #5048 path, so it's neither closed nor regressed by HIGH-2; we'll verify it empirically and follow up on the issue separately. One new latent flagged in the HIGH-2 commit body: delayed triggers arriving during a ChooseOneOf replay (engine_resolution_choices), untested today.

Rebase + gates: series rebased onto 1badc1920 (v0.15.0), clean 9/9 replay (range-diff: 8/9 =, one benign use-line 3-way with #4625). Six new upstream enum variants classified wildcard-free in one adaptation commit (7d34c0185 — three of them depend on features born later in the series, so the pre-PR fold convention wasn't mechanically possible; details + full classification table in the commit body). After the rebase, main advanced by exactly one docs-only commit (63571d2) — no engine surface. Gates at 7d34c0185: workspace clippy 0 lints; cargo test -p engine --features proptest 17376/0; full-DB sweep GREEN, 0 unexplained (swept=13556, se_mb_genuine=6, se_member_bound_class=43, original 18/1/6 ledger unchanged). PR body §8 has the full accounting.

🤖 Generated with Claude Code

[matthewevans]

Findings:

• [HIGH] The new same-event gate is not actually fail-closed for all order-sensitive groups. ability_rw.rs documents that reads_event_live is never consulted on the same-event path, and gives a same-event write-then-read example that remains order-observable but still auto-orders (crates/engine/src/game/ability_rw.rs:33). That contradicts both the PR claim of a sound CR 603.3b same-event gate and the group_is_order_independent contract that says it "can never auto-order order-sensitive triggers" (crates/engine/src/game/triggers.rs:3542). The code path confirms the gap: profiles_conflict only includes reads_event_live in the non-same-event/batch checks (crates/engine/src/game/ability_rw.rs:991, crates/engine/src/game/ability_rw.rs:1005, crates/engine/src/game/ability_rw.rs:1032), while same-event ordering is decided by !same_event_conflict (crates/engine/src/game/triggers.rs:3465). Please either close this same-event event-object read/write feed in the classifier with a discriminating test, or narrow the implementation/claims so we are not landing a known rules-wrong same-event auto-order path as a sound CR 603.3b gate.

[lgray]

🤖 AI text below 🤖

@matthewevans Round-4 finding accepted and fixed via option 1 — the feed is closed (6dc10b9aa), and the claims now match the code.

The fix: a new shared predicate reads_and_writes_event_object() = reads_event_live && writes_event_object.any() — a conjunction, derived rather than copied from the batch guard (the batch's disjunction-of-negations only defers to the feed rows; a prompt-returning discriminator must witness a real feed, i.e. both endpoints). The same-event fast path's source_independent branch gains the exclusion, and a new discriminator same_event ∧ event_object_present ∧ reads_and_writes_event_object → prompt sits after the member-bound row. The event_object_present conjunct mirrors effective_external's existing no-op semantics (a write to a non-present event object provably no-ops), so Phase-mode triggers stay auto and the gate can only drop vacuous prompts. Both edits are same_event-guarded — the batch path is byte-inert. Why the batch path never had this hole: co-departure event objects are frozen LKI (CR 603.10a), so a write either no-ops or trips the freeze-invalidation row; same-event objects are live (CR 608.2h current-information reads), which is exactly where the feed existed.

Measured impact: +13 same-event flips, all over-prompt direction, and — honestly — 0 genuine. Every one of the 13 writes to the shared event object, and k identical functions on one shared object compose to the same final state under every permutation; R3's genuine members existed because their writes diverged into per-source piles. So SAME_EVENT_EVENT_OBJECT_GENUINE ships as an asserted-empty exact-set (a future genuine card must be added explicitly, not silently absorbed), with the 13 in a predicate-keyed conservative class (se_event_object_class, derived membership, mutation-proof floor, asserted disjoint from the member-bound class). Per-card both-orders traces are in the evidence artifact referenced from the PR body.

Claims-consistency: the module doc now records this feed as CLOSED at both depths and enumerates the two residuals that remain — source-actor granted-state, and board-wide writes_external × event-live read — both symmetric across batch and same-event depths. The group_is_order_independent contract comment now says precisely what the code does: never auto-orders order-dependence visible in the profiled read/write sets, sound modulo those two profile-invisible symmetric residuals. The PR body's claims were re-worded to match.

Rebase + gates: upstream moved during the fix (#5080 parser, #5088 World-rule SBA, #5089 data), so the full series was rebased onto 4c0ac54f5 — pure base-move, all 11 commits = in the range-diff, no dual-walk exhaustiveness breaks. #5088 is the rule cited for winter's night's practical unreachability; explicitly re-verified — the sweep's structural reachability keeps it a class member, no silent count movement. Gates at 6dc10b9aa: workspace clippy 0 lints; full engine tests 0 failures; full-DB sweep GREEN, 0 unexplained with every prior count unchanged (se_member_bound_class=43, 6 genuine, 18/1/6 ledger intact) plus the new se_event_object_class=13/0-genuine. PR body §8-R4 has the full accounting.

🤖 Generated with Claude Code

[matthewevans]

[HIGH] Please add a production-path test for the R4 event-object read/write discriminator. Evidence: triggers.rs builds event_object_present from the real pending trigger event and feeds that structure into profiles_conflict through group_is_order_independent; the current R4 coverage I can find is the sweep classifier plus lower-level profiles_conflict coverage, while the explicit group_is_order_independent regression around line 1884 covers the member-bound case, not the event-object feed. Why it matters: this is the exact hot-path threading that regressed in the prior review loop; a future mis-threading/revert in the caller could auto-order the R4 shape while the synthetic predicate test still passes. Suggested fix: add a focused triggers_ordering_parity_tests.rs test that calls group_is_order_independent with distinct sources on one shared event object, an EventSource/EventTarget live read plus a TriggeringSource event-object write, and guard cases for read-only, write-only/no-event, and same-source so the test proves the discriminator rather than a blanket prompt.

[lgray]

🤖 AI text below 🤖

@matthewevans Round-5 test landed (83bb4084a), plus the branch is re-based over your #5084 — and adopting its C2-ungating surfaced something worth your attention.

R5 test: the R4 discriminator is now pinned at the production caller level per your spec — group_is_order_independent with distinct sources on one shared event object, an EventSource/EventTarget live read + a TriggeringSource event-object write ⇒ prompt, with read-only / write-only-or-no-event / all-same-source guards proving it's a discriminator, not a blanket prompt. Revert-to-red measured at the caller level (disabling the discriminator reds the positive case while the guards stay green).

#5084 rebase — full disclosure: we adopted your C2-ungating verbatim (loop detection no longer gates finite ordering), and doing so turned two of this series' own negative tests red — which exposed a latent bug in this series, not in #5084: the coarse ability_scan-computed C2 term is blind to the source-actor residual, and as a disjunct it could override the precise batch/uniformity prompt for a Mixed-controller co-departure (the Dodecapod cause-source-controller channel — a genuine under-prompt). It was reachable only under loop-ON, which our NEGs never exercised; your always-on ungating made it default-path and the tests caught it immediately. Fix (01580f3bf): the C2 term becomes c2_order_independent && !batch_conflict — precision dominates coarseness, so C2 can never override the uniformity gate. This is not a modification of your decision: the loop-ungating stands, and your pr625_c2 fan-out still auto-orders (its group has batch_conflict=false; test green). Review confirmed the conjunct is sound everywhere — a real co-departure batch never reaches the C2 term, and elsewhere the conjunct is strictly more conservative. Revert-to-red: the bare c2 form re-reds both NEGs.

Also from the rebase: your stack.rs self-counter batching classified cleanly as orthogonal to the ordering gate (resolution-time, same-source, checkpoint-proven sequential-equivalent — triggers are ordered before they reach the stack); #5090 added no enum variant, corpus regenerated.

Gates at 01580f3bf (on cf7cd7cb9): workspace clippy 0 lints; engine tests 0 failures (lib 15103/0 + all integration); full-DB sweep GREEN, 0 unexplained with zero count movement across the rebase (43 + 13 conservative classes, 6 genuine, 18/1/6 ledger, all floors). Range-diff: 10/12 =; the two !s are the C1 conflict resolution (ungating re-applied at the tail so HEAD adopts #5084) and a context-line-only visibility bump in HIGH-2. PR body §8-R5 has the full accounting.

🤖 Generated with Claude Code

[github-actions]

Parse changes introduced by this PR

✓ No card-parse changes detected.