[proofs/c] Special/base cartridges (cross-cutting: agentic · nesy · orchestration · fleet · build · debug · health)

[hyperpolymath]

Tracking issue for the special/base cartridges (scope c) — the cross-cutting kinds the maker composes from.

Current state (verified 2026-06-05)

• boj-server-cartridges/cartridges/cross-cutting/: 12 .idr across agentic, build, debug, fleet, health, nesy, orchestration.
• cartridges/templates/: 1 .idr (the maker seed).
• feedback-mcp (in boj-server) is the one fully-real reference cartridge.

Why these are special

Unlike domain cartridges (mostly ABI/memory-safety proofs), the base/cross-cutting kinds carry behavioural / protocol obligations:

• orchestration — routing soundness (a request reaches exactly one correct downstream); no-orphan / no-dup.
• agentic — capability-bound execution (a step can only use granted capabilities).
• nesy — symbolic-soundness (the neural→symbolic bridge preserves declared invariants).
• fleet / build / debug / health — lifecycle + isolation invariants.

What remains

1. Define the bespoke proof-obligation set per cross-cutting kind (above is the starting point).
2. Specify the "base framework proof bundle" the maker (scope f) inherits by construction — the "proven pre-mint framework" the factory carries so individual cartridges never re-derive it.
3. Use feedback-mcp to pin the gold-reference proof set every minted cartridge ships with.

Done when

• Each cross-cutting kind has a defined obligation set + at least a compiling skeleton .idr.
• The inheritable base proof bundle is specified and referenced by the maker (scope f).

Proving track — tightly coupled to the maker (scope f).

---

Filed via Claude Code · https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa

[hyperpolymath]

Verified: cross-cutting/base proofs — 8/13 pass, 5 fail (2026-06-05 real idris2 --check)

PASS (8): agentic/agent-mcp (Protocol, SafeOODA), build/bsp-mcp, debug/dap-mcp, fleet/fleet-mcp, nesy/nesy-mcp (Protocol, SafeReasoning), templates/gossamer-mcp.

FAIL (5 files, 3 root causes):

• agentic/local-coord-mcp — SafeLocalCoord.idr:103 → Can't find an implementation for LTE 1024 7745. MkValidPort 7745 relies on auto-search for LTE 1024 7745, which exhausts Idris2's search depth (~6 min CPU). Needs an explicit LTE witness / decision procedure, not %search. Cascades to Protocol.idr + Identity.idr (they import it). This is a genuine proof gap, not just syntax.
• agentic/model-router-mcp/Protocol.idr:32 — parse error: data CostPreference = MkPref (n : Fin 101) uses named-argument syntax in a data constructor (needs record syntax or an unnamed arg).
• nesy/ml-mcp/SafeMl.idr:127 — namespace : String uses the reserved keyword namespace as a field name.

No axioms in any .idr (one grep hit is a doc-comment).

These are the agentic + nesy base kinds the maker (#200) inherits — they must compile to be the "proven pre-mint bundle." The local-coord LTE obligation is the only one needing real proof work; the other two are mechanical.

---

Generated by Claude Code

[hyperpolymath]

PR #40 — the cross-cutting cartridges now compile.

The compilation blocker is cleared. Verified with real idris2 --check (0.8.0), each synced from its compiling boj-server twin:

• local-coord-mcp (agentic) — exhausted LTE 1024 7745 auto-search → explicit witness;
• model-router-mcp (agentic) — MkPref (n : Fin 101) bad data-ctor arg → MkPref (Fin 101);
• ml-mcp (nesy) — namespace reserved-word record field → namespaceName.

So "at least a compiling skeleton .idr" is satisfied for the agentic + nesy kinds, and proofs.yml now keeps every cross-cutting ABI compiling on each PR.

Still open here (design, not compilation — coupled to the maker):

1. The bespoke proof-obligation set per kind (orchestration routing-soundness; agentic capability-boundedness; nesy symbolic-soundness; fleet/build/debug/health lifecycle + isolation). tools/foundry/proof/Foundry.idr already models the generic mint→provision→configure→harness assurance (no-dropped-proofs + least-authority); these are the per-kind extensions of that.
2. The inheritable base proof bundle the maker carries by construction.

Leaving open for that design work.

---

Generated by Claude Code