Some checks failed
ci / check (push) Failing after 4s
The answer is "it depends what you call an information set", and the distinction is the result. 44,938 decision points, random play, 2/3/4/6 seats. Reading A — information set = the seat's current projection, which is what project(Viewer::Player(seat)) returns and what the page renders: 22 violations. Reading B — information set = the seat's observation history, every view seen and action taken in order: 0. The Reading A witness is concrete. Two histories reach a byte-identical view — round 3, Select step, same hand, same claimed Problem — where the seat had played SOLVE then GROUND-OU(protect) in one and SUPPORT then SOLVE in the other. The view does not tell the seat what it did, because our state is a snapshot rather than a history: selections clear each round and effects coincide, so a player cannot reconstruct their own past from the present. In a real game the player's memory supplies it; in the state, nothing does. That is precisely OpenSpiel's ObservationString vs InformationStateString split, arrived at here by measurement rather than read off. project() is an observation, not an information state. So Track B is not closed, it is constrained, and usefully: an extensive-form game built from this engine must key information sets on observation histories, never on project(). Both directions are asserted — Reading B empty AND Reading A non-empty — because if the sample stops finding Reading A violations the conclusion is unsupported and must be re-derived rather than quietly kept. And the check samples, so it can falsify perfect recall and cannot establish it: Reading B's zero means no counterexample was drawn, which is printed as such. Wired into make panels, so it is re-derived by the gate rather than by hand. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
243 lines
9.8 KiB
Rust
243 lines
9.8 KiB
Rust
//! **Does this engine satisfy perfect recall?** (CB-WP-0041 T01)
|
|
//!
|
|
//! Perfect recall — every player remembers their own past actions and
|
|
//! observations — is the assumption **CFR and exploitability both rest
|
|
//! on** ([`CB-RES-0009`]). Nobody had checked whether ours holds.
|
|
//!
|
|
//! Formally: for a seat `i`, any two histories in the same information
|
|
//! set of `i` must agree on the sequence of `i`'s own past actions.
|
|
//!
|
|
//! **What this can and cannot say.** It samples histories and looks for a
|
|
//! pair that lands in the same information set with different own-action
|
|
//! prefixes. So:
|
|
//!
|
|
//! > **It can prove perfect recall FAILS. It cannot prove it holds.**
|
|
//!
|
|
//! A clean run means "no violation found in this sample", which is a
|
|
//! weaker statement than "the property holds" and is reported as such.
|
|
//! Saying otherwise would be an ACCOUNT failure over an INSTRUMENT that
|
|
//! cannot support it ([`Taxonomy.md`] §2.2).
|
|
//!
|
|
//! [`CB-RES-0009`]: ../../../research/CB-RES-0009-extensive-form-is-the-lingua-franca.md
|
|
//! [`Taxonomy.md`]: ../../../specs/Taxonomy.md
|
|
|
|
use std::cell::RefCell;
|
|
use std::collections::BTreeMap;
|
|
use std::rc::Rc;
|
|
|
|
use cb_game_runtime::{Project, ScenarioGame, Setup, Viewer};
|
|
use cb_kernel::PlayerId;
|
|
use games_ground::bot::{play, Choice, Policy, RandomPolicy};
|
|
use games_ground::{GroundCommand, GroundState};
|
|
|
|
/// One decision point: what the seat could see, and what it had done.
|
|
struct Observed {
|
|
/// **Reading A** — the information set taken to be the seat's
|
|
/// CURRENT projection, which is what `project(Viewer::Player(seat))`
|
|
/// returns and what the page renders.
|
|
observation: String,
|
|
/// **Reading B** — the information set taken to be the seat's whole
|
|
/// OBSERVATION HISTORY: every view it has seen and every action it
|
|
/// has taken, in order.
|
|
///
|
|
/// OpenSpiel draws exactly this distinction —
|
|
/// `ObservationString` versus `InformationStateString` — and the
|
|
/// second exists because the first does not give perfect recall.
|
|
info_state: String,
|
|
/// The seat's own past actions, in order — the thing perfect recall
|
|
/// says must be determined by the information set.
|
|
own_actions: Vec<String>,
|
|
}
|
|
|
|
/// Wraps a policy and records what each seat saw before it moved.
|
|
struct Recorder<P: Policy> {
|
|
inner: P,
|
|
log: Rc<RefCell<Vec<(PlayerId, Observed)>>>,
|
|
own: Rc<RefCell<BTreeMap<PlayerId, Vec<String>>>>,
|
|
hist: Rc<RefCell<BTreeMap<PlayerId, Vec<String>>>>,
|
|
}
|
|
|
|
impl<P: Policy> Policy for Recorder<P> {
|
|
fn name(&self) -> &'static str {
|
|
"recorder"
|
|
}
|
|
fn choose(
|
|
&mut self,
|
|
state: &GroundState,
|
|
seat: PlayerId,
|
|
legal: &[GroundCommand],
|
|
may_pass: bool,
|
|
) -> Choice {
|
|
// The information set is what this seat can see — nothing more.
|
|
let view = state.project(Viewer::Player(seat));
|
|
let observation = serde_json::to_string(&view).expect("view serialises");
|
|
let own_actions = self.own.borrow().get(&seat).cloned().unwrap_or_default();
|
|
// The observation history: what this seat has seen and done, in
|
|
// order, up to and including now.
|
|
let mut hist = self.hist.borrow_mut();
|
|
let h = hist.entry(seat).or_default();
|
|
h.push(observation.clone());
|
|
let info_state = h.join("\u{1e}");
|
|
drop(hist);
|
|
self.log.borrow_mut().push((
|
|
seat,
|
|
Observed {
|
|
observation,
|
|
info_state,
|
|
own_actions,
|
|
},
|
|
));
|
|
|
|
let choice = self.inner.choose(state, seat, legal, may_pass);
|
|
let taken = match &choice {
|
|
Choice::Command(i) => format!("{:?}", legal[*i]),
|
|
Choice::Pass => "pass".to_string(),
|
|
};
|
|
self.own
|
|
.borrow_mut()
|
|
.entry(seat)
|
|
.or_default()
|
|
.push(taken.clone());
|
|
// The action is part of what the seat remembers.
|
|
self.hist.borrow_mut().entry(seat).or_default().push(taken);
|
|
choice
|
|
}
|
|
}
|
|
|
|
fn main() {
|
|
// Random play, because the question is about the SHAPE of the
|
|
// information partition and a greedy policy visits a narrow slice of
|
|
// it. A policy that always makes the same choice cannot produce two
|
|
// histories in one information set with different prefixes.
|
|
let seeds = 0..400u64;
|
|
let mut points = 0usize;
|
|
let mut observation_violations: Vec<String> = Vec::new();
|
|
let mut info_state_violations: Vec<String> = Vec::new();
|
|
let mut witness: Option<(String, Vec<String>, Vec<String>)> = None;
|
|
|
|
for players in [2u8, 3, 4, 6] {
|
|
// Each reading maps its key to the own-action prefix first
|
|
// seen with it. A second, different prefix is a violation.
|
|
let mut by_observation: BTreeMap<String, Vec<String>> = BTreeMap::new();
|
|
let mut by_info_state: BTreeMap<String, Vec<String>> = BTreeMap::new();
|
|
|
|
for seed in seeds.clone() {
|
|
let Ok(st) = GroundState::setup(
|
|
&Setup {
|
|
players,
|
|
preset: format!("standard-{players}p"),
|
|
patch: Default::default(),
|
|
},
|
|
seed,
|
|
) else {
|
|
continue;
|
|
};
|
|
let log = Rc::new(RefCell::new(Vec::new()));
|
|
let own = Rc::new(RefCell::new(BTreeMap::new()));
|
|
let hist = Rc::new(RefCell::new(BTreeMap::new()));
|
|
let mut ps: Vec<Box<dyn Policy>> = (0..players)
|
|
.map(|i| {
|
|
Box::new(Recorder {
|
|
inner: RandomPolicy::new(seed ^ u64::from(i) ^ 0x9E37),
|
|
log: log.clone(),
|
|
own: own.clone(),
|
|
hist: hist.clone(),
|
|
}) as Box<dyn Policy>
|
|
})
|
|
.collect();
|
|
let Ok(_) = play(st, &mut ps) else { continue };
|
|
|
|
for (seat, obs) in log.borrow().iter() {
|
|
points += 1;
|
|
// The key includes WHO is looking: two seats with
|
|
// identical views are different information sets.
|
|
let a = format!("{seat:?}|{}", obs.observation);
|
|
match by_observation.get(&a) {
|
|
None => {
|
|
by_observation.insert(a, obs.own_actions.clone());
|
|
}
|
|
Some(prior) if *prior == obs.own_actions => {}
|
|
Some(prior) => {
|
|
if observation_violations.is_empty() {
|
|
witness = Some((
|
|
obs.observation.clone(),
|
|
prior.clone(),
|
|
obs.own_actions.clone(),
|
|
));
|
|
}
|
|
observation_violations.push(format!("{players}p seed {seed} {seat:?}"));
|
|
}
|
|
}
|
|
|
|
let b = format!("{seat:?}|{}", obs.info_state);
|
|
match by_info_state.get(&b) {
|
|
None => {
|
|
by_info_state.insert(b, obs.own_actions.clone());
|
|
}
|
|
Some(prior) if *prior == obs.own_actions => {}
|
|
Some(prior) => {
|
|
info_state_violations.push(format!(
|
|
"{players}p seed {seed} {seat:?}: {prior:?} vs {:?}",
|
|
obs.own_actions
|
|
));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
println!("perfect recall — CB-WP-0041 T01\n");
|
|
println!(" decision points sampled {points}\n");
|
|
println!(" Reading A — information set = the seat's CURRENT projection");
|
|
println!(
|
|
" violations {}",
|
|
observation_violations.len()
|
|
);
|
|
println!(" Reading B — information set = the seat's OBSERVATION HISTORY");
|
|
println!(
|
|
" violations {}\n",
|
|
info_state_violations.len()
|
|
);
|
|
|
|
if let Some((view, a, b)) = &witness {
|
|
println!(" Reading A witness — one view, two own-action prefixes:");
|
|
println!(" A: {a:?}");
|
|
println!(" B: {b:?}");
|
|
println!(" shared view: {}\n", &view[..view.len().min(220)]);
|
|
}
|
|
|
|
// **Reading B is the load-bearing claim.** If observation histories
|
|
// do not give perfect recall, no EFG can be built from this engine
|
|
// and Track B closes.
|
|
assert!(
|
|
info_state_violations.is_empty(),
|
|
"perfect recall FAILS even under observation histories: {} violation(s). \
|
|
No extensive-form game can be built from this engine, and every \
|
|
equilibrium concept is unsound here.\n{}",
|
|
info_state_violations.len(),
|
|
info_state_violations.first().cloned().unwrap_or_default()
|
|
);
|
|
|
|
// **Reading A failing is the FINDING, not an error.** It is why
|
|
// OpenSpiel separates ObservationString from InformationStateString.
|
|
assert!(
|
|
!observation_violations.is_empty(),
|
|
"Reading A found no violation. Either the sample is too small or the \
|
|
projection carries more history than it appears to — either way the \
|
|
conclusion below is unsupported and must be re-derived."
|
|
);
|
|
|
|
println!(" RESULT");
|
|
println!(" The current projection is an OBSERVATION, not an information");
|
|
println!(
|
|
" state: {} sampled pairs share a view while disagreeing about",
|
|
observation_violations.len()
|
|
);
|
|
println!(" what the seat itself had done. Perfect recall FAILS on that");
|
|
println!(" reading, and an EFG keyed on `project()` would be unsound.");
|
|
println!();
|
|
println!(" Keyed on the observation HISTORY, no violation was found.");
|
|
println!(" **That is not a proof** — this check can falsify perfect");
|
|
println!(" recall and cannot establish it. A clean run means no");
|
|
println!(" counterexample was drawn from this sample.");
|
|
}
|