diff --git a/facts.toml b/facts.toml index 4081f65..5358384 100644 --- a/facts.toml +++ b/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" diff --git a/specs/MetricsAndScenarios.md b/specs/MetricsAndScenarios.md index 9d523f8..372a8e7 100644 --- a/specs/MetricsAndScenarios.md +++ b/specs/MetricsAndScenarios.md @@ -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. +> `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. +> Unlinked: **K10 K14 K18**. +> +> **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 diff --git a/tools/__pycache__/rule-coverage.cpython-312.pyc b/tools/__pycache__/rule-coverage.cpython-312.pyc index a921196..ccfb67d 100644 Binary files a/tools/__pycache__/rule-coverage.cpython-312.pyc and b/tools/__pycache__/rule-coverage.cpython-312.pyc differ diff --git a/tools/facts.py b/tools/facts.py index 00dd687..e6c220a 100644 --- a/tools/facts.py +++ b/tools/facts.py @@ -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 diff --git a/tools/rule-coverage.py b/tools/rule-coverage.py index 9809dbf..f899413 100755 --- a/tools/rule-coverage.py +++ b/tools/rule-coverage.py @@ -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()) diff --git a/workplans/CB-WP-0005-assertion-coverage.md b/workplans/CB-WP-0005-assertion-coverage.md index e574642..d20d952 100644 --- a/workplans/CB-WP-0005-assertion-coverage.md +++ b/workplans/CB-WP-0005-assertion-coverage.md @@ -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