forked from starkware-libs/formal-proofs
-
Notifications
You must be signed in to change notification settings - Fork 0
/
signature_recover_public_key_verify_zero_soundness.lean
192 lines (186 loc) · 8.83 KB
/
signature_recover_public_key_verify_zero_soundness.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
/-
File: signature_recover_public_key_verify_zero_soundness.lean
Autogenerated file.
-/
import starkware.cairo.lean.semantics.soundness.hoare
import .signature_recover_public_key_code
import ..signature_recover_public_key_spec
open tactic
open starkware.cairo.common.cairo_secp.field
open starkware.cairo.common.cairo_secp.bigint3
open starkware.cairo.common.cairo_secp.constants
variables {F : Type} [field F] [decidable_eq F] [prelude_hyps F]
variable mem : F → F
variable σ : register_state F
/- starkware.cairo.common.cairo_secp.field.verify_zero autogenerated soundness theorem -/
theorem auto_sound_verify_zero
-- arguments
(range_check_ptr : F) (val : UnreducedBigInt3 mem)
-- code is in memory at σ.pc
(h_mem : mem_at mem code_verify_zero σ.pc)
-- input arguments on the stack
(hin_range_check_ptr : range_check_ptr = mem (σ.fp - 6))
(hin_val : val = cast_UnreducedBigInt3 mem (σ.fp - 5))
-- conclusion
: ensures_ret mem σ (λ κ τ,
τ.ap = σ.ap + 11 ∧
∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 6)) (mem $ τ.ap - 1)
(spec_verify_zero mem κ range_check_ptr val (mem (τ.ap - 1)))) :=
begin
apply ensures_of_ensuresb, intro νbound,
have h_mem_rec := h_mem,
unpack_memory code_verify_zero at h_mem with ⟨hpc0, hpc1, hpc2, hpc3, hpc4, hpc5, hpc6, hpc7, hpc8, hpc9, hpc10, hpc11, hpc12, hpc13, hpc14, hpc15, hpc16, hpc17, hpc18, hpc19, hpc20, hpc21, hpc22⟩,
-- let (ap reference)
apply of_register_state,
intros regstate_q regstateeq_q,
mkdef hl_q : q = mem regstate_q.ap,
rw [regstateeq_q] at hl_q, try { dsimp at hl_q },
-- let (ap reference)
apply of_register_state,
intros regstate_q_biased regstateeq_q_biased,
mkdef hl_q_biased : q_biased = mem (regstate_q_biased.ap + 1),
rw [regstateeq_q_biased] at hl_q_biased, try { dsimp at hl_q_biased },
-- assert eq
step_assert_eq hpc0 hpc1 with temp0,
have a0: q_biased = q + 2 ^ 127, {
apply assert_eq_reduction temp0,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a0 }, try { arith_simps at a0 },
clear temp0,
-- assert eq
step_assert_eq hpc2 with temp0,
have a2: mem range_check_ptr = q_biased, {
apply assert_eq_reduction temp0.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a2 }, try { arith_simps at a2 },
clear temp0,
-- tempvar
step_assert_eq hpc3 hpc4 with tv_r10,
step_assert_eq hpc5 with tv_r11,
step_assert_eq hpc6 hpc7 with tv_r12,
mkdef hl_r1 : r1 = ((val.d0 + q * SECP_REM) / (BASE : ℤ) : F),
have htv_r1: r1 = _, {
have h_δ3_c0 : ∀ x : F, x / (BASE : ℤ) = x * (-46768052394588894761721767695234645457402928824320 : ℤ),
{ intro x, apply div_eq_mul_inv', apply PRIME.int_cast_mul_eq_one, rw [PRIME], try { simp_int_casts }, norm_num1 },
apply eq.symm, apply eq.trans tv_r12,
try { simp only [h_δ3_c0] at hl_r1 },
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [tv_r10, tv_r11] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
clear tv_r10 tv_r11 tv_r12,
try { dsimp at hl_r1 }, try { arith_simps at hl_r1 },
-- compound assert eq
step_assert_eq hpc8 hpc9 with temp0,
step_assert_eq hpc10 with temp1,
have a8: mem (range_check_ptr + 1) = r1 + 2 ^ 127, {
apply assert_eq_reduction temp1.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1, htv_r1] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [temp0] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a8 }, try { arith_simps at a8 },
clear temp0 temp1,
-- tempvar
step_assert_eq hpc11 with tv_r20,
step_assert_eq hpc12 hpc13 with tv_r21,
mkdef hl_r2 : r2 = ((val.d1 + r1) / (BASE : ℤ) : F),
have htv_r2: r2 = _, {
have h_δ11_c0 : ∀ x : F, x / (BASE : ℤ) = x * (-46768052394588894761721767695234645457402928824320 : ℤ),
{ intro x, apply div_eq_mul_inv', apply PRIME.int_cast_mul_eq_one, rw [PRIME], try { simp_int_casts }, norm_num1 },
apply eq.symm, apply eq.trans tv_r21,
try { simp only [h_δ11_c0] at hl_r2 },
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1, htv_r1, hl_r2] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [tv_r20] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
clear tv_r20 tv_r21,
try { dsimp at hl_r2 }, try { arith_simps at hl_r2 },
-- compound assert eq
step_assert_eq hpc14 hpc15 with temp0,
step_assert_eq hpc16 with temp1,
have a14: mem (range_check_ptr + 2) = r2 + 2 ^ 127, {
apply assert_eq_reduction temp1.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1, htv_r1, hl_r2, htv_r2] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [temp0] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a14 }, try { arith_simps at a14 },
clear temp0 temp1,
-- compound assert eq
have h_δ17_c0 : ((BASE : ℤ) / (4 : ℤ) : F) = (19342813113834066795298816 : ℤ),
{ apply PRIME.div_eq_const,
{ apply PRIME.cast_ne_zero, norm_num1, rw [PRIME], try { simp_int_casts }, norm_num1 },
rw [PRIME], try { simp_int_casts }, norm_num1 },
step_assert_eq hpc17 hpc18 with temp0,
step_assert_eq hpc19 with temp1,
have a17: val.d2 = q * ((BASE : ℤ) / (4 : ℤ)) - r2, {
try { simp only [h_δ17_c0] },
apply assert_eq_reduction (eq_sub_of_eq_add temp1),
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1, htv_r1, hl_r2, htv_r2] },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [temp0] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a17 }, try { arith_simps at a17 },
clear temp0 temp1,
-- let
mkdef hl_range_check_ptr₁ : range_check_ptr₁ = (range_check_ptr + 3 : F),
try { dsimp at hl_range_check_ptr₁ }, try { arith_simps at hl_range_check_ptr₁ },
-- return
step_assert_eq hpc20 hpc21 with hret0,
step_ret hpc22,
-- finish
step_done, use_only [rfl, rfl],
split, refl,
-- range check condition
use_only (3+0+0), split,
linarith [],
split,
{ try { norm_num1 }, arith_simps, try { simp only [hret0] },
try { ring_nf }, try { arith_simps, refl <|> norm_cast }, try { refl } },
intro rc_h_range_check_ptr, repeat { rw [add_assoc] at rc_h_range_check_ptr },
have rc_h_range_check_ptr' := range_checked_add_right rc_h_range_check_ptr,
-- Final Proof
-- user-provided reduction
suffices auto_spec: auto_spec_verify_zero mem _ range_check_ptr val _,
{ apply sound_verify_zero, apply auto_spec },
-- prove the auto generated assertion
dsimp [auto_spec_verify_zero],
try { norm_num1 }, try { arith_simps },
use_only [q],
use_only [q_biased],
use_only [a0],
use_only [a2],
cases rc_h_range_check_ptr' (0) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a2.symm, hin_range_check_ptr], arith_simps, exact hn },
use_only [r1, hl_r1],
try { dsimp }, try { arith_simps },
use_only [a8],
cases rc_h_range_check_ptr' (1) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a8.symm, hin_range_check_ptr], arith_simps, exact hn },
use_only [r2, hl_r2],
try { dsimp }, try { arith_simps },
use_only [a14],
cases rc_h_range_check_ptr' (2) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a14.symm, hin_range_check_ptr], arith_simps, exact hn },
use_only [a17],
have rc_h_range_check_ptr₁ := range_checked_offset' rc_h_range_check_ptr,
have rc_h_range_check_ptr₁' := range_checked_add_right rc_h_range_check_ptr₁,
try { norm_cast at rc_h_range_check_ptr₁' }, try { rw [add_zero] at rc_h_range_check_ptr₁' },
use_only [range_check_ptr₁, hl_range_check_ptr₁],
try { dsimp }, try { arith_simps },
try { split, trivial <|> linarith },
try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_val, hl_q, hl_q_biased, hl_r1, htv_r1, hl_r2, htv_r2, hl_range_check_ptr₁] }, },
try { dsimp [cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [hret0] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end