Skip to content

fix(abi): CapnSchemas proved its claims about implicit variables; qualify, gate it in the ipkg #472

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 9 commits into from
Nov 9, 2026
Merged

fix(abi): CapnSchemas proved its claims about implicit variables; qualify, gate it in the ipkg #472

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
20dc691
fix(deps): move rmcp to 3.9.0 off three RustSec advisories
claude Nov 9, 2026
17ebbb1
style: rustfmt src/rust/proof_search.rs
claude Nov 9, 2026
f48fe0a
fix(ffi): annotate the audited Zig context-pointer casts for Hypatia
claude Nov 9, 2026
b00eec3
Merge remote-tracking branch 'origin/claude/new-session-th4e9w-fmt-pr…
claude Nov 9, 2026
1e0d68a
Merge remote-tracking branch 'origin/claude/new-session-th4e9w-zig-ca…
claude Nov 9, 2026
4dab099
fix(abi): CapnSchemas proved its claims about implicit variables; qua…
claude Nov 9, 2026
1013f3b
Merge remote-tracking branch 'origin/claude/new-session-th4e9w-rustse…
claude Nov 9, 2026
d34d0ef
Merge branch 'main' into claude/new-session-th4e9w-abi-capnschemas
hyperpolymath Nov 9, 2026
1d0d8b6
Merge branch 'main' into claude/new-session-th4e9w-abi-capnschemas
hyperpolymath Nov 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .claude/CLAUDE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,8 @@ package definitions (not metadata files) and must NOT be deleted.
|---------------|----------|-------|
| **Rust** | Core systems, prover backends, trust pipeline, CLI, WASM | Primary implementation language |
| **Julia** | ML inference, batch data processing, extract scripts | Per RSR |
| **Idris2** | ABI formal proofs (zero `believe_me`) | `src/abi/` — 16 modules, constructive |
| **Agda** | Trust-pipeline meta-checker proofs | `proofs/agda/` |
| **Idris2** | ABI formal proofs (zero `believe_me`) | `src/abi/` — modules listed in `echidnaabi.ipkg`, constructive |
| **Agda** | Trust-pipeline meta-checker proofs | `meta-checker/` (CI-gated, pinned Agda); `proofs/agda/` is a fixture corpus (PROOF-POLICY §3) |
| **Zig** | FFI shim between Rust and Chapel | `src/zig_ffi/` |
| **Chapel** | Optional parallel proof dispatch | Wired via Cargo `chapel` feature |
| **Guile Scheme** | Guix package definitions (`guix.scm`, `manifests/*.scm`) | `.scm` metadata files are deprecated — see below |
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/idris2-abi-ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ jobs:
if: steps.detect.outputs.relevant == 'true'
run: |
cd src/abi
echo "=== Type-checking ECHIDNA ABI package (16 modules) ==="
echo "=== Type-checking ECHIDNA ABI package (modules listed in echidnaabi.ipkg) ==="
idris2 --build echidnaabi.ipkg
echo "✓ All ABI modules type-check successfully"

Expand Down
24 changes: 12 additions & 12 deletions src/abi/EchidnaABI/CapnSchemas.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ echidnaSchemaId = 15242516543891767314
||| Cap'n Proto uses 0 as the "no schema" sentinel; a zero schema ID
||| would silently poison all wire messages.
public export
schemaIdNonZero : Not (echidnaSchemaId = 0)
schemaIdNonZero : Not (EchidnaABI.CapnSchemas.echidnaSchemaId = 0)
schemaIdNonZero = \h => absurd h

------------------------------------------------------------------------
Expand Down Expand Up @@ -74,7 +74,7 @@ proofGoalFieldCount = 6
||| Proof: ProofGoal has exactly 6 fields.
||| The Vect literal fixes the length at compile time; this is Refl.
public export
proofGoalFieldCountCorrect : length allProofGoalTags = proofGoalFieldCount
proofGoalFieldCountCorrect : length EchidnaABI.CapnSchemas.allProofGoalTags = EchidnaABI.CapnSchemas.proofGoalFieldCount
proofGoalFieldCountCorrect = Refl

------------------------------------------------------------------------
Expand Down Expand Up @@ -133,7 +133,7 @@ outcomeTagToFinInjective SystemError SystemError Refl = Refl

||| Proof: 8 outcome variants fit in a UInt8 (cardinality ≤ 256).
public export
outcomeBounded : LTE outcomeTagCount 256
outcomeBounded : LTE EchidnaABI.CapnSchemas.outcomeTagCount 256
outcomeBounded = %search

------------------------------------------------------------------------
Expand Down Expand Up @@ -163,7 +163,7 @@ nodeKindCount : Nat
nodeKindCount = 7

public export
nodeKindCountCorrect : length allCapnNodeKinds = nodeKindCount
nodeKindCountCorrect : length EchidnaABI.CapnSchemas.allCapnNodeKinds = EchidnaABI.CapnSchemas.nodeKindCount
nodeKindCountCorrect = Refl

public export
Expand Down Expand Up @@ -191,7 +191,7 @@ nodeKindToFinInjective CNK_Term CNK_Term Refl = Refl

||| Proof: 7 node kinds fit in a UInt8.
public export
nodeKindBounded : LTE nodeKindCount 256
nodeKindBounded : LTE EchidnaABI.CapnSchemas.nodeKindCount 256
nodeKindBounded = %search

------------------------------------------------------------------------
Expand Down Expand Up @@ -222,7 +222,7 @@ edgeKindCount : Nat
edgeKindCount = 8

public export
edgeKindCountCorrect : length allCapnEdgeKinds = edgeKindCount
edgeKindCountCorrect : length EchidnaABI.CapnSchemas.allCapnEdgeKinds = EchidnaABI.CapnSchemas.edgeKindCount
edgeKindCountCorrect = Refl

public export
Expand Down Expand Up @@ -252,7 +252,7 @@ edgeKindToFinInjective CEK_HasSubterm CEK_HasSubterm Refl = Refl

||| Proof: 8 edge kinds fit in a UInt8.
public export
edgeKindBounded : LTE edgeKindCount 256
edgeKindBounded : LTE EchidnaABI.CapnSchemas.edgeKindCount 256
edgeKindBounded = %search

------------------------------------------------------------------------
Expand All @@ -276,7 +276,7 @@ dangerLevelCount : Nat
dangerLevelCount = 4

public export
dangerLevelCountCorrect : length allCapnDangerLevels = dangerLevelCount
dangerLevelCountCorrect : length EchidnaABI.CapnSchemas.allCapnDangerLevels = EchidnaABI.CapnSchemas.dangerLevelCount
dangerLevelCountCorrect = Refl

public export
Expand All @@ -298,7 +298,7 @@ dangerLevelToFinInjective CDL_Reject CDL_Reject Refl = Refl

||| Proof: 4 danger levels fit in a UInt8.
public export
dangerLevelBounded : LTE dangerLevelCount 256
dangerLevelBounded : LTE EchidnaABI.CapnSchemas.dangerLevelCount 256
dangerLevelBounded = %search

------------------------------------------------------------------------
Expand All @@ -321,7 +321,7 @@ dispatchStrategyCount : Nat
dispatchStrategyCount = 3

public export
dispatchStrategyCountCorrect : length allCapnDispatchStrategies = dispatchStrategyCount
dispatchStrategyCountCorrect : length EchidnaABI.CapnSchemas.allCapnDispatchStrategies = EchidnaABI.CapnSchemas.dispatchStrategyCount
dispatchStrategyCountCorrect = Refl

public export
Expand All @@ -341,7 +341,7 @@ dispatchStrategyToFinInjective CDS_Portfolio CDS_Portfolio Refl = Refl

||| Proof: 3 dispatch strategies fit in a UInt8.
public export
dispatchStrategyBounded : LTE dispatchStrategyCount 256
dispatchStrategyBounded : LTE EchidnaABI.CapnSchemas.dispatchStrategyCount 256
dispatchStrategyBounded = %search

------------------------------------------------------------------------
Expand All @@ -356,5 +356,5 @@ defaultTopK = 20
||| Proof: the default topK is positive (> 0).
||| Required by the GNN ranking logic which uses topK as a loop bound.
public export
topKDefaultPositive : GT defaultTopK 0
topKDefaultPositive : GT EchidnaABI.CapnSchemas.defaultTopK 0
topKDefaultPositive = %search
1 change: 1 addition & 0 deletions src/abi/echidnaabi.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ modules = EchidnaABI.AxiomTracker
, EchidnaABI.Provers.AutoActive
, EchidnaABI.Provers.ConstraintSolvers
, EchidnaABI.VqlUt
, EchidnaABI.CapnSchemas

@chatgpt-codex-connector chatgpt-codex-connector Bot Nov 9, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Correct the schema ID before packaging this module

When downstream ABI code imports the newly packaged module, it receives an incorrect echidnaSchemaId: schemas/echidna.capnp:12 declares 0xd3b45f8ae1c79012, whose decimal value is 15254922887908790290, while CapnSchemas.idr:37 exports 15242516543891767314 (0xd3884c09d1af0012). The new nonzero proof still succeeds because it proves only that this mismatched value is not zero, so consumers relying on the mirror for schema identification can use an incompatible ID; correct the constant before adding the module to the package.

Useful? React with 👍 / 👎.

, Overlay
, Overlay.Foreign
, Boj.Foreign
Expand Down
Loading