Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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