diff --git a/crates/engine/src/analysis/resource.rs b/crates/engine/src/analysis/resource.rs index 6bdea35258..6ec4dac558 100644 --- a/crates/engine/src/analysis/resource.rs +++ b/crates/engine/src/analysis/resource.rs @@ -293,11 +293,21 @@ mod verdict_memo { .and_then(|p| crate::game::engine::entry_publishes_pin_slots(frame, entry, p)); let primary = super::stack_entry_resolution_choice_freedom(frame, entry, &mut self.budget); - let residual = match published.as_ref().and_then(|p| p.may.as_ref()) { - Some(_) => { - super::optional_cleared_classification(frame, entry, &mut self.budget) - } - None => None, + // TWO bases need the optional-cleared re-classification, and they are + // MUTUALLY EXCLUSIVE by construction: `entry_publishes_pin_slots` guard (b) + // withholds the `may` slot exactly when a stored auto-choice already answers + // the CR 603.5 gate, so an auto-answered entry publishes NOTHING and would + // otherwise carry `residual: None` — the structural reason gate (6) could not + // relieve it. Computing the residual on the auto basis too is what makes + // `auto_may_choice_relief` able to read the same memo the pin relief reads. + let residual = if published.as_ref().and_then(|p| p.may.as_ref()).is_some() + || matches!( + super::auto_may_answer_for(frame, entry), + Some(crate::types::game_state::AutoMayChoice::Accept) + ) { + super::optional_cleared_classification(frame, entry, &mut self.budget) + } else { + None }; self.memo.insert( key, @@ -638,9 +648,24 @@ pub struct PeriodicDelta { /// count. It has to, for the class [`ring_delta_signature`] certifies: that basis proves /// a periodic DELTA, not a recurring board, so the drive's board-recurrence predicates are /// false at every settle beat and `Fixed(n)`'s `n` would otherwise be structurally inert. - /// The count is measured the same way it is minted — the engine's single - /// `record_loop_detect_sample` call site is inside `pass_priority_once_with_pipeline`, - /// which is the function the drive steps. + /// The count is measured the same way it is minted, and that now takes TWO sites to + /// state: `record_loop_detect_sample` is called from the settle sampler in + /// `game::engine::pass_priority_once_with_pipeline` AND from the forced-window answer + /// site in `game::engine::apply_action`. `drive_one_shortcut_cycle` covers both — it + /// steps `pass_priority_once_with_pipeline` on its priority beats and answers every other + /// prompt through `inject_pinned_answer`. Of its FOUR arms, three end in `apply_action` + /// (`OrderTriggers`, `TriggerTargetSelection`, `OptionalEffectChoice`) and the fourth is + /// `_ => Err(RecastAbort)`, which returns before any frame advance — as do the early `Err` + /// exits inside the two template arms. So every path that returns `Ok` HAS dispatched + /// `apply_action`, and every path that does not aborts the drive rather than advancing it + /// uncounted. + /// + /// The drive advances `frames_this_cycle` in BOTH of ITS OWN arms — the active-player + /// `Priority` arm and the `inject_pinned_answer` arm, not to be confused with the four + /// above — each keyed on the ring's back allocation actually changing, so mint and measure + /// stay one-to-one. Before the second site existed this doc claimed a single call site; + /// that premise is dead, and the count would silently read a HALF period if only one of + /// the drive's two arms counted. /// /// Named for its unit on purpose: `game::engine::shortcut_drive_period` maps a /// TEMPLATE to a repeat count, which is a different quantity in the same subsystem. @@ -1041,10 +1066,17 @@ impl ResourceVector { /// Life GAINS contribute nothing (`(-n).max(0)`), so a proposer gaining 5 while three /// opponents lose 1, 2 and 3 yields 3 — never 5, and never 6. /// - /// Extracted from `game::engine::try_offer_bounded_cycle_shortcut` so the max-vs-sum - /// fork has a callable seam: `victim_slot` is empty on every trajectory that offers - /// today, so this expression's value is dropped in production and no fixture reaches - /// it. `worst_seat_life_loss_is_the_max_seat_never_the_sum` is its only discriminator. + /// Extracted from `game::engine::try_offer_bounded_cycle_shortcut` so the max-vs-sum fork + /// has a callable seam. ⚠ THE NOTE THAT STOOD HERE — *"`victim_slot` is empty on every + /// trajectory that offers today … no fixture reaches it"* — IS FALSIFIED, and is replaced + /// rather than softened: once the answer-beat sampling site in `apply_action` announces + /// the entries a FORCED pre-priority window puts on the stack, a CR 608.2b `Targets` + /// declaration is announced like any other and `victim_slot` is NON-EMPTY on the F4 + /// boards. `worst_seat_life_loss_is_the_max_seat_never_the_sum` is therefore no longer the + /// only discriminator: the real-dump rows re-derive this value through + /// `elimination_bounds` (`r1_the_bounded_offer_fires_on_the_real_f4_dump`), and + /// `b5f_the_declared_term_can_suppress_an_otherwise_legal_offer` measures it flipping a + /// live offer to `NoNarrowedLegalCount`. pub(crate) fn worst_seat_life_loss(&self) -> i64 { self.life.values().map(|&n| (-n).max(0)).max().unwrap_or(0) } @@ -1285,8 +1317,11 @@ fn map_delta( /// that moves no resource states no CR 704 threshold to bound. A certifying window that is /// not TURN-POSITION invariant ⇒ `None` (the CR 703.1 conjunct below). Reading the RING only /// — never the live `state` — keeps the compared frames homogeneous: every ring frame is a -/// `normalize_for_loop` snapshot taken at `WaitingFor::Priority{active_player}` -/// (`game::engine`'s sole `record_loop_detect_sample` call site), while the live state is not +/// `normalize_for_loop` snapshot taken at `WaitingFor::Priority{active_player}`. That holds +/// across BOTH of `game::engine`'s `record_loop_detect_sample` sites (the settle sampler in +/// `pass_priority_once_with_pipeline` and the forced-window answer site in `apply_action`), +/// because the two gate on the same `wf` conjunct — the homogeneity argument no longer rests +/// on there being one site, it rests on that shared conjunct. Meanwhile the live state is not /// normalized. It does not consult a board predicate, but it DOES require the frames it /// compares to be homogeneous in turn position, which is what "homogeneous" above now means /// in full. @@ -1987,6 +2022,70 @@ fn pinned_may_choice_relief( } } +/// CR 603.5: is this entry's optional trigger ALREADY ANSWERED by a stored "don't ask +/// again" auto-choice — and with which answer? +/// +/// ADOPTION C. This used to re-derive the CR 603.5 gate's conjunct set here, which made it a +/// THIRD copy: it asked the three repeat-shape predicates and the recipient authority +/// directly, and — measured — it OMITTED both `optional_for` and the feasibility probe, so it +/// called a may "answered" on two ability shapes where the gate never reads the store at all. +/// It now delegates the whole question to `effects::stored_may_answer`, the consumer half of +/// the one authority `resolve_chain_body`'s own branch and the mint's guard (b) both take. +/// +/// NOT keyed to the proposer, and that survives the adoption: the gate asks whoever +/// `optional_prompt_player` names, and a stored answer specifies that choice regardless of +/// whose it is — a per-iteration window that never opens is specified for every seat at once +/// (CR 732.2a). +/// +/// `None` ⇒ no up-front gate opens, or it will PROMPT, or the ability carries no +/// `may_trigger_origin` for a preference to key on. All are unspecified windows, which is the +/// fail-closed direction. +fn auto_may_answer_for( + frame: &GameState, + entry: &StackEntry, +) -> Option { + let StackEntryKind::TriggeredAbility { ability, .. } = &entry.kind else { + return None; + }; + crate::game::effects::stored_may_answer(frame, ability) +} + +/// CR 732.2a + CR 603.5: relief basis ONE for gate (6)'s `MayPrompt` — the may this entry +/// announces is answered by a stored auto-choice, so the shortcut opens no window there. +/// +/// The SIBLING of [`pinned_may_choice_relief`] and deliberately its identical shape: both +/// discharge exactly the `ability.optional` axis and both hand back the SAME +/// optional-cleared residual for the caller to go on gating, because a specified `may` +/// says nothing about the CR 616.1 replacement surface of the events it then proposes. +/// The five OTHER reasons `ability_resolution_choice_freedom` returns `MayPrompt` — an +/// `unless_pay`, a resolution-time target chooser, a modal header, a controller-choice +/// repeat, a CR 701.34a proliferate sub-ability — keep returning `MayPrompt` as the +/// residual and get no relief here, exactly as they get none from a pin. +/// +/// ONLY `Accept` IS RELIEVED, and the asymmetry is not caution — it is what the residual +/// MEANS. `optional_cleared_classification` re-classifies the ability as if it RESOLVED +/// with its gate discharged, which is what a stored `Accept` produces. A stored `Decline` +/// is equally prompt-free but produces the opposite board, so that residual would be a +/// claim about events the shortcut never proposes. (It also cannot arise in a certified +/// period: a declined `may` contributes none of the per-cycle delta the ring recurrence +/// was built from.) +fn auto_may_choice_relief( + frame: &GameState, + f: FrameIx, + entry: &StackEntry, + verdicts: &mut PeriodVerdicts<'_>, +) -> Option { + use crate::game::resolution_prompt::ResolutionChoiceFreedom; + use crate::types::game_state::AutoMayChoice; + if !matches!(auto_may_answer_for(frame, entry)?, AutoMayChoice::Accept) { + return None; + } + match verdicts.verdict(f, entry).residual.as_ref()? { + ResolutionChoiceFreedom::MayPrompt => None, + residual @ ResolutionChoiceFreedom::FreeUnlessReplacements(_) => Some(residual.clone()), + } +} + /// Karp–Miller-style ω-acceleration (Karp–Miller 1969; Finkel et al. 2021), sound /// GIVEN the in-loop transition relation — the WHOLE beat: top-of-stack resolution /// (CR 608.1) with its resolution-time payments (CR 605.3a / CR 608.2g), trigger @@ -2136,14 +2235,30 @@ pub(crate) fn stack_choices_are_all_specified<'a>( let primary = verdicts.verdict(f, entry).primary.clone(); let verdict = match primary { crate::game::resolution_prompt::ResolutionChoiceFreedom::MayPrompt => { - match pinned_may_choice_relief(f, entry, verdicts, scope) { + // CR 603.5: TWO bases can specify a `may`, and they are mutually exclusive + // by construction — the mint's guard (b) publishes a `MayChoice` slot only + // for a may that has NO stored auto-choice, and withholds it for one that + // does. Asking the auto basis first is therefore an ordering of disjoint + // cases, not a precedence. An auto-answered may is the MOST determined a + // per-iteration choice can be; reading its slotless mint as "unspecified" + // was the defect. + let relief = auto_may_choice_relief(frame, f, entry, verdicts) + .or_else(|| pinned_may_choice_relief(f, entry, verdicts, scope)); + match relief { Some(residual) => residual, None => return false, } } free => free, }; - if !resolution_events_are_discharged(frame, verdict) { + if !resolution_events_are_discharged(frame, verdict.clone()) { + return false; + } + // CR 616.1 + CR 732.2a: the CANDIDATE-AUTHORITY half is a claim about the FUTURE — + // the shortcut's remaining repetitions resolve under the board that exists NOW, so a + // replacement definition that entered play after this frame was captured is invisible + // to the frame-side discharge above. Fail-closed second discharge against `state`. + if !std::ptr::eq(*frame, state) && !resolution_events_are_discharged(state, verdict) { return false; } } @@ -5331,10 +5446,82 @@ mod tests { None } + /// PRODUCTION'S OWN CANDIDATE WALK, CONSUMED rather than imitated: this asks + /// [`crate::game::engine::candidate_windows`] — the very iterator + /// `certified_bounded_cycle_offer` walks — so the ORDER (newest-first), the span + /// arithmetic and the degenerate-pair filter are production's by construction. Returns + /// the first `idx` whose window drives item (4) AT ALL, with that window's certified + /// touch and its measured span. + /// + /// CR 732.2a: `frames_per_period` is a MEASURED span, so a row that hard-codes + /// `&live[live.len() - 2..]` is asserting `span == 1` without saying so — and reads a + /// HALF PERIOD the moment the sampling rate moves. It moved: the answer-beat sampler + /// retains a frame at forced-window ANSWER beats as well, which halves the newest + /// adjacent pair on the dellian dump. + /// + /// **PRECONDITION, NOT CONCLUSION.** `conjunct4_scans() > 0` says items (1)/(2)/(3) + /// passed on SOME production-shaped window so item (4) RAN; it admits `scans ∈ {1, 2}`, + /// which FAILS the caller's `scans > non_exempt` assertion. The search can therefore land + /// on a beat whose assertion fails — that is what keeps the caller non-vacuous. + /// + /// One FRESH container per candidate: the counter is cumulative, so a shared container + /// (which is what production carries) would make `> 0` unattributable after the first + /// candidate that scans. + fn newest_item4_window<'a>( + live: &[&'a GameState], + current: &'a GameState, + proposer: PlayerId, + ) -> Option<(usize, PeriodTouch<'a>, u32)> { + for (idx, span, window) in crate::game::engine::candidate_windows(live) { + let touch = certified_period_touch(window, current, PeriodCertification::BoardCovered); + let mut verdicts = PeriodVerdicts::for_period(live, current, proposer); + let _ = loop_states_cover_modulo_growth_pinned( + window[0], + current, + proposer, + &[], + &touch, + &mut verdicts, + ); + if verdicts.conjunct4_scans() > 0 { + return Some((idx, touch, span)); + } + } + None + } + /// The construction requirement shared by every row that needs a REAL certified window /// carrying a non-empty observed-frozen prefix: a usable ring AND a newest candidate pair /// (`span == 1`, the shape §3 D2's walk reaches first) whose common prefix is /// index-stable. + /// + /// ⚠ THIS PREDICATE HARD-CODES `span == 1`, and the residual that leaves is SMALLER IN + /// COUNT AND LARGER IN KIND than "four authored-ring rows" claimed. MEASURED: exactly TWO + /// call sites remain — `r21_b_the_exemption_narrows_conjunct_six_by_exactly_the_frozen_set` + /// and `r27_a2_every_announced_pair_carries_an_unnormalized_evaluation_board` — and + /// NEITHER is an authored ring. Both drive the REAL `TRACKED_DUMPS` through + /// `drive_dump_until`, so both are exposed to the answer-beat sampler that can halve the + /// newest adjacent pair (the hazard [`newest_item4_window`] exists for). They stay because + /// at the beat this predicate SELECTS the hardcode is EXACT — not because a half period + /// would fail loudly, which it would not. + /// + /// MEASURED at the beat `drive_dump_until(gz, 80, has_frozen_window)` returns: `dina` beat + /// 6, `ring = 2`; `dellian` beat 5, `ring = 2`; and `candidate_windows` yields exactly ONE + /// candidate on each — `idx = 0`, `span = 1`, window length 2. With a two-frame ring + /// `&live[live.len() - 2..]` IS the whole ring, so there is no half period to read here. + /// + /// ⚠ THE REASON THAT STOOD HERE — *"both fail LOUD rather than silently on a half period … + /// each then asserts its own domain non-empty"* — IS UNPROVEN AND WRONG, and is replaced + /// rather than softened. The loud floors are real but do not cover this hazard: a half + /// period is a NON-degenerate window with non-empty domains, so neither + /// `drive_dump_until`'s reach-guard nor either row's domain-non-empty assertion + /// (`frozen_ids`/`announced` in the first, `announced` in the second) would fire on one, + /// and both rows' claims (a set-narrowing identity; a universal over announced pairs) are + /// span-INDEPENDENT, so on a half period they would PASS. The residual is therefore "exact + /// today, SILENT the day the sampling rate grows this ring past two frames" — a smaller + /// hazard than the old text claimed to have closed, and an honest one. The real-dump + /// item-(4) rows, which have no such measured guarantee, use [`newest_item4_window`] + /// instead. fn has_frozen_window(state: &GameState) -> bool { if state.loop_detect_ring.len() < 2 { return false; @@ -10543,14 +10730,26 @@ mod tests { } /// PR-7 Phase 5b (PA-2A(e)) — CR 704.5a: the MAX-vs-SUM fork in `victim_slot`'s magnitude - /// derivation, which is otherwise UNTESTED and whose wrong answer surfaces in playtesting - /// as a wrong elimination bound rather than as a failure. + /// derivation, whose wrong answer surfaces in playtesting as a wrong elimination bound + /// rather than as a failure. + /// + /// WHY IT NEEDS ITS OWN ROW. ⚠ THE REASON THAT STOOD HERE — *"`victim_slot` is EMPTY on + /// every trajectory that offers today … all publish `points == 0` … no fixture reaches the + /// fork"* — IS FALSIFIED, and is replaced rather than softened: once the answer-beat + /// sampling site in `apply_action` announces the entries a FORCED pre-priority window puts + /// on the stack, a CR 608.2b `Targets` declaration is announced like any other, so on the + /// F4 boards `points` carries Torch's `Targets` point and `victim_slot` is NON-EMPTY. This + /// value is therefore no longer collected into an empty `Vec` and dropped — it reaches + /// `elimination_bounds` in production, `r1_the_bounded_offer_fires_on_the_real_f4_dump` + /// re-derives the published bound with a non-zero declared term, and + /// `b5f_the_declared_term_can_suppress_an_otherwise_legal_offer` measures it flipping a live + /// offer to `NoNarrowedLegalCount`. /// - /// WHY IT NEEDS ITS OWN ROW: `victim_slot` is EMPTY on every trajectory that offers today - /// — dina, the ≥3p life drain and the F4 predicate all publish `points == 0` — so in - /// production `worst_seat_life_loss` is evaluated only where its value is collected into - /// an empty `Vec` and dropped. No fixture reaches the fork. Stated as a coverage hole in - /// the PR body; 5d's targeted class is its first production-path consumer. + /// What those real-dump rows do NOT cover is THIS fork. Both take the magnitude off the + /// offer's own published `per_cycle.victim_slot`, so they track whatever the derivation + /// returns instead of discriminating between derivations — swap `max` for `sum` and their + /// expectations move with it. The max-vs-sum discrimination below is still this row's alone, + /// and that, not an absent production consumer, is why it stays. /// /// O4 DERIVE conformance — all THREE legs, not one: /// 1. **DERIVED, never compared to a literal.** `m` is bound from the return value and @@ -13970,18 +14169,32 @@ mod tests { /// item (4) trips on IS ITSELF a frozen one, so the unmutated board already witnesses /// that item (4) does not consult the exemption. /// + /// ⚠ THE WINDOW IS PRODUCTION'S, NOT `len - 2`. The old selection asserted `span == 1` + /// silently, and the answer-beat sampler halved the newest adjacent pair on this dump: + /// MEASURED, a span-1 window scans **0** entries at every beat 0..79, while production's + /// first item-(4) candidate is **span 2** and scans 36. Both the search and the window now + /// come from [`newest_item4_window`], i.e. from `game::engine::candidate_windows`. + /// /// REVERT-PROBE: add a `frozen_ids` skip to item (4)'s closure ⇒ the scan can no longer /// reach index 35 and `conjunct4_scans` collapses to at most the non-exempt population - /// (2 on this board) ⇒ FLIPS. + /// (2 on this board) ⇒ FLIPS **while the search still succeeds and lands on the same + /// beat** — which is what proves the search is a precondition and not the assertion. #[test] fn r21_b_placement_b_item_four_scans_frozen_entries_that_conjunct_six_skips() { - let (beat, board) = drive_dump_until(TRACKED_DUMPS[1].1, 80, has_frozen_window) - .expect("REACH-GUARD: the dellian drive must reach a window with a frozen prefix"); + let (beat, board) = drive_dump_until(TRACKED_DUMPS[1].1, 80, |s| { + let live: Vec<&GameState> = s.loop_detect_ring.iter().map(|f| &f.live).collect(); + newest_item4_window(&live, s, s.active_player).is_some() + }) + .expect( + "REACH-GUARD: the dellian drive must reach a beat whose production candidate window \ + runs item (4) at all", + ); let live: Vec<&GameState> = board.loop_detect_ring.iter().map(|f| &f.live).collect(); - let window = &live[live.len() - 2..]; - let prior = window[0]; let proposer = board.active_player; - let cover = certified_period_touch(window, &board, PeriodCertification::BoardCovered); + let (idx, cover, span) = newest_item4_window(&live, &board, proposer) + .expect("the search predicate accepted this very board one line ago"); + let window = &live[idx..]; + let prior = window[0]; let non_exempt = board.stack.len() - cover.frozen_ids.len(); assert!( cover.frozen_ids.len() > non_exempt, @@ -13998,9 +14211,9 @@ mod tests { let scans = v4.conjunct4_scans() as usize; assert!( scans > non_exempt, - "R21(b-placement-B) beat {beat}: item (4) scanned {scans} entries, which must \ - EXCEED the {non_exempt} non-exempt ones — a scan that consulted `frozen_ids` \ - could never get past them" + "R21(b-placement-B) beat {beat} (window idx {idx}, span {span}): item (4) scanned \ + {scans} entries, which must EXCEED the {non_exempt} non-exempt ones — a scan that \ + consulted `frozen_ids` could never get past them" ); assert!( scans > 0 && scans < board.stack.len(), @@ -14032,10 +14245,20 @@ mod tests { let mut v6 = PeriodVerdicts::for_period(&live, &board, proposer); let specified = stack_choices_are_all_specified(&board, proposer, &[], Some(&cover), &mut v6); - assert!( - specified, - "REACH-GUARD: the resolution gate must run to completion under the exempting \ - certificate, else its skip count is a truncation" + // The guard states what it actually needs: a gate that ASKED must have COMPLETED, and no + // answer was denied. MEASURED on production's own span-2 window the gate returns false + // with `denied=false` and `conjunct6_asks=0` — a structural refusal at a pre-ask + // conjunct, AFTER taking every one of the frozen skips. The exemption's COMPLETENESS is + // checked by the verbatim equality below, not here. (A truncation of the skip count is + // not a reachable failure mode: `note_conjunct6_frozen_skip`'s loop has no break and no + // early return — the gate's `return false`s live in the NEXT loop, which runs only after + // the counting loop has finished.) + assert!( + !v6.denied() && specified == (v6.conjunct6_asks() > 0), + "REACH-GUARD: no answer may be denied, and a gate that ASKED must have completed. \ + specified={specified} denied={} asks={}", + v6.denied(), + v6.conjunct6_asks() ); assert_eq!( v6.conjunct6_frozen_skips() as usize, @@ -14255,19 +14478,50 @@ mod tests { /// (dina, integration row `r16_the_offering_beats_probe_demand_is_exactly_measured`) /// spends 13 and is NOT denied. Same seam, same cap, opposite sides of the budget. /// + /// ⚠ THE SEARCH IS THE ROW'S OWN CONSTRUCTION REQUIREMENT, NOT `has_frozen_window`. "Mintable" + /// means the walk reached the METERED CLASSIFIER, i.e. `meter.spent > 0`. The old predicate + /// asserted `span == 1` on the newest pair and landed on the first ring-bearing beat, where + /// the mint spends 0 and never reaches the classifier at all. `meter.denied` was REJECTED as + /// a search predicate: `denied` can only latch after exhaustion, so `denied ⇒ spent == cap` + /// and the assertion would assert itself. + /// /// REVERT-PROBE: raise `PROBE_BUDGET` above dellian's unexempted demand (measured 96–107 /// at these beats) ⇒ `denied` goes false ⇒ FLIPS. Lowering it cannot flip this arm, which - /// is exactly why the offering-beat row is a separate one. + /// is exactly why the offering-beat row is a separate one. **That revert-probe is SHIPPED + /// IN-ROW as a positive control** ([`ProbeCap::RaisedTwiceLinks`], the same board, one + /// argument apart): the meter provably returns `(x, false)` here, so `(cap, true)` is a + /// verdict about the SHIPPED cap and not a property of the instrument. Self-checking — if + /// the raised cap were still insufficient, `!raised.denied` fails loudly. #[test] fn r16_ii_b_a_non_offering_mintable_beat_saturates_the_probe_budget() { use crate::game::engine::{try_offer_bounded_cycle_shortcut_metered, ProbeCap}; use crate::types::game_state::WaitingFor; - let (beat, board) = drive_dump_until(TRACKED_DUMPS[1].1, 80, has_frozen_window) - .expect("REACH-GUARD: the dellian drive must reach a mintable beat"); - let proposer = board.active_player; - let mut at_priority = board.clone(); - at_priority.waiting_for = WaitingFor::Priority { player: proposer }; + /// The row's board construction, shared by the SEARCH and the measurement so the beat + /// the search accepted is byte-identically the beat the assertions read. + fn at_priority_of(s: &GameState) -> GameState { + let mut at_priority = s.clone(); + at_priority.waiting_for = WaitingFor::Priority { + player: s.active_player, + }; + at_priority + } + + let (beat, board) = drive_dump_until(TRACKED_DUMPS[1].1, 80, |s| { + let (_, meter) = try_offer_bounded_cycle_shortcut_metered( + &at_priority_of(s), + false, + ProbeCap::Shipped, + ); + meter.spent > 0 + }) + .expect("REACH-GUARD: the dellian drive must reach a beat the metered classifier runs on"); + assert!( + beat > 0, + "ANTI-VACUITY: the search must have REJECTED at least one beat, else `spent > 0` is \ + a tautology satisfied by beat 0 rather than a filter" + ); + let at_priority = at_priority_of(&board); assert!( at_priority.last_loop_action_sequence.is_empty() && at_priority.loop_detect_ring.len() >= 2, @@ -14296,6 +14550,23 @@ mod tests { meter {meter:?}, stack {}", at_priority.stack.len() ); + + // ── ANTI-VACUITY: `spent > 0` does NOT imply saturation, proven ON THIS BOARD ─────── + // The row's own revert-probe, shipped. One argument apart from the measurement above: + // same board, same seam, a cap of twice the board's link count. + let (_, raised) = try_offer_bounded_cycle_shortcut_metered( + &at_priority, + false, + ProbeCap::RaisedTwiceLinks, + ); + assert!( + raised.spent > PROBE_BUDGET && !raised.denied, + "POSITIVE CONTROL: at a cap of twice the link count the SAME board must spend past \ + the shipped cap WITHOUT latching exhaustion — otherwise `(cap, true)` above is a \ + property of the instrument rather than a verdict about the shipped cap. \ + raised {raised:?}, shipped cap {PROBE_BUDGET}, stack {}", + at_priority.stack.len() + ); } // ─────────────────────────────────────────────────────────────────────────────────── @@ -15668,6 +15939,198 @@ mod tests { frame } + // ─────────────────────────────────────────────────────────────────────────────────── + // N3 — the CR 616.1 obligation is discharged against the LIVE board as well as the + // carrying frame, because the shortcut's remaining repetitions resolve under the board + // that exists NOW. + // ─────────────────────────────────────────────────────────────────────────────────── + + /// An OPTIONAL (or mandatory) `Draw` replacement definition, of exactly the shape + /// `find_applicable_replacements` draws for a `ProposedEvent::Draw`. + fn n3_draw_replacement(optional: bool) -> crate::types::ability::ReplacementDefinition { + use crate::types::ability::{ + DrawReplacementScope, QuantityModification, ReplacementDefinition, ReplacementMode, + }; + use crate::types::replacements::ReplacementEvent; + let mut def = ReplacementDefinition::new(ReplacementEvent::Draw); + if optional { + def.mode = ReplacementMode::Optional { decline: None }; + } + // CR 121.2: a Draw definition must declare its stage or the pipeline debug-asserts. + def.draw_scope = Some(DrawReplacementScope::IndividualDraw); + def.quantity_modification = Some(QuantityModification::Plus { value: 1 }); + def + } + + /// N3 — **A REPLACEMENT THAT ENTERED PLAY AFTER THE FRAME WAS CAPTURED STILL REFUSES.** + /// + /// CR 616.1 + CR 732.2a. Conjunct (6) classifies each announced entry on its CARRYING + /// FRAME, which is a retained ring sample and therefore a board from the PAST. Discharging + /// the resulting `FreeUnlessReplacements` obligation against that frame alone answers the + /// wrong question: the shortcut is a claim about the FUTURE, and every remaining repetition + /// resolves under the board that exists NOW. A definition that entered the battlefield + /// after the sample was taken is invisible to the frame-side discharge — and it is exactly + /// the CR 616.1 resolution-time choice CR 732.2a forbids a described sequence from + /// containing. + /// + /// The fixture makes the two boards differ in EXACTLY that field: every ring frame is + /// cloned before the definition is installed, so the def exists on `state` and nowhere + /// else. `announced_from_retained_sample` is the reach-guard that the pair really is + /// carried by a frame that is not `current` — without it every arm here would be about the + /// first discharge. + /// + /// | arm | where the def lives | mode | gate | + /// |---|---|---|---| + /// | (pos) | nowhere | — | **specified** | + /// | (live) | live board only | OPTIONAL | **refused** | + /// | (live-mandatory) | live board only | mandatory | **specified** | + /// | (both) | every frame AND live | OPTIONAL | **refused** | + /// + /// (live-mandatory) is what keys (live) to OPTIONALITY rather than to "a definition + /// exists"; (both) proves the frame-side discharge is still doing its own job, so (live) + /// is a strictly ADDED refusal and not a relocated one. + /// + /// REVERT-PROBE: delete the second `resolution_events_are_discharged(state, ..)` call ⇒ + /// arm (live) certifies ⇒ FLIPS, while (pos), (live-mandatory) and (both) are unmoved. + #[test] + fn n3_a_replacement_installed_after_the_frame_was_captured_refuses_certification() { + let announced_id = 9310u64; + let build = |where_def: Option<(bool, bool)>| -> GameState { + // `where_def = Some((in_frames, optional))`. + let in_frames = where_def.is_some_and(|(f, _)| f); + let optional = where_def.is_some_and(|(_, o)| o); + let mut state = ring_announcing_on_its_newest_sample( + |st| { + let src = announcing_ring_source(st, 931); + if in_frames { + st.objects + .get_mut(&src) + .expect("just inserted") + .replacement_definitions + .push(n3_draw_replacement(optional)); + } + }, + |frame| { + let src = ObjectId(931); + let ability = crate::types::ability::ResolvedAbility::new( + u2_draw_effect(), + vec![], + src, + PlayerId(0), + ); + frame.stack.push_back(announced_trigger_entry( + announced_id, + src, + ability, + None, + )); + }, + ); + if where_def.is_some() && !in_frames { + state + .objects + .get_mut(&ObjectId(931)) + .expect("the announcing source is on the live board too") + .replacement_definitions + .push(n3_draw_replacement(optional)); + } + state + }; + + let gate = |state: &GameState| -> bool { + // REACH-GUARD, run on every arm: the pair is carried by a retained frame that is + // NOT `current`, so the second discharge is reachable at all. + announced_from_retained_sample(state, announced_id); + let ring: Vec<&GameState> = state.loop_detect_ring.iter().map(|f| &f.live).collect(); + let cover = certified_period_touch( + &ring[ring.len() - 2..], + state, + PeriodCertification::BoardEqualOnly, + ); + let mut verdicts = PeriodVerdicts::for_period(&ring, state, PlayerId(0)); + stack_choices_are_all_specified(state, PlayerId(0), &[], Some(&cover), &mut verdicts) + }; + + assert!( + gate(&build(None)), + "(pos) MATCHED POSITIVE, asserted first: with no replacement definition anywhere \ + the announced mandatory draw is choice-free and the period certifies. Without \ + this arm every refusal below could belong to an unrelated conjunct" + ); + assert!( + !gate(&build(Some((false, true)))), + "(live) CR 616.1 + CR 732.2a: an OPTIONAL definition that exists on the LIVE board \ + and on no retained frame is a real resolution-time choice for every remaining \ + repetition. The frame-side discharge cannot see it — this is the arm the second \ + discharge exists for" + ); + assert!( + gate(&build(Some((false, false)))), + "(live-mandatory) the SAME live-only definition, MANDATORY, opens no choice and the \ + period still certifies. Without this arm (live) would be keyed to `a definition \ + exists` rather than to OPTIONALITY" + ); + assert!( + !gate(&build(Some((true, true)))), + "(both) the definition present in every frame AND live still refuses — the \ + frame-side discharge keeps doing its own job, so (live) is an ADDED refusal and \ + not a relocated one" + ); + } + + /// N3, the `ptr::eq` short-circuit — **SKIPPING THE SECOND DISCHARGE WHEN THE CARRYING + /// FRAME *IS* THE LIVE BOARD COSTS NOTHING.** + /// + /// CR 616.1. The second discharge is guarded by `!std::ptr::eq(*frame, state)`, which is a + /// de-duplication and not a hole: when the announced pair is carried by `current` itself + /// the FIRST discharge already ran against that very board. This row exhibits that arm — + /// an entry on `current`'s own stack, no ring at all — and shows the optional definition is + /// still refused, on the same board shape where the guard suppresses the second call. + /// + /// Paired with a positive on the identical board one field apart (the mandatory mode), so + /// the refusal is attributable to the definition rather than to the `frames: &[]` shape. + #[test] + fn n3_b_a_live_carried_pair_is_still_discharged_by_the_first_call() { + let board = |optional: Option| -> GameState { + let (mut state, src) = u2_relief_board(); + let entry = u2_shape_b_entry(src, 9311, u2_draw_effect(), |ability| { + // MANDATORY: an optional ability classifies `MayPrompt` and never reaches the + // discharge at all, which would make both arms below vacuous. + ability.optional = false; + }); + if let Some(optional) = optional { + state + .objects + .get_mut(&src) + .expect("u2's source is on the battlefield") + .replacement_definitions + .push(n3_draw_replacement(optional)); + } + state.stack.push_back(entry); + state + }; + let gate = |state: &GameState| -> bool { + let mut verdicts = PeriodVerdicts::for_period(&[], state, PlayerId(0)); + stack_choices_are_all_specified(state, PlayerId(0), &[], None, &mut verdicts) + }; + + assert!( + gate(&board(None)), + "REACH-GUARD: with no definition the live-carried entry certifies, so the arms \ + below are about the definition and not about the `frames: &[]` shape" + ); + assert!( + gate(&board(Some(false))), + "a MANDATORY definition opens no CR 616.1 choice — the paired positive" + ); + assert!( + !gate(&board(Some(true))), + "an OPTIONAL definition on a LIVE-CARRIED pair is still refused by the FIRST \ + discharge, which is why the second one is guarded by `ptr::eq` rather than \ + unconditional: the guard removes a duplicate call, never a refusal" + ); + } + /// R27 (a3) — THE BEHAVIOUR: A RETAINED SAMPLE DERIVES THE SAME EVENT SET THE LIVE BOARD /// DOES, AND THE NORMALIZED HALF DOES NOT. /// @@ -15962,6 +16425,423 @@ mod tests { ); } + // ─────────────────────────────────────────────────────────────────────────────────── + // F2 / N0 / A5 — one CR 603.5 authority, its two consumers, and the stored answer. + // ─────────────────────────────────────────────────────────────────────────────────── + + /// A5 / N0 — **A STORED `Accept` RELIEVES GATE (6). A STORED `Decline` DOES NOT.** + /// + /// CR 603.5 + CR 732.2a. The matched pair `r27_b` is one field short of: same board, same + /// key, ONE value different. It is the whole content of the auto-choice relief basis, and + /// it is the arm the user's own MODE1 board rides on — that capture carries a stored + /// "always take", so guard (b) withholds the pin slot and the ONLY thing that can specify + /// the window is this relief. + /// + /// | stored | pin published | gate (6) | offer | + /// |---|---|---|---| + /// | `Accept` | NO (guard (b) withholds it) | relieved by the AUTO basis | **OFFERS** | + /// | `Decline` | NO (same withholding) | not relieved | **`UnspecifiedChoiceWindow`** | + /// + /// THE ASYMMETRY IS NOT CAUTION, it is what the residual MEANS. + /// `optional_cleared_classification` re-classifies the ability as if it RESOLVED with its + /// gate discharged, which is what a stored `Accept` produces. A stored `Decline` is equally + /// prompt-free but produces the OPPOSITE board, so relieving it would hand the certificate + /// a claim about events the shortcut never proposes. + /// + /// The `Accept` arm is also the anti-vacuity control for the `Decline` arm: without it + /// "Decline refuses" is indistinguishable from a relief that never fires at all. + /// + /// REVERT-PROBE: delete the `auto_may_choice_relief` disjunct from gate (6) ⇒ the `Accept` + /// arm stops offering ⇒ FLIPS. TRIVIALIZE-PROBE: relieve on ANY stored answer (drop the + /// `matches!(.., Accept)` conjunct) ⇒ the `Decline` arm starts offering ⇒ FLIPS. + #[test] + fn a5_a_stored_accept_relieves_gate_six_and_a_stored_decline_does_not() { + use crate::game::engine::{ + entry_publishes_pin_slots, try_offer_bounded_cycle_shortcut_metered, + BoundedOfferRefusal, ProbeCap, + }; + use crate::types::ability::{ + Effect, QuantityExpr, ResolvedAbility, TargetFilter, TriggerBaseSetInstanceRef, + TriggerDefinitionOccurrenceRef, TriggerDefinitionRef, + }; + use crate::types::game_state::{AutoMayChoice, MayTriggerAutoChoiceKey, MayTriggerOrigin}; + use crate::types::identifiers::ObjectIncarnationRef; + + const SRC: ObjectId = ObjectId(940); + const ENTRY: u64 = 954; + let origin = MayTriggerOrigin::Definition { + definition_ref: TriggerDefinitionRef { + source: ObjectIncarnationRef::of(SRC, 3), + occurrence: TriggerDefinitionOccurrenceRef::Printed { + base_set: TriggerBaseSetInstanceRef::INITIAL, + printed_index: 0, + }, + }, + }; + let key = MayTriggerAutoChoiceKey { + player: PlayerId(0), + source_id: SRC, + origin: origin.clone(), + }; + let announce = { + let origin = origin.clone(); + move |frame: &mut GameState| { + let mut ability = ResolvedAbility::new( + Effect::Draw { + count: QuantityExpr::Fixed { value: 1 }, + target: TargetFilter::Controller, + }, + vec![], + SRC, + PlayerId(0), + ); + ability.optional = true; + ability.may_trigger_origin = Some(origin.clone()); + frame + .stack + .push_back(announced_trigger_entry(ENTRY, SRC, ability, None)); + } + }; + let board = |stored: AutoMayChoice| { + let key = key.clone(); + ring_announcing_on_its_newest_sample( + move |s| { + announcing_ring_source(s, SRC.0); + s.set_may_trigger_auto_choice(key.clone(), stored); + }, + announce.clone(), + ) + }; + + for stored in [AutoMayChoice::Accept, AutoMayChoice::Decline] { + let state = board(stored); + let frame = announced_from_retained_sample(&state, ENTRY); + // REACH-GUARD, on BOTH arms: the record is readable on the CARRYING frame under + // the key the authority builds, and guard (b) therefore withholds the pin. Without + // this the `Accept` arm could be offering through the ORDINARY pin basis, which + // would make the whole row about something else. + assert_eq!( + frame.may_trigger_auto_choice(&key), + Some(stored), + "REACH-GUARD [{stored:?}]: the stored answer must be readable on the carrying \ + frame, not only on `current`" + ); + let entry = frame.stack.back().expect("the announced entry").clone(); + assert!( + entry_publishes_pin_slots(frame, &entry, PlayerId(0)) + .is_none_or(|slots| slots.may.is_none()), + "REACH-GUARD [{stored:?}]: guard (b) must WITHHOLD the `MayChoice` slot for an \ + already-answered gate, so the auto basis is the only thing that can specify \ + this window" + ); + + let (outcome, meter) = + try_offer_bounded_cycle_shortcut_metered(&state, false, ProbeCap::Shipped); + match stored { + AutoMayChoice::Accept => assert!( + outcome.is_ok(), + "CR 603.5: a stored `Accept` makes the per-iteration window the MOST \ + determined a choice can be — it never opens — so gate (6) is specified \ + and the offer stands. got {outcome:?}, meter {meter:?}" + ), + AutoMayChoice::Decline => assert_eq!( + outcome, + Err(BoundedOfferRefusal::UnspecifiedChoiceWindow), + "CR 732.2a: a stored `Decline` is equally prompt-free but produces the \ + OPPOSITE board, so the optional-cleared residual would describe events \ + the shortcut never proposes. Fail closed. meter {meter:?}" + ), + } + } + } + + /// F2a — **ONE AUTHORITY, AND THE TWO ABILITY SHAPES THE THIRD COPY GOT WRONG.** + /// + /// CR 603.5 + CR 608.2d + CR 101.4. Before adoption, three places answered *"does this + /// ability open one up-front optional gate?"*: production's own branch in + /// `resolve_chain_body`, the mint's guard (b), and this module's `auto_may_answer_for`. + /// The latter two asked the same four predicates and OMITTED two conjuncts production has + /// — `optional_for` and the CR 608.2d feasibility probe — so on two ability shapes they + /// called a may "already answered" where production never reads the store at all. + /// + /// This row is that divergence, asserted at the authority. Every arm seeds a stored + /// `Accept` under exactly the key the old copy would have built, so an omitted conjunct + /// shows up as a WRONG ANSWER rather than as an absent one. + /// + /// | arm | one field different | gate | `stored_may_answer` | + /// |---|---|---|---| + /// | (P) plain optional | — | `Some` | `Some(Accept)` | + /// | (O) `optional_for: AnyOpponent` | CR 608.2d fan-out | `None` | **`None`** | + /// | (I) infeasible `RemoveCounter` | zero matching counters | `None` | **`None`** | + /// | (I-pos) the SAME `RemoveCounter`, feasible | one counter on the source | `Some` | `Some(Accept)` | + /// + /// (I-pos) is what keys (I) to FEASIBILITY rather than to the effect discriminant: the two + /// boards differ only in whether the source carries a `+1/+1` counter. (P) is the paired + /// positive for (O). + /// + /// It is also the row that EXERCISES `OptionalFeasibility::Probe` on both of its outcomes + /// — `stored_may_answer` passes `Probe`, so (I) and (I-pos) run the real probe and take + /// opposite branches. Without them the variant would be constructed but never decisive. + /// + /// REVERT-PROBE: delete `optional_for.is_some() ⇒ None` from the authority ⇒ (O) FLIPS. + /// Delete the feasibility conjunct ⇒ (I) FLIPS. Neither touches (P) or (I-pos). + #[test] + fn f2a_the_upfront_gate_authority_answers_the_two_shapes_the_third_copy_omitted() { + use crate::game::effects::{stored_may_answer, upfront_optional_gate, OptionalFeasibility}; + use crate::types::ability::{ + Effect, OpponentMayScope, QuantityExpr, ResolvedAbility, TargetFilter, + TriggerBaseSetInstanceRef, TriggerDefinitionOccurrenceRef, TriggerDefinitionRef, + }; + use crate::types::counter::CounterType; + use crate::types::game_state::{AutoMayChoice, MayTriggerAutoChoiceKey, MayTriggerOrigin}; + use crate::types::identifiers::ObjectIncarnationRef; + + let src = ObjectId(CHURN_SRC); + let origin = MayTriggerOrigin::Definition { + definition_ref: TriggerDefinitionRef { + source: ObjectIncarnationRef::of(src, 0), + occurrence: TriggerDefinitionOccurrenceRef::Printed { + base_set: TriggerBaseSetInstanceRef::INITIAL, + printed_index: 0, + }, + }, + }; + // The key the OLD copy built: `optional_prompt_player` (P0 here) + source + origin. + // Seeded on every arm, so an omitted conjunct is a wrong answer and not a missing one. + let key = MayTriggerAutoChoiceKey { + player: PlayerId(0), + source_id: src, + origin: origin.clone(), + }; + let board = |counters: u32| { + let mut state = drain_state(4); + state.set_may_trigger_auto_choice(key.clone(), AutoMayChoice::Accept); + if counters > 0 { + state + .objects + .get_mut(&src) + .expect("drain_state seats the churn source") + .counters + .insert(CounterType::Plus1Plus1, counters); + } + state + }; + let optional_ability = |effect: Effect| { + let mut ability = ResolvedAbility::new(effect, vec![], src, PlayerId(0)); + ability.optional = true; + ability.may_trigger_origin = Some(origin.clone()); + ability + }; + let draw = || { + optional_ability(Effect::Draw { + count: QuantityExpr::Fixed { value: 1 }, + target: TargetFilter::Controller, + }) + }; + let remove_counter = || { + // `SelfRef` is CR 608.2c's printed-name anaphor: it resolves to the source + // object, so the feasibility probe reads THAT object's counters and the two + // boards below differ in exactly one field. + optional_ability(Effect::RemoveCounter { + counter_type: Some(CounterType::Plus1Plus1), + count: QuantityExpr::Fixed { value: 1 }, + target: TargetFilter::SelfRef, + }) + }; + + let plain = board(0); + assert!( + upfront_optional_gate(&plain, &draw(), OptionalFeasibility::Probe).is_some(), + "(P) MATCHED POSITIVE, asserted first: a plain optional ability DOES open one \ + up-front gate. Without it every `None` below could be a broken authority" + ); + assert_eq!( + stored_may_answer(&plain, &draw()), + Some(AutoMayChoice::Accept), + "(P) …and the stored preference answers it" + ); + + let mut fanned = draw(); + fanned.optional_for = Some(OpponentMayScope::AnyOpponent); + assert!( + upfront_optional_gate(&plain, &fanned, OptionalFeasibility::Probe).is_none(), + "(O) CR 608.2d + CR 101.4: an `optional_for` ability opens an APNAP CASCADE of up \ + to one window PER LIVING PLAYER, not one up-front gate — production returns at \ + the fan-out before the gate is reached at all" + ); + assert_eq!( + stored_may_answer(&plain, &fanned), + None, + "(O) THE DIVERGENCE: the store holds an `Accept` under exactly the key the third \ + copy built, and the answer is still `None`, because the gate that preference \ + would answer never opens" + ); + + assert!( + upfront_optional_gate(&plain, &remove_counter(), OptionalFeasibility::Probe).is_none(), + "(I) CR 608.2d: \"a player can't choose an impossible option\" — with zero matching \ + counters the optional removal opens no window" + ); + assert_eq!( + stored_may_answer(&plain, &remove_counter()), + None, + "(I) THE SECOND DIVERGENCE, on the same seeded store" + ); + + let stocked = board(1); + assert!( + upfront_optional_gate(&stocked, &remove_counter(), OptionalFeasibility::Probe) + .is_some(), + "(I-pos) THE FEASIBILITY CONTROL: the SAME ability on a board one counter \ + different DOES open its gate. This is what keys (I) to feasibility rather than \ + to the effect discriminant — and it is the arm that proves \ + `OptionalFeasibility::Probe` reaches a decision, not merely a construction" + ); + assert_eq!( + stored_may_answer(&stocked, &remove_counter()), + Some(AutoMayChoice::Accept), + "(I-pos) …and the same stored preference now answers it" + ); + + // `Known` is the mode production uses, and it must OVERRIDE the probe rather than + // re-run it — otherwise adoption A would pay the clone twice on every resolve. + assert!( + upfront_optional_gate( + &stocked, + &remove_counter(), + OptionalFeasibility::Known(true) + ) + .is_none(), + "`Known(true)` suppresses the gate on a board the probe would call FEASIBLE, so \ + the caller's already-computed answer is what is used" + ); + assert!( + upfront_optional_gate(&plain, &remove_counter(), OptionalFeasibility::Known(false)) + .is_some(), + "…and `Known(false)` admits it on a board the probe would call INFEASIBLE. The \ + pair proves the probe is not re-run under `Known`" + ); + } + + /// F2b — **GUARD (b) WITHHOLDS A PIN THE CR 603.5 GATE CAN NEVER SPEND.** + /// + /// CR 732.2a + CR 608.2d. The mint publishes a `MayChoice` slot so a declaration can pin + /// the ONE up-front window an entry opens. Before adoption it minted that slot for two + /// shapes that open no such window: an `optional_for` fan-out (an APNAP cascade of up to + /// one window per living player — one slot standing for N prompts is exactly the + /// cardinality defect group (c) already argues against) and an infeasible optional (a pin + /// the gate can never spend, invisible even to a fail-closed inject arm). + /// + /// THE FIXTURE IS UNSEEDED ON PURPOSE. Every arm carries `may_trigger_origin: None`, so + /// guard (b)'s store conjunct is vacuously true on both the old predicate and the new one + /// and the ONLY thing that can move `may` is `optional_for` / feasibility. A SEEDED variant + /// is explicitly rejected: a stored answer makes the store conjunct false on every arm, + /// `may` is `None` for the stored-answer reason throughout, and the axis under test cannot + /// move at all. + /// + /// | arm | one field different | published `may` | + /// |---|---|---| + /// | (P) plain optional drain | — | **`Some`** | + /// | (O) `optional_for: AnyOpponent` | CR 608.2d fan-out | **`None`** | + /// | (I) infeasible optional `RemoveCounter` | zero matching counters | **`None`** | + /// | (I-pos) the SAME entry, feasible | one counter on the source | **`Some`** | + /// + /// Direction: strictly FEWER offers, never more. + /// + /// REVERT-PROBE: delete `optional_for.is_some() ⇒ None` from the authority ⇒ (O) publishes + /// ⇒ FLIPS. Delete the feasibility conjunct ⇒ (I) publishes ⇒ FLIPS. (P) and (I-pos) are + /// the paired positives that keep both negatives out of "the mint publishes nothing". + #[test] + fn f2b_guard_b_withholds_a_pin_the_cr_603_5_gate_can_never_spend() { + use crate::game::engine::entry_publishes_pin_slots; + use crate::types::ability::{ + Effect, OpponentMayScope, QuantityExpr, ResolvedAbility, TargetFilter, + }; + use crate::types::counter::CounterType; + + let src = ObjectId(CHURN_SRC); + let board = |counters: u32| { + let mut state = drain_state(4); + if counters > 0 { + state + .objects + .get_mut(&src) + .expect("drain_state seats the churn source") + .counters + .insert(CounterType::Plus1Plus1, counters); + } + state + }; + let published_may = |state: &GameState, entry: &StackEntry| -> bool { + // REACH-GUARD baked into the reader: the entry must carry NO stored preference, so + // guard (b)'s store conjunct cannot be what moves the answer. + assert!( + entry + .ability() + .is_some_and(|a| a.may_trigger_origin.is_none()), + "UNSEEDED FIXTURE: an arm with a `may_trigger_origin` could be answered by the \ + store conjunct and the axis under test would be dominated" + ); + entry_publishes_pin_slots(state, entry, PlayerId(0)) + .is_some_and(|slots| slots.may.is_some()) + }; + + let plain = board(0); + let p_entry = optional_drain(20); + assert!( + published_may(&plain, &p_entry), + "(P) MATCHED POSITIVE, asserted first: a plain optional drain publishes its \ + CR 603.5 gate. Without it every withholding below is indistinguishable from a \ + mint that publishes nothing" + ); + + let o_entry = { + let mut ability = p_entry + .ability() + .expect("the drain is a triggered ability") + .clone(); + ability.optional_for = Some(OpponentMayScope::AnyOpponent); + churn_entry(21, 0, ability, None) + }; + assert!( + !published_may(&plain, &o_entry), + "(O) CR 608.2d + CR 101.4 + CR 732.2a: a fan-out `may` is not ONE window — it is \ + an APNAP cascade of up to one window per living player, and a shortcut must \ + describe THE sequence of choices. One published slot cannot stand for N prompts" + ); + + let remove_counter_entry = |id: u64| { + // Shape (B), may-only: no declared target, so `build_target_slots` surfaces + // nothing and the entry publishes its CR 603.5 gate alone. + let mut ability = ResolvedAbility::new( + Effect::RemoveCounter { + // CR 608.2c `SelfRef`: the probe reads the SOURCE's counters, which is + // the one field (I) and (I-pos) differ in. + counter_type: Some(CounterType::Plus1Plus1), + count: QuantityExpr::Fixed { value: 1 }, + target: TargetFilter::SelfRef, + }, + vec![], + src, + PlayerId(0), + ); + ability.optional = true; + churn_entry(id, 0, ability, None) + }; + assert!( + !published_may(&plain, &remove_counter_entry(22)), + "(I) CR 608.2d: an infeasible optional opens no window at all, so a slot minted \ + for it is a pin the gate can never spend — invisible even to a fail-closed \ + inject arm, which is why the mint has to refuse it here" + ); + assert!( + published_may(&board(1), &remove_counter_entry(23)), + "(I-pos) THE FEASIBILITY CONTROL: the byte-identical entry on a board one counter \ + different DOES publish. (I) is therefore about feasibility and not about the \ + effect discriminant or the shape-(B) route" + ); + } + /// R27 (c) — THE SCOPE-BINDING AXIS: A CR 603.4 INTERVENING-IF ON A RETAINED SAMPLE BINDS /// WITH ITS TRIGGER SOURCE. /// diff --git a/crates/engine/src/game/effects/mod.rs b/crates/engine/src/game/effects/mod.rs index 0c5b7943de..bab5100fb5 100644 --- a/crates/engine/src/game/effects/mod.rs +++ b/crates/engine/src/game/effects/mod.rs @@ -5955,6 +5955,116 @@ fn optional_effect_is_infeasible(state: &GameState, ability: &ResolvedAbility) - } } +/// CR 608.2d: how a caller supplies the feasibility fact [`upfront_optional_gate`]'s LAST +/// conjunct needs. +/// +/// `resolve_chain_body` has ALREADY run the probe by the time it reaches the gate — it needs +/// the value for the `CastFromZone` decline early-return that precedes both the CR 101.4 +/// fan-out and the gate — so it passes [`OptionalFeasibility::Known`] and production never +/// probes twice. That matters: [`optional_effect_is_infeasible`]'s `CastFromZone` arm clones +/// the whole `GameState` per bound object and runs a full `cast_from_zone::resolve` dry-run. +/// Every other caller passes [`OptionalFeasibility::Probe`], which runs only after the cheap +/// conjuncts have all passed. +/// +/// A TWO-VARIANT DOMAIN ENUM RATHER THAN `Option`, and the reason is naming, not +/// CLAUDE.md's `bool` prohibition (`Option` is on its approved list): `Known(bool)` says +/// *"the caller already ran the probe and this is its answer"* while `Probe` says *"run it +/// here, after the cheap conjuncts"*. With `Option`, `None` would mean "probe here" only +/// by convention — undocumented at every call site and indistinguishable from "no opinion". +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum OptionalFeasibility { + /// The caller ran [`optional_effect_is_infeasible`] and hands its answer over. + Known(bool), + /// Run the probe here, LAST — after every cheap conjunct has passed. + Probe, +} + +/// CR 603.5 + CR 608.2c + CR 608.2d + CR 603.12a — THE single authority for *"does this +/// ability open ONE up-front optional gate, and to whom, under which key?"* +/// +/// `None` ⇒ no up-front gate opens at all. Four disjoint reasons, in the order they are +/// evaluated: +/// +/// 1. not `optional`; +/// 2. `optional_for` is set — the CR 608.2d + CR 101.4 fan-out prompts eligible players in +/// APNAP order instead, which is a CASCADE of up to one window per living player and not +/// one gate (`resolve_chain_body` returns at that fan-out before ever reaching the gate; +/// see the coupling note there); +/// 3. one of the three `repeat_for` shapes that re-fire optionality PER ITERATION +/// (CR 608.2c + CR 608.2d + CR 603.12a); +/// 4. an infeasible optional (CR 608.2d: "a player can't choose an impossible option"). +/// +/// **THE FEASIBILITY PROBE IS THE LAST CONJUNCT, AND THAT ORDERING IS A GUARANTEE, NOT AN +/// IMPLEMENTATION ACCIDENT.** `engine::entry_publishes_pin_slots` calls this once per announced +/// entry, per candidate window, per beat, where production pays it once per resolution. LAST +/// ordering restricts the clone-bearing arm to `optional ∧ ¬optional_for ∧ ¬repeat ∧ +/// Effect::CastFromZone` entries — a strict subset of the population production already pays +/// for. It is deliberately NOT charged against `PROBE_BUDGET`: that counter bounds CR 732.2a +/// certification ASKS at the verdict door, and putting wall-clock cost on the same counter +/// would re-base every metered row's pinned spend and make neither number readable. +pub(crate) struct UpfrontOptionalGate { + /// CR 608.2d: [`optional_prompt_player`] names who ANNOUNCES it — not always the controller. + pub prompt_player: PlayerId, + /// `None` ⇒ the ability carries no `may_trigger_origin`, so no stored preference can key + /// on it. That is not the same as "no preference stored": it is "no key exists". + pub key: Option, +} + +pub(crate) fn upfront_optional_gate( + state: &GameState, + ability: &ResolvedAbility, + feasibility: OptionalFeasibility, +) -> Option { + if !ability.optional || ability.optional_for.is_some() { + return None; + } + // CR 608.2c + CR 608.2d + CR 603.12a: the three shapes that SUPPRESS the single up-front + // gate and fire optionality per iteration instead. + if has_kind_driven_repeat(ability) + || has_member_driven_repeat_after_hydration(state, ability) + || is_repeated_optional_payment(ability) + { + return None; + } + let infeasible = match feasibility { + OptionalFeasibility::Known(known) => known, + OptionalFeasibility::Probe => optional_effect_is_infeasible(state, ability), + }; + if infeasible { + return None; + } + let prompt_player = optional_prompt_player(state, ability); + Some(UpfrontOptionalGate { + prompt_player, + key: ability + .may_trigger_origin + .clone() + .map(|origin| MayTriggerAutoChoiceKey { + player: prompt_player, + source_id: ability.source_id, + origin, + }), + }) +} + +/// CR 603.5: is that gate ALREADY ANSWERED by a stored "don't ask again" preference? +/// +/// The CONSUMER half of [`upfront_optional_gate`], so the mint's suppression, the analysis's +/// relief and production's own early return can no longer disagree about which mays are +/// answered. `None` ⇒ the gate will PROMPT, or there is no gate, or the ability carries no +/// `may_trigger_origin` for a preference to key on — all three are unspecified windows, which +/// is the fail-closed direction for every consumer. +/// +/// Passes [`OptionalFeasibility::Probe`]: a caller asking "is this already answered?" has by +/// definition not run the feasibility probe itself. +pub(crate) fn stored_may_answer( + state: &GameState, + ability: &ResolvedAbility, +) -> Option { + let gate = upfront_optional_gate(state, ability, OptionalFeasibility::Probe)?; + state.may_trigger_auto_choice(gate.key.as_ref()?) +} + /// CR 603.12a + CR 608.2c: True when this ability is a "you may pay {cost} up to /// N times. When you do, [reflexive]" process (Hawkeye, Master Marksman — "Trick /// Arrows"). Unlike a generic `repeat_for` loop (one up-front "you may" then N @@ -6533,8 +6643,8 @@ pub(crate) fn resolve_player_for_context_ref( ability.controller } -/// CR 117.3a: Determine which player receives the "may" prompt for an optional -/// effect. Most optional effects go to the caster (CR 608.2d). Subject-anchored +/// CR 608.2d: Determine which player ANNOUNCES the choice — receives the "may" +/// prompt — for an optional effect. Most go to the caster. Subject-anchored /// optional effects — "its controller may search their library" (Assassin's /// Trophy, Path to Exile, Ghost Quarter, Oblation, …) — route the prompt to the /// acting subject (the target permanent's controller). This mirrors the @@ -9205,6 +9315,13 @@ fn resolve_chain_body( // affected player of the resolving replaced event (Zur's Weirding). if ability.optional { if let Some(scope) = ability.optional_for { + // COUPLING, recorded: `upfront_optional_gate` encodes this same fan-out + // pre-emption as `optional_for.is_some() ⇒ None`. The two agree because + // THIS returns first, not because either derives from the other. Moving + // or weakening this early return silently changes what the authority + // means at the gate below (CR 608.2d + CR 101.4). The `debug_assert!` at + // the gate is the executable half of this note. + // // Exhaustive match: there is no compiler exhaustiveness guard at the // other OpponentMayScope consumers, so this serves as the manual // guard. Adding a variant forces a decision here. @@ -9278,23 +9395,38 @@ fn resolve_chain_body( // may" PER iteration via `drive_repeated_optional_payment`, not once up // front — suppress the single gate here exactly as the kind/member-driven // loops do. - if ability.optional - && !has_kind_driven_repeat(ability) - && !has_member_driven_repeat_after_hydration(state, ability) - && !is_repeated_optional_payment(ability) - && !optional_is_infeasible - { + // + // ADOPTION A: this branch IS `upfront_optional_gate`. The conjunct set is not restated + // here — that is what makes the function an authority rather than a fourth copy. The + // feasibility fact is handed over as `Known`, because `optional_is_infeasible` was + // already computed above for the `CastFromZone` decline early-return, and a re-probe + // would run the clone-bearing arm twice on production's hot resolve path. + if let Some(gate) = upfront_optional_gate( + state, + ability, + OptionalFeasibility::Known(optional_is_infeasible), + ) { + // The executable half of the `optional_for` coupling note above: this branch is + // reachable only because the CR 101.4 fan-out already returned, so the authority's + // `optional_for.is_some() ⇒ None` conjunct can never be the thing that admits an + // ability here. MEASURED across the whole `--lib` suite with an `unreachable!` in + // this position: zero firings. + debug_assert!( + ability.optional_for.is_none(), + "CR 608.2d + CR 101.4: the fan-out early return must have taken every \ + `optional_for` ability before the up-front gate" + ); let description = ability.description.clone(); - let prompt_player = optional_prompt_player(state, ability); - let may_trigger_key = - ability - .may_trigger_origin - .clone() - .map(|origin| MayTriggerAutoChoiceKey { - player: prompt_player, - source_id: ability.source_id, - origin, - }); + let UpfrontOptionalGate { + prompt_player, + key: may_trigger_key, + } = gate; + // Deliberately the DIRECT store read rather than `stored_may_answer`, and this is + // not a duplicated authority: the KEY is what has to be built in one place, and it + // was — by `upfront_optional_gate`, above. `stored_may_answer` would re-enter the + // authority with `Probe` and run the feasibility clone a second time, which is the + // exact defect `OptionalFeasibility` exists to prevent. Same key, same store, same + // answer, one probe. if let Some(ref key) = may_trigger_key { if let Some(choice) = state.may_trigger_auto_choice(key) { resolve_optional_effect_decision( diff --git a/crates/engine/src/game/engine.rs b/crates/engine/src/game/engine.rs index 34a0a50aa3..6911c2d464 100644 --- a/crates/engine/src/game/engine.rs +++ b/crates/engine/src/game/engine.rs @@ -1981,6 +1981,37 @@ fn bounded_cycle_offer( outcome } +/// CR 732.2a: THE candidate walk — newest-first over `idx`, one item per candidate pair, +/// `span = live.len() - 1 - idx` in RETAINED RING FRAMES, `span >= 1`. +/// +/// PRODUCTION'S walk, exposed so its test-side consumers CONSUME it instead of imitating it. A +/// row that hard-codes `&live[live.len() - 2..]` is asserting `span == 1` without saying so, +/// and reads a HALF PERIOD the moment the sampling rate moves — which is exactly what the +/// answer-beat sampler did to two of them. +/// +/// A span of 0 is the pair `state` against its own snapshot. It is already refused by +/// `net_progress_for` on the resulting zero delta in every production trajectory, but it is +/// refused HERE too, explicitly: `materialize_fixed_shortcut` DELIMITS a committed cycle by +/// this count, and a published `0` would mean "one repetition spans no frames", which no drive +/// can honour. Filtered BEFORE the window is yielded — `span >= 1` is `window.len() >= 2` +/// identically — so a degenerate window never reaches a touch or a mint. +/// +/// TWO LIFETIMES, not one. `certified_bounded_cycle_offer` carries a `PeriodTouch<'a>` OUT of +/// the loop, so the ELEMENT lifetime must survive independently of the borrow of the slice; +/// that is what `certified_period_touch(window: &[&'a GameState], current: &'a GameState) -> +/// PeriodTouch<'a>` already requires. +pub(crate) fn candidate_windows<'w, 'a>( + ring_live: &'w [&'a GameState], +) -> impl Iterator + 'w { + (0..ring_live.len()) + .rev() + .map(move |idx| { + let span = (ring_live.len() - 1 - idx) as u32; + (idx, span, &ring_live[idx..]) + }) + .filter(|&(_, span, _)| span >= 1) +} + /// CR 732.2a: certification (step 4/4b), the choice gate and the bound — everything that can /// ask the verdict door, split out so its caller owns exactly one meter snapshot. #[allow(clippy::too_many_arguments)] @@ -2010,28 +2041,13 @@ fn certified_bounded_cycle_offer<'a>( PeriodTouch<'_>, PeriodicDelta, )> = None; - for idx in (0..ring.len()).rev() { - // The span, in RETAINED RING FRAMES, that this candidate pair covers. - // `ring.last()` is the sample `pass_priority_once_with_pipeline` recorded at THIS - // beat, before the bridge ran, so the newest frame is the current state and the - // span from `ring[idx]` is `len - 1 - idx`. - // - // A span of 0 is the pair `state` against its own snapshot. It is already refused - // by `net_progress_for` on the resulting zero delta in every production - // trajectory, but it is refused HERE too, explicitly: `materialize_fixed_shortcut` - // now DELIMITS a committed cycle by this count, and a published `0` would mean - // "one repetition spans no frames", which no drive can honour. Fail closed on the - // degenerate pair rather than rely on a downstream conjunct to catch it. - // - // EVALUATED FIRST, before the window is built, touched or minted from — `span >= 1` - // is `window.len() >= 2` identically, so this guard is also what keeps a degenerate - // window out of the touch and the mint. - let span = ring.len() - 1 - idx; - if span < 1 { - continue; - } + // The walk itself — its ORDER, its span arithmetic and its degenerate-pair filter — lives + // in `candidate_windows`, so the rows that need production's candidates take THE SAME + // iterator rather than a copy of it. `ring` and `ring_live` are the two halves of the same + // frames and therefore the same length, so indexing the comparand by the walk's `idx` is + // the pairing it always was. + for (idx, span, window) in candidate_windows(ring_live) { let prior = ring[idx]; - let window = &ring_live[idx..]; // Built under `BoardCovered` unconditionally, because step 4 does not yet know which // disjunct will match; step 4b keeps it or rebuilds it. let touch_cover = certified_period_touch(window, state, PeriodCertification::BoardCovered); @@ -2089,7 +2105,7 @@ fn certified_bounded_cycle_offer<'a>( // `interactive_3p_subset_lethal_does_not_crown` fixture's repetition // spans TWO frames (a gain-life resolution then a lose-life one), and // under the old hardcode its accepted drive committed nothing at all. - frames_per_period: span as u32, + frames_per_period: span, delta, victim_slot: Vec::new(), }, @@ -2238,9 +2254,14 @@ fn certified_bounded_cycle_offer<'a>( // CR 704.5a: what ONE repetition charges to whichever seat a slot's pin names. The // max-vs-sum reasoning, the gain clamp and the fail-closed direction live on the // function; `elimination_bounds` then sums the published slots per declarable victim. - // Extracted rather than inlined so the fork has a callable seam — `victim_slot` is empty - // on every trajectory that offers today, so this value is dropped in production and only - // `worst_seat_life_loss_is_the_max_seat_never_the_sum` discriminates max from sum. + // Extracted rather than inlined so the fork has a callable seam. ⚠ THE "`victim_slot` IS + // EMPTY ON EVERY TRAJECTORY THAT OFFERS TODAY" NOTE THAT STOOD HERE IS FALSIFIED, and is + // replaced rather than softened: the answer-beat sampling site in `apply_action` announces + // the entries a FORCED pre-priority window puts on the stack, and a CR 608.2b `Targets` + // declaration is exactly the shape that resolves across one. On the F4 boards `points` now + // carries Torch's `Targets` point, so this value is NOT dropped — it reaches + // `elimination_bounds` in production and `r1_the_bounded_offer_fires_on_the_real_f4_dump` + // re-derives the published bound with a non-zero declared term. let worst_seat_life_loss: i64 = periodic.delta.worst_seat_life_loss(); periodic.victim_slot = points .iter() @@ -2589,7 +2610,11 @@ pub(crate) fn entry_publishes_pin_slots( // it does NOT bound who the resolver ASKS, nor WHETHER it asks, nor HOW MANY TIMES. // Three mint-time conjunct groups, all FAIL-CLOSED pre-filters on the ONE gate a // `MayChoice` pin is for — the CR 603.5 gate inside `resolve_chain_body` - // (`effects/mod.rs`, the `if ability.optional && !has_kind_driven_repeat(..)` block). + // (`effects/mod.rs`). ⚠ GROUPS (a) AND (c) ARE NO LONGER RESTATED HERE: they, plus the + // `optional_for` and feasibility conjuncts this mint used to OMIT, now live in + // `effects::upfront_optional_gate`, which is the same function production's own branch + // takes. The prose below stays because it records WHY each group is load-bearing; the + // code below asks the authority for all of them at once. // THIS IS THE ONE PLACE `may` IS MINTED, so the guards cover shape (A) and shape (B) // together rather than being restated per shape. Soundness over the OTHER FOUR // production producers of `WaitingFor::OptionalEffectChoice` is NOT claimed here; it is @@ -2616,21 +2641,31 @@ pub(crate) fn entry_publishes_pin_slots( // `Draw` / `Token` of that shape would otherwise mint ONE slot for N prompts. Ask // production's own three predicates rather than re-deriving them here, which is // the same authority-sharing rule (a) follows. - let may = (ability.optional - && crate::game::effects::optional_prompt_player(state, ability) == proposer - && !crate::game::effects::has_kind_driven_repeat(ability) - && !crate::game::effects::has_member_driven_repeat_after_hydration(state, ability) - && !crate::game::effects::is_repeated_optional_payment(ability) - && ability.may_trigger_origin.as_ref().is_none_or(|origin| { - state - .may_trigger_auto_choice(&crate::types::game_state::MayTriggerAutoChoiceKey { - player: proposer, - source_id: ability.source_id, - origin: origin.clone(), - }) - .is_none() - })) - .then(|| DecisionSlot { + // ADOPTION B. All four groups are `effects::upfront_optional_gate`'s, asked of the ONE + // function `resolve_chain_body`'s own branch is, so the mint and the gate cannot drift. + // `Probe` is the right mode here: this caller has NOT run the probe (production's `Known` + // belongs to a resolve that is not happening yet) and the authority evaluates it LAST, so the + // clone-bearing `CastFromZone` arm needs `optional ∧ ¬optional_for ∧ ¬repeat`. MEASURED on a + // full `--test integration` run: 16402 mints ⇒ 4573 probes ⇒ 0 arm entries (59 via `Known`). + // + // BEHAVIOUR CHANGE, and it is rules-correct in the fail-closed direction: this now + // withholds the slot for an `optional_for` ability (CR 608.2d + CR 101.4 — a fan-out is an + // APNAP cascade of up to one window PER LIVING PLAYER, and one published slot standing for + // N prompts is the cardinality defect group (c) already argues against) and for an + // infeasible optional (which opens no window at all, so a slot for it is a pin the gate + // can never spend). Direction: strictly FEWER offers, never more. + let may = crate::game::effects::upfront_optional_gate( + state, + ability, + crate::game::effects::OptionalFeasibility::Probe, + ) + .filter(|gate| gate.prompt_player == proposer) + .filter(|gate| { + gate.key + .as_ref() + .is_none_or(|key| state.may_trigger_auto_choice(key).is_none()) + }) + .map(|_| DecisionSlot { source: source.clone(), index: 1, }); @@ -3268,6 +3303,33 @@ enum CycleOutcome { Abort, } +/// CR 732.2a: THE FRAME DELIMITER — one published repetition is `k` retained ring frames. +/// +/// The SINGLE AUTHORITY for "has the published period elapsed?". `drive_one_shortcut_cycle` +/// has to answer that question in two arms — the active-player settle arm and the +/// forced-window ANSWER arm — and both arms are places a frame can be recorded now that +/// `apply_action` carries a second sampling site. Two inline copies of +/// `frames_per_period.is_some_and(|k| frames_this_cycle >= k)` would be two places to get the +/// comparison wrong, in a predicate whose `>=` vs `==` and whose `None` arm are both +/// load-bearing (see `published_period_elapsed_is_total_over_the_axes_that_delimit_a_cycle`). +/// +/// `None` ⇒ NEVER elapsed. An offer whose producer states no per-period signature publishes +/// no frame count, and a drive must not invent one: such a cycle is delimited by board +/// recurrence alone, exactly as it was before this delimiter existed. That is the fail-closed +/// direction — a `true` here ends a cycle, and ending one early commits a FRACTION of the +/// published delta, which is the conditional action CR 732.2a forbids outright. +/// +/// `>=`, not `==`: a single beat may retain more than one frame, and a cycle that overshot `k` +/// has still elapsed. An `==` would drive past its own boundary and only stop at the beat cap. +/// +/// Beat-kind agnostic BY CONSTRUCTION — it reads only the counter the ring itself advanced, so +/// it is valid at every beat where a frame can be recorded. The two board-recurrence predicates +/// are deliberately NOT folded in: `GameState::normalize_for_loop`'s contract rests on +/// `waiting_for` being `Priority` at the sample point, so they stay in the settle arm. +fn published_period_elapsed(frames_this_cycle: u32, frames_per_period: Option) -> bool { + frames_per_period.is_some_and(|k| frames_this_cycle >= k) +} + /// PR-7 Combo-UI Stage 2: drive ONE whole cycle of a confirmed loop shortcut on a fresh clone /// of `committed`, seeded to the canonical settle beat (`Priority{active_player}`, the same /// beat the detector ring samples). Recurrence is detected against `boundary` (normalized). @@ -3293,12 +3355,17 @@ enum CycleOutcome { /// the beat cap (`Abort`, committing zero cycles) or by crossing lethal, and the declared `n` /// is inert: `Fixed(1)` and `Fixed(3)` produce byte-identical boards. /// -/// The frame count is the same quantity `frames_per_period` names, measured the same way: the -/// single `record_loop_detect_sample` call site lives in `pass_priority_once_with_pipeline`, -/// which is the very function this loop steps, so a driven beat samples the ring under exactly -/// the gates an observed beat does. A new frame is detected by `Arc` identity of the ring's -/// back rather than by length, because the ring evicts at `LOOP_DETECT_RING_CAP` and a length -/// delta reads 0 once it is full. +/// The frame count is the same quantity `frames_per_period` names, measured the same way: this +/// loop steps `pass_priority_once_with_pipeline` and answers its prompts through +/// `apply_action`, which are exactly the two functions the OBSERVED drive samples the ring in, +/// so a driven beat samples under exactly the gates an observed beat does. ⚠ THAT IS TWO +/// SAMPLING SITES, NOT ONE — the note that stood here named only the settle sampler, and the +/// forced-window ANSWER site falsifies it. Which is why the frame counter is advanced in the +/// ANSWER arm too: a period whose extra frames are recorded at answer beats would otherwise +/// never reach `k`, and `frames_per_period` would be unreachable exactly on the boards the +/// widening was for. A new frame is detected by `Arc` identity of the ring's back rather than +/// by length, because the ring evicts at `LOOP_DETECT_RING_CAP` and a length delta reads 0 +/// once it is full. fn drive_one_shortcut_cycle( committed: &GameState, boundary: &GameState, @@ -3339,9 +3406,11 @@ fn drive_one_shortcut_cycle( } // Active-player settle beat: cycle complete iff the board recurred (constant-depth // equal-modulo-resources OR ω-covering growth) or the published period's worth of - // ring frames has elapsed. This is the ONLY beat kind the ring samples at (the - // sampler's own gate is `Priority{player == active_player}`), so the frame counter - // is advanced here and nowhere else. + // ring frames has elapsed. NOT the only beat kind the ring samples at — the + // forced-window ANSWER arm below reaches `apply_action`'s second sampling site, so + // it advances the same counter. Both arms key the advance on the ring's BACK + // ALLOCATION actually changing rather than on the beat kind, which is what keeps + // the drive's frame count equal to the mint's on either path. Ok(WaitingFor::Priority { player }) if player == work.active_player => { ev.append(&mut beat_events); let ring_back_after = work.loop_detect_ring.back().map(std::sync::Arc::as_ptr); @@ -3351,7 +3420,7 @@ fn drive_one_shortcut_cycle( let norm = work.normalize_for_loop(); if crate::analysis::resource::loop_states_equal_modulo_resources(boundary, &norm) || crate::analysis::resource::loop_states_cover_modulo_growth(boundary, &norm) - || frames_per_period.is_some_and(|k| frames_this_cycle >= k) + || published_period_elapsed(frames_this_cycle, frames_per_period) { return CycleOutcome::Recurred { state: Box::new(work), @@ -3370,7 +3439,20 @@ fn drive_one_shortcut_cycle( Ok(other) => { ev.append(&mut beat_events); match inject_pinned_answer(&mut work, template, iteration, &other) { - Ok(()) => continue, + Ok(()) => { + let ring_back_after = + work.loop_detect_ring.back().map(std::sync::Arc::as_ptr); + if ring_back_after.is_some() && ring_back_after != ring_back_before { + frames_this_cycle += 1; + } + if published_period_elapsed(frames_this_cycle, frames_per_period) { + return CycleOutcome::Recurred { + state: Box::new(work), + events: ev, + }; + } + continue; + } Err(RecastAbort) => return CycleOutcome::Abort, } } @@ -6743,10 +6825,12 @@ fn apply_action( // so an action-keyed list could not have expressed the class correctly at all. // `PassPriority` keeps its own action-side exemption because it is answered at a // `Priority` window, which is deliberately NOT in the forced class. + let answering_forced_window = state.waiting_for.is_forced_cascade_window(); + let stack_len_before_action = state.stack.len(); if !matches!( action, GameAction::PassPriority | GameAction::OrderTriggers { .. } - ) && !state.waiting_for.is_forced_cascade_window() + ) && !answering_forced_window { state.loop_detect_ring.clear(); } @@ -11062,7 +11146,52 @@ fn apply_action( triggers_processed_inline, skip_deferred_trigger_drain, )?; - state.waiting_for = wf.clone(); + // CR 732.2a: the SECOND sampling site — a stack entry announced while a player + // answers a FORCED pre-priority window. + // + // NOT "the settle sampler's conjuncts PLUS the window flag". The two sets are the + // same SIZE, one member apart: `answering_forced_window` (captured before the + // reducer consumed the window) REPLACES the settle sampler's `resolved_this_beat`. + // Everything else is shared — `!in_simulation_probe()`, `samples()`, + // `!stack.is_empty()`, the non-shrinking `len >= before`, and + // `Priority{active_player}`. + // + // The settle sampler's `else { ring.clear() }` has NO counterpart here, and that is + // deliberate: this site is not a settle verdict on the beat, it is an additive + // observation of entries a forced window announced, so a miss must leave the + // accumulation alone rather than wipe it. CONSEQUENCE, accepted: a forced-window + // answer that resolves nothing but leaves the stack non-shrinking records a frame + // whose stack duplicates its predecessor's. That costs one ring slot and a zero + // frame-delta; it cannot manufacture a period, because `ring_delta_signature` refuses + // a zero smallest-period delta outright, and it cannot desynchronize the count, + // because MINT AND DRIVE ARE SYMMETRIC — `drive_one_shortcut_cycle` answers its prompts + // through `inject_pinned_answer`: three of its FOUR arms dispatch `apply_action` and walk + // this very branch, advancing `frames_this_cycle`; the fourth `Err`s before any advance. + // + // ORDERING, NOW SYNCHRONIZED (maintainer call on PR #7005; previously carried here + // as a documented latent asymmetry). `game::public_state::sync_waiting_for` is the + // canonical synchronizer — it installs `wf`, runs the legacy-attach normalization, + // and recomputes `priority_player` through `turn_control`'s authorized-submitter + // resolver — and it now runs BEFORE the record, exactly as the settle sampler in + // `pass_priority_once_with_pipeline` does. So a frame minted here carries the same + // `waiting_for`/`priority_player` pair a settle frame carries, and that homogeneity + // is load-bearing: `impl PartialEq for GameState` compares both fields and + // `normalize_for_loop` neutralizes neither, so a mixed ring would break + // `ring_delta_signature`'s turn-position conjunct. BLAST RADIUS IS THE RING ONLY — + // `apply_action_boundary` re-syncs the returned `wf` before the result leaves the + // engine, so the settled state is unchanged. MEASURED before the reorder: a + // `debug_assert_eq!` census on both fields reported 0 divergences over 18,486 lib + + // 4,487 integration rows, so this replaces a coincidence with a guarantee. + sync_waiting_for(state, &wf); + if answering_forced_window + && !in_simulation_probe() + && state.loop_detection.samples() + && !state.stack.is_empty() + && state.stack.len() >= stack_len_before_action + && matches!(wf, WaitingFor::Priority { player } if player == state.active_player) + { + state.record_loop_detect_sample(); + } return Ok(ActionResult { events, waiting_for: wf, @@ -15210,6 +15339,38 @@ mod stage2_injector_tests { // their new coordinates AND still inside the same enclosing functions // (`drive_sequential_repeated_optional_payment` ×2, `resolve_chain_body`), // which is stronger evidence than the coordinate alone. + // THIS PR, REBASED ONTO UPSTREAM `b654513cb` (#6996, #6999, #6998, #7001, + // #6997, #6946): `:6065/:6142/:9324 ⇒ :6175/:6252/:9456`. The three pins + // it replaces were UPSTREAM's own literals, correct for the upstream tree + // — verified by re-deriving them at `b654513cb`, where all three sit + // exactly there — so this shift is THIS BRANCH's commits replayed on top, + // i.e. LOCAL, and the CI-vs-local diagnosis in the header does not apply. + // The shift is NOT UNIFORM (`+110/+110/+132`), and that asymmetry is the + // measurement rather than a puzzle: `git diff -U0 b654513cb HEAD` on this + // file has exactly four hunks. `@@ -5957,0 +5958,110 @@` — C1's + // `upfront_optional_gate` authority plus `OptionalFeasibility` — lands + // above ALL THREE producers and is the whole `+110`. The third producer + // takes a further `+22` from two hunks INSIDE `resolve_chain_body` and + // above its own gate: `@@ -9207,0 +9318,7 @@` (the `optional_for` fan-out + // coupling note) and `@@ -9281,6 +9398,21 @@` (adoption A — the inline + // conjunct chain replaced by the `upfront_optional_gate` call and its + // `debug_assert!`); the fourth hunk is net `0`. Whole-file delta is also + // `+132`, so nothing was added below the third producer, and predicted + // `6065+110`, `6142+110`, `9324+132` equal the observed coordinates + // exactly. Identity re-established, not assumed: each producer at its new + // coordinate is sha256-identical to `b654513cb:effects/mod.rs` at its old + // one (`9869a19f…9b43a2`, `2bc316e3…e861185`, `3134c156…2aeeb66`) + // and to the pre-rebase tip `117baa6a1` at + // `:6109/:6186/:9183`, AND each is still inside the enclosing function + // this row NAMES — `drive_sequential_repeated_optional_payment`, + // `resolve_repeated_optional_payment_choice`, `resolve_chain_body`. The + // diff instrument discriminates: in the NEW tree the three OLD coordinates + // hold a `may_trigger_auto_choice` lookup, a blank line, and a bare `//`, + // none of which mints anything. Set preservation: the two asserts above + // this one ran FIRST and both fired GREEN on the run that caught this — + // total still **37**, partition still **5/7/25** — and the other two + // entries (`scoped_library_search.rs:452`, `engine.rs:11549`) did not move + // at all, both re-read and sha256-confirmed in place. // // ⚠ THIS ROW FAILS IN CI BEFORE IT FAILS LOCALLY, and that is not a bug in the // row. CI checks out `refs/pull//merge` — this branch merged with CURRENT @@ -15222,9 +15383,9 @@ mod stage2_injector_tests { // because that is what makes a NEW mint a counted event; a function + // content-hash anchor would end the drift class while keeping that property, // and is offered as a follow-up rather than taken unannounced mid-review. - "game/effects/mod.rs:6065".to_string(), - "game/effects/mod.rs:6142".to_string(), - "game/effects/mod.rs:9324".to_string(), + "game/effects/mod.rs:6175".to_string(), + "game/effects/mod.rs:6252".to_string(), + "game/effects/mod.rs:9456".to_string(), // UNMOVED across the rebase, and that is itself evidence the SET did not // move: a census that had gained or lost a producer would not leave this // entry both byte-identical AND at the same coordinate. @@ -15264,7 +15425,39 @@ mod stage2_injector_tests { // `begin_pending_trigger_target_selection` (fn now opens at :11271, itself −7). // The OTHER FOUR entries live in `game/effects/`, which this unit does not // touch at all, and did not move — the same set-preservation evidence. - "game/engine.rs:11420".to_string(), + // + // THIS PR (C4's answer-beat sampler + C5's `candidate_windows` extraction), ON + // TOP OF UPSTREAM'S `:11420`: both insertions land in `engine.rs` ABOVE this + // producer and neither is a prompt. The coordinate below is re-derived from the + // row's OWN failure output at this base, with the line re-read and + // sha256-compared there and the enclosing function re-checked. + // + // THIS PR (the ACCEPT-WITH-FIXES doc round), ON TOP OF `:11515`: `⇒ :11549`, + // +34. LOCAL, not upstream, so the CI-vs-local diagnosis in the header does + // not apply. engine.rs's ENTIRE delta this round is two COMMENT hunks, and + // both sit above this producer: `@@ -3409,3 +3409,5 @@` in + // `drive_one_shortcut_cycle` (+2) and `@@ -11148,3 +11150,35 @@` in + // `apply_action` (+32) — 2 + 32 = 34, the whole shift, with nothing below. + // A comment round cannot mint a prompt, and the census agrees: total 37 and + // partition 5/7/25 are untouched and the other four entries did not move. + // Identity re-established rather than assumed: line :11549 is byte-identical + // by sha256 (`8a544e878d3e77fb…5cc7d63`) to `c7b18c3c7:engine.rs:11515`, and + // it is still inside `begin_pending_trigger_target_selection`, which moved by + // the same +34 (opens :11366 ⇒ :11400). + // + // REBASE ONTO UPSTREAM `b654513cb`: re-derived rather than carried over, and + // **UNMOVED** at `:11549`. Upstream's six commits contribute a net ZERO above + // this producer, measured on both sides of the rebase: it sits at `:11420` in + // the OLD base `dcb8f3808` and at `:11420` in the NEW base `b654513cb`, so + // this branch's own `+95` (C4/C5) and `+34` (the doc round) still land it on + // `:11549`. That an entry can stay put while three others move by `+110`/`+132` + // is the set-preservation evidence for this rebase: a gained or lost producer + // could not leave this one byte-identical AND in place. Identity re-checked at + // the unchanged coordinate rather than presumed from the unchanged number: + // sha256 `a6d7f2f9d1e15de5…5cb032`, matching `117baa6a1:engine.rs:11549`, and + // still inside `begin_pending_trigger_target_selection` (opens :11400 here, + // :11271 at `b654513cb`). + "game/engine.rs:11549".to_string(), ], "the five production producers, NAMED: the CR 603.5 gate in `resolve_chain_body` \ plus the two repeated-optional-payment drivers, the per-player acceptance cursor \ @@ -15278,9 +15471,19 @@ mod stage2_injector_tests { let effects_src = std::fs::read_to_string(root.join("game/effects/mod.rs")) .expect("readable effects module"); let authority = format!("{}_prompt_player", "optional"); + // CODE LINES ONLY. A whole-file `matches()` also counted PROSE, and this PR's C1 adds a + // doc link to the authority in `upfront_optional_gate`'s comment — a mention that is + // neither a definition nor a call. Excluding `//` lines makes the instrument STRICTLY + // MORE specific to the thing it names (a second CALL) rather than less: the pinned + // count is unchanged at 2, and a real second call still trips it because a call cannot + // live on a comment line. + let authority_code_hits = effects_src + .lines() + .filter(|l| !l.trim_start().starts_with("//")) + .filter(|l| l.contains(&authority)) + .count(); assert_eq!( - effects_src.matches(&authority).count(), - 2, + authority_code_hits, 2, "one definition + exactly one call — the CR 603.5 gate's `let prompt_player = ..`. \ A second call inside `effects/mod.rs` means a second producer started consulting \ the authority and this row's partition needs re-deriving" @@ -17239,9 +17442,11 @@ mod bounded_offer_conjunct_tests { let field_address = format!("as {}const", '*'); assert_eq!( engine_code_hits(&lines, extent, &sample_identity).len(), - 2, - "the ring-advance detector must read the SAMPLE's allocation at both its before \ - and after sites, in {}-{}", + 3, + "the ring-advance detector must read the SAMPLE's allocation at EVERY one of its \ + sites — the shared per-beat `before` read plus an `after` read in each arm that \ + can advance the ring (the active-player settle arm and the forced-window ANSWER \ + arm), in {}-{}", extent.0 + 1, extent.1 + 1 ); @@ -17317,18 +17522,337 @@ mod bounded_offer_conjunct_tests { lines[*site].trim() ); } + // F-4: after `candidate_windows` was extracted, basis A's carrier decision lives at the + // CALL SITE, not in a `let window`. A `!is_empty()` reach-guard tolerated losing half + // the subject (2 producers -> 1) IN SILENCE — MEASURED: the pin still passed with one + // producer gone. And the obvious repair, widening the extent over `fn + // candidate_windows`, is VACUOUS — also MEASURED: `ring_live` is the walk's own + // PARAMETER NAME, so it reads identically whatever the caller passes, including under + // the DROP mutant that hands the walk the CR 104.4b comparand. Both producers are + // therefore pinned by EXACT COUNT, and each must name the evaluable ring on the line + // that chooses it. + let walk_calls = engine_code_hits(&lines, certified, "candidate_windows("); + assert_eq!( + walk_calls.len(), + 1, + "basis A takes its window from EXACTLY ONE `candidate_windows` call; found {}", + walk_calls.len() + ); let window_bindings = engine_code_hits(&lines, certified, "let window"); - assert!( - !window_bindings.is_empty(), - "REACH-GUARD: the windows must be bound inside this extent" + assert_eq!( + window_bindings.len(), + 1, + "basis B binds EXACTLY ONE window directly; found {}. Together with the walk call \ + that is the TWO producers this pin covers — a count that DROPS is a producer that \ + left the extent, which is exactly what an extraction does silently", + window_bindings.len() ); - for binding in &window_bindings { + for producer in walk_calls.iter().chain(window_bindings.iter()) { assert!( - lines[*binding].contains("ring_live"), - "every window is sliced from the EVALUABLE ring; line {} reads `{}`", - binding + 1, - lines[*binding].trim() + lines[*producer].contains("ring_live"), + "every period-touch window is sliced from the EVALUABLE ring (CR 732.2a), never \ + the CR 104.4b comparand; line {} reads `{}`", + producer + 1, + lines[*producer].trim() ); } } + + // ─────────────────────────────────────────────────────────────────────────────────── + // N1 — the period boundary has ONE authority, and every frame-recording arm asks it. + // ─────────────────────────────────────────────────────────────────────────────────── + + /// N1, BEHAVIOURAL HALF — `published_period_elapsed` is TOTAL over the two axes that + /// delimit a cycle, and each of its three interesting answers is asserted. + /// + /// CR 732.2a. This is the anti-vacuity control for the structural half below: a census + /// proving the two arms call ONE function says nothing if that function is wrong, and the + /// two properties a caller depends on — `None` never elapses, `>=` and not `==` — are + /// invisible at the call sites. + /// + /// * **`None` ⇒ never.** An offer whose producer states no per-period signature publishes + /// no frame count. Inventing one would end the cycle after an arbitrary number of frames + /// and commit a FRACTION of the published delta — the conditional action CR 732.2a + /// forbids. Fail-closed means "keep driving until the board recurs", not "stop early". + /// * **`Some(k)` with fewer frames ⇒ not yet.** The row asserts `k - 1` explicitly, so an + /// off-by-one that closed a 2-frame period after 1 frame FLIPS here. + /// * **`Some(k)` with `k` or MORE ⇒ elapsed.** A single beat may retain more than one + /// frame, so a strict `==` would drive past its own boundary and end at the beat cap + /// instead. `k + 1` is the arm that discriminates `>=` from `==`. + /// + /// REVERT-PROBE: change `is_some_and` to `is_none_or` ⇒ the `None` rows FLIP. Change `>=` + /// to `==` ⇒ the `k + 1` row FLIPS. Change `>=` to `>` ⇒ the exact-`k` row FLIPS. + #[test] + fn published_period_elapsed_is_total_over_the_axes_that_delimit_a_cycle() { + use super::published_period_elapsed; + + // (frames_this_cycle, frames_per_period) -> elapsed + let table: [((u32, Option), bool); 8] = [ + ((0, None), false), + ((1, None), false), + ((7, None), false), + ((0, Some(1)), false), + ((1, Some(1)), true), + ((1, Some(2)), false), + ((2, Some(2)), true), + ((3, Some(2)), true), + ]; + let measured: Vec<((u32, Option), bool)> = table + .iter() + .map(|&(input, _)| (input, published_period_elapsed(input.0, input.1))) + .collect(); + assert_eq!( + measured, + table.to_vec(), + "CR 732.2a: an UNPUBLISHED period never elapses by frame count ({{None}} rows), a \ + period is not over before its k-th frame, and one that overshot k IS over — the \ + three properties `drive_one_shortcut_cycle`'s two arms depend on and neither \ + call site can state" + ); + } + + /// N1, STRUCTURAL HALF — ONE authority for the period boundary, ASKED BY BOTH ARMS. + /// + /// CR 732.2a. `drive_one_shortcut_cycle` can record a ring frame in two places now that + /// `apply_action` carries the forced-window ANSWER sampling site: the active-player settle + /// arm and the injector arm. Both must advance the frame counter and both must ask the + /// same delimiter, or the published `frames_per_period` is unreachable on exactly the + /// boards the widening was for and the drive can only end at its runaway beat cap. + /// + /// The census is EXTENT-SCOPED (`engine_fn_extent` + `engine_code_hits`, the same + /// machinery the two carrier rows and the CR 603.5 census use) and comment lines are + /// excluded, so it cannot count its own prose. + /// + /// REVERT-PROBE: drop the injector arm's counter advance ⇒ `frames_this_cycle += 1` goes + /// 2 → 1 ⇒ FLIPS. Re-inline `frames_per_period.is_some_and(|k| frames_this_cycle >= k)` at + /// either arm ⇒ the raw-comparison count goes 0 → 1 ⇒ FLIPS. + #[test] + fn the_period_delimiter_has_one_authority_and_both_frame_recording_arms_ask_it() { + let src = include_str!("engine.rs"); + let lines: Vec<&str> = src.lines().collect(); + let drive = engine_fn_extent(&lines, "fn drive_one_shortcut_cycle("); + + let delimiter = format!("published_period{}elapsed(", '_'); + let asks = engine_code_hits(&lines, drive, &delimiter); + assert_eq!( + asks.len(), + 2, + "the settle arm and the injector arm must EACH ask the delimiter, in {}-{}; found \ + {:?} (1-based)", + drive.0 + 1, + drive.1 + 1, + asks.iter().map(|i| i + 1).collect::>() + ); + let advances = engine_code_hits(&lines, drive, "frames_this_cycle += 1"); + assert_eq!( + advances.len(), + 2, + "…and each of those two arms must ADVANCE the counter first, else one arm asks a \ + question the other's bookkeeping answers; found {:?} (1-based)", + advances.iter().map(|i| i + 1).collect::>() + ); + let raw = engine_code_hits(&lines, drive, "frames_this_cycle >="); + assert!( + raw.is_empty(), + "the comparison itself lives in the authority and NOWHERE in this extent — an \ + inlined copy is the second place to get `>=` and the `None` arm wrong; found \ + {:?} (1-based)", + raw.iter().map(|i| i + 1).collect::>() + ); + + // POSITIVE CONTROL against a dead grep, same extractor and same filter: one token + // known present in this extent, one known absent. The `raw.is_empty()` assertion above + // is a ZERO census and needs an instrument proven able to return non-zero. + assert!( + !engine_code_hits(&lines, drive, "frames_this_cycle").is_empty(), + "the instrument must be able to find a token that IS there" + ); + assert!( + engine_code_hits(&lines, drive, "certified_period_touch").is_empty(), + "…and must not find one that is not" + ); + } + + /// F2c — **NO FOURTH COPY OF THE CR 603.5 CONJUNCT SET IS BUILT OUT OF THESE FIVE + /// PREDICATES, AND EVERY SURVIVING PRODUCTION CALLER IS INSIDE `game/effects/`.** + /// + /// CR 603.5 + CR 608.2c + CR 608.2d + CR 603.12a. Three places used to answer *"does this + /// ability open ONE up-front optional gate?"* — production's own branch, the mint's guard + /// (b), and `analysis::resource::auto_may_answer_for` — and the latter two omitted + /// conjuncts the first has. After adoption, `effects::upfront_optional_gate` is the only + /// place the set is assembled, and the census is what keeps it that way. + /// + /// MEASURED counts, not derived ones. The plan's derivation predicted `2 / 2 / 2 / 1 / 2` + /// and the tree measures `2 / 2 / 2 / 1 / 2`; if these ever disagree the MEASURED value is + /// what belongs here. + /// + /// | predicate | production sites | where | + /// |---|---|---| + /// | `has_kind_driven_repeat` | 2 | `upfront_optional_gate` + `repeat_for_outermost_with_scope_or_unless` | + /// | `has_member_driven_repeat_after_hydration` | 2 | `upfront_optional_gate` + `resolve_chain_body`'s driver guard | + /// | `is_repeated_optional_payment` | 2 | `upfront_optional_gate` + `resolve_chain_body`'s driver dispatch | + /// | `optional_prompt_player` | 1 | `upfront_optional_gate` only | + /// | `optional_effect_is_infeasible` | 2 | `upfront_optional_gate` + `resolve_chain_body`'s `CastFromZone` decline | + /// + /// **THE THREE NON-AUTHORITY SITES ARE NOT COPIES, AND FOLDING THEM IN WOULD BE WRONG.** + /// They consume these predicates to decide WHICH DRIVER RUNS — whether a counted repeat + /// has to wrap scoped/unless-pay instructions (CR 608.2c), which repeat driver takes the + /// ability, and the CR 603.12a repeated-payment dispatch that fires *because* the up-front + /// gate suppressed itself. That is a different question from "does one up-front window + /// open", and it is asked after the gate has already declined. + /// + /// **HONEST GUARANTEE.** This enforces that no fourth copy is built OUT OF THESE FIVE + /// PREDICATES. A copy that re-derives the same conjunct from `ability.repeat_for` (or from + /// `optional_for`, or from the effect discriminant) inline is NOT caught, and no census + /// over these five tokens can catch it — `has_kind_driven_repeat` is itself exactly such a + /// re-derivation. + /// + /// The zero-outside-`game/effects/` assertion carries its own POSITIVE CONTROL, because a + /// zero census with a dead instrument is indistinguishable from a passing one. + /// + /// REVERT-PROBE: re-introduce any one predicate call in `analysis/resource.rs` or in + /// `entry_publishes_pin_slots` ⇒ that predicate's count rises AND the outside-set becomes + /// non-empty ⇒ FLIPS on two independent assertions. + #[test] + fn f2c_the_cr_603_5_conjunct_set_has_one_production_assembler() { + /// Every `.rs` under the crate's `src`. A whole file whose stem ends `_tests` is + /// test-only (its parent declares it under `#[cfg(test)]`). + fn rs_files(dir: &std::path::Path, out: &mut Vec) { + for entry in std::fs::read_dir(dir).expect("readable source dir") { + let path = entry.expect("readable dir entry").path(); + if path.is_dir() { + rs_files(&path, out); + } else if path.extension().is_some_and(|e| e == "rs") { + out.push(path); + } + } + } + /// The `#[cfg(test)]`-attributed column-0 `mod … {` … column-0 `}` spans, so the + /// census cannot count its own harness. Same shape as the CR 603.5 prompt census. + fn cfg_test_spans(lines: &[&str]) -> Vec<(usize, usize)> { + let mut spans = Vec::new(); + let mut i = 0; + while i < lines.len() { + if lines[i].trim() == "#[cfg(test)]" { + let mut j = i + 1; + while j < lines.len() + && (lines[j].trim_start().starts_with("#[") || lines[j].trim().is_empty()) + { + j += 1; + } + let is_mod = j < lines.len() + && lines[j].starts_with(['m', 'p']) + && lines[j].contains("mod ") + && lines[j].trim_end().ends_with('{'); + if is_mod { + let mut k = j + 1; + while k < lines.len() && lines[k] != "}" { + k += 1; + } + spans.push((j, k)); + i = k; + } + } + i += 1; + } + spans + } + + // ASSEMBLED needles, so this row's own source cannot be counted by its own instrument. + let predicates: [(String, usize); 5] = [ + (format!("has_kind_driven{}repeat(", '_'), 2), + ( + format!("has_member_driven_repeat_after{}hydration(", '_'), + 2, + ), + (format!("is_repeated_optional{}payment(", '_'), 2), + (format!("optional_prompt{}player(", '_'), 1), + (format!("optional_effect_is{}infeasible(", '_'), 2), + ]; + + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("src"); + let mut files = Vec::new(); + rs_files(&root, &mut files); + files.sort(); + assert!(files.len() > 100, "reach-guard: the walker found the crate"); + + let mut sites: Vec<(usize, String)> = Vec::new(); + let mut control_hits = 0usize; + for path in &files { + let text = std::fs::read_to_string(path).expect("readable source file"); + let lines: Vec<&str> = text.lines().collect(); + let spans = cfg_test_spans(&lines); + let rel = path + .strip_prefix(&root) + .expect("under src") + .display() + .to_string(); + let test_file = rel.trim_end_matches(".rs").ends_with("_tests"); + for (n, line) in lines.iter().enumerate() { + if line.trim_start().starts_with("//") { + continue; + } + if test_file || spans.iter().any(|(a, b)| (*a..=*b).contains(&n)) { + continue; + } + // POSITIVE CONTROL for the zero census below: a token that IS present in + // production, counted by this very walker under this very filter. + if line.contains("fn resolve_chain_body(") { + control_hits += 1; + } + for (i, (needle, _)) in predicates.iter().enumerate() { + // The DEFINITION is not a call site. + if line.contains(needle) && !line.contains(&format!("fn {needle}")) { + sites.push((i, format!("{rel}:{}", n + 1))); + } + } + } + } + + assert_eq!( + control_hits, 1, + "POSITIVE CONTROL: the walker+filter must find `fn resolve_chain_body(` exactly \ + once in production source. A zero below is only meaningful with a live instrument" + ); + + let counted: Vec<(String, usize)> = predicates + .iter() + .enumerate() + .map(|(i, (needle, _))| { + ( + needle.clone(), + sites.iter().filter(|(j, _)| *j == i).count(), + ) + }) + .collect(); + let expected: Vec<(String, usize)> = predicates + .iter() + .map(|(needle, want)| (needle.clone(), *want)) + .collect(); + assert_eq!( + counted, expected, + "the CR 603.5 conjunct set gained or lost a production consumer. The surviving \ + non-authority sites are `repeat_for_outermost_with_scope_or_unless` (does a \ + counted repeat wrap scoped/unless-pay instructions), `resolve_chain_body`'s \ + repeat-driver guard and its CR 603.12a driver dispatch, and \ + `resolve_chain_body`'s `CastFromZone` decline probe — every one of them selects a \ + DRIVER rather than opening an up-front window, so a NEW site is a decision to \ + adjudicate here and not a number to move.\nsites={sites:#?}" + ); + + let outside: Vec<&String> = sites + .iter() + .filter(|(_, site)| !site.starts_with("game/effects/")) + .map(|(_, site)| site) + .collect(); + assert!( + outside.is_empty(), + "SINGLE ASSEMBLER: every production consumer of these five predicates lives in \ + `game/effects/`, next to the authority that assembles them. A caller in another \ + module is by construction re-deriving the gate's conjunct set from outside it — \ + which is exactly what `analysis::resource::auto_may_answer_for` and \ + `engine::entry_publishes_pin_slots` used to do, each with a DIFFERENT omission. \ + Found {outside:#?}" + ); + } } diff --git a/crates/engine/src/game/replacement.rs b/crates/engine/src/game/replacement.rs index 48a70eb5df..628ef600c0 100644 --- a/crates/engine/src/game/replacement.rs +++ b/crates/engine/src/game/replacement.rs @@ -7354,7 +7354,15 @@ pub fn find_applicable_replacements( } // =========================================================================== -// CR 614.1a + CR 616.1 — the ONE prompt-cause authority over a proposed event. +// CR 614.1 + CR 616.1 — the ONE prompt-cause authority over a proposed event. +// +// CR 614.1, NOT CR 614.1a. `614.1a` scopes itself to effects that use the word +// "instead"; this authority classifies EVERY applicable replacement — skips +// (`614.1b`), enters-with (`614.1c`/`614.1d`), turned-face-up (`614.1e`), and the +// virtual candidates that carry no `ReplacementDefinition` at all. The definitional +// head (`614.1`: "some continuous effects are replacement effects … such effects +// watch for a particular event") is the anchor; `614.1a` was a sub-rule cited for +// its parent's job. // // Derived from the SAME candidate authority the live pipeline uses // (`find_applicable_replacements`), so VIRTUAL candidates — which have no @@ -7364,8 +7372,9 @@ pub fn find_applicable_replacements( // defs (Giada, Font of Hope), and no def scan can see a virtual. // =========================================================================== -/// CR 614.1a + CR 616.1: why the live replacement pipeline can open a player -/// choice on one proposed event. +/// CR 614.1 + CR 616.1: why the live replacement pipeline can open a player +/// choice on one proposed event. (`614.1`, the definitional head, not `614.1a` — +/// see the block comment above.) #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum ReplacementPromptCause { /// CR 614.1a: a single optional / `MayCost` candidate prompts. An diff --git a/crates/engine/src/types/game_state.rs b/crates/engine/src/types/game_state.rs index b39878c02d..52f69d07ce 100644 --- a/crates/engine/src/types/game_state.rs +++ b/crates/engine/src/types/game_state.rs @@ -13332,9 +13332,12 @@ declare_game_state! { /// CR 732.2a loop-shortcut detection ring (PR-3). A bounded FIFO of recent /// post-resolution [`LoopDetectSample`]s — each carrying BOTH the CR 104.4b /// `normalized` comparand (what this ring held before the two roles were split) and - /// the CR 732.2a `live` evaluable — captured at the post-pipeline frame - /// of `game::engine::pass_priority_once_with_pipeline` (after - /// `run_post_action_pipeline` places refilling triggers, CR 603.3) and scanned at + /// the CR 732.2a `live` evaluable — captured at TWO post-pipeline frames in + /// `game::engine` (both after `run_post_action_pipeline` places refilling triggers, + /// CR 603.3): the settle sampler in `pass_priority_once_with_pipeline` and the + /// forced-window ANSWER site in `apply_action`. See + /// [`GameState::record_loop_detect_sample`] for what the two sites share and where they + /// differ. Scanned at /// the SBA-reconciliation seam (`game::engine::reconcile_terminal_result`). A /// self-refilling MANDATORY cascade drives the engine one resolution per `apply()` /// with no call-local window (the per-beat single-apply drive), so the window that @@ -19643,9 +19646,21 @@ impl GameState { /// PR-3 (Option C): push one NORMALIZED post-resolution snapshot onto the /// CR 732.2a loop-detection ring, evicting the oldest at `LOOP_DETECT_RING_CAP`. /// The snapshot is `normalize_for_loop`d (its own ring cleared, see above) and - /// `Arc`-shared so storage is O(1) per element. Called only from the post-pipeline - /// frame behind the refill gate (`game::engine::pass_priority_once_with_pipeline`, - /// after `run_post_action_pipeline` places refilling triggers). + /// `Arc`-shared so storage is O(1) per element. + /// + /// TWO production call sites, both in `game::engine` and both on the frame AFTER + /// `run_post_action_pipeline` has placed refilling triggers (CR 603.3): + /// + /// 1. the SETTLE sampler behind the refill gate in `pass_priority_once_with_pipeline` + /// (gated on `resolved_this_beat`, and the only one of the two with a `ring.clear()` + /// counterpart on its `else`); and + /// 2. the forced-window ANSWER site in `apply_action` (gated on + /// `answering_forced_window`), added because an entry announced ACROSS a forced + /// pre-priority window never appeared in any settle frame's stack. + /// + /// "Only the settle sampler" was the pre-(2) premise and it is no longer true; the two + /// share every other conjunct, including `WaitingFor::Priority{active_player}`, which is + /// what keeps the ring homogeneous for `analysis::resource::ring_delta_signature`. pub(crate) fn record_loop_detect_sample(&mut self) { if self.loop_detect_ring.len() == LOOP_DETECT_RING_CAP { self.loop_detect_ring.pop_front(); diff --git a/crates/engine/tests/fixtures/f4_user_mode1_no_offer_4p.json.gz b/crates/engine/tests/fixtures/f4_user_mode1_no_offer_4p.json.gz new file mode 100644 index 0000000000..8665818603 Binary files /dev/null and b/crates/engine/tests/fixtures/f4_user_mode1_no_offer_4p.json.gz differ diff --git a/crates/engine/tests/fixtures/f4_user_mode2_accept_commits_nothing_4p.json.gz b/crates/engine/tests/fixtures/f4_user_mode2_accept_commits_nothing_4p.json.gz new file mode 100644 index 0000000000..c8611f2092 Binary files /dev/null and b/crates/engine/tests/fixtures/f4_user_mode2_accept_commits_nothing_4p.json.gz differ diff --git a/crates/engine/tests/integration/fantastic_four_bounded_loop.rs b/crates/engine/tests/integration/fantastic_four_bounded_loop.rs index 43fea5beed..c1fd404e72 100644 --- a/crates/engine/tests/integration/fantastic_four_bounded_loop.rs +++ b/crates/engine/tests/integration/fantastic_four_bounded_loop.rs @@ -22,26 +22,32 @@ //! # MEASURED SCOPE OF THIS MODULE — read this before adding a row //! //! The bounded offer FIRES on this dump (that is 5d's headline and [`r1_the_bounded_offer_fires_ -//! on_the_real_f4_dump`] is the row). It publishes exactly **one** decision point — Sue's -//! `MayChoice`. Torch's `Targets` point and Reed's `MayChoice` point are **NOT** published, and -//! the mechanism is measured and pinned by -//! [`r1b_the_published_point_set_is_exactly_what_the_retained_window_announces`]: the CR 732.2a -//! ring sampler fires only at `Priority { player == active_player }` after a non-shrinking -//! resolution, so on this board the retained frames alternate strictly between the `404` and -//! `402` stack entries. `certified_period_touch`'s `announced` set is "entries in a frame's -//! stack that were absent from the previous frame's", so the `403` and `401` entries are -//! structurally invisible to conjunct (6) and to `bounded_cycle_pin_slots_for_window`. +//! on_the_real_f4_dump`] is the row). It publishes **all three** per-iteration choices this +//! cycle opens — Sue's `MayChoice`, Reed's `MayChoice` and Torch's `Targets` slot — and the +//! mechanism is measured and pinned by +//! [`r1b_the_published_point_set_is_exactly_what_the_retained_window_announces`]. +//! +//! ⚠ **THE PREVIOUS PARAGRAPH SAID THE OPPOSITE, AND IT WAS A MEASUREMENT OF A BLIND SPOT, NOT +//! OF THE BOARD.** The CR 732.2a ring sampler used to fire only at `Priority { player == +//! active_player }` after a non-shrinking resolution, so on this board the retained frames +//! alternated strictly between the `404` and `402` stack entries; `certified_period_touch`'s +//! `announced` set is "entries in a frame's stack that were absent from the previous frame's", +//! which made the `403` and `401` entries structurally invisible to conjunct (6) and to +//! `bounded_cycle_pin_slots_for_window`. Torch and Reed resolve ACROSS a forced pre-priority +//! window, and that window is exactly what the old site could not see. The second sampling site +//! records a frame at the beat such a window is **ANSWERED**, so those two entries are now +//! announced like the other two — a widening of what the offer can publish, not a change to +//! what the board does. //! //! CONSEQUENCE, also measured and pinned -//! ([`r2_an_accepted_declaration_commits_zero_cycles_because_reeds_may_is_unannounced`]): an -//! accepted `Fixed(n)` declaration carrying the FULL published pin set drives cycle 0, answers -//! Sue's "may" from the pin (U4's arm, on the real dump), and then **aborts** on Reed's -//! unpinned "may" ⇒ whole-cycle rollback, zero commit, manual handback. That is fail-CLOSED and -//! rules-safe, but it is not a grant — so the plan's R2a/R2b/R3/R5 (pass ⇒ grant, respond ⇒ -//! no-grant, Sue-Decline rollback, `victim_slot` keyed by Torch) have no non-vacuous form on -//! this tree and are NOT written here. They are handed back with the mechanism above. +//! ([`r2a_an_accepted_declaration_commits_exactly_n_cycles_because_reeds_may_is_announced`]): an +//! accepted `Fixed(n)` declaration carrying the full published pin set now **commits exactly +//! `n` repetitions** — P1 loses `n` life, P0's library loses `n` cards — and `n = 1` and `n = 3` +//! are DISTINGUISHABLE. The former zero-commit was the fail-closed abort on Reed's unpinned +//! "may"; with Reed published there is nothing left to abort on. use engine::analysis::decision_template::{DecisionKind, DecisionPointKind, IterationCount}; +use engine::analysis::resource::ResourceVector; use engine::game::engine::apply; use engine::types::ability::{ReplacementMode, TargetRef}; use engine::types::actions::GameAction; @@ -84,10 +90,8 @@ fn gunzip(gz: &[u8]) -> String { /// The dump was captured with the detector OFF; every row here is about the CR 732.2a /// interactive offer, so the mode is set to `Interactive` at load — the same thing the user's /// own toggle does. -fn load_f4() -> GameState { - let json = gunzip(include_bytes!( - "../fixtures/fantastic_four_bounded_loop_4p.json.gz" - )); +fn load_dump(gz: &[u8]) -> GameState { + let json = gunzip(gz); let envelope: serde_json::Value = serde_json::from_str(&json).expect("dump envelope parses as JSON"); let mut state = serde_json::from_value::(envelope["gameState"].clone()) @@ -97,6 +101,88 @@ fn load_f4() -> GameState { state } +fn load_f4() -> GameState { + load_dump(include_bytes!( + "../fixtures/fantastic_four_bounded_loop_4p.json.gz" + )) +} + +/// **MODE1** — the user's own 2026-08-03 capture of the board that raised NO offer at all +/// (`fastastic-four-no-offer-phase5.zip`, `game-state-turn-5-…19-09-15-030Z.json`), derived by +/// `jq -c '{gameState}' … | gzip -9 -n` (860,451 B; the raw envelope is 20.5 MB, of which +/// `turnCheckpoints` alone is 16.4 MB and no loader reads it). +/// +/// Its distinguishing field is `may_trigger_auto_choices`: it carries the user's stored +/// "always take" for Sue's CR 603.5 `may`, so guard (b) withholds that pin slot and gate (6) +/// can only be discharged by the CR 603.5 auto-answer relief. +fn load_mode1() -> GameState { + load_dump(include_bytes!( + "../fixtures/f4_user_mode1_no_offer_4p.json.gz" + )) +} + +/// **MODE2** — the user's own 2026-08-03 capture of the board where the offer DID fire, the +/// declaration WAS accepted, and the drive then committed **nothing** and re-offered +/// (`f4-offer-fires-no-ff.zip`, `game-state-turn-5-…19-56-54-597Z.json`), derived by the same +/// `jq -c '{gameState}' … | gzip -9 -n` (971,617 B). +/// +/// Its distinguishing field is the COMPLEMENT of MODE1's: `may_trigger_auto_choices` is EMPTY +/// (the user cleared the "always take" as a workaround), so this board reaches the offer +/// through the ordinary CR 603.5 publication path — and the accepted grant aborted on a `may` +/// the offer had not published. The two dumps are therefore one field apart on the axis this +/// change is about, which is why both are tracked. +fn load_mode2() -> GameState { + load_dump(include_bytes!( + "../fixtures/f4_user_mode2_accept_commits_nothing_4p.json.gz" + )) +} + +/// The four axes ONE committed cycle of this loop moves: every seat's life, every seat's +/// library size, The Thing's counters, and the token population. +/// +/// All four, not one: a commit that moved only life could be a stray drain, while a commit +/// that moves all four is the CYCLE. `u32::MAX` for a missing Thing is deliberate — an absent +/// permanent must fail an equality loudly rather than read as "zero counters". +fn commit_axes(state: &GameState) -> (Vec, Vec, u32, usize) { + let thing = state + .battlefield + .iter() + .filter_map(|id| state.objects.get(id)) + .find(|o| o.name == THING) + .map(|o| o.counters.values().copied().sum::()) + .unwrap_or(u32::MAX); + let tokens = state + .battlefield + .iter() + .filter(|id| state.objects.get(id).is_some_and(|o| o.is_token)) + .count(); + ( + state.players.iter().map(|p| p.life).collect(), + state.players.iter().map(|p| p.library.len()).collect(), + thing, + tokens, + ) +} + +/// Every living opponent Accepts the CR 732.2c window, returning how many did. A zero return +/// means the window never opened, which every caller turns into a loud failure. +fn accept_all_opponents(state: &mut GameState) -> usize { + use engine::analysis::loop_check::ShortcutResponse; + let mut responders = 0; + while let WaitingFor::RespondToShortcut { player, .. } = state.waiting_for.clone() { + apply( + state, + player, + GameAction::RespondToShortcut { + response: ShortcutResponse::Accept, + }, + ) + .expect("each living opponent accepts (CR 732.2c)"); + responders += 1; + } + responders +} + /// R18 / §3 D6 TARGET A — resolve a fixture object by CARD NAME, never by literal `ObjectId`. /// /// The user has announced a re-dump of this same board (*"I will then provide a new F4 .zip @@ -359,24 +445,39 @@ fn panic_message(payload: &Box) -> String { /// `apply()`, and its `max_iterations` equals the bound re-derived by this row from the /// offer-beat board. /// -/// **STATUS: PARTIAL — pending the (A)/(B) ruling.** §6 R1 as planned also expected the offer to -/// publish three decision points and to be TAKEABLE (commit ≥ 1 cycle). Measured on this tree it -/// publishes ONE point and commits ZERO cycles (see `r1b` and `r2` for the pinned measurements, -/// and the module header for the mechanism). This row therefore ships the half of R1 that the -/// measurement supports — the offer fires, and its bound arithmetic is correct — and pins the -/// other half AS MEASURED rather than asserting the falsified prediction. R2a/R2b/R3/R4/R5 and -/// the interruptibility pair stay unwritten until the ruling lands. +/// **STATUS: §6 R1's other half is now MEASURED TRUE, in two sibling rows.** R1 as planned also +/// expected the offer to publish three decision points and to be TAKEABLE (commit ≥ 1 cycle). +/// ⚠ THE NOTE THAT STOOD HERE — *"measured on this tree it publishes ONE point and commits ZERO +/// cycles (see `r1b` and `r2`)"* — IS FALSIFIED by this branch's own rows, and is replaced +/// rather than softened: +/// +/// * [`r1b_the_published_point_set_is_exactly_what_the_retained_window_announces`] pins +/// **THREE** points — `[Sue MayChoice, Reed MayChoice, Torch Targets]` — not one; +/// * [`r2a_an_accepted_declaration_commits_exactly_n_cycles_because_reeds_may_is_announced`] +/// commits **exactly `n`**, run at `n = 1` and `n = 3` so the two outcomes are +/// distinguishable — not zero; +/// * the row that measured zero was `r2_an_accepted_declaration_commits_zero_cycles_…`, and it +/// NO LONGER EXISTS. This branch RENAMED it to `r2a_…` once the answer-beat sampler announced +/// the frame Reed's entry sits on, which removed the unannounced `may` the zero-commit was +/// fail-closing on. Any surviving cross-reference to `r2` resolves to nothing. +/// +/// This row keeps the half it always owned — the offer fires, and its bound arithmetic is +/// correct. `r2b`/`r3`/`r4`/`r5` and the interruptibility pair are still unwritten: no `fn r2b_`, +/// `fn r3_`, `fn r4_` or `fn r5_` row exists in this file. /// /// # What the assertion is bound to, and why it is not `f(x) == f(x)` /// /// The expectation is computed HERE from (i) each living seat's life and library on the /// offer-beat board and (ii) the per-period delta the ENGINE published on the certificate — it -/// never calls `elimination_bounds`, which is the function under test. Per §6 R1's ROUND-38 -/// (F3) ruling the row is anchored to the **in-tree MAX form** (`resource.rs` -/// `observed_life_loss.max(declared_life_magnitude)` under the `declarable_victims` guard); -/// the additive per-victim form is a tracked follow-up (R1-fu), not a prerequisite. Measured on -/// this board `victim_slot` is EMPTY (see `r5`'s handback in the module header), so the two -/// forms coincide here and the row states which one it assumes. +/// never calls `elimination_bounds`, which is the function under test. ⚠ THE ANCHOR THAT STOOD +/// HERE — *"anchored to the in-tree MAX form … the additive per-victim form is a tracked +/// follow-up (R1-fu), not a prerequisite … measured on this board `victim_slot` is EMPTY, so the +/// two forms coincide"* — IS FALSIFIED ON BOTH CLAUSES. The in-tree form IS the additive one +/// (`resource.rs` `observed_life_loss.max(0) + declared_life_magnitude` under the +/// `declarable_victims` guard), and `victim_slot` is NON-EMPTY on this board, so the two forms +/// do NOT coincide here — which is why this row's own assertion message states the additive form +/// it assumes, and names what actually remains tracked as F1: the additive form OVER-CHARGES +/// wherever a published slot IS the observed drain. /// /// # Reach-guards (each excludes a way this could pass degenerately) /// @@ -430,9 +531,38 @@ fn r1_the_bounded_offer_fires_on_the_real_f4_dump() { // CR 704.5a headroom is `life - 1`: a seat at exactly 0 has LOST, so a legal shortcut must // stop one point above it. CR 104.3c: an empty library is only lethal on the next draw, so // the library axis divides the whole remaining library. + // CR 704.5a: a published re-aimable `Targets` slot may be pointed at ANY of its legal + // player targets in EVERY remaining repetition, so each of them is charged that slot's + // magnitude ON TOP of its own observed drain. Both terms come off the offer's OWN + // published data — `certificate.per_cycle.victim_slot` and `schema.points` — never from + // `elimination_bounds`, so this stays an independent re-derivation. + let declared_life_magnitude: i64 = per_cycle + .victim_slot + .iter() + .map(|(_, m)| *m) + .filter(|m| *m > 0) + .sum(); + let declarable_victims: std::collections::BTreeSet = schema + .points + .iter() + .filter_map(|p| match &p.kind { + DecisionPointKind::Targets { legal_targets, .. } => Some(legal_targets), + _ => None, + }) + .flatten() + .filter_map(|t| match t { + TargetRef::Player(p) => Some(*p), + _ => None, + }) + .collect(); let mut bounds: Vec = vec![]; for player in state.players.iter().filter(|p| !p.is_eliminated) { - let loss = -per_cycle.delta.life.get(&player.id).copied().unwrap_or(0); + let observed = -per_cycle.delta.life.get(&player.id).copied().unwrap_or(0); + let loss = if declarable_victims.contains(&player.id) { + observed.max(0) + declared_life_magnitude + } else { + observed + }; if loss > 0 { bounds.push((player.life as i64 - 1) / loss); } @@ -458,8 +588,13 @@ fn r1_the_bounded_offer_fires_on_the_real_f4_dump() { expected, "CR 732.2a + CR 704.5a: `max_iterations` is the MIN over every living seat's \ elimination headroom, divided by the per-period consumption the certificate itself \ - published. Re-derived here as {bounds:?} -> {expected}; the offer published {}. \ - (This row assumes the IN-TREE max form; see R1-fu.)", + published, PLUS the published `victim_slot` magnitude charged to every declarable \ + victim. Re-derived here as {bounds:?} -> {expected} with declared={declared_life_magnitude} \ + over victims {declarable_victims:?}; the offer published {}. (The additive per-victim \ + form is now BOTH the in-tree form and this re-derivation, because `victim_slot` is \ + non-empty on this board for the first time. It is NOT the follow-up discharged: the \ + same additive form OVER-CHARGES wherever a published slot IS the observed drain — \ + MEASURED one life point wide by the B5f pair — and that remains tracked as F1.)", schema.max_iterations ); assert!( @@ -469,26 +604,30 @@ fn r1_the_bounded_offer_fires_on_the_real_f4_dump() { ); } -/// §6 R1, SECOND HALF — **a MEASURED CORRECTION to the plan, pinned so it cannot drift -/// silently. STATUS: PARTIAL — this row pins the CURRENT truth of the published point set, not -/// the planned one, pending the (A)/(B) ruling.** +/// §6 R1, SECOND HALF — the published point set, pinned so it cannot drift silently. /// /// R1 as written expects `points ≡ {Targets(403 Torch), MayChoice(401 Reed), -/// MayChoice(402 Sue)}`. That expectation is a HEAD-era SNAPSHOT-mint reading (§2: *"returns 1 -/// point when 403 is up"*), and it does not survive U3's WINDOW mint. Measured on this tree: -/// -/// * the retained ring frames on this board alternate strictly between the `404` and `402` -/// stack entries — the CR 732.2a sampler fires only at `Priority { player == active_player }` -/// after a non-shrinking resolution, and the `403` / `401` entries only ever sit on the stack -/// across a `TriggerTargetSelection` / `OptionalEffectChoice` window; -/// * `certified_period_touch`'s `announced` set is exactly "entries in a frame's stack absent -/// from the previous frame's", so `403` and `401` are never announced; -/// * therefore `bounded_cycle_pin_slots_for_window` publishes exactly ONE point — Sue's -/// `MayChoice`. +/// MayChoice(402 Sue)}`. ⚠ THE MEASUREMENT THAT STOOD HERE — *"the `403` / `401` entries only +/// ever sit on the stack across a `TriggerTargetSelection` / `OptionalEffectChoice` window … +/// so `403` and `401` are never announced … therefore `bounded_cycle_pin_slots_for_window` +/// publishes exactly ONE point — Sue's `MayChoice`"* — IS FALSIFIED BY THIS ROW'S OWN BODY, and +/// is replaced rather than softened. Measured on this tree now: +/// +/// * ALL FOUR cycle sources are retained on some sample's stack — the `framed_sources` census +/// below asserts `{Thing, Sue, Torch, Reed}` exactly, and states `Torch`/`Reed` as its own +/// conjunct because they are the load-bearing half; +/// * `403` and `401` do still resolve ACROSS a forced pre-priority window, but the answer-beat +/// sampling site in `apply_action` records a frame at the beat that window is ANSWERED — so +/// `certified_period_touch`'s `announced` set, still exactly "entries in a frame's stack +/// absent from the previous frame's", now contains them; +/// * therefore `bounded_cycle_pin_slots_for_window` publishes all THREE points, and R1's +/// planned expectation is MET rather than corrected. /// /// The row asserts the MEASUREMENT, with the sources named, and the frame census as its own -/// reach-guard. **If a future change widens the announced set this row FAILS LOUDLY and must be -/// re-keyed — which is the point: R2a/R2b/R3/R5 become writable at exactly that moment.** +/// reach-guard. **If a future change NARROWS the announced set again this row FAILS LOUDLY** — +/// which is what it is for: that shrink is exactly the regression +/// [`r2a_an_accepted_declaration_commits_exactly_n_cycles_because_reeds_may_is_announced`], +/// written on the strength of Reed being published, would otherwise silently lose. #[test] fn r1b_the_published_point_set_is_exactly_what_the_retained_window_announces() { let mut state = load_f4(); @@ -515,17 +654,17 @@ fn r1b_the_published_point_set_is_exactly_what_the_retained_window_announces() { .collect(); assert_eq!( framed_sources, - [thing, sue].into_iter().collect(), - "MEASURED: every retained sample's stack holds a {THING:?} ({thing:?}) or {SUE:?} \ - ({sue:?}) entry and NEVER a {TORCH:?} ({torch:?}) or {REED:?} ({reed:?}) one, because \ - those two resolve across a prompt window and the sampler only fires at an \ - active-player `Priority` settle. This is the reach-guard for the point-set assertion \ - below" + [thing, sue, torch, reed].into_iter().collect(), + "MEASURED: every one of the four cycle sources is retained on some sample's stack. \ + {TORCH:?} ({torch:?}) and {REED:?} ({reed:?}) resolve ACROSS a forced pre-priority \ + window, and the second sampling site in `apply_action` records a frame at the beat \ + that window is ANSWERED — so they are announced exactly like {THING:?} ({thing:?}) \ + and {SUE:?} ({sue:?}). This is the reach-guard for the point-set assertion below" ); assert!( - !framed_sources.contains(&torch) && !framed_sources.contains(&reed), + framed_sources.contains(&torch) && framed_sources.contains(&reed), "stated as its own conjunct because it is the load-bearing half: the two sources whose \ - choices go unpublished are exactly the two the sampler never retains" + choices used to go unpublished are exactly the two the answer-beat sampler adds" ); let published: Vec<(ObjectId, &'static str)> = schema @@ -546,35 +685,40 @@ fn r1b_the_published_point_set_is_exactly_what_the_retained_window_announces() { .collect(); assert_eq!( published, - vec![(sue, "MayChoice")], - "MEASURED PLAN CORRECTION (§6 R1): the window mint publishes ONE point — Sue's \ - CR 603.5 `may`. Torch's CR 608.2b `Targets` point and Reed's CR 603.5 `may` are NOT \ - published because their stack entries are never ANNOUNCED (see the frame census \ - above). If this assertion fails because the set GREW, the announced-set derivation \ - changed and R2a/R2b/R3/R5 must be written in the same change" + vec![(sue, "MayChoice"), (reed, "MayChoice"), (torch, "Targets")], + "MEASURED: the window mint publishes all THREE per-iteration choices this cycle \ + opens — Sue's and Reed's CR 603.5 `may` gates and Torch's CR 608.2b `Targets` slot. \ + The set is exactly the announced set from the census above; if it SHRINKS again the \ + answer-beat sampling site regressed" ); } -/// §6 R2, **as measured** — the consequence of the unannounced choices, driven end to end. +/// §6 R2a, **as measured** — the accepted declaration COMMITS, driven end to end. /// /// A `Fixed(n)` declaration carrying the FULL published pin set is ACCEPTED at declare /// (`predictability_gate` + `validate_pins` both pass — the published set is covered), every -/// living opponent Accepts (CR 732.2c), and then the drive **commits nothing**: cycle 0 answers -/// Sue's `OptionalEffectChoice` from the pin (U4's `inject_pinned_answer` arm, on the real -/// dump), reaches Reed's `OptionalEffectChoice`, finds no pin for it, and returns -/// `CycleOutcome::Abort` ⇒ whole-cycle rollback ⇒ CR 800.4a priority handback. +/// living opponent Accepts (CR 732.2c), and the drive then commits **exactly `n`** repetitions +/// of the published per-cycle delta: cycle 0 answers Sue's `OptionalEffectChoice` from the pin +/// (U4's `inject_pinned_answer` arm, on the real dump), then Reed's from ITS pin, and the cycle +/// closes at the published period boundary. /// -/// This is FAIL-CLOSED and rules-safe; it is also NOT a grant, so §6 R2a's *"exactly N cycles -/// commit"* has no non-vacuous form here and is handed back rather than weakened. The row pins -/// the zero-commit **together with its cause**, so it cannot be read as "the drive works": +/// ⚠ **THIS ROW USED TO ASSERT THE OPPOSITE** (`r2_..._commits_zero_cycles_because_reeds_may_ +/// is_unannounced`) and the rename is the point: the zero-commit was the fail-closed abort on +/// Reed's UNPINNED `may`, which existed only because the sampler could not see the frame +/// Reed's entry announced on. With Reed published there is nothing left to abort on, so §6 +/// R2a's *"exactly N cycles commit"* finally has a non-vacuous form on the real dump. /// -/// * the same `n` is run at 1 and at 3 and BOTH commit zero (a partial commit would separate -/// them, which is the discriminator `bounded_fixed_count_commits_exactly_n_periods` uses); +/// The row pins the commit **together with its cause**, so it cannot be read as "some delta +/// appeared": +/// +/// * the same declaration is run at `n = 1` and `n = 3` and the two outcomes must be +/// DISTINGUISHABLE — the discriminator `bounded_fixed_count_commits_exactly_n_periods` uses, +/// and the guard against an instrument that would satisfy the per-`n` equalities vacuously; /// * the declaration is asserted to have been ACCEPTED (`RespondToShortcut` raised), so the -/// zero is the DRIVE's and not a declare-time refusal — that distinction is the whole row; -/// * Reed's "may" is asserted UNPUBLISHED on the same offer, naming the cause. +/// commit is the DRIVE's and not a declare-time artefact; +/// * Reed's `may` is asserted PUBLISHED on the same offer, naming the cause. #[test] -fn r2_an_accepted_declaration_commits_zero_cycles_because_reeds_may_is_unannounced() { +fn r2a_an_accepted_declaration_commits_exactly_n_cycles_because_reeds_may_is_announced() { use engine::analysis::loop_check::ShortcutResponse; let mut committed_per_n = vec![]; @@ -582,21 +726,33 @@ fn r2_an_accepted_declaration_commits_zero_cycles_because_reeds_may_is_unannounc let mut state = load_f4(); let reed = resolve_by_name(&state, REED); drive_f4_to_offer(&mut state, 400).expect("the bounded offer fires (see R1)"); - let (proposer, _certificate, schema) = offer_parts(&state); + let (proposer, certificate, schema) = offer_parts(&state); + // The row's failure message CLAIMS the published per-cycle delta, so the assertion + // has to READ it. This binding used to be `_certificate` and the expectation two + // literal `1`s — a re-dump that changed the rate reddened the row for a reason that + // has nothing to do with the property under test. + let per_cycle = certificate + .per_cycle + .clone() + .expect("a bounded offer publishes its per-period signature"); let schema = schema.clone(); assert!( - !schema.points.iter().any(|p| matches!(&p.slot.source, + schema.points.iter().any(|p| matches!(&p.slot.source, engine::types::game_state::YieldTarget::ThisObject { source_id, .. } if *source_id == reed)), - "the CAUSE this row is about: Reed's CR 603.5 `may` is NOT among the published \ - points, so no legal declaration can pin it" + "the CAUSE this row is about: Reed's CR 603.5 `may` IS among the published \ + points, so a legal declaration can pin it and the drive has nothing left to \ + abort on" ); let template = f4_pin_template(&schema, proposer, n); let life_before: Vec = state.players.iter().map(|p| p.life as i64).collect(); let libs_before: Vec = state.players.iter().map(|p| p.library.len()).collect(); + // Seat ids read POSITIONALLY, from the same order the two vectors above index, so the + // published rate looked up below belongs to the seat whose movement is measured. + let seats: Vec = state.players.iter().map(|p| p.id).collect(); apply( &mut state, @@ -629,26 +785,53 @@ fn r2_an_accepted_declaration_commits_zero_cycles_because_reeds_may_is_unannounc let life_after: Vec = state.players.iter().map(|p| p.life as i64).collect(); let libs_after: Vec = state.players.iter().map(|p| p.library.len()).collect(); + // Both axes are measured as LOSSES (`before - after`), so the published signed rates + // are negated to match. `libs_*` are `usize`: cast EACH side before subtracting, or a + // library that fails to shrink — the exact zero-commit regression this row guards — + // aborts on an arithmetic overflow instead of printing the diagnostic below. + let life_rate = -per_cycle.delta.life.get(&seats[1]).copied().unwrap_or(0); + let lib_rate = -per_cycle + .delta + .library_delta + .get(&seats[0]) + .copied() + .unwrap_or(0); + assert!( + life_rate > 0 && lib_rate > 0, + "n={n}: ANTI-VACUITY — both published per-cycle rates must be strictly positive, \ + else the equality below degenerates to `0 == 0 * {n}` and asserts nothing. \ + published life={:?} library={:?}", + per_cycle.delta.life, + per_cycle.delta.library_delta + ); assert_eq!( - (&life_after, &libs_after), - (&life_before, &libs_before), - "n={n}: MEASURED — the accepted shortcut commits NOTHING. Cycle 0 answers Sue's \ - `may` from the pin and then aborts on Reed's UNPINNED `may`, and the whole cycle \ - is rolled back (CR 732.2a: an unpinned per-iteration choice is not a describable \ - predictable sequence). If this ever fails because a delta APPEARED, the announced \ - set widened and §6 R2a/R2b/R3/R5 must be written in the same change" + ( + life_before[1] - life_after[1], + libs_before[0] as i64 - libs_after[0] as i64 + ), + (life_rate * i64::from(n), lib_rate * i64::from(n)), + "n={n}: CR 732.2a — the accepted shortcut commits EXACTLY n repetitions of the \ + published per-cycle delta ({:?} loses {life_rate} life and {:?}'s library loses \ + {lib_rate} card(s) per repetition). life {life_before:?} -> {life_after:?}, libs \ + {libs_before:?} -> {libs_after:?}", + seats[1], + seats[0] ); assert!( matches!(state.waiting_for, WaitingFor::Priority { .. }), - "n={n}: CR 800.4a — the aborted drive hands back to ordinary priority, got {:?}", + "n={n}: CR 732.2a — the taken shortcut's ending point is a place where a player \ + has priority, got {:?}", state.waiting_for ); committed_per_n.push((life_after, libs_after)); } - assert_eq!( + assert_ne!( committed_per_n[0], committed_per_n[1], - "n=1 and n=3 must be INDISTINGUISHABLE: a partial commit would separate them, and a \ - partial commit is the one outcome CR 732.2a forbids outright" + "n=1 and n=3 must be DISTINGUISHABLE: the declared count is the whole content of a \ + CR 732.2a `Fixed(n)` grant, so an instrument that cannot separate them would satisfy \ + the per-n assertions above vacuously. This is the discriminator \ + `bounded_fixed_count_commits_exactly_n_periods` uses, adopted here now that this \ + board actually grants" ); } @@ -727,7 +910,14 @@ fn r23_5_reach_no_may_beat_of_the_f4_drive_carries_a_construction_cursor() { /// /// # What the row asserts /// -/// On the offer-beat board, ONE CR 614.1a replacement definition that the resolver's OWN +/// CR ANCHORS, CORRECTED: this row cited **CR 614.1a** for the choice. `614.1a` is +/// "effects that use the word *instead*" — a sub-rule, and not the one that makes an +/// optional replacement a choice. **CR 614.1** is the DEFINITION (replacement effects watch +/// for an event and replace it) and **CR 732.2a** is the LOAD-BEARING half: a shortcut +/// "can't include conditional actions, where the outcome of a game event determines the next +/// action a player takes". CR 616.1 stays where it belongs — the two-or-more ORDERING branch. +/// +/// On the offer-beat board, ONE CR 614.1 replacement definition that the resolver's OWN /// derivation draws turns the OFFER into `UnspecifiedChoiceWindow`; six definitions the /// resolver's derivation does NOT draw leave the offer standing. That contrast IS the claim: /// the obligation is **event-derived**, read off what the resolution proposes through @@ -754,8 +944,9 @@ fn r23_5_reach_no_may_beat_of_the_f4_drive_carries_a_construction_cursor() { /// /// * **(pos)** the UNMODIFIED offer-beat board OFFERS through the metered seam — asserted /// FIRST, so every refusal below is attributable to the definition and not to the replay. -/// * **(a)** one OPTIONAL `AddCounter` definition ⇒ `UnspecifiedChoiceWindow` (CR 614.1a: an -/// optional replacement is a genuine resolution-time choice ⇒ the period is not choice-free). +/// * **(a)** one OPTIONAL `AddCounter` definition ⇒ `UnspecifiedChoiceWindow` (CR 732.2a + +/// CR 614.1: an optional replacement is a genuine resolution-time choice, and a described +/// sequence may not contain one ⇒ the period is not choice-free). /// * **(a′)** the SAME definition, MANDATORY ⇒ still OFFERS. CR 616.1: a lone quantity /// modification commutes with nothing, so there is no ordering choice to make. This is what /// keeps (a) keyed to OPTIONALITY rather than to "a definition exists". @@ -786,7 +977,7 @@ fn r23_5_reach_no_may_beat_of_the_f4_drive_carries_a_construction_cursor() { /// optional replacement — and a MANDATORY entry publishes no `may`, so /// `pinned_may_choice_relief` returns `None` and conjunct (6) refuses there. Disable that /// detection and the entry classifies `FreeUnlessReplacements([AddCounter])`, whereupon the -/// CR 614.1a discharge conjunct refuses instead. Defence in depth is the property; a row that +/// CR 732.2a + CR 614.1 discharge conjunct refuses instead. Defence in depth is the property; a row that /// flipped on either single edit would have been asserting over only one of the two. /// /// ⚠ §6 R9's stated probe (*"swap `proposed_event_prompt_cause` back to a def-scan over @@ -818,7 +1009,10 @@ fn r9_the_offer_refuses_on_a_derived_replacement_obligation_not_on_a_definition_ // One definition, installed on an EXISTING P0-controlled permanent (never a new object), // so board membership — and therefore every certification premise — is untouched. - // CR 614.1a scopes a definition to its controller's events, and The Thing is P0's. + // CR ANCHOR CORRECTED with the two above it: this said "CR 614.1a scopes a definition to + // its controller's events". It does not — `614.1a` is the "effects that use the word + // *instead*" sub-rule and says nothing about controllers. CR 614.1 is the definition a + // replacement definition answers to: it watches for the event its own text names. let with_def = |event: ReplacementEvent, optional: bool| -> GameState { let mut hostile = healthy.clone(); let mut def = ReplacementDefinition::new(event.clone()); @@ -873,7 +1067,7 @@ fn r9_the_offer_refuses_on_a_derived_replacement_obligation_not_on_a_definition_ a_out, Err(engine::game::engine::BoundedOfferRefusal::UnspecifiedChoiceWindow) ), - "(a) CR 614.1a + CR 732.2a: an OPTIONAL replacement candidate applicable to an \ + "(a) CR 732.2a + CR 614.1: an OPTIONAL replacement candidate applicable to an \ ANNOUNCED entry's DERIVED event is a real resolution-time choice, so the period is \ not choice-free and the offer must be refused. got {a_out:?}, meter {a_meter:?}" ); @@ -887,24 +1081,40 @@ fn r9_the_offer_refuses_on_a_derived_replacement_obligation_not_on_a_definition_ to `a definition exists` rather than to OPTIONALITY. got {a2_out:?}, meter {a2_meter:?}" ); - // ── (b) the def-NAME discriminator: six optional definitions the resolver never draws ── + // ── (b) the def-NAME discriminator, RE-DERIVED: the one optional definition whose event + // this board's announced resolutions still never propose ── + let b_event = ReplacementEvent::RemoveCounter; + let (b_out, b_meter) = outcome(&with_def(b_event.clone(), true)); + assert!( + b_out.is_ok(), + "(b) {b_event:?}: this board's announced resolutions never PROPOSE this event, so an \ + event-derived obligation must ignore the definition entirely and the offer must \ + stand. A scan over `def.event` NAMES would refuse here exactly as it refuses in (a), \ + which is what makes this arm the discriminator. got {b_out:?}, meter {b_meter:?}" + ); + + // ── (b′) the five events the WIDENED announced set really does propose ── + // Once Torch's damage and Reed's draw are announced, `ChangeZone`/`Moved`/`CreateToken`/ + // `Draw`/`DamageDone` are genuinely derivable from this period's resolutions, so an + // OPTIONAL definition on any of them is a real CR 616.1 choice and must refuse. This arm + // is the paired positive control for (b): without it, (b) shrinking to one event could be + // read as the obligation going blind rather than as the proposal set widening. for event in [ ReplacementEvent::ChangeZone, ReplacementEvent::Moved, ReplacementEvent::CreateToken, ReplacementEvent::Draw, ReplacementEvent::DamageDone, - ReplacementEvent::RemoveCounter, ] { - let (b_out, b_meter) = outcome(&with_def(event.clone(), true)); + let (c_out, c_meter) = outcome(&with_def(event.clone(), true)); assert!( - b_out.is_ok(), - "(b) {event:?}: this board's announced resolutions never PROPOSE this event, so \ - an event-derived obligation must ignore the definition entirely and the offer \ - must stand. A scan over `def.event` NAMES — round 2's design — would refuse here \ - exactly as it refuses in (a), which is what makes this arm the discriminator. \ - (`ChangeZone`/`CreateToken` are §6 R9's own stated keying; see this row's doc for \ - why `Effect::Token` derives no token-entry event.) got {b_out:?}, meter {b_meter:?}" + matches!( + c_out, + Err(engine::game::engine::BoundedOfferRefusal::UnspecifiedChoiceWindow) + ), + "(b′) {event:?}: the widened announced set PROPOSES this event, so an OPTIONAL \ + replacement applicable to it is a genuine resolution-time choice and the offer \ + must refuse. got {c_out:?}, meter {c_meter:?}" ); } } @@ -1129,11 +1339,14 @@ fn optional_entries(state: &GameState) -> usize { // `handle_declare_shortcut` does with each member of it. // // ⚠ MEASURED SCOPE. §5 U6 as planned expects a declare candidate "whose template pins all -// three F4 slots (or declines)". F4 publishes ONE point, not three (see `r1b`), and the -// measured answer to the underlying question is the second branch: the AI DECLINES, because -// the only declaration it can emit is one the engine refuses outright. These rows pin that, -// name the two independent reasons, and pin the accepted shape the generator never emits — -// they do not assert the planned prediction. +// three F4 slots (or declines)". F4 does publish all THREE slots — `r1b` pins +// `[Sue MayChoice, Reed MayChoice, Torch Targets]` — and the measured answer is still the +// SECOND branch: the AI DECLINES, because the only declaration it can emit is one the engine +// refuses outright. The generator builds no pinning template at ALL (its only `Fixed` candidate +// carries `template: None`), so a published set of three is exactly as unreachable for it as a +// set of one would have been — the count is not what excludes it, its emptiness gate is. These +// rows pin that, name the two independent reasons, and pin the accepted shape the generator +// never emits — they do not assert the planned prediction. // ───────────────────────────────────────────────────────────────────────────────────────── /// §5 U6 (i) — MEASURED: at the real F4 bounded offer the engine's AI candidate generator @@ -1147,7 +1360,8 @@ fn optional_entries(state: &GameState) -> usize { /// `handle_declare_shortcut` refuses it — measured in /// [`u6_no_declaration_the_generator_can_emit_opens_the_window_while_the_accepted_shape_is_one_it_never_builds`]. /// * `Fixed(max_iterations)` is gated on `schema.points.is_empty()` — it carries -/// `template: None`, and a published pin set fail-closes on that. F4 publishes one point. +/// `template: None`, and a published pin set fail-closes on that. F4 publishes THREE points +/// (`r1b`), so the gate is closed with room to spare; ONE would already have closed it. /// /// So the AI declines because it has nothing else it can legally say, not because it emitted a /// declaration the engine then accepted-and-discarded. @@ -1260,10 +1474,10 @@ fn u6_the_ai_candidate_set_at_the_f4_offer_is_decline_only() { /// be satisfied by a board that refuses every declaration for some unrelated reason. With it, /// the three refusals are proved to be refusals of *those* declarations. /// -/// ⚠ This row deliberately does NOT assert that the accepted declaration accomplishes -/// anything — measured, it commits zero cycles ([`r2_an_accepted_declaration_commits_zero_cycles_because_reeds_may_is_unannounced`]). -/// Closing the generator gap would therefore ride the grant mechanism, which is why U6 reports -/// the gap rather than building the candidate. +/// ⚠ This row deliberately does NOT assert what the accepted declaration then accomplishes — +/// that is [`r2a_an_accepted_declaration_commits_exactly_n_cycles_because_reeds_may_is_announced`]'s +/// job, and it now measures an exact `n`-repetition commit (it measured a zero commit while +/// Reed's `may` was unpublished). Splitting the two keeps this row a DECLARE-time matrix. /// /// The `UntilLethal` rows are what justifies the generator's `!schema.is_bounded()` gate /// ([`u6_the_ai_candidate_set_at_the_f4_offer_is_decline_only`]): the engine refuses that count @@ -1425,3 +1639,535 @@ fn u6_the_declare_owner_firewall_holds_on_the_real_f4_offer() { so the event counts are exact rather than wildcards" ); } + +// ───────────────────────────────────────────────────────────────────────────────────────── +// B5f — the DECLARED term is load-bearing on a real board, in both directions +// ───────────────────────────────────────────────────────────────────────────────────────── + +/// §4 B5f — **`elimination_bounds`'s `declared_life_magnitude` can suppress an offer that is +/// otherwise legal, and the suppression is measured ONE LIFE POINT WIDE on the user's own +/// board.** +/// +/// CR 704.5a (a seat at 0 or less life has lost) + CR 732.2a (a shortcut describes a +/// PREDICTABLE sequence, so a repetition that could eliminate a seat mid-proposal is not +/// describable). Once the answer-beat sampling site announces Torch's CR 608.2b `Targets` +/// entry, `victim_slot` is non-empty and every declarable victim is charged +/// `observed.max(0) + S` rather than `observed` alone. On MODE1 that is `1 + 1 = 2`, so P1's +/// headroom must be at least 2 for a single legal repetition to exist. +/// +/// ARM (α), the matched positive: P1 seeded at **7** and at **6** — headroom 3 and 2 at the +/// offer beat — both OFFER, with `max_iterations == 1`. +/// ARM (β), the typed refusal: P1 seeded at **5** and at **4** — headroom 1 and 0 — the drive +/// reaches the SAME beat and raises NO window, and the typed verdict on that very board is +/// `NoNarrowedLegalCount`. Asserted BY REASON, never as a bare absence: a row that only +/// observes "no offer" stops testing its own conjunct the moment an earlier one refuses first. +/// +/// The two arms are **one life point apart** (6 offers, 5 refuses), which is what makes the +/// row about the divisor and not about the board. +/// +/// REVERT-PROBE (DROP): delete `declared_life_magnitude` from `elimination_bounds`'s additive +/// form ⇒ the divisor falls 2 → 1 ⇒ headroom 1 at P1=5 yields `1 / 1 == 1` ⇒ (β) OFFERS ⇒ +/// FLIPS. REVERT-PROBE (TRIVIALIZE): make the term unconditional (charge it to every seat, not +/// only to declarable victims) ⇒ P0/P2/P3 are charged 0 + 1 with 39 headroom, which does not +/// narrow below 1, so (α) survives — and the arm that flips is the reach-guard below, which +/// asserts P1 is the ONLY declarable victim on this board. +#[test] +fn b5f_the_declared_term_can_suppress_an_otherwise_legal_offer() { + use engine::game::engine::{ + try_offer_bounded_cycle_shortcut_metered, BoundedOfferRefusal, ProbeCap, + }; + + /// The MODE1 board with P1's life REPLACED. Every other field — including the stored + /// auto-choice guard (b) reads — is the user's own capture, so the only axis that moves + /// between the arms below is the headroom `elimination_bounds` divides. + fn seeded(life: i32) -> GameState { + let mut state = load_mode1(); + let p1 = state + .players + .iter_mut() + .find(|p| p.id == P1) + .expect("MODE1 is a 4-player board"); + p1.life = life; + state + } + + // ── ARM (α) — the matched positive, asserted FIRST ────────────────────────────────── + let mut alpha = seeded(7); + let alpha_beat = drive_f4_to_offer(&mut alpha, 400).expect( + "REACH-GUARD (α): MODE1 with P1 at 7 must raise the bounded offer, else every \ + refusal below is asserted over a board that was refusing anyway", + ); + let (proposer, certificate, schema) = offer_parts(&alpha); + let per_cycle = certificate + .per_cycle + .clone() + .expect("a bounded offer publishes its per-period signature"); + + // ── REACH-GUARD: the DECLARED term is what this row is about, so it must be non-zero, + // and P1 must be the only seat it is charged to. ── + let declared: i64 = per_cycle + .victim_slot + .iter() + .map(|(_, m)| *m) + .filter(|m| *m > 0) + .sum(); + assert!( + declared > 0, + "REACH-GUARD: `victim_slot` must publish a strictly positive magnitude, else the \ + additive term is 0 and (β) below would be about the observed drain alone; \ + victim_slot = {:?}", + per_cycle.victim_slot + ); + let declarable: std::collections::BTreeSet = schema + .points + .iter() + .filter_map(|p| match &p.kind { + DecisionPointKind::Targets { legal_targets, .. } => Some(legal_targets), + _ => None, + }) + .flatten() + .filter_map(|t| match t { + TargetRef::Player(p) => Some(*p), + _ => None, + }) + .collect(); + assert!( + declarable.contains(&P1), + "REACH-GUARD: P1 — the seat this row starves — must be a DECLARABLE victim of the \ + published `Targets` slot, or the extra term is never charged to it; declarable = \ + {declarable:?}" + ); + let observed_p1 = -per_cycle.delta.life.get(&P1).copied().unwrap_or(0); + let life_at_offer = alpha + .players + .iter() + .find(|p| p.id == P1) + .expect("P1 is seated") + .life as i64; + assert_eq!( + i64::from(schema.max_iterations), + (life_at_offer - 1) / (observed_p1.max(0) + declared), + "(α) CR 704.5a: the published bound is P1's headroom divided by the ADDITIVE \ + magnitude — observed {observed_p1} plus declared {declared} — at P1 life \ + {life_at_offer}. Under the `max` form this divisor would be \ + {} and the bound would be {}", + observed_p1.max(declared), + (life_at_offer - 1) / observed_p1.max(declared).max(1) + ); + assert_eq!( + schema.max_iterations, 1, + "(α) the seeded headroom admits exactly ONE legal repetition; a larger bound would \ + mean (β) is one point further away than this row claims" + ); + + let mut alpha6 = seeded(6); + assert_eq!( + drive_f4_to_offer(&mut alpha6, 400), + Some(alpha_beat), + "(α) the SECOND positive, one point down: P1 at 6 still offers, at the same beat. \ + This is the arm (β) is one life point away from" + ); + + // ── ARM (β) — the TYPED refusal, on the same beat the positive offered at ─────────── + for life in [5, 4] { + let mut beta = seeded(life); + assert_eq!( + drive_f4_to_offer(&mut beta, alpha_beat + 1), + None, + "(β) P1 at {life}: no window may be raised through beat {alpha_beat} — the beat \ + the (α) arms both offered at" + ); + let at_priority = replay_at_priority(&beta, proposer); + let (outcome, meter) = + try_offer_bounded_cycle_shortcut_metered(&at_priority, false, ProbeCap::Shipped); + assert!( + matches!(outcome, Err(BoundedOfferRefusal::NoNarrowedLegalCount)), + "(β) P1 at {life}: the refusal must be TYPED at the elimination bound — \ + `observed {observed_p1} + declared {declared}` exceeds P1's remaining headroom, \ + so no legal repetition count exists (CR 704.5a + CR 732.2a). A different variant \ + here means an EARLIER conjunct refused and this row stopped testing its own. \ + got {outcome:?}, meter {meter:?}" + ); + } +} + +// ───────────────────────────────────────────────────────────────────────────────────────── +// M1 / A1 — THE USER'S OWN TWO CAPTURES, DRIVEN TO AN ACCEPTED GRANT THAT COMMITS +// ───────────────────────────────────────────────────────────────────────────────────────── + +/// The published point set as `(source card name, kind)` — the offer's OWN data, read off +/// `state.waiting_for` rather than re-derived, so a row asserting a cause asserts the thing +/// the engine published. +fn published_point_names(state: &GameState) -> Vec<(String, &'static str)> { + let (_, _, schema) = offer_parts(state); + schema + .points + .iter() + .map(|p| { + let source = match &p.slot.source { + engine::types::game_state::YieldTarget::ThisObject { source_id, .. } => state + .objects + .get(source_id) + .map(|o| o.name.clone()) + // NOT a synthetic `obj`: every caller compares this string against the + // SUE / REED / TORCH constants, so an unresolvable source would read as + // "not that card" and silently SATISFY the by-name ABSENCE assertions this + // helper feeds (m1's owner-firewall row). Same class of failure as the + // `other =>` arm below, so the same treatment. + .unwrap_or_else(|| { + panic!( + "a published point names {source_id:?}, absent from `objects` — an \ + unresolvable name would silently satisfy the by-name ABSENCE \ + assertions this helper feeds" + ) + }), + other => panic!("unexpected decision source {other:?}"), + }; + let kind = match &p.kind { + DecisionPointKind::MayChoice => "MayChoice", + DecisionPointKind::Targets { .. } => "Targets", + other => panic!("unexpected point kind {other:?}"), + }; + (source, kind) + }) + .collect() +} + +/// THE GUARD ABOVE MUST BE ABLE TO FIRE. A guard that cannot is worse than none: it reads as +/// protection while the hole it names stays open, which is the exact defect the synthetic +/// `obj` fallback was. Drive the real capture to its offer, then delete the first +/// published point's source object — the one state the fallback used to paper over — and +/// require the typed panic. `expected` is a substring match, so a panic from any OTHER cause +/// (an empty point set, a non-`ThisObject` source) fails this row instead of passing it. +#[test] +#[should_panic(expected = "absent from `objects`")] +fn published_point_names_panics_when_a_points_source_is_absent() { + let mut state = load_f4(); + drive_f4_to_offer(&mut state, 400).expect("the bounded offer fires (see R1)"); + let (_, _, schema) = offer_parts(&state); + let source_id = match &schema + .points + .first() + .expect("the offer publishes at least one point") + .slot + .source + { + engine::types::game_state::YieldTarget::ThisObject { source_id, .. } => *source_id, + other => panic!("unexpected decision source {other:?}"), + }; + state.objects.remove(&source_id); + published_point_names(&state); +} + +/// Drive one user capture to its offer, declare a CONFORMANT `Fixed(n)`, have every living +/// opponent Accept, and measure what the grant actually committed. +/// +/// The life, library and COUNTER axes are asserted EXACTLY and every expectation is DERIVED +/// FROM THE OFFER'S OWN published `per_cycle.delta` — `n` repetitions of the signature the +/// certificate itself carries — so no repetition rate is hard-coded and a re-dump flows +/// through unedited. Each of the three carries an ANTI-VACUITY guard on the published rate, +/// because `x == rate * n` is satisfied by any `x` when `rate` is zero. +/// +/// ⚠ THE COUNTER AXIS WAS WEAKENED FOR A REASON THAT WAS FALSE. The note here used to say the +/// counter axis is event-fed and left at zero by `ResourceVector::snapshot`. MEASURED, the +/// published vector carries `counters: {(Plus1Plus1, Creature): 2}` — non-zero, and +/// state-readable (`snapshot` walks the battlefield for it). The real obstacle was the +/// ACCESSOR: [`commit_axes`] reads ONE named object's counters (The Thing) while the published +/// key `(CounterClass, ObjectClass)` is an AGGREGATE over every battlefield object of that +/// class, so the two are not comparable quantities. Asserted here against the aggregate +/// accessor the certificate is minted from, and still returned for the caller's per-object +/// `n`-scaling arm. MEASURED on both captures: aggregate `(Plus1Plus1, Creature)` moves `2` +/// at `n = 1` and `6` at `n = 3`, i.e. exactly `2n`, which is the assertion this note's false +/// predecessor had waved off as underivable. +/// +/// The TOKEN axis genuinely cannot be asserted against the certificate: `tokens_created` IS +/// event-fed, and the published vector carries `tokens_created: 0` on both captures, so an +/// exact expectation derived from it would be the vacuous `0 == 0 * n`. It keeps the +/// `n`-scaling arm alone. +/// +/// Returns `(offer beat, published points, Thing-counter delta, token delta)`. +fn accept_a_fixed_grant( + mut state: GameState, + n: u32, + label: &str, +) -> (u32, Vec<(String, &'static str)>, i64, i64) { + let beat = drive_f4_to_offer(&mut state, 400).unwrap_or_else(|| { + panic!("[{label} n={n}] REACH-GUARD: the CR 732.2a bounded offer must FIRE on this capture") + }); + let (proposer, certificate, schema) = offer_parts(&state); + let per_cycle = certificate + .per_cycle + .clone() + .expect("a bounded offer publishes its per-period signature"); + let schema = schema.clone(); + assert!( + schema.max_iterations >= n, + "[{label} n={n}] REACH-GUARD: the published bound {} must admit this count, else the \ + declaration is refused for a reason that has nothing to do with the drive", + schema.max_iterations + ); + let points = published_point_names(&state); + let before = commit_axes(&state); + let before_rv = ResourceVector::snapshot(&state); + + let template = f4_pin_template(&schema, proposer, n); + apply( + &mut state, + proposer, + GameAction::DeclareShortcut { + count: IterationCount::Fixed(n), + template: Some(template), + }, + ) + .expect("the conformant declaration is dispatched"); + assert!( + matches!(state.waiting_for, WaitingFor::RespondToShortcut { .. }), + "[{label} n={n}] the declaration must be ACCEPTED and open the CR 732.2b APNAP window; \ + a `Priority` here is a DECLARE-time refusal, a different defect entirely. got {:?}", + state.waiting_for + ); + let responders = accept_all_opponents(&mut state); + assert!( + responders > 0, + "[{label} n={n}] REACH-GUARD: at least one living opponent must have answered the \ + CR 732.2c window, else the grant was never put to the table" + ); + + let after = commit_axes(&state); + let measured = ResourceVector::delta(&before_rv, &ResourceVector::snapshot(&state)); + // ── ANTI-VACUITY on the published RATES (F3) ───────────────────────────────────────── + // Every equality below has the shape `moved == rate * n`, which an all-zero certificate + // satisfies with a board that never moved. The counters/tokens half already guards this + // in `assert_axis_scales`; these are the life and library halves' matching guards. + assert!( + per_cycle.delta.life.values().any(|&rate| rate != 0), + "[{label} n={n}] ANTI-VACUITY: the published per-cycle LIFE delta must move some \ + seat, else every life equality below is `0 == 0 * {n}` and asserts nothing. \ + published life = {:?}", + per_cycle.delta.life + ); + assert!( + per_cycle + .delta + .library_delta + .values() + .any(|&rate| rate != 0), + "[{label} n={n}] ANTI-VACUITY: the published per-cycle LIBRARY delta must move some \ + seat, else every library equality below is `0 == 0 * {n}` and asserts nothing. \ + published library = {:?}", + per_cycle.delta.library_delta + ); + + for (i, player) in state.players.iter().enumerate() { + let life_rate = per_cycle.delta.life.get(&player.id).copied().unwrap_or(0); + assert_eq!( + i64::from(after.0[i]) - i64::from(before.0[i]), + life_rate * i64::from(n), + "[{label} n={n}] CR 732.2a: seat {:?}'s life must move by EXACTLY {n} repetitions \ + of the offer's own published per-cycle life delta ({life_rate}). \ + before={:?} after={:?}", + player.id, + before.0, + after.0 + ); + let lib_rate = per_cycle + .delta + .library_delta + .get(&player.id) + .copied() + .unwrap_or(0); + assert_eq!( + after.1[i] as i64 - before.1[i] as i64, + lib_rate * i64::from(n), + "[{label} n={n}] CR 732.2a: seat {:?}'s library must move by EXACTLY {n} \ + repetitions of the published per-cycle library delta ({lib_rate}). \ + before={:?} after={:?}", + player.id, + before.1, + after.1 + ); + } + // ── THE COUNTER AXIS, EXACTLY (F4) ─────────────────────────────────────────────────── + // CR 122.1 + CR 732.2a. Against the AGGREGATE accessor the certificate is minted from, + // not against `commit_axes`'s single named object — that mismatch, not "the axis is + // event-fed", is why this assertion was previously only a scaling arm. + assert!( + per_cycle.delta.counters.values().any(|&rate| rate != 0), + "[{label} n={n}] ANTI-VACUITY: the published per-cycle COUNTER delta must be \ + non-zero, else the equality below is `0 == 0 * {n}`. published = {:?}", + per_cycle.delta.counters + ); + for (key, rate) in &per_cycle.delta.counters { + assert_eq!( + measured.counters.get(key).copied().unwrap_or(0), + rate * i64::from(n), + "[{label} n={n}] CR 732.2a: the {key:?} counter axis must move by EXACTLY {n} \ + repetitions of the offer's own published per-cycle rate ({rate}). \ + measured = {:?}", + measured.counters + ); + } + // Nothing may move on a counter axis the certificate never published: a commit that + // pumped an unpublished counter class would satisfy every equality above and still be a + // cycle the offer did not describe. + for (key, moved) in &measured.counters { + if *moved != 0 { + assert!( + per_cycle.delta.counters.contains_key(key), + "[{label} n={n}] CR 732.2a: {key:?} moved by {moved} but is absent from the \ + published per-cycle signature {:?}", + per_cycle.delta.counters + ); + } + } + + assert!( + matches!(state.waiting_for, WaitingFor::Priority { .. }), + "[{label} n={n}] CR 732.2a: a taken shortcut's ending point is a place where a player \ + has priority, got {:?}", + state.waiting_for + ); + ( + beat, + points, + i64::from(after.2) - i64::from(before.2), + after.3 as i64 - before.3 as i64, + ) +} + +/// The `n`-scaling arm shared by both captures: every axis a cycle moves must move `n` times +/// as far at `n = 3` as at `n = 1`, and must move AT ALL at `n = 1`. +/// +/// The non-zero guard is the anti-vacuity half and is not decoration: `3 * 0 == 0`, so without +/// it an axis that never moved would satisfy the scaling equality silently. Together the two +/// halves are the discriminator `bounded_fixed_count_commits_exactly_n_periods` uses — a +/// partial commit, a saturating commit and a zero commit each break one of them. +fn assert_axis_scales(label: &str, axis: &str, at_1: i64, at_3: i64) { + assert_ne!( + at_1, 0, + "[{label}] ANTI-VACUITY: the {axis} axis must MOVE on a single committed repetition, \ + else the scaling equality below is `3 * 0 == 0` and asserts nothing" + ); + assert_eq!( + at_3, + at_1 * 3, + "[{label}] CR 732.2a: three repetitions must move the {axis} axis exactly three times \ + as far as one ({at_1}); a partial or saturating commit separates them" + ); +} + +/// **M1 — the user's own capture that raised NO offer at all now offers, and the accepted +/// grant COMMITS on every axis one cycle moves.** +/// +/// CR 732.2a + CR 603.5. MODE1's distinguishing field is a stored `may_trigger_auto_choices` +/// entry — the user's "always take" for Sue's `may`. Guard (b) of `entry_publishes_pin_slots` +/// WITHHOLDS a pin slot the CR 603.5 gate can never spend, so Sue's `MayChoice` is deliberately +/// absent from the published set; the gate is discharged instead by the auto-answer relief. +/// That is the whole reason this board raised nothing before: the relief did not exist, so a +/// stored answer looked like an unanswerable choice. +/// +/// The row asserts the CAUSE alongside the effect, so a green cannot be read as "some offer +/// appeared": +/// +/// * the capture's identity is reach-guarded (`may_trigger_auto_choices` NON-EMPTY) — on a +/// board without one, the relief path is not the mechanism under test; +/// * Sue is asserted ABSENT from the published points while Reed and Torch are PRESENT, which +/// is guard (b) discriminating between a stored answer and an open choice on ONE board; +/// * every axis is asserted exactly, against the offer's own published per-cycle signature. +/// +/// REVERT-PROBE: ablate the CR 603.5 auto-answer relief in `auto_may_choice_relief` ⇒ gate (6) +/// can no longer be discharged for Sue's withheld slot ⇒ no offer fires ⇒ the reach-guard in +/// `accept_a_fixed_grant` FLIPS. Positive control: the same drive on MODE2, whose +/// `may_trigger_auto_choices` is EMPTY, reaches its offer through the ordinary publication +/// path (the row below) — so "the drive reaches an offer" is not a property of the harness. +#[test] +fn m1_the_users_stored_auto_choice_board_offers_and_the_grant_commits_on_every_axis() { + let identity = load_mode1(); + assert!( + !identity.may_trigger_auto_choices.is_empty(), + "REACH-GUARD: MODE1 is the capture whose CR 603.5 answer is STORED; without one, guard \ + (b) withholds nothing and this row measures the ordinary publication path instead" + ); + + let (beat1, points, counters_1, tokens_1) = accept_a_fixed_grant(load_mode1(), 1, "MODE1"); + assert!( + points + .iter() + .any(|(src, kind)| src == REED && *kind == "MayChoice") + && points + .iter() + .any(|(src, kind)| src == TORCH && *kind == "Targets"), + "MODE1: the two choices with NO stored answer must be PUBLISHED — that is the paired \ + positive that makes Sue's absence below an attribution rather than an empty set. \ + published = {points:?}" + ); + assert!( + !points.iter().any(|(src, _)| src == SUE), + "MODE1 THE CAUSE: Sue's `may` is answered by the user's stored auto-choice, so guard \ + (b) withholds a pin slot the CR 603.5 gate could never spend and the relief discharges \ + gate (6) instead. published = {points:?}" + ); + + let (beat3, _, counters_3, tokens_3) = accept_a_fixed_grant(load_mode1(), 3, "MODE1"); + assert_eq!( + beat1, beat3, + "the two arms must offer at the SAME beat — they are one declared count apart and \ + nothing else" + ); + assert_axis_scales("MODE1", "The Thing's counters", counters_1, counters_3); + assert_axis_scales("MODE1", "token", tokens_1, tokens_3); +} + +/// **A1 — the user's own capture where the accepted grant committed NOTHING now commits on +/// every axis, and the declared count scales it.** +/// +/// CR 732.2a. This is the capture the user took after clearing the stored auto-choice as a +/// workaround: the offer fired, the declaration was accepted, and the drive then rolled the +/// whole cycle back and re-offered — because Reed's `may` resolves across a forced +/// pre-priority window that the ring sampler could not see, so the offer published a pin set +/// that did not cover every per-iteration choice and cycle 0 aborted on the first uncovered +/// one. +/// +/// With the answer-beat sampling site the announced set contains all three choices, so the +/// published set covers the cycle and the grant commits. The row is the fix bar for this +/// change: it asserts a commit on ALL FOUR axes and `n = 1` vs `n = 3` DISTINGUISHABLE. +/// +/// * the capture's identity is reach-guarded (`may_trigger_auto_choices` EMPTY), which is +/// MODE1's field inverted — the two captures are one axis apart; +/// * all three sources are asserted PUBLISHED, naming the cause of the commit; +/// * every axis is asserted exactly, against the offer's own published per-cycle signature. +/// +/// REVERT-PROBE: ablate the answer-beat sampling site ⇒ Reed's and Torch's entries are never +/// announced ⇒ the published set shrinks ⇒ cycle 0 aborts on the uncovered `may` ⇒ every axis +/// delta collapses to 0 ⇒ both the exact-axis assertions and the scaling arm FLIP. +#[test] +fn a1_the_users_accept_committed_nothing_board_now_commits_on_every_axis() { + let identity = load_mode2(); + assert!( + identity.may_trigger_auto_choices.is_empty(), + "REACH-GUARD: MODE2 is the POST-workaround capture — the user cleared the stored \ + answer, so this board reaches its offer through the ordinary CR 603.5 publication \ + path and not through the relief MODE1 exercises" + ); + + let (beat1, points, counters_1, tokens_1) = accept_a_fixed_grant(load_mode2(), 1, "MODE2"); + for expected in [(SUE, "MayChoice"), (REED, "MayChoice"), (TORCH, "Targets")] { + assert!( + points + .iter() + .any(|(src, kind)| src == expected.0 && *kind == expected.1), + "MODE2 THE CAUSE: every per-iteration choice this cycle opens must be PUBLISHED, \ + or the drive aborts on the first uncovered one and commits nothing — which is \ + exactly what the user captured. missing {expected:?}; published = {points:?}" + ); + } + + let (beat3, _, counters_3, tokens_3) = accept_a_fixed_grant(load_mode2(), 3, "MODE2"); + assert_eq!( + beat1, beat3, + "the two arms must offer at the SAME beat — they are one declared count apart and \ + nothing else" + ); + assert_axis_scales("MODE2", "The Thing's counters", counters_1, counters_3); + assert_axis_scales("MODE2", "token", tokens_1, tokens_3); +} diff --git a/crates/engine/tests/integration/loop_shortcut.rs b/crates/engine/tests/integration/loop_shortcut.rs index 1931072877..f716c86b29 100644 --- a/crates/engine/tests/integration/loop_shortcut.rs +++ b/crates/engine/tests/integration/loop_shortcut.rs @@ -8630,9 +8630,11 @@ fn multiplayer_pure_life_drain_offers_at_three_and_four_players() { .as_ref() .expect("a bounded offer publishes its per-period signature"); assert_eq!( - per_cycle.frames_per_period, 1, - "{seats}p: a PERIOD-WIDTH tripwire, not a basis attribution. This cascade's \ - certifying prior sits one retained frame back, so its MEASURED span is 1 — a drift \ + per_cycle.frames_per_period, 2, + "{seats}p: a PERIOD-WIDTH tripwire, not a basis attribution. This cascade puts its \ + two same-controller triggers on the stack through a CR 603.3b `OrderTriggers` \ + window, and the answer-beat sampling site retains a frame there as well as at the \ + settle — so ONE repetition now spans 2 retained frames. A drift \ means the fixture changed shape and the row must be re-derived, not relaxed. It \ establishes nothing about the basis in either direction: basis B derives k from 1 \ upward, and since fix round 1 basis A measures its span too (2 on \ @@ -10241,16 +10243,8 @@ fn r5_board() -> (GameRunner, ObjectId, ObjectId, ObjectId) { /// A `Fixed(count)` template pinning the Sanguine Bond trigger's `target opponent` to one /// seat for every iteration. The slot's source is the Bond itself, so `slot_source_prompted` /// matches the mid-drive `TriggerTargetSelection` the injector must answer. -fn r5_pin_template(bond: ObjectId, seat: PlayerId, count: u32) -> DecisionTemplate { - let source = YieldTarget::ThisObject { - source_id: bond, - incarnation: None, - trigger_description: None, - }; - let slot = DecisionSlot { - source: source.clone(), - index: 0, - }; +fn r5_pin_template(slot: DecisionSlot, seat: PlayerId, count: u32) -> DecisionTemplate { + let source = slot.source.clone(); DecisionTemplate { owner: P0, decisions: vec![PinnedDecision::Targets { @@ -10269,7 +10263,7 @@ fn r5_pin_template(bond: ObjectId, seat: PlayerId, count: u32) -> DecisionTempla /// /// The offer is the ENGINE's, read off `state.waiting_for` — never an out-of-band call to the /// offer predicate, which would only prove the predicate agrees with itself. -fn r5_reach_offer() -> (GameRunner, ObjectId, ObjectId, Vec) { +fn r5_reach_offer() -> (GameRunner, DecisionSlot, ObjectId, ObjectId, Vec) { let (mut runner, bond, hexproof_src, kickoff) = r5_board(); let _ = runner.cast(kickoff).target_player(P1).resolve(); let WaitingFor::LoopShortcut { @@ -10282,33 +10276,60 @@ fn r5_reach_offer() -> (GameRunner, ObjectId, ObjectId, Vec) { ); }; assert_eq!(proposer, P0, "P0 has priority and proposes the shortcut"); - // LAYER ATTRIBUTION, half one: this offer publishes NO decision points, so - // `handle_declare_shortcut`'s pin firewall (`if !offer.schema.points.is_empty()`) is - // provably not the refuser in the kill arm below. Whatever refuses there is downstream. + // SHAPE PIN, re-derived: the Bond's `target opponent` trigger resolves across a + // `TriggerTargetSelection` window, so the answer-beat sampling site announces its entry + // and the offer publishes exactly ONE CR 608.2b `Targets` point for the Bond's own slot. + // A drift here means the announced set changed shape and the callers must be re-derived, + // not relaxed. + // + // LAYER ATTRIBUTION NO LONGER RESTS ON EMPTINESS, and no shared helper replaces it — each + // caller measures the declare-time outcome ITSELF, on its own board. The kill arm of + // `a_declared_target_made_illegal_mid_drive_stops_short_and_never_retargets` asserts + // `WaitingFor::RespondToShortcut` immediately after its `DeclareShortcut` ("LAYER + // ATTRIBUTION, half two"), which proves the declare firewall INGESTED that declaration and + // therefore that the refusal it measures later is the DRIVE's; the r28 rows assert the + // complementary declare-time refusal on their own staged schemas. + assert_eq!( + schema.points.len(), + 1, + "the R5 offer publishes the Bond's re-aimable `Targets` slot and nothing else; got \ + {:?}", + schema.points + ); assert!( - schema.points.is_empty(), - "this offer publishes no points, so declare-time `validate_pins` never runs — the \ - kill arm's refusal must therefore come from the drive; got {} points", - schema.points.len() + matches!( + schema.points[0].kind, + DecisionPointKind::Targets { + min_targets: 1, + max_targets: 1, + .. + } + ), + "the published point is the Bond trigger's single-player target slot; got {:?}", + schema.points[0].kind ); + // CR 732.2a: the ENGINE-issued slot is the pin authority. Hand-assembling one here + // silently drifted from it (`incarnation: None` vs the published `Some(0)`), which + // `validate_pins` then rejected — a test artefact, not an engine defect. + let pinned_slot = schema.points[0].slot.clone(); let lives = vec![ life(&runner, P0), life(&runner, P1), life(&runner, P2), life(&runner, P3), ]; - (runner, bond, hexproof_src, lives) + (runner, pinned_slot, bond, hexproof_src, lives) } /// The per-cycle life the pinned seat loses, probed by an independent `Fixed(1)` /// materialization of this same board (one recurrence = one full cycle). Mirrors /// [`probe_drain_delta`]; nothing below is bound to a literal drain rate. fn r5_probe_delta() -> i32 { - let (mut runner, bond, _hexproof_src, l0) = r5_reach_offer(); + let (mut runner, slot, _bond, _hexproof_src, l0) = r5_reach_offer(); runner .act(GameAction::DeclareShortcut { count: IterationCount::Fixed(1), - template: Some(r5_pin_template(bond, P1, 1)), + template: Some(r5_pin_template(slot.clone(), P1, 1)), }) .expect("declare Fixed(1) with a Player pin"); accept_all_opponents(&mut runner); @@ -10436,11 +10457,11 @@ fn a_declared_target_made_illegal_mid_drive_stops_short_and_never_retargets() { // ───────────────────────── CLEAN arm — the positive control ───────────────────────── // Identical board, hexproof source left in hand (its static does not function there), so the // ONLY difference from the kill arm is whether the refuser is on the battlefield. - let (mut clean, clean_bond, _clean_hexproof_src, clean_l0) = r5_reach_offer(); + let (mut clean, clean_slot, _clean_bond, _clean_hexproof_src, clean_l0) = r5_reach_offer(); clean .act(GameAction::DeclareShortcut { count: IterationCount::Fixed(N), - template: Some(r5_pin_template(clean_bond, P1, N)), + template: Some(r5_pin_template(clean_slot.clone(), P1, N)), }) .expect("declare Fixed(N) with a Player pin"); accept_all_opponents(&mut clean); @@ -10456,7 +10477,7 @@ fn a_declared_target_made_illegal_mid_drive_stops_short_and_never_retargets() { ); // ───────────────────────────────── KILL arm ───────────────────────────────────────── - let (mut runner, bond, hexproof_src, l0) = r5_reach_offer(); + let (mut runner, slot, bond, hexproof_src, l0) = r5_reach_offer(); assert!( !engine::game::static_abilities::player_has_hexproof(runner.state(), P1), "setup anti-vacuity: the pinned seat must START without hexproof, or the kill below \ @@ -10466,7 +10487,7 @@ fn a_declared_target_made_illegal_mid_drive_stops_short_and_never_retargets() { runner .act(GameAction::DeclareShortcut { count: IterationCount::Fixed(N), - template: Some(r5_pin_template(bond, P1, N)), + template: Some(r5_pin_template(slot.clone(), P1, N)), }) .expect("declare Fixed(N) with a Player pin"); // LAYER ATTRIBUTION, half two: the declare-time firewall INGESTED this declaration. The @@ -10693,13 +10714,11 @@ fn a_recorded_loop_detect_sample_keeps_a_live_half_normalization_would_have_eras // ─────────── 5d U2 / R28 — the declared template's `owner` is ENGINE-BOUND ─────────── -/// The engine-issued offer's own point set, hand-assembled to match `r5_pin_template`'s slot. -/// -/// The R5 board's live offer publishes an EMPTY schema (`r5_reach_offer` asserts it), so a -/// NON-empty-schema declaration has to be staged. This is the tree's own idiom for staging a -/// `LoopShortcut` wait; `offer.proposer` — the firewall's engine-issued comparand — still comes -/// from `WaitingFor::LoopShortcut`, which is what the row is about. -fn r28_nonempty_schema_offer(runner: &mut GameRunner, bond: ObjectId) { +/// CR 732.2a: stage the live offer with an EMPTY point set, so arm (a″) can reach the +/// `!offer.schema.points.is_empty()` block's SKIPPED path. Counterpart to +/// [`r28_nonempty_schema_offer`]; `offer.proposer` still comes from the live +/// `WaitingFor::LoopShortcut`, which is the firewall's engine-issued comparand. +fn r28_empty_schema_offer(runner: &mut GameRunner) { let WaitingFor::LoopShortcut { proposer, predicted_winner, @@ -10709,13 +10728,32 @@ fn r28_nonempty_schema_offer(runner: &mut GameRunner, bond: ObjectId) { else { panic!("staged from the live offer, never from thin air"); }; - let slot = DecisionSlot { - source: YieldTarget::ThisObject { - source_id: bond, - incarnation: None, - trigger_description: None, + runner.state_mut().waiting_for = WaitingFor::LoopShortcut { + proposer, + predicted_winner, + certificate, + schema: ShortcutDecisionSchema { + points: vec![], + ..schema }, - index: 0, + }; +} + +/// The engine-issued offer's own point set, hand-assembled to match `r5_pin_template`'s slot. +/// +/// The R5 board's live offer publishes ONE `Targets` point whose `legal_targets` are minted +/// from the live board; this stages the same shape with a FIXED target list so the row is +/// insensitive to seat-population drift. `offer.proposer` — the firewall's engine-issued +/// comparand — still comes from `WaitingFor::LoopShortcut`, which is what the row is about. +fn r28_nonempty_schema_offer(runner: &mut GameRunner, slot: DecisionSlot) { + let WaitingFor::LoopShortcut { + proposer, + predicted_winner, + certificate, + schema, + } = runner.state().waiting_for.clone() + else { + panic!("staged from the live offer, never from thin air"); }; runner.state_mut().waiting_for = WaitingFor::LoopShortcut { proposer, @@ -10761,8 +10799,8 @@ fn r28_nonempty_schema_offer(runner: &mut GameRunner, bond: ObjectId) { #[test] fn r28_a_declared_template_owning_another_seat_is_refused_at_declare() { for hostile in [false, true] { - let (mut runner, bond, _hexproof, _lives) = r5_reach_offer(); - r28_nonempty_schema_offer(&mut runner, bond); + let (mut runner, slot, _bond, _hexproof, _lives) = r5_reach_offer(); + r28_nonempty_schema_offer(&mut runner, slot.clone()); let WaitingFor::LoopShortcut { schema, .. } = runner.state().waiting_for.clone() else { panic!("staged offer"); }; @@ -10773,7 +10811,7 @@ fn r28_a_declared_template_owning_another_seat_is_refused_at_declare() { `validate_pins` really run and (a′) proves they PASS" ); - let mut template = r5_pin_template(bond, P1, 1); + let mut template = r5_pin_template(slot.clone(), P1, 1); if hostile { template.owner = P1; } @@ -10845,19 +10883,29 @@ fn r28_a_declared_template_owning_another_seat_is_refused_at_declare() { /// `validate_pins` both live inside it. Arms (a)/(a′) run on a non-empty schema and therefore /// pass whether the firewall is inside the block or outside it. /// -/// The R5 offer's schema is empty (asserted by `r5_reach_offer`), so this arm reaches exactly -/// that path. +/// ⚠ **DISCLOSED REACHABILITY DOWNGRADE.** This arm used to run on the R5 offer's OWN empty +/// schema — the empty-schema path was reached NATURALLY. It no longer is: the answer-beat +/// sampling site announces the Bond's trigger entry, so the LIVE schema now publishes one +/// `Targets` point (`r5_reach_offer` pins that shape). BOTH arms below therefore STAGE the +/// empty schema through `r28_empty_schema_offer`, the same idiom `r28_nonempty_schema_offer` +/// uses in the other direction. What survives the downgrade: `offer.proposer` — the firewall's +/// engine-issued comparand — is still the live one, and the matched positive accepts an honest +/// declaration on the SAME staged path, so the row still discriminates the firewall from "the +/// staged path refuses everything". What does NOT survive: the claim that a real board reaches +/// this path on its own. Treat that as unproven here until a fixture whose live offer publishes +/// nothing is added. /// /// REVERT-PROBE: move the firewall INSIDE the `!offer.schema.points.is_empty()` block ⇒ the /// wrong-owner declaration is accepted here ⇒ **(a″) FLIPS TO FAIL** while (a)/(a′) stay green. #[test] fn r28_a_the_owner_firewall_is_reached_on_an_empty_schema_offer_too() { // matched positive first: the empty-schema path DOES accept an honest declaration. - let (mut runner, bond, _h, _l) = r5_reach_offer(); + let (mut runner, slot, _bond, _h, _l) = r5_reach_offer(); + r28_empty_schema_offer(&mut runner); runner .act(GameAction::DeclareShortcut { count: IterationCount::Fixed(1), - template: Some(r5_pin_template(bond, P1, 1)), + template: Some(r5_pin_template(slot.clone(), P1, 1)), }) .expect("declare"); assert!( @@ -10869,8 +10917,9 @@ fn r28_a_the_owner_firewall_is_reached_on_an_empty_schema_offer_too() { refusal below is the firewall and not the empty-schema path refusing everything" ); - let (mut runner, bond, _h, _l) = r5_reach_offer(); - let mut template = r5_pin_template(bond, P1, 1); + let (mut runner, slot, _bond, _h, _l) = r5_reach_offer(); + r28_empty_schema_offer(&mut runner); + let mut template = r5_pin_template(slot.clone(), P1, 1); template.owner = P1; let result = runner .act(GameAction::DeclareShortcut { @@ -10921,11 +10970,11 @@ fn r28_c_a_restored_proposal_with_a_foreign_template_owner_is_refused_at_consump for hostile in [false, true] { for trusted in [false, true] { let label = format!("hostile={hostile} trusted={trusted}"); - let (mut runner, bond, _h, lives) = r5_reach_offer(); + let (mut runner, slot, _bond, _h, lives) = r5_reach_offer(); runner .act(GameAction::DeclareShortcut { count: IterationCount::Fixed(1), - template: Some(r5_pin_template(bond, P1, 1)), + template: Some(r5_pin_template(slot.clone(), P1, 1)), }) .expect("declare opens APNAP"); @@ -10952,7 +11001,6 @@ fn r28_c_a_restored_proposal_with_a_foreign_template_owner_is_refused_at_consump // consequence here is that ingress I3 is reachable only for `per_cycle: None` // proposals, which is exactly the shipped `Some(template)` population. The guard // under test does not read `per_cycle`, so nulling it costs the row nothing. - proposal.per_cycle = None; // The TRUSTED arm must carry a real resolution-wire envelope, not a bare // `GameState` under a `"state"` key. Upstream #6933 made @@ -11033,3 +11081,277 @@ fn r28_c_a_restored_proposal_with_a_foreign_template_owner_is_refused_at_consump } } } + +// ─────── AI1 — the AI's bounded-declare candidate withdraws on a 0→1 schema ─────── + +/// **AI1 — the generator's `Fixed(max)` candidate is keyed to the PUBLISHED PIN SET, measured +/// in BOTH directions on ONE board.** +/// +/// CR 732.2a. `ai_support::candidates` emits `DeclareShortcut { count: Fixed(max_iterations), +/// template: None }` only `if schema.points.is_empty() && schema.is_bounded()`, because a +/// `template: None` declaration fail-closes against a published pin set — the engine would +/// ACCEPT it and then discard it, handing the search layer an action that looks legal and is +/// not. +/// +/// The R5 offer is exactly the board that MOVED: it used to publish nothing (so the `Fixed` +/// candidate was emitted), and the answer-beat sampling site now announces the Bond's trigger +/// entry, so it publishes one `Targets` point. This row is the pin for that transition. +/// +/// * **arm (a), the live board:** one published point ⇒ the candidate set is `DeclineShortcut` +/// alone, and specifically carries NO `Fixed` declaration. +/// * **arm (b), the POSITIVE CONTROL, same board one field apart:** stage the schema's `points` +/// empty ([`r28_empty_schema_offer`]) ⇒ the `Fixed` candidate RETURNS. Without this arm, +/// arm (a) would be satisfied by a generator that had stopped emitting `Fixed` for any +/// reason at all — including not running. +/// +/// Both arms read the ENGINE's candidate set through `legal_actions`, the same seam +/// `phase-ai`'s search calls, so this is not a re-implementation of the gate agreeing with +/// itself. The row is deliberately NOT `#[ignore]`d: the two pre-existing `phase-ai` bounded +/// rows are, and an ignored row reports `ok` while executing nothing. +#[test] +fn ai1_the_bounded_declare_candidate_withdraws_when_the_offer_publishes_a_pin() { + // ── arm (a): the LIVE offer, which now publishes one point ── + let (mut runner, _slot, _bond, _hexproof, _lives) = r5_reach_offer(); + let WaitingFor::LoopShortcut { schema, .. } = runner.state().waiting_for.clone() else { + panic!("r5_reach_offer returns at the offer"); + }; + assert!( + schema.is_bounded(), + "REACH-GUARD: the `Fixed` candidate is gated on `is_bounded()` as well, so an unbounded \ + offer would withhold it for the wrong reason" + ); + assert_eq!( + schema.points.len(), + 1, + "REACH-GUARD: the published pin set is the conjunct this row is about; got {:?}", + schema.points + ); + let live = engine::ai_support::legal_actions(runner.state()); + assert_eq!( + live, + vec![GameAction::DeclineShortcut], + "AI1(a): against a points-carrying bounded offer the ONLY legal candidate is the \ + decline — a `template: None` declaration is accepted and then discarded by \ + `handle_declare_shortcut`, which is worse than no candidate at all" + ); + + // ── arm (b): the POSITIVE CONTROL — the same board with an EMPTY point set ── + r28_empty_schema_offer(&mut runner); + let staged = engine::ai_support::legal_actions(runner.state()); + assert!( + staged.iter().any(|a| matches!( + a, + GameAction::DeclareShortcut { + count: IterationCount::Fixed(_), + template: None, + } + )), + "AI1(b) POSITIVE CONTROL: with `points` empty the generator MUST emit the \ + `Fixed(max_iterations)` candidate again. Its absence here would mean arm (a) measured \ + a generator that emits nothing rather than one keyed to the pin set. got {staged:?}" + ); + assert!( + staged.contains(&GameAction::DeclineShortcut), + "AI1(b): the decline stays legal on both arms — only the `Fixed` candidate moves, which \ + is what makes the pair one axis apart" + ); +} + +// ───── PR #7005 maintainer item: the answer-beat sampler records the SYNCHRONIZED window ───── + +/// CR 732.2a. `game::engine::apply_action`'s forced-window ANSWER sampler (the site gated on +/// `answering_forced_window`) called `record_loop_detect_sample` BEFORE installing the +/// pipeline's returned `wf`, while the settle sampler in `pass_priority_once_with_pipeline` +/// records AFTER its `sync_waiting_for`. A frame minted at the answer site therefore carried +/// the PRE-pipeline `waiting_for`/`priority_player` pair and a settle frame carried the synced +/// one. That is a detection hazard, not cosmetics: `impl PartialEq for GameState` compares both +/// fields and `normalize_for_loop` neutralizes neither, so a heterogeneous ring breaks +/// `analysis::resource::ring_delta_signature`'s turn-position conjunct. The fix routes `wf` +/// through `game::public_state::sync_waiting_for` — the canonical synchronizer, which also +/// recomputes `priority_player` via `turn_control::authorized_submitter_for_player` — before +/// the record, so both producers mint the same shape. +/// +/// FIXTURE: the tracked `dina_conqueror_4p` dump, driven through the production `apply()` path, +/// so every frame asserted below was minted by `record_loop_detect_sample` itself rather than +/// staged by the test. +/// +/// SITE ATTRIBUTION IS EXACT, not assumed. The answer site's own gate conjunct is +/// `state.waiting_for.is_forced_cascade_window()` read BEFORE the action; the settle sampler is +/// reachable only from `pass_priority_once_with_pipeline`, i.e. from a `Priority` window, which +/// `is_forced_cascade_window` deliberately excludes. So "the pre-beat window was forced AND the +/// ring grew" names the answer site and nothing else. MEASURED on this drive: 2 answer-beat +/// mints (beats 5 and 14), 3 settle mints, offer at beat 19 over a 5-frame ring. +/// +/// ⚠ WHAT THIS ROW DOES **NOT** CATCH, stated rather than implied. A PURE REVERT of the reorder +/// leaves all three arms GREEN, and that is a measurement rather than an oversight: a +/// `debug_assert_eq!` census on both fields at that position reported 0 divergences over 18,486 +/// lib + 4,487 integration rows, so no fixture in the corpus reaches the divergence. The row is +/// consequently the STANDING pin — it fires the first time a beat does diverge — and its +/// instrument is proved live by MUTANTS at the sampler instead of by the revert: +/// * `state.priority_player = PlayerId(3);` after the sync ⇒ arm (2) FAILS at the first mint. +/// * `state.waiting_for = WaitingFor::GameOver { winner: None };` after the sync ⇒ arm (1) +/// FAILS at the first mint (arm (2) still passes, so the two arms are separately live). +/// +/// Arm (3) is the BLAST-RADIUS pin: the certificate is byte-exact under the pure revert, which +/// is what makes "this reorder does not perturb detection" a measurement. +#[test] +fn answer_beat_frames_carry_the_synced_window_and_the_offer_certificate_is_exact() { + use engine::analysis::resource::{PeriodicDelta, ResourceVector}; + + let mut state = restore_dump(&gunzip_dump(include_bytes!( + "../fixtures/dina_conqueror_4p.json.gz" + ))); + + // ── REACH-GUARDS. Without these every assertion below is vacuous. + assert!( + state.loop_detection.samples(), + "reach-guard: a non-sampling mode never populates the ring, so neither a frame nor an \ + offer could exist; got {:?}", + state.loop_detection + ); + assert_eq!( + state.loop_detect_ring.len(), + 0, + "reach-guard: the dump ships with an EMPTY ring — every frame asserted below was \ + accumulated by THIS drive through the production producer, not restored from the dump" + ); + + let pin = engine_live_opponents(&state, P0).first().copied(); + let mut answer_mints = 0usize; + let mut settle_mints = 0usize; + let mut offer_beat = None; + for beat in 0..400usize { + if matches!( + state.waiting_for, + WaitingFor::LoopShortcut { + predicted_winner: None, + .. + } + ) { + offer_beat = Some(beat); + break; + } + let answered_forced_window = state.waiting_for.is_forced_cascade_window(); + let before = state.loop_detect_ring.len(); + if dump_drive_one_beat(&mut state, pin).is_err() { + break; + } + if state.loop_detect_ring.len() == before { + continue; + } + if !answered_forced_window { + settle_mints += 1; + continue; + } + answer_mints += 1; + let frame = &state + .loop_detect_ring + .back() + .expect("the ring just grew, so it has a back element") + .live; + // ── (2) ITS PRIORITY PLAYER. Asserted FIRST so a mutation that touches only + // `priority_player` is caught by its own arm instead of being masked by arm (1). + assert_eq!( + frame.priority_player, frame.active_player, + "beat {beat}: `sync_waiting_for` recomputes `priority_player` from the window it \ + installs, so an answer-beat frame must carry the post-sync submitter for the \ + returned `Priority{{active_player}}` window, not whatever the pre-pipeline window \ + left behind" + ); + // ── (1) THE NEWEST SAMPLED STATE: the window the action RETURNS, never the forced one + // it answered. + assert_eq!( + frame.waiting_for, + WaitingFor::Priority { + player: frame.active_player + }, + "beat {beat}: the sampler's own gate requires the RETURNED `wf` to be \ + `Priority{{active_player}}`, so recording before the sync is the only way the \ + frame can carry a different window — and `impl PartialEq for GameState` compares it" + ); + } + + assert!( + answer_mints > 0, + "reach-guard: the drive must mint at least one frame at the FORCED-WINDOW ANSWER site, \ + else arms (1)/(2) never ran and this row passes vacuously; got answer={answer_mints} \ + settle={settle_mints}" + ); + let offer_beat = offer_beat.expect( + "reach-guard: the bounded offer must FIRE on this real 4p drain, else arm (3) asserts \ + about a certificate that was never published", + ); + + // ── (3) THE RESULTING CERTIFICATE, EXACT. The destructure is EXHAUSTIVE on purpose: a new + // `LoopCertificate` field cannot slip past this pin unstated. + let (proposer, certificate, _schema) = bounded_offer_parts(&state); + assert_eq!( + proposer, P0, + "the offer beat {offer_beat} publishes the drain's controller as proposer" + ); + let LoopCertificate { + unbounded, + win_kind, + mandatory, + residual_board_delta, + per_cycle, + } = certificate; + assert_eq!( + *unbounded, + vec![ + ResourceAxis::Life(P0), + ResourceAxis::Life(P1), + ResourceAxis::Life(P2), + ResourceAxis::Life(P3), + ], + "CR 119.3: the Dina/Conqueror drain moves EVERY seat's life each period — the three \ + opponents down and the controller up — so all four axes are unbounded" + ); + assert_eq!( + *win_kind, + WinKind::LethalDamage, + "CR 704.5a: opponents reach 0 life" + ); + assert!( + !*mandatory, + "CR 732.2a: the interactive offer exists only for an OPTIONAL loop" + ); + assert_eq!( + *residual_board_delta, + BoardDelta::default(), + "CR 110.1: this cycle recycles its board exactly, so there is no non-recycled remainder" + ); + let Some(PeriodicDelta { + frames_per_period, + delta, + victim_slot, + }) = per_cycle + else { + panic!( + "the bounded producer is the one that NARROWS the CR 704 bound, so it publishes \ + a per-period signature; got None" + ) + }; + assert_eq!( + *frames_per_period, 2, + "one repetition spans two retained ring frames on this board — the gain-life \ + resolution and the lose-life one" + ); + assert!( + victim_slot.is_empty(), + "no decision slot is attributed a per-period life swing on this untargeted drain; \ + got {victim_slot:?}" + ); + let mut expected_delta = ResourceVector::default(); + expected_delta.life.insert(P0, 1); + expected_delta.life.insert(P1, -1); + expected_delta.life.insert(P2, -1); + expected_delta.life.insert(P3, -1); + assert_eq!( + *delta, expected_delta, + "EXACT per-period signature: +1 to the controller, -1 to each opponent, and every \ + other axis at rest. A ring whose frames disagreed on `waiting_for`/`priority_player` \ + could not produce this signature at all, because `ring_delta_signature` compares the \ + frames with `impl PartialEq for GameState`" + ); +}