test(k9): make M6's mirror guard real; fix(ci): give the debt measurement provenance

.github/workflows/debt-measure.yml

@@ -49,6 +49,21 @@ jobs:
         id: measure
         run: |
           set -uo pipefail
+
+          # Record WHAT we measured against. This workflow measures on Monday
+          # and a human merges whenever they get to it; between those two
+          # moments `main` can move, and the recorded numbers then describe a
+          # tree that is not the tree they land in. That is exactly what
+          # happened with #1302: it measured 83 against e16a231 on 2026-10-19,
+          # `docs/reorg/2026-10-14-tidy/WORK-ORDERS-2026-10-19.adoc` landed
+          # later that day (#1298) taking the tree to 84, and the merged file
+          # said 83 — so `todo-fixme-markers` breached every Monday for five
+          # weeks. Nothing in the pipeline can close that window while the
+          # merge is a human act, so the numbers carry their own provenance
+          # and the PR says out loud how to check them.
+          echo "base_sha=$(git rev-parse HEAD)" >> "$GITHUB_OUTPUT"
+          echo "base_when=$(git log -1 --format=%cd --date=short HEAD)" >> "$GITHUB_OUTPUT"
+
           if [ ! -f .machine_readable/Debtfile.a2ml ]; then
             echo "No Debtfile — nothing to measure."
             echo "changed=no" >> "$GITHUB_OUTPUT"
@@ -89,10 +104,11 @@ jobs:
           # leaves the workflow unparseable — the estate already has a large
           # population of workflows broken exactly this way.
           git commit -m "chore(debt): re-measure Debtfile probes" \
-                     -m "Machine-written by .github/workflows/debt-measure.yml. Counts follow the probes; ceilings only ever fall. A ceiling that needs to RISE is not done here — raise it in a human PR with a Debt-exception: trailer."
+                     -m "Machine-written by .github/workflows/debt-measure.yml. Counts follow the probes; ceilings only ever fall. A ceiling that needs to RISE is not done here — raise it in a human PR with a Debt-exception: trailer." \
+                     -m "Measured against ${{ steps.measure.outputs.base_sha }} (${{ steps.measure.outputs.base_when }}). If main has moved since, these numbers are stale; re-run this workflow before merging."
           git push -f origin "$BRANCH"
 
-          BODY="$(printf 'Automated re-measurement of `.machine_readable/Debtfile.a2ml`.\n\n```\n%s\n```\n\nCeilings only fall here. If an entry breached its ceiling this PR is red on\npurpose — pay the debt down, or raise the ceiling in a human commit carrying\na `Debt-exception:` trailer naming the entry.\n\nSee `docs/DEBTFILE-SPEC.adoc`.\n' "$(cat "$RUNNER_TEMP/report.txt")")"
+          BODY="$(printf 'Automated re-measurement of `.machine_readable/Debtfile.a2ml`.\n\n```\n%s\n```\n\n**Measured against `%s` (%s).** These numbers describe that tree, not\nnecessarily the tree this PR will land in. If `main` has moved since, re-run\nthe workflow before merging — merging a stale measurement is what left\n`todo-fixme-markers` breached for five weeks after #1302.\n\nCeilings only fall here. If an entry breached its ceiling this PR is red on\npurpose — pay the debt down, or raise the ceiling in a human commit carrying\na `Debt-exception:` trailer naming the entry.\n\nSee `docs/DEBTFILE-SPEC.adoc`.\n' "$(cat "$RUNNER_TEMP/report.txt")" "${{ steps.measure.outputs.base_sha }}" "${{ steps.measure.outputs.base_when }}")"
 
           if gh pr view "$BRANCH" --json number >/dev/null 2>&1; then
             gh pr edit "$BRANCH" --body "$BODY"

1-formats/k9/spec/MIGRATION-1058.adoc

@@ -80,6 +80,42 @@ Rule incidence across the 25:
 |K9-S014 |3 |Leash claim outside `pedigree.security`.
 |===
 
+=== Re-measured 2026-10-24
+
+The table above is the baseline as it stood when this plan was written. It no
+longer describes the tree, so here is the same measurement taken again rather
+than a silent edit of history. Same command, same validator:
+
+[cols="2,1,4"]
+|===
+|Files in scope |15 |Not 30. The 12 session-management `PROTOCOL.k9` paths
+named in M2 were never tracked files under that path, and the three templates
+in M3 were renamed to `*.k9.ncl.in` — a template is not a component and is
+never loaded, so it is out of scope by construction.
+|Conforming |*12* |
+|Routed |*2* |`coordination.k9` and
+`2-protocols/k9-coordination/examples/minimal.k9`, both to the coordination
+grammar rather than to this contract.
+|Non-conforming |*1* |`9-archive/rhodium-standard-repositories/rsr-compliance-checklist.k9.ncl`
+— M5. It fails K9-S004, K9-S005 and K9-S014. `.githooks/validate-k9.sh` prunes
+`9-archive/`, so it is outside the gate; the command above does not prune it,
+which is why the two disagree. That difference is worth knowing about rather
+than discovering: the gate's scope is narrower than this plan's measurement
+command.
+|Ledger entries |*0* |`.machine_readable/k9-contract-debt.txt` is empty and
+stays as the place a future exemption goes, with its `Ratchet-exception` line.
+|Self-test assertions |*48* |
+|Fixtures |6 positive, 21 negative |Two negative controls need `nickel` to
+assert L2 rejection and report SKIP without it; they run in CI.
+|===
+
+M1, M3 and M4 are resolved. M2 is resolved by the discovery above — there was
+no suffix collision to settle in tracked files. M5's file is archived and out
+of gate scope. The plan has therefore reached *M6*, and M6 is where the work
+resumes.
+
+
+
 == Why this is a ratchet and not a wall
 
 Turning 25 files red in one commit is how this estate has twice ended up
@@ -375,6 +411,28 @@ duplication is deliberate for now — those files carry host-side machinery
 business holding — and `--self-test` asserts the mirrors agree, so it cannot
 drift silently.
 
+*2026-10-24: that last clause was false, and is now made true.* `--self-test`
+asserted the *bash* mirrors in `k9-validate.sh` against the contract and never
+opened `leash.ncl` or `capabilities.ncl` at all — `grep -nE
+'leash\.ncl|capabilities\.ncl'` over the validator returned nothing. The two
+lists happened to agree, so nothing had drifted yet, but the guard this
+paragraph relied on did not exist: exactly the defect class this whole body of
+work exists to catch. Four assertions now close it — `leash.ncl`'s
+`SecurityLevel` enum against the contract's `leash_levels`, `capabilities.ncl`'s
+`core` array against `core_capabilities`, and the two closed sets pinned in
+their own right (the leash taxonomy is exactly three, `hunt_preconditions` is
+exactly the five of §9.2). Each value is extracted as data, from the enum and
+array literals, never from a comment, so rewriting the prose that documents a
+list cannot satisfy the check that tests it. All four were mutation-tested:
+renaming a capability in `capabilities.ncl`, dropping `'Yard` from
+`leash.ncl`, deleting `dry_run` from the contract's `hunt_preconditions` —
+which would silently weaken Hunt — and adding a fourth leash, each produce a
+FAIL. The last trips three assertions at once, including the closed-set one.
+
+Still open in M6: deriving the lists from one source rather than asserting two
+copies agree, and making the §16.2 relationship between the component pedigree
+and the repository pedigree explicit in `SPEC.adoc`.
+
 Deriving them from one source is the right end state. Do it *after* M1–M5, so
 that the change can be verified against a corpus that already conforms rather
 than against one that does not.

1-formats/k9/tools/README.adoc

@@ -149,6 +149,35 @@ and *both of these controls were accepted*. They are the reason L2 now
 evaluates as well as typechecks (§12.2). A suite whose negative controls can
 only pass would not have noticed.
 
+=== The host-side mirrors
+
+The closed leash set and the closed core capability set are each written down
+twice: once in link:../spec/contract/k9_contract.ncl[`k9_contract.ncl`], which
+is normative, and once in link:../leash.ncl[`leash.ncl`] and
+link:../capabilities.ncl[`capabilities.ncl`], which carry the host-side
+machinery — `detect_level`, `check_level`, the handshake records — that a
+contract file has no business holding. The validator never loads those two.
+
+`--self-test` therefore asserts the two copies agree, and pins each set in its
+own right:
+
+[horizontal]
+`leash.ncl SecurityLevel mirrors k9_contract.ncl` |The enum literal against the
+contract's `leash_levels`.
+`capabilities.ncl core mirrors k9_contract.ncl` |The array literal against
+`core_capabilities`, order included.
+`the leash taxonomy is exactly three, closed (§7)` |So a fourth leash cannot
+appear in the contract without a decision.
+`hunt_preconditions is exactly the five, closed (§9.2)` |So Hunt cannot be
+weakened by dropping a precondition. A valid signature alone was never
+sufficient and this is one of the places that stops it becoming so by accident.
+
+Every value is extracted from the enum and array literals, never from a
+comment: rewriting the prose that documents a list must not be able to satisfy
+the check that tests it. All four were mutation-tested — renaming a capability,
+dropping `'Yard` from the enum, deleting `dry_run` from `hunt_preconditions`,
+and adding a fourth leash each produce a FAIL.
+
 == Byte-preserved fixtures
 
 `L0-K9-E003-crlf.k9.ncl` exists to be rejected for its line endings.
@@ -172,4 +201,6 @@ Corpus scans must skip `fixtures/` entirely, for the mirror-image reason: a
 . Add a negative control named for it, and assert it fires *at the layer you
   claimed*.
 . If the rule duplicates a list already in `leash.ncl` or `capabilities.ncl`,
-  add a `--self-test` mirror assertion so the duplication cannot drift.
+  add a `--self-test` mirror assertion so the duplication cannot drift. The two
+  lists that exist today are already covered — see _The host-side mirrors_
+  below — so this step is about the next one, not those.

1-formats/k9/tools/k9-validate.sh

@@ -74,6 +74,17 @@
 CORE_CAPABILITIES="fs.read fs.write net.fetch process.spawn container.run secret.read deploy.apply rollback.apply"
 EXTENSION_PREFIX="x-"
 
+# The same two closed lists are also written down in the host-side files
+# leash.ncl and capabilities.ncl, which this validator never loads — they carry
+# `detect_level`, `check_level` and the handshake records a contract file has no
+# business holding. MIGRATION-1058 M6 states that "--self-test asserts the
+# mirrors agree, so it cannot drift silently". That was true of the bash
+# constants above and false of these two files: nothing read them. --self-test
+# now does.
+K9_DIR="$(cd -- "$SPEC_DIR/.." && pwd)"
+LEASH_NCL="$K9_DIR/leash.ncl"
+CAPABILITIES_NCL="$K9_DIR/capabilities.ncl"
+
 LAYER="all"
 STRICT=0
 JSON=0
@@ -745,6 +756,27 @@
   t "schema_major mirrors k9_contract.ncl" "$SCHEMA_MAJOR" \
     "$(grep -oE 'schema_major = "[^"]+"' "$CONTRACT" | sed 's/.*"\(.*\)"/\1/')"
 
+  echo "== the host-side .ncl mirrors cannot drift either (M6) =="
+  # Every value below is extracted as DATA — the enum literal and the array
+  # literal — and never from a comment, so rewriting the prose that documents
+  # a list cannot satisfy the assertion that checks it.
+  local cn hp
+  t "leash.ncl SecurityLevel mirrors k9_contract.ncl" \
+    "$(grep -oE "leash_levels = \[[^]]*\]" "$CONTRACT" | grep -oE "'[A-Za-z]+" | tr '\n' ' ' | sed 's/ $//')" \
+    "$(grep -oE "let SecurityLevel = \[\|[^]]*\|\]" "$LEASH_NCL" | grep -oE "'[A-Za-z]+" | tr '\n' ' ' | sed 's/ $//')"
+  cn="$(awk '/core_capabilities = \[/,/^  \]/' "$CONTRACT" | grep -oE '"[a-z]+\.[a-z]+"' | tr -d '"' | tr '\n' ' ' | sed 's/ $//')"
+  t "capabilities.ncl core mirrors k9_contract.ncl" "$cn" \
+    "$(awk '/^  core = \[/,/^  \]/' "$CAPABILITIES_NCL" | grep -oE '"[a-z]+\.[a-z]+"' | tr -d '"' | tr '\n' ' ' | sed 's/ $//')"
+  # §9.2 — Hunt needs all five, always. This is a closed set: a precondition
+  # removed from the contract must fail here rather than quietly weaken Hunt.
+  hp="$(awk '/hunt_preconditions = \[/,/^  \]/' "$CONTRACT" | grep -oE '"[a-z_]+"' | tr -d '"' | tr '\n' ' ' | sed 's/ $//')"
+  t "hunt_preconditions is exactly the five, closed (§9.2)" \
+    "signature policy sandbox dry_run capability_grant" "$hp"
+  # §7 — the leash taxonomy is likewise closed, in both directions.
+  t "the leash taxonomy is exactly three, closed (§7)" \
+    "'Kennel 'Yard 'Hunt" \
+    "$(grep -oE "leash_levels = \[[^]]*\]" "$CONTRACT" | grep -oE "'[A-Za-z]+" | tr '\n' ' ' | sed 's/ $//')"
+
   echo "== capability arithmetic (§8) =="
   expect_ok  capability_ok "fs.read"
   expect_ok  capability_ok "rollback.apply"