Skip to content

Commit 8b161f0

Browse files
feggefegge
committed
Added u128 shr_k2 and shr_k3 correctness proofs
1 parent 349b1e5 commit 8b161f0

File tree

3 files changed

+323
-0
lines changed

3 files changed

+323
-0
lines changed

‎MidenLean/Proofs/U128/Common.lean‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,35 @@
1+
import MidenLean.Proofs.Helpers
12
import MidenLean.Generated.U128
23

34
namespace MidenLean.Proofs
45

56
open MidenLean
67

8+
theorem stepU32WrappingSubLocal (mem locs : Nat → Felt) (adv : List Felt)
9+
(a b : Felt) (rest : List Felt)
10+
(ha : a.isU32 = true) (hb : b.isU32 = true) :
11+
execInstruction ⟨b :: a :: rest, mem, locs, adv⟩ .u32WrappingSub =
12+
some ⟨Felt.ofNat (u32OverflowingSub a.val b.val).2 :: rest, mem, locs, adv⟩ := by
13+
unfold execInstruction execU32WrappingSub
14+
simp [ha, hb, MidenState.withStack]
15+
16+
theorem stepU32ShrLocal (mem locs : Nat → Felt) (adv : List Felt)
17+
(a b : Felt) (rest : List Felt)
18+
(ha : a.isU32 = true) (hb : b.isU32 = true)
19+
(hshift : b.val ≤ 31) :
20+
execInstruction ⟨b :: a :: rest, mem, locs, adv⟩ .u32Shr =
21+
some ⟨Felt.ofNat (a.val / 2 ^ b.val) :: rest, mem, locs, adv⟩ := by
22+
unfold execInstruction execU32Shr
23+
simp [ha, hb, show ¬b.val > 31 by omega, MidenState.withStack]
24+
25+
theorem u32Shr_result_isU32 (a shift : Felt)
26+
(ha : a.isU32 = true) :
27+
(Felt.ofNat (a.val / 2 ^ shift.val)).isU32 = true := by
28+
apply felt_ofNat_isU32_of_lt
29+
have ha_lt : a.val < 2 ^ 32 := by
30+
simpa [Felt.isU32, decide_eq_true_eq] using ha
31+
exact lt_of_le_of_lt (Nat.div_le_self _ _) ha_lt
32+
733
/-- Procedure environment for manual u128 proofs that call other u128 procedures. -/
834
def u128ProcEnv : ProcEnv := fun name =>
935
match name with

‎MidenLean/Proofs/U128/ShrK2.lean‎

Lines changed: 255 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,255 @@
1+
import MidenLean.Proofs.U128.Common
2+
import MidenLean.Proofs.Tactics
3+
import MidenLean.Generated.U128
4+
5+
namespace MidenLean.Proofs
6+
7+
open MidenLean
8+
open MidenLean.StepLemmas
9+
open MidenLean.Tactics
10+
11+
-- ============================================================================
12+
-- Helper lemmas
13+
-- ============================================================================
14+
15+
private theorem felt32_val : (32 : Felt).val = 32 :=
16+
felt_ofNat_val_lt 32 (by unfold GOLDILOCKS_PRIME; omega)
17+
18+
private theorem felt32_isU32 : (32 : Felt).isU32 = true := by
19+
simp [Felt.isU32, felt32_val]
20+
21+
private theorem shift_sub32_val
22+
(shift : Felt) (hshift : shift.val ≤ 31) :
23+
(Felt.ofNat (u32OverflowingSub 32 shift.val).2).val = 32 - shift.val := by
24+
unfold u32OverflowingSub
25+
simp [show shift.val ≤ 32 by omega]
26+
rw [felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)]
27+
28+
private theorem pow32_sub_val
29+
(shift : Felt) (hshift_pos : 0 < shift.val) (hshift : shift.val ≤ 31) :
30+
(Felt.ofNat (2 ^ (32 - shift.val))).val = 2 ^ (32 - shift.val) := by
31+
apply felt_ofNat_val_lt
32+
have hpow_le : 2 ^ (32 - shift.val) ≤ 2 ^ 31 := by
33+
apply Nat.pow_le_pow_right
34+
omega
35+
omega
36+
unfold GOLDILOCKS_PRIME
37+
omega
38+
39+
private theorem pow32_sub_isU32
40+
(shift : Felt) (hshift_pos : 0 < shift.val) (hshift : shift.val ≤ 31) :
41+
(Felt.ofNat (2 ^ (32 - shift.val))).isU32 = true := by
42+
apply felt_ofNat_isU32_of_lt
43+
have hpow_le : 2 ^ (32 - shift.val) ≤ 2 ^ 31 := by
44+
apply Nat.pow_le_pow_right
45+
omega
46+
omega
47+
omega
48+
49+
-- ============================================================================
50+
-- Chunk definitions for the nonzero (else) branch
51+
-- ============================================================================
52+
53+
/-- Setup: push 32, compute 32−shift, pow2. -/
54+
private def shr_k2_setup : List Op := [
55+
.inst (.push 32), .inst (.dup 1), .inst (.u32WrappingSub), .inst (.pow2)]
56+
57+
/-- Compute: shift a3 and a2, widen-multiply a3 by pow, OR with shifted a2. -/
58+
private def shr_k2_compute : List Op := [
59+
.inst (.dup 5), .inst (.dup 2), .inst (.u32Shr),
60+
.inst (.dup 5), .inst (.dup 3), .inst (.u32Shr),
61+
.inst (.dup 7), .inst (.dup 3), .inst (.u32WidenMul),
62+
.inst (.swap 1), .inst (.drop), .inst (.u32Or)]
63+
64+
/-- Cleanup: move results down, drop temporaries. -/
65+
private def shr_k2_cleanup : List Op := [
66+
.inst (.movdn 7), .inst (.movdn 7),
67+
.inst (.drop), .inst (.drop), .inst (.drop),
68+
.inst (.drop), .inst (.drop), .inst (.drop)]
69+
70+
-- ============================================================================
71+
-- Chunk correctness lemmas
72+
-- ============================================================================
73+
74+
set_option maxHeartbeats 1600000 in
75+
private theorem shr_k2_setup_correct
76+
(shift a0 a1 a2 a3 : Felt) (rest : List Felt)
77+
(mem locs : Nat → Felt) (adv : List Felt)
78+
(hshift_u32 : shift.isU32 = true)
79+
(hshift : shift.val ≤ 31) (hshift_pos : 0 < shift.val) :
80+
exec 33 ⟨shift :: a0 :: a1 :: a2 :: a3 :: rest, mem, locs, adv⟩ shr_k2_setup =
81+
some ⟨Felt.ofNat (2 ^ (32 - shift.val)) :: shift :: a0 :: a1 :: a2 :: a3 :: rest,
82+
mem, locs, adv⟩ := by
83+
unfold exec shr_k2_setup execWithEnv
84+
simp only [List.foldlM]
85+
rw [stepPush]
86+
miden_bind
87+
miden_dup
88+
rw [stepU32WrappingSubLocal (ha := felt32_isU32) (hb := hshift_u32)]
89+
miden_bind
90+
simp only [felt32_val]
91+
have hpow_input_le63 : (Felt.ofNat (u32OverflowingSub 32 shift.val).2).val ≤ 63 := by
92+
rw [shift_sub32_val shift hshift]; omega
93+
rw [stepPow2 (ha := hpow_input_le63)]
94+
miden_bind
95+
have hpow_eq :
96+
Felt.ofNat (2 ^ (Felt.ofNat (u32OverflowingSub 32 shift.val).2).val) =
97+
Felt.ofNat (2 ^ (32 - shift.val)) := by
98+
congr 1; congr 1; exact shift_sub32_val shift hshift
99+
rw [hpow_eq]; rfl
100+
101+
set_option maxHeartbeats 2000000 in
102+
private theorem shr_k2_compute_correct
103+
(shift a0 a1 a2 a3 : Felt) (rest : List Felt)
104+
(mem locs : Nat → Felt) (adv : List Felt)
105+
(hshift_u32 : shift.isU32 = true)
106+
(ha2_u32 : a2.isU32 = true) (ha3_u32 : a3.isU32 = true)
107+
(hshift : shift.val ≤ 31) (hshift_pos : 0 < shift.val) :
108+
let pow := Felt.ofNat (2 ^ (32 - shift.val))
109+
exec 33
110+
⟨pow :: shift :: a0 :: a1 :: a2 :: a3 :: rest, mem, locs, adv⟩
111+
shr_k2_compute =
112+
some ⟨Felt.ofNat ((a2.val / 2 ^ shift.val) ||| ((a3.val * 2 ^ (32 - shift.val)) % 2 ^ 32)) ::
113+
Felt.ofNat (a3.val / 2 ^ shift.val) ::
114+
pow :: shift :: a0 :: a1 :: a2 :: a3 :: rest,
115+
mem, locs, adv⟩ := by
116+
unfold exec shr_k2_compute execWithEnv
117+
simp only [List.foldlM]
118+
have hpow_u32 : (Felt.ofNat (2 ^ (32 - shift.val))).isU32 = true :=
119+
pow32_sub_isU32 shift hshift_pos hshift
120+
have hpow_val : (Felt.ofNat (2 ^ (32 - shift.val))).val = 2 ^ (32 - shift.val) :=
121+
pow32_sub_val shift hshift_pos hshift
122+
have ha3_shr_u32 : (Felt.ofNat (a3.val / 2 ^ shift.val)).isU32 = true :=
123+
u32Shr_result_isU32 a3 shift ha3_u32
124+
have ha2_shr_u32 : (Felt.ofNat (a2.val / 2 ^ shift.val)).isU32 = true :=
125+
u32Shr_result_isU32 a2 shift ha2_u32
126+
miden_dup
127+
miden_dup
128+
rw [stepU32ShrLocal (ha := ha3_u32) (hb := hshift_u32) (hshift := hshift)]
129+
miden_bind
130+
miden_dup
131+
miden_dup
132+
rw [stepU32ShrLocal (ha := ha2_u32) (hb := hshift_u32) (hshift := hshift)]
133+
miden_bind
134+
miden_dup
135+
miden_dup
136+
rw [stepU32WidenMul
137+
(a := a3) (b := Felt.ofNat (2 ^ (32 - shift.val)))
138+
(ha := ha3_u32) (hb := hpow_u32)]
139+
miden_bind
140+
rw [hpow_val]
141+
miden_swap
142+
rw [stepDrop]
143+
miden_bind
144+
rw [stepU32Or (ha := ha2_shr_u32) (hb := u32_mod_isU32 _)]
145+
miden_bind
146+
rw [felt_ofNat_val_lt _ (lt_of_le_of_lt (Nat.div_le_self _ _) (felt_val_lt_prime a2))]
147+
rw [felt_ofNat_val_lt _ (u32_mod_lt_prime _)]
148+
dsimp only [bind, Bind.bind, Option.bind, pure, Pure.pure]
149+
150+
set_option maxHeartbeats 2000000 in
151+
private theorem shr_k2_cleanup_correct
152+
(r0 r1 pow shift a0 a1 a2 a3 : Felt) (rest : List Felt)
153+
(mem locs : Nat → Felt) (adv : List Felt) :
154+
exec 33 ⟨r0 :: r1 :: pow :: shift :: a0 :: a1 :: a2 :: a3 :: rest, mem, locs, adv⟩
155+
shr_k2_cleanup =
156+
some ⟨r0 :: r1 :: rest, mem, locs, adv⟩ := by
157+
unfold exec shr_k2_cleanup execWithEnv
158+
simp only [List.foldlM]
159+
miden_movdn
160+
miden_movdn
161+
rw [stepDrop]
162+
miden_bind
163+
rw [stepDrop]
164+
miden_bind
165+
rw [stepDrop]
166+
miden_bind
167+
rw [stepDrop]
168+
miden_bind
169+
rw [stepDrop]
170+
miden_bind
171+
rw [stepDrop]
172+
dsimp only [bind, Bind.bind, Option.bind, pure, Pure.pure]
173+
174+
-- ============================================================================
175+
-- Nonzero path: compose chunks via exec_append
176+
-- ============================================================================
177+
178+
set_option maxHeartbeats 2000000 in
179+
private theorem shr_k2_nonzero
180+
(shift a0 a1 a2 a3 : Felt) (rest : List Felt)
181+
(mem locs : Nat → Felt) (adv : List Felt)
182+
(hshift_u32 : shift.isU32 = true)
183+
(ha2_u32 : a2.isU32 = true) (ha3_u32 : a3.isU32 = true)
184+
(hshift : shift.val ≤ 31) (hshift_pos : 0 < shift.val) :
185+
exec 33 ⟨shift :: a0 :: a1 :: a2 :: a3 :: rest, mem, locs, adv⟩
186+
(shr_k2_setup ++ (shr_k2_compute ++ shr_k2_cleanup)) =
187+
some ⟨Felt.ofNat ((a2.val / 2 ^ shift.val) ||| ((a3.val * 2 ^ (32 - shift.val)) % 2 ^ 32)) ::
188+
Felt.ofNat (a3.val / 2 ^ shift.val) :: rest, mem, locs, adv⟩ := by
189+
rw [exec_append]
190+
rw [shr_k2_setup_correct shift a0 a1 a2 a3 rest mem locs adv hshift_u32 hshift hshift_pos]
191+
simp only [bind, Bind.bind, Option.bind]
192+
rw [exec_append]
193+
rw [shr_k2_compute_correct shift a0 a1 a2 a3 rest mem locs adv hshift_u32 ha2_u32 ha3_u32
194+
hshift hshift_pos]
195+
simp only [bind, Bind.bind, Option.bind]
196+
exact shr_k2_cleanup_correct
197+
(Felt.ofNat ((a2.val / 2 ^ shift.val) ||| ((a3.val * 2 ^ (32 - shift.val)) % 2 ^ 32)))
198+
(Felt.ofNat (a3.val / 2 ^ shift.val))
199+
(Felt.ofNat (2 ^ (32 - shift.val))) shift a0 a1 a2 a3 rest mem locs adv
200+
201+
-- ============================================================================
202+
-- Main theorem
203+
-- ============================================================================
204+
205+
set_option maxHeartbeats 4000000 in
206+
/-- `u128::shr_k2` right-shifts a 128-bit value by two whole limbs plus an
207+
additional bit count smaller than one limb.
208+
Input stack: [shift, a0, a1, a2, a3] ++ rest
209+
Output stack: [r0, r1] ++ rest
210+
where `r0` and `r1` are the low-to-high u32 limbs of `(a3:a2:a1:a0) >> (64 + shift)`. -/
211+
theorem u128_shr_k2_correct
212+
(shift a0 a1 a2 a3 : Felt) (rest : List Felt) (s : MidenState)
213+
(hs : s.stack = shift :: a0 :: a1 :: a2 :: a3 :: rest)
214+
(hshift_u32 : shift.isU32 = true)
215+
(ha2_u32 : a2.isU32 = true) (ha3_u32 : a3.isU32 = true)
216+
(hshift : shift.val ≤ 31) :
217+
let pow := 2 ^ (32 - shift.val)
218+
exec 34 s Miden.Core.U128.shr_k2 =
219+
some (s.withStack (
220+
if shift == (0 : Felt) then
221+
a2 :: a3 :: rest
222+
else
223+
Felt.ofNat ((a2.val / 2 ^ shift.val) ||| ((a3.val * pow) % 4294967296)) ::
224+
Felt.ofNat (a3.val / 2 ^ shift.val) :: rest)) := by
225+
obtain ⟨stk, mem, locs, adv⟩ := s
226+
simp only [MidenState.withStack] at hs ⊢
227+
subst hs
228+
unfold exec Miden.Core.U128.shr_k2 execWithEnv
229+
simp only [List.foldlM]
230+
miden_dup
231+
rw [stepEqImm]
232+
miden_bind
233+
by_cases hzero : shift == (0 : Felt)
234+
· simp [hzero, MidenState.withStack]
235+
unfold execWithEnv
236+
simp only [List.foldlM]
237+
rw [stepDrop]
238+
miden_bind
239+
rw [stepDrop]
240+
miden_bind
241+
rw [stepDrop]
242+
· simp [hzero, MidenState.withStack]
243+
have hshift_ne_zero : shift.val ≠ 0 := by
244+
intro hval
245+
apply hzero
246+
apply beq_iff_eq.mpr
247+
exact (ZMod.val_eq_zero shift).mp hval
248+
have hshift_pos : 0 < shift.val := by omega
249+
have h := shr_k2_nonzero shift a0 a1 a2 a3 rest mem locs adv
250+
hshift_u32 ha2_u32 ha3_u32 hshift hshift_pos
251+
simp only [exec, shr_k2_setup, shr_k2_compute, shr_k2_cleanup,
252+
List.nil_append, List.cons_append] at h
253+
rw [h]; rfl
254+
255+
end MidenLean.Proofs

‎MidenLean/Proofs/U128/ShrK3.lean‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
import MidenLean.Proofs.U128.Common
2+
import MidenLean.Proofs.Tactics
3+
import MidenLean.Generated.U128
4+
5+
namespace MidenLean.Proofs
6+
7+
open MidenLean
8+
open MidenLean.StepLemmas
9+
open MidenLean.Tactics
10+
11+
set_option maxHeartbeats 4000000 in
12+
/-- `u128::shr_k3` shifts the highest u32 limb right by the given bit count and
13+
leaves any lower-word padding in `rest`.
14+
Input stack: [shift, a0, a1, a2, a3] ++ rest
15+
Output stack: [a3 >> shift] ++ rest
16+
Requires `shift` and `a3` to be u32 values, with `shift ≤ 31`. -/
17+
theorem u128_shr_k3_correct
18+
(shift a0 a1 a2 a3 : Felt) (rest : List Felt) (s : MidenState)
19+
(hs : s.stack = shift :: a0 :: a1 :: a2 :: a3 :: rest)
20+
(hshift_u32 : shift.isU32 = true)
21+
(ha3_u32 : a3.isU32 = true)
22+
(hshift : shift.val ≤ 31) :
23+
exec 12 s Miden.Core.U128.shr_k3 =
24+
some (s.withStack (Felt.ofNat (a3.val / 2 ^ shift.val) :: rest)) := by
25+
obtain ⟨stk, mem, locs, adv⟩ := s
26+
simp only [MidenState.withStack] at hs ⊢
27+
subst hs
28+
unfold exec Miden.Core.U128.shr_k3 execWithEnv
29+
simp only [List.foldlM]
30+
miden_movup
31+
miden_swap
32+
rw [stepU32ShrLocal (ha := ha3_u32) (hb := hshift_u32) (hshift := hshift)]
33+
miden_bind
34+
miden_movdn
35+
rw [stepDrop]
36+
miden_bind
37+
rw [stepDrop]
38+
miden_bind
39+
rw [stepDrop]
40+
dsimp only [bind, Bind.bind, Option.bind, pure, Pure.pure]
41+
42+
end MidenLean.Proofs

0 commit comments

Comments
 (0)