forked from starkware-libs/formal-proofs
-
Notifications
You must be signed in to change notification settings - Fork 0
/
signature_recover_public_key_nondet_bigint3_soundness.lean
144 lines (138 loc) · 6.56 KB
/
signature_recover_public_key_nondet_bigint3_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
/-
File: signature_recover_public_key_nondet_bigint3_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.bigint
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.bigint.nondet_bigint3 autogenerated soundness theorem -/
theorem auto_sound_nondet_bigint3
-- arguments
(range_check_ptr : F)
-- code is in memory at σ.pc
(h_mem : mem_at mem code_nondet_bigint3 σ.pc)
-- input arguments on the stack
(hin_range_check_ptr : range_check_ptr = mem (σ.fp - 3))
-- conclusion
: ensures_ret mem σ (λ κ τ,
τ.ap = σ.ap + 8 ∧
∃ μ ≤ κ, rc_ensures mem (rc_bound F) μ (mem (σ.fp - 3)) (mem $ τ.ap - 4)
(spec_nondet_bigint3 mem κ range_check_ptr (mem (τ.ap - 4)) (cast_BigInt3 mem (τ.ap - 3)))) :=
begin
apply ensures_of_ensuresb, intro νbound,
have h_mem_rec := h_mem,
unpack_memory code_nondet_bigint3 at h_mem with ⟨hpc0, hpc1, hpc2, hpc3, hpc4, hpc5, hpc6, hpc7, hpc8, hpc9, hpc10, hpc11⟩,
-- let (ap reference)
apply of_register_state,
intros regstate_res regstateeq_res,
mkdef hl_res : res = cast_BigInt3 mem (regstate_res.ap + 5),
rw [regstateeq_res] at hl_res, try { dsimp at hl_res },
-- const
mkdef hc_MAX_SUM : MAX_SUM = (232113757366008801543585789 : F),
-- compound assert eq
step_assert_eq hpc0 hpc1 with temp0,
step_assert_eq hpc2 with temp1,
step_assert_eq hpc3 with temp2,
step_assert_eq hpc4 with temp3,
step_assert_eq hpc5 with temp4,
have a0: mem range_check_ptr = MAX_SUM - (res.d0 + res.d1 + res.d2), {
apply assert_eq_reduction temp4.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM] },
try { dsimp [cast_BigInt3] },
try { arith_simps }, try { simp only [temp0, temp1, temp2, (eq_sub_of_eq_add temp3)] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a0 }, try { arith_simps at a0 },
clear temp0 temp1 temp2 temp3 temp4,
-- tempvar
step_assert_eq hpc6 hpc7 with tv_range_check_ptr0,
mkdef hl_range_check_ptr₁ : range_check_ptr₁ = (range_check_ptr + 4 : F),
have htv_range_check_ptr₁: range_check_ptr₁ = _, {
apply eq.symm, apply eq.trans tv_range_check_ptr0,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁] },
try { dsimp [cast_BigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } }, },
clear tv_range_check_ptr0,
try { dsimp at hl_range_check_ptr₁ }, try { arith_simps at hl_range_check_ptr₁ },
-- assert eq
step_assert_eq hpc8 with temp0,
have a8: mem (range_check_ptr₁ - 3) = res.d0, {
apply assert_eq_reduction temp0.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
try { dsimp [cast_BigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a8 }, try { arith_simps at a8 },
clear temp0,
-- assert eq
step_assert_eq hpc9 with temp0,
have a9: mem (range_check_ptr₁ - 2) = res.d1, {
apply assert_eq_reduction temp0.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
try { dsimp [cast_BigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a9 }, try { arith_simps at a9 },
clear temp0,
-- assert eq
step_assert_eq hpc10 with temp0,
have a10: mem (range_check_ptr₁ - 1) = res.d2, {
apply assert_eq_reduction temp0.symm,
try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] },
try { dsimp [cast_BigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
},
try { dsimp at a10 }, try { arith_simps at a10 },
clear temp0,
-- return
step_ret hpc11,
-- finish
step_done, use_only [rfl, rfl],
split, refl,
-- range check condition
use_only (4+0+0), split,
linarith [],
split,
{ try { norm_num1 }, arith_simps,
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_nondet_bigint3 mem _ range_check_ptr _ _,
{ apply sound_nondet_bigint3, apply auto_spec },
-- prove the auto generated assertion
dsimp [auto_spec_nondet_bigint3],
try { norm_num1 }, try { arith_simps },
use_only [res],
use [MAX_SUM, hc_MAX_SUM],
use_only [a0],
cases rc_h_range_check_ptr' (0) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a0.symm, hin_range_check_ptr], arith_simps, exact hn },
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 },
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, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
use_only [a9],
cases rc_h_range_check_ptr' (2) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a9.symm, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
use_only [a10],
cases rc_h_range_check_ptr' (3) (by norm_num1) with n hn, arith_simps at hn,
use_only [n], { simp only [a10.symm, hl_range_check_ptr₁, hin_range_check_ptr], arith_simps, exact hn },
try { split, trivial <|> linarith },
try { ensures_simps; try { simp only [add_neg_eq_sub, hin_range_check_ptr, hl_res, hc_MAX_SUM, hl_range_check_ptr₁, htv_range_check_ptr₁] }, },
try { dsimp [cast_BigInt3] },
try { arith_simps; try { split }; triv <|> refl <|> simp <|> abel; try { norm_num } },
end