Skip to content

Commit aa3a16d

Browse files
claudeclaude
committed
fix(meta-checker): make Agda trust-pipeline proofs type-check
The meta-checker proofs were committed but had never actually run; `agda src/Echidna/MetaChecker.agda` failed. Three genuine errors fixed: - TrustLevel.min-trust-lb-right: min-trust splits on its first argument, so `min-trust a Level1` is stuck for a neutral a; enumerate the first arg (as min-trust-lb-left already does). - AxiomSafety.worst-assoc: three refl clauses relied on reductions that do not hold for a neutral argument; enumerate the remaining cases. - Dispatch: drop two unreachable compute-trust clauses; fix max-trust-requires-all (destructure the record so compute-trust reduces and the Level5 hypothesis is absurd in every other branch); pipeline- monotonic used DangerClass where cap-if-dangerous expects DangerLevel. Verified: agda src/Echidna/MetaChecker.agda exits 0 (Agda 2.6.3, stdlib 1.7.3). https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
1 parent 04e0e92 commit aa3a16d

3 files changed

Lines changed: 68 additions & 20 deletions

File tree

‎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≤

0 commit comments

Comments
 (0)