docs(cartridges): deep-annotate 6 lead cartridges (18 per-dir READMEs)

Adds per-directory README.adoc inside abi/, ffi/, and adapter/ for the
six lead cartridges on the D→C path: database-mcp, git-mcp, fleet-mcp,
hypatia-mcp, reposystem-mcp, verisimdb-mcp.

Each README covers the CRG v2.0 deep-annotation checklist for that layer:
purpose, files (with one-line role each), invariants (quoting or
near-quoting source — mutex discipline, state-machine transitions,
bounds checks, conservation proofs, enum hardening), test/proof surface
(inline Zig test count, Idris2 .ipkg if present), and read-first line
ranges so a reviewer can orient without source archaeology.

Honest-by-design: hypatia-mcp, reposystem-mcp, and verisimdb-mcp FFI
layers are labelled "(stubs)" in their README titles and carry an
explicit "Promotion gate" section stating that C-promotion requires
swapping stubs for real backends. This prevents the cartridge-fleet
readiness grade from silently overstating what's implemented.

database-mcp and fleet-mcp are the substantive ones (live SQLite + three
curl-backed query protocols; six-gate quality tracker with mandatory
subset enforcement). git-mcp sits between — full state-machine
implementation, no external backend yet.

This closes one of the two concrete D→C requirements for the
cartridge-fleet row in docs/READINESS.md. The other (active home-context
dogfooding with no known failures for four weeks) accumulates in
docs/practice/DOGFOOD-LOG.adoc.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

cartridges/database-mcp/abi/README.adoc

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= database-mcp / abi — Idris2 ABI layer
+:orientation: deep
+
+== Purpose
+
+Encodes the database **connection state machine** and the **MCP tool catalogue**
+for the database-mcp cartridge. The state machine (`Disconnected → Connected →
+Querying → Connected → Disconnected`, plus `Querying → Error → Disconnected`)
+is the source of truth that the Zig FFI layer mirrors — the ABI proves the
+transition graph is well-formed at the type level via the `ValidTransition`
+indexed type, and the FFI re-implements the same graph as a runtime predicate.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `database-mcp.ipkg`                          | Idris2 package descriptor. Type-check entry point (`idris2 --check database-mcp.ipkg`).
+| `DatabaseMcp/SafeDatabase.idr`               | Whole cartridge in one module. Defines `ConnState`, `ValidTransition` (6 constructors), `canTransition` runtime predicate, `DatabaseBackend` (5 backends + `Custom`), `QuerySafety`, `SafeQuery`, `QueryResult`, `Connection` record, `IsConnected` proof, the 7 `McpTool` constructors, and two C-ABI exports (`db_can_transition`, `db_tool_requires_connection`).
+|===
+
+== Invariants
+
+* `%default total` at module top (line 19) — every definition must be total.
+* `Disconnected → Querying` is **not** in `ValidTransition`; entering a query
+  requires passing through `Connected`. The FFI enforces the same by switching
+  on the current state before every transition.
+* `requiresConnection` marks `ToolConnect` and `ToolListDatabases` as
+  callable without an active connection; every other tool requires one.
+* `backendToInt` and `connStateToInt` are the authoritative encoding the
+  FFI must agree with byte-for-byte.
+
+== Test/proof surface
+
+Type-check only — `idris2 --check DatabaseMcp/SafeDatabase.idr` via the
+`.ipkg`. No inline `test` blocks (that is the FFI's job — see `../ffi/`).
+Proofs here are structural: `ValidTransition` is a GADT with exactly six
+inhabitants.
+
+== Read-first
+
+. `SafeDatabase.idr` lines 22–58 — state machine (`ConnState`, `ValidTransition`, `canTransition`).
+. Lines 64–82 — backend enum and its C-ABI encoding.
+. Lines 129–161 — `Connection` record, `IsConnected` proof, and the seven `McpTool` constructors.
+. Lines 167–196 — the two exported FFI primitives.

cartridges/database-mcp/adapter/README.adoc

@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= database-mcp / adapter — REST/gRPC/GraphQL bridge
+:orientation: deep
+
+== Purpose
+
+Exposes the FFI layer over three protocols so non-Zig callers can drive the
+cartridge. The adapter is **stateless** — it does not hold its own connection
+or slot state; all state lives behind the FFI mutex in `../ffi/`. The adapter
+simply parses an incoming request, routes to a tool name, calls the matching
+FFI export, and serialises the response.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `build.zig`                             | Zig build graph for the adapter binary.
+| `database_adapter.zig`                  | Three-protocol dispatcher. Listens on three ports, maps tool names to FFI calls, returns JSON over HTTP.
+| `SIDELINED-database_adapter.v.adoc`     | Historical V-lang predecessor. Retained for lineage per the 2026-04-10 V-ban transition rule ("V sources MOVE, don't delete"). Not compiled.
+|===
+
+== Invariants
+
+* **Stateless.** No global mutable state beyond protocol listeners. The
+  adapter never caches slot indices; the caller must carry them.
+* **One tool call per HTTP request.** Pipelining or keep-alive batching is
+  out of scope for this layer.
+* **JSON content type.** Responses are always `Content-Type:
+  application/json`; errors are `{"error": "<code>", "message": "<text>"}`.
+* **Port binding.** Each protocol runs on a dedicated port so a single
+  cartridge can simultaneously serve all three without header-based
+  multiplexing.
+
+== Test/proof surface
+
+No inline tests in the adapter (FFI tests cover correctness; the adapter is
+thin scaffolding). Adapter-level integration is exercised by the
+cartridge-matrix tests run from the repo root via `zig build test` in the
+main tree.
+
+== Read-first
+
+. `database_adapter.zig` top of file — port constants and protocol enum.
+. The `dispatch` function — canonical tool-name → FFI-call mapping.
+. The three protocol routers (REST, gRPC-compat, GraphQL) — each is a thin
+  wrapper around `dispatch`.
+. `main` — listener thread spawn.
+
+Skip `SIDELINED-database_adapter.v.adoc` for current work; it documents the
+pre-sidelining design only.

cartridges/database-mcp/ffi/README.adoc

@@ -0,0 +1,73 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= database-mcp / ffi — Zig FFI layer
+:orientation: deep
+
+== Purpose
+
+The Zig implementation of the connection state machine from `../abi/`, plus
+live SQL execution against SQLite (linked via `@cImport("sqlite3.h")`) and
+live VQL / KQL / GQL execution against VeriSimDB / QuandleDB / LithoGlyph via
+child `curl` processes. Exposes the four standard cartridge symbols
+(`boj_cartridge_init`, `boj_cartridge_deinit`, `boj_cartridge_name`,
+`boj_cartridge_version`) and ~20 database-specific `db_*` exports.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `build.zig`          | Zig build graph — produces the loadable shared library plus the unit-test binary.
+| `database_ffi.zig`   | All of it. ~1200 lines. State machine, 16-slot connection pool, SQLite integration, VQL/KQL/GQL curl execution, 24 inline tests.
+| `zig-out/`           | Build artefacts (gitignored).
+|===
+
+== Invariants
+
+* **Mutex discipline.** All reads and writes to the global `connections`
+  array are protected by `var mutex: std.Thread.Mutex`. Every C-ABI export
+  opens with `mutex.lock(); defer mutex.unlock();`. Pure helpers
+  (`isValidTransition`, `appendJsonEscaped`) do not need the lock.
+* **Two-phase pattern** for blocking I/O. `db_execute_vql` / `_kql` / `_gql`
+  release the mutex during the `curl` call and re-acquire it afterwards,
+  then **re-validate slot state** (`active && state == .querying`) before
+  writing the result back. See lines 515–587 for the canonical pattern.
+* **Bounds checks before dereference.** All `*_ptr` / `*_len` pairs reject
+  zero-length and oversize inputs (error codes `-6`, `-8`) before any
+  `@memcpy`. Pointer safety is documented in-line with `SAFETY:` comments.
+* **Enum hardening.** All public exports use `std.meta.intToEnum` rather
+  than `@enumFromInt` on `c_int` arguments, so an invalid enum returns `-1`
+  instead of panicking.
+* **State-machine mirror.** `isValidTransition` (lines 81–88) is the exact
+  graph from `SafeDatabase.idr`. Changes there must land in both files.
+* **Slot capacity** is `MAX_CONNECTIONS = 16`. Exhaustion returns `-1`.
+* **Error codes**: `-1` invalid slot / exhausted, `-2` invalid transition,
+  `-3` no sqlite handle (wrong backend), `-4` sqlite3_exec failed,
+  `-5` output buffer too small, `-6` URL/path empty or too long, `-7` curl
+  failed, `-8` zero-length input/output.
+
+== Test/proof surface
+
+24 inline `test "..."` blocks in `database_ffi.zig` (lines 878–1189). Coverage:
+
+* State machine (lines 878–931): connect, disconnect, double-close, query
+  lifecycle, error recovery, transition validation.
+* SQLite live execution (lines 933–1045): in-memory DB open, execute
+  `CREATE`/`INSERT`/`SELECT`, multiple rows, invalid SQL → error state,
+  non-sqlite slot rejection.
+* VeriSimDB / QuandleDB / LithoGlyph connection lifecycle (lines 1047–1169):
+  URL storage, empty/oversize rejection, query lifecycle via manual state
+  transitions (no live server in test).
+* Wrong-backend rejection (lines 1171–1188).
+
+Run with `cd ffi && zig build test`.
+
+== Read-first
+
+. Lines 14–57 — types and the `ConnectionSlot` struct; note `url_buf[512]` for the HTTP backends.
+. Lines 59–88 — `connections` array, `mutex` declaration, `isValidTransition`.
+. Lines 95–113 — the simplest export (`db_connect`); read before the sqlite/verisimdb variants.
+. Lines 324–401 — `db_execute_sql` — full state-machine-guarded sqlite exec with JSON serialisation.
+. Lines 515–641 — `db_execute_vql` + `runCurlPost` — the two-phase lock pattern for blocking I/O.
+. Lines 842–872 — the standard cartridge-interface exports required by the BoJ loader.

cartridges/fleet-mcp/abi/README.adoc

@@ -0,0 +1,46 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= fleet-mcp / abi — Idris2 ABI layer
+:orientation: deep
+
+== Purpose
+
+Encodes the **six quality gates** (Rhodibot, Echidnabot, Sustainabot,
+Panicbot, Glambot, Seambot) and a `FleetCertified` indexed type that is
+inhabited only when every gate has passed. `deriveStatus` folds a list of
+gate results into one of four `RepoStatus` values so the runtime can publish
+a repo's health in one byte.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `fleet-mcp.ipkg`                    | Idris2 package descriptor. `modules = FleetMcp.SafeFleet`, `depends = base, contrib`.
+| `FleetMcp/SafeFleet.idr`            | `BotGate` enum, `RepoStatus` enum, the indexed type `FleetCertified` with single constructor `FullyVerified`, record `GateScanResult`, helper predicates `hasMandatoryGates` and `hasAllGates`, and `deriveStatus`.
+|===
+
+== Invariants
+
+* **Mandatory subset** = [`Rhodibot`, `Echidnabot`, `Panicbot`] (line 115).
+  A release requires *all three* to pass.
+* **Status derivation** (lines 131–135):
+  * all six pass → `Healthy`
+  * mandatory three pass but not all six → `Degraded`
+  * any gate passed → `Scanning`
+  * none passed → `Unscanned`
+* **Single constructor** for `FleetCertified`: `FullyVerified` exists only
+  when all six gates have produced a pass result. You cannot fabricate a
+  `FleetCertified` by pattern-matching anything else.
+* Gate-integer encoding excludes `-1` via `mapMaybe` (lines 168, 175).
+
+== Test/proof surface
+
+Type-check only via `.ipkg`. No inline `test` blocks.
+
+== Read-first
+
+. Lines 25–60 — `BotGate` enum and its integer encoding.
+. Lines 100–127 — `FleetCertified` type, `hasMandatoryGates`, `hasAllGates`.
+. Lines 143–158 — `GateScanResult`, `passedGates`, and `deriveStatus`.

cartridges/fleet-mcp/adapter/README.adoc

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= fleet-mcp / adapter — REST/gRPC/GraphQL bridge
+:orientation: deep
+
+== Purpose
+
+Exposes the fleet-mcp FFI over three protocols: REST on **9235**, gRPC-compat
+on **9236**, GraphQL on **9237**. Stateless; all gate state lives behind the
+FFI mutex in `../ffi/`.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `build.zig`                          | Zig build graph for the adapter binary.
+| `fleet_adapter.zig`                  | `dispatch` routes tool names to FFI calls. Tools: `fleet_record_gate`, `fleet_bot_status`, `fleet_gate_score`, `fleet_has_mandatory`, `fleet_fleet_status`.
+| `SIDELINED-fleet_adapter.v.adoc`     | Archived V-lang predecessor. Not built.
+|===
+
+== Invariants
+
+* **Stateless**; adapter holds no gate state of its own.
+* One gate-query per HTTP request; no pipelining.
+
+== Test/proof surface
+
+No inline tests; correctness lives in the FFI.
+
+== Read-first
+
+. Lines 27–44 — `dispatch` routing.
+. Lines 47–78 — protocol routers (REST/gRPC/GraphQL).

cartridges/fleet-mcp/ffi/README.adoc

@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= fleet-mcp / ffi — Zig FFI layer
+:orientation: deep
+
+== Purpose
+
+Runtime gate tracker. Mutex-guarded arrays hold per-gate pass/fail booleans
+and per-gate scores (0–100). Exposes the ABI's three predicates
+(`fleet_has_mandatory`, `fleet_has_all`, derived `fleet_status`) over the
+C-ABI so the BoJ server can ask "is this repo release-ready?" with one call.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `build.zig`                  | Zig build graph (shared library + test binary).
+| `fleet_ffi.zig`              | Gate-state arrays, mutex, the C-ABI exports `fleet_record_gate`, `fleet_has_mandatory`, `fleet_has_all`, `fleet_status`, `fleet_gate_score`, and the four `boj_cartridge_*` symbols.
+| `zig-out/`                   | Build artefacts (gitignored).
+|===
+
+== Invariants
+
+* **Mutex discipline** on every gate read/write (lines 45, 53, 64, 72, 82, 102).
+* **Mandatory** = indices 0, 1, 3 (Rhodibot, Echidnabot, Panicbot). The
+  check lives at line 68 — changing mandatory composition means changing
+  those three index constants.
+* **Deadlock avoidance.** `fleet_status` inlines the mandatory/all checks
+  (lines 85–98) rather than calling `fleet_has_mandatory` / `fleet_has_all`
+  which would re-acquire the mutex.
+* Gate indices arriving from callers use the 1–6 range from the ABI;
+  internal arrays are 0–5.
+
+== Test/proof surface
+
+4 inline `test "..."` blocks (lines 143–185):
+
+* initial state — no gates recorded, status is `Unscanned`.
+* mandatory gates insufficient until Panicbot is added (tests the 0/1/3
+  triple specifically).
+* all six gates → `Healthy`.
+* failed gate prevents `Healthy` even when mandatory still satisfied.
+
+Run with `cd ffi && zig build test`.
+
+== Read-first
+
+. Lines 37–49 — gate-result arrays, scores, and the mutex.
+. Lines 64–79 — `fleet_has_mandatory` and `fleet_has_all`.
+. Lines 82–99 — `fleet_status` with its inline (non-re-locking) logic.
+. Lines 143–185 — tests.

cartridges/git-mcp/abi/README.adoc

@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= git-mcp / abi — Idris2 ABI layer
+:orientation: deep
+
+== Purpose
+
+Encodes the forge-session state machine
+(`Unauthenticated → Authenticated → RepoSelected → Operating → RepoSelected`)
+as an Idris2 indexed type plus a parallel runtime predicate. The ABI is the
+source-of-truth spec; the FFI implements the same graph in Zig. Tools are
+tagged with their state precondition so the FFI can refuse an operation that
+would require a `RepoSelected` session when no repo has been selected.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `git-mcp.ipkg`                | Idris2 package descriptor. `modules = GitMcp.SafeGit`, `depends = base, contrib`. Type-check with `idris2 --check git-mcp.ipkg`.
+| `GitMcp/SafeGit.idr`          | 5-state `GitState`, `ValidTransition` type proof, `ForgeSession` record with state tag, `HasRepo` proof, the `McpTool` enum, `requiresRepo` predicate, and C-ABI exports `git_can_transition`, `git_tool_requires_repo`.
+|===
+
+== Invariants
+
+* Linear session pipeline: the state machine cannot jump — e.g. a tool that
+  needs `RepoSelected` cannot be called from `Authenticated` without going
+  through `git_select_repo`.
+* Read-only ops (`ToolStatus`, `ToolLog`, `ToolDiff`) do **not** require a
+  selected repo; mutating ops (`ToolCreatePR`, `ToolPush`, `ToolCreateBranch`)
+  do. See `requiresRepo` predicate.
+* Module commentary at line 26 pins the intended progression:
+  `Unauthenticated -> Authenticated -> RepoSelected -> Operating -> RepoSelected`.
+
+== Test/proof surface
+
+Type-check only (`idris2 --check`). No inline `test` blocks.
+
+== Read-first
+
+. Lines 22–63 — `GitState`, `ValidTransition` constructors, and `canTransition`.
+. Lines 89–104 — `ForgeSession` record and `HasRepo` proof.
+. Lines 113–143 — `McpTool` constructors and `requiresRepo` predicate.

cartridges/git-mcp/adapter/README.adoc

@@ -0,0 +1,37 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= git-mcp / adapter — REST/gRPC/GraphQL bridge
+:orientation: deep
+
+== Purpose
+
+Exposes the git-mcp FFI over three protocols: REST on **9250**, gRPC-compat on
+**9251**, GraphQL on **9252**. Stateless — the session state lives behind the
+FFI mutex in `../ffi/`.
+
+== Files
+
+[cols="1,4"]
+|===
+| File | Role
+
+| `build.zig`                         | Zig build graph for the adapter binary.
+| `git_adapter.zig`                   | Three listener threads spawned from `main`. `dispatchRest`, `dispatchGrpc`, and `dispatchGraphql` map a path or body shape to a tool name, then call the shared `dispatch` stub that forwards to the FFI. Tool set: `git_authenticate`, `git_select_repo`, `git_status`, `git_log`, `git_diff`, `git_create_branch`, `git_push`.
+| `SIDELINED-git_adapter.v.adoc`      | Archived V-lang predecessor. Kept for lineage; not built.
+|===
+
+== Invariants
+
+* **Stateless** — the adapter carries no session data.
+* **Port binding** — three sibling ports, no header-multiplexing.
+* Responses always `application/json`; 200 success, 404 unknown tool.
+
+== Test/proof surface
+
+No inline tests. Adapter is integration scaffolding.
+
+== Read-first
+
+. Lines 27–51 — `dispatch` mapping (tool name → FFI call).
+. Lines 53–70 — REST/gRPC routing.
+. Lines 125–144 — listener loop and `main`.