rfc: ADR-0014 cross-cartridge composition safety (epic #87 Tier C item 12) by hyperpolymath · Pull Request #109 · hyperpolymath/boj-server

hyperpolymath · 2026-05-20T08:09:25Z

Summary

New ADR docs/decisions/0014-cross-cartridge-composition-safety.md framing the genuinely-open research question that item 11 doesn't touch: per-cartridge ABI proofs do not compose automatically across boj_cartridge_invoke.
Defines composition safety as a two-level contract — static Idris2 envelope (Boj.Composition.InvocationOf lifting IsUnbreakable + ProtocolMatch + per-cartridge ArgsContract into the inter-cartridge call) plus dynamic Nickel compositions block in ADR-0007's policy-mcp PDP (composition admissibility, tier-elevation guards, call-depth caps).
Lays out a six-sub-PR campaign (envelope skeleton → first pair proof → bridge PEP → PDP policy → tests → JOSS paper).

Honest-framing carryovers from item 11

First proof pair is panic-attack-mcp → vordr-mcp (both cartridges actually exist on disk), not the prompt's "panic-attack → sandbox → vordr" three-step chain — because cartridges/sandbox-mcp/ does not exist. ADR-0009 proposes it but no implementation has landed. The longer chain is parked behind ADR-0009 build-out.
No believe_me net-additions. The five class (J) axioms in SafetyLemmas.idr remain irreducible (PROOF-NEEDS audit 2026-05-18) and the composition envelope must respect them.
Existing per-cartridge proofs are not weakened to make composition easier — if a P-01..P-07 obligation conflicts with the envelope, the obligation is right and the envelope shape is wrong.

What this PR is and is not

Is: a framing ADR. No implementation. No code beyond the markdown doc.

Not: a build plan with deadlines. The campaign is genuinely months-long research with a JOSS-paper deliverable. Sub-PRs land at whatever cadence the proofs support; the ADR is the durable framing they all hang off.

Test plan

Markdown well-formed.
Reviewer agreement on the static/dynamic two-level split.
Reviewer agreement on panic-attack → vordr as first pair vs waiting for sandbox-mcp.
Reviewer agreement on ArgsContract open-question resolution (cartridge.json lift vs hand-written vs Nickel intermediate).

Open questions called out in the ADR

ArgsContract derivation strategy.
Federation (ADR-0010) composition story — punted to follow-on.
Sandbox-mcp build-out as a prerequisite to the canonical three-step chain.

Refs epic #87 Tier C item 12. Item 11 (proof-debt honest framing) is a separate draft PR.

🤖 Generated with Claude Code

…m 12) Frames the genuinely-open research question that item 11 doesn't touch: per-cartridge ABI proofs do not compose automatically across `boj_cartridge_invoke`. Defines composition safety as a two-level contract — Idris2 `Boj.Composition.InvocationOf` envelope for the static (typed) level, Nickel `compositions` block in ADR-0007's policy-mcp PDP for the dynamic (admissibility) level — and lays out a six-sub-PR campaign to discharge it. Key honest framings carried over from the item 11 audit: - Recommended first proof pair is `panic-attack-mcp -> vordr-mcp` (both cartridges exist on disk), NOT the three-step `panic-attack -> sandbox -> vordr` chain suggested for the campaign — because `sandbox-mcp` (ADR-0009) is RFC-only and not yet built. - No new believe_me net-additions. The five class (J) axioms in `SafetyLemmas.idr` remain irreducible (per PROOF-NEEDS audit 2026-05-18) and the composition envelope must respect them. - Existing per-cartridge proofs are not weakened to make the composition story easier. If an obligation conflicts, the obligation is right and the envelope shape is wrong. - JOSS paper sketched alongside the first pair's proof (not after), using the cartridge pair that actually exists as the worked example. This ADR is a framing document — no implementation here. The campaign proceeds via six sub-PRs (Boj.Composition skeleton; first pair proof; PEP bridge wiring; PDP policy block; tests; JOSS paper draft). Refs epic #87 Tier C item 12. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-20T08:10:24Z

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-05-20T08:13:28Z

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

… baseline rot) (#116) ## Summary Restores `Boj.SafeAPIKey` to a green Idris2 0.8.0 build. The pre-existing `logSafeBounded` proof on `main` does not type-check; this PR rebuilds it against the current stdlib + elaborator behaviour. **No new axioms.** The 5-class-(J) framing established in #108 is preserved. Discovered while verifying #108 (item 11). Was originally stacked on #108; rebased onto `main` after #108 merged at 2026-05-20T08:13Z. ## Three independent defects, each fixed 1. **Removed the redundant local `plusLteMonotone` helper.** It wrapped `lteTransitive (plusLteMonotoneRight _ lmn) (plusLteMonotoneLeft _ lpq)`: - `lteTransitive` is no longer in stdlib — Idris2 0.8.0 uses `Control.Relation.transitive`, but that's ambiguous in this import context. - `plusLteMonotoneRight` / `plusLteMonotoneLeft` have signature `(p, q, r : Nat) -> LTE q r -> LTE (q+p) (r+p)` in this stdlib — the wrapper passed wildcards expecting a different shape. The stdlib already ships `Data.Nat.plusLteMonotone : LTE m n -> LTE p q -> LTE (m + p) (n + q)` — exactly what the wrapper was trying to be. Use it directly. 2. **Lifted both branches out of the `with`-block.** Inside `logSafeBounded s with (length s <= 8) proof cond`, Idris2 0.8.0 does not reduce `length "***"` (or `length "..."`) at type level — the goal is exposed as `LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if True then ... else ...)))) 11` with the `if`-arm unreduced. Outside the with-block, the same lemmas type-check via Refl-equivalent computation. Extracted `logSafeBoundedShort` / `logSafeBoundedLong` as private helpers; the with-block now just dispatches. 3. **Right-associated the long-path proof.** `(++)` is right-associative in Idris (`a ++ b ++ c = a ++ (b ++ c)`), but the original composed `(p1 ++ "...") ++ p3` (left-associative) — its conclusion didn't match the with-block's False-branch goal. New proof: `step23 (length "..." + length (substr ...) ≤ 3 + 4)` then `step123 (length (substr 0 4 s) + length (...) ≤ 4 + 7)`. Plus two bound-name typos in `toLogSafeShortEq` / `toLogSafeLongEq` where the outer `_` discarded the `prf` argument that the inner branch then referenced. ## Test plan Per-module `idris2 --check` on every safety module — **all 12 green**: ``` Boj.SafetyLemmas green Boj.SafeAPIKey green (this PR) Boj.Safety green Boj.APIContractCoverage green Boj.CartridgeDispatch green Boj.Catalogue green Boj.CredentialIsolation green Boj.Federation green Boj.SafeCORS green Boj.SafeHTTP green Boj.SafePromptInjection green Boj.SafeWebSocket green ``` `idris2 --build src/abi/boj.ipkg` does not complete in 9 min on my dev box (gets SIGTERMed) — same note as #108. Per-module `--check` is the verification surface. ## Why this matters `PROOF-NEEDS.md`'s 2026-05-18 audit claims `SafeAPIKey` carries constructive proofs that close BJ2-partial. Pre-this-PR the proof did not compile. The audit was, like the SafetyLemmas axiom count noted in #108, evidently a desk-read of the source rather than a build. With this PR merged, the audited safety surface is buildable from scratch. Refs epic #87 Tier C (companion to #108 / #109). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…eep (#126) ## Summary Human + machine documentation close-out for the 2026-05-20 epic #87 Tier C session and follow-on baseline-rot sweep. No code, no behavioural change. ## Files - **`CHANGELOG.md`** `[Unreleased]`: - *Added* — ADR-0014 RFC (#109); README "Formal verification" section (#108). - *Fixed* — SafeAPIKey `logSafeBounded` proof rebuild for Idris2 0.8.0 (#116); `tests/aspect_tests.sh` grep-count bash bug (#118); honest framing of the ABI axiom count + `(s t : T)` → `(s, t : T)` parser-comma fix to `SafetyLemmas.idr` (#108). - **`.machine_readable/6a2/STATE.a2ml`**: - `last-updated` bumped `2026-04-25` → `2026-05-20`. - `believe-me-count` corrected `4` → `5`, with citation back to `PROOF-NEEDS.md` 2026-05-18 audit + #108. - `[session-history]` entry appended summarising items 11 + 12 + the SafeAPIKey baseline-rot follow-up + the CI baseline-rot sweep + operational notes (parallel-session branch drift, workflow OAuth scope dance). ## Companion PRs from this thread | PR | Status | What | |---|---|---| | #108 | MERGED 2026-05-20T08:13Z | item 11 honest framing (docstring + README + parser-comma) | | #109 | MERGED 2026-05-20T08:12Z | item 12 ADR-0014 RFC (cross-cartridge composition safety) | | #116 | MERGED 2026-05-20T08:46Z | SafeAPIKey `logSafeBounded` rebuild for Idris2 0.8.0 | | #118 | MERGED 2026-05-20T09:02Z | `tests/aspect_tests.sh` grep-count bash bug | | #123 | OPEN | `.github/workflows/e2e.yml` Zig + Deno pin refresh | | **#126 (this)** | OPEN | session-close docs | ## Out of scope (intentionally) - `governance / Language / package anti-pattern policy` baseline rot stays untouched per the parallel-session-branch-drift guardrail (parent campaign standards#66 owns it). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Merge branch 'main' into rfc/item12-cross-cartridge-composition-adr0014

868ab36

hyperpolymath marked this pull request as ready for review May 20, 2026 08:12

hyperpolymath merged commit 746c352 into main May 20, 2026
13 of 16 checks passed

hyperpolymath deleted the rfc/item12-cross-cartridge-composition-adr0014 branch May 20, 2026 08:12

hyperpolymath mentioned this pull request May 20, 2026

fix(idris): rebuild logSafeBounded proof for Idris2 0.8.0 (SafeAPIKey baseline rot) #116

Merged

hyperpolymath mentioned this pull request May 20, 2026

docs(state): close-out 2026-05-20 — epic #87 Tier C + baseline-rot sweep #126

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

rfc: ADR-0014 cross-cartridge composition safety (epic #87 Tier C item 12) - #109

rfc: ADR-0014 cross-cartridge composition safety (epic #87 Tier C item 12)#109
hyperpolymath merged 2 commits into
mainfrom
rfc/item12-cross-cartridge-composition-adr0014

hyperpolymath commented May 20, 2026

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented May 20, 2026

Summary

Honest-framing carryovers from item 11

What this PR is and is not

Test plan

Open questions called out in the ADR

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant