Skip to content

docs(readme): disclose class-J axiom + 13/13 build posture (Refs standards#131)#43

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/proof-disclosure-readme
May 20, 2026
Merged

docs(readme): disclose class-J axiom + 13/13 build posture (Refs standards#131)#43
hyperpolymath merged 1 commit into
mainfrom
docs/proof-disclosure-readme

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Adds a == Formal verification section to the gossamer README, mirroring boj-server's section added in boj-server#108. Necessary post-#41 because the README's previous claim ("machine-checked in Idris2") needed nuance now that one believe_me-bodied class-J axiom (stringNotEqCommut) exists in PanelIsolation.

Refs hyperpolymath/standards#131 (the campaign that introduced the axiom), Refs hyperpolymath/standards#124 (proof-debt epic).

What's in

A new section between == Research and == License:

== Formal verification

* All 13 ABI proof modules build green. (gossamer-abi.ipkg
  idris2 0.8.0 --typecheck passes 13/13, %default total.)
* One believe_me invocation — stringNotEqCommut in PanelIsolation.idr,
  class-(J), axiomatising prim__eq_String commutativity. Sanctioned
  principled assumption over a primitive, not unproven debt.
* No other unproven obligations remain in the audited surface.

Forward links to PROOF-NEEDS.md "Class-J axioms (trusted base)" section (added in PR #41) for the full per-site rationale + reduce-the-trusted-base path.

Estate symmetry

Mirrors boj-server's README.adoc:109-129 § Formal verification (which documents that repo's 5 class-(J) axioms in Boj.SafetyLemmas). Same posture: honest disclosure at README level, full audit in PROOF-NEEDS, machine-readable state in STATE.a2ml.

Verification

  • AsciiDoc renders cleanly in GitHub.
  • Link to gossamer-abi.ipkg and PROOF-NEEDS.md resolve.

Risk

Negligible. README-only.

🤖 Generated with Claude Code

…dards#131)

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) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 20, 2026 13:03
@hyperpolymath hyperpolymath merged commit c71c88d into main May 20, 2026
14 of 16 checks passed
@hyperpolymath hyperpolymath deleted the docs/proof-disclosure-readme branch May 20, 2026 13:05
@hyperpolymath hyperpolymath restored the docs/proof-disclosure-readme branch May 20, 2026 13:06
hyperpolymath added a commit that referenced this pull request May 20, 2026
…#45)

Closes the design question flagged in cli/src/Main.eph:13-16. Adds
cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc documenting the actual
call chain and amends the Main.eph comment to point at it.

Short answer: the existing single-threaded launcher + synchronous
host-import bridges are already the correct integration. When the
guest calls env::gossamer_run via wasmtime, control passes through
bridges.zig:270 (bRun) back into Zig on the same OS thread that
called gtk_init via gossamer_create_ex — satisfying GTK's
"same thread for init + main" invariant. No architectural change
required.

Unblocks Phase 14b subcommand-body port (#42) for `dev` and `run`.

Refs #42

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 20, 2026
…#48)

Closes the design question flagged in cli/src/Main.eph:13-16. Adds
cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc documenting the actual
call chain and amends the Main.eph comment to point at it.

Short answer: the existing single-threaded launcher + synchronous
host-import bridges are already the correct integration. When the
guest calls env::gossamer_run via wasmtime, control passes through
bridges.zig:270 (bRun) back into Zig on the same OS thread that
called gtk_init via gossamer_create_ex — satisfying GTK's
"same thread for init + main" invariant. No architectural change
required.

Unblocks Phase 14b subcommand-body port (#42) for `dev` and `run`.

Refs #42

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath deleted the docs/proof-disclosure-readme branch May 20, 2026 22:01
@github-actions
Copy link
Copy Markdown

🔍 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant