feat(k9): normative Nickel contract, canonical validator, conformance suite (#1058, D173) - #1143
Merged
Merged
Conversation
… suite (#1058, D173) Ruling D173: "K9 needs a Nickel contract, not an ABNF." Implements it. Standards - 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc v1.0.0 — normative. File envelope, dialect rules, versioned contract, closed leash set, default-deny capability model, the five Hunt preconditions, signature semantics, four conformance layers. 23 rule ids, indexed in Appendix A. - spec/contract/k9_contract.ncl — the machine-readable contract. - SPEC.adoc — points at the contract as normative; names the component/repo pedigree collision instead of leaving two shapes called "pedigree". Deliberately no k9.abnf: a component body IS a Nickel term, so a whole-file grammar would be a drifting restatement of a language we do not own. The envelope is specified as three octets plus a first-significant-line table. Two distinctions made load-bearing rather than prose - Presence is not verification (10.4): the Hunt `signature` precondition is satisfiable by 'Verified only. 'Present_Unverified is false. No input turns "no verifier ran" into "verified". - A flag is a request that must be paid for (8.4): allow_network/fs_write/ subprocess now REQUIRE net.fetch/fs.write/process.spawn in the grant. A component asking for the network while granting itself nothing is invalid. Hunt is otherwise unchanged: all five preconditions, always, no subset. Validators aligned - tools/k9-validate.sh — canonical. Layered L0 envelope / L1 structural / L2 Nickel / L3 crypto, so a lexical check cannot report a higher layer's authority. A check that could not run is SKIPPED, never a pass; --strict fails the run rather than reporting green over nothing. - .githooks/validate-k9.sh — was its own format: it grepped for a line beginning `contract`, which 0 of 30 tracked K9 files have, so it exited 1 with 30 errors on a clean tree. Now delegates and owns only commit policy. - .githooks/validate-lint-format.sh — excludes *.k9.ncl from the bare nickel typecheck, matching ci-pipeline.yml (2 staged .ncl in, 1 out). - k9-contractile.yml — installs Nickel pinned+sha256 (same pin as ci-pipeline.yml) and runs --self-test, the fixtures --strict, and the corpus. Fixtures: 5 positive, 21 negative. Each negative names its rule and layer and the runner asserts it was rejected BY that rule AT that layer, so a fixture cannot pass for the wrong reason. 20 of 23 rules have a control. Migration: spec/MIGRATION-1058.adoc. Baseline measured — 30 tracked K9 files, 5 conforming, 25 not. .machine_readable/k9-contract-debt.txt grandfathers them shrink-only: fixing a file forces its entry out, and editing a listed file removes its protection. Not yet run: L2. No nickel binary is obtainable in the preparation sandbox (release-asset host TLS-refused, no cargo to build the codeload tarball), so this commit's L2 result comes from the workflow_dispatch run of the job added here. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 39 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configuration
📒 Files selected for processing (38)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,9 @@ | |||
| K9! | |||
The three K9 steps now tee into $GITHUB_STEP_SUMMARY. Step conclusions were already readable through the check-run API; the step bodies were not, and the log blob host is not reachable from every machine that needs the result. The PR now carries the verdict itself. No behavioural change to the gates: each step still exits with the validator's own status via PIPESTATUS[0], and the run scripts drop -e so a failing validator reaches the tee instead of aborting before it. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
The step summaries written last commit turned out not to be readable: the check-run API returns an empty output.summary for Actions jobs, and the log blob hosts are unreachable from the sandbox that needs the result. So the verdict is now posted to the PR itself, edited in place on re-runs. Adds pull-requests:write at the job level (the workflow-level grant stays contents:read) and runs with always(), because a failing gate is exactly when the detail is needed. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37167980969 K9 contract self-testK9 conformance fixtures |
| # always(): a failing gate is exactly when the detail is needed, and a | ||
| # skipped step would publish nothing. | ||
| if: ${{ always() && github.event_name == 'pull_request' }} | ||
| env: |
hyperpolymath
marked this pull request as ready for review
October 4, 2026 01:28
…uld not fail
The first CI run of this branch produced the first Nickel verdict this corpus
has ever had, and it found two defects — both in this PR's own code.
1. `Record` is not a Nickel type. Component's three open fields named it, so
k9_contract.ncl failed with `unbound identifier` and every L2 verdict
downstream was void. All 5 positive controls failed. Now `{ _ : Any }`.
2. Negative-control attribution matched the rule id in the FILENAME. A control
is named `L2-K9-N001-…`, and the human finding line echoes the path, so
grepping that output for `K9-N001` succeeded no matter which rule fired.
With the contract broken, both L2 controls were rejected by K9-N002 and
both still reported `ok`. The suite exists to catch gates that cannot fire;
this was one. Attribution now reads the structured findings and requires an
`error`-severity finding whose rule AND layer both match the filename.
A broken contract is also called out by name rather than reported as "wrong
rule": when K9-N002 fires, no L2 control proved anything.
self-test gains a block asserting the predicate itself — a rule id present only
in a path is not attributed, and a skipped finding cannot satisfy a control.
24 assertions become 29. The first draft of that block asserted E001 fires
once; it fires twice (bad magic also leaves the body unclaimed), so the
well-formedness count is compared rather than fixed at 1.
Still unverified locally: L2. No nickel binary is obtainable in this sandbox,
so the fixtures' L2 half is asserted by the workflow run of this commit.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Contributor
|
Autopilot could not be updated. Open Coding to check access and billing. |
hyperpolymath
enabled auto-merge (squash)
October 4, 2026 01:30
|
hyperpolymath
pushed a commit
that referenced
this pull request
Oct 4, 2026
Two follow-ups to what landed in #1143, both about being able to READ a failure rather than about the gate: - A whole-report ::error never reached the check-run API. Annotations are now emitted per FAIL/ERROR line, capped at 20, each short enough to survive. - The publish step tried to PATCH its previous comment and failed, pinning the PR to a stale report for two runs. It now always posts; stacked reports are cheaper than no result. The K9 fixtures step is red on main as of b3075e0 and this is the change that makes the reason legible. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 4, 2026
Follow-up to #1143. The K9 fixtures step is **red on `main` as of `b3075e0`** and nothing about that is currently readable: the log blob host is unreachable from the sandbox, the step summary is not exposed by the check-run API, and the report comment was pinned to a stale run because the publish step failed trying to PATCH it. This PR changes no gate. It changes only whether a failure can be read. - **One annotation per failure.** A whole-report `::error` never reached `check-runs/{id}/annotations`. Annotations are now emitted per `FAIL`/`ERROR` line (capped at 20), each short enough to survive the parser. - **Always post the report.** The publish step's PATCH branch failed and left the PR showing the report from two runs earlier. It now always creates a comment; each names its run. ## Why this matters beyond convenience The first CI run of #1143 was the **first time any tool in this estate ran Nickel over a K9 file**, and it immediately found two defects in that PR's own code: 1. `k9_contract.ncl` named a `Record` type that does not exist in Nickel. The contract failed with `unbound identifier`, so every L2 verdict downstream was void and all 5 positive controls failed. 2. Negative-control attribution grepped the human-readable finding line, which echoes the **file path** — and a control is named `L2-K9-N001-…`. So the assertion "rejected by K9-N001" succeeded no matter which rule fired. With the contract broken, both L2 controls were rejected by `K9-N002` and both still printed `ok`. A gate that cannot fire is the defect class #49 and #64 established; this suite was built to prevent it and contained one. Both are fixed in #1143. What is *not* yet established is whether the fixtures pass at L2 with the contract repaired — the step is still red, and this PR is how that gets read. `self-test` now asserts the attribution predicate itself (29 assertions): a rule id present only in a filename is not attributed, and a skipped finding cannot satisfy a control. --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <arena-agent@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 4, 2026
, D173) (#1145) **`K9-SVC contractile validation` is green.** Run [`37169542241`](https://github.com/hyperpolymath/standards/actions/runs/37169542241), reconfirmed on `76b841e`: ``` K9 normative contract typecheck ok K9 contract self-test ok 30 assertions K9 conformance fixtures ok 5 positive, 21 negative, 0 failures K9 corpus conformance ok 5 conforming, 25 grandfathered ``` This is the first time any tool in this estate has run Nickel over a K9 file. It found **seven defects, every one of them in #1143's own code**, and not one was visible without a `nickel` binary — which is not obtainable in the sandbox where this was written. | Defect | Effect | |---|---| | `Record` used as a type | Not a Nickel type. The contract did not typecheck, so every L2 verdict was void and all five positive controls failed. | | `Any` used as its replacement | Also not a type; the dynamic type is `Dyn`. Same failure, one run later. | | `let doc = …` in the L2 driver | `doc` is a Nickel keyword (metadata, `x \| doc "…"`). Parse error at the identifier. | | `default = { … }` in two fixtures | `default` is the default-value marker keyword. Nickel's `Ident` admits only `or`, `as`, `include`. | | **L2 ran only `nickel typecheck`** | Documented as *"typechecks the program but does not run it"*. Contracts apply when a value flows, so the predicate behind `schema_version` never fired and **both L2 negative controls were accepted**. | | **Attribution grepped free text** | A control's filename contains its rule id, so "rejected by K9-N001" matched the *path* and succeeded no matter which rule fired — a gate that could not fail, in the suite built to prevent them. | | `std.string.substring i 1 s` | 1.18.0's `substring` is `(start, end, str)`, not a length. It returned `""` past index 0, so `is_semver_of` rejected `"1.0.0"` and every component control with it. | Four are the same lesson: the contract and driver were written against Nickel as *remembered* rather than as *shipped*. Three are gates that reported success without doing the work. ## What changed here - `{ _ : Any }` → `{ _ : Dyn }`; `doc` → `k9_doc`; `default` → `default_recipe`. - **L2 now evaluates** (`nickel export --format json`) as well as typechecks — spec §12.2. - Attribution reads structured findings and requires an `error` whose rule **and** layer match. - A `K9 normative contract typecheck` step ahead of the fixtures, so a broken contract reports as a broken contract instead of five "non-conforming" files. - Failures publish as per-line annotations and a PR comment, because the log blob host is unreachable from here. - self-test: 24 → **30 assertions**, including a Nickel-keyword guard over the contract and all 26 fixtures (verified in both directions: planting `doc = "planted"` turns it red). Ground truth came from the 1.18.0 source tarball over `codeload`, which *is* reachable: `parser/src/lexer.rs` for the keyword list and the `Ident` production, `core/stdlib/std.ncl` for all nine `std` signatures this contract uses. ## Still open The corpus step is pinned to `--layer L1` so it can run in a pre-commit hook, so the **25 grandfathered files have never been through Nickel**. `nickel format --check` has never run on a `.k9.ncl` body anywhere. Both are M7 in `spec/MIGRATION-1058.adoc`, which now records measured results instead of predictions. --------- Co-authored-by: arena-agent <arena-agent@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements ruling D173 on #1058: K9 needs a Nickel contract, not an ABNF.
What this adds
1-formats/k9/spec/K9-CONTRACT-SPEC.adocspec/contract/k9_contract.ncltools/k9-validate.shtools/fixtures/spec/MIGRATION-1058.adocDeliberately no
k9.abnf— a component body is a Nickel term, so a whole-file grammar would be a drifting restatement of a language this estate does not own. The envelope is specified as three octets plus a first-significant-line table.Two distinctions made load-bearing
signatureprecondition is satisfiable by'Verifiedonly;'Present_Unverifiedis false, and no input turns "no verifier ran" into "verified".allow_network/allow_filesystem_write/allow_subprocessnow requirenet.fetch/fs.write/process.spawnin the grant.Hunt is not weakened: all five preconditions, always, no configurable subset, no self-granted evidence. Two items make
'Huntharder to reach, not easier.Validators aligned
.githooks/validate-k9.shwas implementing its own format — it grepped for a line beginningcontract, which 0 of 30 tracked K9 files have, so it exited1with 30 errors on a clean tree. It now delegates to the canonical validator and owns only commit policy..githooks/validate-lint-format.shexcluded nothing, so it rannickel typecheckon*.k9.ncl— whichci-pipeline.ymldocuments as dying "at 1:3 on the!". Now aligned with CI.k9-contractile.ymlinstalls Nickel pinned + sha256-verified (same pin asci-pipeline.yml) and runs--self-test, the fixtures--strict, and the corpus.Verification
--self-test--fixtures--strictwithout nickel3— refuses to report a conformance result0— 5 conforming, 25 grandfathered1, 30 errorscheck-standards-map.sh.nclelsewhere still failsL2 (Nickel semantics) had never run in the sandbox where this was written — no
nickelbinary is obtainable there. This PR's CI run is the first time K9 semantics have been checked in this repository.Refs #1058 · ruling D173