coulomb/clay-borg
4
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

CB-WP-0006 T07: implement K18, amend K14

Browse source 
Two rules, two different answers, which is the point of a task phrased
"implement, or amend and say why".

K18 is implemented. "Criterion benches driving the same scenario format at
scale" was false — the bench hardcoded its commands and never touched
ScenarioFile, while MetricsAndScenarios §3 pointed at a benchmarks/
directory containing only baselines/. benchmarks/synthetic-3p.yaml now
holds the workload and both the bench and bench_shape read it: the
workload is data, not code.

A second defect surfaced while fixing the first. After the bench switched
to the file, bench_shape still hardcoded the same sequence, so the
workload existed twice — deleting end_round from the YAML broke bench-test
while bench_shape kept passing. Duplicated-fact drift in executable form.
Both now read the same include_str! and deleting a command breaks both.

Explicitly not claimed: this does not unblock AM-3. AM-3's baseline is a
declarative game object — moves, turn order, rules. synthetic-3p.yaml is a
command list; the rules live in games/ground. Marking it as AM-3's subject
would compare a script to a game definition, which is the category error
AM-3 is blocked on. The file says so in its own header, where the next
person will be tempted.

K14 is amended. CommitWindow had zero non-test users and GROUND enforces
the same contract inline. Wiring GROUND through it was rejected: it would
change the serialized shape of `selections`, which four scenario files
assert by dot-path and every state hash depends on, for the sole benefit
of making a sentence literally true.

The deciding argument is INTENT's, not convenience: abstractions are
extracted from working games rather than invented in isolation, and no
concept becomes canonical until it survives a second concrete use.
CommitWindow was invented before any game needed it and has survived none.
Imposing it on GROUND would manufacture the first use rather than discover
it. So K14 states what is actually guaranteed, CommitWindow is marked
provisional in the source, and it carries a delete-by date of 2026-12-31.

Kernel spec->code link 16/18 -> 18/18, stated with the caveat the gate
prints every run: that is about names, not assertions.

Two self-tests broke and both broke correctly. rule-coverage's gate test
hardcoded "unlinked rules exist today" and failed when the last one was
linked; it now computes that and asserts the gate fails iff rules are
unlinked. facts' text check rejected k_unlinked once it became
legitimately empty; empty now renders as "(none)" and the check
distinguishes absent from empty.

M-D1-MUT: 8 of 14, unchanged — K14 and K18 are kernel rules, not
acceptance rows.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
tegwick 2026-08-01 12:47:16 +02:00
parent 4e82a520b3
commit 327bda64ab
11 changed files with 256 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

46
benchmarks/synthetic-3p.yaml Normal file
View file

@ -0,0 +1,46 @@
# K18: the benchmark workload, expressed in the scenario format.
#
# Until CB-WP-0006 T07 the bench hardcoded this command sequence in Rust
# and never touched `ScenarioFile`, so K18 — "Criterion benches driving
# the same scenario format at scale" — was false, and
# MetricsAndScenarios §3's "benchmarks live in benchmarks/" pointed at a
# directory containing only `baselines/`.
#
# Mirrors the CB-RES-0001 harness shape: 3 players, commit/reveal round.
# The bench replays these commands per round at scale; `bench_shape` in
# the aggregate crate pins the resulting 7 commands / 13 events, so a
# change here that alters the shape breaks a test rather than silently
# rescaling AM-6 and AM-7.
#
# NOT an AM-3 subject. AM-3's baseline is a declarative *game object*
# (~36 LOC, boardgame.io) — moves, turn order, rules. This is a command
# list; the rules live in games/ground (1,575 lines). Marking this file
# as AM-3 would compare a script to a game definition, which is the
# category error AM-3 is currently blocked on.
scenario: ground/bench-synthetic-3p
description: One 3-player GROUND round, replayed at scale by the Criterion bench.
covers: []
seed: 42
setup:
players: 3
preset: standard-3p
commands:
- actor: P1
cmd: select_action
args: { action: ATTACK, target: P2 }
- actor: P3
cmd: select_action
args: { action: SUPPORT, target: P2 }
- actor: P2
cmd: select_action
args: { action: GROUND }
- actor: SYSTEM
cmd: reveal
- actor: P2
cmd: choose_ground_mode
args: { mode: GR }
- actor: SYSTEM
cmd: resolve
- actor: SYSTEM
cmd: end_round
expect: {}

11
crates/cb-game-runtime/src/lib.rs
View file

@ -18,6 +18,17 @@ use std::collections::BTreeMap;
/// A simultaneous commit window (GameKernel K12): the runtime opens it
/// naming who must submit; submissions are commitment events hidden from
/// projections until reveal.
///
/// **PROVISIONAL — zero non-test users as of 2026-08-01 (K14, GameKernel
/// §2.5a).** GROUND implements the same contract inline in its own
/// aggregate. This type is the *extracted* form, kept because it
/// documents the seam stage 3 and stage 4 will need — but INTENT says a
/// concept becomes canonical only *"after surviving a second concrete
/// use"*, and this has survived none.
///
/// **Delete it if no second game uses it by 2026-12-31.** A primitive
/// with one hypothetical user and a test that exercises only itself is
/// the AM-11 shape, and this project has paid for that shape twice.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CommitWindow<C> {
/// Players who must submit, and their commitment once received.

8
facts.toml
View file

@ -70,8 +70,8 @@ fmt = "{:,}"
by = "tools/rule-coverage.py"
[k_linked]
value = 16
text = "16"
value = 18
text = "18"
fmt = "{:,}"
by = "tools/rule-coverage.py"
@ -82,8 +82,8 @@ fmt = "{:,}"
by = "tools/rule-coverage.py"
[k_unlinked]
value = 'K14 K18'
text = "K14 K18"
value = '(none)'
text = "(none)"
fmt = "{}"
by = "tools/rule-coverage.py"

84
games/ground/benches/synthetic.rs
View file

@ -9,7 +9,7 @@
//! what matters is the shape of the curve, not only the peak number.
use cb_events::state_hash_hex;
use cb_game_runtime::{ScenarioGame, Setup};
use cb_game_runtime::{ScenarioFile, ScenarioGame, Setup};
use cb_kernel::{Actor, Aggregate, PlayerId};
use criterion::{criterion_group, criterion_main, BatchSize, Criterion, Throughput};
use games_ground::{Action, GroundCommand, GroundMode, GroundState};
@ -39,66 +39,50 @@ fn apply(state: &mut GroundState, actor: Actor, command: &GroundCommand) -> usiz
}
}
/// One full round for three players: three Selects, Reveal, the GROUND
/// mode choice, Resolve, End. Returns the number of events applied.
fn play_round(state: &mut GroundState) -> usize {
let picks = [
(
PlayerId(0),
GroundCommand::SelectAction {
action: Action::Attack,
target: Some(PlayerId(1)),
problem: None,
},
),
(
PlayerId(2),
GroundCommand::SelectAction {
action: Action::Support,
target: Some(PlayerId(1)),
problem: None,
},
),
(
PlayerId(1),
GroundCommand::SelectAction {
action: Action::Ground,
target: None,
problem: None,
},
),
];
/// K18: the benchmark workload, **loaded from the scenario format**.
///
/// Until CB-WP-0006 T07 this function hardcoded the command sequence in
/// Rust and never touched `ScenarioFile`, so K18 — "Criterion benches
/// driving the same scenario format at scale" — was false. Embedding the
/// file at compile time keeps the bench self-contained while making the
/// workload *data*: editing `benchmarks/synthetic-3p.yaml` changes what
/// AM-6 and AM-7 measure, and `bench_shape` in the aggregate crate breaks
/// if that changes the round's shape.
const WORKLOAD_YAML: &str = include_str!("../../../benchmarks/synthetic-3p.yaml");
let mut applied = 0;
for (seat, command) in picks {
applied += apply(state, Actor::Player(seat), &command);
}
applied += apply(state, Actor::System, &GroundCommand::Reveal);
// GR-R05: the GROUND player picks a mode before resolution.
applied += apply(
state,
Actor::Player(PlayerId(1)),
&GroundCommand::ChooseGroundMode {
mode: GroundMode::Gr,
choice: None,
},
fn workload() -> Vec<(Actor, GroundCommand)> {
let sc = ScenarioFile::from_yaml(WORKLOAD_YAML).expect("bench workload parses");
// Positive control: an empty or mis-parsed workload would benchmark
// nothing while still reporting a rate.
assert!(
!sc.commands.is_empty(),
"K18: the bench workload has no commands"
);
applied += apply(state, Actor::System, &GroundCommand::Resolve);
applied += apply(state, Actor::System, &GroundCommand::EndRound);
sc.commands
.iter()
.map(|step| GroundState::parse_command(step).expect("bench command parses"))
.collect()
}
/// One full round for three players, replayed from the scenario workload.
/// Returns the number of events applied.
fn play_round(state: &mut GroundState, round: &[(Actor, GroundCommand)]) -> usize {
let mut applied = 0;
for (actor, command) in round {
applied += apply(state, *actor, command);
}
applied
}
/// A game ends after Round 5 (GR-R09), so a long run starts a fresh game
/// rather than idling on a finished one. Setup cost is therefore part of
/// the measurement, at one setup per five rounds.
fn run_rounds(rounds: usize) -> usize {
let mut applied = 0;
let mut state = setup(42);
let script = workload();
for round in 0..rounds {
if state.outcome.is_some() {
state = setup(42 + round as u64);
}
let produced = play_round(&mut state);
let produced = play_round(&mut state, &script);
// A workload whose commands get rejected still "runs", but it
// measures nothing. An earlier version of this bench stalled on
// the GR-R03 stress gate and reported throughput for rounds that
@ -163,7 +147,7 @@ fn record_round(state: &mut GroundState, log: &mut Vec<games_ground::GroundEvent
fn bench_synthetic(c: &mut Criterion) {
// Events per round is fixed by the workload, so throughput can be
// reported in events/second — the AM-6 unit.
assert_eq!(play_round(&mut setup(1)), EVENTS_PER_ROUND);
assert_eq!(play_round(&mut setup(1), &workload()), EVENTS_PER_ROUND);
let mut group = c.benchmark_group("synthetic-ground-3p");
// AM-6 headline throughput and AM-7 scaling, at the sizes the

51
games/ground/src/lib.rs
View file

@ -2099,61 +2099,34 @@ mod tests {
#[cfg(test)]
mod bench_shape {
use super::*;
use cb_game_runtime::{ScenarioGame, Setup};
use cb_game_runtime::{ScenarioFile, ScenarioGame};
/// AM-6 reports events/second; the evidence file converts that to
/// rounds and commands per second. Both divisors are pinned here so
/// a change to the workload cannot silently rescale the metric.
#[test]
fn synthetic_round_shape_is_pinned() {
let mut state = GroundState::setup(
&Setup {
players: 3,
preset: "standard-3p".into(),
patch: BTreeMap::new(),
},
1,
)
.unwrap();
// K18 / single source of fact (InnerLoop v1.3): the workload is
// read from the SAME file the Criterion bench replays. It used to
// be hardcoded here as well, so the round existed twice and the
// two copies could drift — editing the YAML broke `bench-test`
// while this test kept passing.
let yaml = include_str!("../../../benchmarks/synthetic-3p.yaml");
let sc = ScenarioFile::from_yaml(yaml).expect("bench workload parses");
let mut state = GroundState::setup(&sc.setup, sc.seed).unwrap();
let mut events = 0;
let mut commands = 0;
let mut run = |state: &mut GroundState, actor: Actor, cmd: &GroundCommand| {
for step in &sc.commands {
let (actor, cmd) = GroundState::parse_command(step).expect("workload command");
commands += 1;
if let Ok(produced) = state.validate(actor, cmd) {
if let Ok(produced) = state.validate(actor, &cmd) {
for e in &produced {
state.fold(e);
}
events += produced.len();
}
};
for (seat, action, target) in [
(0u8, Action::Attack, Some(PlayerId(1))),
(2, Action::Support, Some(PlayerId(1))),
(1, Action::Ground, None),
] {
run(
&mut state,
Actor::Player(PlayerId(seat)),
&GroundCommand::SelectAction {
action,
target,
problem: None,
},
);
}
run(&mut state, Actor::System, &GroundCommand::Reveal);
run(
&mut state,
Actor::Player(PlayerId(1)),
&GroundCommand::ChooseGroundMode {
mode: GroundMode::Gr,
choice: None,
},
);
run(&mut state, Actor::System, &GroundCommand::Resolve);
run(&mut state, Actor::System, &GroundCommand::EndRound);
assert_eq!(commands, 7, "commands per synthetic round");
assert_eq!(events, 13, "events per synthetic round");

77
history/260801-cb-wp-0006-log.md
View file

@ -334,3 +334,80 @@ immediately caught the spec's copy of that number going stale — the DFD
gate earning its place on a number that moved the same hour.
**M-D1-MUT: 8 of 14** (unchanged; AM-7 remains partial).
## CB-WP-0006-T07
**Two rules, two different answers — which is the point of a task phrased
"implement, or amend and say why".**
### K18: implemented
"Criterion benches driving the same scenario format at scale" was false —
the bench hardcoded its command sequence in Rust and never touched
`ScenarioFile`, while MetricsAndScenarios §3 pointed at a `benchmarks/`
directory containing only `baselines/`.
`benchmarks/synthetic-3p.yaml` now holds the workload, and both the bench
and `bench_shape` read it. **The workload is data, not code.**
**A second defect surfaced while fixing the first.** After the bench
switched to the file, `bench_shape` still hardcoded the same sequence — so
the workload existed **twice**, and deleting `end_round` from the YAML
broke `bench-test` while `bench_shape` kept passing. That is
duplicated-fact drift in executable form. Both now read the same
`include_str!`, and deleting a command breaks both:
```text
assertion `left == right` failed: commands per synthetic round
```
**Explicitly not claimed:** this does *not* unblock AM-3. AM-3's baseline
is a declarative **game object** (~36 LOC, boardgame.io) — moves, turn
order, rules. `synthetic-3p.yaml` is a command list; the rules live in
`games/ground` (1,575 lines). Marking it as AM-3's subject would compare a
script to a game definition, which is the category error AM-3 is blocked
on. The file says so in its own header, where the next person will be
tempted.
### K14: amended, and the reasoning is recorded because it could have gone
the other way
`CommitWindow` had **zero non-test users**; GROUND enforces the same
contract inline. Wiring GROUND through it was rejected: it would change
the serialized shape of `selections`, which four scenario files assert by
dot-path and every state hash depends on — a large, risky refactor whose
only benefit is making a sentence literally true.
The deciding argument is INTENT's, not convenience: *"abstractions are
extracted from working games... rather than invented in isolation"*, and
*"No concept becomes canonical merely because it looks general. It becomes
canonical after surviving a second concrete use."* `CommitWindow` was
invented before any game needed it and has survived **zero** uses.
Imposing it on GROUND would **manufacture** the first use rather than
discover it.
So K14 now states what is actually guaranteed, `CommitWindow` is marked
**provisional in the source**, and it carries a **delete-by date of
2026-12-31** if no second game uses it. A primitive with one hypothetical
user and a test that exercises only itself is the AM-11 shape, and this
project has now paid for that shape twice.
### Consequences
**Kernel spec→code link: 16/18 → 18/18 (100%).** Stated with the caveat
the gate prints on every run: that is a statement about **names**, not
assertions.
Two self-tests broke and both broke *correctly*:
* `rule-coverage`'s gate test hardcoded "unlinked rules exist today" and
failed the moment the last one was linked. It now computes whether
anything is unlinked and asserts the gate fails **iff** so — the
assertion was right, its premise was transient.
* `facts`' "every fact records a value and its rendered text" rejected
`k_unlinked` once it became legitimately empty. Empty now renders as
`(none)`, and the check distinguishes *absent* from *empty*.
**M-D1-MUT: 8 of 14, unchanged.** K14 and K18 are kernel rules, not
acceptance rows, so neither moves that number — worth stating, because the
temptation is to imply progress on a metric this task never touched.

49
specs/GameKernel.md
View file

@ -105,13 +105,54 @@ Command (actor-tagged intent)
PlayerView` that structurally cannot include: other players' unrevealed
commitments, face-down problem identities, other players' hands.
Projections are derived views — never inputs to `validate`/`fold`.
- **K14** The GROUND round (GR-R01..R09) is expressed through runtime
primitives: one commit window per Select, reveal, then fixed-order
resolution steps with Lead-order iteration (GR-R06/R07) driven by
system commands.
- **K14** *(amended 2026-08-01, CB-WP-0006 T07 — see §2.5a)* The GROUND
round (GR-R01..R09) **implements the commit-window contract**: one
window per Select, duplicate submission rejected, completeness required
before Reveal, then fixed-order resolution steps with Lead-order
iteration (GR-R06/R07) driven by system commands. It implements that
contract **in its own aggregate**; `CommitWindow` in `cb-game-runtime`
is the extracted form, and is **provisional until a second game uses
it**.
### 2.6 GROUND aggregate (`games/ground`)
#### 2.5a Why K14 was amended rather than implemented
The original K14 said the round *is expressed through* runtime
primitives. It was not: `CommitWindow` had **zero non-test users** and
`games/ground` did not import it. GROUND collects selections in its own
`BTreeMap` and enforces the same contract inline — duplicate submission
(`second_selection_is_a_duplicate`), completeness before Reveal
(`GR-R04`), and ordered reveal.
Two options were available and the choice is recorded because it could
reasonably have gone the other way.
**Wiring GROUND through `CommitWindow` was rejected.** It would change
the serialized shape of `selections`, which four scenario files assert by
dot-path (`selections.0.action`) and which every state hash depends on —
a large, risky refactor whose only benefit is making a sentence literally
true. More importantly it inverts INTENT: *"abstractions are extracted
from working games... rather than invented in isolation"*, and *"No
concept becomes canonical merely because it looks general. It becomes
canonical after surviving a second concrete use."* `CommitWindow` was
invented before any game needed it and has survived **zero** uses.
Imposing it on GROUND now would manufacture the first use rather than
discover it.
**So the rule was amended to state what is actually guaranteed**, and the
primitive is kept and marked provisional. It costs ~60 lines, it documents
the seam stage 3 (networked sessions) and stage 4 (packaging) will need,
and re-extracting it from GROUND when a second game exists will be
better-informed than keeping it aligned by hand now.
**Open, with a date:** if no second game uses `CommitWindow` by
**2026-12-31**, it should be deleted rather than carried — a primitive
with one hypothetical user and a test that exercises only itself is the
AM-11 shape (a claim resting on a pair with no consumer), and this project
has now paid for that shape twice.
- **K15** State implements specs/GroundRules.md §1 exactly; every GR-rule
is realized in `validate`/`fold` and cross-referenced by rule ID in doc
comments, giving a greppable rule→code→scenario chain.

9
specs/MetricsAndScenarios.md
View file

@ -53,9 +53,12 @@ and add capability-specific rows only when these don't cover the claim.
> `58/58 (100%)` read as "all rules".
>
> `make coverage` now reports a second, separate denominator:
> **16 of 18** K-rules are named across the source. <!-- fact:k_linked -->
> Unlinked: **K14 K18**. <!-- fact:k_unlinked -->
> (K10 was unlinked until CB-WP-0006 T06 implemented replay bundles.)
> **18 of 18** K-rules are named across the source. <!-- fact:k_linked -->
> Unlinked: **(none)**. <!-- fact:k_unlinked -->
> K10 was unlinked until T06 implemented replay bundles; K14 and K18 until
> T07 amended one and implemented the other. The link is complete — which
> is a statement about **names**, not about assertions, and the gate says
> so on every run.
>
> **Kernel rules are link-only, by design.** They are kernel invariants,
> not game rules: there is no kernel aggregate, setup preset or command

BIN
tools/__pycache__/rule-coverage.cpython-312.pyc
View file

Binary file not shown.

9
tools/facts.py
View file

@ -142,8 +142,10 @@ def measure():
facts["am_rows"] = (len(mrows), "{:,}", "tools/mutation-check.py")
facts["am_unmutatable"] = (sum(1 for r in mrows if r.unmutatable), "{:,}",
"tools/mutation-check.py")
# "(none)" rather than "" — an empty rendered value cannot be tagged in
# prose, and reads as a malformed fact rather than a true one.
facts["k_unlinked"] = (
" ".join(r for r in k_rules if r not in k_named), "{}",
" ".join(r for r in k_rules if r not in k_named) or "(none)", "{}",
"tools/rule-coverage.py")
return facts
@ -350,7 +352,10 @@ def self_test():
check_("every fact records the instrument that produced it",
all(v.get("by") for v in keys.values()))
check_("every fact records both a value and its rendered text",
all("value" in v and v.get("text") for v in keys.values()))
all("value" in v and v.get("text") is not None
for v in keys.values()),
"a legitimately empty value is still a fact — it must not be "
"reported as malformed")
check_("registry is generated, not hand-written",
open(REGISTRY).read().startswith("# GENERATED"))

17
tools/rule-coverage.py
View file

@ -186,6 +186,14 @@ def self_test():
# The gate date must actually change behaviour, in both directions.
# A "binds later" that never binds is the AM-4 failure this replaces.
# What the gate must do depends on whether anything is unlinked, so
# compute that rather than assuming it. An earlier version hardcoded
# "unlinked rules exist today" and failed the moment T07 linked the
# last one — correctly, but for the wrong reason.
_k = parse_rules(open(os.path.join("specs", "GameKernel.md")).read(),
r"\*\*(K\d+)\*\*")
_named = code_ids_over(source_files(), r"\bK\d+\b")
_unlinked = [r for r in _k if r not in _named]
before = kernel_arm(today=datetime.date(2026, 1, 1), quiet=True)
after = kernel_arm(today=datetime.date(2027, 1, 1), quiet=True)
@ -208,9 +216,12 @@ def self_test():
f"{len(out.splitlines())} lines")
check("kernel: quiet suppresses output, loud does not",
out.strip() != "" and _silent_output() == "")
check("kernel: gate reports before the binding date, fails after",
before == 0 and after == 2,
f"before={before} after={after}; unlinked rules exist today")
check("kernel: gate never fails before the binding date",
before == 0, f"before={before}")
check("kernel: after the binding date the gate fails iff rules are unlinked",
after == (2 if _unlinked else 0),
f"after={after}, {len(_unlinked)} unlinked"
+ (f" ({' '.join(_unlinked)})" if _unlinked else " — all linked"))
print("rule-coverage self-test (positive control)")
ok = True