feat(k9): normative Nickel contract, canonical validator, conformance suite (#1058, D173)

.githooks/validate-k9.sh

@@ -1,42 +1,172 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
-# K9 Contract Validation
-
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# validate-k9.sh — the LOCAL (hook) K9 gate. It owns no rules.
+#
+# ── WHAT THIS FILE USED TO BE ───────────────────────────────────────────
+# Until standards#1058 this hook implemented its own idea of a K9 file: it
+# grepped for a line beginning `contract` and warned if no SPDX identifier
+# appeared in the first five lines. Not one of the 30 tracked `*.k9` /
+# `*.k9.ncl` files in this repository contains a line beginning `contract`, so
+# the hook reported 30 errors on a clean tree and had no rule in common with
+# any specification. That is the "local assumption" the issue asked about: it
+# was not a weak implementation of the contract, it was an implementation of
+# something else that happened to share a filename.
+#
+# ── WHAT IT IS NOW ──────────────────────────────────────────────────────
+# A thin caller around the canonical validator,
+# 1-formats/k9/tools/k9-validate.sh, which implements
+# 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc against
+# 1-formats/k9/spec/contract/k9_contract.ncl. There is exactly one place where
+# K9 rules are written down, and this is not it.
+#
+# The only thing this hook adds is POLICY about which files block a commit:
+#
+#   * a file changed by this commit that does not conform  -> FAIL
+#   * a file in the shrink-only debt ledger that conforms  -> FAIL (stale)
+#   * an unlisted, unchanged file that does not conform    -> FAIL
+#   * a listed, UNCHANGED file that does not conform       -> advisory
+#
+# The ledger (.machine_readable/k9-contract-debt.txt) exists because the
+# contract landed after 25 files did, and turning 25 files red at once is how
+# this estate has twice ended up deleting a gate instead of fixing the files
+# (see the A2ML notes in .githooks/pre-commit). It can only shrink: fixing a
+# file forces its entry out, and an edit to a listed file removes its
+# protection for that commit.
+#
+# Runs at --layer L1 by default. L2 needs the `nickel` binary and belongs to
+# CI, where it is installed and pinned; a pre-commit hook that fails because a
+# laptop lacks a toolchain teaches people to pass --no-verify. Set
+# K9_VALIDATE_LAYER=all to check semantics locally too.
 set -euo pipefail
-SCAN_PATH="${INPUT_PATH:-.}"
+
+REPO_ROOT="${INPUT_PATH:-$(git rev-parse --show-toplevel 2>/dev/null || pwd)}"
+cd "$REPO_ROOT"
+
+VALIDATOR="1-formats/k9/tools/k9-validate.sh"
+LEDGER=".machine_readable/k9-contract-debt.txt"
+LAYER="${K9_VALIDATE_LAYER:-L1}"
 STAGED_FILES="${INPUT_STAGED_FILES:-}"
-ERRORS=0
-
-validate_file() {
-  local file="$1"
-
-  # Basic structure check
-  if ! grep -qE '^contract' "$file"; then
-    echo "[validate-k9] ERROR: $file missing contract declaration" >&2
-    ERRORS=$((ERRORS + 1))
-  fi
-
-  # SPDX header check
-  if ! head -5 "$file" | grep -qE '^# SPDX-License-Identifier:'; then
-    echo "[validate-k9] WARNING: $file missing SPDX header" >&2
-  fi
+
+RED='\033[0;31m'; GRN='\033[0;32m'; YEL='\033[1;33m'; BLU='\033[0;34m'; NC='\033[0m'
+[ -t 2 ] || { RED=''; GRN=''; YEL=''; BLU=''; NC=''; }
+
+if [ ! -x "$VALIDATOR" ] && [ ! -f "$VALIDATOR" ]; then
+  # Fail loudly rather than silently. A missing validator that reports success
+  # is indistinguishable from a conforming tree.
+  echo -e "${RED}[validate-k9] canonical validator missing: $VALIDATOR${NC}" >&2
+  exit 1
+fi
+
+# The conformance fixtures are the validator's own test corpus. Scanning them
+# repo-wide would report the negative controls as violations — and worse, a
+# "fix" that made them pass would be a fix that broke the suite.
+is_fixture() {
+  case "$1" in
+    1-formats/k9/tools/fixtures/*) return 0 ;;
+  esac
+  return 1
+}
+
+is_k9() {
+  case "$1" in
+    *.k9|*.k9.ncl) return 0 ;;
+  esac
+  return 1
+}
+
+ledger_entries() {
+  [ -f "$LEDGER" ] || return 0
+  grep -vE '^[[:space:]]*(#|$)' "$LEDGER"
+}
+
+in_ledger() {
+  ledger_entries | grep -qxF "$1"
 }
 
-# If staged files provided, only check those
+# Collect the file list.
+FILES=()
 if [ -n "$STAGED_FILES" ]; then
-  while IFS=$'\n' read -r file; do
-    [ -z "$file" ] && continue
-    # Only check .k9 files
-    [[ "$file" == *.k9 || "$file" == *.k9.ncl ]] || continue
-    [ -f "$file" ] || continue
-    validate_file "$file"
+  while IFS= read -r f; do
+    [ -z "$f" ] && continue
+    is_k9 "$f" || continue
+    is_fixture "$f" && continue
+    [ -f "$f" ] || continue
+    FILES+=("$f")
   done <<< "$STAGED_FILES"
 else
-  while IFS= read -r file; do
-    validate_file "$file"
-  done < <(find "$SCAN_PATH" -path '*/.git/*' -prune -o \( -name '*.k9' -o -name '*.k9.ncl' \) -type f -print 2>/dev/null)
+  while IFS= read -r f; do
+    is_fixture "$f" && continue
+    FILES+=("$f")
+  done < <(git ls-files -- '*.k9' '*.k9.ncl')
+fi
+
+if [ ${#FILES[@]} -eq 0 ]; then
+  echo -e "${BLU}[validate-k9]${NC} no K9 files to check"
+  exit 0
+fi
+
+# One validator invocation for the whole set: it is faster, and it keeps the
+# per-file verdicts coming from a single process rather than N slightly
+# different environments.
+REPORT="$(mktemp)"
+set +e
+bash "$VALIDATOR" --layer "$LAYER" --json --quiet "${FILES[@]}" > "$REPORT" 2>/dev/null
+set -e
+
+CHANGED="$STAGED_FILES"
+HARD=0
+ADVISORY=0
+CONFORMING=0
+STALE=0
+
+while IFS= read -r line; do
+  [ -z "$line" ] && continue
+  file="$(printf '%s' "$line" | sed -E 's/.*"file":"([^"]*)".*/\1/')"
+  verdict="$(printf '%s' "$line" | sed -E 's/.*"verdict":"([^"]*)".*/\1/')"
+  # `|| true` is load-bearing: a conforming file has no findings, grep exits 1,
+  # and under `set -o pipefail` that would abort the hook halfway through a
+  # clean tree — reporting neither a pass nor a failure.
+  rules="$(printf '%s' "$line" | grep -oE '"rule":"K9-[ESNC][0-9]+"' | sed 's/.*:"//; s/"//' | sort -u | tr '\n' ' ' | sed 's/ $//' || true)"
+
+  case "$verdict" in
+    pass|routed)
+      CONFORMING=$((CONFORMING + 1))
+      if in_ledger "$file"; then
+        # A conforming file must not keep its exemption: that is how a ledger
+        # becomes a permanent licence for debt that no longer exists.
+        echo -e "${RED}[validate-k9] STALE ledger entry: $file now conforms — remove it from $LEDGER in this change${NC}" >&2
+        STALE=$((STALE + 1))
+      fi
+      continue ;;
+  esac
+
+  touched=0
+  if [ -n "$CHANGED" ] && printf '%s\n' "$CHANGED" | grep -qxF "$file"; then
+    touched=1
+  fi
+
+  if [ $touched -eq 1 ] || ! in_ledger "$file"; then
+    echo -e "${RED}[validate-k9] FAIL${NC} $file ($verdict)${rules:+ — $rules}" >&2
+    HARD=$((HARD + 1))
+  else
+    echo -e "${YEL}[validate-k9] debt${NC} $file ($verdict)${rules:+ — $rules} (grandfathered; touching it makes it blocking)" >&2
+    ADVISORY=$((ADVISORY + 1))
+  fi
+done < "$REPORT"
+rm -f "$REPORT"
+
+if [ "$STALE" -gt 0 ] || [ "$HARD" -gt 0 ]; then
+  echo -e "${RED}[validate-k9] $HARD violation(s), $STALE stale ledger entr(ies)${NC}" >&2
+  echo -e "${RED}[validate-k9] spec: 1-formats/k9/spec/K9-CONTRACT-SPEC.adoc · plan: 1-formats/k9/spec/MIGRATION-1058.adoc${NC}" >&2
+  exit 1
 fi
 
-[ $ERRORS -gt 0 ] && exit 1
-echo "[validate-k9] All K9 contracts valid"
+echo -e "${GRN}[validate-k9]${NC} $CONFORMING conforming, $ADVISORY grandfathered (layer $LAYER, contract v1.0.0)"
+if [ "$LAYER" = "L0" ] || [ "$LAYER" = "L1" ]; then
+  # Say out loud what was NOT checked. A lexical pass is not a conformance
+  # result, and the difference is the whole point of §12.
+  echo -e "${YEL}[validate-k9] lexical layers only — Nickel semantics (L2) and signature verification (L3) were not checked here${NC}" >&2
+fi
 exit 0

.githooks/validate-lint-format.sh

@@ -100,7 +100,20 @@ else
 fi
 
 # ── Nickel ──────────────────────────────────────────────────────────────
-NCL="$(staged_matching '\.ncl$')"
+# `*.k9.ncl` is EXCLUDED here, matching .github/workflows/ci-pipeline.yml,
+# which excludes the same pathspec in both its `detect` and `nickel` jobs.
+#
+# A K9 component opens with the three-octet `K9!` sentinel, which is not
+# Nickel: `nickel typecheck` dies at 1:3 on the `!` (the CI comment says so
+# verbatim). Running it here anyway was not a strict gate, it was a wrong one
+# — it failed on a byte the format requires, on files no edit could fix, which
+# is the shape of a hook people learn to bypass with --no-verify.
+#
+# K9 files are not therefore unchecked. They are checked by the gate that
+# knows the format: .githooks/validate-k9.sh, which delegates to
+# 1-formats/k9/tools/k9-validate.sh and applies the envelope-strip rule
+# (K9-CONTRACT-SPEC §3.6) before it reaches for Nickel at all.
+NCL="$(staged_matching '\.ncl$' | grep -v '\.k9\.ncl$' || true)"
 if [ -n "$NCL" ]; then
   note "Nickel: $(echo "$NCL" | grep -c .) staged file(s)"
   if require_tool nickel Nickel "https://github.com/tweag/nickel/releases"; then

.githooks/validate-spdx.sh

@@ -40,6 +40,29 @@
   esac
 }
 
+# A NEGATIVE CONTROL CANNOT ALSO SATISFY THE RULE IT TESTS.
+#
+# 1-formats/k9/tools/fixtures/invalid/ holds the K9 conformance corpus, and
+# every file in it exists to violate one named rule. L0-K9-E004-no-spdx.k9.ncl
+# is there precisely BECAUSE it has no SPDX header: it is the control that
+# proves rule K9-E004 can fire. Requiring a header on it would not tighten this
+# gate, it would delete the fixture and leave the K9 rule untested.
+#
+# The exemption is keyed to the RULE the fixture tests, not to the directory:
+# only a fixture whose name declares K9-E004 may lack a header. Every other
+# negative control still has to carry one, so this cannot become a blanket hole
+# in the corpus. It is also a separate predicate from is_source_file, so the two
+# reasons stay distinct: "is this a source file" is about syntax, "is this a
+# test vector for the licence rule" is about intent. Same reasoning as the
+# secret scanner's exclusion of published conformance vectors
+# (secret-scanner-reusable.yml).
+is_exempt_path() {
+  case "$1" in
+    1-formats/k9/tools/fixtures/invalid/*K9-E004*) return 0 ;;
+  esac
+  return 1
+}
+
 # If staged files provided, only check those
 if [ -n "$STAGED_FILES" ]; then
   FILES_TO_CHECK=$STAGED_FILES
@@ -68,6 +91,7 @@
   [ -n "$file" ] || continue
   [ -f "$file" ] || continue
   is_source_file "$file" || continue
+  is_exempt_path "$file" && continue
 
   CHECKED=$((CHECKED + 1))
 

.github/workflows/k9-contractile.yml

@@ -36,6 +36,12 @@
     name: K9-SVC contractile validation
     timeout-minutes: 10
     runs-on: ubuntu-latest
+    # Needed only by the final step, which posts the validator's verdict to
+    # the pull request. Log blobs are not reachable from every machine that
+    # needs the result, so the result is published where it can be read.
+    permissions:
+      contents: read
+      pull-requests: write
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
@@ -89,4 +95,107 @@
             echo "❌ $missing contractile(s) missing"
             exit 1
           fi
-          echo "✅ All ${#files[@]} contractiles present"
+          echo "✅ All ${#files[@]} contractiles present"
+      # ── K9 CONTRACT CONFORMANCE (standards#1058, ruling D173) ──────────
+      #
+      # Everything above this line checks that contractile FILES EXIST. None of
+      # it checked that a `.k9.ncl` file is a valid K9 component: the local hook
+      # grepped for a line beginning `contract`, which no file in this repo has,
+      # and ci-pipeline.yml excludes `*.k9.ncl` from Nickel entirely. So the
+      # required check named "K9-SVC contractile validation" validated the
+      # registry and never once read a pedigree.
+      #
+      # Nickel is installed here, pinned and sha256-verified with the SAME pin
+      # as ci-pipeline.yml's `nickel` job — one version estate-wide, so a file
+      # cannot typecheck in one lane and not in another.
+      - name: Install Nickel (pinned, sha256-verified)
+        env:
+          NICKEL_VERSION: '1.18.0'
+          NICKEL_SHA256: '9cba4dd65ae9915ec61f73033aafcff307a377665a83fd8f530df086763318cb'
+        run: |
+          set -euo pipefail
+          URL="https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 --retry 3 -o "$RUNNER_TEMP/nickel" "$URL"
+          echo "${NICKEL_SHA256}  ${RUNNER_TEMP}/nickel" | sha256sum -c -
+          chmod +x "$RUNNER_TEMP/nickel"
+          echo "$RUNNER_TEMP" >> "$GITHUB_PATH"
+          echo "K9_REPORT=$RUNNER_TEMP/k9-report.md" >> "$GITHUB_ENV"
+
+      # Each step mirrors its output into $GITHUB_STEP_SUMMARY as well as
+      # stdout. The PR then shows the verdict without anyone opening a raw log,
+      # and `gh api repos/{o}/{r}/check-runs/{job_id} --jq .output.summary`
+      # 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 contract self-test
+        run: |
+          set -uo pipefail
+          # Asserts the validator's bash mirrors still agree with the normative
+          # contract, the capability arithmetic, the structural extractor, and
+          # the envelope strip. Runs before the fixtures so a broken validator
+          # is reported as a broken validator rather than as a broken corpus.
+          {
+            echo '## K9 contract self-test'
+            echo '```'
+            bash 1-formats/k9/tools/k9-validate.sh --self-test 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: K9 conformance fixtures (positive AND negative controls)
+        run: |
+          set -uo pipefail
+          # --strict: with Nickel on PATH every format layer (L0-L2) must
+          # actually run, so a missing toolchain cannot report a pass. The 21
+          # negative controls are the load-bearing half — a validator that
+          # accepts everything satisfies the positive half trivially.
+          {
+            echo '## K9 conformance fixtures'
+            echo '```'
+            bash 1-formats/k9/tools/k9-validate.sh --strict \
+              --fixtures 1-formats/k9/tools/fixtures 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: K9 corpus conformance (ratcheted)
+        run: |
+          set -uo pipefail
+          # The whole tracked corpus, through the same gate the pre-commit hook
+          # uses, so CI and the hook cannot disagree about what a K9 file is.
+          # .machine_readable/k9-contract-debt.txt grandfathers the 25 files
+          # that predate the contract; it is shrink-only (a conforming file
+          # left in it fails), and it does not protect a file this PR touches.
+          {
+            echo '## K9 corpus conformance'
+            echo '```'
+            bash .githooks/validate-k9.sh 2>&1
+            echo '```'
+          } | tee -a "$GITHUB_STEP_SUMMARY" "$K9_REPORT"
+          exit "${PIPESTATUS[0]}"
+
+      - name: Publish the K9 verdict to the pull request
+        # always(): a failing gate is exactly when the detail is needed, and a
+        # skipped step would publish nothing.
+        if: ${{ always() && github.event_name == 'pull_request' }}
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+        run: |
+          set -uo pipefail
+          [ -s "$K9_REPORT" ] || { echo "no K9 report produced"; exit 0; }
+          {
+            echo '<!-- k9-contractile-report: regenerated on every run -->'
+            echo '# K9 contract conformance'
+            echo
+            echo "_run_ $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+            cat "$K9_REPORT"
+          } > "$RUNNER_TEMP/body.md"
+          prev=$(gh pr view "$PR_NUMBER" --repo "$GITHUB_REPOSITORY" --json comments \
+            --jq '.comments[] | select(.body | startswith("<!-- k9-contractile-report")) | .url' | tail -1 || true)
+          if [ -n "$prev" ]; then
+            # Edit the previous report in place so repeated runs do not stack up.
+            gh api -X PATCH "${prev#https://github.com/}" -F body=@"$RUNNER_TEMP/body.md" >/dev/null
+          else
+            gh pr comment "$PR_NUMBER" --repo "$GITHUB_REPOSITORY" --body-file "$RUNNER_TEMP/body.md" >/dev/null
+          fi