diff --git a/.github/workflows/debt-measure.yml b/.github/workflows/debt-measure.yml index 175f2bb9..84d94d7c 100644 --- a/.github/workflows/debt-measure.yml +++ b/.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" diff --git a/1-formats/k9/spec/MIGRATION-1058.adoc b/1-formats/k9/spec/MIGRATION-1058.adoc index 7befcec4..d24b6279 100644 --- a/1-formats/k9/spec/MIGRATION-1058.adoc +++ b/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. diff --git a/1-formats/k9/tools/README.adoc b/1-formats/k9/tools/README.adoc index ff1f45ef..ea50879b 100644 --- a/1-formats/k9/tools/README.adoc +++ b/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. diff --git a/1-formats/k9/tools/k9-validate.sh b/1-formats/k9/tools/k9-validate.sh index 6df6aa4a..8ada4afe 100755 --- a/1-formats/k9/tools/k9-validate.sh +++ b/1-formats/k9/tools/k9-validate.sh @@ -74,6 +74,17 @@ LEASH_LEVELS="'Kennel 'Yard 'Hunt" 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 @@ self_test() { 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"