Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 71 additions & 0 deletions .machine_readable/svc/k9/README.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
// SPDX-License-Identifier: MPL-2.0
= K9 Contractiles — nextgen-languages self-validation
:toc: left
:icons: font

== Why K9 lives here

Per **ADR-001 (2026-04-18)** (see `../README.adoc`), K9 self-validating
components live under `.machine_readable/svc/k9/` rather than under
`contractiles/`, so the contractile directory stays a pure six-verb set
(intend, trust, must, bust, adjust, dust). The verb contractiles *declare*
invariants; the K9 validators here *machine-check* them.

NOTE: `../../MUST.contractile` historically points its `enforcement` at
`contractiles/k9/must-check.k9.ncl`. The canonical location is here
(`svc/k9/must-check.k9.ncl`) per ADR-001; the stale path in MUST.contractile
is a known doc gap (it lives outside this sweep's write-scope and is left as
a TODO for a future MUST.contractile refresh).

== The Leash — three security levels

K9 components declare their trust requirements:

[horizontal]
`'Kennel`:: Pure data, no execution (safest; no signature)
`'Yard`:: Nickel evaluation with contracts (medium trust; signature recommended)
`'Hunt`:: Full execution with Just recipes (signature *required*)

== Components in this directory

`must-check.k9.ncl`:: **Yard.** The runnable surface of the hard invariants
declared in `../../MUST.contractile` and
`../../contractiles/must/Mustfile.a2ml`. CI runs it on every PR
(`quality.yml`); violations of `error`-severity checks block merge.

`methodology-guard.k9.ncl`:: **Yard.** Checks that agent work respects the
methodology constraints in `../../agent_instructions/methodology.a2ml`
(believe_me / assert_total ceilings, state-file template-placeholder
rejection, coverage staleness).

`template-kennel.k9.ncl`:: **Kennel.** Starting point for new pure-data K9
components.

== Validate / run

[source,bash]
----
# Typecheck a Yard/Kennel component (no I/O)
nickel typecheck svc/k9/must-check.k9.ncl

# Evaluate a Yard component (validation, no side effects)
nickel eval svc/k9/methodology-guard.k9.ncl

# Export Kennel data
nickel export svc/k9/template-kennel.k9.ncl > out.json
----

== Dependencies

* **Nickel** — configuration language and contract evaluator.
* **k9-svc** (https://github.com/hyperpolymath/k9-svc) — the `must` shim,
signing, and the full SPEC. IANA media type `application/vnd.k9+nickel`.

== Adding a K9 component

1. Pick the lowest sufficient leash (Kennel > Yard > Hunt).
2. Document what it does in the `pedigree.metadata.description`.
3. Put real contracts in Yard/Hunt components — a Yard file with no
contracts is just a Kennel file in disguise.
4. Sign Hunt components before committing; never run unsigned Hunt.
5. Wire `error`-severity validators into `quality.yml`.
99 changes: 99 additions & 0 deletions .machine_readable/svc/k9/methodology-guard.k9.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
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 (nextgen-languages)
# Security Level: Yard (Nickel evaluation; no I/O)
#
# Checks that agent work respects the methodology constraints declared in
# ../../agent_instructions/methodology.a2ml.
#
# Usage: k9 validate methodology-guard

let methodology_guard = {
pedigree = {
schema_version = "1.0.0",
component_type = "methodology-validator",
security = {
leash = 'Yard,
trust_level = "validated-config",
allow_network = false,
allow_filesystem_write = false,
allow_subprocess = false,
},
metadata = {
name = "methodology-guard",
version = "1.0.0",
description = "Validates that agent work respects declared methodology constraints",
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
paired_files = [
"../../agent_instructions/methodology.a2ml",
],
},
},

name = "methodology-guard",
version = "1.0.0",
description = "Validates that agent work respects declared methodology constraints",

source_of_truth = ".machine_readable/agent_instructions/methodology.a2ml",

checks = {
believe_me_ceiling = {
description = "believe_me count must not exceed the declared ceiling",
severity = "error",
pattern = "believe_me",
ceiling_key = "methodology.divergent-invariants.believe-me-ceiling",
default_ceiling = 0,
note = "Hub-level scan; submodule trees enforce their own ceilings.",
},

assert_total_ceiling = {
description = "assert_total count must not exceed the declared ceiling",
severity = "error",
pattern = "assert_total",
ceiling_key = "methodology.divergent-invariants.assert-total-ceiling",
default_ceiling = 0,
},

state_not_template = {
description = "STATE.a2ml must not contain template placeholders",
severity = "warning",
file = ".machine_readable/6a2/STATE.a2ml",
reject_patterns = ["{{PLACEHOLDER}}", "{{PROJECT}}", "rsr-template-repo"],
reject_key = "methodology.state-validation.reject-if-contains",
},

state_not_stale = {
description = "STATE.a2ml last-updated should be within the staleness threshold",
severity = "info",
file = ".machine_readable/6a2/STATE.a2ml",
staleness_key = "methodology.state-validation.staleness-threshold-days",
default_staleness_days = 90,
},

coverage_updated = {
description = "coverage.a2ml should be refreshed within 30 days",
severity = "info",
file = ".machine_readable/agent_instructions/coverage.a2ml",
staleness_days = 30,
},

spike_required = {
description = "Sessions must ship code, not only designs (methodology.spike-required)",
severity = "info",
key = "methodology.spike-required",
expected = true,
},
},

# KNOWN GAP: methodology.a2ml still carries template defaults for
# unique-strength, divergent-invariants.rules, and known-constraints.
# Until those are filled, the divergent-mode checks fall back to defaults.
open_gaps = [
"methodology.unique-strength.description == {{PROJECT_UNIQUE_STRENGTH}}",
"methodology.divergent-invariants.rules == []",
"methodology.known-constraints.constraints == []",
],
}
in methodology_guard
105 changes: 105 additions & 0 deletions .machine_readable/svc/k9/must-check.k9.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
K9!
# SPDX-License-Identifier: MPL-2.0
# K9 Yard-level validator: MUST-check
# Security Level: Yard (Nickel evaluation with contracts; no I/O)
#
# Runnable surface of the hard invariants declared in
# ../../MUST.contractile and ../../contractiles/must/Mustfile.a2ml.
# CI (quality.yml) runs this on every PR; `error`-severity failures block
# merge. Keep the check IDs aligned with Mustfile.a2ml section names.

{
pedigree = {
schema_version = "1.0.0",
component_type = "must-validator",
security = {
leash = 'Yard,
trust_level = "validated-config",
allow_network = false,
allow_filesystem_write = false,
allow_subprocess = false,
},
metadata = {
name = "must-check",
version = "1.0.0",
description = "Machine-checks the nextgen-languages MUST invariants (hub-level hygiene; submodule trees are each repo's own concern).",
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
paired_files = [
"../../MUST.contractile",
"../../contractiles/must/Mustfile.a2ml",
],
},
},

# Each check declares a severity and a shell predicate (exit 0 = pass).
# A K9 'Yard runner evaluates these; it does not itself run the shell —
# the predicate string is handed to the CI executor named in `run`.
checks = {
license_present = {
description = "LICENSE file must exist",
severity = 'error,
predicate = "test -f LICENSE",
},

ai_manifest_present = {
description = "0-AI-MANIFEST.a2ml entry point must exist",
severity = 'error,
predicate = "test -f 0-AI-MANIFEST.a2ml",
},

machine_readable_dir = {
description = ".machine_readable/ directory preserved",
severity = 'error,
predicate = "test -d .machine_readable",
},

no_root_scm_duplication = {
description = "No STATE/META/ECOSYSTEM state file orphaned in repo root (canonical home is .machine_readable/6a2/)",
severity = 'error,
predicate = "! ls STATE.* META.* ECOSYSTEM.* 2>/dev/null | head -1 | grep -q .",
},

six_a_two_complete = {
description = "The 6a2 metadata set is complete (>= 6 .a2ml files)",
severity = 'warning,
predicate = "test $(ls .machine_readable/6a2/*.a2ml 2>/dev/null | wc -l) -ge 6",
},

spdx_on_machine_readable = {
description = "Every .a2ml under .machine_readable/ carries an SPDX header",
severity = 'warning,
predicate = "! grep -rL 'SPDX-License-Identifier' .machine_readable --include='*.a2ml' 2>/dev/null | head -1 | grep -q .",
},

no_agpl = {
description = "No AGPL references in dotfiles (estate policy is MPL-2.0)",
severity = 'error,
predicate = "! grep -rE 'AGPL-3[.]0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q .",
},

actions_sha_pinned = {
description = "Third-party GitHub Actions are SHA-pinned (reusable callers to hyperpolymath/standards excepted)",
severity = 'warning,
predicate = "! grep -rEn 'uses:[[:space:]]+[^#]+@(main|master|v[0-9]+)[[:space:]]*$' .github/workflows 2>/dev/null | grep -v 'hyperpolymath/standards' | head -1 | grep -q .",
},

hypatia_waiver_registry = {
description = "Hypatia accepted-findings registry exists (NEUROSYM.a2ml)",
severity = 'warning,
predicate = "grep -q '\\[accepted-findings\\]' .machine_readable/6a2/NEUROSYM.a2ml",
},

kitchenspeak_postulate_axiom = {
description = "KitchenSpeak Agda postulates remain annotated as trusted base (AXIOM marker)",
severity = 'warning,
predicate = "test ! -d kitchenspeak/proofs/agda || ! grep -rl 'postulate' kitchenspeak/proofs/agda --include='*.agda' 2>/dev/null | xargs -r grep -L 'AXIOM' 2>/dev/null | head -1 | grep -q .",
},
},

run = {
executor = "ci:quality.yml",
on_error_severity = "exit-nonzero", # error-severity failures block merge
on_warning_severity = "report-only",
report_format = "a2ml",
},
}
53 changes: 53 additions & 0 deletions .machine_readable/svc/k9/template-kennel.k9.ncl
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
K9!
# SPDX-License-Identifier: MPL-2.0
# K9 Kennel-level template: Pure data configuration
# Security Level: Kennel (data-only, no execution)
# No signature required — safe for any use.

{
pedigree = {
schema_version = "1.0.0",
component_type = "TODO: describe component type (e.g., 'language-metadata', 'build-config')",
security = {
leash = 'Kennel,
trust_level = "data-only",
allow_network = false,
allow_filesystem_write = false,
allow_subprocess = false,
},
metadata = {
name = "TODO: component-name",
version = "1.0.0",
description = "TODO: Brief description of what this component contains",
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
},
},

# Pure data only. No contracts, no recipes — promote to template-yard
# (Nickel contracts) or a Hunt component if you need validation/execution.
config = {
setting_1 = "value",
setting_2 = 42,
setting_3 = true,

nested = {
key = "value",
},

list = [
"item1",
"item2",
],
},

export = {
format = "json", # or "yaml", "toml"
destination = "output.json",
},
}

# Usage:
# 1. Fill in TODO items above.
# 2. Replace config = { ... } with your data.
# 3. Validate: nickel typecheck your-file.k9.ncl
# 4. Export: nickel export your-file.k9.ncl > output.json
Loading