fix(abi): wire PanelIsolation + ResourceCleanup via class-J axiom (proof-debt standards#131)

PROOF-NEEDS.md

@@ -14,7 +14,9 @@
 - `src/interface/abi/ResourceCleanup.idr` — Resource cleanup on teardown proofs ✅
 - `src/interface/abi/WindowStateMachine.idr` — Window state machine correctness (GS1) ✅ NEW 2026-04-11
 - `src/interface/abi/IPCDispatch.idr` — IPC handler type safety, 25 handlers (GS2) ✅ NEW 2026-04-11
-- No `believe_me`, `sorry`, `postulate`, or `assert_total` in ABI layer
+- **All 13 ABI modules above are now wired into `gossamer-abi.ipkg` and pass `idris2 0.8.0 --typecheck` cleanly** (2026-05-20, `standards#131` close-out). Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle.
+- **One class-J axiom**: `Gossamer.ABI.PanelIsolation.stringNotEqCommut` — sanctioned principled assumption over the Idris2 backend primitive `prim__eq_String` (content-symmetry on every supported backend; cannot be derived inside Idris2). `%unsafe`-annotated, `believe_me ()`-bodied, documented at the use site. Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` and four sibling axioms over String / Char primitives. See "Class-J axioms (trusted base)" section below.
+- No other `believe_me`, `sorry`, `postulate`, or `assert_total` in the ABI layer.
 - Zig FFI layer in `src/interface/ffi/`
 
 ## What needs proving
@@ -32,3 +34,27 @@
 
 ## Priority
 - **LOW** — 7 of 8 proof requirements completed. Only extension loading safety remains, blocked on Ephapax module system completion.
+
+## Class-J axioms (trusted base)
+
+This repo has one class-J axiom, sanctioned and documented:
+
+| Axiom | Module | Justification | Soundness oracle |
+|---|---|---|---|
+| `stringNotEqCommut` | `Gossamer.ABI.PanelIsolation` | Commutativity of `prim__eq_String`: the Idris2 backend primitive for `String == String`. Holds on every supported backend (Chez, Racket, Node, JS — all dispatch to native string-equal which is content-symmetric). Cannot be derived inside Idris2 (opaque primitive with no constructors / induction principle). | Per-backend property-test validation (deferred to the backend-assurance harness once ported from boj-server's `project_boj_server_backend_assurance_harness`). |
+
+The axiom is `%unsafe`-marked and the function body is `believe_me ()` — explicit, named, audited; **not unproven debt**. Sites that depend on it: `PanelIsolation.distinctSym`.
+
+**Reduce-the-trusted-base path**: when gossamer adopts the backend-assurance harness, `stringNotEqCommut` can be promoted from class-J axiom to a backend-verified theorem via runtime correspondence tests against the primitive.
+
+## Discharge ledger (2026-05-20, standards#131 close-out)
+
+| Module | Discharged in | State |
+|---|---|---|
+| GrooveTermination | [gossamer#36](https://github.com/hyperpolymath/gossamer/pull/36) | **MERGED** |
+| LayoutStability | [gossamer#40](https://github.com/hyperpolymath/gossamer/pull/40) | **MERGED** |
+| IPCIntegrity | [gossamer#40](https://github.com/hyperpolymath/gossamer/pull/40) | **MERGED** |
+| PanelIsolation (+ class-J axiom) | [gossamer#41](https://github.com/hyperpolymath/gossamer/pull/41) | open, ready, idris2 ✓ 13/13 local |
+| ResourceCleanup | [gossamer#41](https://github.com/hyperpolymath/gossamer/pull/41) | same branch as #41 |
+
+**Lesson memorialised**: the OWED notes carried in the original gossamer#22 deferred-list misdiagnosed the root cause on every one of the four deferred items. The notes named `choose` / theorem restatement / axiom-vs-refactor; the actual fixes were `module-qualify the names` / `reorder + 0-quantity-mark + add accessors` / `import + capitalise the typo` / `class-J axiom` (the last one was right by accident). **Build is the only oracle for proof-bearing code; comment-only notes from never-built modules are hints, not specs.**

gossamer-abi.ipkg

@@ -35,13 +35,18 @@ modules = Gossamer.ABI.Types
         , Gossamer.ABI.GrooveTermination
         , Gossamer.ABI.LayoutStability
         , Gossamer.ABI.IPCIntegrity
-
--- DEFERRED (owner design call — Refs standards#131). Syntactic/structural
--- defects were fixed in-tree, but each module has RESIDUAL proof/design
--- debt that is not a clean discharge. Excluded so the CI gate stays
--- green and the debt stays visible rather than silently bit-rotting:
---   * PanelIsolation / ResourceCleanup — `distinctSym` needs commutativity
---     of primitive String `==`: a sanctioned String-primitive bridge axiom
---     or refactor `Distinct` to carry `Not (a = b)`.
---      , Gossamer.ABI.PanelIsolation
---      , Gossamer.ABI.ResourceCleanup
+        , Gossamer.ABI.PanelIsolation
+        , Gossamer.ABI.ResourceCleanup
+
+-- All formerly-deferred ABI proof modules from gossamer#22's OWED list
+-- are now wired and `idris2 --typecheck` green:
+--   * GrooveTermination  — discharged in gossamer#36 (MERGED)
+--   * LayoutStability    — discharged in gossamer#40 (MERGED)
+--   * IPCIntegrity       — discharged in gossamer#40 (MERGED)
+--   * PanelIsolation     — discharged in this branch via a sanctioned
+--                           class-J axiom (`stringNotEqCommut`) over the
+--                           Idris2 backend primitive `prim__eq_String`.
+--                           First class-J axiom in gossamer; same trust
+--                           posture as boj-server's `Boj.SafetyLemmas.*`.
+--   * ResourceCleanup    — discharged in this branch (missing `Data.DPair`
+--                           import + lowercase `exists` → `Exists`).

src/interface/abi/PanelIsolation.idr

@@ -15,7 +15,11 @@
 ||| 3. Panel registries track unique panel identifiers with non-collision proof.
 ||| 4. No panel can forge another panel's state token.
 |||
-||| Zero believe_me. All proofs are constructive.
+||| One class-J axiom: `stringNotEqCommut` — commutativity of the
+||| Idris2 backend primitive `prim__eq_String`. Sanctioned principled
+||| assumption over a foreign primitive (same trust posture as
+||| boj-server's `Boj.SafetyLemmas.charEqSym`), not unproven debt. All
+||| other proofs in this module are constructive.
 
 module Gossamer.ABI.PanelIsolation
 
@@ -50,10 +54,47 @@ data Distinct : (a : PanelTag) -> (b : PanelTag) -> Type where
              -> {auto 0 prf : So (not (a == b))}
              -> Distinct a b
 
+--------------------------------------------------------------------------------
+-- Class-J axiom: String `==` commutativity (Refs standards#131 / #124)
+--------------------------------------------------------------------------------
+
+||| AXIOM (class-J): primitive String inequality is commutative.
+|||
+||| The `(==)` operator on `String` is the `Eq String` instance, which
+||| dispatches to Idris2's backend primitive `prim__eq_String`. The
+||| primitive is an opaque foreign function with no constructors and no
+||| in-language induction principle — its commutativity over content
+||| equality (`a == b` ⇔ `b == a`) holds on every supported backend
+||| (Chez, Racket, Node, JS — all dispatch to native string-equal which
+||| is content-symmetric) but cannot be derived inside Idris2 itself.
+|||
+||| Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym`
+||| (symmetry of `prim__eqChar`) and four sibling axioms over String /
+||| Char primitives. Audited as **class-(J)** — principled assumption
+||| over an Idris2 primitive, not unproven debt. See PROOF-NEEDS.md (in
+||| boj-server) for the per-site convention; this is gossamer's first
+||| class-J axiom and is documented at the use site rather than in a
+||| dedicated `SafetyLemmas` module — that module can be lifted out
+||| later if a second axiom appears.
+|||
+||| Soundness oracle: property-test validation against the runtime,
+||| per the boj-server backend-assurance harness pattern. A reduce-the-
+||| trusted-base PR can replace this axiom with a `prim__eq_String` /
+||| `prim__strEq` symmetry proof once that harness exists for gossamer.
+|||
+||| Refs: standards#131 (PanelIsolation `distinctSym`),
+||| standards#124 (proof-debt epic).
+%unsafe
+export
+stringNotEqCommut : {a, b : String} -> So (not (a == b)) -> So (not (b == a))
+stringNotEqCommut _ = believe_me ()
+
 ||| Distinctness is symmetric: if a /= b then b /= a.
+||| Constructive modulo `stringNotEqCommut` (class-J axiom above).
 public export
 distinctSym : Distinct a b -> Distinct b a
-distinctSym (MkDistinct {a} {b} {prf}) = MkDistinct {a=b} {b=a}
+distinctSym (MkDistinct {a} {b} {prf}) =
+  MkDistinct {a=b} {b=a} {prf = stringNotEqCommut prf}
 
 --------------------------------------------------------------------------------
 -- Panel-Scoped State

src/interface/abi/ResourceCleanup.idr

@@ -27,6 +27,7 @@ import Data.Bits
 import Data.Nat
 import Data.List
 import Data.List.Elem
+import Data.DPair
 
 %default total
 
@@ -224,7 +225,7 @@ data ShellTeardown : Type where
 ||| Given any number of panel registries and a shell registry,
 ||| we can always produce a complete ShellTeardown.
 public export
-shellTeardownTotal : (panels : List (exists (\rs => Registry rs)))
+shellTeardownTotal : (panels : List (Exists (\rs => Registry rs)))
                    -> (shell : Registry shellRs)
                    -> ShellTeardown
 shellTeardownTotal panels shell =