fix(k9): make L2 real — seven defects the first Nickel runs found (#1058, D173) - #1145
Merged
Merged
Conversation
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>
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 9 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configuration
📒 Files selected for processing (8)
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 |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37168907268 K9 normative contract typecheckK9 contract self-testK9 conformance fixtures |
`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>
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37169159595 K9 normative contract typecheckK9 contract self-testK9 conformance fixtures |
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>
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37169337108 K9 normative contract typecheckK9 contract self-testK9 conformance fixtures |
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>
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37169542241 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
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>
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37169726396 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
|
hyperpolymath
changed the title
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
2 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.
K9-SVC contractile validationis green. Run37169542241, reconfirmed on76b841e: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
nickelbinary — which is not obtainable in the sandbox where this was written.Recordused as a typeAnyused as its replacementDyn. Same failure, one run later.let doc = …in the L2 driverdocis a Nickel keyword (metadata,x | doc "…"). Parse error at the identifier.default = { … }in two fixturesdefaultis the default-value marker keyword. Nickel'sIdentadmits onlyor,as,include.nickel typecheckschema_versionnever fired and both L2 negative controls were accepted.std.string.substring i 1 ssubstringis(start, end, str), not a length. It returned""past index 0, sois_semver_ofrejected"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.nickel export --format json) as well as typechecks — spec §12.2.errorwhose rule and layer match.K9 normative contract typecheckstep ahead of the fixtures, so a broken contract reports as a broken contract instead of five "non-conforming" files.doc = "planted"turns it red).Ground truth came from the 1.18.0 source tarball over
codeload, which is reachable:parser/src/lexer.rsfor the keyword list and theIdentproduction,core/stdlib/std.nclfor all ninestdsignatures this contract uses.Still open
The corpus step is pinned to
--layer L1so it can run in a pre-commit hook, so the 25 grandfathered files have never been through Nickel.nickel format --checkhas never run on a.k9.nclbody anywhere. Both are M7 inspec/MIGRATION-1058.adoc, which now records measured results instead of predictions.