docs: record TLA+ Elixir harness coverage in STATE and Developer-Guide

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "boj-server"
 version = "1.1.0-wip"
-last-updated = "2026-06-13"
+last-updated = "2026-06-24"
 status = "active"
 grade = "C"
 
@@ -50,6 +50,7 @@ js-dispatch-chain-verified  = true  # JsWorkerPool → JsWorker → Deno port 
 believe-me-count            = 4     # all in SafetyLemmas.idr — 4 class (J) axioms over Idris2 primitives (charEqSound, unpackLength, appendLengthSum, substrLengthBound). charEqSym discharged to a constructive theorem (derived from charEqSound) — first §(a) discharge under standards#203, was 5. (The 2026-05-18 audit + #108 had reconciled a stale "4" up to a true 5; this discharge brings it to a true 4.) Reduced from 31 on 2026-04-12.
 zig-files                = 0     # all .v files removed 2026-04-12
 cartridges-available-real   = 1     # only feedback-mcp is built+verified-real (available:true). ~97 cartridges build a .so that returns {"status":"stub"}; 10 have no FFI — ALL now marked available:false (PR #196, 2026-06-05). Catalogue no longer over-claims; tests/truthfulness_check.sh gate enforces it.
+tla-elixir-harness          = "specs/elixir-harness/ — 3 TLA+ models: JsWorker (341 states, depth 8), JsWorkerPool (RouteConsistency + crash-isolation + NoPendingWhileDown), Invoker (DoneOnce + 7 exit-code sanity controls). All have .cfg + non-vacuity checks. Formal-proof axis only; CRG grade unchanged."
 
 [open-gaps]
 # Ordered by impact on users hitting POST /cartridge/:name/invoke
@@ -74,6 +75,7 @@ test-coverage = "CLOSED 2026-04-25 — 165 ExUnit tests; CRG C met"
 
 [session-history]
 entries = [
+  { date = "2026-06-24", description = "TLA+ formal coverage of Elixir REST harness (PRs #252 + #253, MERGED). Three TLA+ models in specs/elixir-harness/ now cover the BEAM-side concurrency layer: JsWorker.tla (pre-existing; 341 states, depth 8; ReplyOnce, EventuallyReplied), JsWorkerPool.tla (PR #252; N-slot pool; RouteConsistency proves phash2 routing invariant; crash-isolation enforced structurally by Crash(w) guard; NoPendingWhileDown), Invoker.tla (PR #253; stateless fork-per-request dispatcher; DoneOnce; 7 exit-code sanity controls). EventuallyDone is [ASSUMED] in the Invoker model — no per-invocation timeout in Phase 2 (System.cmd blocks indefinitely; ADR-0005 Phase 3 pool will close this gap). All models include .cfg files and non-vacuity sanity-control checks (each ReachXxx expected to be refuted by TLC). Formal-proof axis only; CRG readiness grade unchanged." },
   { date = "2026-06-13", description = "CI required-gate skip-shim + estate-wide unblock. ROOT CAUSE: 7 required gates (abi-drift, backend-assurance, e2e, lsp-dap-bsp, proofs, truthfulness, zig-test) were workflow-level path-filtered (on.*.paths); on any PR touching none of a gate's paths the workflow never ran, so its required status check stayed 'Expected' forever and the PR sat mergeable_state=blocked even fully-green (stranded #213 dependabot flake.lock + #215 scripts-only). FIX (PR #216, MERGED): dropped on.*.paths from all 7; added an always-run `changes` job that recomputes each gate's original path set via `git diff origin/<base>...HEAD`; gated every heavy job with needs:changes + if:run=='true' (a job skipped via if: reports SUCCESS to required checks). Fail-safe toward running; job/check names unchanged so no branch-protection edit needed. Validated: actionlint clean; detection regex 77/77; live on #216 all 15 heavy jobs skipped->success. Then merged #213 + #215. MIRRORED to boj-server-cartridges (PR #45, MERGED): same shim on proofs/zig-test/foundry. Conventions captured this session: docs/AI-CONVENTIONS.adoc + .claude/CLAUDE.md (new 'CI / Required Status Checks' sections) + docs/wikis/CI-and-Required-Checks.adoc + PLAYBOOK [ci-required-gates]; AI-CONVENTIONS Banned-Languages 'TypeScript->ReScript' corrected to '->AffineScript' (ReScript retired 2026-04-30). Follow-ups filed: #218 (boj-server Hypatia/governance hygiene: stale GEMINI.md, unpinned governance.yml action, missing timeout-minutes, shellcheck infos); cartridges #46 (TS->AffineScript port of stack-orchestrator-mcp + proof-lsp adapters), #47 (cartridges Hypatia hygiene), #48 (language-cartridge IDE completeness)." },
   { date = "2026-06-05", description = "Truthfulness + Foundry + governance-checkpoint session. (1) Catalogue honesty (PR #196, MERGED) — router.ex defaulted every cartridge to available:true, so all 125 advertised as working when only feedback-mcp is built+real (97 build a .so that returns {\"status\":\"stub\"}; 10 have no FFI). Fixed: explicit `available` on all 125 cartridge.json (true only for feedback-mcp) + `status` where missing; router `available` default flipped true→false (a cartridge must opt in to being advertised, never by omission); new tests/truthfulness_check.sh + .github/workflows/truthfulness.yml gate builds every available cartridge and invokes its first tool, failing on a stub marker (verified to catch an injected stub→available lie); fixed router_test.exs + contract_test.exs /menu tests that asserted the pre-tiering cartridges/count shape (broken since the tiered /menu landed) to assert tier_*/summary + the availability invariant (summary.ready == count of available). believe-me-count unchanged at 5. (2) Foundry (boj-server-cartridges PR #38, MERGED) — the integrated mint→provision→configure→harness cartridge-making workflow, built ON the existing cartridge-minter + gossamer-mcp template (not from scratch). tools/foundry/proof/Foundry.idr (Idris2 0.8.0, typechecked) machine-checks two properties: NO-DROPPED-PROOFS (a `failing` block proves skipping the harness won't compile, pinned to `Can't find an implementation for Elem Truthful`) and LEAST-AUTHORITY (capability index = exact grant; no stage widens it). stages/harness.sh = the one general gate (idris2 --check + zig build + the #196 truthfulness probe + capability-subset check), verified PASS on gossamer-mcp. (3) Filed 8 tracking issues: proofs a/b/c (#197, hyperpolymath/boj-server-cartridges#36, #37), obleeny long-term #198, catch-all hygiene #199, maker #200, implement-stubs #201, gate-enforcement #202. (4) Branch reconciliation — retired superseded branches (e2e-rest-contract, feedback-otron; truthfulness-pass/feedback-otron-fix already auto-deleted on merge); reset zen-galileo to main; PRESERVED claude/cartridge-abi-proofs (unmerged proof-CI groundwork: 17 ABI .idr typecheck-fixes for 0.8.0 + typecheck-proofs.sh — captured in #197 for rebase-and-land); one clean main per repo. (5) Governance checkpoint (this commit) — STATE refreshed; ANCHOR realigned to current language policy. FLAGGED: boj-server-cartridges has NO .machine_readable/ at all (entire standard layout missing); no bot_directives/ dir in either repo; standards + rsr-template unreachable from this session (GitHub scope = boj-server + boj-server-cartridges only, no list_repos/add_repo) so the rsr-template-vs-standards divergence check is BLOCKED pending access." },
   { date = "2026-05-26", description = "Repo-tidy / rsr-template-repo taxonomy alignment (PR #149). Six commits; 136 files changed (+5096 -3322). (1) Root .adoc relocations — EXPLAINME.adoc -> docs/, BOJ_LOGIC.adoc + NeSy_SERVERS.adoc -> docs/architecture/, FUTURE_PLANS.adoc + ROADMAP.adoc -> docs/status/, QUICKSTART-{USER,DEV,MAINTAINER}.adoc -> docs/quickstarts/. Cross-refs updated in 0-AI-MANIFEST.a2ml, Justfile, elixir/boj-rest.service, methodology.a2ml (fallback-files list), docs/README.adoc, docs/accessibility/README.adoc, and two outreach drafts. Historical mentions in CHANGELOG.md and dated log entries in STATE.a2ml deliberately left intact. (2) README merge — substantive 518-line README.md converted to AsciiDoc and merged with the unique sections from the shorter 176-line README.adoc (Features bullets, Formal verification). README.md deleted. Refs in jsr.json publish list, mcp-bridge/lib/resources.js docs URL, .github/SECURITY.md, and Intentfile repointed at README.adoc. (3) Wiki + warmup conversions — five wiki pages converted .md->.adoc and moved docs/wiki/ -> docs/wikis/ (template's spelling); llm-warmup-{dev,user}.md -> docs/developer/; CARTRIDGE-PHASE-3B-COMPLETION.md -> docs/status/. Drift fix: STATE.a2ml cartridges-total 112 -> 125 (every dir under cartridges/* has cartridge.json), cartridges-with-zig-ffi 111 -> 115 (manifest-counted), cartridges-with-js-mod 111 -> 113, project-context.purpose '112 cartridges' -> '125 cartridges'. (4) Bulk docs/*.md -> .adoc — ABI-FFI-README, AI-CONVENTIONS, API-CONTRACT, CULTURAL-RESPECT, EXTENSIBILITY, FEDERATION, READINESS, THREAT-MODEL; plus relocations docs/ARCHITECTURE.md -> docs/architecture/README.adoc and docs/DEVELOPERS.md -> docs/developer/README.adoc. 99 files cross-rewritten (55 cartridge READMEs + governance/wiki/dev/architecture refs + Justfile, .github/copilot-instructions.md, SECURITY.md, src/abi/Boj/Catalogue.idr docstring, k8s/service.yaml, mcp-bridge/lib/api-clients.js, plus outreach/practice docs). New subdir orientation READMEs in docs/quickstarts/, docs/status/, docs/wikis/. docs/READINESS.adoc deliberately stays at docs/ root (not under docs/status/) because 55+ cartridge READMEs link to that canonical path. (5) Quickstart consolidation — substantive docs/QUICKSTART.md (72 lines) -> docs/quickstarts/DEV.adoc (replaces 39-line stub); docs/GETTING-STARTED.md (198 lines) -> docs/quickstarts/BUILD-FROM-SOURCE.adoc (new sibling); docs/OPERATOR-QUICKSTART.md (296 lines) -> docs/quickstarts/MAINTAINER.adoc (replaces 40-line stub). docs/quickstarts/README.adoc updated to list all four with audience guidance. Refs in Mustfile + flake.nix + CRG-LIFT-PLAN + outreach drafts updated. (6) docs/README.adoc index rewritten in full (Reading-order-by-audience + Directory-taxonomy + Standalone-docs/-root + Related-root-level sections) + last lone .md in docs/architecture/ (TYPED-WASM-MCP-BRIDGE.md) converted to .adoc. Hypatia approved-exemption manifest patch /tmp/hypatia-approved-exemptions.patch delivered to user for upstream application to hyperpolymath/hypatia (separate PR). Known-deferred (high coupling, not in this PR): PROOF-NEEDS.md (16 cross-refs incl. CI + Idris proofs + 4 Elixir test files), TOPOLOGY.md (11 cross-refs incl. CI workflow), TEST-NEEDS.md (5 cross-refs); follow-up PR should bulk-rewrite. GEMINI.md left at root — load-bearing (gemini-extension.json contextFileName). CI failures on PR #149 (ABI Specification Check, FFI Build, abi-drift verify, Aspect, E2E) all confirmed pre-existing on main; this PR's diff is comment-line-only outside docs/, cannot have introduced them." },

docs/wikis/Developer-Guide.adoc

@@ -343,7 +343,7 @@ src/abi/              # Idris2 ABI -- formal proofs
   Guardian.idr        #   Resource-aware failure tolerance
 
 ffi/zig/              # Zig FFI -- native execution
-  src/catalogue.zig   #   Mount/unmount, cartridge ops
+  src/catalogue.zig   #   Catalogue tests
   src/loader.zig      #   Dynamic cartridge loading
   src/federation.zig  #   Gossip protocol, QUIC transport
   src/verisimdb.zig   #   VeriSimDB backing store
@@ -371,6 +371,11 @@ container/            # Deployment
 generated/abi/        # Auto-generated C headers from Idris2
 .machine_readable/    # State files, menu, policies
 docs/                 # Architecture, API contract, guides
+specs/elixir-harness/ # TLA+ formal models of the Elixir concurrency layer
+  JsWorker.tla        #   Single GenServer slot (ReplyOnce, 341 states, depth 8)
+  JsWorkerPool.tla    #   N-slot pool (RouteConsistency, crash isolation)
+  Invoker.tla         #   Stateless fork-per-request dispatcher (DoneOnce)
+  README.adoc         #   Properties, code-to-model mapping, TLC run instructions
 ----
 
 == Contributing