Repository navigation
docs(k9): close M6 and M7 with measured evidence - #1330
Conversation
MIGRATION-1058 claimed two things were still open. One was already done and the other is a decision, not a deferral. Both are now recorded as measured rather than asserted. M6, the §16.2 half: §16.2 of K9-CONTRACT-SPEC.adoc — "`pedigree.ncl` — a different contract" — already names both pedigrees, tables them by subject and normative source, and states that a reader MUST NOT apply one to the other. Checking that exposed a worse error in the tooling used to write the note: the cross-reference pass did not model AsciiDoc's `:sectnums!:` at line 16 and `:sectnums:` at line 68 of the spec, so it numbered the unnumbered _Abstract_ and _Status_ sections and reported every reference in the document as two sections out. §16.2 appeared to resolve to "The negative controls are the point". With the toggle modelled, all 121 `§`-references across the 25 K9 documents resolve and §16.2 is the pedigree section. Five references were nearly "corrected" into being wrong. M6, the derivation half: closed as a decision. Nothing in this repository imports leash.ncl or capabilities.ncl — the only import of any host-side file is two illustrative snippets in GUIDE.adoc, and they import pedigree.ncl. hyperpolymath/k9-ecosystem, which the archived k9-svc scorecard names as where the implementation went, keeps its own copies (its Containerfile COPYs pedigree.ncl register.ncl leash.ncl; its Justfile typechecks them); cloned at 20f6be5 it references nothing under standards/1-formats/k9/ and never mentions capabilities.ncl. And the leash taxonomy cannot be single-sourced in Nickel at all: SecurityLevel is a type, `[| 'Kennel, 'Yard, 'Hunt |]`, and a type cannot be derived from the array leash_levels. The closed set must therefore exist in at least two forms, which makes the four mutation-tested assertions the correct permanent control rather than a stopgap. Importing the capability array alone would trade a cross-check for a tautology, for one list, in files nothing consumes. M7: L2 over the corpus is live. k9-conformance.yml:272 runs every committed K9 file through `--strict --layer L2`, and line 204 scopes it to tracked files outside .k9-canon/, 9-archive/ and the fixtures. The ledger is empty, so there is nothing left to work down. M5's prediction that the archived checklist is a Nickel parse error is not tested and never will be by this gate, because that pathspec excludes 9-archive/ — recorded as unverified rather than dropped. A green lane is not on its own evidence that L2 ran: a file with any `skipped` finding is graded indeterminate (scripts/lib/k9-grid.jq:132), indeterminate makes the state orange, and the Gate only fails orange when fail-on-indeterminate is set. A run with no Nickel binary would grade every file indeterminate and pass. What settles it is the step list of run 40052958049 on main, read from the jobs API: Install Nickel, Contract typecheck, Validate every committed K9 file (L0–L2, strict) and Gate all success. Verified: 121 §-references across 25 K9 documents resolve against numbering that models the sectnums toggles; table delimiters balanced; --self-test 48/48 (0 FAIL, 0 SKIP); fixtures 6 positive, 21 negative (2 needing nickel), 0 failures; hook 12 conforming, 0 grandfathered, 2 routed, exit 0; ledger 0 entries; link-rot findings in 1-formats/k9 unchanged at 7, all in files this commit does not touch. The only item left from this plan is `nickel format --check` on a `.k9.ncl` body — proposal P5. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Caution Review failedThe pull request is closed. 📝 Summary
Merge Risk:
|
|
🟢 conformant · commit
K9 live corpus (L0–L2): 2 finding(s) / scope notes
Scope: DEED syntax and K9 contracts L0–L2. L3 signature verification and routed coordination dialects are not certified. Green is limited to this scope. Orange is missing evidence; grey is an explicit scope exclusion. Logs and report.json are in the dated conformance-evidence artifact on the linked run. |
|



Closes out M6 and M7 of
1-formats/k9/spec/MIGRATION-1058.adoc. Both were recorded as open; one was already done and the other is a decision rather than a deferral.The correction that matters most
Last turn's note said M6 still needed "making the §16.2 relationship … explicit in
SPEC.adoc". §16.2 already does exactly that — it names the component pedigree and the repository pedigree, tables them by subject and normative source, and states a reader MUST NOT apply one to the other.Checking that exposed a worse problem in the tooling used to write the note. The cross-reference pass did not model AsciiDoc's
:sectnums!:(line 16) /:sectnums:(line 68) toggle inK9-CONTRACT-SPEC.adoc, so it numbered the unnumbered Abstract and Status sections and reported every reference in the document as two sections out. §16.2 appeared to resolve to "The negative controls are the point". Five references were nearly "corrected" into being wrong.With the toggle modelled:
k9-grid.jqand the spec are both right; the checker was wrong.M6 — derivation is a decision, measured not assumed
leash.ncl/capabilities.ncl?GUIDE.adoc, and they importpedigree.ncl.hyperpolymath/k9-ecosystemconsume them?20f6be5: itsContainerfileCOPYspedigree.ncl register.ncl leash.ncl, itsJustfiletypechecks them, and it references nothing understandards/1-formats/k9/.capabilities.nclis never mentioned.SecurityLevelis a type — `[So the closed set must exist in at least two forms regardless, which makes the four mutation-tested assertions added in #1329 the correct permanent control rather than a stopgap. Importing the capability array alone would trade a cross-check for a tautology, for one list, in files nothing consumes. Not done, on purpose.
M7 — L2 over the corpus is live
k9-conformance.yml:272runs every committed K9 file through--strict --layer L2; line 204 scopes it to tracked files outside.k9-canon/,9-archive/and the fixtures. The ledger is empty, so there is nothing left to work down.A green lane is not by itself evidence that L2 ran. A file with any
skippedfinding is gradedindeterminate(scripts/lib/k9-grid.jq:132),indeterminatemakes the stateorange, and the Gate only failsorangewhenfail-on-indeterminateis set — which it is not by default. A run with no Nickel binary would grade every file indeterminate and pass.What settles it is the step list of run
40052958049onmain, read from the jobs API:Nickel was present, so L2 was not skipped, so the 12 files passed Nickel semantics and not merely the lexical screen.
Recorded as unverified, not dropped: M5's prediction that
rsr-compliance-checklist.k9.nclis a Nickel parse error is not tested and never will be by this gate, because that pathspec excludes9-archive/.Issue breakdown status
#A/#C/#D done. #B moot (its files were never tracked). #E moot (archived, out of gate scope). #F done. #G closed as a decision. None was filed as an issue; the work was done directly.
Verification
The only item left from this plan is
nickel format --checkon a.k9.nclbody — proposal P5. Behind that sits the larger open hole: L3 has no implementation, soK9_SIG_VERIFIERis unset everywhere, every'Huntcomponent reports'Present_Unverified, and Hunt is unauthorised estate-wide.