diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 30116321..7a8bf2a4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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." }, diff --git a/CHANGELOG.md b/CHANGELOG.md index 53994259..6a06b2ca 100644 --- a/CHANGELOG.md +++ b/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