+ { 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, OPEN-DRAFT) — `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 (OPEN) 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." },
0 commit comments