From e37ada9be82f9f657f087924f6c1ab4d4caf3bea Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 24 Jun 2026 21:31:02 +0100 Subject: [PATCH] docs: record TLA+ Elixir harness coverage in STATE + Developer-Guide MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - STATE.a2ml: last-updated 2026-06-13→2026-06-24; new tla-elixir-harness quality entry; new 2026-06-24 session-history entry covering PRs #252 (JsWorkerPool.tla) and #253 (Invoker.tla) - docs/wikis/Developer-Guide.adoc: add specs/elixir-harness/ to project structure with per-file descriptions Formal-proof axis only; CRG readiness grade unchanged. --- .machine_readable/6a2/STATE.a2ml | 4 +++- docs/wikis/Developer-Guide.adoc | 7 ++++++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a0b3dc7f..2a6e2475 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-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/...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." }, diff --git a/docs/wikis/Developer-Guide.adoc b/docs/wikis/Developer-Guide.adoc index 89880ce9..7c821a17 100644 --- a/docs/wikis/Developer-Guide.adoc +++ b/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