Claude/cartridge abi proofs#204
Merged
Merged
Conversation
All 104 cartridge ABI modules now type-check under the pinned toolchain
(Idris2 0.8.0, Chez). Previously 21 cartridges failed — they had never
been gated (CI only runs iseriser's structural check; `just typecheck`
covers just 5 cartridges and isn't wired into CI), so they drifted into
non-compiling states. Fixes are grouped by root cause; theorem
statements and the axiom budget are unchanged.
- Reserved-keyword record fields (0.8.0 reserves these): `total`→
`totalCount` (conflow, panic-attack, reposystem), `data`→`payload`
(ephapax), `namespace`→`namespaceName` (k8s, ml), `prefix`→`txnPrefix`
(matrix).
- Missing imports: `Data.List` for `NonEmpty` (panic-attack, stapeln,
civic-connect, hypatia, local-coord/Protocol); `Data.Nat` for `LTE`
(pmpl).
- `lteTransitive`→`transitive` + explicit `{s,n}` binders, since the
index is needed at the use site (hypatia).
- Visibility/layout: `public` → `public export`; modifier on its own
line so the `where`-block isn't mis-indented relative to `record`/
`data` (academic-workflow, hesiod); unqualified `interface` names.
- `data X = MkC (n : T)` → `MkC T` (named fields are GADT-only syntax)
(model-router, burble-admin).
- `octadLength` via `Data.Vect.lengthCorrect` (Refl can't reduce
`length` on an abstract `Vect`) (verisimdb).
- Name collision: `ValidTransition` `Connect`/`Disconnect` (proof-only)
renamed `TConnect`/`TDisconnect` so the FFI-bearing `PostgresqlAction`
enum keeps its constructors (postgresql).
- Large type-level Nat blowup: `ValidPort` now takes explicit `LTE`
proofs built via `Data.Nat.lteReflectsLTE` (the builtin-Integer path),
mirroring SafeWebSocket's `FrameSizeSafeUpTo` fix — typecheck drops
from >90s (OOM/timeout) to ~2s (local-coord).
- `IsLoopback` moved from a type-level function with a giant Nat literal
pattern (`IsLoopback 5178 = ()`, ~150s) into a top-level GADT, matching
the other adapters (~1s) (bofig, ephapax, fireflag, sanctify).
- A pre-existing proof bug surfaced once the blowup was gone:
`identityDoesNotEnableFederation` relied on the nullary CAF
`coordFederationPolicy` reducing to `LocalOnly` in the unifier (it
doesn't); restated over `LocalOnly` directly (local-coord/Identity).
https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa
Root-cause durability for the cartridge-ABI drift: nothing in CI ran `idris2 --typecheck` on cartridges/**/abi (abi-drift.yml only runs iseriser's structural manifest), and the Justfile's `typecheck` recipe covered just 5 of ~50 cartridge ABIs. So 99 ABIs rotted undetected. - scripts/typecheck-proofs.sh — type-checks the core ABI package and EVERY cartridge ABI (ipkg if present, else each .idr). PASS=105/105. - scripts/check-trusted-base.sh — the trusted-base audit that PROOF-NEEDS.md and docs/proof-debt.md already reference but which never existed: fails on any unsound construct outside SafetyLemmas.idr and on drift from the 5 sanctioned class-(J) axioms. - .github/workflows/proofs.yml — runs both gates on changes under src/abi, cartridges/**/abi, verification, and the toolchain pin. Installs the pinned Idris2 (.tool-versions → 0.8.0) via asdf. - Justfile: `typecheck` and `verify-no-believe-me` now delegate to the scripts, so local `just` and CI share one source of truth. https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa
- trusted-base job gets timeout-minutes (Hypatia workflow_audit rule). - typecheck-proofs.sh: cd||exit (SC2164) and find instead of ls (SC2012). https://claude.ai/code/session_019tMcRS1Dm1nWjjYP4WvbJa
🏁 path-claims benchCommit NumbersHost-dependent — compare deltas across commits, not absolute values. |
🔍 Hypatia Security ScanFindings: 278 issues detected
View findings[
{
"reason": "Stale AI session file -- delete",
"type": "stale",
"file": "GEMINI.md",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "medium"
},
{
"reason": "Action if: always()\n uses: actions/upload-artifact@ea165f8 needs attention",
"type": "unpinned_action",
"file": "e2e.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in abi-drift.yml",
"type": "missing_timeout_minutes",
"file": "abi-drift.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in container-publish.yml",
"type": "missing_timeout_minutes",
"file": "container-publish.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
enabled auto-merge (squash)
June 5, 2026 13:40
🔍 Hypatia Security ScanFindings: 278 issues detected
View findings[
{
"reason": "Stale AI session file -- delete",
"type": "stale",
"file": "GEMINI.md",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "medium"
},
{
"reason": "Action if: always()\n uses: actions/upload-artifact@ea165f8 needs attention",
"type": "unpinned_action",
"file": "e2e.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in abi-drift.yml",
"type": "missing_timeout_minutes",
"file": "abi-drift.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in container-publish.yml",
"type": "missing_timeout_minutes",
"file": "container-publish.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
.machine_readable/STATE.a2mlupdated (if project state changed).machine_readable/ECOSYSTEM.a2mlupdated (if integrations changed).machine_readable/META.a2mlupdated (if architectural decisions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/abi/andffi/zig/consistent)Testing
Screenshots