Skip to content

Commit 349b1e5

Browse files
feggefegge
committed
Added a few more u128 correctness proofs
1 parent 1ca6e31 commit 349b1e5

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

69 files changed

+2495
-121
lines changed

‎MidenLean/Proofs/U128/And.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ open MidenLean.StepLemmas
99
open MidenLean.Tactics
1010

1111
set_option maxHeartbeats 4000000 in
12-
/-- u128.and correctly computes bitwise AND of two 128-bit values.
12+
/-- `u128::and` correctly computes bitwise AND of two 128-bit values.
1313
Input stack: [b0, b1, b2, b3, a0, a1, a2, a3] ++ rest
1414
Output stack: [b0 &&& a0, b1 &&& a1, b2 &&& a2, b3 &&& a3] ++ rest. -/
1515
theorem u128_and_correct

‎MidenLean/Proofs/U128/Clo.lean‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
import MidenLean.Proofs.Tactics
2+
import MidenLean.Generated.U128
3+
4+
namespace MidenLean.Proofs
5+
6+
open MidenLean
7+
open MidenLean.StepLemmas
8+
open MidenLean.Tactics
9+
10+
set_option maxHeartbeats 12000000 in
11+
/-- `u128::clo` correctly counts leading ones of a u128 value.
12+
Input stack: [a, b, c, d] ++ rest
13+
Output stack: [result] ++ rest
14+
where `a..d` are low-to-high u32 limbs and the result is the number of
15+
leading one bits in the 128-bit value. -/
16+
theorem u128_clo_correct
17+
(a b c d : Felt) (rest : List Felt) (s : MidenState)
18+
(hs : s.stack = a :: b :: c :: d :: rest)
19+
(ha : a.isU32 = true) (hb : b.isU32 = true)
20+
(hc : c.isU32 = true) (hd : d.isU32 = true) :
21+
exec 33 s Miden.Core.U128.clo =
22+
some (s.withStack (
23+
(if d == (4294967295 : Felt) then
24+
if c == (4294967295 : Felt) then
25+
if b == (4294967295 : Felt) then
26+
Felt.ofNat (u32CountLeadingZeros (u32Max - 1 - a.val)) + 96
27+
else
28+
Felt.ofNat (u32CountLeadingZeros (u32Max - 1 - b.val)) + 64
29+
else
30+
Felt.ofNat (u32CountLeadingZeros (u32Max - 1 - c.val)) + 32
31+
else
32+
Felt.ofNat (u32CountLeadingZeros (u32Max - 1 - d.val))) :: rest)) := by
33+
obtain ⟨stk, mem, locs, adv⟩ := s
34+
simp only [MidenState.withStack] at hs ⊢
35+
subst hs
36+
unfold exec Miden.Core.U128.clo execWithEnv
37+
simp only [List.foldlM]
38+
miden_movup
39+
miden_dup
40+
rw [stepEqImm]
41+
miden_bind
42+
by_cases hd1 : d == (4294967295 : Felt)
43+
· simp [hd1, MidenState.withStack]
44+
unfold execWithEnv
45+
simp only [List.foldlM]
46+
rw [stepDrop]
47+
miden_bind
48+
miden_movup
49+
miden_dup
50+
rw [stepEqImm]
51+
miden_bind
52+
by_cases hc1 : c == (4294967295 : Felt)
53+
· simp [hc1, MidenState.withStack]
54+
unfold execWithEnv
55+
simp only [List.foldlM]
56+
rw [stepDrop]
57+
miden_bind
58+
miden_swap
59+
miden_dup
60+
rw [stepEqImm]
61+
miden_bind
62+
by_cases hb1 : b == (4294967295 : Felt)
63+
· simp [hb1, MidenState.withStack]
64+
unfold execWithEnv
65+
simp only [List.foldlM]
66+
rw [stepDrop]
67+
miden_bind
68+
rw [stepU32Clo (ha := ha)]
69+
miden_bind
70+
rw [stepAddImm]
71+
have hc_eq : c = 4294967295 := by exact beq_iff_eq.mp hc1
72+
have hb_eq : b = 4294967295 := by exact beq_iff_eq.mp hb1
73+
simp [hc_eq, hb_eq]
74+
· simp [hb1, MidenState.withStack]
75+
unfold execWithEnv
76+
simp only [List.foldlM]
77+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
78+
rw [stepSwap (hn := by decide) (htop := rfl) (hnth := rfl)]
79+
miden_bind
80+
rw [stepDrop]
81+
miden_bind
82+
rw [stepU32Clo (ha := hb)]
83+
miden_bind
84+
rw [stepAddImm]
85+
have hc_eq : c = 4294967295 := by exact beq_iff_eq.mp hc1
86+
have hb_ne : b ≠ 4294967295 := by
87+
intro hb_eq
88+
exact hb1 (by simp [hb_eq])
89+
simp [hc_eq, hb_ne]
90+
· simp [hc1, MidenState.withStack]
91+
unfold execWithEnv
92+
simp only [List.foldlM]
93+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
94+
miden_movdn
95+
rw [stepDrop]
96+
miden_bind
97+
rw [stepDrop]
98+
miden_bind
99+
rw [stepU32Clo (ha := hc)]
100+
miden_bind
101+
rw [stepAddImm]
102+
have hc_ne : c ≠ 4294967295 := by
103+
intro hc_eq
104+
exact hc1 (by simp [hc_eq])
105+
simp [hc_ne]
106+
· simp [hd1, MidenState.withStack]
107+
unfold execWithEnv
108+
simp only [List.foldlM]
109+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
110+
miden_movdn
111+
rw [stepDrop]
112+
miden_bind
113+
rw [stepDrop]
114+
miden_bind
115+
rw [stepDrop]
116+
miden_bind
117+
rw [stepU32Clo (ha := hd)]
118+
119+
end MidenLean.Proofs

‎MidenLean/Proofs/U128/Clz.lean‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
import MidenLean.Proofs.Tactics
2+
import MidenLean.Generated.U128
3+
4+
namespace MidenLean.Proofs
5+
6+
open MidenLean
7+
open MidenLean.StepLemmas
8+
open MidenLean.Tactics
9+
10+
set_option maxHeartbeats 12000000 in
11+
/-- `u128::clz` correctly counts leading zeros of a u128 value.
12+
Input stack: [a, b, c, d] ++ rest
13+
Output stack: [result] ++ rest
14+
where `a..d` are low-to-high u32 limbs and the result is the number of
15+
leading zero bits in the 128-bit value. -/
16+
theorem u128_clz_correct
17+
(a b c d : Felt) (rest : List Felt) (s : MidenState)
18+
(hs : s.stack = a :: b :: c :: d :: rest)
19+
(ha : a.isU32 = true) (hb : b.isU32 = true)
20+
(hc : c.isU32 = true) (hd : d.isU32 = true) :
21+
exec 33 s Miden.Core.U128.clz =
22+
some (s.withStack (
23+
(if d == (0 : Felt) then
24+
if c == (0 : Felt) then
25+
if b == (0 : Felt) then
26+
Felt.ofNat (u32CountLeadingZeros a.val) + 96
27+
else
28+
Felt.ofNat (u32CountLeadingZeros b.val) + 64
29+
else
30+
Felt.ofNat (u32CountLeadingZeros c.val) + 32
31+
else
32+
Felt.ofNat (u32CountLeadingZeros d.val)) :: rest)) := by
33+
obtain ⟨stk, mem, locs, adv⟩ := s
34+
simp only [MidenState.withStack] at hs ⊢
35+
subst hs
36+
unfold exec Miden.Core.U128.clz execWithEnv
37+
simp only [List.foldlM]
38+
miden_movup
39+
miden_dup
40+
rw [stepEqImm]
41+
miden_bind
42+
by_cases hd0 : d == (0 : Felt)
43+
· simp [hd0, MidenState.withStack]
44+
unfold execWithEnv
45+
simp only [List.foldlM]
46+
rw [stepDrop]
47+
miden_bind
48+
miden_movup
49+
miden_dup
50+
rw [stepEqImm]
51+
miden_bind
52+
by_cases hc0 : c == (0 : Felt)
53+
· simp [hc0, MidenState.withStack]
54+
unfold execWithEnv
55+
simp only [List.foldlM]
56+
rw [stepDrop]
57+
miden_bind
58+
miden_swap
59+
miden_dup
60+
rw [stepEqImm]
61+
miden_bind
62+
by_cases hb0 : b == (0 : Felt)
63+
· simp [hb0, MidenState.withStack]
64+
unfold execWithEnv
65+
simp only [List.foldlM]
66+
rw [stepDrop]
67+
miden_bind
68+
rw [stepU32Clz (ha := ha)]
69+
miden_bind
70+
rw [stepAddImm]
71+
have hc_eq : c = 0 := by exact beq_iff_eq.mp hc0
72+
have hb_eq : b = 0 := by exact beq_iff_eq.mp hb0
73+
simp [hc_eq, hb_eq]
74+
· simp [hb0, MidenState.withStack]
75+
unfold execWithEnv
76+
simp only [List.foldlM]
77+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
78+
rw [stepSwap (hn := by decide) (htop := rfl) (hnth := rfl)]
79+
miden_bind
80+
rw [stepDrop]
81+
miden_bind
82+
rw [stepU32Clz (ha := hb)]
83+
miden_bind
84+
rw [stepAddImm]
85+
have hc_eq : c = 0 := by exact beq_iff_eq.mp hc0
86+
have hb_ne : b ≠ 0 := by
87+
intro hb_eq
88+
exact hb0 (by simp [hb_eq])
89+
simp [hc_eq, hb_ne]
90+
· simp [hc0, MidenState.withStack]
91+
unfold execWithEnv
92+
simp only [List.foldlM]
93+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
94+
miden_movdn
95+
rw [stepDrop]
96+
miden_bind
97+
rw [stepDrop]
98+
miden_bind
99+
rw [stepU32Clz (ha := hc)]
100+
miden_bind
101+
rw [stepAddImm]
102+
have hc_ne : c ≠ 0 := by
103+
intro hc_eq
104+
exact hc0 (by simp [hc_eq])
105+
simp [hc_ne]
106+
· simp [hd0, MidenState.withStack]
107+
unfold execWithEnv
108+
simp only [List.foldlM]
109+
simp (config := { decide := true }) only [bind, Bind.bind, Option.bind, pure, Pure.pure]
110+
miden_movdn
111+
rw [stepDrop]
112+
miden_bind
113+
rw [stepDrop]
114+
miden_bind
115+
rw [stepDrop]
116+
miden_bind
117+
rw [stepU32Clz (ha := hd)]
118+
119+
end MidenLean.Proofs

‎MidenLean/Proofs/U128/Common.lean‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,11 @@ def u128ProcEnv : ProcEnv := fun name =>
1111
| "overflowing_sub" => some Miden.Core.U128.overflowing_sub
1212
| "overflowing_mul" => some Miden.Core.U128.overflowing_mul
1313
| "gt" => some Miden.Core.U128.gt
14+
| "gte" => some Miden.Core.U128.gte
1415
| "lt" => some Miden.Core.U128.lt
16+
| "lte" => some Miden.Core.U128.lte
17+
| "max" => some Miden.Core.U128.max
18+
| "min" => some Miden.Core.U128.min
1519
| "wrapping_mul" => some Miden.Core.U128.wrapping_mul
1620
| "shr_k0" => some Miden.Core.U128.shr_k0
1721
| "shr_k1" => some Miden.Core.U128.shr_k1
@@ -22,4 +26,34 @@ def u128ProcEnv : ProcEnv := fun name =>
2226
| "divmod" => some Miden.Core.U128.divmod
2327
| _ => none
2428

29+
def u128Sub0 (a0 b0 : Felt) : Nat × Nat :=
30+
u32OverflowingSub a0.val b0.val
31+
32+
def u128Sub1 (a1 b1 : Felt) : Nat × Nat :=
33+
u32OverflowingSub a1.val b1.val
34+
35+
def u128Borrow1 (a0 a1 b0 b1 : Felt) : Felt :=
36+
if decide ((u128Sub1 a1 b1).2 < (u128Sub0 a0 b0).1) || decide (a1.val < b1.val) then
37+
1
38+
else
39+
0
40+
41+
def u128Sub2 (a2 b2 : Felt) : Nat × Nat :=
42+
u32OverflowingSub a2.val b2.val
43+
44+
def u128Borrow2 (a0 a1 a2 b0 b1 b2 : Felt) : Felt :=
45+
if decide ((u128Sub2 a2 b2).2 < (u128Borrow1 a0 a1 b0 b1).val) || decide (a2.val < b2.val) then
46+
1
47+
else
48+
0
49+
50+
def u128Sub3 (a3 b3 : Felt) : Nat × Nat :=
51+
u32OverflowingSub a3.val b3.val
52+
53+
def u128LtBool (a0 a1 a2 a3 b0 b1 b2 b3 : Felt) : Bool :=
54+
decide ((u128Sub3 a3 b3).2 < (u128Borrow2 a0 a1 a2 b0 b1 b2).val) || decide (a3.val < b3.val)
55+
56+
def u128GtBool (a0 a1 a2 a3 b0 b1 b2 b3 : Felt) : Bool :=
57+
u128LtBool b0 b1 b2 b3 a0 a1 a2 a3
58+
2559
end MidenLean.Proofs

0 commit comments

Comments
 (0)