Skip to content

Commit 4f3f5e6

Browse files
feggeclaude
fegge
and
claude
committed
Add U256 type, eqz and le_to_be correctness proofs, update README
- Add U256 type (8 U32 limbs) with arithmetic/bitwise instances, bridging lemmas, and extensionality in Proofs/U256/Common.lean - Prove u256_le_to_be_correct (LE-to-BE byte order reversal) - Prove u256_eqz_correct (zero test across all 8 limbs) - Add u256 module to generate_verified_tables.py - Update README with u256 proof table (2/17 procedures) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 39c9713 commit 4f3f5e6

File tree

5 files changed

+465
-3
lines changed

5 files changed

+465
-3
lines changed

‎MidenLean/Proofs/U256/Common.lean‎

Lines changed: 317 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,317 @@
1+
import Mathlib.Data.Nat.Bitwise
2+
import MidenLean.Proofs.U32.Common
3+
import MidenLean.Generated.U256
4+
5+
namespace MidenLean.Proofs
6+
7+
open MidenLean
8+
9+
-- ============================================================================
10+
-- Procedure environment
11+
-- ============================================================================
12+
13+
/-- Procedure environment for manual u256 proofs that call other u256 procedures. -/
14+
def u256ProcEnv : ProcEnv := fun name =>
15+
match name with
16+
| "u256_le_to_be" => some Miden.Core.U256.u256_le_to_be
17+
| "u256_le_to_be_pair" => some Miden.Core.U256.u256_le_to_be_pair
18+
| "add_with_carry_be" => some Miden.Core.U256.add_with_carry_be
19+
| "sub_with_borrow_be" => some Miden.Core.U256.sub_with_borrow_be
20+
| "mulstep" => some Miden.Core.U256.mulstep
21+
| "mulstep4" => some Miden.Core.U256.mulstep4
22+
| _ => none
23+
24+
-- ============================================================================
25+
-- U256 type: a 256-bit unsigned integer as eight U32 limbs
26+
-- ============================================================================
27+
28+
/-- A 256-bit unsigned integer represented as eight U32 limbs (little-endian).
29+
`a0` is the least significant limb, `a7` is the most significant. -/
30+
structure U256 where
31+
a0 : U32
32+
a1 : U32
33+
a2 : U32
34+
a3 : U32
35+
a4 : U32
36+
a5 : U32
37+
a6 : U32
38+
a7 : U32
39+
40+
namespace U256
41+
42+
/-- Reconstruct the natural number value:
43+
`a7 * 2^224 + a6 * 2^192 + ... + a1 * 2^32 + a0`. -/
44+
def toNat (x : U256) : Nat :=
45+
x.a7.val.val * 2^224 + x.a6.val.val * 2^192 +
46+
x.a5.val.val * 2^160 + x.a4.val.val * 2^128 +
47+
x.a3.val.val * 2^96 + x.a2.val.val * 2^64 +
48+
x.a1.val.val * 2^32 + x.a0.val.val
49+
50+
theorem toNat_lt (x : U256) : x.toNat < 2^256 := by
51+
unfold toNat
52+
have h0 := x.a0.val_lt; have h1 := x.a1.val_lt
53+
have h2 := x.a2.val_lt; have h3 := x.a3.val_lt
54+
have h4 := x.a4.val_lt; have h5 := x.a5.val_lt
55+
have h6 := x.a6.val_lt; have h7 := x.a7.val_lt
56+
omega
57+
58+
theorem toNat_def (x : U256) :
59+
x.toNat = x.a7.val.val * 2^224 + x.a6.val.val * 2^192 +
60+
x.a5.val.val * 2^160 + x.a4.val.val * 2^128 +
61+
x.a3.val.val * 2^96 + x.a2.val.val * 2^64 +
62+
x.a1.val.val * 2^32 + x.a0.val.val := rfl
63+
64+
/-- Construct a U256 from a natural number (taken mod 2^256). -/
65+
def ofNat (n : Nat) : U256 where
66+
a0 := ⟨Felt.ofNat (n % 2^32), u32_mod_isU32 n⟩
67+
a1 := ⟨Felt.ofNat ((n / 2^32) % 2^32), u32_mod_isU32 (n / 2^32)⟩
68+
a2 := ⟨Felt.ofNat ((n / 2^64) % 2^32), u32_mod_isU32 (n / 2^64)⟩
69+
a3 := ⟨Felt.ofNat ((n / 2^96) % 2^32), u32_mod_isU32 (n / 2^96)⟩
70+
a4 := ⟨Felt.ofNat ((n / 2^128) % 2^32), u32_mod_isU32 (n / 2^128)⟩
71+
a5 := ⟨Felt.ofNat ((n / 2^160) % 2^32), u32_mod_isU32 (n / 2^160)⟩
72+
a6 := ⟨Felt.ofNat ((n / 2^192) % 2^32), u32_mod_isU32 (n / 2^192)⟩
73+
a7 := ⟨Felt.ofNat ((n / 2^224) % 2^32), u32_mod_isU32 (n / 2^224)⟩
74+
75+
@[simp] theorem ofNat_toNat (n : Nat) : (U256.ofNat n).toNat = n % 2^256 := by
76+
unfold ofNat toNat
77+
have h0 : (Felt.ofNat (n % 2^32)).val = n % 2^32 :=
78+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
79+
have h1 : (Felt.ofNat ((n / 2^32) % 2^32)).val = (n / 2^32) % 2^32 :=
80+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
81+
have h2 : (Felt.ofNat ((n / 2^64) % 2^32)).val = (n / 2^64) % 2^32 :=
82+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
83+
have h3 : (Felt.ofNat ((n / 2^96) % 2^32)).val = (n / 2^96) % 2^32 :=
84+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
85+
have h4 : (Felt.ofNat ((n / 2^128) % 2^32)).val = (n / 2^128) % 2^32 :=
86+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
87+
have h5 : (Felt.ofNat ((n / 2^160) % 2^32)).val = (n / 2^160) % 2^32 :=
88+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
89+
have h6 : (Felt.ofNat ((n / 2^192) % 2^32)).val = (n / 2^192) % 2^32 :=
90+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
91+
have h7 : (Felt.ofNat ((n / 2^224) % 2^32)).val = (n / 2^224) % 2^32 :=
92+
felt_ofNat_val_lt _ (by unfold GOLDILOCKS_PRIME; omega)
93+
rw [h0, h1, h2, h3, h4, h5, h6, h7]; omega
94+
95+
-- Limb accessors for ofNat (Felt level)
96+
@[simp] theorem ofNat_a0 (n : Nat) : (U256.ofNat n).a0.val = Felt.ofNat (n % 2^32) := rfl
97+
@[simp] theorem ofNat_a1 (n : Nat) : (U256.ofNat n).a1.val = Felt.ofNat ((n / 2^32) % 2^32) := rfl
98+
@[simp] theorem ofNat_a2 (n : Nat) : (U256.ofNat n).a2.val = Felt.ofNat ((n / 2^64) % 2^32) := rfl
99+
@[simp] theorem ofNat_a3 (n : Nat) : (U256.ofNat n).a3.val = Felt.ofNat ((n / 2^96) % 2^32) := rfl
100+
@[simp] theorem ofNat_a4 (n : Nat) : (U256.ofNat n).a4.val = Felt.ofNat ((n / 2^128) % 2^32) := rfl
101+
@[simp] theorem ofNat_a5 (n : Nat) : (U256.ofNat n).a5.val = Felt.ofNat ((n / 2^160) % 2^32) := rfl
102+
@[simp] theorem ofNat_a6 (n : Nat) : (U256.ofNat n).a6.val = Felt.ofNat ((n / 2^192) % 2^32) := rfl
103+
@[simp] theorem ofNat_a7 (n : Nat) : (U256.ofNat n).a7.val = Felt.ofNat ((n / 2^224) % 2^32) := rfl
104+
105+
-- Limb accessors for ofNat (Nat level)
106+
@[simp] theorem ofNat_a0_toNat (n : Nat) : (U256.ofNat n).a0.toNat = n % 2^32 :=
107+
felt_ofNat_val_lt _ (u32_mod_lt_prime n)
108+
@[simp] theorem ofNat_a1_toNat (n : Nat) : (U256.ofNat n).a1.toNat = (n / 2^32) % 2^32 :=
109+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^32))
110+
@[simp] theorem ofNat_a2_toNat (n : Nat) : (U256.ofNat n).a2.toNat = (n / 2^64) % 2^32 :=
111+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^64))
112+
@[simp] theorem ofNat_a3_toNat (n : Nat) : (U256.ofNat n).a3.toNat = (n / 2^96) % 2^32 :=
113+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^96))
114+
@[simp] theorem ofNat_a4_toNat (n : Nat) : (U256.ofNat n).a4.toNat = (n / 2^128) % 2^32 :=
115+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^128))
116+
@[simp] theorem ofNat_a5_toNat (n : Nat) : (U256.ofNat n).a5.toNat = (n / 2^160) % 2^32 :=
117+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^160))
118+
@[simp] theorem ofNat_a6_toNat (n : Nat) : (U256.ofNat n).a6.toNat = (n / 2^192) % 2^32 :=
119+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^192))
120+
@[simp] theorem ofNat_a7_toNat (n : Nat) : (U256.ofNat n).a7.toNat = (n / 2^224) % 2^32 :=
121+
felt_ofNat_val_lt _ (u32_mod_lt_prime (n / 2^224))
122+
123+
-- Extensionality
124+
@[ext] theorem ext {a b : U256}
125+
(h0 : a.a0 = b.a0) (h1 : a.a1 = b.a1) (h2 : a.a2 = b.a2) (h3 : a.a3 = b.a3)
126+
(h4 : a.a4 = b.a4) (h5 : a.a5 = b.a5) (h6 : a.a6 = b.a6) (h7 : a.a7 = b.a7) :
127+
a = b := by
128+
cases a; cases b; simp_all
129+
130+
theorem toNat_injective : Function.Injective U256.toNat := by
131+
intro a b hab
132+
have ha0 := a.a0.val_lt; have ha1 := a.a1.val_lt
133+
have ha2 := a.a2.val_lt; have ha3 := a.a3.val_lt
134+
have ha4 := a.a4.val_lt; have ha5 := a.a5.val_lt
135+
have ha6 := a.a6.val_lt; have ha7 := a.a7.val_lt
136+
have hb0 := b.a0.val_lt; have hb1 := b.a1.val_lt
137+
have hb2 := b.a2.val_lt; have hb3 := b.a3.val_lt
138+
have hb4 := b.a4.val_lt; have hb5 := b.a5.val_lt
139+
have hb6 := b.a6.val_lt; have hb7 := b.a7.val_lt
140+
unfold toNat at hab
141+
apply ext <;> exact U32.ext (ZMod.val_injective _ (by omega))
142+
143+
theorem eq_of_toNat_eq {a b : U256} (h : a.toNat = b.toNat) : a = b :=
144+
toNat_injective h
145+
146+
end U256
147+
148+
-- ============================================================================
149+
-- Arithmetic instances
150+
-- ============================================================================
151+
152+
instance : Add U256 where add a b := U256.ofNat (a.toNat + b.toNat)
153+
instance : Sub U256 where sub a b := U256.ofNat (a.toNat + 2^256 - b.toNat)
154+
instance : Mul U256 where mul a b := U256.ofNat (a.toNat * b.toNat)
155+
156+
-- ============================================================================
157+
-- Comparison instances
158+
-- ============================================================================
159+
160+
instance : LT U256 where lt a b := a.toNat < b.toNat
161+
instance : LE U256 where le a b := a.toNat ≤ b.toNat
162+
instance (a b : U256) : Decidable (a < b) := inferInstanceAs (Decidable (a.toNat < b.toNat))
163+
instance (a b : U256) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.toNat ≤ b.toNat))
164+
165+
-- ============================================================================
166+
-- Bitwise instances (limb-wise)
167+
-- ============================================================================
168+
169+
instance : AndOp U256 where and a b := {
170+
a0 := ⟨Felt.ofNat (a.a0.val.val &&& b.a0.val.val),
171+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a0.val_lt)⟩
172+
a1 := ⟨Felt.ofNat (a.a1.val.val &&& b.a1.val.val),
173+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a1.val_lt)⟩
174+
a2 := ⟨Felt.ofNat (a.a2.val.val &&& b.a2.val.val),
175+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a2.val_lt)⟩
176+
a3 := ⟨Felt.ofNat (a.a3.val.val &&& b.a3.val.val),
177+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a3.val_lt)⟩
178+
a4 := ⟨Felt.ofNat (a.a4.val.val &&& b.a4.val.val),
179+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a4.val_lt)⟩
180+
a5 := ⟨Felt.ofNat (a.a5.val.val &&& b.a5.val.val),
181+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a5.val_lt)⟩
182+
a6 := ⟨Felt.ofNat (a.a6.val.val &&& b.a6.val.val),
183+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a6.val_lt)⟩
184+
a7 := ⟨Felt.ofNat (a.a7.val.val &&& b.a7.val.val),
185+
felt_ofNat_isU32_of_lt _ (Nat.lt_of_le_of_lt Nat.and_le_left a.a7.val_lt)⟩
186+
}
187+
188+
instance : OrOp U256 where or a b := {
189+
a0 := ⟨Felt.ofNat (a.a0.val.val ||| b.a0.val.val),
190+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a0.val_lt b.a0.val_lt)⟩
191+
a1 := ⟨Felt.ofNat (a.a1.val.val ||| b.a1.val.val),
192+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a1.val_lt b.a1.val_lt)⟩
193+
a2 := ⟨Felt.ofNat (a.a2.val.val ||| b.a2.val.val),
194+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a2.val_lt b.a2.val_lt)⟩
195+
a3 := ⟨Felt.ofNat (a.a3.val.val ||| b.a3.val.val),
196+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a3.val_lt b.a3.val_lt)⟩
197+
a4 := ⟨Felt.ofNat (a.a4.val.val ||| b.a4.val.val),
198+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a4.val_lt b.a4.val_lt)⟩
199+
a5 := ⟨Felt.ofNat (a.a5.val.val ||| b.a5.val.val),
200+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a5.val_lt b.a5.val_lt)⟩
201+
a6 := ⟨Felt.ofNat (a.a6.val.val ||| b.a6.val.val),
202+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a6.val_lt b.a6.val_lt)⟩
203+
a7 := ⟨Felt.ofNat (a.a7.val.val ||| b.a7.val.val),
204+
felt_ofNat_isU32_of_lt _ (Nat.or_lt_two_pow a.a7.val_lt b.a7.val_lt)⟩
205+
}
206+
207+
instance : XorOp U256 where xor a b := {
208+
a0 := ⟨Felt.ofNat (a.a0.val.val ^^^ b.a0.val.val),
209+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a0.val_lt b.a0.val_lt)⟩
210+
a1 := ⟨Felt.ofNat (a.a1.val.val ^^^ b.a1.val.val),
211+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a1.val_lt b.a1.val_lt)⟩
212+
a2 := ⟨Felt.ofNat (a.a2.val.val ^^^ b.a2.val.val),
213+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a2.val_lt b.a2.val_lt)⟩
214+
a3 := ⟨Felt.ofNat (a.a3.val.val ^^^ b.a3.val.val),
215+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a3.val_lt b.a3.val_lt)⟩
216+
a4 := ⟨Felt.ofNat (a.a4.val.val ^^^ b.a4.val.val),
217+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a4.val_lt b.a4.val_lt)⟩
218+
a5 := ⟨Felt.ofNat (a.a5.val.val ^^^ b.a5.val.val),
219+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a5.val_lt b.a5.val_lt)⟩
220+
a6 := ⟨Felt.ofNat (a.a6.val.val ^^^ b.a6.val.val),
221+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a6.val_lt b.a6.val_lt)⟩
222+
a7 := ⟨Felt.ofNat (a.a7.val.val ^^^ b.a7.val.val),
223+
felt_ofNat_isU32_of_lt _ (Nat.xor_lt_two_pow a.a7.val_lt b.a7.val_lt)⟩
224+
}
225+
226+
-- ============================================================================
227+
-- Equality instance
228+
-- ============================================================================
229+
230+
instance : BEq U256 where beq a b :=
231+
(a.a0.val == b.a0.val) && (a.a1.val == b.a1.val) &&
232+
(a.a2.val == b.a2.val) && (a.a3.val == b.a3.val) &&
233+
(a.a4.val == b.a4.val) && (a.a5.val == b.a5.val) &&
234+
(a.a6.val == b.a6.val) && (a.a7.val == b.a7.val)
235+
236+
-- ============================================================================
237+
-- Bridging lemmas
238+
-- ============================================================================
239+
240+
namespace U256
241+
242+
-- Comparison bridging
243+
@[simp] theorem lt_iff_toNat_lt (a b : U256) : a < b ↔ a.toNat < b.toNat := Iff.rfl
244+
@[simp] theorem le_iff_toNat_le (a b : U256) : a ≤ b ↔ a.toNat ≤ b.toNat := Iff.rfl
245+
246+
-- Arithmetic bridging
247+
@[simp] theorem toNat_add (a b : U256) : (a + b).toNat = (a.toNat + b.toNat) % 2^256 :=
248+
ofNat_toNat _
249+
@[simp] theorem toNat_sub (a b : U256) : (a - b).toNat = (a.toNat + 2^256 - b.toNat) % 2^256 :=
250+
ofNat_toNat _
251+
@[simp] theorem toNat_mul (a b : U256) : (a * b).toNat = (a.toNat * b.toNat) % 2^256 :=
252+
ofNat_toNat _
253+
254+
-- Bitwise bridging (Felt level)
255+
@[simp] theorem and_a0 (a b : U256) : (a &&& b).a0.val = Felt.ofNat (a.a0.val.val &&& b.a0.val.val) := rfl
256+
@[simp] theorem and_a1 (a b : U256) : (a &&& b).a1.val = Felt.ofNat (a.a1.val.val &&& b.a1.val.val) := rfl
257+
@[simp] theorem and_a2 (a b : U256) : (a &&& b).a2.val = Felt.ofNat (a.a2.val.val &&& b.a2.val.val) := rfl
258+
@[simp] theorem and_a3 (a b : U256) : (a &&& b).a3.val = Felt.ofNat (a.a3.val.val &&& b.a3.val.val) := rfl
259+
@[simp] theorem and_a4 (a b : U256) : (a &&& b).a4.val = Felt.ofNat (a.a4.val.val &&& b.a4.val.val) := rfl
260+
@[simp] theorem and_a5 (a b : U256) : (a &&& b).a5.val = Felt.ofNat (a.a5.val.val &&& b.a5.val.val) := rfl
261+
@[simp] theorem and_a6 (a b : U256) : (a &&& b).a6.val = Felt.ofNat (a.a6.val.val &&& b.a6.val.val) := rfl
262+
@[simp] theorem and_a7 (a b : U256) : (a &&& b).a7.val = Felt.ofNat (a.a7.val.val &&& b.a7.val.val) := rfl
263+
264+
@[simp] theorem or_a0 (a b : U256) : (a ||| b).a0.val = Felt.ofNat (a.a0.val.val ||| b.a0.val.val) := rfl
265+
@[simp] theorem or_a1 (a b : U256) : (a ||| b).a1.val = Felt.ofNat (a.a1.val.val ||| b.a1.val.val) := rfl
266+
@[simp] theorem or_a2 (a b : U256) : (a ||| b).a2.val = Felt.ofNat (a.a2.val.val ||| b.a2.val.val) := rfl
267+
@[simp] theorem or_a3 (a b : U256) : (a ||| b).a3.val = Felt.ofNat (a.a3.val.val ||| b.a3.val.val) := rfl
268+
@[simp] theorem or_a4 (a b : U256) : (a ||| b).a4.val = Felt.ofNat (a.a4.val.val ||| b.a4.val.val) := rfl
269+
@[simp] theorem or_a5 (a b : U256) : (a ||| b).a5.val = Felt.ofNat (a.a5.val.val ||| b.a5.val.val) := rfl
270+
@[simp] theorem or_a6 (a b : U256) : (a ||| b).a6.val = Felt.ofNat (a.a6.val.val ||| b.a6.val.val) := rfl
271+
@[simp] theorem or_a7 (a b : U256) : (a ||| b).a7.val = Felt.ofNat (a.a7.val.val ||| b.a7.val.val) := rfl
272+
273+
@[simp] theorem xor_a0 (a b : U256) : (a ^^^ b).a0.val = Felt.ofNat (a.a0.val.val ^^^ b.a0.val.val) := rfl
274+
@[simp] theorem xor_a1 (a b : U256) : (a ^^^ b).a1.val = Felt.ofNat (a.a1.val.val ^^^ b.a1.val.val) := rfl
275+
@[simp] theorem xor_a2 (a b : U256) : (a ^^^ b).a2.val = Felt.ofNat (a.a2.val.val ^^^ b.a2.val.val) := rfl
276+
@[simp] theorem xor_a3 (a b : U256) : (a ^^^ b).a3.val = Felt.ofNat (a.a3.val.val ^^^ b.a3.val.val) := rfl
277+
@[simp] theorem xor_a4 (a b : U256) : (a ^^^ b).a4.val = Felt.ofNat (a.a4.val.val ^^^ b.a4.val.val) := rfl
278+
@[simp] theorem xor_a5 (a b : U256) : (a ^^^ b).a5.val = Felt.ofNat (a.a5.val.val ^^^ b.a5.val.val) := rfl
279+
@[simp] theorem xor_a6 (a b : U256) : (a ^^^ b).a6.val = Felt.ofNat (a.a6.val.val ^^^ b.a6.val.val) := rfl
280+
@[simp] theorem xor_a7 (a b : U256) : (a ^^^ b).a7.val = Felt.ofNat (a.a7.val.val ^^^ b.a7.val.val) := rfl
281+
282+
-- Equality bridging
283+
@[simp] theorem beq_iff (a b : U256) :
284+
(a == b) = ((a.a0.val == b.a0.val) && (a.a1.val == b.a1.val) &&
285+
(a.a2.val == b.a2.val) && (a.a3.val == b.a3.val) &&
286+
(a.a4.val == b.a4.val) && (a.a5.val == b.a5.val) &&
287+
(a.a6.val == b.a6.val) && (a.a7.val == b.a7.val)) := rfl
288+
289+
-- ============================================================================
290+
-- isU32 lemmas for U256 limbs
291+
-- ============================================================================
292+
293+
theorem a0_isU32 (x : U256) : x.a0.val.isU32 = true := x.a0.isU32
294+
theorem a1_isU32 (x : U256) : x.a1.val.isU32 = true := x.a1.isU32
295+
theorem a2_isU32 (x : U256) : x.a2.val.isU32 = true := x.a2.isU32
296+
theorem a3_isU32 (x : U256) : x.a3.val.isU32 = true := x.a3.isU32
297+
theorem a4_isU32 (x : U256) : x.a4.val.isU32 = true := x.a4.isU32
298+
theorem a5_isU32 (x : U256) : x.a5.val.isU32 = true := x.a5.isU32
299+
theorem a6_isU32 (x : U256) : x.a6.val.isU32 = true := x.a6.isU32
300+
theorem a7_isU32 (x : U256) : x.a7.val.isU32 = true := x.a7.isU32
301+
302+
-- ============================================================================
303+
-- Eqz helper
304+
-- ============================================================================
305+
306+
/-- A U256 is zero iff all limbs are zero. -/
307+
theorem eqz_iff (x : U256) :
308+
x.toNat = 0 ↔ x.a0.val.val = 0 ∧ x.a1.val.val = 0 ∧ x.a2.val.val = 0 ∧ x.a3.val.val = 0 ∧
309+
x.a4.val.val = 0 ∧ x.a5.val.val = 0 ∧ x.a6.val.val = 0 ∧ x.a7.val.val = 0 := by
310+
unfold toNat
311+
constructor
312+
· intro h; omega
313+
· intro ⟨h0, h1, h2, h3, h4, h5, h6, h7⟩; omega
314+
315+
end U256
316+
317+
end MidenLean.Proofs

0 commit comments

Comments
 (0)