|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# 14. Cross-cartridge composition safety — defining what we mean and how to prove it |
| 5 | + |
| 6 | +Date: 2026-05-20 |
| 7 | + |
| 8 | +## Status |
| 9 | + |
| 10 | +Proposed (RFC — implementation tracked in epic #87 Tier C item 12; this |
| 11 | +ADR is the framing document, not a build plan) |
| 12 | + |
| 13 | +## Context |
| 14 | + |
| 15 | +The existing Idris2 ABI proves a lot for **individual** cartridges: |
| 16 | + |
| 17 | +- `Boj.CartridgeDispatch` (BJ1) shows the dispatcher is type-safe: |
| 18 | + `ProtocolMatch + ReadinessGuard + Disjointness` — well-typed dispatch |
| 19 | + cannot route a request to a cartridge that doesn't advertise the |
| 20 | + protocol or that hasn't passed the safety gate (`IsUnbreakable`). |
| 21 | +- `Boj.Catalogue` defines `IsUnbreakable` as the gate that admits only |
| 22 | + `Ready` cartridges. |
| 23 | +- Per-cartridge `Safe*.idr` modules (`SafeHTTP`, `SafeCORS`, `SafeAPIKey`, |
| 24 | + `SafeWebSocket`, `SafePromptInjection`, `Federation`, |
| 25 | + `CredentialIsolation`, `APIContractCoverage`) discharge the P-01..P-07 |
| 26 | + proof obligations local to that cartridge. |
| 27 | + |
| 28 | +The 2026-05-18 audit (`PROOF-NEEDS.md`) records 5 remaining `believe_me` |
| 29 | +sites, all class (J) — principled assumptions over Idris2 0.8.0's opaque |
| 30 | +`Char`/`String` primitives. Within the per-cartridge ABI surface, the |
| 31 | +proof debt is closed. |
| 32 | + |
| 33 | +What is **not** proved is what happens when one cartridge calls another. |
| 34 | +Concretely: BoJ exposes a 5th-standard-symbol Zig FFI export per |
| 35 | +cartridge — `boj_cartridge_invoke(tool, args_json, out, out_len)` — and |
| 36 | +the bridge happily lets cartridge A's handler call cartridge B's |
| 37 | +`boj_cartridge_invoke` to compose tools. ADR-0006 defines the invoke |
| 38 | +surface; ADR-0009 (sandbox cartridge, RFC-only as of this writing — |
| 39 | +`cartridges/sandbox-mcp/` does not yet exist on disk) and ADR-0010 |
| 40 | +(cross-machine coord federation) both lean on composition without |
| 41 | +defining what makes a composition *safe*. |
| 42 | + |
| 43 | +We have a hole: per-cartridge invariants do not compose automatically. |
| 44 | +If cartridge A's tool requires `IsUnbreakable` and produces JSON whose |
| 45 | +shape satisfies its own `SafeHTTP` contract, that says nothing about |
| 46 | +whether the resulting JSON, fed into cartridge B's |
| 47 | +`boj_cartridge_invoke`, satisfies B's preconditions. The Idris2 type |
| 48 | +system can only check this if the cartridges share a typed composition |
| 49 | +boundary; today they share only bytes. |
| 50 | + |
| 51 | +This ADR scopes the problem so a campaign can attack it. |
| 52 | + |
| 53 | +## Decision (framing, not implementation) |
| 54 | + |
| 55 | +Define **composition safety** for BoJ as a **two-level contract**, with |
| 56 | +the Idris2 ABI carrying the *static* level and a Nickel-encoded policy |
| 57 | +layer (via ADR-0007's `policy-mcp` PDP) carrying the *dynamic* level. |
| 58 | +Discharge them in a first pair, then generalise. |
| 59 | + |
| 60 | +### Level 1 — Static (Idris2): typed composition envelope |
| 61 | + |
| 62 | +Introduce a new module `Boj.Composition` that lifts the per-cartridge |
| 63 | +ABI obligations into a composition-aware envelope: |
| 64 | + |
| 65 | +```idris |
| 66 | +||| A typed inter-cartridge invocation. |
| 67 | +||| Carries proofs that the source cartridge is Ready, the target |
| 68 | +||| cartridge is Ready, the requested tool is in the target's |
| 69 | +||| advertised tool list, and the marshalled args satisfy the target's |
| 70 | +||| input contract. |
| 71 | +public export |
| 72 | +record InvocationOf (src, tgt : Cartridge) (tool : ToolName) where |
| 73 | + constructor MkInvocation |
| 74 | + srcReady : IsUnbreakable src |
| 75 | + tgtReady : IsUnbreakable tgt |
| 76 | + toolValid : tool `elem` advertisedTools tgt = True |
| 77 | + argsOk : ArgsContract tgt tool args |
| 78 | +``` |
| 79 | + |
| 80 | +A composition is **statically safe** iff `boj_cartridge_invoke` only |
| 81 | +fires when the caller can construct a witness of `InvocationOf src tgt |
| 82 | +tool`. The dispatcher (BJ1) already proves the field-2 and field-3 |
| 83 | +analogues for *external* requests; this lifts the same proofs into the |
| 84 | +*internal* invocation path. |
| 85 | + |
| 86 | +`ArgsContract` is the open piece — it has to be defined per-cartridge, |
| 87 | +mirroring whatever invariants the target's local `Safe*.idr` already |
| 88 | +encodes. For the first proof pair we propose mechanically deriving it |
| 89 | +from each cartridge's existing JSON-schema in `cartridge.json`. |
| 90 | + |
| 91 | +### Level 2 — Dynamic (Nickel policy contract): composition admissibility |
| 92 | + |
| 93 | +The static envelope says *if* you can typecheck the invocation, it's |
| 94 | +shape-safe. It does not say the invocation is *policy*-safe — e.g. a |
| 95 | +Teranga-tier cartridge should not be allowed to invoke an |
| 96 | +Ayo-tier cartridge in a way that elevates privilege. That's the job of |
| 97 | +the PDP introduced by ADR-0007. |
| 98 | + |
| 99 | +Extend `policy-mcp`'s Nickel schema with a `compositions` block: |
| 100 | + |
| 101 | +```nickel |
| 102 | +compositions = { |
| 103 | + # Allow panic-attack -> vordr (untrusted-execution flow per ADR-0009) |
| 104 | + "panic-attack-mcp".allows_invoking = ["vordr-mcp"], |
| 105 | + "panic-attack-mcp".max_call_depth = 1, |
| 106 | + "panic-attack-mcp".target_must_be_tier_lte = 2, |
| 107 | +
|
| 108 | + # Deny ayo -> teranga (privilege elevation) |
| 109 | + "*-ayo".allows_invoking_tier_lt_self = false, |
| 110 | +} |
| 111 | +``` |
| 112 | + |
| 113 | +The bridge's `hardeningGate` consults the PDP on every internal |
| 114 | +invocation, the same way it already consults it for external dispatch. |
| 115 | + |
| 116 | +### First proof pair (recommended, with caveat) |
| 117 | + |
| 118 | +The prompt suggested `panic-attack-mcp → sandbox-mcp → vordr-mcp` as the |
| 119 | +canonical untrusted-execution chain. Two of the three exist on disk |
| 120 | +today: |
| 121 | + |
| 122 | +- `cartridges/panic-attack-mcp/` — exists |
| 123 | +- `cartridges/sandbox-mcp/` — **does not exist**; ADR-0009 proposes |
| 124 | + it but no implementation has landed |
| 125 | +- `cartridges/vordr-mcp/` — exists |
| 126 | + |
| 127 | +Therefore the first composition pair to discharge is **`panic-attack-mcp |
| 128 | +→ vordr-mcp`** (a real pair, both Teranga / Shield, both with extant |
| 129 | +ABI). The three-cartridge chain remains the eventual target; sandbox-mcp |
| 130 | +needs to be built (per ADR-0009) before the longer chain can be proved. |
| 131 | + |
| 132 | +### What we are explicitly **not** doing |
| 133 | + |
| 134 | +- **Not lifting all cartridges into a single shared Idris2 module.** |
| 135 | + That would be a multi-year refactor. `InvocationOf` is parameterised |
| 136 | + on `Cartridge` (already defined in `Boj.Catalogue`) and pulls the |
| 137 | + per-cartridge contract via a typeclass / interface, not by source-level |
| 138 | + unification. |
| 139 | +- **Not making every existing cross-cartridge call retroactively |
| 140 | + proven.** Existing internal invocations stay on the untyped byte |
| 141 | + path; new ones go through `InvocationOf` once it lands. Migration is |
| 142 | + per-pair, prioritised by trust-tier risk. |
| 143 | +- **Not weakening any existing single-cartridge proof.** If a P-01..P-07 |
| 144 | + obligation conflicts with the composition envelope, the obligation is |
| 145 | + right and the envelope shape is wrong. |
| 146 | + |
| 147 | +## Discharge mechanism — sub-RFCs and PRs |
| 148 | + |
| 149 | +The campaign decomposes into roughly six sub-issues, each its own PR: |
| 150 | + |
| 151 | +1. **`Boj.Composition` skeleton.** Define `InvocationOf`, `ArgsContract` |
| 152 | + as an interface, and helpers. No cartridge wired up. Build-green via |
| 153 | + `idris2 --check`. Refs item 12. |
| 154 | +2. **First pair: `panic-attack-mcp → vordr-mcp` static proof.** Provide |
| 155 | + `ArgsContract` instances for both cartridges' tools, prove one real |
| 156 | + panic-attack → vordr invocation in `cartridges/panic-attack-mcp/abi/ |
| 157 | + PanicAttackMcp/CompositionWithVordr.idr`. PR pattern: one |
| 158 | + `CompositionWith*.idr` per pair. |
| 159 | +3. **Bridge wiring (PEP).** `mcp-bridge/lib/dispatcher.js` learns to |
| 160 | + look for a composition envelope on internal `boj_cartridge_invoke` |
| 161 | + calls; rejects on absence when the source/target pair is gated. |
| 162 | +4. **`policy-mcp` `compositions` block (PDP).** Schema, fixtures, |
| 163 | + ADR-0007 follow-on PR. |
| 164 | +5. **Wire-up tests** in `mcp-bridge/tests/composition_test.js` — |
| 165 | + property tests across the gate truth table (allowed pair, denied |
| 166 | + pair, depth-exceeded, tier-violation, target-not-ready). |
| 167 | +6. **JOSS paper.** `docs/papers/joss-composition-proof.md` — the |
| 168 | + formal-verification differentiation of BoJ vs other MCP servers, |
| 169 | + with `panic-attack → vordr` as the worked example. |
| 170 | + |
| 171 | +## JOSS paper angle |
| 172 | + |
| 173 | +BoJ's unique posture relative to other MCP servers is the |
| 174 | +formally-verified ABI. No other MCP server (per ADR-0008's |
| 175 | +marketplace survey) carries an Idris2 proof layer. Submitting the |
| 176 | +composition-proof artifact to JOSS does two things: |
| 177 | + |
| 178 | +- Establishes priority on the framing of MCP composition as a typed |
| 179 | + problem. |
| 180 | +- Provides academic citability for downstream users — the OU |
| 181 | + affiliation makes the route tractable. |
| 182 | + |
| 183 | +The paper draft should be sketched **alongside** the first pair's |
| 184 | +proof, not after, so the framing in the paper and the framing in the |
| 185 | +code stay coherent. |
| 186 | + |
| 187 | +## Constraints and non-negotiables |
| 188 | + |
| 189 | +1. **Idris2 build stays green throughout.** Every PR must include a |
| 190 | + `idris2 --check` invocation. (Note: at time of writing, `src/abi/ |
| 191 | + boj.ipkg --build` does not complete in 9 min on a local dev box but |
| 192 | + individual `--check` runs are fast. Pre-existing baseline-rot in |
| 193 | + `Boj.SafeAPIKey` is tracked separately; do not block composition |
| 194 | + work on it.) |
| 195 | +2. **No `believe_me` net-additions.** The 5 existing axioms are |
| 196 | + irreducible (PROOF-NEEDS audit 2026-05-18). New axioms only via |
| 197 | + explicit `parameters` blocks with documented rationale. |
| 198 | +3. **The honest count rule.** If a proof obligation in the composition |
| 199 | + envelope turns out to be irreducible, **document it as a principled |
| 200 | + assumption** rather than papering over it. The honest count is more |
| 201 | + valuable than a forced "zero". |
| 202 | +4. **No cartridge invented for proof convenience.** Specifically: |
| 203 | + `sandbox-mcp` (ADR-0009) is RFC-only today. The campaign uses real |
| 204 | + cartridges (panic-attack, vordr) for the first pair; the three-step |
| 205 | + chain is parked behind ADR-0009 implementation. |
| 206 | + |
| 207 | +## Definition of done |
| 208 | + |
| 209 | +- [ ] `Boj.Composition` lands and type-checks (sub-PR 1). |
| 210 | +- [ ] At least one composition pair proven end-to-end (sub-PR 2). |
| 211 | +- [ ] Bridge PEP + PDP composition rules in production for that pair |
| 212 | + (sub-PRs 3 + 4). |
| 213 | +- [ ] Wire-up tests pass on CI (sub-PR 5). |
| 214 | +- [ ] JOSS paper draft submitted, with `panic-attack → vordr` as the |
| 215 | + worked example (sub-PR 6). |
| 216 | +- [ ] Per-pair sub-issues filed for the next composition pairs; epic |
| 217 | + #87 item 12 stays open until coverage is "meaningful" (specific |
| 218 | + threshold TBD with the owner — likely "all destructive-side-effect |
| 219 | + cartridges have at least one proven invoker"). |
| 220 | + |
| 221 | +## Open questions |
| 222 | + |
| 223 | +- **`ArgsContract` derivation strategy.** Mechanically lift from each |
| 224 | + cartridge's `cartridge.json` JSON-schema (cheap, brittle) vs hand- |
| 225 | + written per cartridge (expensive, robust) vs a Nickel intermediate |
| 226 | + schema (medium). Recommend deciding before sub-PR 1 lands. |
| 227 | +- **Federation interaction.** Cross-machine invocations (ADR-0010) need |
| 228 | + their own composition story — the envelope has to survive |
| 229 | + serialisation. Punt to a follow-on ADR once the local case lands. |
| 230 | +- **Sandbox-mcp build-out.** The full panic-attack → sandbox → vordr |
| 231 | + chain is the JOSS-paper-shaped goal; without sandbox-mcp it's a two- |
| 232 | + cartridge demo. ADR-0009 needs to be built first, or the proof scope |
| 233 | + needs to be honestly limited to the two-cartridge case in the paper. |
| 234 | + |
| 235 | +## References |
| 236 | + |
| 237 | +- ADR-0006 — cartridge-invoke ABI (defines `boj_cartridge_invoke`) |
| 238 | +- ADR-0007 — trust-tier policy DSL (defines policy-mcp PDP that this |
| 239 | + ADR extends with a `compositions` block) |
| 240 | +- ADR-0009 — sandbox cartridge (RFC-only; the missing cartridge in the |
| 241 | + canonical three-step chain) |
| 242 | +- ADR-0010 — cross-machine coord federation (depends on a composition |
| 243 | + story; needs follow-on) |
| 244 | +- `PROOF-NEEDS.md` — 2026-05-18 audit; the 5 class (J) axioms; closure |
| 245 | + of P1/P2 obligations per cartridge |
| 246 | +- `src/abi/Boj/CartridgeDispatch.idr` — BJ1 (the existing external- |
| 247 | + dispatch proof that this ADR lifts into the internal-invocation |
| 248 | + envelope) |
| 249 | +- Epic #87 Tier C item 12 — the campaign tracker |
0 commit comments