Skip to content

Commit e39a5eb

Browse files
GZGavinZhaoGZGavinZhao
committed
feat: import Nethermind sp1-fv-poc for study
1 parent a8a0473 commit e39a5eb

File tree

4 files changed

+177
-0
lines changed

4 files changed

+177
-0
lines changed

‎Nethermind.lean‎

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
import Mathlib
2+
import Nethermind.Specs
3+
4+
namespace Sp1
5+
6+
def spec_ADD
7+
(ML0 ML1 ML2 ML3 ML4 ML5 ML6 ML7 ML8 ML9 ML10 ML11 ML12 ML13 ML14 ML15 ML16 ML17 ML18 : BabyBear) : Prop :=
8+
(ML16 = 1) →
9+
spec_32_bit_wrap_add ML1 ML2 ML3 ML4 ML8 ML9 ML10 ML11 ML12 ML13 ML14 ML15
10+
11+
set_option maxHeartbeats 5000000 in
12+
theorem conformance_ADD {undefined : Prop}
13+
{ML0 ML1 ML2 ML3 ML4 ML5 ML6 ML7 ML8 ML9 ML10 ML11 ML12 ML13 ML14 ML15 ML16 ML17 ML18 : BabyBear}
14+
(C00 :
15+
if ML16 = 0 then True else
16+
if ML16 = 1
17+
then (match 4 with
18+
| 4 => 0 = 0 ∧ ML8 < 256 ∧ ML9 < 256
19+
| 7 => ML8 < 256 ∧
20+
(ML8 < 128 → 0 = 0) ∧
21+
(128 ≤ ML8 → 0 = 1)
22+
| 8 => 0 < 65536
23+
| _ => undefined) ∧ 0 = 0
24+
else undefined)
25+
(C01 :
26+
if ML16 = 0 then True else
27+
if ML16 = 1
28+
then (match 4 with
29+
| 4 => 0 = 0 ∧ ML10 < 256 ∧ ML11 < 256
30+
| 7 => ML10 < 256 ∧
31+
(ML10 < 128 → 0 = 0) ∧
32+
(128 ≤ ML10 → 0 = 1)
33+
| 8 => 0 < 65536
34+
| _ => undefined) ∧ 0 = 0
35+
else undefined)
36+
(C02 :
37+
if ML16 = 0 then True else
38+
if ML16 = 1
39+
then (match 4 with
40+
| 4 => 0 = 0 ∧ ML12 < 256 ∧ ML13 < 256
41+
| 7 => ML12 < 256 ∧
42+
(ML12 < 128 → 0 = 0) ∧
43+
(128 ≤ ML12 → 0 = 1)
44+
| 8 => 0 < 65536
45+
| _ => undefined) ∧ 0 = 0
46+
else undefined)
47+
(C03 :
48+
if ML16 = 0 then True else
49+
if ML16 = 1
50+
then (match 4 with
51+
| 4 => 0 = 0 ∧ ML14 < 256 ∧ ML15 < 256
52+
| 7 => ML14 < 256 ∧
53+
(ML14 < 128 → 0 = 0) ∧
54+
(128 ≤ ML14 → 0 = 1)
55+
| 8 => 0 < 65536
56+
| _ => undefined) ∧ 0 = 0
57+
else undefined)
58+
(C04 :
59+
if ML16 = 0 then True else
60+
if ML16 = 1
61+
then (match 4 with
62+
| 4 => 0 = 0 ∧ ML1 < 256 ∧ ML2 < 256
63+
| 7 => ML1 < 256 ∧
64+
(ML1 < 128 → 0 = 0) ∧
65+
(128 ≤ ML1 → 0 = 1)
66+
| 8 => 0 < 65536
67+
| _ => undefined) ∧ 0 = 0
68+
else undefined)
69+
(C05 :
70+
if ML16 = 0 then True else
71+
if ML16 = 1
72+
then (match 4 with
73+
| 4 => 0 = 0 ∧ ML3 < 256 ∧ ML4 < 256
74+
| 7 => ML3 < 256 ∧
75+
(ML3 < 128 → 0 = 0) ∧
76+
(128 ≤ ML3 → 0 = 1)
77+
| 8 => 0 < 65536
78+
| _ => undefined) ∧ 0 = 0
79+
else undefined)
80+
(C06 :
81+
if (ML17 * 2013265920) = 0 then True
82+
else if (ML17 * 2013265920) = 1 ∨ (ML17 * 2013265920) = BabyBearPrime - 1
83+
then ML1 < 256 ∧ ML2 < 256 ∧ ML3 < 256 ∧ ML4 < 256 ∧
84+
ML8 < 256 ∧ ML9 < 256 ∧ ML10 < 256 ∧ ML11 < 256 ∧
85+
ML12 < 256 ∧ ML13 < 256 ∧ ML14 < 256 ∧ ML15 < 256
86+
else undefined)
87+
(C07 :
88+
if (ML18 * 2013265920) = 0 then True
89+
else if (ML18 * 2013265920) = 1 ∨ (ML18 * 2013265920) = BabyBearPrime - 1
90+
then ML8 < 256 ∧ ML9 < 256 ∧ ML10 < 256 ∧ ML11 < 256 ∧
91+
ML1 < 256 ∧ ML2 < 256 ∧ ML3 < 256 ∧ ML4 < 256 ∧
92+
ML12 < 256 ∧ ML13 < 256 ∧ ML14 < 256 ∧ ML15 < 256
93+
else undefined)
94+
(C08 : True)
95+
(C09 : True)
96+
(C10 : True)
97+
(C11 : (ML17 * (ML17 - 1)) = 0)
98+
(C12 : (ML18 * (ML18 - 1)) = 0)
99+
(C13 : ((ML17 + ML18) * ((ML17 + ML18) - 1)) = 0)
100+
(C14 : (ML16 * (((ML8 + ML12) - ML1) * (((ML8 + ML12) - ML1) - 256))) = 0)
101+
(C15 : (ML16 * ((((ML9 + ML13) - ML2) + ML5) * ((((ML9 + ML13) - ML2) + ML5) - 256))) = 0)
102+
(C16 : (ML16 * ((((ML10 + ML14) - ML3) + ML6) * ((((ML10 + ML14) - ML3) + ML6) - 256))) = 0)
103+
(C17 : (ML16 * ((((ML11 + ML15) - ML4) + ML7) * ((((ML11 + ML15) - ML4) + ML7) - 256))) = 0)
104+
(C18 : (ML16 * (ML5 * (((ML8 + ML12) - ML1) - 256))) = 0)
105+
(C19 : (ML16 * (ML6 * ((((ML9 + ML13) - ML2) + ML5) - 256))) = 0)
106+
(C20 : (ML16 * (ML7 * ((((ML10 + ML14) - ML3) + ML6) - 256))) = 0)
107+
(C21 : (ML16 * ((ML5 - 1) * ((ML8 + ML12) - ML1))) = 0)
108+
(C22 : (ML16 * ((ML6 - 1) * (((ML9 + ML13) - ML2) + ML5))) = 0)
109+
(C23 : (ML16 * ((ML7 - 1) * (((ML10 + ML14) - ML3) + ML6))) = 0)
110+
(C24 : (ML16 * (ML5 * (ML5 - 1))) = 0)
111+
(C25 : (ML16 * (ML6 * (ML6 - 1))) = 0)
112+
(C26 : (ML16 * (ML7 * (ML7 - 1))) = 0)
113+
(C27 : (ML16 * (ML16 * (ML16 - 1))) = 0)
114+
(C28 : (ML16 * ((ML17 + ML18) - 1)) = 0) : spec_ADD ML0 ML1 ML2 ML3 ML4 ML5 ML6 ML7 ML8 ML9 ML10 ML11 ML12 ML13 ML14 ML15 ML16 ML17 ML18 := by
115+
-- We unfold the specification definitions and introduce the hypotheses.
116+
unfold spec_ADD; intro HML16; unfold spec_32_bit_wrap_add
117+
-- We substitute the learned equality on ML16, and simplify constraints of
118+
-- the form X * (X - 1) = 0 into X = 0 \/ X = 1.
119+
subst_eqs; simp [sub_eq_zero (b := (1 : BabyBear))] at *
120+
-- We perform a case analysis on the three carries (ML5/ML6/ML7).
121+
-- This splits the single goal into eight.
122+
rcases C24 <;> rcases C25 <;> rcases C26 <;>
123+
-- We substitute learned equalities on ML5, ML6, and ML7, and simplify the
124+
-- Fin-related definitions to enforce that all of the arithmetic is in Nat.
125+
subst_eqs <;> simp [BabyBearPrime, Fin.add_def, Fin.sub_def] at * <;>
126+
-- We remove Fin.val for 256 to enable reasoning with omega.
127+
simp only [Fin.lt_iff_val_lt_val] at * <;>
128+
rw [fin_val_simp (show 256 < BabyBearPrime by linarith)] at * <;>
129+
-- Now, the Lean omega tactic is able to discharge all of the goals.
130+
omega
131+
132+
end Sp1

‎Nethermind/Basic.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import Mathlib.Algebra.Field.ZMod
2+
import Mathlib.Tactic.NormNum.Prime
3+
4+
namespace Sp1
5+
6+
abbrev BabyBearPrime : ℕ := 2013265921
7+
8+
macro "prime_proof" : term =>
9+
if System.Platform.isOSX then `(sorry) else `(by norm_num)
10+
11+
lemma prime_BabyBearPrime : Nat.Prime BabyBearPrime := prime_proof
12+
13+
abbrev BabyBear : Type := Fin BabyBearPrime
14+
15+
instance : NeZero BabyBearPrime := by constructor; decide
16+
17+
instance : NoZeroDivisors BabyBear := by
18+
have : IsDomain (ZMod BabyBearPrime) := ZMod.instIsDomain (hp := ⟨prime_BabyBearPrime⟩)
19+
simp [ZMod] at this
20+
infer_instance
21+
22+
lemma fin_val_simp {n : ℕ} (Hlt : n < BabyBearPrime) :
23+
(@Fin.val Sp1.BabyBearPrime (@OfNat.ofNat.{0} Sp1.BabyBear n (@Fin.instOfNat Sp1.BabyBearPrime Sp1.instNeZeroNatBabyBearPrime n))) = n := by
24+
simp [BabyBearPrime, OfNat.ofNat] at *; assumption
25+
26+
syntax "PROOF" : term
27+
macro_rules | `(PROOF) => `(sorry)
28+
29+
end Sp1

‎Nethermind/Specs.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
import Nethermind.Basic
2+
3+
namespace Sp1
4+
5+
def spec_32_bit_wrap_add (A1 A2 A3 A4 B1 B2 B3 B4 C1 C2 C3 C4 : BabyBear) : Prop :=
6+
( A1.val < 256 ) ∧ ( A2.val < 256 ) ∧ ( A3.val < 256 ) ∧ ( A4.val < 256 ) ∧
7+
( B1.val < 256 ) ∧ ( B2.val < 256 ) ∧ ( B3.val < 256 ) ∧ ( B4.val < 256 ) ∧
8+
( C1.val < 256 ) ∧ ( C2.val < 256 ) ∧ ( C3.val < 256 ) ∧ ( C4.val < 256 ) ∧
9+
( ( B1.val + 256 * B2.val + 65536 * B3.val + 16777216 * B4.val ) +
10+
( C1.val + 256 * C2.val + 65536 * C3.val + 16777216 * C4.val ) ) % 4294967296 =
11+
( A1.val + 256 * A2.val + 65536 * A3.val + 16777216 * A4.val )
12+
13+
end Sp1

‎lakefile.toml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,6 @@ scope = "leanprover-community"
1313

1414
[[lean_lib]]
1515
name = "Sp1Lean"
16+
17+
[[lean_lib]]
18+
name = "Nethermind"

0 commit comments

Comments
 (0)