From 6d79c7c6c13712eecda904032f6ed36a8a599aed Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 13:55:39 +0100 Subject: [PATCH] docs(readme): disclose class-J axiom + 13/13 build posture (Refs standards#131) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a `== Formal verification` section to the README mirroring boj-server's (PR #108, 2026-05-20). Necessary update post-#41 because the README's previous claim of "machine-checked in Idris2" needed nuance now that one believe_me-bodied class-J axiom (`stringNotEqCommut`) exists in PanelIsolation. The new section names: * 13/13 ABI modules build green (was a mix of wired-and-tested vs wired-but-never-built before the standards#131 campaign discharged all four originally-deferred modules). * One believe_me invocation, isolated, classified, soundness-oracle explicit. * Forward link to PROOF-NEEDS.md "Class-J axioms (trusted base)" section (added in PR #41) for full per-site rationale. Symmetric with boj-server's README.adoc:109-129 § Formal verification which documents that repo's 5 class-(J) axioms. Estate-wide pattern: honest disclosure at the README level, full audit in PROOF-NEEDS, machine-readable state in STATE.a2ml. Refs hyperpolymath/standards#131 Refs hyperpolymath/standards#124 Co-Authored-By: Claude Opus 4.7 (1M context) --- README.adoc | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/README.adoc b/README.adoc index 2e450fd..e4f2abd 100644 --- a/README.adoc +++ b/README.adoc @@ -123,6 +123,32 @@ Gossamer is backed by formal research. The type system and its guarantees are ma _Gossamer: A Linearly-Typed Webview Shell with Provable Resource Safety_ — link:docs/whitepapers/gossamer-arxiv-paper.tex[paper source] +== Formal verification + +Gossamer's ABI is written in Idris2 with the proof obligations audited in +`PROOF-NEEDS.md`. Headline posture (as of `standards#131` close-out, 2026-05-20): + +* *All 13 ABI proof modules build green.* `gossamer-abi.ipkg` + `idris2 0.8.0 --typecheck` passes 13/13 with `%default total`. Modules: + `Types`, `Layout`, `Foreign`, `Groove`, `CapabilityAuthenticity`, + `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`, + `GrooveTermination`, `LayoutStability`, `IPCIntegrity`, + `PanelIsolation`, `ResourceCleanup`. Discharge ledger in `PROOF-NEEDS.md`. + +* *One `believe_me` invocation*, isolated in + `src/interface/abi/PanelIsolation.idr` (`stringNotEqCommut`), class (J) — + a *principled assumption*, not unproven debt. It axiomatises the + commutativity of Idris2 0.8.0's opaque `prim__eq_String` primitive + (content-symmetric on every supported backend — Chez, Racket, Node, JS — + but not derivable in-language). Same trust posture as boj-server's + `Boj.SafetyLemmas` axioms over Char/String primitives. Reduction path: + external backend-assurance evidence (property-test harness against the + primitive), not constructive in-language proof. + +* *No other unproven obligations remain in the audited surface.* The full + per-site rationale + reduce-the-trusted-base path are tracked in + `PROOF-NEEDS.md` ("Class-J axioms (trusted base)" section). + == License PMPL-1.0-or-later — Copyright (c) 2026 Jonathan D.A. Jewell