Skip to content
131 changes: 111 additions & 20 deletions crates/engine/src/analysis/resource.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1880,22 +1880,15 @@ fn window_scope_from_cover_frames<'a>(
&& pb.extra_phases.is_empty())
.then_some(pa.phase);

// (s1) BOTH sequences non-empty β€” the `(Some, Some)` arm; (s2) one controller
// across BOTH sequences.
let sole_driver = match (
pa.last_loop_action_sequence.first(),
pb.last_loop_action_sequence.first(),
) {
(Some(first), Some(_)) => {
let driver = first.controller;
pa.last_loop_action_sequence
.iter()
.chain(pb.last_loop_action_sequence.iter())
.all(|ctx| ctx.controller == driver)
.then_some(driver)
}
_ => None,
};
// (s1) BOTH sequences non-empty; (s2) one controller across BOTH sequences. Both conjuncts
// are exactly [`GameState::loop_period_controller`] applied per frame β€” "whose period is
// this", the single authority every routing site reads β€” with the two answers required to
// agree. Stating it that way rather than re-deriving `first().controller` + `all()` here is
// the point of hoisting that authority: a two-frame twin of the same question cannot drift
// from the one-frame form it duplicates.
let sole_driver = pa
.loop_period_controller()
.filter(|driver| pb.loop_period_controller() == Some(*driver));

LoopWindowScope {
phase_invariant,
Expand Down Expand Up @@ -2360,7 +2353,25 @@ pub(crate) fn loop_states_cover_modulo_growth_pinned<'a>(
/// nothing". `Some(vec![])` would assert the latter and relieve EVERY conditioned
/// self-cost static β€” relief in the forbidden direction. `None` = scan everything.
/// Pinned by `empty_loop_action_sequence_proves_nothing_about_casting`.
fn window_cast_card_ids(state: &GameState) -> Option<Vec<CardId>> {
///
/// FAIL-CLOSED ON A FOREIGN PERIOD, for the same reason one level up (CR 732.2a). A recorded
/// period is evidence about the seat that recorded it and no one else, so when the caller names
/// a `proposer` only THAT seat's own period is proof of what this window casts. Otherwise an
/// opponent's choice of WHICH CARD TO ACTIVATE would select which soundness relief applies to
/// the proposer's certification β€” the same "relief in the forbidden direction" the emptiness
/// contract above rules out, arriving through a different door. This became reachable when the
/// bounded mint's step (1b) went seat-relative: before that, a bounded offer could not be minted
/// with any sequence present, so the question never arose.
///
/// `is_some_and`, NOT `is_some`: the proposer-less 2-arg entry
/// [`loop_states_cover_modulo_growth`] builds a `PeriodVerdicts::unproven` container used by the
/// object-growth detection covers in `analysis::loop_check`, which have no proposer to bind. When
/// the container names none, this is byte-identical to the pre-fix behaviour; requiring
/// `Some(proposer)` there would strip relief from that whole class.
fn window_cast_card_ids(state: &GameState, proposer: Option<PlayerId>) -> Option<Vec<CardId>> {
if proposer.is_some_and(|p| state.loop_period_controller() != Some(p)) {
return None;
}
let ids: Vec<CardId> = state
.last_loop_action_sequence
.iter()
Expand Down Expand Up @@ -2464,7 +2475,12 @@ pub(crate) fn loop_states_cover_modulo_growth_scoped<'a>(
// (5) Off-stack fail-closed fire-time condition guard (the second read surface).
// CR 601.2f: `cast_ids` is bound BEFORE `projected_scope` so NLL keeps the borrow
// live across the call (`LoopWindowScope::cast_card_ids` is `Option<&'a [CardId]>`).
let cast_ids = window_cast_card_ids(current);
//
// SITE E (CR 732.2a): the window's cast-set proof is scoped to the seat this container is
// bound to, so a period recorded by ANOTHER seat cannot select which relief applies here.
// `verdicts.proposer()` is `None` for the proposer-less 2-arg entry, where this stays
// byte-identical to the unscoped read.
let cast_ids = window_cast_card_ids(current, verdicts.proposer());
// All four fields written explicitly β€” no functional-update base, so there is no
// `LoopWindowScope<'static>` -> `LoopWindowScope<'_>` variance question to reason
// about, and a future FIFTH field is a compile error that forces a decision rather
Expand Down Expand Up @@ -11394,7 +11410,7 @@ mod tests {
let mut state = GameState::new_two_player(7);
assert!(state.last_loop_action_sequence.is_empty());
assert_eq!(
window_cast_card_ids(&state),
window_cast_card_ids(&state, None),
None,
"(1) an empty driving sequence is NO PROOF β€” `Some(vec![])` would assert \
`this window casts nothing` and relieve every conditioned self-cost static"
Expand All @@ -11413,12 +11429,87 @@ mod tests {
pins: Vec::new(),
}];
assert_eq!(
window_cast_card_ids(&state),
window_cast_card_ids(&state, None),
Some(vec![CardId(64)]),
"(2) a one-entry sequence yields exactly that card id"
);
}

/// X4-5 β€” [`window_cast_card_ids`]'s PROPOSER SCOPING (CR 732.2a), the sibling contract to
/// X4-4's emptiness one, called DIRECTLY for the same anti-domination reason.
///
/// A recorded period is evidence about the seat that recorded it. Once the bounded mint's
/// step (1b) went seat-relative, a certification could be taken with a FOREIGN period sitting
/// in state β€” and an unscoped read would then let an OPPONENT'S choice of which card to
/// activate decide which conditioned self-cost static gets relieved for THIS proposer.
///
/// THREE-WAY AND EACH ARM IS LOAD-BEARING, so no constant implementation passes:
/// * `None` (the proposer-less 2-arg entry) β‡’ unscoped, byte-identical to pre-fix. Dropping
/// the `Option` guard β€” the UNCONDITIONAL-MATCH form `if state.loop_period_controller() !=
/// proposer { return None; }` β€” refuses the unbound container and FAILS (1); this is the arm
/// that protects `loop_check`'s object-growth detection covers. (MEASURED, and it corrects
/// this row's own earlier claim: the `is_some`-instead-of-`is_some_and` swap does NOT fail
/// (1) β€” with `proposer == None` it never returns early β€” it fails (2), by refusing the
/// seat that DID record the period.)
/// * `Some(owner)` β‡’ proof. An always-`None` implementation FAILS (2), as does the `is_some`
/// swap above.
/// * `Some(other)` β‡’ no proof. The pre-fix unscoped implementation FAILS (3).
///
/// (4) pins the fail-closed homogeneity clause: a two-seat run is nobody's period, so it is
/// proof for NEITHER seat β€” an implementation testing only `seq[0].controller` FAILS it.
#[test]
fn a_foreign_driving_period_proves_nothing_about_this_proposers_casting() {
use crate::types::game_state::{BuybackUsage, LoopAction, LoopActionContext};

let owner = PlayerId(0);
let other = PlayerId(1);
let step = |controller: PlayerId, card_id: CardId| LoopActionContext {
card_id,
controller,
action: LoopAction::Recast {
from_zone: Zone::Hand,
uses_buyback: BuybackUsage::Used,
},
convoke: None,
pins: Vec::new(),
};

let mut state = GameState::new_two_player(7);
state.last_loop_action_sequence = vec![step(owner, CardId(64))];

assert_eq!(
window_cast_card_ids(&state, None),
Some(vec![CardId(64)]),
"(1) an UNBOUND container (the proposer-less 2-arg entry `loop_check` uses) reads \
the period unscoped β€” `is_some_and`, not `is_some`, or the object-growth detection \
covers lose their relief"
);
assert_eq!(
window_cast_card_ids(&state, Some(owner)),
Some(vec![CardId(64)]),
"(2) the seat that RECORDED the period is proved by it"
);
assert_eq!(
window_cast_card_ids(&state, Some(other)),
None,
"(3) CR 732.2a: another seat's independent activation describes no sequence THIS \
proposer takes, so it is no proof about this window's cast set β€” relieving on it \
would hand an opponent the choice of which soundness relief applies"
);

// (4) the fail-closed homogeneity clause: nobody's period.
state.last_loop_action_sequence = vec![step(owner, CardId(64)), step(other, CardId(90))];
assert_eq!(
(
window_cast_card_ids(&state, Some(owner)),
window_cast_card_ids(&state, Some(other)),
),
(None, None),
"(4) a heterogeneous run belongs to no seat, so it proves nothing for EITHER β€” \
reading only `seq[0].controller` would wrongly prove it for the first"
);
}

/// X4-3 β€” the REAL 4-player Dina/Conqueror capture (`dina_conqueror_4p.json.gz`),
/// loaded through the production restore chokepoint
/// `PersistedGameState::into_game_state`. It carries dump-D obj 90 **Mortality
Expand Down
Loading
Loading