Skip to content

Commit 1017da7

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(cartridges): add k9iser-mcp — central K9 contract regeneration
Reference implementation of the -iser regeneration-cartridge pattern. Wraps the k9iser generator so generated/k9iser/*.k9 are regenerated centrally on trigger instead of run ad hoc + hand-committed (the drift that broke Dogfood Gate estate-wide — k9iser#8, idaptik#77). Mirrors ssg-mcp structure: cartridge.json (5 tools, ADR-0006 ffi symbols), mod.js MCP bridge (backend :7743), abi/ Idris2 pipeline state machine + safety GADT (no apply-without-validate, no validate-without- generate), ffi/ Zig C-ABI + boj_cartridge_invoke dispatch, three- protocol adapter, Panll panels. Verified: ffi `zig build test` 16/16 pass (state machine + invariants + ADR-0006 dispatch); adapter builds on Zig 0.15.2 (adapter/build.zig uses the modern root_module API — the ssg-mcp exemplar's is stale). Grade D Alpha: invoke returns shaped stubs; live path additionally needs the backend service + the BoJ REST runtime (pending Elixir rewrite), exactly as ssg-mcp/boj-build.yml are today. Refs hyperpolymath/k9iser#8. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 23c7398 commit 1017da7

14 files changed

Lines changed: 1311 additions & 0 deletions

File tree

‎cartridges/k9iser-mcp/README.adoc‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= k9iser-mcp — K9 contract regeneration cartridge
4+
:toc: macro
5+
:orientation: shallow
6+
7+
toc::[]
8+
9+
== Purpose
10+
11+
Wraps the `k9iser` generator as a BoJ cartridge so that a repository's
12+
`generated/k9iser/*.k9` contracts are regenerated *centrally, on trigger*
13+
instead of being run ad hoc and hand-committed (which is how they rot —
14+
see hyperpolymath/k9iser#8 and the idaptik#77 triage).
15+
16+
This is the reference implementation for the `-iser` regeneration-cartridge
17+
pattern (standards epic): every `-iser` generator should ship an equivalent
18+
so `generated/*` stops being hand-maintained drift estate-wide.
19+
20+
== Pipeline
21+
22+
[source]
23+
----
24+
Empty -> ManifestLoaded -> Generated -> Validated -> Applied
25+
----
26+
27+
Enforced safety invariants (formally in `abi/K9iserMcp/SafeK9iser.idr`,
28+
executably in `ffi/k9iser_ffi.zig`):
29+
30+
. *No apply without validate* — contracts that fail the canonical
31+
`k9-validate` ruleset (K9! magic + pedigree) can never be committed back
32+
to a repository.
33+
. *No validate without generate* — stale/absent output is never validated.
34+
. *Generate requires a loaded manifest.*
35+
36+
== Tools (`cartridge.json`)
37+
38+
[cols="1,3"]
39+
|===
40+
| `k9_load_manifest` | Load a repo's `k9iser.toml`
41+
| `k9_generate` | Generate K9 contracts from configs + manifest rules
42+
| `k9_validate` | Validate against the canonical K9! + pedigree ruleset
43+
| `k9_apply` | Commit + push regenerated contracts to the branch
44+
| `k9_clean` | Clean the session
45+
|===
46+
47+
== Layout
48+
49+
* `cartridge.json` — manifest (tools, ADR-0006 ffi symbols)
50+
* `mod.js` — Deno MCP bridge → backend at `K9ISER_BACKEND_URL`
51+
(default `http://127.0.0.1:7743`)
52+
* `abi/` — Idris2 ABI: pipeline state machine + safety GADT
53+
* `ffi/` — Zig FFI: C-ABI exports + ADR-0006 `boj_cartridge_invoke`
54+
dispatch (16/16 tests pass)
55+
* `adapter/` — three-protocol (REST/gRPC-compat/GraphQL) adapter
56+
* `panels/` — Panll dashboard manifest
57+
58+
== Status
59+
60+
Grade D Alpha. Cartridge package + verified state machine are complete.
61+
`boj_cartridge_invoke` returns shaped stubs; the live path additionally
62+
needs the backend service (runs the `k9iser` binary against a checked-out
63+
working tree) *and* the BoJ REST runtime, which is pending the Elixir
64+
rewrite — until that deploys, the templated `k9iser-regen` trigger is
65+
fire-and-forget exactly like `boj-build.yml` is today.

‎cartridges/k9iser-mcp/abi/K9iserMcp/SafeK9iser.idr‎

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
||| K9iserMcp.SafeK9iser: Formally verified K9-contract generation pipeline.
4+
|||
5+
||| Cartridge: k9iser-mcp
6+
||| Matrix cell: config domain x {MCP, REST} protocols
7+
|||
8+
||| This module defines a regeneration pipeline state machine that prevents:
9+
||| - Applying (committing) contracts that were never validated
10+
||| - Validating contracts that were never generated
11+
||| - Generating from an unloaded manifest
12+
|||
13+
||| State machine: Empty -> ManifestLoaded -> Generated -> Validated -> Applied
14+
module K9iserMcp.SafeK9iser
15+
16+
import Data.List
17+
18+
%default total
19+
20+
-- ═══════════════════════════════════════════════════════════════════════════
21+
-- K9iser Pipeline State Machine
22+
-- ═══════════════════════════════════════════════════════════════════════════
23+
24+
||| k9iser regeneration lifecycle states.
25+
||| Progresses: Empty -> ManifestLoaded -> Generated -> Validated -> Applied
26+
public export
27+
data K9State
28+
= Empty
29+
| ManifestLoaded
30+
| Generated
31+
| Validated
32+
| Applied
33+
| K9Error
34+
35+
||| Equality for K9 states.
36+
public export
37+
Eq K9State where
38+
Empty == Empty = True
39+
ManifestLoaded == ManifestLoaded = True
40+
Generated == Generated = True
41+
Validated == Validated = True
42+
Applied == Applied = True
43+
K9Error == K9Error = True
44+
_ == _ = False
45+
46+
||| Valid state transitions (enforced at the type level).
47+
||| Critically, Generated -> Applied is NOT valid (must validate first).
48+
||| And ManifestLoaded -> Validated is NOT valid (must generate first).
49+
public export
50+
data ValidTransition : K9State -> K9State -> Type where
51+
LoadManifest : ValidTransition Empty ManifestLoaded
52+
Generate : ValidTransition ManifestLoaded Generated
53+
Regenerate : ValidTransition Generated Generated
54+
Validate : ValidTransition Generated Validated
55+
Apply : ValidTransition Validated Applied
56+
CleanApplied : ValidTransition Applied Empty
57+
CleanReady : ValidTransition Validated Empty
58+
ManifestErr : ValidTransition ManifestLoaded K9Error
59+
GenerateErr : ValidTransition Generated K9Error
60+
Recover : ValidTransition K9Error Empty
61+
62+
||| Runtime transition validator (matches the Zig FFI isValidTransition).
63+
public export
64+
canTransition : K9State -> K9State -> Bool
65+
canTransition Empty ManifestLoaded = True
66+
canTransition ManifestLoaded Generated = True
67+
canTransition Generated Generated = True -- regenerate
68+
canTransition Generated Validated = True
69+
canTransition Validated Applied = True
70+
canTransition Applied Empty = True -- clean
71+
canTransition Validated Empty = True -- clean without applying
72+
canTransition ManifestLoaded K9Error = True -- parse error
73+
canTransition Generated K9Error = True -- generation error
74+
canTransition K9Error Empty = True -- recover
75+
canTransition _ _ = False
76+
77+
-- ═══════════════════════════════════════════════════════════════════════════
78+
-- Config Format Types
79+
-- ═══════════════════════════════════════════════════════════════════════════
80+
81+
||| Config formats k9iser can wrap (mirrors k9iser's ConfigFormat).
82+
public export
83+
data K9Format
84+
= Toml
85+
| Yaml
86+
| Json
87+
| Ini
88+
| Custom String
89+
90+
||| C-ABI encoding.
91+
public export
92+
formatToInt : K9Format -> Int
93+
formatToInt Toml = 1
94+
formatToInt Yaml = 2
95+
formatToInt Json = 3
96+
formatToInt Ini = 4
97+
formatToInt (Custom _) = 99
98+
99+
-- ═══════════════════════════════════════════════════════════════════════════
100+
-- MCP Tool Definitions
101+
-- ═══════════════════════════════════════════════════════════════════════════
102+
103+
||| MCP tools exposed by this cartridge.
104+
public export
105+
data McpTool
106+
= ToolLoadManifest -- Load the k9iser.toml manifest
107+
| ToolGenerate -- Generate K9 contracts from configs
108+
| ToolValidate -- Validate contracts (K9! magic + pedigree)
109+
| ToolApply -- Commit + push regenerated contracts
110+
| ToolClean -- Clean the session
111+
| ToolStatus -- Pipeline health check
112+
113+
||| MCP tool name (for JSON-RPC method name).
114+
public export
115+
toolName : McpTool -> String
116+
toolName ToolLoadManifest = "k9/load_manifest"
117+
toolName ToolGenerate = "k9/generate"
118+
toolName ToolValidate = "k9/validate"
119+
toolName ToolApply = "k9/apply"
120+
toolName ToolClean = "k9/clean"
121+
toolName ToolStatus = "k9/status"
122+
123+
||| Which tools require generated contracts already present.
124+
||| Validate and Apply both require a successful generate first.
125+
public export
126+
toolRequiresGenerate : McpTool -> Bool
127+
toolRequiresGenerate ToolValidate = True
128+
toolRequiresGenerate ToolApply = True
129+
toolRequiresGenerate _ = False
130+
131+
-- ═══════════════════════════════════════════════════════════════════════════
132+
-- C-ABI Exports
133+
-- ═══════════════════════════════════════════════════════════════════════════
134+
135+
||| K9 state to integer.
136+
public export
137+
k9StateToInt : K9State -> Int
138+
k9StateToInt Empty = 0
139+
k9StateToInt ManifestLoaded = 1
140+
k9StateToInt Generated = 2
141+
k9StateToInt Validated = 3
142+
k9StateToInt Applied = 4
143+
k9StateToInt K9Error = 5
144+
145+
||| FFI: Validate a state transition.
146+
export
147+
k9_can_transition : Int -> Int -> Int
148+
k9_can_transition from to =
149+
let fromState = case from of
150+
0 => Empty
151+
1 => ManifestLoaded
152+
2 => Generated
153+
3 => Validated
154+
4 => Applied
155+
_ => K9Error
156+
toState = case to of
157+
0 => Empty
158+
1 => ManifestLoaded
159+
2 => Generated
160+
3 => Validated
161+
4 => Applied
162+
_ => K9Error
163+
in if canTransition fromState toState then 1 else 0
164+
165+
||| FFI: Check if a tool requires generated contracts.
166+
export
167+
k9_tool_requires_generate : Int -> Int
168+
k9_tool_requires_generate 2 = 1 -- ToolValidate
169+
k9_tool_requires_generate 3 = 1 -- ToolApply
170+
k9_tool_requires_generate _ = 0 -- All others do not

‎cartridges/k9iser-mcp/abi/README.adoc‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= k9iser-mcp / abi — Idris2 ABI layer
4+
:orientation: shallow
5+
6+
== Purpose
7+
8+
Cartridge-local protocol types for `k9iser-mcp`. Defines the data, tool, and
9+
transition vocabulary this cartridge speaks. Inherits safety lemmas and the
10+
matrix-cell identifier scheme from the trunk ABI at `src/abi/`.
11+
12+
== Files
13+
14+
* `K9iserMcp/SafeK9iser.idr` — the regeneration pipeline state machine
15+
(`Empty -> ManifestLoaded -> Generated -> Validated -> Applied`), the
16+
`ValidTransition` GADT proving the safety invariants (no apply without
17+
validate; no validate without generate), and the C-ABI exports
18+
(`k9_can_transition`, `k9_tool_requires_generate`).
19+
* `k9iser-mcp.ipkg` — Idris2 package descriptor.
20+
21+
== Safety invariants
22+
23+
. A contract set can only be *applied* (committed back to the repo) from
24+
the `Validated` state — regenerated contracts that failed the canonical
25+
`k9-validate` ruleset (K9! magic + pedigree) can never be pushed.
26+
. A contract set can only be *validated* from `Generated` — there is no
27+
path that validates stale or absent output.
28+
. Generation requires a loaded manifest.
29+
30+
The Zig FFI (`../ffi/k9iser_ffi.zig`) mirrors `canTransition` exactly; the
31+
`state transition validation` test there is the executable cross-check.

‎cartridges/k9iser-mcp/abi/k9iser-mcp.ipkg‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
package k9isermcp
3+
4+
authors = "Jonathan D.A. Jewell"
5+
version = 0.1.0
6+
license = "PMPL-1.0-or-later"
7+
brief = "k9iser-mcp cartridge — K9 contract regeneration pipeline state machine"
8+
9+
sourcedir = "."
10+
modules = K9iserMcp.SafeK9iser
11+
depends = base, contrib

‎cartridges/k9iser-mcp/adapter/README.adoc‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= k9iser-mcp / adapter — protocol bridge
4+
:orientation: shallow
5+
6+
== Purpose
7+
8+
Exposes this cartridge's FFI over the wire protocols declared in
9+
`cartridge.json`. Dispatches tool invocations to the C-ABI exports at
10+
`../ffi/` and formats responses per protocol.
11+
12+
== Files
13+
14+
[cols="1,4"]
15+
|===
16+
| File | Role
17+
18+
| `build.zig` | Zig build graph — depends on the sibling `ffi` target.
19+
| `k9iser_adapter.zig` | Protocol dispatch (134 lines). Tool catalogue matches `cartridge.json`.
20+
| `SIDELINED-*.v.adoc` | V-lang predecessor(s). Not built — V-lang banned 2026-04-10.
21+
|===
22+
23+
== Invariants
24+
25+
* **Stateless** — all state lives behind the FFI, never in the adapter.
26+
* **Response passthrough** — whatever the FFI returns goes back to the wire
27+
unmodified (no embellishment, no silent recovery).
28+
* **Cartridge.json is source of truth** for the tool catalogue; drift between
29+
adapter and manifest is a CI failure.
30+
31+
== Test/proof surface
32+
33+
No inline tests at the adapter layer — protocol routing is exercised by the
34+
trunk seam tests at `ffi/zig/src/seams.zig`.
35+
36+
== Read-first
37+
38+
. `k9iser_adapter.zig` — dispatch function and per-protocol routers.
39+
. `../cartridge.json` — the tool manifest the dispatcher mirrors.

‎cartridges/k9iser-mcp/adapter/build.zig‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// k9iser-mcp/adapter/build.zig
5+
6+
const std = @import("std");
7+
8+
pub fn build(b: *std.Build) void {
9+
const target = b.standardTargetOptions(.{});
10+
const optimize = b.standardOptimizeOption(.{});
11+
12+
const ffi_mod = b.createModule(.{
13+
.root_source_file = b.path("../ffi/k9iser_ffi.zig"),
14+
.target = target,
15+
.optimize = optimize,
16+
});
17+
18+
const adapter_mod = b.createModule(.{
19+
.root_source_file = b.path("k9iser_adapter.zig"),
20+
.target = target,
21+
.optimize = optimize,
22+
});
23+
adapter_mod.addImport("k9iser_ffi", ffi_mod);
24+
25+
const adapter = b.addExecutable(.{
26+
.name = "k9iser_adapter",
27+
.root_module = adapter_mod,
28+
});
29+
b.installArtifact(adapter);
30+
}

0 commit comments

Comments
 (0)