Skip to content

Commit 27466d0

Browse files
claudeclaude
committed
fix(verification): harden Idris2 trust-ordering proofs with lteLit
The LTE order facts in ClampTrustBounds and TrustKernelMonotonicity were hand-written LTESucc towers whose off-diagonal entries mis-counted (e.g. l1lteL2 proved LTE 2 2 not LTE 1 2; level4LTELevel5 proved LTE 5 5 not LTE 4 5), so neither file type-checked. Add NatLte.lteLit, a decision-procedure helper over Data.Nat.isLTE that computes the witness so the count can never be wrong, and route every tower through it. Also fix TrustKernelMonotonicity's undefined \/ operator to Either, matching the Left/Right witnesses already in the bodies. Verified: idris2 --check exits 0 for NatLte, ClampTrustBounds and TrustKernelMonotonicity (ProverKindInjectivity tracked separately). https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv
1 parent 439cf3b commit 27466d0

3 files changed

Lines changed: 84 additions & 39 deletions

File tree

‎verification/proofs/idris2/ClampTrustBounds.idr‎

Lines changed: 36 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
module ClampTrustBounds
2525

2626
import Data.Nat
27+
import NatLte
2728

2829
%default total
2930

@@ -92,12 +93,12 @@ clamp_trust (S (S (S (S (S _))))) = Level5
9293
||| TrustLevel whose trustValue ≥ 1 by direct computation.
9394
public export
9495
clamp_lower_bound : (n : Nat) -> 1 `LTE` trustValue (clamp_trust n)
95-
clamp_lower_bound 0 = LTESucc LTEZero
96-
clamp_lower_bound 1 = LTESucc LTEZero
97-
clamp_lower_bound 2 = LTESucc LTEZero
98-
clamp_lower_bound 3 = LTESucc LTEZero
99-
clamp_lower_bound 4 = LTESucc LTEZero
100-
clamp_lower_bound (S (S (S (S (S _))))) = LTESucc LTEZero
96+
clamp_lower_bound 0 = lteLit 1 1
97+
clamp_lower_bound 1 = lteLit 1 1
98+
clamp_lower_bound 2 = lteLit 1 2
99+
clamp_lower_bound 3 = lteLit 1 3
100+
clamp_lower_bound 4 = lteLit 1 4
101+
clamp_lower_bound (S (S (S (S (S _))))) = lteLit 1 5
101102

102103
-- ==========================================================================
103104
-- Section 5: clamp_upper_bound
@@ -109,12 +110,12 @@ clamp_lower_bound (S (S (S (S (S _))))) = LTESucc LTEZero
109110
||| TrustLevel whose trustValue ≤ 5 by direct computation.
110111
public export
111112
clamp_upper_bound : (n : Nat) -> trustValue (clamp_trust n) `LTE` 5
112-
clamp_upper_bound 0 = LTESucc LTEZero
113-
clamp_upper_bound 1 = LTESucc LTEZero
114-
clamp_upper_bound 2 = LTESucc (LTESucc LTEZero)
115-
clamp_upper_bound 3 = LTESucc (LTESucc (LTESucc LTEZero))
116-
clamp_upper_bound 4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
117-
clamp_upper_bound (S (S (S (S (S _))))) = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
113+
clamp_upper_bound 0 = lteLit 1 5
114+
clamp_upper_bound 1 = lteLit 1 5
115+
clamp_upper_bound 2 = lteLit 2 5
116+
clamp_upper_bound 3 = lteLit 3 5
117+
clamp_upper_bound 4 = lteLit 4 5
118+
clamp_upper_bound (S (S (S (S (S _))))) = lteLit 5 5
118119

119120
-- ==========================================================================
120121
-- Section 6: clamp_monotone
@@ -145,12 +146,12 @@ data ClampZone : Nat -> Type where
145146
||| Every Nat inhabits a ClampZone.
146147
public export
147148
classifyNat : (n : Nat) -> ClampZone n
148-
classifyNat 0 = Zone01 0 LTEZero
149-
classifyNat 1 = Zone01 1 (LTESucc LTEZero)
149+
classifyNat 0 = Zone01 0 (lteLit 0 1)
150+
classifyNat 1 = Zone01 1 (lteLit 1 1)
150151
classifyNat 2 = Zone2
151152
classifyNat 3 = Zone3
152153
classifyNat 4 = Zone4
153-
classifyNat (S (S (S (S (S k))))) = Zone5up (S (S (S (S (S k))))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))
154+
classifyNat (S (S (S (S (S k))))) = Zone5up (S (S (S (S (S k))))) (lteLit 5 (S (S (S (S (S k))))))
154155

155156
||| clamp_trust is constant on zone 0 (returns Level1 for 0 and 1).
156157
clampZone01 : (n : Nat) -> n `LTE` 1 -> clamp_trust n = Level1
@@ -169,50 +170,55 @@ clampZone5up (S (S (S (S (S _))))) _ = Refl
169170

170171
-- TrustLTE lemmas for adjacent levels (used to build the monotonicity table).
171172

173+
-- Bodies use `lteLit` (machine-checked via Data.Nat.isLTE) rather than
174+
-- hand-counted LTESucc towers; the off-diagonal towers previously mis-counted
175+
-- (e.g. l1lteL2 proved LTE 2 2 instead of LTE 1 2). The count can no longer
176+
-- be wrong: `lteLit i j` type-checks iff i <= j.
177+
172178
l1lteL1 : TrustLTE Level1 Level1
173-
l1lteL1 = LTESucc LTEZero
179+
l1lteL1 = lteLit 1 1
174180

175181
l1lteL2 : TrustLTE Level1 Level2
176-
l1lteL2 = LTESucc (LTESucc LTEZero)
182+
l1lteL2 = lteLit 1 2
177183

178184
l1lteL3 : TrustLTE Level1 Level3
179-
l1lteL3 = LTESucc (LTESucc (LTESucc LTEZero))
185+
l1lteL3 = lteLit 1 3
180186

181187
l1lteL4 : TrustLTE Level1 Level4
182-
l1lteL4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
188+
l1lteL4 = lteLit 1 4
183189

184190
l1lteL5 : TrustLTE Level1 Level5
185-
l1lteL5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
191+
l1lteL5 = lteLit 1 5
186192

187193
l2lteL2 : TrustLTE Level2 Level2
188-
l2lteL2 = LTESucc (LTESucc LTEZero)
194+
l2lteL2 = lteLit 2 2
189195

190196
l2lteL3 : TrustLTE Level2 Level3
191-
l2lteL3 = LTESucc (LTESucc (LTESucc LTEZero))
197+
l2lteL3 = lteLit 2 3
192198

193199
l2lteL4 : TrustLTE Level2 Level4
194-
l2lteL4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
200+
l2lteL4 = lteLit 2 4
195201

196202
l2lteL5 : TrustLTE Level2 Level5
197-
l2lteL5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
203+
l2lteL5 = lteLit 2 5
198204

199205
l3lteL3 : TrustLTE Level3 Level3
200-
l3lteL3 = LTESucc (LTESucc (LTESucc LTEZero))
206+
l3lteL3 = lteLit 3 3
201207

202208
l3lteL4 : TrustLTE Level3 Level4
203-
l3lteL4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
209+
l3lteL4 = lteLit 3 4
204210

205211
l3lteL5 : TrustLTE Level3 Level5
206-
l3lteL5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
212+
l3lteL5 = lteLit 3 5
207213

208214
l4lteL4 : TrustLTE Level4 Level4
209-
l4lteL4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
215+
l4lteL4 = lteLit 4 4
210216

211217
l4lteL5 : TrustLTE Level4 Level5
212-
l4lteL5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
218+
l4lteL5 = lteLit 4 5
213219

214220
l5lteL5 : TrustLTE Level5 Level5
215-
l5lteL5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
221+
l5lteL5 = lteLit 5 5
216222

217223
||| clamp_monotone: n ≤ m → TrustLTE (clamp_trust n) (clamp_trust m).
218224
|||

‎verification/proofs/idris2/NatLte.idr‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- NatLte.idr — machine-checked `LTE` for literal Nats.
5+
--
6+
-- Order facts like `LTE 4 5` were previously written as hand-counted Peano
7+
-- towers `LTESucc (LTESucc (... LTEZero))`. That representation silently
8+
-- mis-counts (off-by-one between the source and target index) and is
9+
-- unreviewable for large bounds. `lteLit m n` instead runs the `Data.Nat`
10+
-- decision procedure, so the witness is computed: it type-checks iff
11+
-- `m <= n` actually holds, and the count can never be wrong.
12+
13+
module NatLte
14+
15+
import Data.Nat
16+
17+
||| Inhabited exactly when a decision landed in the `Yes` branch.
18+
public export
19+
0 IsYes : Dec p -> Type
20+
IsYes (Yes _) = ()
21+
IsYes (No _) = Void
22+
23+
||| Extract the witness from a `Yes` decision; the `No` branch is ruled out
24+
||| by `IsYes` being `Void` there.
25+
public export
26+
fromYes : (d : Dec p) -> IsYes d -> p
27+
fromYes (Yes pf) _ = pf
28+
fromYes (No _) v = absurd v
29+
30+
||| Machine-checked `LTE` for literal Nats. `lteLit m n` elaborates to the
31+
||| witness computed by `isLTE m n`; it compiles iff `m <= n` is true.
32+
public export
33+
lteLit : (m : Nat) -> (n : Nat) -> {auto ok : IsYes (isLTE m n)} -> LTE m n
34+
lteLit m n = fromYes (isLTE m n) ok

‎verification/proofs/idris2/TrustKernelMonotonicity.idr‎

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@
2020

2121
module TrustKernelMonotonicity
2222

23+
import Data.Nat
24+
import NatLte
25+
2326
%default total
2427

2528
-- ==========================================================================
@@ -68,18 +71,20 @@ TrustLTE a b = trustValue a `LTE` trustValue b
6871
-- Convenience constructor aliases used in proofs below.
6972

7073
trustLTE_refl : (t : TrustLevel) -> TrustLTE t t
71-
trustLTE_refl Level1 = LTESucc LTEZero
72-
trustLTE_refl Level2 = LTESucc (LTESucc LTEZero)
73-
trustLTE_refl Level3 = LTESucc (LTESucc (LTESucc LTEZero))
74-
trustLTE_refl Level4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
75-
trustLTE_refl Level5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
74+
trustLTE_refl Level1 = lteLit 1 1
75+
trustLTE_refl Level2 = lteLit 2 2
76+
trustLTE_refl Level3 = lteLit 3 3
77+
trustLTE_refl Level4 = lteLit 4 4
78+
trustLTE_refl Level5 = lteLit 5 5
7679

7780
||| Level4 ≤ Level4 and Level4 ≤ Level5: both satisfy ≥ Level4.
81+
||| Bodies use lteLit (machine-checked); level4LTELevel5 previously mis-counted
82+
||| as LTE 5 5 instead of LTE 4 5.
7883
level4LTELevel4 : TrustLTE Level4 Level4
79-
level4LTELevel4 = LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))
84+
level4LTELevel4 = lteLit 4 4
8085

8186
level4LTELevel5 : TrustLTE Level4 Level5
82-
level4LTELevel5 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero))))
87+
level4LTELevel5 = lteLit 4 5
8388

8489
-- ==========================================================================
8590
-- Section 4: TrustFactors record
@@ -224,7 +229,7 @@ trustMono_level5_exact
224229
: (n : Nat)
225230
-> (n >= 2 = True)
226231
-> (danger : DangerLevel)
227-
-> (danger = Safe \/ danger = Noted)
232+
-> Either (danger = Safe) (danger = Noted)
228233
-> computeTrustLevel (MkTrustFactors n True danger True True) = Level5
229234
trustMono_level5_exact n hge Safe (Left Refl) with (n >= 2)
230235
trustMono_level5_exact n hge Safe (Left Refl) | True = Refl
@@ -244,7 +249,7 @@ trustMono_level5_conditions
244249
: (n : Nat)
245250
-> (n >= 2 = True)
246251
-> (danger : DangerLevel)
247-
-> (danger = Safe \/ danger = Noted)
252+
-> Either (danger = Safe) (danger = Noted)
248253
-> TrustLTE Level4
249254
(computeTrustLevel (MkTrustFactors n True danger True True))
250255
trustMono_level5_conditions n hge Safe (Left Refl) with (n >= 2)

0 commit comments

Comments
 (0)