Repository navigation
fix(k9): M1 contractile pedigrees + M2 PROTOCOL.k9 rename (#1058) - #1149
Merged
Merged
Conversation
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 22 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configuration
📒 Files selected for processing (33)
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/37262479888 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
Owner
Author
|
Note for whoever merges the #A–#E batch: PR #1148 (#C) also edits |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37262876162 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
hyperpolymath
changed the title
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37263079909 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37263205797 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37263947191 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37264039138 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37264301468 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37264400793 K9 fmt probe (temporary)diff (unformatted -> formatted)--- 1-formats/k9/spec/contract/k9_contract.ncl 2026-10-05 04:38:36.445798949 +0000
+++ /dev/fd/63 2026-10-05 04:38:41.300978720 +0000
@@ -1,509 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-#
-# k9_contract.ncl — THE NORMATIVE K9 COMPONENT CONTRACT (v1.0.0).
-#
-# Ruling D173 (standards#1058, 2026-09-30): "K9 needs a Nickel contract, not an
-# ABNF." This file is that contract. It is normative; the prose that governs it
-# is ../K9-CONTRACT-SPEC.adoc, and where the two disagree the prose wins and
-# this file is a bug.
-#
-# WHAT THIS FILE IS
-# The closed, versioned, machine-checkable shape of a K9 component's
-# `pedigree` block, plus the decision functions a host must consult before
-# it lets a component do anything:
-#
-# leash_levels / is_leash §7 the leash taxonomy as a CLOSED set
-# required_capabilities §8 what a security flag costs you
-# granted_ok / denied §8 default-deny capability arithmetic
-# authorize_hunt §9 all five preconditions, always
-# signature_verdict §10 presence is NOT verification
-#
-# WHAT THIS FILE IS NOT
-# * It is not a grammar. K9 has no syntax of its own: the body of a
-# `.k9.ncl` file is a Nickel term and Nickel's grammar is normative by
-# reference (K9-CONTRACT-SPEC §3.5). Re-specifying it here, in ABNF or
-# otherwise, would fork a language we do not own.
-# * It is not a validator. A contract states what holds; the canonical
-# validator (../../tools/k9-validate.sh) decides whether a check could be
-# run at all, and reports a check it could not run as SKIPPED rather than
-# as a pass.
-# * It does not verify signatures. Nickel has no cryptographic primitive,
-# so nothing in this file can produce `signature_check = 'Passed`. See
-# §10: an implementation that has not run a verifier MUST report 'Not_Run,
-# and 'Not_Run can never authorise Hunt.
-#
-# NAMING HAZARD — carried from SPEC.adoc, unchanged:
-# K9's execution triad is must / just / nickel.
-# The contractiles family is must / trust / dust / intend.
-# `must` appears in both and means different things. Never conflate them.
-# Nothing in this file names a contractile verb; a contractile component is
-# an ordinary K9 component whose `component_type` begins "contractile:".
-#
-# API SURFACE DISCIPLINE
-# Every std function used below is one already exercised by a `.ncl` file
-# this repository typechecks in CI (capabilities.ncl, leash.ncl,
-# pedigree.ncl): std.string.length, std.string.substring, std.string.split,
-# std.string.join, std.array.length, std.array.any, std.array.filter,
-# std.record.has_field, std.contract.from_predicate. A normative artefact
-# must not be the first thing in the estate to touch an unexercised corner
-# of a dependency's standard library.
-#
-# ─────────────────────────────────────────────────────────────────────────
-# Type aliases (top-level `let` — the idiom pedigree.ncl and leash.ncl use)
-# ─────────────────────────────────────────────────────────────────────────
-
-# §7 — the leash taxonomy. CLOSED: three members, and adding a fourth is a
-# MAJOR change to this contract, not an extension.
-let SecurityLevel = [| 'Kennel, 'Yard, 'Hunt |] in
-
-# §10 — the result of an attempted cryptographic check. 'Not_Run is the honest
-# default and it is load-bearing: it is the value a validator reports when no
-# verifier was available, and it must never be silently upgraded.
-let SignatureCheck = [| 'Not_Run, 'Passed, 'Failed |] in
-
-# §10 — what a host may infer from "does the file carry a signature block"
-# (lexical) combined with "did a verifier accept it" (cryptographic).
-let SignatureVerdict = [| 'Absent, 'Present_Unverified, 'Verified, 'Rejected |] in
-
-# §8.1 — the reserved extension namespace prefix.
-let ExtensionPrefix = "x-" in
-
-# ─────────────────────────────────────────────────────────────────────────
-# §5.2 / §8.1 — name shapes, using nothing beyond length and substring
-# ─────────────────────────────────────────────────────────────────────────
-
-let is_digit = fun c =>
- c == "0"
- || c == "1"
- || c == "2"
- || c == "3"
- || c == "4"
- || c == "5"
- || c == "6"
- || c == "7"
- || c == "8"
- || c == "9" in
-
-# A numeric dot-triple whose MAJOR segment equals `major`. Walks the string
-# once. Rejects: non-digits, a leading or trailing dot, an empty segment, a
-# leading zero in any segment ("1.00.0"), and the wrong number of segments.
-#
-# `prev_dot` starts TRUE so a leading "." is refused by the same branch that
-# refuses ".."; `seg_len` must end > 0 so a trailing "." is refused too.
-let is_semver_of = fun major v =>
- let want = major ++ "." in
- let rec go = fun i dots seg_len first_zero s =>
- if i >= std.string.length s then
- dots == 2 && seg_len > 0
- else
- # `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
- (first_zero == false || seg_len == 0)
- && go (i + 1) dots (seg_len + 1) (c == "0") s
- 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
-
-# ─────────────────────────────────────────────────────────────────────────
-# The contract record. Nickel records are recursive, so fields below refer to
-# their siblings by name; the type aliases above stay top-level so no field
-# ever shadows the binding it is defined in terms of.
-# ─────────────────────────────────────────────────────────────────────────
-{
- # ── §5 Identity and versioning ───────────────────────────────────────
- #
- # `contract_version` is the version of THIS file. `schema_major` is the
- # major segment a conforming component's `pedigree.schema_version` must
- # carry to be readable by this contract. They are separate numbers on
- # purpose: this contract can be revised (1.0.0 -> 1.0.1) without changing
- # what a component must look like.
- contract_name = "k9-svc-component",
- contract_version = "1.0.0",
- schema_major = "1",
-
- # §4 — the dialects a K9 envelope may carry. A file whose body is not one of
- # these is not a K9 file, whatever its suffix says.
- dialect = {
- # `K9!` envelope + Nickel body declaring a `pedigree`. In scope here.
- component = "k9-svc-component",
- # No `K9!` envelope, Nickel body, no top-level `pedigree`. Imported, never
- # executed. In scope for §11 only.
- library = "k9-svc-library",
- # `K9!` envelope + YAML body. Governed by
- # 2-protocols/k9-coordination/spec/abnf/coordination-k9-grammar_v1.1.abnf,
- # NOT by this contract. Named here so a validator can route it instead of
- # misreporting it as a broken component.
- coordination = "k9-coordination",
- },
-
- # ── §7 Leash taxonomy — CLOSED SET ───────────────────────────────────
- #
- # Machine-checkable enumeration of the three levels in ascending order of
- # what they permit. This list IS the closed set the prose promises, and it
- # lives in the same file as the `SecurityLevel` enum it mirrors so the two
- # cannot drift silently; the conformance suite asserts they agree.
- leash_levels = ['Kennel, 'Yard, 'Hunt],
-
- # Total order over the closed set. Used for the monotonicity rule (§7.4): a
- # host may enforce a level STRICTER than the component declares, never laxer.
- level_rank = fun l =>
- if l == 'Kennel then
- 0
- else if l == 'Yard then
- 1
- else
- 2,
-
- is_leash = fun v =>
- std.array.length (std.array.filter (fun l => l == v) leash_levels) == 1,
-
- # The leash a component DECLARES. Fail-closed: a pedigree with no readable
- # `security.leash` ranks as 'Kennel here, and is rejected outright by the
- # Pedigree contract below. This helper exists so a host handed a partial
- # pedigree cannot crash on it.
- leash_of = fun pedigree =>
- if std.record.has_field "security" pedigree
- && std.record.has_field "leash" pedigree.security
- then
- pedigree.security.leash
- else
- 'Kennel,
-
- # ── §8 Capability model — DEFAULT-DENY ───────────────────────────────
- #
- # §8.1 CLOSED CORE SET. Exhaustive for the core namespace. Adding or
- # removing a name here is a MAJOR change to this contract.
- core_capabilities = [
- "fs.read",
- "fs.write",
- "net.fetch",
- "process.spawn",
- "container.run",
- "secret.read",
- "deploy.apply",
- "rollback.apply",
- ],
-
- # §8.1 RESERVED EXTENSION NAMESPACE. Non-core names MUST be "x-<vendor>.<p>"
- # so they can never collide with a future core name.
- extension_prefix = ExtensionPrefix,
-
- is_core = fun name => std.array.any (fun c => c == name) core_capabilities,
-
- # A well-formed extension: starts with the prefix and has at least one "."
- # after the vendor segment, i.e. "x-vendor.something", never bare "x-vendor".
- is_extension = fun name =>
- std.string.length name > std.string.length ExtensionPrefix
- && std.string.substring 0 (std.string.length ExtensionPrefix) name
- == ExtensionPrefix
- && std.array.length (std.string.split "." name) >= 2,
-
- Capability = std.contract.from_predicate (fun name =>
- is_core name || is_extension name
- ),
-
- # An explicit allow-list. DEFAULT-DENY is expressed by the empty grant: it
- # permits nothing, and "nothing" is the correct answer for an absent grant.
- CapabilityGrant = Array Capability,
-
- default_grant = [],
-
- permits = fun grant name => std.array.any (fun g => g == name) grant,
-
- denied = fun grant requested =>
- std.array.filter (fun r => !(permits grant r)) requested,
-
- granted_ok = fun grant requested =>
- std.array.length (denied grant requested) == 0,
-
- # §8.4 DERIVED REQUIREMENTS — the rule that makes the grant load-bearing.
- #
- # A security flag is a REQUEST for a capability, and a request the grant
- # does not cover is a contradiction inside the pedigree, not a preference.
- # `allow_network = true` with an empty grant is therefore INVALID, not
- # merely unwise: the component asks for the network while granting itself
- # nothing. This STRENGTHENS the pre-#1058 state, where the flags and the
- # grant were two unrelated opinions in the same block.
- required_capabilities = fun security =>
- (
- if std.record.has_field "allow_network" security
- && security.allow_network
- then
- ["net.fetch"]
- else
- []
- )
- @ (
- if std.record.has_field "allow_filesystem_write" security
- && security.allow_filesystem_write
- then
- ["fs.write"]
- else
- []
- )
- @ (
- if std.record.has_field "allow_subprocess" security
- && security.allow_subprocess
- then
- ["process.spawn"]
- else
- []
- ),
-
- # What the grant fails to cover. Empty iff the pedigree is self-consistent.
- grant_deficit = fun grant security =>
- denied grant (required_capabilities security),
-
- # ── §9 Hunt preconditions — ALL FIVE, ALWAYS ─────────────────────────
- #
- # Owner directive 2026-06-03, restated and NOT RELAXED by this contract:
- # Hunt requires all five, always. There is no configurable subset, and a
- # valid signature alone is not sufficient. Reproduced from leash.ncl
- # verbatim so the two cannot drift; the conformance suite asserts equality.
- hunt_preconditions = [
- "signature",
- "policy",
- "sandbox",
- "dry_run",
- "capability_grant",
- ],
-
- # The host supplies one Bool of EVIDENCE per precondition. Evidence is
- # runtime fact, not a static component field — which is why `check_level`
- # in leash.ncl can never authorise Hunt on its own.
- # Host-side, and deliberately CLOSED unlike the component-facing records
- # above: §9.2 says the host supplies one Boolean of evidence per
- # precondition, so a misspelt evidence field must be an error rather than a
- # silently ignored precondition. §5.5's openness is about a *component's*
- # fields.
- HuntEvidence = {
- signature | Bool,
- policy | Bool,
- sandbox | Bool,
- dry_run | Bool,
- capability_grant | Bool,
- },
-
- # §9.2 The gate. Identical semantics to leash.ncl `authorize_hunt`, and
- # deliberately so: a host implementing this file and a host implementing
- # leash.ncl must reach the same verdict on the same evidence.
- authorize_hunt = fun evidence =>
- let unmet =
- (if evidence.signature then [] else ["signature"])
- @ (if evidence.policy then [] else ["policy"])
- @ (if evidence.sandbox then [] else ["sandbox"])
- @ (if evidence.dry_run then [] else ["dry_run"])
- @ (if evidence.capability_grant then [] else ["capability_grant"])
- in
- if std.array.length unmet == 0 then
- {
- permitted = true,
- enforced_level = 'Hunt,
- unmet_preconditions = [],
- }
- else
- {
- permitted = false,
- enforced_level = 'Yard,
- reason =
- "Hunt requires all five preconditions; unmet: "
- ++ std.string.join ", " unmet,
- unmet_preconditions = unmet,
- },
-
- # ── §10 Signature semantics — PRESENCE IS NOT VERIFICATION ───────────
- #
- # A `signature` block in a pedigree is a CLAIM. Reading it proves the file
- # says it was signed. It does not prove the file was signed, and it does not
- # prove the signature covers the bytes about to be executed.
- signature_checks = ['Not_Run, 'Passed, 'Failed],
- signature_verdicts = ['Absent, 'Present_Unverified, 'Verified, 'Rejected],
-
- # §10.2 — the only mapping a conforming implementation may make.
- # no block -> 'Absent (nothing was claimed)
- # block, verifier passed -> 'Verified (cryptographic fact)
- # block, verifier rejected -> 'Rejected (cryptographic fact)
- # block, no verifier ran -> 'Present_Unverified (lexical fact ONLY)
- #
- # Note what is absent from that table: there is no input that turns
- # 'Not_Run into 'Verified. An implementation cannot infer verification from
- # presence, and a validator that reports 'Verified without having run a
- # verifier is non-conforming (§10.3).
- signature_verdict = fun has_block check =>
- if has_block == false then
- 'Absent
- else if check == 'Passed then
- 'Verified
- else if check == 'Failed then
- 'Rejected
- else
- 'Present_Unverified,
-
- # §10.4 — the Hunt `signature` precondition is satisfiable by 'Verified and
- # by nothing else. Presence yields 'Present_Unverified, which is false here.
- # This is the line that stops a lexical check from becoming an execution
- # licence, and it is the reason this contract cannot be replaced by a grep.
- hunt_signature_evidence = fun verdict => verdict == 'Verified,
-
- # The signature block a component MAY carry. Every field but `algorithm` is
- # optional at the CONTRACT level, because §10.1 makes presence a per-leash
- # rule rather than a universal one: 'Kennel and 'Yard components are
- # ordinarily unsigned, and that is correct rather than a defect.
- Signature = {
- algorithm | String | default = "Ed25519",
- public_key | String | optional,
- signature | String | optional,
- payload_hash | String | optional,
- signed_at | String | optional,
- key_id | String | default = "primary",
- # §5.5 — unknown fields are PERMITTED; see the `..` block above `Metadata`.
- # A host that reads `signature.public_key` MUST NOT be the reason a future
- # `counter_signature` field is rejected.
- ..
- },
-
- # ── §6 The component pedigree, v1 ────────────────────────────────────
- #
- # Field-for-field this is the shape the estate's `.k9.ncl` components
- # actually carry (`.machine_readable/svc/k9/template-*.k9.ncl`), with two
- # normative tightenings: `component_type` is REQUIRED (§6.2), and the
- # security flags must be paid for in the capability grant (§8.4).
- #
- # ── THE `..` TAIL, AND WHY EVERY COMPONENT-FACING RECORD HERE HAS ONE ──
- #
- # §5.5's table ends with "Unknown fields anywhere | PERMITTED. A reader SHOULD
- # report them and MUST NOT consult them to relax any requirement of §8 or §9."
- # That is normative prose, and by this file's own first rule the prose wins:
- # where the two disagree, this file is the bug.
- #
- # They disagreed until 2026-10-05. A Nickel record contract is CLOSED by
- # default — the sharp edge is recorded in Nickel's own integration suite,
- # core/tests/integration/inputs/contracts/record_contract_extra_field.ncl,
- # which asserts `EvalError::BlameError` with the message "extra field" and
- # advises appending `, ..`. So a component carrying a legitimate extension
- # field was blamed by this file while §5.5 permitted the field. The six
- # `.machine_readable/contractiles/*/*.k9.ncl` components are the live case
- # (they keep `semantics`, `contractile_verb`, `tier`, `authority`,
- # `variance_schema`, `execution`, `failure_mode_defenses` in the pedigree;
- # `probe_scope`, `probe_kinds_*`, `allow_filesystem_write_conditional` in
- # security; `paired_xfile`, `paired_runner` in metadata), and
- # `2-protocols/axel/config/*.k9.ncl` keep their payload at top level.
- #
- # Opening these five records is a CONFORMANCE fix, not a contract revision:
- # the specified contract (the prose) never changed, so `contract_version`
- # stays 1.0.0. It does not weaken §8 or §9 either — §5.5's own last clause
- # forbids that, and the validator enforces the capability arithmetic over the
- # extracted facts whatever an extension field claims (K9-S007, K9-S008).
- #
- # The positive control `tools/fixtures/valid/extension-fields.k9.ncl` exists
- # so this cannot silently regress: it fails at L2 the moment any of these
- # records closes again.
-
- Metadata = {
- name | String,
- version | String | default = "0.0.0",
- description | String | optional,
- author | String | optional,
- # §5.5 — see the block comment above. The estate's contractiles add
- # `paired_xfile` / `paired_runner` here.
- ..
- },
-
- Security = {
- # §7 — closed set. An unknown LEASH TAG is a contract violation, not a
- # warning; an unknown FIELD in this block is §5.5's business.
- leash | SecurityLevel,
- trust_level | String | default = "unset",
- allow_network | Bool | default = false,
- allow_filesystem_write | Bool | default = false,
- allow_subprocess | Bool | default = false,
- # §10.1 — REQUIRED to be true when leash == 'Hunt. The validator enforces
- # the implication; this contract cannot, because it is a cross-field rule.
- signature_required | Bool | default = false,
- # §8.3 — the explicit grant. Default-deny: absent means empty.
- capabilities | CapabilityGrant | default = [],
- # §5.5 — unknown fields are PERMITTED, and the prose names this block's own
- # examples: "the estate's contractiles use `probe_scope` and
- # `authorised_probes_only`". No conforming reader may let one of them
- # weaken §8 or §9 — the grant above is what a host enforces.
- ..
- },
-
- Pedigree = {
- # §5.2 — a numeric dot-triple whose major segment equals `schema_major`.
- # A component from another major is not "older"; it is unreadable, and
- # must be refused rather than guessed at (§5.4).
- schema_version | std.contract.from_predicate (is_semver_of schema_major),
- # §6.2 — REQUIRED: what this component IS. A template placeholder is not
- # a value; the canonical validator rejects "TODO" here at L1.
- component_type | String,
- security | Security,
- metadata | Metadata,
- # §6.5 — advisory to a reader, mandatory to declare. A 'Hunt component
- # with an empty side_effects list claims full system access and describes
- # none of it, which the validator rejects at L1.
- warnings | Array String | default = [],
- side_effects | Array String | default = [],
- # §10.1 — the signature claim. Presence is per-leash; see Signature above.
- signature | Signature | optional,
- # §5.5 — unknown fields are PERMITTED. This is the line MIGRATION-1058 M1
- # turned on: the contractile family keeps its own vocabulary in the pedigree
- # (`semantics`, `contractile_verb`, `tier`, `authority`, `variance_schema`,
- # `execution`, `failure_mode_defenses`), and nothing in this file may force
- # those names out of it.
- ..
- },
-
- # The whole component: the pedigree plus the optional Nickel payload.
- # `config`, `recipes` and `validation` stay open on purpose — they are the
- # component's own business — but §6.7 makes one thing non-negotiable: a
- # non-empty `recipes` block is an execution surface and therefore forces
- # 'Hunt. The validator enforces that; this contract only shapes the blocks.
- Component = {
- pedigree | Pedigree,
- # 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,
- # §5.5 — unknown fields are PERMITTED at top level too, which is the case
- # MIGRATION-1058 M4 recorded for whoever first ran the corpus at L2:
- # `2-protocols/axel/config/*.k9.ncl` keep their payload (`ci`, `local_dev`,
- # `quality`; `metadata.k9.ncl`: `project`, `tech_stack`, `deployment`,
- # `features`, `status`) beside `pedigree`.
- ..
- },
-
- # ── §11 Library dialect ──────────────────────────────────────────────
- #
- # A library is imported; it is never executed as a component and never
- # carries an envelope. The contract it must satisfy is the negative one:
- # no pedigree, no leash claim, no execution licence of any kind.
- is_library = fun lib =>
- !(std.record.has_field "pedigree" lib)
- && !(std.record.has_field "leash" lib),
-}formatted file, base64 -w 100idempotenceK9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37264538561 K9 fmt probe (temporary)nickel format --help (first lines) |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37264691994 K9 fmt probe (temporary)formatted bytes / sha256diff (unformatted -> formatted)--- 1-formats/k9/spec/contract/k9_contract.ncl 2026-10-05 04:42:38.189676676 +0000
+++ /home/runner/work/_temp/formatted.ncl 2026-10-05 04:42:43.295666817 +0000
@@ -72,18 +72,18 @@
# ─────────────────────────────────────────────────────────────────────────
# §5.2 / §8.1 — name shapes, using nothing beyond length and substring
# ─────────────────────────────────────────────────────────────────────────
-
let is_digit = fun c =>
c == "0"
- || c == "1"
- || c == "2"
- || c == "3"
- || c == "4"
- || c == "5"
- || c == "6"
- || c == "7"
- || c == "8"
- || c == "9" in
+ || c == "1"
+ || c == "2"
+ || c == "3"
+ || c == "4"
+ || c == "5"
+ || c == "6"
+ || c == "7"
+ || c == "8"
+ || c == "9"
+in
# A numeric dot-triple whose MAJOR segment equals `major`. Walks the string
# once. Rejects: non-digits, a leading or trailing dot, an empty segment, a
@@ -109,14 +109,15 @@
seg_len > 0 && go (i + 1) (dots + 1) 0 false s
else if is_digit c then
(first_zero == false || seg_len == 0)
- && go (i + 1) dots (seg_len + 1) (c == "0") s
+ && go (i + 1) dots (seg_len + 1) (c == "0") s
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
+ && std.string.substring 0 (std.string.length want) v == want
+ && go 0 0 0 false v
+in
# ─────────────────────────────────────────────────────────────────────────
# The contract record. Nickel records are recursive, so fields below refer to
@@ -177,8 +178,7 @@
# pedigree cannot crash on it.
leash_of = fun pedigree =>
if std.record.has_field "security" pedigree
- && std.record.has_field "leash" pedigree.security
- then
+ && std.record.has_field "leash" pedigree.security then
pedigree.security.leash
else
'Kennel,
@@ -208,13 +208,13 @@
# after the vendor segment, i.e. "x-vendor.something", never bare "x-vendor".
is_extension = fun name =>
std.string.length name > std.string.length ExtensionPrefix
- && std.string.substring 0 (std.string.length ExtensionPrefix) name
- == ExtensionPrefix
- && std.array.length (std.string.split "." name) >= 2,
-
- Capability = std.contract.from_predicate (fun name =>
- is_core name || is_extension name
- ),
+ && std.string.substring 0 (std.string.length ExtensionPrefix) name == ExtensionPrefix
+ && std.array.length (std.string.split "." name) >= 2,
+
+ Capability =
+ std.contract.from_predicate (fun name =>
+ is_core name || is_extension name
+ ),
# An explicit allow-list. DEFAULT-DENY is expressed by the empty grant: it
# permits nothing, and "nothing" is the correct answer for an absent grant.
@@ -241,28 +241,25 @@
required_capabilities = fun security =>
(
if std.record.has_field "allow_network" security
- && security.allow_network
- then
+ && security.allow_network then
["net.fetch"]
else
[]
)
- @ (
- if std.record.has_field "allow_filesystem_write" security
- && security.allow_filesystem_write
- then
- ["fs.write"]
- else
- []
- )
- @ (
- if std.record.has_field "allow_subprocess" security
- && security.allow_subprocess
- then
- ["process.spawn"]
- else
- []
- ),
+ @ (
+ if std.record.has_field "allow_filesystem_write" security
+ && security.allow_filesystem_write then
+ ["fs.write"]
+ else
+ []
+ )
+ @ (
+ if std.record.has_field "allow_subprocess" security
+ && security.allow_subprocess then
+ ["process.spawn"]
+ else
+ []
+ ),
# What the grant fails to cover. Empty iff the pedigree is self-consistent.
grant_deficit = fun grant security =>
@@ -304,10 +301,10 @@
authorize_hunt = fun evidence =>
let unmet =
(if evidence.signature then [] else ["signature"])
- @ (if evidence.policy then [] else ["policy"])
- @ (if evidence.sandbox then [] else ["sandbox"])
- @ (if evidence.dry_run then [] else ["dry_run"])
- @ (if evidence.capability_grant then [] else ["capability_grant"])
+ @ (if evidence.policy then [] else ["policy"])
+ @ (if evidence.sandbox then [] else ["sandbox"])
+ @ (if evidence.dry_run then [] else ["dry_run"])
+ @ (if evidence.capability_grant then [] else ["capability_grant"])
in
if std.array.length unmet == 0 then
{
@@ -321,7 +318,7 @@
enforced_level = 'Yard,
reason =
"Hunt requires all five preconditions; unmet: "
- ++ std.string.join ", " unmet,
+ ++ std.string.join ", " unmet,
unmet_preconditions = unmet,
},
@@ -505,5 +502,5 @@
# no pedigree, no leash claim, no execution licence of any kind.
is_library = fun lib =>
!(std.record.has_field "pedigree" lib)
- && !(std.record.has_field "leash" lib),
+ && !(std.record.has_field "leash" lib),
}formatted file, base64 -w 100idempotenceK9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
MIGRATION-1058 M2 offered two outcomes: (a) rename the twelve 3-practice/session-management-standards/*/*/PROTOCOL.k9 stubs to PROTOCOL.yaml, or (b) give them a K9 envelope and a registered dialect. Ruling: (a). They are plain YAML session-management contracts that no K9 host loads; (b) would invent a dialect to preserve a naming collision. - git mv all 12 PROTOCOL.k9 -> PROTOCOL.yaml (contents otherwise unchanged) - add MPL-2.0 SPDX headers to the 11 that lacked one: *.yaml is inside .githooks/validate-spdx.sh's scope, the .k9 suffix was not - shrink .machine_readable/k9-contract-debt.txt: 17 -> 5 entries - repoint the scorecard's dead 1-formats/k9/actions/validate/validate-k9.sh path at 1-formats/k9/tools/k9-validate.sh; re-grade S1 as pass on the extension-reservation rule with an executable check; refresh the M1-M4 and S4 suffix/line-count references - update README Protocol File Contract, substantial-completion CHECKLIST, K9-CONTRACT-SPEC 4.2 (also fixes its "migration item M4" -> M2), MIGRATION-1058 M2 (ruling recorded), and the k9-contractile CI comment - regenerate REGISTRY.a2ml (source_hash covers the home) and the derived COMPLIANCE-DASHBOARD.adoc; the regeneration also clears 3 pre-existing registry drifts (1-formats/k9, 2-protocols/axel, form-fill-provenance) Clears K9-E005 x12 and K9-E004 x11; no session-management path is in the hook's violation list any more, stale-ledger is 0, and the 8 remaining violations are the pre-existing contractile/Axel items owned by #A/#C/#D. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
The six contractile components imported `../k9/template-hunt.k9.ncl`, which does not exist (there is no k9/ subdirectory under .machine_readable/contractiles/), so K9-S013 fired and the pedigree a reviewer read was not the one a host would evaluate. They now merge `base.pedigree_schema` from ../_base.ncl and declare the §5.5 core: schema_version, `component_type = "contractile:<verb>"`, semantics and security (the §8.4 capabilities that pay for each allow_* flag). Leash discipline is unchanged: adjust and dust are 'Yard (config-only substrate, §7.3 caps); bust, intend, must and trust are 'Hunt. The four Hunt components gain the §6.5/§9 material they need to be evaluated — signature_required, a signature block (verdict 'Present_Unverified, per §10.2/§10.4; not yet authorised to run) and 3 irreducible side_effects. variance_schema is marked `not_exported`: its fields are contract declarations with no definitions, which Nickel's export refuses to serialize. Naming: the `contractile:` component_type prefix is the sole tie between the contractile family (must/trust/dust/intend) and K9's execution triad (must/just/nickel). The K9 contract never names a contractile verb, so DEED translation renames nothing. Ref #1058 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Two paragraphs of K9-CONTRACT-SPEC still described the six contractiles as broken, and one of them named the wrong migration item: * §11.2 claimed all six carried a pedigree "and no envelope"; the envelope was already line 1 of all six when that was checked against the tree, so K9-S012 never had a live instance. The paragraph described the pre-envelope revision and is now marked resolved, pointing at what actually remained (component_type, the §8.4 grant, and the §6.5/§9 Hunt material). * §11.4 claimed all six imported "../k9/template-hunt.k9.ncl" and were a live K9-S013 instance. The import now resolves to ../_base.ncl, so the paragraph is recorded as fixed rather than live. MIGRATION-1058 gains "M1 — resolved (2026-10-05)" in the shape M2/M3/M4 used: the three corrections (envelope already present, the import's real source, the ledger's entries already removed), the naming resolution stated in full (the `contractile:` component_type prefix is the entire tie between the contractiles family and K9's execution triad, so DEED translation renames nothing), the 'Yard request-vs-permission reading for adjust/dust, and the L2 caveat this item does not close: §5.5 permits the contractiles' extension fields but the contract's record contracts are closed by default, so the corpus-at-L2 item (#F/M7) needs a `..` tail on Component/Pedigree/Security. Ref #1058 (M1 · #A). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…ity (#1058) The note recorded in 47751ee named "top-level variance_schema" as an extra field on Component. Reading the six files' structure rather than their reports: nothing is top-level but `pedigree`, and every contractile field is inside it — pedigree.semantics/contractile_verb/tier/authority/ variance_schema/execution/failure_mode_defenses, and security.probe_scope/probe_kinds_*/allow_filesystem_write_conditional. An L2 pass would blame Pedigree and Security, not Component (Component is M4's note, for components that keep a payload at top level). Naming the fields correctly matters to whoever picks up #F/M7 and has to make the blame go away. Ref #1058 (M1 · #A). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
§5.5's table ends with "Unknown fields anywhere | PERMITTED". The machine-readable contract did not implement that: Component, Pedigree, Metadata, Security and Signature in k9_contract.ncl were plain Nickel record contracts, which are CLOSED by default, so any component carrying a legitimate extension field was blamed with "extra field" — the sharp edge Nickel records in its own suite as core/tests/integration/inputs/contracts/record_contract_extra_field.ncl. The live cases are the six `.machine_readable/contractiles/*/*.k9.ncl` components (pedigree.tier/authority/semantics/contractile_verb/ variance_schema/execution/failure_mode_defenses, security.probe_scope/ probe_kinds_*/allow_filesystem_write_conditional, metadata.paired_xfile/ paired_runner) and the two `2-protocols/axel/config/*.k9.ncl` files, which keep their payload at top level. Both were recorded as M7's problem by MIGRATION-1058 M1 and M4 — this is that fix. The five records now take a `, ..` tail. By the contract's own first rule — the prose wins and the file is the bug — this is a conformance fix, not a contract revision, so `contract_version` stays 1.0.0. It relaxes nothing in §8 or §9: §5.5 forbids consulting an unknown field to grant access, and the validator's capability arithmetic still runs over the extracted facts. HuntEvidence stays closed on purpose (host-side evidence, §9.2). New positive control `tools/fixtures/valid/extension-fields.k9.ncl`, shaped like a contractile: extension fields at four levels plus a declaration-only `variance_schema` marked `not_exported`, so L2 exercises `nickel export` too, not only the typecheck. It fails the moment any of the tails is removed, which is what nothing in the suite could do before. Suite is now 6 positive / 21 negative; the self-test's keyword-scan label (hardcoded count) follows. CI: the corpus step now sets K9_VALIDATE_LAYER=all, so the whole corpus is checked at L2 where the pinned binary is installed. The pre-commit hook keeps its L1 default — a hook that fails on a laptop without a toolchain is a hook people bypass — and ledger entries stay advisory at either layer. This is MIGRATION-1058 M7's first step: the five grandfathered files are reported, not failed, and still need their own items (M3, M5). Verification here is L1-only by construction: no nickel binary is obtainable in this environment (release-asset host TLS-refused; MIGRATION-1058 §L2 records the limitation). `--self-test` all assertions passed; `--fixtures` 6 positive, 21 negative; the hook is clean at L1 and reports 5 grandfathered at L2. The L2 verdict itself is CI's to give, which is the point of raising the layer there. Ref #1058 (M1 · #A follow-up, M4 · #D follow-up, M7 · #F started). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
`source_hash` is sha256 over `git ls-files -s <home>`, so two homes moved:
* `1-formats/k9/` — the new positive control
`tools/fixtures/valid/extension-fields.k9.ncl`;
* `2-protocols/axel/` — M4's pedigree fix (`leash` moved under
`pedigree.security`), which was cherry-picked onto this branch with the
release-pre-flight scorecard but not with a registry regeneration.
`bash scripts/build-registry.sh --check` now passes, as do
`build-scorecards.sh --check --strict` and a link-rot diff against the
pre-change tree (the two `{contract-file}` findings on K9-CONTRACT-SPEC
predate this branch).
Ref #1058.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
`nickel format --check` has failed on this file in ci-pipeline.yml since it landed — on main (`a41f369`) as much as on this branch, which the Nickel job's annotations show. No `nickel` binary is obtainable in this environment, so a temporary CI step printed the formatter's output and this commit applies it byte-for-byte (sha256 d68f75cb5662bd2af9b219203b43e6ecd84270a15612b8bb5018bc7e98608c7b, verified idempotent by a second pass). The step is not in the tree: this commit is the whole of the change. Nothing semantic changes: continuation-operator indentation (`||`, `&&`, `@`, `++`) moves under its operator, `in` gets its own line, one comment header loses a blank line. The formatter did NOT touch the §5.5 `..` tails or any comment added by this branch, which is itself evidence that the record-contract syntax is canonical Nickel. `--self-test` still passes, so `contract_version` and `schema_major` still mirror the validator. Ref #1058. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
force-pushed
the
arena/01a10a3b-standards
branch
from
October 5, 2026 04:48
44f30e6 to
42bef07
Compare
Contributor
|
Autopilot could not be updated. Open Coding to check access and billing. |
Contributor
K9 contract conformancerun https://github.com/hyperpolymath/standards/actions/runs/37265105561 K9 normative contract typecheckK9 contract self-testK9 conformance fixturesK9 corpus conformance (L2) |
|
hyperpolymath
added a commit
that referenced
this pull request
Oct 5, 2026
…ormatted `source_hash` covers every tracked file in a home, so `nickel format` on `1-formats/k9/spec/contract/k9_contract.ncl` moved the `1-formats/k9/` hash again — one commit after the earlier regeneration. Registry Verify caught it on main (`aa1c4dd`), which is the check doing its job. `bash scripts/build-registry.sh --check` passes again; the only changed line is the `1-formats/k9/` source_hash. Scorecards and the compliance dashboard were already in sync. Follow-up to #1149 (M1 · #A, M7 · #F). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 5, 2026
The #1149 squash (M1 contractiles + M2 PROTOCOL.k9 rename) touched 9 files under 1-formats/k9/ but shipped the home's source_hash from before those edits, so origin/main is red on "Registry + topology in sync" and on the Justfile validate chain (registry-check is a hard dependency there). `just registry`: one hash line changes; TOPOLOGY.adoc is unchanged. `build-registry.sh --check` and `build-scorecards.sh --check --strict` both green after. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 5, 2026
…1149 follow-up) (#1151) Follow-up to #1149 (merged as `aa1c4dd`), which landed one commit too early: `nickel format` on `1-formats/k9/spec/contract/k9_contract.ncl` moved the `1-formats/k9/` `source_hash` **after** the registry had been regenerated, so `Registry Verify` failed on main. `source_hash` is `sha256(git ls-files -s <home>)`, so the formatted contract — not just the new fixture — is part of the hash. This regenerates `.machine_readable/REGISTRY.a2ml`; the only changed line is that one hash. ``` bash scripts/build-registry.sh --check → OK bash scripts/build-scorecards.sh --check --strict → OK (dashboard in sync) 1-formats/k9/tools/k9-validate.sh --self-test → all assertions passed K9_VALIDATE_LAYER=all bash .githooks/validate-k9.sh → 13 conforming, 5 grandfathered ``` Refs: #1058 (M1 · #A, M7 · #F). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Owner
Author
The
|
6 of 13 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 6, 2026
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> ## Summary This turns `K9-SVC Contractile Validation` green on `main`. #1154 removed the `..` tails from the five component-facing records in `1-formats/k9/spec/contract/k9_contract.ncl` (`Component`, `Pedigree`, `Security`, `Metadata`, `Signature`), and deleted the comments that explained them. Nickel record contracts are closed by default, so the contract again rejected extension fields that SPEC §5.5 permits ("Unknown fields anywhere | PERMITTED"). As a result the positive control `tools/fixtures/valid/extension-fields.k9.ncl` failed K9-N001 at L2, which made main red. **Owner ruling D310** (standards#787, 2026-10-06): `K9.Component` is an **open** record. This PR restores the tails and their rationale exactly as #1149 wrote them. It keeps #1154's one real improvement, the `.k9.ncl.in` template wording. `HuntEvidence` stays **closed** (§9.2 host evidence, where a misspelt field must be an error), and its comment saying so is restored. Closes #1165 ## Type of change - [x] 🐛 Bug fix (non-breaking change that fixes an issue): contract conformance to §5.5; `contract_version` stays 1.0.0, because the prose never changed. - [ ] ✨ New feature: no - [ ] 💥 Breaking change: no. This only widens acceptance to what §5.5 already permits. - [ ] 🕳️ Soundness fix: not a checker false-negative. It fixes a false-*positive* rejection. - [ ] 📖 Documentation: comments only, restored with the code they explain - [ ] 🧹 Refactor: no - [ ] ⚡ Performance: no - [ ] 🔧 Build / CI / tooling: no workflow change ## 📌 New pins Head SHA: **51321ad504550233854297a892e420d81e3635b8**. This PR adds or changes no action pins, `actions.lock` entries, lockfiles or container digests. ## How has this been verified? Run locally with `nickel 1.17.0`. CI pins 1.18.0. - `nickel typecheck 1-formats/k9/spec/contract/k9_contract.ncl` → rc 0 - `1-formats/k9/tools/k9-validate.sh --strict --fixtures fixtures` → `fixtures: 6 positive, 21 negative (0 needing nickel), 0 failure(s)` - **The control can fail.** With main's contract (`git show origin/main:…`) swapped back in, the same command gives `ERROR K9-N001 [L2] fixtures/valid/extension-fields.k9.ncl: … extra fields failure_mode_defenses, execution` → `1 failure(s)`, the exact CI error on main. **#1165 acceptance item 3** asks that the fix not open the contract wholesale. The tails admit only *unknown names*. Known fields keep their contracts, as the negatives that still fail show: - `L2-K9-N001-wrong-field-type` (a declared field with a wrong type, rejected at L2) - `L2-K9-N001-two-segment-version` - `L1-K9-S004-unknown-leash` (an unknown tag in the closed `SecurityLevel` set) - `HuntEvidence` remains closed. §5.5's last clause (an unknown field never relaxes §8/§9) is enforced by the validator's capability arithmetic, which this PR leaves unchanged (K9-S007/S008 negatives pass). ## Checklist - [x] My commits are **signed**: `git log --format=%G?` → `G`. - [x] I ran the project's own checks/tests locally and they pass: the pre-commit suite and `k9-validate.sh --strict --fixtures`, as above. - [x] SPDX: no new files; the existing MPL-2.0 header is untouched. - [x] Docs are updated, and no public claim overstates the code. The restored comments describe the restored behaviour. - [x] No soundness hole: see item 3 above. ## Notes for reviewers - #1154 was titled "Pr 1148 fixed" with an empty template, so its removal of the tails did not look deliberate. D310 now settles the direction. - Local nickel is 1.17.0 against CI's 1.18.0. CI is the authority. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01D6JVLvmCeSFGcY6jSNesbL Co-authored-by: Claude Opus 5.5 <noreply@anthropic.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
1 participant
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.
Executes migration item M2 / issue #B of
1-formats/k9/spec/MIGRATION-1058.adoc(parent campaign: standards#1058).Ruling
M2 offered two outcomes. Ruling: (a) rename off the reserved suffix. The twelve files are plain YAML session-management contracts: no Nickel body, no
K9!envelope, no k9-coordination schema, and no K9 host loads them. Outcome (b) would mean inventing a dialect so a naming collision could keep its name. All twelve are nowPROTOCOL.yaml; the K9 spec's extension reservation (§4.2) and the discriminator (K9-E005) stay intact.What changed
3-practice/session-management-standards/{continuity,handover,verify}/*/PROTOCOL.k9→PROTOCOL.yaml(12 files, contents otherwise unchanged).MPL-2.0, matching planned-session-close and the directory's other machine artefacts.*.yamlis inside.githooks/validate-spdx.sh'sis_source_filescope, so without this the rename would have planted 11 files that fail the SPDX pre-commit gate on their next touch..machine_readable/k9-contract-debt.txt17 → 5 entries; nothing left to grandfather for this home (the renamed files leave the*.k9population entirely).session-management-standards.scorecard.a2ml)1-formats/k9/actions/validate/validate-k9.shpath (no such directory) at1-formats/k9/tools/k9-validate.sh— this was the explicit ask in M2's note;fail→passon the extension-reservation rule, with an executablecheck(git ls-filesfor*.k9/*.k9.nclunder the home) so the pass is grounded, not asserted;22 of 42recount is now19 of 51(measured).assessed_date2026-07-03 → 2026-10-05.PROTOCOL.yaml, with the reservation rule cited),verify/substantial-completion/CHECKLIST.adoc(link + the wrong "K9 coordination format" wording),K9-CONTRACT-SPEC.adoc§4.2 (past tense; also fixes its "migration item M4" → M2),MIGRATION-1058.adoc§M2 (ruling recorded, note marked fixed), fixture/validator comments kept truthful, CI comment de-numbered.REGISTRY.a2mlregenerated (source_hashissha256(git ls-files -s <home>), so the rename moves it) and0-canon/COMPLIANCE-DASHBOARD.adocregenerated. The same regeneration also clears 3 pre-existing registry drifts (1-formats/k9,2-protocols/axel,form-fill-provenance— the last was carrying the empty-string hash), soregistry-checkgoes from red to green.Verification
scripts/tests/build-scorecards-test.shreports 3 failures in this sandbox only because--verify's preflight refuses to judge passes withoutxmllint, which is not installable here; the scorecard's three pass-row checks were extracted and run directly (M5,S1,S2→ all exit 0).Known-red context
The corpus K9 job runs
.githooks/validate-k9.shover the whole repo and exits non-zero on the 8 pre-existing violations above, which predate this PR and belong to sibling items #A (contractiles) and #D (Axel configs). This PR removes 12 errors from the reported population and adds none.Refs: #1058 (M2 · #B).
M1 · #A also landed on this branch (added 2026-10-05)
6d96f8a— fix(k9): give contractiles a resolvable pedigree (M1, #1058) — rides on top of the M2 commit above: the branch is this session's branch, so #A's half of the fix could not land anywhere else.What the six files now say.
import "../k9/template-hunt.k9.ncl"(which resolved to nothing — there is nok9/below.machine_readable/contractiles/) is replaced bybase.pedigree_schemafrom../_base.ncl, the file that actually defines it. Each of the six now declares §5.5's core —schema_version,component_type = "contractile:<verb>",semantics— plus the §8.4security.capabilitiesthat pay for itsallow_*flags:process.spawnfor all six (allow_subprocess),fs.writeadditionally for adjust and dust (the conditional write path). The four'Huntcomponents (bust, intend, must, trust) gainsignature_required, asignatureblock and 3 irreducibleside_effects; the signature block is a claim, so the §10.2 verdict is'Present_Unverifiedand §10.4 leaves Hunt unauthorised until the signing ceremony replaces it.variance_schema | not_exportedbecause its fields are declarations with no definitions, and Nickel's export refuses a record containing one (missing field definition for \entry_id``).The
mustnaming collision, stated rather than implied. The collision is between K9's execution triad (must/just/nickel) and the contractiles family (must/trust/dust/intend). Resolution: the K9 contract never names a contractile verb. A contractile component is an ordinary K9 component whosecomponent_typebeginscontractile:— that prefix is the entire tie, and it is the only name K9 machinery ever sees. DEED translation therefore renames nothing the K9 spec depends on, and the contractile family keeps its verbs.'Yardvs'Huntfor the two'Yardverbs. adjust and dust requestprocess.spawn(andfs.write) while sitting at'Yard. §7.3 makes'Yardpure evaluation, so those entries are requests recorded in the grant, not permissions in force: at'Yardthe leash is still the cap. Recording them is nonetheless mandatory — §8.4/K9-S007 makes a flag whose capability the grant does not cover a self-contradiction inside the pedigree, not a preference, and leaving the request unwritten would make the file lie about what it asks for.Ledger. No re-listing and no re-grandfathering: no contractile path is in
.machine_readable/k9-contract-debt.txtbefore or after this commit (count 5 entries, unchanged by #A). The removal of the six recorded in the ledger header is now backed by conforming files instead of being premature — before this commit the hook reported all six as hard FAILs precisely because they had no exemption and did not conform.Verification (this branch, run
37262876162):Locally:
--layer L1 --jsonover the six →pass, 0 findings each;bash .githooks/validate-k9.sh→ 2 violations, 0 stale.Known L2 caveat for #F/M7 — recorded, not hidden. The corpus step runs the hook at L1, so the six were not evaluated against
K9.Componentin CI. §5.5 says unknown fields anywhere are PERMITTED and names the contractiles' ownsecurity.probe_scope/authorised_probes_onlyas legitimate extension fields — butk9_contract.ncl'sComponent,PedigreeandSecurityare Nickel record contracts, which are closed by default. Nickel's ownrecord_contract_extra_field.nclfixture is theEvalError::BlameErrorcontrol for exactly this. So when #F raises the corpus to L2, a contractile would be blamed for the extension fields it keeps inside the pedigree —pedigree.semantics/contractile_verb/tier/authority/variance_schema/execution/failure_mode_defenses, andsecurity.probe_scope/probe_kinds_*/allow_filesystem_write_conditional— i.e. onPedigreeandSecurity(M4's note records the same forComponent, for components that keep a payload at top level). The fix belongs to #F and is a..tail on those three records: the prose already permits the fields, and the contract's own header says the prose wins where the two disagree.Docs.
47751eerecords the resolution where the prose still called the six files broken: K9-CONTRACT-SPEC §11.2 (it claimed "no envelope" — the envelope was already there, and the item was misnumbered) and §11.4 (the dangling import), plus a "M1 — resolved" note in MIGRATION-1058 in the same shape M2/M3/M4 used. CI on47751ee: run37263079909— identical K9 result (all steps green except the corpus step, still the two Axel files of #D).