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

[hyperpolymath]

Summary

Discharges the LAST OWED item from gossamer#22's deferred list — the PanelIsolation / ResourceCleanup pair flagged "design call: String == commutativity axiom vs Distinct refactor".

idris2 0.8.0 --typecheck gossamer-abi.ipkg passes 11/11 on this branch, %default total. After gossamer#40 merges and this rebases, the result will be all 13 ABI proof modules wired and green.

Refs hyperpolymath/standards#131 and hyperpolymath/standards#124. NOT Closes — standards#131 close is owner-only (joint-close on agreement; the design choice between axiom and refactor is the substantive bit you'd want a maintainer to sign off on).

Branch base note

This branch is on origin/main (which contains GrooveTermination from gossamer#36). LayoutStability + IPCIntegrity are still in flight on gossamer#40. When both this branch and #40 land, a small ipkg-comment rebase will resolve the overlap. Module count on origin/main today: 9 wired; this branch adds 2; #40 adds 2; final state after both merge: 13 wired.

Decision: Option 1 — sanctioned class-J axiom

The earlier analysis comment on standards#131 (and this session's conversation) walked through Option 1 (axiom) vs Option 2 (Distinct-refactor). Picking Option 1 because:

1. The axiom is genuine and load-bearing for any approach. Option 2 doesn't eliminate it — it relocates the trust from "== is commutative" to "decEq correctly decides propositional equality on Strings", which is the same primitive (prim__eq_String) at one more level of indirection. Same trust budget.
2. Naming it explicitly (stringNotEqCommut, classified J in the docstring) makes the trust visible rather than hiding it inside decEq String's implementation.
3. Aligns gossamer with boj-server's posture — Boj.SafetyLemmas has 5 class-J axioms over prim__eqChar / prim__strAppend / etc, with a dedicated property-test + trusted-extraction validation harness on the way (campaign project_boj_server_backend_assurance_harness). One consistent estate story for primitive-boundary reasoning beats per-repo divergence.
4. Option 2 ergonomic cost — touching every Distinct call site, creating a style split with sibling So types in the same file (MkPanelState, MkPanelChannel) — was non-trivial for the same trust budget.

Changes

PanelIsolation.idr

A new class-J axiom between the Distinct data declaration and the distinctSym proof:

%unsafe
export
stringNotEqCommut : {a, b : String}
                 -> So (not (a == b))
                 -> So (not (b == a))
stringNotEqCommut _ = believe_me ()

distinctSym re-implemented using the axiom:

distinctSym : Distinct a b -> Distinct b a
distinctSym (MkDistinct {a} {b} {prf}) =
  MkDistinct {a=b} {b=a} {prf = stringNotEqCommut prf}

Moduledoc's "Zero believe_me" banner replaced with an honest "One class-J axiom (stringNotEqCommut); all other proofs constructive." — better accurate than aspirational; this is gossamer's first class-J axiom.

ResourceCleanup.idr

The OWED note bundled this with PanelIsolation, but the actual defects were independent:

#	Defect	Fix
1	Missing import Data.DPair (for Exists / Evidence)	Added the import
2	Typo: lowercase exists should be Exists (Idris2 0.8.0 stdlib capitalises it; idris2 suggested the fix in the error message)	Renamed at line 228

gossamer-abi.ipkg

Module list extended with the two newly-wired modules. Header deferred-list comment replaced with a closure summary noting where each formerly-deferred module landed (#36 / #40 / this branch).

Verification

$ idris2 --typecheck gossamer-abi.ipkg
 1/11: Building Gossamer.ABI.Types
 2/11: Building Gossamer.ABI.Groove
 3/11: Building Gossamer.ABI.HandleLinearity
 4/11: Building Gossamer.ABI.PanelIsolation
 5/11: Building Gossamer.ABI.ResourceCleanup
 6/11: Building Gossamer.ABI.GrooveTermination
 7/11: Building Gossamer.ABI.WindowStateMachine
 8/11: Building Gossamer.ABI.IPCDispatch
 9/11: Building Gossamer.ABI.CapabilityAuthenticity
10/11: Building Gossamer.ABI.Layout
11/11: Building Gossamer.ABI.Foreign
EXIT=0

Soundness oracle (deferred)

This class-J axiom is principled (prim__eq_String is commutative on every supported backend — Chez, Racket, Node, JS — because they all dispatch to native string-equal which is content-symmetric), but it's still trust that needs external validation. The boj-server project_boj_server_backend_assurance_harness campaign is building exactly that validation infrastructure (property-tests + trusted-extraction against Chez/BEAM). When that harness exists for gossamer, this axiom can be replaced with a backend-verified theorem.

🤖 Generated with Claude Code

[hyperpolymath]

CI auto-trigger anomaly — same as boj-server#132 earlier this session

pull_request workflows did not auto-fire on this branch. Only dogfood-gate.yml (on a push event) ran, and it failed at setup level — not a code defect.

Same diagnosis as boj-server#132 (PR comment): the estate-wide CI concurrency-pool exhaustion from the active sweep122 campaign (memory: project_ci_concurrency_pool_estate, Terminal-7 PID 244005 launched 09:33Z). Other PRs in this session triggered fine when slots were free; the pool is now saturated.

The critical workflow (abi-typecheck.yml → idris2 --typecheck gossamer-abi.ipkg) does NOT support workflow_dispatch, so I cannot manually trigger it.

Local oracle:

$ idris2 --typecheck gossamer-abi.ipkg
 1/11: Building Gossamer.ABI.Types
 2/11: Building Gossamer.ABI.Groove
 3/11: Building Gossamer.ABI.HandleLinearity
 4/11: Building Gossamer.ABI.PanelIsolation
 5/11: Building Gossamer.ABI.ResourceCleanup
 6/11: Building Gossamer.ABI.GrooveTermination
 7/11: Building Gossamer.ABI.WindowStateMachine
 8/11: Building Gossamer.ABI.IPCDispatch
 9/11: Building Gossamer.ABI.CapabilityAuthenticity
10/11: Building Gossamer.ABI.Layout
11/11: Building Gossamer.ABI.Foreign
EXIT=0

Owner: please re-run from the Actions tab once the pool frees up — that's the merge oracle.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	11
🟠 High	4
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/upload-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/download-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/gossamer/gossamer/src/interface/abi/IPCDispatch.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/gossamer/gossamer/src/interface/abi/ResourceCleanup.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/gossamer/gossamer/src/interface/abi/GrooveTermination.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/gossamer/gossamer/src/interface/abi/HandleLinearity.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/gossamer/gossamer/src/interface/abi/WindowStateMachine.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence