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

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "boj-server"
 version = "1.1.0-wip"
-last-updated = "2026-04-25"
+last-updated = "2026-05-20"
 status = "active"
 grade = "C"
 
@@ -47,7 +47,7 @@ cartridges-with-both        = 0     # no cartridge uses both paths
 exunit-tests                = 173   # 10 properties + 163 regular tests across 11 files; Phase 9 auth tests added 2026-04-25
 zig-ffi-chain-verified      = true  # boj-invoke → dlopen → libboj_health.so end-to-end tested 2026-04-25
 js-dispatch-chain-verified  = true  # JsWorkerPool → JsWorker → Deno port → mod.js handleTool
-believe-me-count            = 4     # 3 axiomatic primitives + 1 logSafeBounded — reduced from 31 on 2026-04-12
+believe-me-count            = 5     # all in SafetyLemmas.idr — 5 class (J) axioms over Idris2 primitives (charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound); reconciled from stale "4" framing per PROOF-NEEDS.md 2026-05-18 audit + #108 honest-framing PR. Reduced from 31 on 2026-04-12.
 v-lang-files                = 0     # all .v files removed 2026-04-12
 
 [open-gaps]
@@ -73,6 +73,7 @@ test-coverage = "CLOSED 2026-04-25 — 165 ExUnit tests; CRG C met"
 
 [session-history]
 entries = [
+  { date = "2026-05-20", description = "Epic #87 Tier C session (items 11 + 12 + follow-on baseline-rot sweep): (1) Item 11 (PR #108, MERGED) — honest framing of the remaining ABI axioms. Session-prompt premise that '4 believe_me axioms remain' was stale; PROOF-NEEDS.md's 2026-05-18 audit had already classified 5 sites, all class (J), all irreducible over Idris2 0.8.0's opaque Char/String primitives (charEqSound, charEqSym, unpackLength, appendLengthSum, substrLengthBound). Fixed three loose ends: SafetyLemmas.idr's module docstring (claimed 'three axiomatic primitives', listed only three of the five) corrected to enumerate all five with prim__* attribution; appendLengthSum and substrLengthBound's `(x y : T)` multi-binder syntax (rejected by Idris2 0.8.0 at parse time) commaed to `(x, y : T)`; README.adoc gained a 'Formal verification' section so the audited posture is surfaced outside PROOF-NEEDS.md. (2) Item 12 (PR #109, MERGED) — ADR-0014 'Cross-cartridge composition safety' as an RFC framing document, no implementation. Defines composition safety as a two-level contract: static Idris2 `Boj.Composition.InvocationOf` envelope (lifting IsUnbreakable + ProtocolMatch + per-cartridge ArgsContract into the inter-cartridge call) plus dynamic Nickel `compositions` block in ADR-0007's policy-mcp PDP. Six-sub-PR campaign laid out. First proof pair is panic-attack-mcp → vordr-mcp (both cartridges exist on disk); the prompt-suggested three-step `panic-attack → sandbox → vordr` chain is parked behind ADR-0009 sandbox-mcp build-out (sandbox-mcp does not yet exist on disk). (3) SafeAPIKey baseline-rot follow-up (PR #116, MERGED 2026-05-20T08:46Z) — `logSafeBounded` proof did not type-check on Idris2 0.8.0 despite PROOF-NEEDS.md's audit claiming it did (audit was desk-read, not build). Three independent defects: removed redundant local plusLteMonotone helper (called now-gone lteTransitive and used wrong arg order on plusLteMonotoneRight/Left; stdlib's Data.Nat.plusLteMonotone has exactly the needed shape); lifted both short and long paths out of the with-block (Idris2 0.8.0 doesn't reduce `length \"***\"` at type level inside a with-block — the goal stays as `LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if ...)))) 11` with the `if`-arm unreduced); right-associated the long-path proof to match `++`'s right-associativity (`a ++ b ++ c = a ++ (b ++ c)`). Plus fixed two bound-name typos in toLogSafeShortEq/toLogSafeLongEq where outer `_` discarded the prf the inner branch then referenced. Per-module `idris2 --check` is now green on all 12 safety modules (SafetyLemmas, SafeAPIKey, Safety, APIContractCoverage, CartridgeDispatch, Catalogue, CredentialIsolation, Federation, SafeCORS, SafeHTTP, SafePromptInjection, SafeWebSocket); `idris2 --build src/abi/boj.ipkg` does not complete in 9 min on dev machine (SIGTERM, gets nowhere). No new axioms; the 5-class-(J) framing from #108 preserved. (4) Estate baseline-rot CI sweep — diagnosed 5 reds on PR #116 and on main: 4 mechanical, 1 owned by parallel session. PR #118 (MERGED 2026-05-20T09:02Z) repairs tests/aspect_tests.sh grep-count bash bug (`grep -c X file 2>/dev/null || echo \"0\"` produced `\"0\\n0\"` and broke `[[ -gt 0 ]]` arithmetic — swapped `|| echo \"0\"` for `|| true` on all 4 call-sites). PR #123 (OPEN) repairs .github/workflows/e2e.yml: Zig 0.15.0 → 0.15.1 (`.tool-versions` canonical; 0.15.0 retired upstream from the GitHub Actions Zig download index) and `denoland/setup-deno@5fae568d…` → `@667a34cdef…` v2.0.4 SHA (the old SHA no longer resolves; the v2.0.4 SHA already in use by publish.yml verified via GitHub API). `governance / Language / package anti-pattern policy` deliberately untouched per the parallel-session-branch-drift guardrail — owned by another session under the Estate-drift-remediation 2026-05 campaign (parent standards#66). (5) Operational notes: parallel session in this repo committed `feat(mcp-bridge): Streamable HTTP transport` (#105) on a different branch under me mid-task; caught the branch drift via `git reflog` and untangled by hard-resetting HEAD to the intended item11 branch tip. gh OAuth token from device-code login granted only `gist, read:org, repo`; pushing `.github/workflows/e2e.yml` required a `workflow` scope refresh (`gh auth refresh -h github.com -s workflow`) before the push went through — hence the split between #118 (sh fix) and #123 (yaml fix). believe-me-count in STATE.a2ml stale at 4; bumped to 5 in this commit." },
   { date = "2026-05-18", description = "k9iser-mcp PR #73 session: (1) Added k9iser-mcp cartridge — reference -iser regeneration-cartridge pattern (central K9 contract regeneration) mirroring ssg-mcp: cartridge.json, mod.js, Idris2 ABI, Zig FFI, panels. (2) Unified transaction-gated adapter: ONE internal/loopback listener, protocol-routed REST+SSE+GraphQL+gRPC-compat → SINGLE dispatch → one Zig ABI, replacing the ssg-era 3-parallel-port anti-pattern; trust gate runs before every dispatch mirroring the Idris2 exposureSatisfied contract (no gatekeeperless path); internal-only behind http-capability-gateway per ADR-0004. (3) boj-rest SSE: POST /cartridge/:name/sse on the same single Cowboy listener + trust-gated dispatch, text/event-stream. (4) Doc reconciliation: elixir/README.adoc, mcp-bridge/api-clients.js, OPERATOR-QUICKSTART.md corrected to the verified runtime + ADR-0004 tiered model (previously wrongly 'skeleton/501/pending rewrite'). (5) CI ROOT-CAUSE FIX: dogfood-gate.yml failed YAML validation at startup (0s, no jobs) on every branch incl. main — inline `python3 -c \"` placed Python at column 1 inside a `run: |` block scalar, terminating the scalar early; since 'Dogfood Gate' is a required status check this silently blocked EVERY PR in the repo. Validator extracted to .github/scripts/validate-eclexiaiser.py and invoked from the workflow (commit 891b162). Verification: Elixir 177/177 (incl. 2 SSE tests); Zig ffi 16/16 + unified adapter 5/5 (exposure-gate truth table mirroring Idris2 contract); idris2 --check K9iserMcp/SafeK9iser.idr passes. Out of scope / separately tracked: http-capability-gateway production-wiring (ADR-0004 tier-2, ~8-12wk) and iseriser-scaffold rollout. Refs hyperpolymath/k9iser#8. NOTE: merge held — GitHub Actions runner-starved estate-wide (standards#122), required checks cannot execute until that clears." },
   { date = "2026-04-27", description = "Worker briefing + hook session: (1) Created .boj/project-memories.a2ml — standing worker briefing template covering coord registration, completion contract ('push succeeds, not TODO list'), backend wiring checklist, banned patterns (unimplemented!/sorry/Admitted/believe_me/.unwrap()-as-debt), comms protocol, git hygiene, and echidna language policy. Committed 039908a + pushed to main. (2) Updated ~/.config/coord-tui/coord-hooks.sh claude() function to auto-prepend project-memories.a2ml via --append-system-prompt when launched from a repo with .boj/project-memories.a2ml. Repos without the file are unaffected." },
   { date = "2026-04-25", description = "Close-out documentation sweep: ROADMAP.adoc current status → 'v1.1.0 Active (Grade C)'; seed node v0.3.0 bullet updated with fly.dev hostnames + LIVE date; Phase 8/9/Grade-C bullets added. EXPLAINME.adoc testing section expanded to 11 modules (173 total, 0 failures); 'harnesses pending' note removed; seed node infrastructure table added. AI-WORK-todo.md §8 header updated from 'in progress' to 'Grade C / 4 nodes LIVE'; docs-sweep bullet added. All changes committed + pushed to main." },

CHANGELOG.md

@@ -29,6 +29,23 @@ All notable changes to Bundle of Joy Server are documented here.
 
 ### Added
 
+- **ADR-0014 — cross-cartridge composition safety (RFC)** — frames the
+  unresolved research question that the per-cartridge ABI proofs do not
+  compose automatically across `boj_cartridge_invoke`. Defines composition
+  safety as a two-level contract: a static Idris2 envelope
+  (`Boj.Composition.InvocationOf` lifting `IsUnbreakable` + `ProtocolMatch`
+  + per-cartridge `ArgsContract` into the inter-cartridge call) and a
+  dynamic Nickel `compositions` block in ADR-0007's `policy-mcp` PDP.
+  First proof pair is `panic-attack-mcp → vordr-mcp` (both cartridges
+  exist on disk); the prompt-suggested `panic-attack → sandbox → vordr`
+  chain is parked behind ADR-0009's `sandbox-mcp` build-out.
+
+- **README "Formal verification" section** — surfaces the audited posture
+  outside `PROOF-NEEDS.md` so external readers can see, without digging,
+  that all P1/P2 obligations are closed with constructive proofs and that
+  the remaining `believe_me` invocations are *principled assumptions over
+  Idris2 primitives*, not unproven debt.
+
 - **Streamable HTTP transport (ADR-0013, PR1 of 2)** — MCP bridge now selects
   between stdio (default), `http`, and `both` via `BOJ_TRANSPORT`. HTTP
   endpoints: `POST /mcp` for JSON-RPC, `GET /mcp` for the server-initiated
@@ -65,6 +82,44 @@ All notable changes to Bundle of Joy Server are documented here.
 
 ### Fixed
 
+- **`Boj.SafeAPIKey.logSafeBounded` rebuilt for Idris2 0.8.0.** The pre-
+  existing proof did not type-check on `main`; the 2026-05-18 audit's claim
+  that `SafeAPIKey` carried constructive proofs closing BJ2-partial was a
+  desk-read, not a build. Three independent defects: (1) removed the
+  redundant local `plusLteMonotone` helper (called now-gone `lteTransitive`
+  and used wrong arg order on `plusLteMonotoneRight`/`Left`; stdlib's
+  `Data.Nat.plusLteMonotone` has exactly the needed shape); (2) lifted both
+  short and long paths out of the `with`-block (the elaborator doesn't
+  reduce `length "***"` at type level inside a `with`-block — goal stays
+  as `LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if ...))))
+  11` with the `if`-arm unreduced); (3) right-associated the long-path
+  proof to match `++`'s associativity (`a ++ b ++ c = a ++ (b ++ c)`).
+  Plus two bound-name typos in `toLogSafeShortEq`/`toLogSafeLongEq`. All
+  12 safety modules now build green via per-module `idris2 --check`. No
+  new `believe_me` axioms.
+
+- **`tests/aspect_tests.sh` grep-count bash bug.** `Aspect — Thread
+  Safety + ABI Contract + SPDX` had been red on `main`, gating every PR
+  with `tests/aspect_tests.sh: line 77: [[: 0\n0: syntax error in
+  expression`. Root cause: `grep -c 'pattern' file 2>/dev/null || echo
+  "0"`. `grep -c` always prints the count (including `0`) **and** exits
+  non-zero on no-match, so `|| echo "0"` also fires — `has_export` ends
+  up `"0\n0"` and `[[ "0\n0" -gt 0 ]]` chokes on the newline in
+  arithmetic context. Swapped `|| echo "0"` → `|| true` on all four
+  call-sites.
+
+- **Honest framing of the ABI axiom count.** `src/abi/Boj/SafetyLemmas.idr`'s
+  module docstring claimed "Three axiomatic `believe_me` primitives" while
+  five live in the file. Docstring now enumerates all five and tags each to
+  its underlying `prim__*` primitive. `appendLengthSum` and
+  `substrLengthBound` also had `(x y : T)` multi-binder syntax that Idris2
+  0.8.0 rejects at parse time — comma-separated form `(x, y : T)` restores
+  parsability. Types and proof terms unchanged. The 2026-05-18
+  `PROOF-NEEDS.md` audit (5 axioms, all class (J) — irreducible over Idris2
+  primitives, principled assumptions not unproven debt) is now consistent
+  with the source and surfaced via the new README "Formal verification"
+  section.
+
 - **`dogfood-gate.yml` failed YAML validation at startup** (0 s, no jobs) on
   every branch including `main`: an inline `python3 -c "` block placed Python
   source at column 1 inside a `run: |` block scalar, terminating the scalar