Skip to content

Commit b5245ae

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(007-mcp): install cartridge + register oo7_mcp in CartridgeData.idr
Installs 007-mcp from 007-lang into the boj-server cartridge matrix. All 11 files copied (manifests, Zig FFI + adapter sources, Idris2 ABI, A2ML schema, ReScript docs). CartridgeData.idr gains oo7_mcp in the Agent domain section (tier Ayo); bojCatalogue updated to 5 Agent entries. The FFI already implements coord_report_outcome for clean session exit (coordDeregister landed in 007-lang c030966). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 97e58ac commit b5245ae

11 files changed

Lines changed: 3178 additions & 2 deletions

File tree

‎cartridges/007-mcp/README.adoc‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
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+
= 007-mcp — 007 agent-meta-language BoJ cartridge
5+
:toc: left
6+
:source-highlighter: rouge
7+
8+
The `007-mcp` cartridge surfaces the full `oo7` CLI + 007-lang methodology
9+
as MCP tools, so any AI session entering 007-lang automatically gets the
10+
right context without having to recall it.
11+
12+
== Why this lives here (not in boj-server)
13+
14+
Per design-log decision DD-24, cartridge source stays next to the code
15+
it exposes. The install hook (see top-level `Justfile` recipe
16+
`cartridge-install`) builds the adapter and FFI, copies the artefacts
17+
into `boj-server/cartridges/007-mcp/`, and commits in the boj-server
18+
repo separately. Two repos, two commits, one seam.
19+
20+
== Design-log anchors
21+
22+
Anything here tracks these entries in `Desktop/COORD-MCP-DESIGN-LOG.md`:
23+
24+
* *DD-24* — source location + install hook
25+
* *DD-25* — expose the full CLI (no curated subset)
26+
* *DD-26* — memory auto-lift via dynamic tag-indexed lookup
27+
* *DD-31* — VeriSimDB FFI is stubs today; memory auto-lift uses the
28+
static-mapping fallback option (b) and is wired for an in-place swap
29+
when VeriSimDB lands.
30+
31+
== Loopback-only bind
32+
33+
The adapter binds `127.0.0.1:1066`. The port is locked at the Idris2
34+
ABI layer (`abi/Oo7Mcp/SafeCli.idr :: cartridgeBind`), where
35+
`BindAddress` carries an `IsLoopback` proof. The sum type has exactly
36+
two constructors — `Ipv4Loopback` and `Ipv6Loopback` — so naming any
37+
non-loopback address is type-impossible.
38+
39+
== Layout
40+
41+
[source]
42+
----
43+
007-mcp/
44+
├── abi/Oo7Mcp/SafeCli.idr # Idris2 ABI — loopback proof + state machine + risk table
45+
├── ffi/
46+
│ ├── oo7_mcp_ffi.zig # Zig FFI — recipe dispatch, lifecycle state, coord client
47+
│ └── build.zig # Zig 0.15+ build (self-contained)
48+
├── adapter/
49+
│ ├── oo7_adapter.zig # HTTP-REST surface at 127.0.0.1:1066
50+
│ └── build.zig
51+
├── schemas/
52+
│ └── memory-tag-map.a2ml # Static tag → memory-file index (DD-26 option b)
53+
├── docs/ # Rationale + per-tool usage notes
54+
├── cartridge.ncl # Nickel source-of-truth manifest
55+
└── README.adoc # You are here
56+
----
57+
58+
== Tool surface
59+
60+
Seventy-two MCP tools:
61+
62+
* 2 lifecycle — `oo7_on_enter`, `oo7_on_exit`
63+
* 5 runtime — `oo7_parse`, `oo7_run`, `oo7_trace`, `oo7_demo`, `oo7_run_examples`
64+
* 7 build — `oo7_build`, `oo7_build_cli{,_release}`, `oo7_build_watch`,
65+
`oo7_release`, `oo7_clean{,_all}`
66+
* 7 test — `oo7_test{,_parser,_eval,_trace,_aspect,_filter,_verbose}`
67+
* 6 quality gates — `oo7_check`, `oo7_ci`, `oo7_preflight`, `oo7_fmt`,
68+
`oo7_fmt_check`, `oo7_lint`
69+
* 3 dependency audits — `oo7_audit`, `oo7_deny`, `oo7_outdated`
70+
* 1 pre-commit scan — `oo7_assail`
71+
* 2 toolchain — `oo7_doctor`, `oo7_heal`
72+
* 17 contractile — `oo7_contractile_check`, `oo7_must_*`, `oo7_trust_*`,
73+
`oo7_intend_list*`, `oo7_dust_*`
74+
* 3 verification — `oo7_verify{,_harvard,_template}`
75+
* 2 grammar/spec — `oo7_grammar_check`, `oo7_spec_check`
76+
* 4 proof suite — `oo7_canonical_proof_suite`, `oo7_v{0,1}_differential{,_full}`
77+
* 2 Groove — `oo7_groove_{daemon,setup}`
78+
* 3 containers — `oo7_container_{build,run,verify}`
79+
* 8 meta — `oo7_docs`, `oo7_cookbook`, `oo7_info`, `oo7_tour`,
80+
`oo7_help{,_me}`, `oo7_self_assess`, plus `oo7_crg_{badge,grade}`
81+
82+
Each tool maps 1:1 to a Justfile recipe. Lifecycle tools are handled
83+
natively by the adapter (coord-peer handshake + 6a2 load + memory
84+
auto-lift on enter; drift check + deregister on exit).
85+
86+
== Risk table (DD-5 ladder)
87+
88+
Most tools default to Tier 1 (logged, no gate). Promotions:
89+
90+
[cols="1,1,2",options="header"]
91+
|===
92+
| Tool | Tier | Why
93+
| `oo7_dust_source_rollback` | 3 | Destructive — reverts uncommitted work
94+
| `oo7_clean_all` | 2 | Drops generated artefacts outside target/
95+
| `oo7_container_run` | 3 | Long-running with host mounts
96+
| `oo7_groove_daemon` | 3 | Starts a daemon with a network socket
97+
|===
98+
99+
`supervised` peers never reach the Tier-3 path — the adapter rejects
100+
before invoking FFI.
101+
102+
== Running locally
103+
104+
[source,bash]
105+
----
106+
# Build FFI + adapter.
107+
cd cartridges/007-mcp/ffi && zig build test && zig build
108+
cd ../adapter && zig build
109+
110+
# Start the adapter (loopback 127.0.0.1:1066).
111+
OO7_WORKTREE=/var/mnt/eclipse/repos/007-lang ./zig-out/bin/oo7_adapter
112+
113+
# Probe health.
114+
curl -s http://127.0.0.1:1066/health
115+
116+
# Fire the OnEnter hook.
117+
curl -s -X POST http://127.0.0.1:1066/tools/oo7_on_enter \
118+
-d '{"session_hint":"afternoon m3-dispatch work"}'
119+
----
120+
121+
== Install into boj-server
122+
123+
From the 007-lang repo root:
124+
125+
[source,bash]
126+
----
127+
just cartridge-install # build + deploy to ../boj-server/cartridges/007-mcp/
128+
----
129+
130+
See the top-level `Justfile` for the install-hook recipe.
131+
132+
== Swap-in path for VeriSimDB
133+
134+
When `verisimdb-mcp`'s FFI is real (design-log Task #7b), replace the
135+
body of `memoryAutolift` in `ffi/oo7_mcp_ffi.zig` with a VeriSimDB
136+
tag-index query. The cartridge contract (return shape, tag set) stays
137+
constant — only the lookup backend changes.

‎cartridges/007-mcp/abi/Oo7Mcp/SafeCli.idr‎

Lines changed: 241 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,241 @@
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+
-- Oo7Mcp.SafeCli — Type-safe ABI for the 007-mcp cartridge.
5+
--
6+
-- Three compile-time invariants:
7+
--
8+
-- 1. Loopback-only bind. The `IsLoopback` sum type has exactly two
9+
-- constructors (Ipv4Loopback, Ipv6Loopback). Every BindAddress
10+
-- value threads an `IsLoopback` proof, so constructing a bind to
11+
-- any non-loopback address is type-impossible. Mirrors the same
12+
-- pattern used by local-coord-mcp.
13+
--
14+
-- 2. Lifecycle ordering. The `SessionState` state machine forces
15+
-- `OnEnter` before any tool dispatch and `OnExit` before
16+
-- deregistration. `ValidTransition` enumerates exactly the legal
17+
-- edges — anything else is a type error in well-typed callers.
18+
--
19+
-- 3. Risk-gated destructive tools. `ToolRisk` lifts the DD-5 risk
20+
-- ladder into Idris2. The `dust_source_rollback` tool is Tier 3
21+
-- (hard gate); the adapter rejects invocations that lack a
22+
-- supervisor-approval witness.
23+
24+
module Oo7Mcp.SafeCli
25+
26+
%default total
27+
28+
-- ---------------------------------------------------------------------------
29+
-- Loopback-only bind proof
30+
-- ---------------------------------------------------------------------------
31+
32+
||| Witness that a bind address is on the local loopback interface.
33+
||| The only two constructors are IPv4 127.0.0.1 and IPv6 ::1.
34+
||| There is intentionally no constructor for any other address, so
35+
||| `BindAddress` values cannot name a non-loopback target.
36+
public export
37+
data IsLoopback : Type where
38+
Ipv4Loopback : IsLoopback -- 127.0.0.1
39+
Ipv6Loopback : IsLoopback -- ::1
40+
41+
||| A bind address carrying proof of loopback-ness.
42+
||| The Idris2 ABI never constructs a BindAddress without this proof,
43+
||| so the adapter's runtime bind inherits the compile-time guarantee.
44+
public export
45+
record BindAddress where
46+
constructor MkBindAddress
47+
host : String
48+
port : Int
49+
proof : IsLoopback
50+
51+
||| The one and only production bind — 127.0.0.1:1066.
52+
||| Port 1066 chosen in design-log decision-log 2026-04-20.
53+
public export
54+
cartridgeBind : BindAddress
55+
cartridgeBind = MkBindAddress "127.0.0.1" 1066 Ipv4Loopback
56+
57+
||| C-ABI export: fetch the host as a cstring.
58+
||| The FFI wrapper reads this at server-start time.
59+
export
60+
oo7_mcp_bind_host : String
61+
oo7_mcp_bind_host = cartridgeBind.host
62+
63+
export
64+
oo7_mcp_bind_port : Int
65+
oo7_mcp_bind_port = cartridgeBind.port
66+
67+
||| Encode the loopback proof tag for C consumption: 4 or 6.
68+
||| Lets the adapter sanity-check that the proof travelled across FFI.
69+
export
70+
oo7_mcp_bind_family : Int
71+
oo7_mcp_bind_family = case cartridgeBind.proof of
72+
Ipv4Loopback => 4
73+
Ipv6Loopback => 6
74+
75+
-- ---------------------------------------------------------------------------
76+
-- Session state machine
77+
-- ---------------------------------------------------------------------------
78+
79+
||| Session states for a 007-mcp cartridge instance.
80+
|||
81+
||| Fresh — constructed, no lifecycle hook run yet
82+
||| Registered — OnEnter has registered this session with local-coord-mcp
83+
||| and loaded the 6a2 methodology pack
84+
||| InvokingTool — a tool dispatch is in flight (serialised)
85+
||| Deregistered — OnExit has released claims and deregistered
86+
||| Degraded — local-coord-mcp was unreachable during OnEnter; the
87+
||| cartridge operates in local-only mode (no coord ops)
88+
public export
89+
data SessionState
90+
= Fresh
91+
| Registered
92+
| InvokingTool
93+
| Deregistered
94+
| Degraded
95+
96+
||| Proof that a state transition is valid.
97+
public export
98+
data ValidTransition : SessionState -> SessionState -> Type where
99+
EnterOk : ValidTransition Fresh Registered
100+
EnterDegrade : ValidTransition Fresh Degraded
101+
BeginDispatch : ValidTransition Registered InvokingTool
102+
BeginDispatchD : ValidTransition Degraded InvokingTool -- local-only tools still run
103+
EndDispatchR : ValidTransition InvokingTool Registered
104+
EndDispatchD : ValidTransition InvokingTool Degraded
105+
ExitR : ValidTransition Registered Deregistered
106+
ExitD : ValidTransition Degraded Deregistered
107+
108+
||| Encode session state as C-compatible integer for FFI boundary.
109+
export
110+
sessionStateToInt : SessionState -> Int
111+
sessionStateToInt Fresh = 0
112+
sessionStateToInt Registered = 1
113+
sessionStateToInt InvokingTool = 2
114+
sessionStateToInt Deregistered = 3
115+
sessionStateToInt Degraded = 4
116+
117+
||| Decode integer back to session state.
118+
export
119+
intToSessionState : Int -> Maybe SessionState
120+
intToSessionState 0 = Just Fresh
121+
intToSessionState 1 = Just Registered
122+
intToSessionState 2 = Just InvokingTool
123+
intToSessionState 3 = Just Deregistered
124+
intToSessionState 4 = Just Degraded
125+
intToSessionState _ = Nothing
126+
127+
||| C-ABI export: is a transition permitted?
128+
||| Returns 1 if yes, 0 if no — consumed by the Zig adapter's guard
129+
||| before flipping its own state atomic.
130+
export
131+
oo7_mcp_can_transition : Int -> Int -> Int
132+
oo7_mcp_can_transition from to =
133+
case (intToSessionState from, intToSessionState to) of
134+
(Just Fresh, Just Registered) => 1
135+
(Just Fresh, Just Degraded) => 1
136+
(Just Registered, Just InvokingTool) => 1
137+
(Just Degraded, Just InvokingTool) => 1
138+
(Just InvokingTool, Just Registered) => 1
139+
(Just InvokingTool, Just Degraded) => 1
140+
(Just Registered, Just Deregistered) => 1
141+
(Just Degraded, Just Deregistered) => 1
142+
_ => 0
143+
144+
-- ---------------------------------------------------------------------------
145+
-- Tool risk classification (DD-5 risk ladder)
146+
-- ---------------------------------------------------------------------------
147+
148+
||| Risk tier for a tool invocation.
149+
||| Tier 0 — free (status, reads)
150+
||| Tier 1 — logged (runtime reads, tests, builds, lint)
151+
||| Tier 2 — light gate (container builds, docs generate, heal)
152+
||| Tier 3 — hard gate (rollback, destructive clean, container-run w/ privileged)
153+
||| Tier 4 — forbidden for supervised role (NONE on 007-mcp — no public-repo writes,
154+
||| no license touches here; Tier 4 is reserved for future tools only)
155+
public export
156+
data ToolRisk
157+
= Tier0
158+
| Tier1
159+
| Tier2
160+
| Tier3
161+
| Tier4
162+
163+
export
164+
tierToInt : ToolRisk -> Int
165+
tierToInt Tier0 = 0
166+
tierToInt Tier1 = 1
167+
tierToInt Tier2 = 2
168+
tierToInt Tier3 = 3
169+
tierToInt Tier4 = 4
170+
171+
-- ---------------------------------------------------------------------------
172+
-- Tool taxonomy
173+
-- ---------------------------------------------------------------------------
174+
175+
||| High-level categories for the 007-mcp tool surface. Finer-grained
176+
||| names live in the Zig dispatcher; this enum is the compile-time
177+
||| coarse classification used for risk inference.
178+
public export
179+
data ToolCategory
180+
= Lifecycle -- on-enter, on-exit
181+
| Runtime -- parse, run, trace, demo
182+
| BuildArtifact -- build, clean, docs, release
183+
| Test -- test*, check, ci, preflight
184+
| Quality -- lint, fmt, audit, deny, outdated, assail
185+
| Contractile -- must/trust/intend/dust/bust/adjust
186+
| Verification -- verify*, grammar-check, spec-check
187+
| ProofSuite -- canonical-proof-suite, v0/v1 differential
188+
| Groove -- groove-daemon, groove-setup
189+
| Container -- container-build, container-run, container-verify
190+
| Meta -- info, tour, help, self-assess, cookbook, crg-*
191+
| ToolchainMgmt -- doctor, heal
192+
193+
||| Default risk tier per category. The dispatcher can promote
194+
||| individual tools (see riskPromotion below) for destructive variants.
195+
export
196+
categoryDefaultRisk : ToolCategory -> ToolRisk
197+
categoryDefaultRisk Lifecycle = Tier0 -- lifecycle hooks are idempotent reads
198+
categoryDefaultRisk Runtime = Tier1
199+
categoryDefaultRisk BuildArtifact = Tier1
200+
categoryDefaultRisk Test = Tier1
201+
categoryDefaultRisk Quality = Tier1
202+
categoryDefaultRisk Contractile = Tier1
203+
categoryDefaultRisk Verification = Tier0
204+
categoryDefaultRisk ProofSuite = Tier1
205+
categoryDefaultRisk Groove = Tier2 -- starts a daemon, long-running
206+
categoryDefaultRisk Container = Tier2
207+
categoryDefaultRisk Meta = Tier0
208+
categoryDefaultRisk ToolchainMgmt = Tier2 -- `heal` mutates system state
209+
210+
||| Promotion table for specific tools whose risk exceeds their
211+
||| category default. Names are the canonical MCP tool names from
212+
||| cartridge.ncl.
213+
export
214+
riskPromotion : String -> Maybe ToolRisk
215+
riskPromotion "oo7_dust_source_rollback" = Just Tier3
216+
riskPromotion "oo7_clean_all" = Just Tier2
217+
riskPromotion "oo7_container_run" = Just Tier3
218+
riskPromotion "oo7_groove_daemon" = Just Tier3
219+
riskPromotion _ = Nothing
220+
221+
-- ---------------------------------------------------------------------------
222+
-- Counts for the FFI header generator
223+
-- ---------------------------------------------------------------------------
224+
225+
||| Total tool count — kept in sync with cartridge.ncl.
226+
||| 2 lifecycle + 5 runtime + 7 build + 7 test + 6 quality + 3 audits
227+
||| + 1 assail + 2 toolchain + 17 contractile + 3 verification
228+
||| + 2 grammar/spec + 4 proof suite + 2 groove + 3 container
229+
||| + 8 meta + 2 crg = 72 (re-derived each version bump)
230+
export
231+
toolCount : Nat
232+
toolCount = 72
233+
234+
||| Fixed-width wire counts (useful for FFI buffer sizing).
235+
export
236+
maxToolNameLen : Nat
237+
maxToolNameLen = 48
238+
239+
export
240+
maxArgStringLen : Nat
241+
maxArgStringLen = 4096

0 commit comments

Comments
 (0)