From cb7153ace1a1dfcc8941f8d1ca4195c342fc021c Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 4 Oct 2026 01:43:52 +0000 Subject: [PATCH 1/5] =?UTF-8?q?fix(k9):=20Dyn,=20not=20Any=20=E2=80=94=20a?= =?UTF-8?q?nd=20typecheck=20the=20contract=20as=20its=20own=20step?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main is red on the K9 gate. #1144 merged at 9c971da, one commit before this fix, so `{ _ : Any }` is what shipped — and `Any` is not a Nickel type. The annotations #1144 added name it: `unbound identifier 'Any'` at k9_contract.ncl:422:20. The dynamic type is `Dyn`. `Record` was wrong before it; both names were asserted from memory in a sandbox with no nickel binary, and both voided every L2 verdict downstream, because a contract that does not typecheck cannot judge anything. The static audit meant to catch the first one did not: it scanned `| T` positions only, and `{ _ : Any }` puts its type after a colon. It now also scans `_ : T` and `Array T`, and its builtin whitelist is narrowed to the four types this repo's CI-passing .ncl actually uses. It reports exactly one identifier it cannot evidence from the repo: `Dyn`, lines 428-430. k9-contractile.yml gains a `K9 normative contract typecheck` step ahead of the fixtures. `nickel typecheck` stops at the first error, and a broken contract presents as five non-conforming positive controls rather than one broken contract — that misdirection cost two runs to see through. Unverified here: whether `Dyn` typechecks. Nothing else in this repo uses it, so the workflow run of this commit is the evidence. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/k9-contractile.yml | 25 ++++++++++++++++++++++ 1-formats/k9/spec/contract/k9_contract.ncl | 24 +++++++++++++-------- 2 files changed, 40 insertions(+), 9 deletions(-) diff --git a/.github/workflows/k9-contractile.yml b/.github/workflows/k9-contractile.yml index 939bf2f21..db20bb2c8 100644 --- a/.github/workflows/k9-contractile.yml +++ b/.github/workflows/k9-contractile.yml @@ -127,6 +127,31 @@ jobs: # reads it back — which matters on a machine that cannot reach the log # blob host. `set -uo pipefail` without `-e` so a failing validator still # reaches the tee and its own status is what the step exits with. + - name: K9 normative contract typecheck + run: | + set -uo pipefail + # Its own step, ahead of the fixtures. `nickel typecheck` stops at the + # first error, and when the contract is broken every fixture verdict + # downstream is void — reported as five "non-conforming" positive + # controls rather than one broken contract. Twice now that cost a run + # to diagnose (`Record`, then `Any`: neither is a Nickel type). + set +e + out="$(nickel typecheck 1-formats/k9/spec/contract/k9_contract.ncl 2>&1)"; rc=$? + set -e + { + echo '## K9 normative contract typecheck' + echo '```' + [ $rc -eq 0 ] && echo 'k9_contract.ncl typechecks' || printf '%s\n' "$out" + echo '```' + } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT" + if [ $rc -ne 0 ]; then + printf '%s\n' "$out" | head -20 | while IFS= read -r line; do + esc="$(printf '%s' "$line" | sed 's/%/%25/g' | tr -d '\r\n')" + [ -n "$esc" ] && printf '::error title=k9_contract.ncl does not typecheck::%s\n' "$esc" + done + fi + exit $rc + - name: K9 contract self-test run: | set -uo pipefail diff --git a/1-formats/k9/spec/contract/k9_contract.ncl b/1-formats/k9/spec/contract/k9_contract.ncl index c9d85c0e4..647f0bde1 100644 --- a/1-formats/k9/spec/contract/k9_contract.ncl +++ b/1-formats/k9/spec/contract/k9_contract.ncl @@ -413,15 +413,21 @@ let is_semver_of = fun major v => # 'Hunt. The validator enforces that; this contract only shapes the blocks. Component = { pedigree | Pedigree, - # `{ _ : Any }` is the open record: any fields, any values. These three - # blocks are the component's own business and the contract deliberately - # does not shape them — §6.7's `recipes`-forces-'Hunt rule is enforced by - # the validator over the extracted facts, not by a type here. There is no - # `Record` builtin in Nickel; this field used to name one, so the contract - # itself failed to typecheck and every L2 verdict downstream was void. - config | { _ : Any } | optional, - recipes | { _ : Any } | optional, - validation | { _ : Any } | optional, + # An open record: any fields, any values. These three blocks are the + # component's own business and the contract deliberately does not shape + # them — §6.7's `recipes`-forces-'Hunt rule is enforced by the validator + # over the extracted facts, not by a type here. + # + # Two names were tried and rejected by Nickel before this one: `Record` + # and then `Any`. Neither exists; the dynamic type is `Dyn`. Both failures + # were invisible locally — no nickel binary is obtainable in the sandbox + # that wrote this file — and both made every L2 verdict downstream void, + # because a contract that does not typecheck cannot judge anything. That + # is why k9-contractile.yml now typechecks this file as its own named step + # before the fixtures run. + config | { _ : Dyn } | optional, + recipes | { _ : Dyn } | optional, + validation | { _ : Dyn } | optional, }, # ── §11 Library dialect ────────────────────────────────────────────── From 76b85614694c9111925ccf0fc7cdd13a2da8321a Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 4 Oct 2026 01:49:10 +0000 Subject: [PATCH 2/5] fix(k9): `doc` and `default` are Nickel keywords, not identifiers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Dyn` typechecks — the new contract step passed, so the contract itself is sound. What was left was the L2 driver, and the fixture bodies it feeds. unexpected token ┌─ .k9-validate.7812.799.driver.ncl:2:5 2 │ let doc = import "./.k9-validate.7812.799.body.ncl" in │ ^^^ Nickel's lexer reserves `doc` — it is the metadata keyword in `x | doc "..."`. Its `Ident` production admits exactly three contextual keywords, `or`, `as` and `include`; everything else on the keyword list is unusable as a binding or field name. `let k9_doc = ...` replaces it. The same list caught a second violation the CI run had not reached yet: two fixtures declare a recipe field named `default`, which is the default-value marker keyword. Renamed to `default_recipe`. self-test gains a guard over the contract and all 26 fixtures, keyword list taken from nickel 1.18.0's parser/src/lexer.rs. `| default = x` is Nickel's marker and is deliberately not a hit, so the contract's 11 defaulted fields still pass. Verified in both directions: planting `doc = "planted"` in a positive fixture turns the self-test red (exit 1); removing it returns exit 0. 30 assertions. Ground truth for all of this came from the 1.18.0 source tarball via codeload, which is reachable; the release binary is not, so these were untestable locally. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .../invalid/L1-K9-S011-recipes-at-yard.k9.ncl | 2 +- .../fixtures/valid/hunt-fully-granted.k9.ncl | 2 +- 1-formats/k9/tools/k9-validate.sh | 35 +++++++++++++++++-- 3 files changed, 35 insertions(+), 4 deletions(-) diff --git a/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl b/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl index 0dc6fb025..6172adfac 100644 --- a/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl +++ b/1-formats/k9/tools/fixtures/invalid/L1-K9-S011-recipes-at-yard.k9.ncl @@ -20,7 +20,7 @@ K9! }, recipes = { - default = { recipe = "run" }, + default_recipe = { recipe = "run" }, run = { commands = ["echo 'this should never be reachable at Yard'"], }, diff --git a/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl b/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl index b48d1b21c..0cdb5e92f 100644 --- a/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl +++ b/1-formats/k9/tools/fixtures/valid/hunt-fully-granted.k9.ncl @@ -56,7 +56,7 @@ K9! }, recipes = { - default = { recipe = "deploy" }, + default_recipe = { recipe = "deploy" }, deploy = { description = "Apply the deployment.", commands = ["echo '[fixture] would deploy to %{config.target_dir}'"], diff --git a/1-formats/k9/tools/k9-validate.sh b/1-formats/k9/tools/k9-validate.sh index 2bfa86884..0b7aaa1b7 100755 --- a/1-formats/k9/tools/k9-validate.sh +++ b/1-formats/k9/tools/k9-validate.sh @@ -577,10 +577,15 @@ check_l2() { err K9-N001 L2 "library does not typecheck: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" fi else + # `k9_doc`, not `doc`: Nickel's lexer reserves `doc` (it is the metadata + # keyword in `x | doc "..."`), and its `Ident` production admits only `or`, + # `as` and `include` as contextual keywords. `let doc = ...` is a parse + # error at the identifier, which is what four positive controls died on. + # Keyword list: nickel 1.18.0 parser/src/lexer.rs. cat > "$drv_tmp" <&1)"; then err K9-N001 L2 "component does not satisfy K9.Component: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" @@ -822,6 +827,32 @@ EOF echo -e "${YEL}SKIP${NC} attribution assertions: $impostor not present" fi + echo "== no Nickel reserved word is used as an identifier ==" + # D173 gives the body to Nickel's grammar rather than restating it in an + # ABNF, which means Nickel's lexer is normative for identifiers and this + # validator cannot see a violation the way it sees a missing field. Two such + # violations cost CI runs to find: `let doc = ...` in the L2 driver, and a + # `default = { ... }` recipe field in two fixtures. Nickel's `Ident` + # production admits only `or`, `as` and `include` as contextual keywords, so + # every other keyword is unusable as a binding or field name. + # Keyword list: nickel 1.18.0 parser/src/lexer.rs. + local k9_kw='as default doc else false forall force fun if import in match merge nix not_exported null optional priority rec then true' + local kw_hits=0 kf k + for kf in "$CONTRACT" "$SCRIPT_DIR"/fixtures/valid/* "$SCRIPT_DIR"/fixtures/invalid/*; do + [ -f "$kf" ] || continue + case "$kf" in *.sh|*.adoc) continue ;; esac + for k in $k9_kw; do + # Field or binding position only: `| default = x` is Nickel's default + # marker and is correct, so a keyword preceded by `|` is not a hit. + if grep -qE "(^[[:space:]]*|[{(,][[:space:]]*)$k[[:space:]]*=[^=]" "$kf" \ + || grep -qE "\blet[[:space:]]+$k[[:space:]]*=" "$kf"; then + echo -e "${RED}FAIL${NC} $(basename "$kf") uses the Nickel keyword '$k' as an identifier" + kw_hits=$((kw_hits + 1)) + fi + done + done + t "the contract and all 26 fixtures avoid Nickel's reserved words" 0 "$kw_hits" + echo if [ $SELFTEST_FAILS -eq 0 ]; then echo -e "${GRN}self-test: all assertions passed${NC}" From 87a279efe366cd09c048650126ff1e2d2d5fc789 Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 4 Oct 2026 01:52:42 +0000 Subject: [PATCH 3/5] =?UTF-8?q?fix(k9):=20L2=20must=20evaluate,=20not=20on?= =?UTF-8?q?ly=20typecheck=20=E2=80=94=20contracts=20are=20runtime?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All five positive controls pass now. The two L2 negative controls were ACCEPTED, which is the finding that matters: FAIL L2-K9-N001-wrong-field-type.k9.ncl was ACCEPTED — the gate did not fire FAIL L2-K9-N001-two-segment-version.k9.ncl was ACCEPTED — the gate did not fire `nickel typecheck` is described by Nickel's own CLI as "typechecks the program but does not run it". A Nickel contract (`|`) is applied when a value flows through it, and a predicate contract has no static type to reason about — so `schema_version | std.contract.from_predicate (is_semver_of schema_major)` never fired, and `schema_version = "1.0"` sailed through. Same for `allow_network = "yes"`. check_l2 now runs `nickel export --format json` on the driver as well, since evaluation is what applies the contracts. Those two fixtures are the pair written specifically to prove L2 sees what L1 cannot; a validator that typechecked only was reporting the authority of a layer it was not performing — the exact defect class §12.3 is about, in this PR's own code. Libraries stay typecheck-only: they are imported rather than evaluated as components and may legitimately hold functions, which do not serialise. Spec gains §12.2 "L2 is two Nickel invocations, not one" and the K9-N001 row now names both. Cross-references re-verified by simulation: 87 numbered sections, 29 distinct §refs, none unresolved. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc | 20 +++++++++++++++++++- 1-formats/k9/tools/k9-validate.sh | 21 ++++++++++++++++++++- 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc b/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc index 23d9d9e65..7189ab6f8 100644 --- a/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc +++ b/1-formats/k9/spec/K9-CONTRACT-SPEC.adoc @@ -767,6 +767,24 @@ importer's enforced level. |L3 |Cryptographic |the signature verifies |an external verifier |=== +=== L2 is two Nickel invocations, not one + +`nickel typecheck` is described by Nickel's own CLI as _"typechecks the program +but does not run it"_. A Nickel contract (`|`) is applied when a value flows +through it, and a predicate contract — `std.contract.from_predicate +(is_semver_of schema_major)` is how §5.2's dot-triple rule is expressed — has no +static type for a checker to reason about. + +A reader MUST therefore both *typecheck* the body against `K9.Component` and +*evaluate* it, because evaluation is what applies the contracts. Typechecking +alone accepts `schema_version = "1.0"` and `allow_network = "yes"`, which are +exactly the two defects the L2 negative controls exist to catch; a validator +that ran only `typecheck` reported both as conforming. + +Libraries are the exception. A library is imported rather than evaluated as a +component, and it may legitimately contain functions, which have no serialisable +form. A library MUST be typechecked; it MUST NOT be required to export. + === Why the layers are separate Each layer has a different *authority*, and collapsing them is the failure @@ -1042,7 +1060,7 @@ violations, and this specification makes no claim about them. |K9-S012 |L0 |error |No envelope ⇒ no top-level `pedigree`. |K9-S013 |L1 |error |Every `import` resolves. |K9-S014 |L0/L1 |error |No leash claim outside `pedigree.security`. -|K9-N001 |L2 |error |The body satisfies `K9.Component` / library typecheck. +|K9-N001 |L2 |error |The body typechecks against `K9.Component` *and* evaluates without violating it; a library need only typecheck (§12.2). |K9-N002 |L2 |error |The normative contract itself typechecks. |K9-C001 |L3 |skip/error |Signature verification, where a verifier exists. |=== diff --git a/1-formats/k9/tools/k9-validate.sh b/1-formats/k9/tools/k9-validate.sh index 0b7aaa1b7..b5875c683 100755 --- a/1-formats/k9/tools/k9-validate.sh +++ b/1-formats/k9/tools/k9-validate.sh @@ -573,6 +573,11 @@ check_l2() { strip_envelope "$f" "$body_tmp" if [ "$DIALECT" = "library" ]; then + # Static check only. A library is imported, never evaluated as a + # component, and it may legitimately hold functions, which have no JSON + # representation — so `export` would fail on a conforming library. What a + # library must satisfy is the negative contract of §11 (no pedigree, no + # leash), which L1 already establishes lexically. if ! out="$("$nb" typecheck "$body_tmp" 2>&1)"; then err K9-N001 L2 "library does not typecheck: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" fi @@ -587,8 +592,22 @@ let K9 = import "$CONTRACT" in let k9_doc = import "./$(basename "$body_tmp")" in k9_doc | K9.Component EOF + # Two Nickel invocations, because they answer different questions. + # + # `typecheck` is documented in Nickel's own CLI as "typechecks the program + # but does not run it". A Nickel CONTRACT (`|`) is enforced when a value + # flows through it, and a predicate contract such as + # `std.contract.from_predicate (is_semver_of …)` has no static type the + # checker could reason about. Running only `typecheck` accepted both L2 + # negative controls — `schema_version = "1.0"` and `allow_network = "yes"` + # — which is precisely the pair written to prove L2 sees what L1 cannot. + # + # `export` evaluates, and evaluation is what applies the contracts. if ! out="$("$nb" typecheck "$drv_tmp" 2>&1)"; then - err K9-N001 L2 "component does not satisfy K9.Component: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" + err K9-N001 L2 "component does not typecheck against K9.Component: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" + fi + if ! out="$("$nb" export --format json "$drv_tmp" 2>&1 >/dev/null)"; then + err K9-N001 L2 "component violates the K9.Component contract: $(printf '%s' "$out" | head -n 5 | tr '\n' ' ')" fi fi rm -f "$body_tmp" "$drv_tmp" From 37b42e958fb638f4eccc3860844ae869ff217793 Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 4 Oct 2026 01:56:53 +0000 Subject: [PATCH 4/5] fix(k9): std.string.substring takes an END index, not a length MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With L2 evaluating, the contracts fire — and `is_semver_of` rejected "1.0.0", failing all four component positive controls: contract broken by the value of `schema_version` ┌─ k9_contract.ncl:394:22 Nickel 1.18.0's core/stdlib/std.ncl documents `substring start end str` — the slice from `start` (included) to `end` (excluded). The character walk called `substring i 1 s`, which returns "1" at i=0 by coincidence and "" at every later index, so the walk fell out at the second character and no version string could pass. Now `substring i (i + 1) s`. The other two calls are `substring 0 (length x) v` prefix slices, which the end-index reading makes correct as written. All nine std functions this contract uses were checked against 1.18.0's std.ncl, and all 23 call sites against those signatures: substring : Number -> Number -> String -> String split : String -> String -> Array String join : String -> Array String -> String string.length : String -> Number array.{length,any,filter}, record.has_field, contract.from_predicate The stdlib was read from the 1.18.0 source tarball over codeload, which is reachable; the release binary is not, so none of this was testable locally. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- 1-formats/k9/spec/contract/k9_contract.ncl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/1-formats/k9/spec/contract/k9_contract.ncl b/1-formats/k9/spec/contract/k9_contract.ncl index 647f0bde1..be8736428 100644 --- a/1-formats/k9/spec/contract/k9_contract.ncl +++ b/1-formats/k9/spec/contract/k9_contract.ncl @@ -97,7 +97,14 @@ let is_semver_of = fun major v => if i >= std.string.length s then dots == 2 && seg_len > 0 else - let c = std.string.substring i 1 s in + # `substring start end str`, NOT (start, length, str): 1.18.0's + # std.ncl documents `substring start end str` as the slice from `start` + # (included) to `end` (excluded), so the single character at `i` is + # `substring i (i + 1) s`. Written as `substring i 1 s` it returned "1" + # at i=0 by coincidence and "" at every later index, so the walk fell + # out at the second character and `is_semver_of` rejected "1.0.0" — + # every positive control with it. Verified against core/stdlib/std.ncl. + let c = std.string.substring i (i + 1) s in if c == "." then seg_len > 0 && go (i + 1) (dots + 1) 0 false s else if is_digit c then @@ -106,6 +113,7 @@ let is_semver_of = fun major v => else false in + # A dot-triple is at least `want` plus "N.N": three more characters. std.string.length v >= (std.string.length want + 3) && std.string.substring 0 (std.string.length want) v == want && go 0 0 0 false v in From 76b841e40d441b04b80513f08ba08b49226cbe5c Mon Sep 17 00:00:00 2001 From: arena-agent Date: Sun, 4 Oct 2026 02:00:32 +0000 Subject: [PATCH 5/5] docs(k9): record what the first Nickel runs actually found MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit M7 said L2 had never run. It has now, in CI, and the result is recorded rather than left as a prediction: contract typecheck ok, 30-assertion self-test ok, fixtures 5 positive / 21 negative / 0 failures, corpus 5 conforming and 25 grandfathered. The corpus step is pinned to --layer L1 so it can run in a pre-commit hook, so the 25 grandfathered files have still never been through Nickel and M5's parse-error prediction is still a prediction. M7 is restated as that remaining work rather than as an unknown. A table records the seven defects the first Nickel runs found, all of them in this work's own code. Four are the same lesson — the contract and its driver were written against Nickel as remembered rather than Nickel as shipped. Three are gates that reported success without doing the work. The README's L2-controls section now says what they caught: L2 typechecked only, so both were accepted, and they are why L2 evaluates as well. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- 1-formats/k9/spec/MIGRATION-1058.adoc | 95 +++++++++++++++++++-------- 1-formats/k9/tools/README.adoc | 8 +++ 2 files changed, 76 insertions(+), 27 deletions(-) diff --git a/1-formats/k9/spec/MIGRATION-1058.adoc b/1-formats/k9/spec/MIGRATION-1058.adoc index fffecb9d6..484f36245 100644 --- a/1-formats/k9/spec/MIGRATION-1058.adoc +++ b/1-formats/k9/spec/MIGRATION-1058.adoc @@ -264,30 +264,36 @@ a component pedigree have different required fields for good reasons, and merging them to end a naming collision would be the naming collision winning. What M6 should do is make the relationship explicit in `SPEC.adoc`. -=== M7 — L2 has never actually run on this corpus +=== M7 — L2 on the corpus: still open, and now measurable *Rules cleared:* unknown until it runs · *ledger entries removed:* unknown -This is the honest gap in the work. `nickel` is not available in the -environment where this migration was prepared (the GitHub release-asset host is -unreachable from it), so **L2 has not been executed against the corpus or the -fixtures**. Everything asserted in this plan was asserted at L0/L1, plus the -self-test. +L2 has now run, but only over the **fixtures**. The result of the first run of +`K9-SVC Contractile Validation` with Nickel installed (run `37169542241`, +commit `37b42e9`): -The conformance suite is built so this cannot pass unnoticed: `--strict` exits -`3` with the message *"no nickel binary — L2 semantics were never checked, so -this run is not a conformance result"*, and the CI step runs `--strict` with -Nickel installed. The first CI run on a branch with Nickel will be the first -time K9 semantics have ever been checked in this repository. +---- +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 +---- + +The corpus step runs the local hook, which is pinned to `--layer L1` so it can +run in a pre-commit hook without a toolchain. So the 25 grandfathered files +have **still never been through Nickel**, and M5's prediction is untested: +`rhodium-standard-repositories/rsr-compliance-checklist.k9.ncl` opens with a +top-level *sequence of bindings*, which is not a Nickel term and should be a +parse error the moment anything typechecks it. -Expect it to find things. At minimum: +M7 is therefore: raise the corpus step to L2 for the five conforming files, +then work the ledger down. Expect each removal to need a real fix, not a +relabel. -* M5's top-level binding sequence is a Nickel parse error; -* the two `L2-K9-N001-*` negative fixtures become assertable (they are held to - be lexically clean by the runner today, which is the precondition for being - an L2 control at all); -* `nickel format --check` has never been run on any `.k9.ncl` body, and may - object to all of them. +Still never run anywhere: `nickel format --check` on a `.k9.ncl` body. +`ci-pipeline.yml` excludes that pathspec, and formatting is not reproducible +without the binary — so any M1–M6 change that adds a body will be the first +thing to discover what `nickel fmt` thinks of these files. == Suggested issue breakdown @@ -346,13 +352,48 @@ Every count and path in this plan was produced by running the tools named in it, in the repository, at the revision this plan was written against. The two exceptions are stated rather than hidden: -* *L2 (Nickel semantics) was not run.* No `nickel` binary was obtainable in the - preparation environment. See M7. -* *`nickel format --check` was not run*, for the same reason. It has never been - run on a `.k9.ncl` body in this repository, because `ci-pipeline.yml` - excludes that pathspec. +* *L2 (Nickel semantics) was not run where this plan was written.* No `nickel` + binary was obtainable in the preparation environment — the GitHub + release-asset host is TLS-refused from it, and `codeload` serves only the + source tarball with no `cargo` to build it. It has since been run in CI; see + M7 for what that found and what is still outstanding. +* *`nickel format --check` has still not been run*, anywhere, on a `.k9.ncl` + body. `ci-pipeline.yml` excludes that pathspec. + +What *was* run, and passed: the validator's 30-assertion self-test; the +conformance suite under Nickel (5 positive controls, 21 negative controls, all +21 rejected by their named rule at their named layer); the local hook in all +four ratchet paths; and the corpus baseline above. + +=== What the first Nickel runs found + +Seven defects, every one of them in this work's own code, and not one of them +visible without a `nickel` binary: + +[cols="1,3",options="header"] +|=== +|Defect |Effect +|`Record` used as a type |Not a Nickel type. The contract did not typecheck, so +every L2 verdict downstream was void and all five positive controls failed. +|`Any` used as its replacement |Also not a Nickel type; the dynamic type is +`Dyn`. Same failure, one run later. +|`let doc = …` in the L2 driver |`doc` is a Nickel keyword (the metadata +keyword in `x \| doc "…"`). Parse error at the identifier. +|`default = { … }` recipe fields in two fixtures |`default` is the +default-value marker keyword. Nickel's `Ident` admits only `or`, `as` and +`include` as contextual keywords. +|L2 ran only `nickel typecheck` |Documented as "typechecks the program but +does not run it". Contracts are applied when a value flows, so a predicate +contract never fired and *both L2 negative controls were accepted*. +|Negative-control 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` takes `(start, end, str)`, +not a length. It returned `""` at every index past 0, so `is_semver_of` +rejected `"1.0.0"` and every component positive control with it. +|=== -What *was* run, and passed: the validator's 26-assertion self-test; the -conformance suite (5 positive controls, 19 negative controls asserted, 2 L2 -controls held to be lexically clean); the local hook in all four ratchet paths; -and the corpus baseline above. +Four of the seven are the same lesson: the contract and its driver were written +against Nickel as remembered rather than Nickel as shipped. The other three are +gates that reported success without doing the work. diff --git a/1-formats/k9/tools/README.adoc b/1-formats/k9/tools/README.adoc index f6ba54bfa..f9402be88 100644 --- a/1-formats/k9/tools/README.adoc +++ b/1-formats/k9/tools/README.adoc @@ -112,6 +112,14 @@ the runner does not pretend to assert them: it verifies the half it *can* — that they are lexically clean, which is the precondition for being an L2 control at all — reports `SKIP`, and `--strict` refuses the run outright. +They have already earned their place. The first CI runs with Nickel installed +had L2 calling `nickel typecheck` only, which Nickel's own CLI documents as +*"typechecks the program but does not run it"*. Contracts are applied when a +value flows through them, so the predicate behind `schema_version` never fired +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. + == Byte-preserved fixtures `L0-K9-E003-crlf.k9.ncl` exists to be rejected for its line endings.