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/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/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/spec/contract/k9_contract.ncl b/1-formats/k9/spec/contract/k9_contract.ncl index c9d85c0e4..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 @@ -413,15 +421,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 ────────────────────────────────────────────── 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. 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..b5875c683 100755 --- a/1-formats/k9/tools/k9-validate.sh +++ b/1-formats/k9/tools/k9-validate.sh @@ -573,17 +573,41 @@ 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 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' ' ')" + 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" @@ -822,6 +846,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}"