Skip to content

Commit 93d72b2

Browse files
claudeclaude
committed
fix(abi): make Idris2 ABI package type-check
idris2 --build echidnaabi.ipkg failed at several modules; all are genuine (the package had never been built clean): - Foreign.idr declared module Echidna.ABI.Foreign and imported Echidna.ABI.{Types,Layout}; corrected to the EchidnaABI.* namespace the package + path require. Added the missing Result ADT it uses and passed the callback to the FFI directly (no closure->AnyPtr cast). - Gnn.idr: trailing ||| doc block -> -- (must attach to a decl); featureDimPositive proved LTE 32 32 not LTE 1 32; sparseAdjLengthsEqual needs lengthCorrect (length recurses, Refl will not reduce abstract vectors); maxNodesMonotone is false for a zero branching factor, restated for (S bf); makeDualPair inlines its edges so the projections reduce. - AxiomTracker.idr: comma-separate multi-arg lambdas; import Data.List.Elem; DecEq not DecidableEq; soundness/precision assumed any reduces structurally (it folds via foldl) -> introduced a structural hasDanger and reproved both. Verified: clean idris2 --build echidnaabi.ipkg exits 0 (19/19, Idris2 0.8.0). https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
1 parent aa3a16d commit 93d72b2

3 files changed

Lines changed: 105 additions & 78 deletions

File tree

‎src/abi/EchidnaABI/AxiomTracker.idr‎

Lines changed: 54 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ module EchidnaABI.AxiomTracker
1717

1818
import EchidnaABI.Types -- ProverKind, Platform, etc.
1919
import Data.List
20+
import Data.List.Elem
2021
import Data.So
2122
import Decidable.Equality
2223

@@ -44,7 +45,7 @@ Eq DangerLevel where
4445
_ == _ = False
4546

4647
public export
47-
DecidableEq DangerLevel where
48+
DecEq DangerLevel where
4849
decEq Safe Safe = Yes Refl
4950
decEq Noted Noted = Yes Refl
5051
decEq Warning Warning = Yes Refl
@@ -117,6 +118,15 @@ isAcceptable _ = True
117118
-- (These are what SPARK GNATprove formally verifies on the Ada side.)
118119
-- ════════════════════════════════════════════════════════════════════════════
119120

121+
||| Structural existential over a danger level. Unlike the Foldable `any`
122+
||| (which folds via `foldl`, so it does NOT reduce on cons), this recurses
123+
||| structurally — letting the soundness/precision proofs below go through by
124+
||| induction with definitional reduction of the head test `x == d`.
125+
public export
126+
hasDanger : DangerLevel -> List DangerLevel -> Bool
127+
hasDanger _ [] = False
128+
hasDanger d (x :: xs) = (x == d) || hasDanger d xs
129+
120130
||| Specification of enforcePolicySpec: the reference function that the
121131
||| SPARK implementation must replicate.
122132
|||
@@ -125,9 +135,9 @@ isAcceptable _ = True
125135
public export
126136
enforcePolicySpec : List DangerLevel -> AxiomPolicy
127137
enforcePolicySpec usages =
128-
if any (== Reject) usages then PolicyRejected
129-
else if any (== Warning) usages then PolicyIncomplete
130-
else if any (== Noted) usages then PolicyClassical
138+
if hasDanger Reject usages then PolicyRejected
139+
else if hasDanger Warning usages then PolicyIncomplete
140+
else if hasDanger Noted usages then PolicyClassical
131141
else PolicyClean
132142

133143
-- ────────────────────────────────────────────────────────────────────────────
@@ -141,25 +151,21 @@ soundness
141151
-> Elem Reject usages
142152
-> enforcePolicySpec usages = PolicyRejected
143153
soundness usages prf =
144-
rewrite anyRejectIsTrue usages prf in Refl
154+
rewrite hasRejectIsTrue usages prf in Refl
145155
where
146-
-- Prove any (== Reject) us = True given Reject ∈ us.
147-
-- We case-split on the head constructor so that 'x == Reject' reduces
156+
-- Prove hasDanger Reject us = True given Reject ∈ us.
157+
-- Case-split on the head constructor so that 'x == Reject' reduces
148158
-- definitionally before applying the induction hypothesis via rewrite.
149-
anyRejectIsTrue
159+
hasRejectIsTrue
150160
: (us : List DangerLevel)
151161
-> Elem Reject us
152-
-> any (== Reject) us = True
153-
anyRejectIsTrue [] p = absurd p
154-
anyRejectIsTrue (Reject :: _) Here = Refl
155-
anyRejectIsTrue (Safe :: xs) (There p) =
156-
let ih := anyRejectIsTrue xs p in rewrite ih in Refl
157-
anyRejectIsTrue (Noted :: xs) (There p) =
158-
let ih := anyRejectIsTrue xs p in rewrite ih in Refl
159-
anyRejectIsTrue (Warning :: xs) (There p) =
160-
let ih := anyRejectIsTrue xs p in rewrite ih in Refl
161-
anyRejectIsTrue (Reject :: xs) (There p) =
162-
let ih := anyRejectIsTrue xs p in rewrite ih in Refl
162+
-> hasDanger Reject us = True
163+
hasRejectIsTrue [] p = absurd p
164+
hasRejectIsTrue (Reject :: _) Here = Refl
165+
hasRejectIsTrue (Safe :: xs) (There p) = rewrite hasRejectIsTrue xs p in Refl
166+
hasRejectIsTrue (Noted :: xs) (There p) = rewrite hasRejectIsTrue xs p in Refl
167+
hasRejectIsTrue (Warning :: xs) (There p) = rewrite hasRejectIsTrue xs p in Refl
168+
hasRejectIsTrue (Reject :: xs) (There _) = Refl
163169

164170
-- ────────────────────────────────────────────────────────────────────────────
165171
-- Invariant 2 (Precision): no Reject-in → not PolicyRejected-out
@@ -172,35 +178,38 @@ precision
172178
-> ((e : DangerLevel) -> Elem e usages -> Not (e = Reject))
173179
-> Not (enforcePolicySpec usages = PolicyRejected)
174180
precision usages noReject prf =
175-
-- Derive any (== Reject) usages = False from the no-Reject hypothesis.
176-
-- Then case-split on all three 'any' booleans so enforcePolicySpec usages
177-
-- reduces definitionally in each branch; each non-Rejected result gives a
178-
-- constructor mismatch with prf : ... = PolicyRejected.
179-
let anyFalse := noRejectMeansAnyFalse usages noReject
180-
in case any (== Reject) usages of
181-
True => absurd anyFalse -- anyFalse : True = False
182-
False =>
183-
case any (== Warning) usages of
184-
True => case prf of { Refl impossible } -- PolicyIncomplete ≠ PolicyRejected
185-
False =>
186-
case any (== Noted) usages of
187-
True => case prf of { Refl impossible } -- PolicyClassical ≠ PolicyRejected
188-
False => case prf of { Refl impossible } -- PolicyClean ≠ PolicyRejected
181+
-- A PolicyRejected verdict forces the Reject flag True (rejTrue); the
182+
-- no-Reject hypothesis forces it False — contradiction.
183+
absurd (trans (sym (rejTrue usages prf)) (noRejectMeansFalse usages noReject))
189184
where
190-
-- Case-split on each constructor so 'x == Reject' reduces definitionally,
191-
-- making 'False || any (== Reject) xs = any (== Reject) xs' automatic.
192-
noRejectMeansAnyFalse
185+
-- enforcePolicySpec us = PolicyRejected can only arise via the Reject
186+
-- guard. `with` on each flag lets the spec reduce per branch, so every
187+
-- non-Reject branch contradicts `p` and the Reject branch returns Refl.
188+
rejTrue : (us : List DangerLevel) ->
189+
enforcePolicySpec us = PolicyRejected -> hasDanger Reject us = True
190+
rejTrue us p with (hasDanger Reject us)
191+
rejTrue us p | True = Refl
192+
rejTrue us p | False with (hasDanger Warning us)
193+
rejTrue us p | False | True = case p of { Refl impossible }
194+
rejTrue us p | False | False with (hasDanger Noted us)
195+
rejTrue us p | False | False | True = case p of { Refl impossible }
196+
rejTrue us p | False | False | False = case p of { Refl impossible }
197+
198+
-- No Reject in the list ⇒ the structural Reject check is False.
199+
-- 'x == Reject' reduces definitionally, so 'False || hasDanger Reject xs'
200+
-- collapses to the inductive hypothesis.
201+
noRejectMeansFalse
193202
: (us : List DangerLevel)
194203
-> ((e : DangerLevel) -> Elem e us -> Not (e = Reject))
195-
-> any (== Reject) us = False
196-
noRejectMeansAnyFalse [] _ = Refl
197-
noRejectMeansAnyFalse (Safe :: xs) noR =
198-
noRejectMeansAnyFalse xs (\e p => noR e (There p))
199-
noRejectMeansAnyFalse (Noted :: xs) noR =
200-
noRejectMeansAnyFalse xs (\e p => noR e (There p))
201-
noRejectMeansAnyFalse (Warning :: xs) noR =
202-
noRejectMeansAnyFalse xs (\e p => noR e (There p))
203-
noRejectMeansAnyFalse (Reject :: xs) noR =
204+
-> hasDanger Reject us = False
205+
noRejectMeansFalse [] _ = Refl
206+
noRejectMeansFalse (Safe :: xs) noR =
207+
rewrite noRejectMeansFalse xs (\e, p => noR e (There p)) in Refl
208+
noRejectMeansFalse (Noted :: xs) noR =
209+
rewrite noRejectMeansFalse xs (\e, p => noR e (There p)) in Refl
210+
noRejectMeansFalse (Warning :: xs) noR =
211+
rewrite noRejectMeansFalse xs (\e, p => noR e (There p)) in Refl
212+
noRejectMeansFalse (Reject :: xs) noR =
204213
void (noR Reject Here Refl)
205214

206215
-- ════════════════════════════════════════════════════════════════════════════

‎src/abi/EchidnaABI/Foreign.idr‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,28 @@
77
||| All functions are declared here with type signatures and safety proofs.
88
||| Implementations live in ffi/zig/
99

10-
module Echidna.ABI.Foreign
10+
module EchidnaABI.Foreign
1111

12-
import Echidna.ABI.Types
13-
import Echidna.ABI.Layout
12+
import EchidnaABI.Types
13+
import EchidnaABI.Layout
1414

1515
%default total
1616

17+
--------------------------------------------------------------------------------
18+
-- FFI Result codes
19+
--------------------------------------------------------------------------------
20+
21+
||| Result / error codes returned across the C ABI boundary.
22+
||| Mirrors the discriminant set consumed by `resultFromInt` below and the
23+
||| `echidna_*` C entry points implemented in ffi/zig/.
24+
public export
25+
data Result : Type where
26+
Ok : Result
27+
Error : Result
28+
InvalidParam : Result
29+
OutOfMemory : Result
30+
NullPointer : Result
31+
1732
--------------------------------------------------------------------------------
1833
-- Library Lifecycle
1934
--------------------------------------------------------------------------------
@@ -184,13 +199,13 @@ Callback = Bits64 -> Bits32 -> Bits32
184199
||| Register a callback
185200
export
186201
%foreign "C:echidna_register_callback, libechidna"
187-
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
202+
prim__registerCallback : Bits64 -> Callback -> PrimIO Bits32
188203

189204
||| Safe callback registration
190205
export
191206
registerCallback : Handle -> Callback -> IO (Either Result ())
192207
registerCallback h cb = do
193-
result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
208+
result <- primIO (prim__registerCallback (handlePtr h) cb)
194209
pure $ case resultFromInt result of
195210
Just Ok => Right ()
196211
Just err => Left err

‎src/abi/EchidnaABI/Gnn.idr‎

Lines changed: 31 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -55,13 +55,8 @@ FeatureVector = Vect FeatureDim Double
5555
||| Required for normalisation denominators and embedding operations.
5656
public export
5757
featureDimPositive : GT FeatureDim 0
58-
featureDimPositive = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
59-
(LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
60-
(LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
61-
(LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
62-
(LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
63-
(LTESucc (LTESucc (LTESucc (LTESucc (LTESucc
64-
(LTESucc (LTESucc LTEZero)))))))))))))))))))))))))))))))
58+
-- GT FeatureDim 0 ≡ LT 0 32 ≡ LTE 1 32 ≡ LTESucc (LTEZero : LTE 0 31).
59+
featureDimPositive = LTESucc LTEZero
6560

6661
------------------------------------------------------------------------
6762
-- Graph Structure Properties
@@ -114,7 +109,12 @@ public export
114109
sparseAdjLengthsEqual : (adj : SparseAdjacency n) ->
115110
(length (rows adj) = length (cols adj),
116111
length (cols adj) = length (vals adj))
117-
sparseAdjLengthsEqual (MkSparseAdj rs cs vs) = (Refl, Refl)
112+
-- `Data.Vect.length` recurses structurally, so it does not reduce to the
113+
-- type-level index for an abstract vector; `lengthCorrect xs : length xs = n`
114+
-- supplies the bridge, and the two equalities chain through `n`.
115+
sparseAdjLengthsEqual (MkSparseAdj rs cs vs) =
116+
( trans (lengthCorrect rs) (sym (lengthCorrect cs))
117+
, trans (lengthCorrect cs) (sym (lengthCorrect vs)) )
118118

119119
------------------------------------------------------------------------
120120
-- Premise Ranking Properties
@@ -167,16 +167,16 @@ maxNodesAtDepth : (maxDepth : Nat) -> (branchingFactor : Nat) -> Nat
167167
maxNodesAtDepth Z _ = 1
168168
maxNodesAtDepth (S d) bf = bf * maxNodesAtDepth d bf
169169

170-
||| Proof: maxNodesAtDepth is monotonically non-decreasing in depth.
170+
||| Proof: maxNodesAtDepth is monotonically non-decreasing in depth, for a
171+
||| positive branching factor. A factor of 0 is degenerate (0^0 = 1 but
172+
||| 0^(d+1) = 0, which is NOT monotone), so the property genuinely requires
173+
||| branchingFactor >= 1; we encode that by taking the factor as `S bf`.
174+
||| Then maxNodesAtDepth (S d) (S bf) = (S bf) * m = m + bf * m, so the bound
175+
||| is exactly `lteAddRight m`.
171176
public export
172177
maxNodesMonotone : (d : Nat) -> (bf : Nat) ->
173-
LTE (maxNodesAtDepth d bf) (maxNodesAtDepth (S d) bf)
174-
maxNodesMonotone Z bf = lteAddRight 1
175-
maxNodesMonotone (S d) bf =
176-
let ih = maxNodesMonotone d bf
177-
prev = maxNodesAtDepth (S d) bf
178-
next = maxNodesAtDepth (S (S d)) bf
179-
in lteTransitive (lteAddRight prev) (lteReflexive {n = next})
178+
LTE (maxNodesAtDepth d (S bf)) (maxNodesAtDepth (S d) (S bf))
179+
maxNodesMonotone d bf = lteAddRight (maxNodesAtDepth d (S bf))
180180

181181
------------------------------------------------------------------------
182182
-- Node Kind Enumeration Completeness
@@ -261,10 +261,13 @@ data DualEdgePair : (src : Nat) -> (tgt : Nat) -> Type where
261261
||| we can construct the corresponding UsefulFor edge.
262262
public export
263263
makeDualPair : (src : Nat) -> (tgt : Nat) -> (w : Double) -> DualEdgePair src tgt
264+
-- The edges are inlined (rather than `let`-bound) so the record
265+
-- projections in MkDual's equality arguments reduce definitionally and
266+
-- each proof closes by `Refl`.
264267
makeDualPair src tgt w =
265-
let fwd = MkGraphEdge src tgt DependsOn w
266-
rev = MkGraphEdge tgt src UsefulFor w
267-
in MkDual fwd rev Refl Refl Refl Refl Refl Refl
268+
MkDual (MkGraphEdge src tgt DependsOn w) -- forward edge: DependsOn
269+
(MkGraphEdge tgt src UsefulFor w) -- reverse edge: UsefulFor
270+
Refl Refl Refl Refl Refl Refl
268271

269272
------------------------------------------------------------------------
270273
-- Cosine Similarity Bounds
@@ -285,12 +288,12 @@ data CosineSimilarityWellDefined : Type where
285288
-- Graph Invariants Summary
286289
------------------------------------------------------------------------
287290

288-
||| Summary of all GNN integration invariants proven in this module:
289-
|||
290-
||| 1. featureDimPositive: Feature dimension is > 0 (safe for division)
291-
||| 2. sparseAdjLengthsEqual: Adjacency vectors are length-consistent
292-
||| 3. nodeKindIndexInjective: Node kind encoding has no collisions
293-
||| 4. edgeKindIndexInjective: Edge kind encoding has no collisions
294-
||| 5. maxNodesMonotone: Deeper expansion produces >= nodes (termination)
295-
||| 6. makeDualPair: DependsOn/UsefulFor edges are always paired
296-
||| 7. combinedScoreBounded: Weighted score combination preserves bounds
291+
-- Summary of all GNN integration invariants proven in this module:
292+
--
293+
-- 1. featureDimPositive: Feature dimension is > 0 (safe for division)
294+
-- 2. sparseAdjLengthsEqual: Adjacency vectors are length-consistent
295+
-- 3. nodeKindIndexInjective: Node kind encoding has no collisions
296+
-- 4. edgeKindIndexInjective: Edge kind encoding has no collisions
297+
-- 5. maxNodesMonotone: Deeper expansion produces >= nodes (termination)
298+
-- 6. makeDualPair: DependsOn/UsefulFor edges are always paired
299+
-- 7. combinedScoreBounded: Weighted score combination preserves bounds

0 commit comments

Comments
 (0)