W0 hygiene: K9 gate fix, proof gate that can fail, repo deed, ABI/FFI seam aligned

.machine_readable/root-allow.txt

@@ -28,6 +28,7 @@ CHANGELOG.md
 # ─── Build entry points (must live at root for their tooling) ────────────────
 Justfile                   # delegates phases to build/just/*.just
 coordination.k9            # repo-local session binding (template-mandated)
+recon-silly-ation_chora.deed  # the repo deed (standards#837, D312): one machine-readable record per repo; read with scripts/deed-field.sh
 
 # ─── Conventional dotfiles (tool-required at root) ───────────────────────────
 .editorconfig

.machine_readable/self-validating/methodology-guard.k9.ncl

@@ -1,9 +1,11 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # K9 Validator: Methodology Guard
-# Checks that agent work respects methodology constraints declared in
-# bot_directives/methodology.a2ml.
+# Checks that agent work respects methodology constraints declared in the
+# repo deed's (bot-directives (methodology)) clause, read with
+# scripts/deed-field.sh.
 #
 # Usage: k9 validate methodology-guard
 
@@ -12,6 +14,18 @@ let methodology_guard = {
   version = "1.0.0",
   description = "Validates that agent work respects declared methodology constraints",
 
+  pedigree = {
+    schema_version = "1.0.0",
+    component_type = "validator:methodology-guard",
+    metadata = {
+      name = "methodology-guard",
+      version = "1.0.0",
+    },
+    security = {
+      leash = 'Yard,
+    },
+  },
+
   checks = {
     divergent_invariant_language = {
       description = "No files in languages violating the divergent language invariant",
@@ -41,11 +55,14 @@ let methodology_guard = {
     },
 
     state_not_template = {
-      description = "STATE.a2ml must not contain template placeholders",
+      description = "The ROADMAP journal must not contain template placeholders",
       severity = "warning",
-      file = ".machine_readable/6a2/STATE.a2ml",
+      # The journal, not the repo deed: a deed names rsr-template-repo in
+      # (lineage :instantiated-from) by design, so this pattern would always
+      # fire there.
+      file = "docs/status/ROADMAP.adoc",
       # NOTE: the PROJECT token below is written as a Nickel concat
-      # ("{{" ++ "PROJECT}}") ON PURPOSE. `just init` runs a sed substitution for
+      # ("{{" ++ "PROJECT}}") ON PURPOSE. `just repo-init` runs a sed substitution for
       # the brace-PROJECT-brace token over EVERY text file, which would otherwise
       # rewrite this guard's own pattern into the consumer's name and break the
       # check. Splitting the literal across "++" keeps the contiguous token text
@@ -57,9 +74,14 @@ let methodology_guard = {
     },
 
     coverage_updated = {
-      description = "coverage.a2ml should be updated within 30 days",
+      description = "The deed's coverage record should be updated within 30 days",
       severity = "info",
-      file = ".machine_readable/bot_directives/coverage.a2ml",
+      # The repo deed (<repo>_chora.deed, a glob: its stem is the repo slug).
+      # The date is the clause's own :last-updated, not the file's mtime: the
+      # deed changes for many reasons, so its mtime says nothing about coverage.
+      file_glob = "*_chora.deed",
+      deed_clause = "bot-directives/coverage/metadata",
+      date_key = "last-updated",
       staleness_days = 30,
     },
   },

.machine_readable/self-validating/template-kennel.k9.ncl

@@ -19,7 +19,7 @@ K9!
       name = "TODO: component-name",
       version = "1.0.0",
       description = "TODO: Brief description of what this component contains",
-      author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>",
+      author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
     },
   },
 

build/just/proofs.just

@@ -12,126 +12,33 @@
 proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
     @echo "=== All proof checks complete ==="
 
-# Check Idris2 proofs (ABI, types, dependent type proofs)
+# Each proof-check-<prover> delegates to scripts/check-proofs.sh, the single
+# source of truth. A missing toolchain is FATAL (never a skip); every module is
+# checked from its own source root; a proof file absent from the prover's
+# manifest (verification/proofs/<prover>/MANIFEST) is an error. See the script
+# header for the four "checks that could not fail" this replaces.
+
+# Check Idris2 proofs (per MANIFEST; fatal if idris2 absent)
 proof-check-idris2:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Idris2 proofs ==="
-    if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if idris2 --check "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Idris2 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Idris2 proofs verified"
+    @bash scripts/check-proofs.sh idris2
 
-# Check Lean4 proofs
+# Check Lean4 proofs (per MANIFEST; fatal if lean absent)
 proof-check-lean4:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Lean4 proofs ==="
-    if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if lean "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Lean4 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Lean4 proofs verified"
+    @bash scripts/check-proofs.sh lean4
 
-# Check Agda proofs
+# Check Agda proofs (per MANIFEST; fatal if agda absent)
 proof-check-agda:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Agda proofs ==="
-    if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if agda --safe "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Agda proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Agda proofs verified"
+    @bash scripts/check-proofs.sh agda
 
-# Check Coq proofs
+# Check Coq proofs (per MANIFEST; fatal if coqc absent)
 proof-check-coq:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Coq proofs ==="
-    if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if coqc "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Coq proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Coq proofs verified"
+    @bash scripts/check-proofs.sh coq
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan for dangerous constructs USED in proof code (believe_me, sorry, Admitted,
+# postulate, ...). Comments are ignored — a comment naming a banned construct
+# must not trip the gate. See scripts/scan-dangerous.sh.
 proof-scan-dangerous:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Scanning for dangerous patterns in proofs ==="
-    DANGEROUS=0
-    PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic"
-    for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do
-        MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true)
-        if [ -n "$MATCHES" ]; then
-            echo "  DANGEROUS: $f"
-            echo "$MATCHES" | sed 's/^/    /'
-            DANGEROUS=$((DANGEROUS + 1))
-        fi
-    done
-    if [ "$DANGEROUS" -gt 0 ]; then
-        echo "FAIL: $DANGEROUS file(s) contain dangerous patterns"
-        exit 1
-    fi
-    echo "PASS: No dangerous patterns found in proofs"
+    @bash scripts/scan-dangerous.sh
 
 # Show proof status summary
 proof-status: