diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f59943a0..a0b3dc7f 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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 = 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. +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. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index e5f59ba4..c75c4b53 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -14,6 +14,23 @@ Copyright (c) Jonathan D.A. Jewell > greps. Keep both in sync when the marker count in > `src/abi/Boj/SafetyLemmas.idr` changes. +## Discharge (2026-06-24) — `charEqSym` axiom → constructive theorem + +`charEqSym : (x, y : Char) -> (x == y) = (y == x)` is no longer a +`believe_me` axiom. It is now **derived constructively from `charEqSound`** +in `src/abi/Boj/SafetyLemmas.idr`: a `True` result forces propositional +equality (`charEqSound`), collapsing both sides to the same expression; a +mixed `True`/`False` split is impossible under soundness. This is the first +**§(a) DISCHARGED** entry under the trusted-base reduction policy +(standards#203) and drops the sanctioned class-(J) count **5 → 4** +(`charEqSound`, `unpackLength`, `appendLengthSum`, `substrLengthBound` +remain — all genuinely irreducible over opaque `Char`/`String` primitives). + +Verified locally: `cd src/abi && idris2 --typecheck boj.ipkg` → 17/17 +modules clean (Idris2 0.8.0, Chez 9.5.8). `scripts/check-trusted-base.sh` +updated to `EXPECTED_AXIOMS=4` and passes. The dated audits below are +retained as history; where they say "5", read "4 since 2026-06-24". + ## Build Verification (2026-06-13) — full sweep, freshly built toolchain Re-verified end-to-end on a clean machine with a from-source toolchain @@ -76,9 +93,10 @@ fails on anything else (or on axiom-count drift). ## Current State (Updated 2026-06-03) - **src/abi/Boj/**: 17 Idris2 ABI files -- **Dangerous patterns**: **5** `believe_me` invocations, **all** in +- **Dangerous patterns**: **4** `believe_me` invocations, **all** in `src/abi/Boj/SafetyLemmas.idr`, **all** classified `(J)` genuinely - unavoidable (see audit table below). `logSafeBounded` (SafeAPIKey.idr) + unavoidable (see audit table below; `charEqSym` was a 5th, discharged to a + theorem 2026-06-24). `logSafeBounded` (SafeAPIKey.idr) consumes these structurally and contains no direct `believe_me` — down from 31 historically. - Note: a raw `grep believe_me *.idr` returns **9** hits. 4 of these @@ -99,12 +117,15 @@ Classification key: **(J)** genuinely unavoidable, documented as an axiom; | # | Site | Function | Type | Class | Rationale | |---|------|----------|------|-------|-----------| | 1 | `SafetyLemmas.idr:60` | `charEqSound` | `(c1,c2:Char) -> c1 == c2 = True -> c1 = c2` | **J ✓** | `Char` is an opaque primitive; `==` is `prim__eqChar` (foreign `Bool`). Idris2 0.8.0 has no in-language soundness principle for primitive equality. Standard, well-understood axiom. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__eqChar.md` + BEAM property test). | -| 2 | `SafetyLemmas.idr:67` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **J ✓** | Symmetry of `prim__eqChar`. Same reason as #1 — opaque primitive, no decision procedure to recurse on. **Externally validated** (same harness as #1). | +| 2 | `SafetyLemmas.idr` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **DISCHARGED 2026-06-24** | ~~Symmetry of `prim__eqChar`~~ — superseded. NOT a necessary axiom: derived constructively from `charEqSound` (a `True` result forces `x = y`, collapsing both sides; mixed `True`/`False` impossible under soundness). Now a theorem in `SafetyLemmas.idr`; no longer counts against the trusted base. | | 3 | `SafetyLemmas.idr:218` | `unpackLength` | `length (unpack s) = length s` | **J ✓** | `unpack` = `prim__strToCharList` (foreign). `String` is opaque with no induction principle; the relation between primitive `String` length and `List Char` length is not reducible in-language. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strToCharList.md` + BEAM property test). | | 4 | `SafetyLemmas.idr:226` | `appendLengthSum` | `length (s ++ t) = length s + length t` | **J ✓** | `++` on `String` = `prim__strAppend` (foreign). Length additivity is a backend-semantics guarantee, not type-level reducible. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strAppend.md` + BEAM property test). | | 5 | `SafetyLemmas.idr:233` | `substrLengthBound` | `LTE (length (substr start len s)) len` | **J ✓** | `substr` = `prim__strSubstr` (foreign). The "result no longer than `len`" bound is a primitive-semantics guarantee with no in-language proof. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strSubstr.md` + BEAM property test). | -**Verdict: 5/5 are class (J).** All five reduce to the same root cause: +**Verdict (revised 2026-06-24): 4 class (J) + 1 discharged.** `charEqSym` +(row 2) is no longer an axiom — it was found derivable from `charEqSound` +and is now a constructive theorem (see the Discharge entry at the top of +this file). The remaining four reduce to the same root cause: Idris2 treats `Char` and `String` as opaque primitive types whose operations are foreign functions with no constructors and no induction principle. There is no constructive in-language proof for any of them; a @@ -148,19 +169,20 @@ All P1/P2 proof obligations are now closed. | BJ2 | Auth/credential handling — full isolation model | ✅ DONE (`CredentialIsolation.idr`) | | BJ3 | API contract compliance — protocol/domain coverage | ✅ DONE (`APIContractCoverage.idr`) | -### Remaining axiomatic surface (5 believe_me, all in SafetyLemmas.idr) +### Remaining axiomatic surface (4 believe_me, all in SafetyLemmas.idr) -All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0 +All four are class **(J)** — genuinely unavoidable in Idris2 0.8.0 (opaque `Char`/`String` primitives, foreign-backed operations). See the -**Axiom Audit (2026-05-18)** table above for per-site detail. +**Axiom Audit** table above for per-site detail. (`charEqSym` was a 5th here +until 2026-06-24, now discharged to a theorem — see the Discharge entry at +the top of this file.) | Axiom | Site | Justification | Backend-assurance evidence | |-------|------|---------------|----------------------------| -| `charEqSound` | `SafetyLemmas.idr:60` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` | -| `charEqSym` | `SafetyLemmas.idr:67` | Symmetry of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` | -| `unpackLength` | `SafetyLemmas.idr:218` | `prim__strToCharList` preserves length — backend primitive correctness, externally validated | `docs/backend-assurance/prim__strToCharList.md` + `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` | -| `appendLengthSum` | `SafetyLemmas.idr:226` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` | -| `substrLengthBound` | `SafetyLemmas.idr:233` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` | +| `charEqSound` | `SafetyLemmas.idr` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` | +| `unpackLength` | `SafetyLemmas.idr` | `prim__strToCharList` preserves length — backend primitive correctness, externally validated | `docs/backend-assurance/prim__strToCharList.md` + `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` | +| `appendLengthSum` | `SafetyLemmas.idr` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` | +| `substrLengthBound` | `SafetyLemmas.idr` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` | Note: `logSafeBounded` in SafeAPIKey.idr no longer uses `believe_me` directly; it calls the documented SafetyLemmas axioms via structural proof. @@ -187,8 +209,9 @@ sites stay in `SafetyLemmas.idr`. The harness shrinks the trusted base from "we trust the backend" to "we read the lowering and randomly tested the operation". -Primitives validated so far: `prim__eqChar` (covering `charEqSound` -and `charEqSym`), `prim__strToCharList` (covering `unpackLength`), +Primitives validated so far: `prim__eqChar` (covering `charEqSound`; +formerly also `charEqSym`, now a derived theorem), `prim__strToCharList` +(covering `unpackLength`), `prim__strAppend` (covering `appendLengthSum`), and `prim__strSubstr` (covering `substrLengthBound`). Tracked under epic #87 Tier C backend-assurance campaign. @@ -198,7 +221,7 @@ backend-assurance campaign. **LOW** — All named proof obligations closed. Future work: - Proofs for Dap/Bsp/CodeIntel domains when those cartridges reach Ready status - Proof that `dispatch` is surjective onto all BJ3-covered (domain, protocol) pairs -- The 5 string/char-primitive axioms are **irreducible within Idris2** +- The 4 string/char-primitive axioms are **irreducible within Idris2** (opaque primitive types). They cannot be "proved away" in-language; the only reduction path is to shrink the trusted base by validating `prim__eqChar` / `prim__strToCharList` / `prim__strAppend` / diff --git a/docs/backend-assurance/prim__eqChar.md b/docs/backend-assurance/prim__eqChar.md index f668837d..d9fa6574 100644 --- a/docs/backend-assurance/prim__eqChar.md +++ b/docs/backend-assurance/prim__eqChar.md @@ -6,18 +6,24 @@ Copyright (c) Jonathan D.A. Jewell # Backend-Assurance: `prim__eqChar` -Trusted-extraction validation for the two class-(J) axioms over -Idris2's `prim__eqChar` primitive: +Trusted-extraction validation for the class-(J) axiom over Idris2's +`prim__eqChar` primitive: - `charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2` - (`src/abi/Boj/SafetyLemmas.idr:53`) -- `charEqSym : (x, y : Char) -> (x == y) = (y == x)` - (`src/abi/Boj/SafetyLemmas.idr:60`) + (`src/abi/Boj/SafetyLemmas.idr`) -Both are `%unsafe` `believe_me` declarations in Idris2 0.8.0 because -`Char` is an opaque primitive type with no in-language induction +`charEqSound` is a `%unsafe` `believe_me` declaration in Idris2 0.8.0 +because `Char` is an opaque primitive type with no in-language induction principle. This document argues — by inspecting the backend lowerings -that BoJ actually ships against — that the believed properties hold. +that BoJ actually ships against — that the believed property holds. + +> **Note (2026-06-24):** `charEqSym : (x, y : Char) -> (x == y) = (y == x)` +> was previously a second axiom validated here. It is now a **constructive +> theorem** derived from `charEqSound` (see `SafetyLemmas.idr`), so it no +> longer needs independent backend validation — its correctness rides on +> `charEqSound` plus an in-language proof. The symmetry analysis in the +> backend sections below is retained as corroborating context (and as the +> validation basis should `charEqSym` ever be re-axiomatised). The companion property test (`elixir/test/backend_assurance/prim_eq_char_test.exs`) exercises the @@ -124,4 +130,5 @@ matching property test. - R6RS §11.11 "Characters" — `char=?` specification. - OTP `erlang(3)` — `=:=`/`=/=` specification. - `PROOF-NEEDS.md` — axiom audit (2026-05-18). -- `src/abi/Boj/SafetyLemmas.idr` — axiom declarations (lines 53, 60). +- `src/abi/Boj/SafetyLemmas.idr` — `charEqSound` axiom declaration + (`charEqSym` is now a derived theorem, not an axiom). diff --git a/docs/proof-debt.md b/docs/proof-debt.md index 9cf29272..bc13a965 100644 --- a/docs/proof-debt.md +++ b/docs/proof-debt.md @@ -7,11 +7,13 @@ Copyright (c) Jonathan D.A. Jewell **Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203). boj-server is the **reference implementation** for the estate trusted-base -reduction policy (cited as such in standards#203). The 5 class-J axioms +reduction policy (cited as such in standards#203). The 4 class-J axioms this repo isolates in `src/abi/Boj/SafetyLemmas.idr` are the canonical example of disposition §(c) NECESSARY AXIOM, and the `docs/backend-assurance/` per-axiom files are the canonical example of -external validation under §(b)-style discipline. +external validation under §(b)-style discipline. (A 5th former axiom, +`charEqSym`, was discharged to a constructive theorem on 2026-06-24 — the +first §(a) entry below.) This `docs/proof-debt.md` is a thin schema-aligned index. The substantive content lives in: @@ -26,13 +28,22 @@ content lives in: ## (a) DISCHARGED in this repo -*(None — the 5 class-J axioms are genuinely unavoidable in Idris2 0.8.0. -Items would move here if a future Idris2 version exposes in-language -soundness principles for `Char` / `String` primitives.)* +- **`charEqSym`** : `(x, y : Char) -> (x == y) = (y == x)` — *discharged + 2026-06-24*. Formerly a class-J axiom; now **derived constructively from + `charEqSound`** in `src/abi/Boj/SafetyLemmas.idr`. Intuition: a `True` + result forces propositional equality via `charEqSound`, collapsing both + sides to the same expression; a mixed `True`/`False` split is impossible + under soundness. Verified by `idris2 --typecheck boj.ipkg` (Idris2 0.8.0, + 17/17 modules clean). This is the first §(a) discharge and the reason the + sanctioned count dropped **5 → 4**. + +The remaining 4 class-J axioms are genuinely unavoidable in Idris2 0.8.0; +they would move here only if a future Idris2 exposes in-language soundness +principles for `Char` / `String` primitives. ## (b) BUDGETED — tested with a refutation budget -The 5 axioms below are documented under §(c) (NECESSARY) rather than §(b) +The 4 axioms below are documented under §(c) (NECESSARY) rather than §(b) (BUDGETED) because they cannot be discharged in-language. **However**, each one is *externally validated* via the [backend-assurance harness](./backend-assurance/) — property tests @@ -45,19 +56,19 @@ extraction-boundary code. ## (c) NECESSARY AXIOM -All 5 are class-J ("genuinely unavoidable") per -[PROOF-NEEDS.md §Axiom Audit](../PROOF-NEEDS.md) (2026-05-18). Each -reduces to the same root cause: Idris2 0.8.0 treats `Char` and `String` -as opaque primitive types whose operations are foreign functions with no -constructors and no induction principle. +All 4 are class-J ("genuinely unavoidable") per +[PROOF-NEEDS.md §Axiom Audit](../PROOF-NEEDS.md). Each reduces to the same +root cause: Idris2 0.8.0 treats `Char` and `String` as opaque primitive +types whose operations are foreign functions with no constructors and no +induction principle. (`charEqSym` was a 5th entry here until 2026-06-24, +now discharged — see §(a).) -| # | Site | Signature | External validation | +| # | Site (`SafetyLemmas.idr`) | Signature | External validation | |---|------|-----------|---------------------| -| 1 | `src/abi/Boj/SafetyLemmas.idr:60` | `charEqSound : (c1,c2 : Char) -> c1 == c2 = True -> c1 = c2` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) | -| 2 | `src/abi/Boj/SafetyLemmas.idr:67` | `charEqSym : (x,y : Char) -> (x == y) = (y == x)` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) | -| 3 | `src/abi/Boj/SafetyLemmas.idr:218` | `unpackLength : length (unpack s) = length s` | [`docs/backend-assurance/prim__strToCharList.md`](./backend-assurance/prim__strToCharList.md) | -| 4 | `src/abi/Boj/SafetyLemmas.idr:226` | `appendLengthSum : length (s ++ t) = length s + length t` | [`docs/backend-assurance/prim__strAppend.md`](./backend-assurance/prim__strAppend.md) | -| 5 | `src/abi/Boj/SafetyLemmas.idr:233` | `substrLengthBound : LTE (length (substr start len s)) len` | [`docs/backend-assurance/prim__strSubstr.md`](./backend-assurance/prim__strSubstr.md) | +| 1 | `charEqSound` | `(c1,c2 : Char) -> c1 == c2 = True -> c1 = c2` | [`docs/backend-assurance/prim__eqChar.md`](./backend-assurance/prim__eqChar.md) | +| 2 | `unpackLength` | `length (unpack s) = length s` | [`docs/backend-assurance/prim__strToCharList.md`](./backend-assurance/prim__strToCharList.md) | +| 3 | `appendLengthSum` | `length (s ++ t) = length s + length t` | [`docs/backend-assurance/prim__strAppend.md`](./backend-assurance/prim__strAppend.md) | +| 4 | `substrLengthBound` | `LTE (length (substr start len s)) len` | [`docs/backend-assurance/prim__strSubstr.md`](./backend-assurance/prim__strSubstr.md) | Citation: see standards#203 §"Precedent" — boj-server's harness is the reference implementation the estate trusted-base policy directs other @@ -65,14 +76,16 @@ proof-bearing repos to adopt. ## (d) DEBT — actively to be closed -*(None in the Idris2 ABI layer. The 5 class-J axioms above are §(c), +*(None in the Idris2 ABI layer. The 4 class-J axioms above are §(c), not §(d); they are not "to be closed" — they are load-bearing -assumptions about the trusted base.)* +assumptions about the trusted base. `charEqSym` moved §(c) → §(a) on +2026-06-24, not via Idris2 change but because it was found to be derivable +from `charEqSound`.)* Future work that would generate §(d) entries: - Migration to a future Idris2 version exposing in-language soundness - principles for primitive types — would let entries #1–#5 move from + principles for primitive types — would let entries #1–#4 move from §(c) → §(a) via discharge. - New `believe_me` introduced in non-SafetyLemmas.idr files — these must be classified as §(a)/§(b)/§(c) before merge or land here as diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh index 80a82418..2f926b0c 100755 --- a/scripts/check-trusted-base.sh +++ b/scripts/check-trusted-base.sh @@ -5,7 +5,7 @@ # check-trusted-base.sh — enforce the estate trusted-base reduction policy # (hyperpolymath/standards#203, enforcement #211) for boj-server. # -# The policy sanctions EXACTLY the 5 class-(J) axioms isolated in +# The policy sanctions EXACTLY the 4 class-(J) axioms isolated in # src/abi/Boj/SafetyLemmas.idr — opaque Char/String primitives that have no # in-language induction principle in Idris2 0.8.0, externally validated by the # backend-assurance harness (docs/backend-assurance/). Every other proof in the @@ -20,7 +20,9 @@ set -euo pipefail cd "$(dirname "$0")/.." AXIOM_FILE="src/abi/Boj/SafetyLemmas.idr" -EXPECTED_AXIOMS=5 +# 4 since charEqSym was discharged to a constructive theorem (was 5); the +# survivors are charEqSound + the three String-primitive length axioms. +EXPECTED_AXIOMS=4 echo "==> Scanning for unsound constructs outside ${AXIOM_FILE}..." FOUND=$(grep -rn 'believe_me\|assert_total\|assert_smaller\|idris_crash' \ diff --git a/specs/elixir-harness/.gitignore b/specs/elixir-harness/.gitignore new file mode 100644 index 00000000..5f4ea42e --- /dev/null +++ b/specs/elixir-harness/.gitignore @@ -0,0 +1,8 @@ +# TLC model-checker run artifacts (not source) +states/ +*_TTrace_*.tla +*_TTrace_*.bin +*.st +*.fp +MC*.tla +MC*.cfg diff --git a/specs/elixir-harness/JsWorker.cfg b/specs/elixir-harness/JsWorker.cfg new file mode 100644 index 00000000..ac3ee1d5 --- /dev/null +++ b/specs/elixir-harness/JsWorker.cfg @@ -0,0 +1,17 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Copyright (c) Jonathan D.A. Jewell +\* TLC config for the JsWorker model. +\* Run: java -cp /path/to/tla2tools.jar tlc2.TLC JsWorker.tla +CONSTANTS + Requests = {r1, r2, r3} + +SPECIFICATION Spec + +INVARIANTS + TypeOK + Consistent + ReplyOnce + NoPendingWhileDown + +PROPERTIES + EventuallyReplied diff --git a/specs/elixir-harness/JsWorker.tla b/specs/elixir-harness/JsWorker.tla new file mode 100644 index 00000000..f74cf779 --- /dev/null +++ b/specs/elixir-harness/JsWorker.tla @@ -0,0 +1,135 @@ +---------------------------- MODULE JsWorker ---------------------------- +\* SPDX-License-Identifier: MPL-2.0 +\* Copyright (c) Jonathan D.A. Jewell +(***************************************************************************) +(* Formal model of `BojRest.JsWorker` *) +(* (elixir/lib/boj_rest/js_worker.ex). *) +(* *) +(* A JsWorker is a GenServer wrapping one persistent Deno OS process (a *) +(* Port). It PIPELINES several concurrent requests to that one process, *) +(* keeping a `pending` map of id -> {caller, timer}; replies are matched by *) +(* id. Each request carries a 30s timeout. If the Deno process exits, all *) +(* pending callers are replied `:worker_crashed` and the GenServer stops so *) +(* the :one_for_one pool Supervisor can restart it with a fresh process. *) +(* *) +(* This model abstracts the Deno process to a nondeterministic oracle that, *) +(* for any pending request, may: respond ok, respond error, stay silent *) +(* (so the timer fires), or crash. Requests are opaque ids. JSON, the *) +(* HTTP layer and the Zig FFI are out of scope. *) +(* *) +(* The headline property is REPLY-ONCE: a response, a timeout and a crash *) +(* race for every in-flight id, yet each caller must be replied EXACTLY *) +(* once. In the code this is enforced by `Map.pop` (whoever pops the id *) +(* first replies; the loser sees `nil`) plus `Process.cancel_timer`. Here *) +(* it is enforced by every delivering action requiring `status[r]="pending"` *) +(* and atomically moving it to `"done"`, which disables the racing actions. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS Requests \* finite set of opaque request ids + +Replies == {"none", "ok", "jsErr", "timeout", "crashed"} + +VARIABLES + status, \* [Requests -> {"new","pending","done"}] + reply, \* [Requests -> Replies] (classification once done) + replyCount, \* [Requests -> 0..2] (how many replies were delivered) + up \* BOOLEAN (worker process alive) + +vars == <> + +TypeOK == + /\ status \in [Requests -> {"new", "pending", "done"}] + /\ reply \in [Requests -> Replies] + /\ replyCount \in [Requests -> 0..2] + /\ up \in BOOLEAN + +Init == + /\ status = [r \in Requests |-> "new"] + /\ reply = [r \in Requests |-> "none"] + /\ replyCount = [r \in Requests |-> 0] + /\ up = TRUE + +(* handle_call({:invoke, ...}): a fresh request is accepted; timer armed. *) +Arrive(r) == + /\ up + /\ status[r] = "new" + /\ status' = [status EXCEPT ![r] = "pending"] + /\ UNCHANGED <> + +(* The single guarded reply path. `Map.pop` is modelled by the *) +(* status[r]="pending" guard + atomic move to "done": once delivered, the *) +(* racing actions for r are disabled, so reply-once holds by construction. *) +Deliver(r, kind) == + /\ up + /\ status[r] = "pending" + /\ status' = [status EXCEPT ![r] = "done"] + /\ reply' = [reply EXCEPT ![r] = kind] + /\ replyCount' = [replyCount EXCEPT ![r] = @ + 1] + /\ UNCHANGED up + +RespondOk(r) == Deliver(r, "ok") \* dispatch_response, status 2xx +RespondErr(r) == Deliver(r, "jsErr") \* dispatch_response, status not 2xx +Timeout(r) == Deliver(r, "timeout") \* handle_info({:timeout, id}) + +(* handle_info({port,{:exit_status,_}}): reply-all pending, then :stop. *) +Crash == + /\ up + /\ up' = FALSE + /\ status' = [r \in Requests |-> + IF status[r] = "pending" THEN "done" ELSE status[r]] + /\ reply' = [r \in Requests |-> + IF status[r] = "pending" THEN "crashed" ELSE reply[r]] + /\ replyCount' = [r \in Requests |-> + IF status[r] = "pending" THEN replyCount[r] + 1 ELSE replyCount[r]] + +(* Supervisor :one_for_one restart: a fresh worker with empty `pending`. *) +(* Requests already replied stay replied; no pending is carried across. *) +Restart == + /\ ~up + /\ up' = TRUE + /\ UNCHANGED <> + +Next == + \/ \E r \in Requests : Arrive(r) \/ RespondOk(r) \/ RespondErr(r) \/ Timeout(r) + \/ Crash + \/ Restart + +Spec == + /\ Init /\ [][Next]_vars + /\ \A r \in Requests : WF_vars(Timeout(r)) \* the 30s timer guarantees progress + /\ WF_vars(Restart) \* the supervisor eventually restarts + +(*-------------------------------- SAFETY --------------------------------*) + +(* A pending request has no reply yet; a done request has exactly one. *) +Consistent == + /\ \A r \in Requests : (status[r] = "pending") => (reply[r] = "none") + /\ \A r \in Requests : (status[r] = "done") => (reply[r] # "none") + /\ \A r \in Requests : (status[r] = "new") => (reply[r] = "none") + +(* The headline: no caller is ever replied twice (no double GenServer.reply).*) +ReplyOnce == \A r \in Requests : replyCount[r] <= 1 + +(* Crash clears `pending` atomically: while the worker is down, nothing is *) +(* left in-flight (so a stale message cannot be replied after :stop). *) +NoPendingWhileDown == (~ up) => (\A r \in Requests : status[r] # "pending") + +(*------------------------------- LIVENESS -------------------------------*) + +(* Every request that enters the worker eventually gets a reply — the *) +(* per-request timeout guarantees this even if Deno hangs forever. *) +EventuallyReplied == + \A r \in Requests : (status[r] = "pending") ~> (status[r] = "done") + +(*--------------------------- SANITY CONTROLS ----------------------------*) +(* Each of these is EXPECTED TO BE VIOLATED when checked as an invariant *) +(* (see the loop in README.adoc). Each asserts a terminal reply kind is *) +(* never reached; TLC refuting it returns a short witness trace, proving *) +(* the model is non-vacuous and that the ok / timeout / crashed outcomes *) +(* are all genuinely reachable. They are NOT part of JsWorker.cfg. *) +ReachOk == \A r \in Requests : reply[r] # "ok" +ReachTimeout == \A r \in Requests : reply[r] # "timeout" +ReachCrashed == \A r \in Requests : reply[r] # "crashed" + +============================================================================ diff --git a/specs/elixir-harness/README.adoc b/specs/elixir-harness/README.adoc new file mode 100644 index 00000000..132ecb9b --- /dev/null +++ b/specs/elixir-harness/README.adoc @@ -0,0 +1,107 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Elixir Harness — Formal Models (TLA+) +:toc: macro + +TLA+ models of the concurrency-bearing parts of the Elixir REST harness +(`elixir/lib/boj_rest/`). These close the "the Elixir harness has no formal +coverage" gap on the *proof axis*: the Idris2 ABI proofs stop at the Zig FFI +boundary, and the BEAM-side process/supervision protocol is otherwise covered +only by ExUnit tests. + +[NOTE] +==== +This is the *formal-proof* axis. It does **not** move the CRG readiness grade +(that is the empirical/dogfooding axis in `docs/READINESS.adoc`). It closes a +verification gap, not a maturity one. +==== + +== JsWorker.tla — models `BojRest.JsWorker` + +Source: `elixir/lib/boj_rest/js_worker.ex`. A `JsWorker` is a GenServer wrapping +one persistent Deno OS process (a `Port`). It *pipelines* several concurrent +requests to that one process, keeping a `pending` map of `id -> {caller, timer}`; +replies are matched by `id`. Each request carries a 30 s timeout. If the Deno +process exits, all pending callers are replied `:worker_crashed` and the +GenServer `:stop`s so the `:one_for_one` pool Supervisor restarts it. + +=== Abstraction + +* Requests are opaque ids (the `Requests` constant). +* The Deno process is a nondeterministic oracle: for any pending request it may + respond ok, respond error, stay silent (so the timer fires), or crash. +* Out of scope: JSON encoding, the HTTP layer, and the Zig FFI — other layers + (the FFI is item 3's territory). + +=== Code → model mapping + +[cols="1,1",options="header"] +|=== +| `js_worker.ex` | model action + +| `handle_call({:invoke,...})` — adds to `pending`, arms timer | `Arrive(r)` +| `dispatch_response`, status 2xx / non-2xx (`Map.pop` + `GenServer.reply`) | `RespondOk(r)` / `RespondErr(r)` +| `handle_info({:timeout, id})` | `Timeout(r)` +| `handle_info({port,{:exit_status,_}})` — reply-all pending, `:stop` | `Crash` +| `:one_for_one` restart with a fresh Deno process | `Restart` +|=== + +The `Map.pop` rule — *whoever pops the id first replies; the loser sees `nil`* — +is modelled by every delivering action requiring `status[r] = "pending"` and +atomically moving it to `"done"`, which disables the racing actions. (In the +real code an already-queued `{:timeout,id}` message can still be delivered after +`Process.cancel_timer`, but its `Map.pop` returns `nil`, i.e. a no-op — exactly +the disabled action here.) + +=== Properties verified (TLC, `Requests = {r1, r2, r3}`) + +Safety invariants: + +* `ReplyOnce` — no caller is ever replied twice (no double `GenServer.reply`), + under *every* interleaving of response / timeout / crash. **This is the + headline result.** +* `Consistent` — pending ⟺ no reply yet; done ⟺ exactly one reply. +* `NoPendingWhileDown` — `Crash` clears `pending` atomically, so no stale + message can be replied after `:stop`. + +Liveness: + +* `EventuallyReplied` — every request that enters the worker eventually gets a + reply; the 30 s timer guarantees termination even if Deno hangs forever. + Fairness: weak fairness on each request's `Timeout` and on `Restart`. + +Result: **No error found** — 341 distinct states, search depth 8. + +=== Non-vacuity (sanity controls) + +`ReachOk`, `ReachTimeout`, `ReachCrashed` (in `JsWorker.tla`, *not* in +`JsWorker.cfg`) each assert a terminal reply kind is never reached. All three +are *refuted* by TLC with short witness traces, proving the ok / timeout / +crashed outcomes are genuinely reachable and the invariants are not passing +vacuously. + +== Running + +[source,bash] +---- +# tla2tools.jar: https://github.com/tlaplus/tlaplus/releases (needs a JRE) +java -cp tla2tools.jar tlc2.TLC JsWorker.tla + +# sanity controls — each is EXPECTED to report "Invariant ... is violated" +for inv in ReachOk ReachTimeout ReachCrashed; do + printf 'CONSTANTS Requests = {r1, r2, r3}\nSPECIFICATION Spec\nINVARIANT %s\n' "$inv" > /tmp/ctrl.cfg + java -cp tla2tools.jar tlc2.TLC -config /tmp/ctrl.cfg JsWorker.tla +done +---- + +Verified with TLC 2026.05.26 (tla2tools) on OpenJDK 21. + +== Not yet modelled (future work) + +* **`JsWorkerPool`** (`js_worker_pool.ex`) — hash-routing determinism (same + `mod_js_path` → same worker via `:erlang.phash2`, or graceful fork-per-call + fallback when the slot is dead) and `:one_for_one` crash isolation across the + N-worker pool. +* **`Invoker`** (Zig-FFI path) is currently fork-per-request — *no pool yet*; + the ADR-0005 OS-port pool is future work (waits on ADR-0006). Model the pool's + checkout/backpressure when it lands. diff --git a/src/abi/Boj/SafetyLemmas.idr b/src/abi/Boj/SafetyLemmas.idr index 7629f90d..f676cea4 100644 --- a/src/abi/Boj/SafetyLemmas.idr +++ b/src/abi/Boj/SafetyLemmas.idr @@ -6,7 +6,7 @@ ||| proofs in SafeHTTP, SafeCORS, SafeWebSocket, SafePromptInjection, ||| SafeAPIKey, and Safety modules. ||| -||| Five AXIOM-tagged believe_me primitives are declared here (per the +||| Four AXIOM-tagged believe_me primitives are declared here (per the ||| estate trusted-base reduction policy — hyperpolymath/standards#203). ||| Each is class (J) — genuinely unavoidable in Idris2 0.8.0 because ||| `Char` and `String` are opaque primitive types whose operations are @@ -17,11 +17,14 @@ ||| (audit narrative) for the per-site disposition. ||| ||| charEqSound — soundness of prim__eqChar (c1 == c2 = True → c1 = c2) -||| charEqSym — symmetry of prim__eqChar (x == y = y == x) ||| unpackLength — prim__strToCharList preserves length ||| appendLengthSum — prim__strAppend: length (s ++ t) = length s + length t ||| substrLengthBound — prim__strSubstr: result no longer than the requested count ||| +||| `charEqSym` (symmetry of prim__eqChar) is NOT in this list: it was an +||| axiom historically but is now derived constructively from `charEqSound` +||| (see its definition below). Discharging it reduced the sanctioned trusted +||| base from 5 to 4 — the first §(a) DISCHARGED entry under standards#203. ||| All other proofs in this module are constructive. module Boj.SafetyLemmas @@ -66,14 +69,33 @@ export charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2 charEqSound _ _ _ = believe_me () -||| Helper: symmetry of Char equality. -||| AXIOM: charEqSym; class-(J) — symmetry of prim__eqChar on the BEAM/Chez -||| backend. Same root cause as charEqSound. See docs/proof-debt.md §(c) -||| and docs/backend-assurance/prim__eqChar.md. -%unsafe +||| Symmetry of Char equality — a THEOREM, derived from `charEqSound`; no +||| longer a class-(J) axiom. Intuition: if either `x == y` or `y == x` is +||| `True`, soundness forces `x = y`, which collapses both sides to the same +||| expression; a mixed `True`/`False` split is therefore impossible. This +||| discharges the former `charEqSym` believe_me, shrinking the sanctioned +||| trusted base from 5 to 4 (the first §(a) DISCHARGED entry under the estate +||| trusted-base reduction policy, standards#203). See PROOF-NEEDS.md +||| §Axiom Audit and docs/proof-debt.md §(a). export charEqSym : (x, y : Char) -> (x == y) = (y == x) -charEqSym _ _ = believe_me () +charEqSym x y with (x == y) proof xy + -- `x == y = True` ⟹ `x = y`; transport the True fact along `x = y` to get + -- `y == y = True`, then rewrite the goal's `y == x` to `y == y`. + charEqSym x y | True = + let eqXY : (x = y) := charEqSound x y xy + reflY : (y == y = True) := replace {p = \z => z == y = True} eqXY xy + in rewrite eqXY in sym reflY + charEqSym x y | False with (y == x) proof yx + -- Both directions `False`: the goal is `False = False`. + charEqSym x y | False | False = Refl + -- `y == x = True` ⟹ `y = x` ⟹ `x == y = True`, contradicting + -- `x == y = False`. This split cannot occur. + charEqSym x y | False | True = + let eqYX : (y = x) := charEqSound y x yx + reflX : (x == x = True) := replace {p = \z => z == x = True} eqYX yx + xyTrue : (x == y = True) := replace {p = \z => x == z = True} (sym eqYX) reflX + in void (trueNotFalse (trans (sym xyTrue) xy)) -------------------------------------------------------------------------------- -- allRec: core lemmas for `allRec` over lists diff --git a/src/abi/README.adoc b/src/abi/README.adoc index b06faea0..6b8a57d0 100644 --- a/src/abi/README.adoc +++ b/src/abi/README.adoc @@ -50,7 +50,7 @@ The 15 modules under `Boj/` fall into four concentric rings. |=== | Module | Role -| `Boj.CartridgeDispatch` | Requirement **BJ1** — proves three core dispatch invariants (type-safe dispatch, exhaustive routing, no lost traffic). Not yet listed in `boj.ipkg` `modules`; treat as WIP trunk. +| `Boj.CartridgeDispatch` | Requirement **BJ1** — proves three core dispatch invariants (type-safe dispatch, exhaustive routing, no lost traffic). Listed in `boj.ipkg` `modules`; type-checks with the rest of the trunk. | `Boj.CredentialIsolation` | Requirement **BJ2** — per-cartridge credential-store isolation modelled at the type level. Each vault partition is indexed by cartridge name; a token must carry the matching index to read. | `Boj.Federation` | Umoja federated network protocol. Community nodes volunteer compute (Tor/IPFS-style) and prove identity by hash attestation. | `Boj.Guardian` | Resource-aware failure tolerance, preemptive thresholds, circuit breaker, self-diagnostics. @@ -81,13 +81,17 @@ matrix-cell identifier scheme. * **`%default total`** at every module top. Partial definitions are a review blocker across the whole trunk. -* **`believe_me` budget is 4 and declared.** All four live in this trunk: - * `Boj.SafetyLemmas`: `charEqSound`, `charEqSym`, `unpackLength` — three - axiomatic primitives covering discharge of `Char`/`String` equalities - that the Idris2 prelude does not expose constructively. - * `Boj.SafeAPIKey`: `logSafeBounded` at line 152 — bound on logger - safe-substring length. - Any growth in this count triggers the estate-wide believe_me sweep rule. +* **`believe_me` budget is 4 and declared.** All four live in + `Boj.SafetyLemmas`: `charEqSound`, `unpackLength`, `appendLengthSum`, + `substrLengthBound` — class-(J) axioms over opaque `Char`/`String` + primitives whose foreign `prim__*` operations the Idris2 0.8.0 prelude + does not expose constructively (no in-language induction principle). + `charEqSym` was an axiom historically but is now *derived* from + `charEqSound` (see `SafetyLemmas.idr`), dropping the count from 5 to 4 — + the first discharge under the trusted-base reduction policy (standards#203). + `Boj.SafeAPIKey`'s `logSafeBounded` is fully constructive — it consumes + these axioms structurally and contains no `believe_me`. Any growth in this + count triggers the estate-wide believe_me sweep rule. * **Zero `assert_total`, zero `postulate`, zero `Admitted`, zero `sorry`** across the trunk (verified by grep: count = 0). * **Module DAG is acyclic.** `SafeHTTP`/`SafeCORS`/`SafeWebSocket`/ @@ -105,21 +109,23 @@ blocks across 13 files; see `ffi/zig/src/README.adoc`). . `Boj/Protocol.idr` + `Boj/Domain.idr` — matrix axes. Short, definitional. . `Boj/Catalogue.idr` — what it means to be a cartridge cell, and `IsUnbreakable`. -. `Boj/SafetyLemmas.idr` — the four (three here, one in `SafeAPIKey`) - axiomatic leaves of the proof tree. Everything else refers to them. +. `Boj/SafetyLemmas.idr` — the four axiomatic leaves of the proof tree (all + here; `charEqSym` is a derived theorem, not an axiom). Everything else + refers to them. . `Boj/CartridgeDispatch.idr` (BJ1) and `Boj/CredentialIsolation.idr` (BJ2) — the two named requirements; read after you know the matrix. . Safe* modules last — they are leaves that compose the rest. == Promotion gate -This trunk is graded D in `docs/READINESS.adoc`. Lifting to C requires: +The Catalogue ABI is graded C (`alpha-stable`) in `docs/READINESS.adoc`. +Remaining proof-side hygiene: . Four `believe_me` sites justified and cross-referenced from - `SafetyLemmas` docstrings (the three lemmas are already documented as - axiomatic primitives; `logSafeBounded` needs the same treatment). -. `CartridgeDispatch.idr` added to `boj.ipkg modules` once BJ1 is ready - to be consumed. + `SafetyLemmas` docstrings — all four are documented as axiomatic + primitives, externally validated by the backend-assurance harness. +. `CartridgeDispatch.idr` (BJ1) is in `boj.ipkg modules` and type-checks + with the rest of the trunk. . Dogfood evidence in `docs/practice/DOGFOOD-LOG.adoc` showing the trunk being used in anger (cartridge load → type-check → matrix lookup round trip) in the home context.