CB-WP-0005 T01: spec->code link over every numbered spec and every crate
AGGREGATE becomes a list of source roots and rule patterns become
per-spec, so the link runs over every numbered spec x every crate rather
than GroundRules.md x games/ground/src/lib.rs.
The prediction held on the first run:
AM-1b kernel spec->code link: 15/18 (83%) across 10 source files
unlinked: K10 K14 K18
Kernel rules are link-only by design, and the output says so: they are
kernel invariants with no aggregate, setup preset or command vocabulary,
so scenarios/kernel/*.yaml with covers: [K11] would be a tag in a
directory the runner cannot dispatch. Claiming scenario coverage for them
is the inflation this gate exists to prevent.
Per ADR-0005 §5 the kernel arm reports without feeding the exit code
until 2026-08-31, then binds — the date in the tool, not in prose, with
days remaining printed every run, because open-ended "gate it later" is
how AM-4's targets went unratified for four workplans. The self-test
asserts the gate returns 0 before that date and 2 after.
The zero-rules positive control is replicated on the new denominator: a
kernel regex that stops matching aborts rather than printing 0/0 as
though it were 100%.
The self-test passed while the tool was completely broken. A print(
inside say() became say(), so every real `make coverage` died with
RecursionError while --self-test reported all-ok — it only ever called
kernel_arm(quiet=True) and never executed the reporting path. The control
named the behaviour and did not assert it, which is precisely what this
workplan is about. Fixed by exercising the loud path and asserting it
prints, then verified by re-breaking say() and confirming both new checks
go red. Seventh instance of the harness-does-nothing shape, in the tool
written to find that shape.
Also caught by its own gate: a self-test label that printed "0 K-ids"
beside a passing ">5" assertion, because the detail string rebuilt the
pattern with different escaping. A label that contradicts its own check
is worse than no label.
k_rules, k_linked and k_unlinked are registered facts under facts-check.
A limit of that checker is recorded rather than patched: it is
line-based, so a tagged value that prose-wraps fails.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
parent
bd4423a8e4
commit
bb35fcb168
6 changed files with 289 additions and 19 deletions
18
facts.toml
18
facts.toml
|
|
@ -57,6 +57,24 @@ text = "21"
|
|||
fmt = "{:,}"
|
||||
by = "tools/rule-coverage.py"
|
||||
|
||||
[k_linked]
|
||||
value = 15
|
||||
text = "15"
|
||||
fmt = "{:,}"
|
||||
by = "tools/rule-coverage.py"
|
||||
|
||||
[k_rules]
|
||||
value = 18
|
||||
text = "18"
|
||||
fmt = "{:,}"
|
||||
by = "tools/rule-coverage.py"
|
||||
|
||||
[k_unlinked]
|
||||
value = 'K10 K14 K18'
|
||||
text = "K10 K14 K18"
|
||||
fmt = "{}"
|
||||
by = "tools/rule-coverage.py"
|
||||
|
||||
[pinned_main]
|
||||
value = 92.03371920000004
|
||||
text = "$92.03"
|
||||
|
|
|
|||
|
|
@ -45,7 +45,34 @@ and add capability-specific rows only when these don't cover the claim.
|
|||
| M-D4-LEAK | D4 | foreign types in canonical interfaces | count | novel — must be 0; enforced by grep/deny rule, the Clay-Borg hard rule |
|
||||
| M-D4-SWAP | D4 | capability has null + reference impls passing the same conformance suite | bool | adapted:hexagonal-architecture port testing |
|
||||
|
||||
### 1b. The coverage gate's two numbers (M-D1-COV, M-D1-LNK)
|
||||
### 1b. The coverage gate's numbers (M-D1-COV, M-D1-LNK)
|
||||
|
||||
> **Widened 2026-07-31 (CB-WP-0005 T01).** Until then the instrument
|
||||
> matched `GR-` only, against `GroundRules.md` only, and linked against
|
||||
> one source file, so all **18** K-rules were outside it. <!-- fact:k_rules -->
|
||||
> `58/58 (100%)` read as "all rules".
|
||||
>
|
||||
> `make coverage` now reports a second, separate denominator:
|
||||
> **15 of 18** K-rules are named across the source. <!-- fact:k_linked -->
|
||||
> Unlinked: **K10 K14 K18**. <!-- fact:k_unlinked -->
|
||||
>
|
||||
> **Kernel rules are link-only, by design.** They are kernel invariants,
|
||||
> not game rules: there is no kernel aggregate, setup preset or command
|
||||
> vocabulary, so a `scenarios/kernel/*.yaml` carrying `covers: [K11]`
|
||||
> would be a tag in a directory the runner cannot dispatch. Claiming
|
||||
> scenario coverage for them would be the inflation this gate exists to
|
||||
> prevent.
|
||||
>
|
||||
> Per ADR-0005 §5 the kernel arm **reports without feeding the exit
|
||||
> code until 2026-08-31**, then binds. A newly widened denominator is not
|
||||
> a regression. The date lives in `tools/rule-coverage.py`, not here, and
|
||||
> the tool prints the days remaining on every run.
|
||||
|
||||
**Both numbers count names.** Neither proves anything fails when a rule is
|
||||
violated. That is **M-D1-MUT** (`make mutation-check`, CB-WP-0005 T02) —
|
||||
four of the seven defects found by CB-RES-0004 were named in the source
|
||||
and inert, and therefore invisible to everything on this page.
|
||||
|
||||
|
||||
M-D1-COV counts tags. It proves no rule is unclaimed and no claimed rule
|
||||
is invented; it does **not** prove a scenario exercises what it names, and
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -128,6 +128,18 @@ def measure():
|
|||
facts["gr_covered"] = (len(hit), "{:,}", "tools/rule-coverage.py")
|
||||
facts["gr_linked"] = (len(hit & code_ids), "{:,}", "tools/rule-coverage.py")
|
||||
facts["gr_scenarios"] = (len(paths), "{:,}", "tools/rule-coverage.py")
|
||||
|
||||
# CB-WP-0005 T01: the kernel denominator, so its numbers are under the
|
||||
# DFD gate from the day they first exist rather than after they drift.
|
||||
k_rules = rc.parse_rules(
|
||||
open(os.path.join(ROOT, "specs/GameKernel.md")).read(), r"\*\*(K\d+)\*\*")
|
||||
k_named = rc.code_ids_over(rc.source_files(), r"\bK\d+\b")
|
||||
facts["k_rules"] = (len(k_rules), "{:,}", "tools/rule-coverage.py")
|
||||
facts["k_linked"] = (len(set(k_rules) & k_named), "{:,}",
|
||||
"tools/rule-coverage.py")
|
||||
facts["k_unlinked"] = (
|
||||
" ".join(r for r in k_rules if r not in k_named), "{}",
|
||||
"tools/rule-coverage.py")
|
||||
return facts
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,26 +1,45 @@
|
|||
#!/usr/bin/env python3
|
||||
"""AM-1 / M-D1-COV: every numbered GR-rule needs >=1 scenario.
|
||||
"""AM-1 / M-D1-COV and AM-1b / M-D1-LNK, over **every** numbered spec.
|
||||
|
||||
Compares the rule IDs declared in specs/GroundRules.md against the
|
||||
`covers:` lists in scenarios/ground/*.yaml. Exits non-zero when a
|
||||
scenario claims a rule the spec does not define, so coverage can never
|
||||
be inflated by a typo'd or invented rule ID.
|
||||
Two denominators, deliberately separate because they are measured
|
||||
differently:
|
||||
|
||||
Stated limit (InnerLoop implementation rule 4): this gate counts tags. It
|
||||
proves no rule is unclaimed and no claimed rule is invented. It does NOT
|
||||
prove a scenario exercises the rule it names.
|
||||
ground GR-rules in specs/GroundRules.md, covered by `covers:` lists in
|
||||
scenarios/ground/*.yaml, and linked to the aggregate source.
|
||||
kernel K-rules in specs/GameKernel.md. **Link only.** K-rules are
|
||||
kernel invariants, not game rules: there is no kernel aggregate,
|
||||
no setup preset and no command vocabulary, so a
|
||||
`scenarios/kernel/*.yaml` with `covers: [K11]` would be a tag in
|
||||
a directory the runner cannot dispatch. Claiming scenario
|
||||
coverage for them would be the inflation this gate exists to
|
||||
prevent.
|
||||
|
||||
Positive control (InnerLoop v1.1 §Step 5): the run asserts it actually
|
||||
found rules and scenarios. Before this was added, a broken spec regex
|
||||
yielded rules=[] and missing=[] and the tool exited 0 reporting "0/0" —
|
||||
the harness-does-nothing class, in the tool that reports our headline
|
||||
coverage number.
|
||||
Until CB-WP-0005 T01, `AGGREGATE` was one file and the rule pattern
|
||||
matched `GR-` only, so the kernel spec was outside the instrument
|
||||
entirely. K10, K14 and K18 were unimplemented for four workplans while
|
||||
`make coverage` printed `58/58 (100%)`.
|
||||
|
||||
Stated limit (InnerLoop implementation rule 4), now doubly important:
|
||||
**this gate counts names.** It proves no rule is unclaimed, no claimed
|
||||
rule is invented, and no rule is absent from the source. It does NOT
|
||||
prove anything fails when a rule is violated — that is M-D1-MUT
|
||||
(`make mutation-check`, CB-WP-0005 T02), and four of the seven defects
|
||||
found in CB-RES-0004 were invisible to a name-based check.
|
||||
|
||||
Positive control (InnerLoop v1.1 §Step 5): every denominator asserts it
|
||||
actually found rules. Before this was added, a broken spec regex yielded
|
||||
rules=[] and missing=[] and the tool exited 0 reporting "0/0" — the
|
||||
harness-does-nothing class, in the tool that reports our headline
|
||||
coverage number. A new denominator inherits the control, or it
|
||||
reintroduces the defect the old one was fixed for.
|
||||
|
||||
Usage:
|
||||
python3 tools/rule-coverage.py
|
||||
python3 tools/rule-coverage.py --self-test
|
||||
"""
|
||||
import datetime
|
||||
import glob
|
||||
import os
|
||||
import re
|
||||
import sys
|
||||
|
||||
|
|
@ -35,14 +54,45 @@ AGGREGATE = "games/ground/src/lib.rs"
|
|||
PROVISIONAL_WARN_DAYS = 30
|
||||
ID_RE = r"GR-[A-Z]+\d+"
|
||||
|
||||
# ADR-0005 §5: a newly widened denominator is not a regression, so the
|
||||
# kernel arm reports without feeding the exit code — but only until a
|
||||
# date that lives in the tool rather than in prose. An open-ended "we
|
||||
# will gate it later" is how AM-4's targets went unratified for four
|
||||
# workplans. The remaining days are printed on every run.
|
||||
KERNEL_GATES_FROM = datetime.date(2026, 8, 31)
|
||||
|
||||
def parse_rules(spec_text):
|
||||
return sorted(set(re.findall(RULE_RE, spec_text)))
|
||||
# Source roots searched for rule IDs. A list, not one file: K-rules live
|
||||
# in cb-kernel, cb-events and cb-game-runtime, so a single-file AGGREGATE
|
||||
# would report every one of them unlinked forever.
|
||||
SOURCE_ROOTS = ("crates", "games", "tools")
|
||||
|
||||
|
||||
def parse_code_ids(text):
|
||||
"""Rule IDs named anywhere in the aggregate source (T09)."""
|
||||
return set(re.findall(ID_RE, text))
|
||||
def source_files(roots=SOURCE_ROOTS):
|
||||
"""Every .rs file under the given roots, excluding build output."""
|
||||
out = []
|
||||
for root in roots:
|
||||
for dirpath, dirnames, files in os.walk(root):
|
||||
dirnames[:] = [d for d in dirnames if d != "target"]
|
||||
out += [os.path.join(dirpath, f) for f in sorted(files)
|
||||
if f.endswith(".rs")]
|
||||
return sorted(out)
|
||||
|
||||
|
||||
def parse_rules(spec_text, pattern=RULE_RE):
|
||||
return sorted(set(re.findall(pattern, spec_text)))
|
||||
|
||||
|
||||
def parse_code_ids(text, pattern=ID_RE):
|
||||
"""Rule IDs named anywhere in the source (T09)."""
|
||||
return set(re.findall(pattern, text))
|
||||
|
||||
|
||||
def code_ids_over(paths, pattern):
|
||||
"""Union of rule IDs named across many source files."""
|
||||
found = set()
|
||||
for p in paths:
|
||||
found |= parse_code_ids(open(p).read(), pattern)
|
||||
return found
|
||||
|
||||
|
||||
def provisional_items(paths):
|
||||
|
|
@ -67,6 +117,17 @@ def parse_covers(text):
|
|||
return {c.strip() for c in match.group(1).split(",") if c.strip()}
|
||||
|
||||
|
||||
def _silent_output():
|
||||
"""Whatever the kernel arm prints with quiet=True — must be nothing."""
|
||||
import io
|
||||
from contextlib import redirect_stdout
|
||||
|
||||
buf = io.StringIO()
|
||||
with redirect_stdout(buf):
|
||||
kernel_arm(today=datetime.date(2026, 1, 1), quiet=True)
|
||||
return buf.getvalue()
|
||||
|
||||
|
||||
def self_test():
|
||||
"""Each assertion pins a failure this tool must detect."""
|
||||
results = []
|
||||
|
|
@ -99,6 +160,58 @@ def self_test():
|
|||
bool(prov) and all(o and r for _, o, r in prov),
|
||||
f"{len(prov)} provisional item(s)")
|
||||
|
||||
# --- CB-WP-0005 T01: the kernel denominator ---
|
||||
# The control the old arm was fixed for, replicated. A pattern that
|
||||
# stops matching must abort, not report 0/0 as though it were 100%.
|
||||
check("kernel: zero rules detected as a failure",
|
||||
parse_rules("no kernel rules here", r"\*\*(K\d+)\*\*") == [])
|
||||
check("kernel: matcher works on the real spec format",
|
||||
parse_rules("- **K10** A replay bundle\n- **K9** A snapshot",
|
||||
r"\*\*(K\d+)\*\*") == ["K10", "K9"])
|
||||
check("kernel: matcher does not match GR-rules",
|
||||
parse_rules("**GR-R06** lead first", r"\*\*(K\d+)\*\*") == [])
|
||||
# A single-file AGGREGATE reported every K-rule unlinked forever; the
|
||||
# union across roots is the fix, so assert it actually unions.
|
||||
# Compute once and report the same value that was asserted. Building
|
||||
# the detail string with a second, re-escaped copy of the pattern
|
||||
# printed "0 K-ids" beside a passing ">5" assertion — a label that
|
||||
# contradicts its own check is worse than no label.
|
||||
srcs = source_files()
|
||||
k_in_src = code_ids_over(srcs, r"\bK\d+\b")
|
||||
check("kernel: ids union across many files, not just one",
|
||||
code_ids_over([os.devnull], r"\bK\d+\b") == set() and len(k_in_src) > 5,
|
||||
f"{len(k_in_src)} K-ids across {len(srcs)} files")
|
||||
check("kernel: source roots resolve to real files",
|
||||
len(srcs) >= 5, f"{len(srcs)} .rs files")
|
||||
|
||||
# The gate date must actually change behaviour, in both directions.
|
||||
# A "binds later" that never binds is the AM-4 failure this replaces.
|
||||
before = kernel_arm(today=datetime.date(2026, 1, 1), quiet=True)
|
||||
after = kernel_arm(today=datetime.date(2027, 1, 1), quiet=True)
|
||||
|
||||
# The reporting path must be exercised, not only the quiet one. When
|
||||
# this control ran `quiet=True` exclusively, a broken `say()` made
|
||||
# every real `make coverage` die with RecursionError while the
|
||||
# self-test printed all-ok — a positive control that named the
|
||||
# behaviour without asserting it, which is exactly the defect
|
||||
# CB-RES-0004 is about.
|
||||
import io
|
||||
from contextlib import redirect_stdout
|
||||
|
||||
buf = io.StringIO()
|
||||
with redirect_stdout(buf):
|
||||
loud = kernel_arm(today=datetime.date(2026, 1, 1))
|
||||
out = buf.getvalue()
|
||||
check("kernel: the reporting path actually prints",
|
||||
loud == before and "AM-1b kernel spec->code link:" in out
|
||||
and "gate:" in out,
|
||||
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")
|
||||
|
||||
print("rule-coverage self-test (positive control)")
|
||||
ok = True
|
||||
for name, passed, detail in results:
|
||||
|
|
@ -192,8 +305,72 @@ def main():
|
|||
print(" ERROR — claimed but not defined in the spec:", " ".join(invented),
|
||||
file=sys.stderr)
|
||||
return 1
|
||||
|
||||
kernel_rc = kernel_arm()
|
||||
if kernel_rc:
|
||||
return kernel_rc
|
||||
return 0 if not missing else 2
|
||||
|
||||
|
||||
def kernel_arm(today=None, quiet=False):
|
||||
"""AM-1b over specs/GameKernel.md × every crate (CB-WP-0005 T01).
|
||||
|
||||
Link only — see the module docstring for why K-rules cannot use the
|
||||
scenario `covers:` mechanism. Returns a non-zero code only once
|
||||
KERNEL_GATES_FROM has passed.
|
||||
"""
|
||||
today = today or datetime.date.today()
|
||||
|
||||
def say(*a, **kw):
|
||||
if not quiet:
|
||||
print(*a, **kw)
|
||||
|
||||
spec = os.path.join("specs", "GameKernel.md")
|
||||
rules = parse_rules(open(spec).read(), r"\*\*(K\d+)\*\*")
|
||||
|
||||
# The inherited positive control. A pattern that stops matching must
|
||||
# abort, not report 0/0 as though it were an answer.
|
||||
if not rules:
|
||||
print(f"\nERROR — no K-rules parsed from {spec}; refusing to report "
|
||||
f"kernel coverage", file=sys.stderr)
|
||||
return 1
|
||||
paths = source_files()
|
||||
if not paths:
|
||||
print("\nERROR — no source files found under "
|
||||
f"{'/, '.join(SOURCE_ROOTS)}/; refusing to report kernel coverage",
|
||||
file=sys.stderr)
|
||||
return 1
|
||||
|
||||
named = code_ids_over(paths, r"\bK\d+\b")
|
||||
known = set(rules)
|
||||
linked = sorted(known & named)
|
||||
unlinked = [r for r in rules if r not in named]
|
||||
phantom = sorted(named - known)
|
||||
|
||||
days = (KERNEL_GATES_FROM - today).days
|
||||
binding = days <= 0
|
||||
pct = 100 * len(linked) // len(rules)
|
||||
say(f"\nAM-1b kernel spec->code link: {len(linked)}/{len(rules)} ({pct}%) "
|
||||
f"K-rules named across {len(paths)} source files")
|
||||
say(" NOTE: link only — K-rules are kernel invariants with no scenario "
|
||||
"mechanism; and this counts names, not assertions (see "
|
||||
"`make mutation-check`)")
|
||||
if binding:
|
||||
say(f" gate: BINDING since {KERNEL_GATES_FROM}")
|
||||
else:
|
||||
say(f" gate: reporting only for {days} more day(s), binds "
|
||||
f"{KERNEL_GATES_FROM} (ADR-0005 §5)")
|
||||
if unlinked:
|
||||
say(" unlinked (declared in the spec, named nowhere in source):")
|
||||
say(" ", " ".join(unlinked))
|
||||
if phantom:
|
||||
say(" ERROR — K-id in code that the spec does not define:",
|
||||
" ".join(phantom), file=sys.stderr)
|
||||
return 1
|
||||
if unlinked and binding:
|
||||
return 2
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
|
|
|
|||
|
|
@ -66,6 +66,42 @@ output:
|
|||
**Refuted if** any numbered rule in any spec is still unnamed in source
|
||||
after the pass and the tool does not say so.
|
||||
|
||||
**Delivered, and the prediction held on the first run:**
|
||||
|
||||
```text
|
||||
AM-1b kernel spec->code link: 15/18 (83%) K-rules named across 10 source files
|
||||
NOTE: link only — K-rules are kernel invariants with no scenario
|
||||
mechanism; and this counts names, not assertions
|
||||
gate: reporting only for 31 more day(s), binds 2026-08-31 (ADR-0005 §5)
|
||||
unlinked (declared in the spec, named nowhere in source):
|
||||
K10 K14 K18
|
||||
```
|
||||
|
||||
`AGGREGATE` is now a list of source roots, rule patterns are per-spec, and
|
||||
the link runs over every numbered spec × every crate. The binding date
|
||||
lives in the tool and the days remaining are printed every run. The
|
||||
kernel figures (`k_rules`, `k_linked`, `k_unlinked`) are registered facts,
|
||||
so they are under `make facts-check` from the day they first exist rather
|
||||
than after they drift.
|
||||
|
||||
**The self-test passed while the tool was completely broken.** A
|
||||
`print(` inside `say()` was rewritten to `say(`, so every real
|
||||
`make coverage` died with `RecursionError` — while `--self-test` reported
|
||||
all-ok, because it only ever called `kernel_arm(quiet=True)` and never
|
||||
executed the reporting path.
|
||||
|
||||
That is this task's own thesis in miniature: **the control named the
|
||||
behaviour and did not assert it.** Fixed by exercising the loud path under
|
||||
`redirect_stdout` and asserting it prints, and verified by re-breaking
|
||||
`say()` and confirming the two new checks go red. Seventh instance of the
|
||||
harness-does-nothing shape, found in the tool written to find that shape.
|
||||
|
||||
**A limit of `facts-check` surfaced here and is recorded, not patched:**
|
||||
the check is line-based, so a tagged value that prose-wraps onto the next
|
||||
line fails. It cost three edits to place two tags. Reported for T07 —
|
||||
either the checker spans a paragraph, or the rule is stated as
|
||||
"tagged values must not wrap".
|
||||
|
||||
## Task: M-D1-MUT — one mutation per acceptance row
|
||||
|
||||
```task
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue