CB-WP-0006 T05: K9's assertion, K11's format, and the AM-11 suites
K11 is implemented: crates/cb-events/src/store.rs, magic + version header, 4-byte little-endian length prefix, append-only. Reimplemented not assimilated per ADR-0005 §2 — no new dependency, and AM-4a/AM-4b are unchanged at 246,250 / 317,021 because nothing entered the graph. The operative clause is "detected", so corruption is tested rather than assumed: a tail short by one byte, a half-written length prefix, a length prefix corrupted to claim more than the file holds, foreign magic, and a future format version are each rejected with a distinct error. A reader that accepts a truncated tail is worse than no format, because it silently returns a short history that looks complete. AM-11 is earned. LogStore has two impls — MemLogStore and FileLogStore — driven through ONE conformance(). The trait carries raw/set_raw precisely so the corruption controls live in the shared suite: a format contract that only one impl enforces is not a contract. The same shape is retro-fitted to KernelRng, which is what AM-11 actually names: ChaChaRng and NullRng now pass one suite asserting bounds, draw(1) == 0, determinism across fresh instances, and shuffle preserving the multiset. They were previously exercised by two separate tests, which is why "met, narrow" was never earned and ADR-0005 §4 downgraded it. K9 gets the assertion it did not have: snapshot at seq N + events N+1..M must equal the from-genesis fold, hash-compared, on GroundState, single-seed on purpose — AM-7's probe folds a multi-seed log, which is not a replay of anything, and that defect is not repeated. Two positive controls: the log must exceed 50 events, and the mid-log snapshot must differ from the end state or "apply the remainder" is vacuous. Proof it works: the exact mutation that SURVIVED in CB-WP-0005 — making Snapshot::take discard its EventSeq — now fails on the K9 assertion. AM-11's mutation breaks NullRng::draw to return its bound and the shared suite fails. That is what M-D4-SWAP claims — either impl substitutable — and exactly what two separate per-impl tests could never demonstrate. M-D1-MUT: 7 -> 8 of 14. CB-EV-0001's scoreboard is refreshed: AM-2, AM-5 and AM-9 added, AM-6 moved to enforced, and the headline total corrected from 4 to 8 — it had gone stale inside the same workplan that produced it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
parent
5f7d9015d9
commit
98c6cd24c3
12 changed files with 638 additions and 19 deletions
|
|
@ -2163,8 +2163,9 @@ mod bench_shape {
|
|||
#[cfg(test)]
|
||||
mod replay_probe {
|
||||
use super::*;
|
||||
use cb_events::state_hash_hex;
|
||||
use cb_events::{state_hash_hex, Snapshot};
|
||||
use cb_game_runtime::{ScenarioGame, Setup};
|
||||
use cb_kernel::EventSeq;
|
||||
use std::time::Instant;
|
||||
|
||||
fn fresh(seed: u64) -> GroundState {
|
||||
|
|
@ -2219,6 +2220,81 @@ mod replay_probe {
|
|||
n
|
||||
}
|
||||
|
||||
/// K9: `snapshot + remaining events -> state` must be hash-identical to
|
||||
/// a from-genesis fold.
|
||||
///
|
||||
/// **This is the assertion K9 did not have.** Its entire evidence was
|
||||
/// one test round-tripping a `BTreeMap<String, u8>` with `EventSeq(17)`
|
||||
/// as a literal — no game aggregate, no events applied, no
|
||||
/// from-genesis comparison. CB-WP-0005 proved it inert by mutation:
|
||||
/// making `Snapshot::take` discard its `EventSeq` and store 0 left the
|
||||
/// test green, so the half of K9 that says "**+ the EventId it
|
||||
/// includes**" was unverified.
|
||||
///
|
||||
/// Single-seed on purpose. AM-7's probe folds a log built across games
|
||||
/// seeded 42, 43, 44... into a state from `fresh(42)`, which is not a
|
||||
/// replay of anything; that defect is not repeated here.
|
||||
#[test]
|
||||
fn k9_snapshot_plus_remaining_events_equals_genesis_fold() {
|
||||
let mut source = fresh(42);
|
||||
let mut log = Vec::new();
|
||||
while log.len() < 400 && source.outcome.is_none() {
|
||||
if record_round(&mut source, &mut log) == 0 {
|
||||
break;
|
||||
}
|
||||
}
|
||||
// Positive control: a trivial log would make the comparison pass
|
||||
// for the wrong reason.
|
||||
assert!(
|
||||
log.len() >= 50,
|
||||
"K9 needs a non-trivial single-game log, got {} events",
|
||||
log.len()
|
||||
);
|
||||
|
||||
let mut genesis = fresh(42);
|
||||
for e in &log {
|
||||
genesis.fold(e);
|
||||
}
|
||||
let genesis_hash = state_hash_hex(&genesis);
|
||||
|
||||
let n = log.len() / 2;
|
||||
let mut mid = fresh(42);
|
||||
for e in &log[..n] {
|
||||
mid.fold(e);
|
||||
}
|
||||
let snap = Snapshot::take(&mid, EventSeq(n as u64));
|
||||
|
||||
// The clause the mutation exposed: a snapshot is the aggregate
|
||||
// **plus the EventId it includes**. Without this, `take` could
|
||||
// discard `through` entirely and nothing would notice.
|
||||
assert_eq!(
|
||||
snap.through,
|
||||
EventSeq(n as u64),
|
||||
"K9: the snapshot must carry the EventSeq it includes"
|
||||
);
|
||||
|
||||
let mut restored: GroundState = snap.restore().unwrap();
|
||||
// And the snapshot must not already equal the end state, or
|
||||
// "apply the remainder" would be vacuous.
|
||||
assert_ne!(
|
||||
state_hash_hex(&restored),
|
||||
genesis_hash,
|
||||
"K9: the mid-log snapshot must differ from the end state"
|
||||
);
|
||||
for e in &log[n..] {
|
||||
restored.fold(e);
|
||||
}
|
||||
|
||||
assert_eq!(
|
||||
state_hash_hex(&restored),
|
||||
genesis_hash,
|
||||
"K9 UNMET: snapshot at seq {n} + {} remaining events did not \
|
||||
reproduce the from-genesis fold over {} events",
|
||||
log.len() - n,
|
||||
log.len()
|
||||
);
|
||||
}
|
||||
|
||||
/// AM-6 target from GameKernel §5, in applied events per second.
|
||||
///
|
||||
/// **Pinned, not tuned.** CB-WP-0006 T01 named the trap up front: a
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue