Skip to content

Commit af3d805

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into feat/l3-gate-path-checklist
2 parents d9b4e7f + 192a25a commit af3d805

15 files changed

Lines changed: 297 additions & 159 deletions

File tree

‎.trusted-base-ignore‎

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,19 @@ crates/echidna-core-spark/src/axiom_tracker.rs
2828
# ─────────────────────────────────────────────────────────────────────────────
2929
# Hazard-classification helpers in the corpus extractor (NOT uses)
3030
# ─────────────────────────────────────────────────────────────────────────────
31-
# `corpus/agda.rs::collect_hazards` and `corpus/idris2.rs::collect_hazards`
32-
# each run a single-line `if text.contains("unsafePerformIO" / "unsafeCoerce"
33-
# / "Obj.magic")` to flag corpus entries that *contain* those patterns.
31+
# `corpus/agda.rs`, `corpus/idris2.rs` and `corpus/fstar.rs` each run a
32+
# single-line `if text.contains("unsafePerformIO" / "unsafeCoerce" / "Obj.magic"
33+
# / "admit" / ...)` to flag corpus entries that *contain* those patterns.
3434
# Same FP class — the substring is a hazard sentinel, not an escape hatch.
3535
src/rust/corpus/agda.rs
3636
src/rust/corpus/idris2.rs
37+
src/rust/corpus/fstar.rs
38+
39+
# ─────────────────────────────────────────────────────────────────────────────
40+
# Test corpus fixtures (sample prover inputs, NOT trust-kernel proofs)
41+
# ─────────────────────────────────────────────────────────────────────────────
42+
# `tests/corpus_fixtures/` holds sample source files fed to the corpus
43+
# extractors as test inputs — e.g. a minif2f Lean problem stubbed with `sorry`,
44+
# an F* smoke file with `assume val oracle`. They exercise the scanner; they are
45+
# not proof obligations in the trusted base.
46+
tests/corpus_fixtures/

‎meta-checker/src/Echidna/AxiomSafety.agda‎

Lines changed: 30 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -174,11 +174,20 @@ worst-comm Rejected IncompleteProof = refl
174174
worst-comm Rejected Rejected = refl
175175

176176
-- THEOREM: worst-policy is associative
177+
-- NB: `worst-policy` splits on its FIRST argument, so `worst-policy x c` is
178+
-- stuck for a neutral `c` unless `x` reduces to the absorbing element
179+
-- `Rejected`. Clauses whose left fold collapses to `Rejected` may keep the
180+
-- `c` wildcard; the `IncompleteProof·IncompleteProof`, `ClassicalAxioms·
181+
-- IncompleteProof` and the whole `Clean` row do NOT collapse, so they must
182+
-- enumerate the remaining argument(s) concretely for `refl` to reduce.
177183
worst-assoc : ∀ (a b c : AxiomPolicy) →
178184
worst-policy (worst-policy a b) c ≡ worst-policy a (worst-policy b c)
179185
worst-assoc Rejected _ _ = refl
180186
worst-assoc IncompleteProof Rejected _ = refl
181-
worst-assoc IncompleteProof IncompleteProof _ = refl
187+
worst-assoc IncompleteProof IncompleteProof Rejected = refl
188+
worst-assoc IncompleteProof IncompleteProof IncompleteProof = refl
189+
worst-assoc IncompleteProof IncompleteProof ClassicalAxioms = refl
190+
worst-assoc IncompleteProof IncompleteProof Clean = refl
182191
worst-assoc IncompleteProof ClassicalAxioms Rejected = refl
183192
worst-assoc IncompleteProof ClassicalAxioms IncompleteProof = refl
184193
worst-assoc IncompleteProof ClassicalAxioms ClassicalAxioms = refl
@@ -188,7 +197,10 @@ worst-assoc IncompleteProof Clean IncompleteProof = refl
188197
worst-assoc IncompleteProof Clean ClassicalAxioms = refl
189198
worst-assoc IncompleteProof Clean Clean = refl
190199
worst-assoc ClassicalAxioms Rejected _ = refl
191-
worst-assoc ClassicalAxioms IncompleteProof _ = refl
200+
worst-assoc ClassicalAxioms IncompleteProof Rejected = refl
201+
worst-assoc ClassicalAxioms IncompleteProof IncompleteProof = refl
202+
worst-assoc ClassicalAxioms IncompleteProof ClassicalAxioms = refl
203+
worst-assoc ClassicalAxioms IncompleteProof Clean = refl
192204
worst-assoc ClassicalAxioms ClassicalAxioms Rejected = refl
193205
worst-assoc ClassicalAxioms ClassicalAxioms IncompleteProof = refl
194206
worst-assoc ClassicalAxioms ClassicalAxioms ClassicalAxioms = refl
@@ -197,7 +209,22 @@ worst-assoc ClassicalAxioms Clean Rejected = refl
197209
worst-assoc ClassicalAxioms Clean IncompleteProof = refl
198210
worst-assoc ClassicalAxioms Clean ClassicalAxioms = refl
199211
worst-assoc ClassicalAxioms Clean Clean = refl
200-
worst-assoc Clean b c = refl
212+
worst-assoc Clean Rejected Rejected = refl
213+
worst-assoc Clean Rejected IncompleteProof = refl
214+
worst-assoc Clean Rejected ClassicalAxioms = refl
215+
worst-assoc Clean Rejected Clean = refl
216+
worst-assoc Clean IncompleteProof Rejected = refl
217+
worst-assoc Clean IncompleteProof IncompleteProof = refl
218+
worst-assoc Clean IncompleteProof ClassicalAxioms = refl
219+
worst-assoc Clean IncompleteProof Clean = refl
220+
worst-assoc Clean ClassicalAxioms Rejected = refl
221+
worst-assoc Clean ClassicalAxioms IncompleteProof = refl
222+
worst-assoc Clean ClassicalAxioms ClassicalAxioms = refl
223+
worst-assoc Clean ClassicalAxioms Clean = refl
224+
worst-assoc Clean Clean Rejected = refl
225+
worst-assoc Clean Clean IncompleteProof = refl
226+
worst-assoc Clean Clean ClassicalAxioms = refl
227+
worst-assoc Clean Clean Clean = refl
201228

202229
------------------------------------------------------------------------
203230
-- CRITICAL: Comment-skipping soundness

‎meta-checker/src/Echidna/Dispatch.agda‎

Lines changed: 29 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -57,12 +57,9 @@ compute-trust tf with TrustFactors.integrity-ok tf
5757
... | true | DC-Noted | true | false | true = Level3
5858
... | true | DC-Safe | true | false | false = Level3
5959
... | true | DC-Noted | true | false | false = Level3
60-
-- No certificate → Level2
60+
-- No certificate → Level2 (covers every small-kernel / cross-checked combo)
6161
... | true | DC-Safe | false | _ | _ = Level2
6262
... | true | DC-Noted | false | _ | _ = Level2
63-
-- Cross-checked large kernel without certificate → Level2
64-
... | true | DC-Safe | _ | false | true = Level2
65-
... | true | DC-Noted | _ | false | true = Level2
6663

6764
------------------------------------------------------------------------
6865
-- THEOREM: Failed integrity always produces Level1
@@ -104,25 +101,41 @@ max-trust-requires-all : ∀ (tf : TrustFactors) →
104101
TrustFactors.has-certificate tf ≡ true ×
105102
TrustFactors.small-kernel tf ≡ true ×
106103
TrustFactors.cross-checked tf ≡ true
107-
max-trust-requires-all tf p with TrustFactors.integrity-ok tf
108-
| TrustFactors.axiom-danger tf
109-
| TrustFactors.has-certificate tf
110-
| TrustFactors.small-kernel tf
111-
| TrustFactors.cross-checked tf
112-
... | true | DC-Safe | true | true | true = refl , refl , refl , refl
113-
... | true | DC-Noted | true | true | true = refl , refl , refl , refl
104+
-- Destructure the record so `compute-trust` actually reduces when we split
105+
-- on the five factors; then the hypothesis `p` reduces to a concrete
106+
-- `Levelₙ ≡ Level5`, which is `refl` only in the two genuine Level5 branches
107+
-- and absurd (`()`) in every other.
108+
max-trust-requires-all
109+
record { integrity-ok = i ; axiom-danger = d ; has-certificate = h
110+
; small-kernel = s ; cross-checked = c } p
111+
with i | d | h | s | c | p
112+
... | true | DC-Safe | true | true | true | _ = refl , refl , refl , refl
113+
... | true | DC-Noted | true | true | true | _ = refl , refl , refl , refl
114+
... | true | DC-Safe | true | true | false | ()
115+
... | true | DC-Noted | true | true | false | ()
116+
... | true | DC-Safe | true | false | true | ()
117+
... | true | DC-Noted | true | false | true | ()
118+
... | true | DC-Safe | true | false | false | ()
119+
... | true | DC-Noted | true | false | false | ()
120+
... | true | DC-Safe | false | _ | _ | ()
121+
... | true | DC-Noted | false | _ | _ | ()
122+
... | true | DC-Warning | _ | _ | _ | ()
123+
... | true | DC-Reject | _ | _ | _ | ()
124+
... | false | _ | _ | _ | _ | ()
114125

115126
------------------------------------------------------------------------
116127
-- Pipeline composition: running two stages
117128
------------------------------------------------------------------------
118129

119130
-- The pipeline result is always ≤ the initial trust level
120-
pipeline-monotonic : ∀ (t : TrustLevel) (d : DangerClass) →
131+
-- `cap-if-dangerous` (TrustLevel.agda) is indexed by `DangerLevel`
132+
-- (Safe/Noted/Warning/Reject), NOT the AxiomSafety `DangerClass`.
133+
pipeline-monotonic : ∀ (t : TrustLevel) (d : DangerLevel) →
121134
cap-if-dangerous t d ≤ₜ t
122-
pipeline-monotonic t DC-Safe = ≤ₜ-refl t
123-
pipeline-monotonic t DC-Noted = ≤ₜ-refl t
124-
pipeline-monotonic _ DC-Warning = l1≤
125-
pipeline-monotonic _ DC-Reject = l1≤
135+
pipeline-monotonic t Safe = ≤ₜ-refl t
136+
pipeline-monotonic t Noted = ≤ₜ-refl t
137+
pipeline-monotonic _ Warning = l1≤
138+
pipeline-monotonic _ Reject = l1≤
126139

127140
------------------------------------------------------------------------
128141
-- THEOREM: Pipeline is deterministic

‎meta-checker/src/Echidna/TrustLevel.agda‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,15 @@ min-trust-lb-left Level5 Level4 = l4≤5
175175
min-trust-lb-left Level5 Level5 = l5≤5
176176

177177
min-trust-lb-right : ∀ (a b : TrustLevel) → min-trust a b ≤ₜ b
178-
min-trust-lb-right _ Level1 = l1≤
178+
-- `min-trust` splits on its FIRST argument (clause `min-trust Level1 _`),
179+
-- so `min-trust a Level1` is stuck for a neutral `a`: it does not reduce to
180+
-- `Level1`. We therefore enumerate the first argument explicitly (mirroring
181+
-- `min-trust-lb-left`) so each `min-trust <Lvl> Level1` reduces to `Level1`.
182+
min-trust-lb-right Level1 Level1 = l1≤
183+
min-trust-lb-right Level2 Level1 = l1≤
184+
min-trust-lb-right Level3 Level1 = l1≤
185+
min-trust-lb-right Level4 Level1 = l1≤
186+
min-trust-lb-right Level5 Level1 = l1≤
179187
min-trust-lb-right Level1 Level2 = l1≤
180188
min-trust-lb-right Level1 Level3 = l1≤
181189
min-trust-lb-right Level1 Level4 = l1≤

‎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

0 commit comments

Comments
 (0)