Surfaced while proving the occurrence-exactness invariant of
filter_already_collected_trigger_events_from (crates/engine/src/game/triggers.rs).
Escalated rather than fixed: the follow-up to #7058 is chartered test-and-doc, and
closing this would land production code in turns.rs. Anchors are at
84a4d01e63fd712936e58c9ab4e6834dc66e9e19.
The structural claim
The queued-context witness in filter_already_collected_trigger_events_from
compares slice events against state.deferred_triggers using full GameEvent
equality. The field that makes two distinct zone-change occurrences of one object
compare unequal is ZoneChangeRecord::turn_zone_change_index, allocated by
restrictions::record_zone_change (restrictions.rs:606-621) as
state.zone_changes_this_turn.len().
That index is per-turn. start_next_turn (turns.rs:1007) clears
zone_changes_this_turn at turns.rs:1253 (CR 514.2 cleanup), so indices restart at
0 every turn. It does not clear state.deferred_triggers: the only two
deferred_triggers references in turns.rs are a doc comment (:2610) and a
read-only guard (:2946), both outside start_next_turn's body.
The queue is bounded only by:
- drain-at-priority (
triggers.rs:7704, :8224, :8747);
- the CR 724 "end the turn" / "end the combat phase" effects
(effects/end_phase.rs:34, reached from effects/end_the_turn.rs:20 and
effects/end_combat_phase.rs:34) — not the ordinary cleanup step;
- elimination (
elimination.rs:150, :380, :405).
It is not bounded by the turn boundary. So a witness queued in turn N can in
principle alias a reset index in turn N+1, and the filter would then consume an
occurrence its witness does not name.
Why it is not simply "very unlikely"
For most families the two incarnation-bearing fields
(ZoneChangeRecord::entered_incarnation and
trigger_source_context.identity.reference.incarnation) would also have to coincide,
which makes cross-turn aliasing implausible. For the within-Library reposition
family that requirement is vacuous: entered_incarnation is None on both (not a
battlefield destination) and the incarnation is deliberately never bumped
(zones.rs:1809-1812, CR 400.7 / CR 701.20b — a within-zone reposition is zero
moves). For that family R1 reduces to index aliasing across a turn boundary alone.
Precedent already in the same file
turns.rs:1256-1262 already calls out exactly this cross-turn aliasing hazard for
pending_token_battlefield_entry and defends it. It does not defend
deferred_triggers.
Explicit non-remedy — do not re-propose without new evidence
A debug_assert!(state.deferred_triggers.is_empty()) in start_next_turn was
considered and affirmatively rejected, for three reasons:
- It asserts a non-invariant. Per the bounds above, a non-empty
deferred_triggers at a turn boundary is legal engine state. An assertion that
fires on legal states is a false tripwire, not a guard.
- Shipped code in the same file contradicts it.
turns.rs:2946 reads
if !state.deferred_triggers.is_empty() || state.pending_trigger.is_some() { —
a read-only guard that exists precisely because the queue can be non-empty in the
turn machinery.
- It is a production assertion on a turn-boundary hot path.
Whoever picks this up should not re-propose the assertion without new evidence that
the queue is bounded by the turn boundary.
Status
Reachability is unquantified. Structurally possible; not demonstrated. No live
misbehaviour is claimed. Recorded so the bound is tracked rather than assumed.
The invariant this residual bounds is documented in the doc contract on
filter_already_collected_trigger_events_from (scoped explicitly to live play).
Surfaced while proving the occurrence-exactness invariant of
filter_already_collected_trigger_events_from(crates/engine/src/game/triggers.rs).Escalated rather than fixed: the follow-up to #7058 is chartered test-and-doc, and
closing this would land production code in
turns.rs. Anchors are at84a4d01e63fd712936e58c9ab4e6834dc66e9e19.The structural claim
The queued-context witness in
filter_already_collected_trigger_events_fromcompares slice events against
state.deferred_triggersusing fullGameEventequality. The field that makes two distinct zone-change occurrences of one object
compare unequal is
ZoneChangeRecord::turn_zone_change_index, allocated byrestrictions::record_zone_change(restrictions.rs:606-621) asstate.zone_changes_this_turn.len().That index is per-turn.
start_next_turn(turns.rs:1007) clearszone_changes_this_turnatturns.rs:1253(CR 514.2 cleanup), so indices restart at0every turn. It does not clearstate.deferred_triggers: the only twodeferred_triggersreferences inturns.rsare a doc comment (:2610) and aread-only guard (
:2946), both outsidestart_next_turn's body.The queue is bounded only by:
triggers.rs:7704,:8224,:8747);(
effects/end_phase.rs:34, reached fromeffects/end_the_turn.rs:20andeffects/end_combat_phase.rs:34) — not the ordinary cleanup step;elimination.rs:150,:380,:405).It is not bounded by the turn boundary. So a witness queued in turn N can in
principle alias a reset index in turn N+1, and the filter would then consume an
occurrence its witness does not name.
Why it is not simply "very unlikely"
For most families the two incarnation-bearing fields
(
ZoneChangeRecord::entered_incarnationandtrigger_source_context.identity.reference.incarnation) would also have to coincide,which makes cross-turn aliasing implausible. For the within-Library reposition
family that requirement is vacuous:
entered_incarnationisNoneon both (not abattlefield destination) and the incarnation is deliberately never bumped
(
zones.rs:1809-1812, CR 400.7 / CR 701.20b — a within-zone reposition is zeromoves). For that family R1 reduces to index aliasing across a turn boundary alone.
Precedent already in the same file
turns.rs:1256-1262already calls out exactly this cross-turn aliasing hazard forpending_token_battlefield_entryand defends it. It does not defenddeferred_triggers.Explicit non-remedy — do not re-propose without new evidence
A
debug_assert!(state.deferred_triggers.is_empty())instart_next_turnwasconsidered and affirmatively rejected, for three reasons:
deferred_triggersat a turn boundary is legal engine state. An assertion thatfires on legal states is a false tripwire, not a guard.
turns.rs:2946readsif !state.deferred_triggers.is_empty() || state.pending_trigger.is_some() {—a read-only guard that exists precisely because the queue can be non-empty in the
turn machinery.
Whoever picks this up should not re-propose the assertion without new evidence that
the queue is bounded by the turn boundary.
Status
Reachability is unquantified. Structurally possible; not demonstrated. No live
misbehaviour is claimed. Recorded so the bound is tracked rather than assumed.
The invariant this residual bounds is documented in the doc contract on
filter_already_collected_trigger_events_from(scoped explicitly to live play).