CB-WP-0041 done: ADR-0020 refuses the port, and T02 is why
Some checks failed
ci / check (push) Failing after 3s
Some checks failed
ci / check (push) Failing after 3s
T02 — all chance derives from one root seed. Three chance points, all reading it: the setup deck shuffle, the setup Lead draw, and the reshuffle permutation. The Problems deal is not chance at all. So in extensive-form terms the tree has a single chance node at the root. That test was wrong first, and the mutation caught it. It compared state hashes — and GroundState carries `seed` as a field, so "different seeds differ" was true by construction. Mutating the shuffle away left it green. It now compares the dealt configuration, and the same mutation fails it: a wrong-subject error inside the control written for T02. The reshuffle is a pure function of (seed, round) because K5 requires deterministic replay, where a real table reshuffles independently. That is a modelling restriction, not a defect, and it is now pinned. T03 — commit/reveal checked in both directions: before Reveal each seat sees its own selection and no other; after Reveal the information sets merge, because an encoding that hides forever is not commit/reveal either. T04 — ADR-0020 refuses the EFG port, and the blocker is T02 rather than T01, which inverts what the workplan expected. Perfect recall looked like the risk and is a constraint with a known answer: key on observation histories. Making chance explicit is the expensive one — the reshuffle would become a real chance node and break the K5 purity that every recording, replay bundle and trial-note hash depends on. A port would trade the property this project is built on for one it has never needed. Track B's first move is therefore a question, not a build: take "is exploitability meaningful for a co-operative game with a shared threshold" to OpenSpiel on a toy model, where answering it costs nothing. D4 states what being wrong looks like — OpenSpiel settling on a toy what three rounds of policy sweeps could not — and makes watching for it the next action. Taxonomy §4.1 records the EFG correspondence with the test that checks each row, so a later pass starts from a specification rather than a memory. Chaos window 4 at three declarations. Window 3's verdict is now two windows behind and should be evaluated rather than restated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
parent
81f9339b2d
commit
2806b3acb7
5 changed files with 372 additions and 4 deletions
|
|
@ -2256,6 +2256,159 @@ mod tests {
|
|||
);
|
||||
}
|
||||
|
||||
/// **Commit/reveal IS the extensive-form encoding of simultaneous
|
||||
/// moves** (CB-WP-0041 T03), and this checks it rather than
|
||||
/// asserting it.
|
||||
///
|
||||
/// An EFG has no simultaneity: the textbook encoding sequences
|
||||
/// the moves and puts the later mover in an information set that
|
||||
/// cannot see the earlier one. GROUND's Select step does exactly
|
||||
/// that — seats choose in order, and no seat may see another's
|
||||
/// selection until Reveal.
|
||||
///
|
||||
/// **The property is load-bearing.** If a seat can see another's
|
||||
/// pending selection, the encoding is not simultaneous, the
|
||||
/// information partition is wrong, and every equilibrium concept
|
||||
/// computed on it answers a different game.
|
||||
#[test]
|
||||
fn a_pending_selection_is_hidden_until_reveal() {
|
||||
use cb_game_runtime::{Project, Viewer};
|
||||
|
||||
let mut s = setup(4, Variant::Baseline, 9);
|
||||
let seats: Vec<PlayerId> = s.players.keys().copied().collect();
|
||||
// Every seat commits.
|
||||
for seat in &seats {
|
||||
s.selections.insert(
|
||||
*seat,
|
||||
Selection {
|
||||
action: Action::Investigate,
|
||||
target: None,
|
||||
problem: s.problems.keys().next().copied(),
|
||||
},
|
||||
);
|
||||
}
|
||||
|
||||
// Before Reveal: a seat sees its own and nobody else's.
|
||||
s.step = RoundStep::Select;
|
||||
for viewer in &seats {
|
||||
let v = s.project(Viewer::Player(*viewer));
|
||||
for (seat, shown) in &v.selections {
|
||||
let visible = matches!(shown, crate::view::SelectionView::Shown(_));
|
||||
assert_eq!(
|
||||
visible,
|
||||
seat == viewer,
|
||||
"before Reveal, {viewer:?} could see {seat:?}'s selection — \
|
||||
the Select step is not simultaneous and the information \
|
||||
partition is wrong"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
// After Reveal: public, which is the other half of the
|
||||
// encoding — the information sets must MERGE, or the reveal
|
||||
// never happened.
|
||||
s.step = RoundStep::Reveal;
|
||||
for viewer in &seats {
|
||||
let v = s.project(Viewer::Player(*viewer));
|
||||
assert!(
|
||||
v.selections
|
||||
.values()
|
||||
.all(|x| matches!(x, crate::view::SelectionView::Shown(_))),
|
||||
"after Reveal, {viewer:?} still cannot see every selection"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// **All chance derives from the root seed** (CB-WP-0041 T02).
|
||||
///
|
||||
/// The claim T02 rests on, made checkable rather than asserted:
|
||||
/// a game is determined by `(seed, players, mode, variant)`, so
|
||||
/// in extensive-form terms the tree has **a single chance node at
|
||||
/// the root** rather than chance distributed through it.
|
||||
///
|
||||
/// Three chance points exist and all three read that seed:
|
||||
/// the setup deck shuffle, the setup Lead draw, and the mid-game
|
||||
/// reshuffle permutation (`seed ^ round`). The **Problems deal is
|
||||
/// not chance at all** — `edition::deal` is a pure function of the
|
||||
/// vendored CSV.
|
||||
#[test]
|
||||
fn a_game_is_determined_by_its_seed() {
|
||||
for players in [2u8, 3, 6] {
|
||||
// **The dealt configuration, NOT the state hash.**
|
||||
// `GroundState` carries `seed` as a field, so hashing the
|
||||
// state makes "different seeds differ" true by
|
||||
// construction — a wrong-subject error, caught by
|
||||
// mutating the shuffle away and watching this stay green.
|
||||
let at = |seed: u64| {
|
||||
let s = setup(players, Variant::Baseline, seed);
|
||||
let hands: Vec<Vec<Suit>> = s
|
||||
.players
|
||||
.values()
|
||||
.map(|p| p.hand.iter().map(|c| c.suit).collect())
|
||||
.collect();
|
||||
format!("{:?}|{:?}|{:?}", hands, s.lead, s.solution_deck)
|
||||
};
|
||||
// Same seed, same game — twice, because "deterministic"
|
||||
// that only holds once is not determinism.
|
||||
assert_eq!(at(11), at(11), "{players}p: setup is not reproducible");
|
||||
// And the full state still round-trips, which is the
|
||||
// replay property this rests on.
|
||||
assert_eq!(
|
||||
cb_events::state_hash_hex(&setup(players, Variant::Baseline, 11)),
|
||||
cb_events::state_hash_hex(&setup(players, Variant::Baseline, 11)),
|
||||
);
|
||||
// Different seeds must actually differ, or the seed is
|
||||
// not the chance node and this claim is empty.
|
||||
let distinct: std::collections::BTreeSet<String> = (0..12u64).map(at).collect();
|
||||
assert!(
|
||||
distinct.len() > 1,
|
||||
"{players}p: every seed produced the same game, so the root \
|
||||
chance node carries no information"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/// **The reshuffle is correlated with the root seed, and a real
|
||||
/// table's is not** (CB-WP-0041 T02).
|
||||
///
|
||||
/// `draw_solution` reshuffles the discard with
|
||||
/// `ChaChaRng::from_seed(seed ^ round)` — deliberate, so replay
|
||||
/// never re-derives it (GameKernel K5), and the comment says so.
|
||||
///
|
||||
/// **The consequence is a modelling one, not a defect.** At a
|
||||
/// table the reshuffle is an independent random event; here it is
|
||||
/// determined by the initial shuffle and the round number. An
|
||||
/// extensive-form game built from this engine inherits that
|
||||
/// correlation, and would be modelling a *restriction* of the
|
||||
/// game as played.
|
||||
#[test]
|
||||
fn the_reshuffle_permutation_is_a_function_of_seed_and_round() {
|
||||
let deck: Vec<SolutionCard> = [Suit::Clarify, Suit::Repair, Suit::Boundary]
|
||||
.into_iter()
|
||||
.flat_map(|suit| std::iter::repeat_n(SolutionCard { suit }, 3))
|
||||
.collect();
|
||||
let shuffled = |seed: u64, round: u8| {
|
||||
let mut order = deck.clone();
|
||||
let mut rng = ChaChaRng::from_seed(Seed(seed ^ u64::from(round)));
|
||||
rng.shuffle(&mut order);
|
||||
order
|
||||
};
|
||||
// Same seed and round: the same permutation, always.
|
||||
assert_eq!(shuffled(7, 2), shuffled(7, 2));
|
||||
// And it moves with BOTH inputs, or the correlation claim is
|
||||
// about something that does not vary.
|
||||
assert_ne!(
|
||||
shuffled(7, 2),
|
||||
shuffled(8, 2),
|
||||
"the reshuffle does not depend on the seed"
|
||||
);
|
||||
assert_ne!(
|
||||
shuffled(7, 2),
|
||||
shuffled(7, 3),
|
||||
"the reshuffle does not depend on the round"
|
||||
);
|
||||
}
|
||||
|
||||
/// **H1-A lands before the DARVO arm check** (review M5).
|
||||
///
|
||||
/// The delta orders it "+1 Stress, then clamp, then DARVO arm
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue