-
Notifications
You must be signed in to change notification settings - Fork 13
/
signature_recover_public_key_compute_slope_soundness.lean
194 lines (188 loc) · 10.3 KB
/
signature_recover_public_key_compute_slope_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
192
193
/-
File: signature_recover_public_key_compute_slope_soundness.lean
Autogenerated file.
-/
import starkware.cairo.lean.semantics.soundness.hoare
import .signature_recover_public_key_code
import ..signature_recover_public_key_spec
import .signature_recover_public_key_nondet_bigint3_soundness
import .signature_recover_public_key_unreduced_mul_soundness
import .signature_recover_public_key_verify_zero_soundness
open tactic
open starkware.cairo.common.cairo_secp.ec
open starkware.cairo.common.cairo_secp.bigint
open starkware.cairo.common.cairo_secp.bigint3
open starkware.cairo.common.cairo_secp.field
open starkware.cairo.common.cairo_secp.ec_point
variables {F : Type} [field F] [decidable_eq F] [prelude_hyps F]
variable mem : F → F
variable σ : register_state F
/- starkware.cairo.common.cairo_secp.ec.compute_slope autogenerated soundness theorem -/
theorem auto_sound_compute_slope
-- arguments
(range_check_ptr : F) (point0 point1 : EcPoint mem)
-- code is in memory at σ.pc
(h_mem : mem_at mem code_compute_slope σ.pc)
-- all dependencies are in memory
(h_mem_4 : mem_at mem code_nondet_bigint3 (σ.pc - 220))
(h_mem_5 : mem_at mem code_unreduced_mul (σ.pc - 208))
(h_mem_7 : mem_at mem code_verify_zero (σ.pc - 172))
-- input arguments on the stack
(hin_range_check_ptr : range_check_ptr = mem (σ.fp - 15))
(hin_point0 : point0 = cast_EcPoint mem (σ.fp - 14))
(hin_point1 : point1 = cast_EcPoint mem (σ.fp - 8))
-- conclusion
: ensures_ret mem σ (λ κ τ,
τ.ap = σ.ap + 59 ∧
∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 15)) (mem $ τ.ap - 4)
(spec_compute_slope mem κ range_check_ptr point0 point1 (mem (τ.ap - 4)) (cast_BigInt3 mem (τ.ap - 3)))) :=
begin
apply ensures_of_ensuresb, intro νbound,
have h_mem_rec := h_mem,
unpack_memory code_compute_slope 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, hpc23⟩,
-- function call
step_assert_eq hpc0 with arg0,
step_sub hpc1 (auto_sound_nondet_bigint3 mem _ range_check_ptr _ _),
{ rw hpc2, norm_num2, exact h_mem_4 },
{ try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1] },
try { dsimp [cast_EcPoint, cast_BigInt3] },
try { arith_simps }, try { simp only [arg0] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
intros κ_call3 ap3 h_call3,
rcases h_call3 with ⟨h_call3_ap_offset, h_call3⟩,
rcases h_call3 with ⟨rc_m3, rc_mle3, hl_range_check_ptr₁, h_call3⟩,
mkdef htv_range_check_ptr₁ : range_check_ptr₁ = (mem (ap3 - 4)),
simp only [←htv_range_check_ptr₁] at h_call3,
mkdef htv_slope : slope = (cast_BigInt3 mem (ap3 - 3)),
simp only [←htv_slope] at h_call3,
try { simp only [arg0] at hl_range_check_ptr₁ },
try { rw [←htv_range_check_ptr₁] at hl_range_check_ptr₁ }, try { rw [←hin_range_check_ptr] at hl_range_check_ptr₁ },
try { simp only [arg0] at h_call3 },
rw [hin_range_check_ptr] at h_call3,
clear arg0,
-- let
mkdef hl_x_diff : x_diff = ({
d0 := point0.x.d0 - point1.x.d0,
d1 := point0.x.d1 - point1.x.d1,
d2 := point0.x.d2 - point1.x.d2
} : BigInt3 mem),
try { dsimp at hl_x_diff }, try { arith_simps at hl_x_diff },
-- function call
step_assert_eq hpc3 with arg0,
step_assert_eq hpc4 with arg1,
step_assert_eq hpc5 with arg2,
step_assert_eq hpc6 with arg3,
step_assert_eq hpc7 with arg4,
step_assert_eq hpc8 with arg5,
step_sub hpc9 (auto_sound_unreduced_mul mem _ x_diff slope _ _ _),
{ rw hpc10, norm_num2, exact h_mem_5 },
{ try { ext } ; {
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1, htv_range_check_ptr₁, htv_slope, hl_x_diff] },
try { dsimp [cast_EcPoint, cast_BigInt3] },
try { arith_simps }, try { simp only [(eq_sub_of_eq_add arg0), (eq_sub_of_eq_add arg1), (eq_sub_of_eq_add arg2), arg3, arg4, arg5] },
try { simp only [h_call3_ap_offset] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
{ try { ext } ; {
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1, htv_range_check_ptr₁, htv_slope, hl_x_diff] },
try { dsimp [cast_EcPoint, cast_BigInt3] },
try { arith_simps }, try { simp only [(eq_sub_of_eq_add arg0), (eq_sub_of_eq_add arg1), (eq_sub_of_eq_add arg2), arg3, arg4, arg5] },
try { simp only [h_call3_ap_offset] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
intros κ_call11 ap11 h_call11,
rcases h_call11 with ⟨h_call11_ap_offset, h_call11⟩,
mkdef htv_x_diff_slope : x_diff_slope = (cast_UnreducedBigInt3 mem (ap11 - 3)),
simp only [←htv_x_diff_slope] at h_call11,
clear arg0 arg1 arg2 arg3 arg4 arg5,
-- function call
step_assert_eq hpc11 with arg0,
step_assert_eq hpc12 with arg1,
step_assert_eq hpc13 with arg2,
step_assert_eq hpc14 with arg3,
step_assert_eq hpc15 with arg4,
step_assert_eq hpc16 with arg5,
step_assert_eq hpc17 with arg6,
step_sub hpc18 (auto_sound_verify_zero mem _ range_check_ptr₁ {
d0 := x_diff_slope.d0 - point0.y.d0 + point1.y.d0,
d1 := x_diff_slope.d1 - point0.y.d1 + point1.y.d1,
d2 := x_diff_slope.d2 - point0.y.d2 + point1.y.d2
} _ _ _),
{ rw hpc19, norm_num2, exact h_mem_7 },
{ try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1, htv_range_check_ptr₁, htv_slope, hl_x_diff, htv_x_diff_slope] },
try { dsimp [cast_EcPoint, cast_BigInt3, cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [(eq_sub_of_eq_add arg0), (eq_sub_of_eq_add arg1), (eq_sub_of_eq_add arg2), arg3, arg4, arg5, arg6] },
try { simp only [h_call3_ap_offset, h_call11_ap_offset] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
{ try { ext } ; {
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1, htv_range_check_ptr₁, htv_slope, hl_x_diff, htv_x_diff_slope] },
try { dsimp [cast_EcPoint, cast_BigInt3, cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [(eq_sub_of_eq_add arg0), (eq_sub_of_eq_add arg1), (eq_sub_of_eq_add arg2), arg3, arg4, arg5, arg6] },
try { simp only [h_call3_ap_offset, h_call11_ap_offset] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },}, },
intros κ_call20 ap20 h_call20,
rcases h_call20 with ⟨h_call20_ap_offset, h_call20⟩,
rcases h_call20 with ⟨rc_m20, rc_mle20, hl_range_check_ptr₂, h_call20⟩,
mkdef htv_range_check_ptr₂ : range_check_ptr₂ = (mem (ap20 - 1)),
simp only [←htv_range_check_ptr₂] at h_call20,
try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6] at hl_range_check_ptr₂ },
try { rw [h_call11_ap_offset] at hl_range_check_ptr₂ }, try { arith_simps at hl_range_check_ptr₂ },
try { rw [←htv_range_check_ptr₂] at hl_range_check_ptr₂ }, try { rw [←htv_range_check_ptr₁] at hl_range_check_ptr₂ },
try { simp only [arg0 ,arg1 ,arg2 ,arg3 ,arg4 ,arg5 ,arg6] at h_call20 },
try { rw [h_call11_ap_offset] at h_call20 }, try { arith_simps at h_call20 },
rw [←htv_range_check_ptr₁, hl_range_check_ptr₁, hin_range_check_ptr] at h_call20,
clear arg0 arg1 arg2 arg3 arg4 arg5 arg6,
-- return
step_assert_eq hpc20 with hret0,
step_assert_eq hpc21 with hret1,
step_assert_eq hpc22 with hret2,
step_ret hpc23,
-- finish
step_done, use_only [rfl, rfl],
split,
{ try { simp only [h_call3_ap_offset ,h_call11_ap_offset ,h_call20_ap_offset] },
try { arith_simps }, try { refl } },
-- range check condition
use_only (rc_m3+rc_m20+0+0), split,
linarith [rc_mle3, rc_mle20],
split,
{ try { norm_num1 }, arith_simps, try { simp only [hret0 ,hret1 ,hret2] },
try { rw [←htv_range_check_ptr₂] }, try { rw [hl_range_check_ptr₂] }, try { rw [←htv_range_check_ptr₁] }, try { rw [hl_range_check_ptr₁] }, try { rw [hin_range_check_ptr] },
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_compute_slope mem _ range_check_ptr point0 point1 _ _,
{ apply sound_compute_slope, apply auto_spec },
-- prove the auto generated assertion
dsimp [auto_spec_compute_slope],
try { norm_num1 }, try { arith_simps },
use_only [κ_call3],
use_only [range_check_ptr₁],
use_only [slope],
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₁' },
have spec3 := h_call3 rc_h_range_check_ptr',
try { rw [←hin_range_check_ptr] at spec3 }, try { rw [←htv_range_check_ptr₁] at spec3 },
try { dsimp at spec3, arith_simps at spec3 },
use_only [spec3],
use_only [x_diff, hl_x_diff],
try { dsimp }, try { arith_simps },
use_only [κ_call11],
use_only [x_diff_slope],
try { dsimp at h_call11, arith_simps at h_call11 },
try { use_only [h_call11] },
use_only [κ_call20],
use_only [range_check_ptr₂],
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₂' },
have spec20 := h_call20 rc_h_range_check_ptr₁',
try { rw [←hin_range_check_ptr] at spec20 }, try { rw [←hl_range_check_ptr₁] at spec20 }, try { rw [←htv_range_check_ptr₂] at spec20 },
try { dsimp at spec20, arith_simps at spec20 },
use_only [spec20],
try { split, trivial <|> linarith },
try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hin_point0, hin_point1, htv_range_check_ptr₁, htv_slope, hl_x_diff, htv_x_diff_slope, htv_range_check_ptr₂] }, },
try { dsimp [cast_EcPoint, cast_BigInt3, cast_UnreducedBigInt3] },
try { arith_simps }, try { simp only [hret0, hret1, hret2] },
try { simp only [h_call3_ap_offset, h_call11_ap_offset, h_call20_ap_offset] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end