forked from starkware-libs/formal-proofs
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsquash_dict_code.lean
185 lines (174 loc) · 8.16 KB
/
squash_dict_code.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
/-
File: squash_dict_code.lean
Autogenerated file.
-/
import starkware.cairo.lean.semantics.soundness.hoare
variables {F : Type} [field F] [decidable_eq F]
/- function starkware.cairo.common.math.assert_le_felt code definition -/
def starkware.cairo.common.math.code_assert_le_felt : list F := [
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res['op1[op0]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res['op1[op0+ 1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res[op0* 'op1[imm]];ap++].to_nat,
3544607988759775765608368578435044694,
'assert_eq[op0:='op0[ap+ -3], 'dst[ap] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res['op1[op0+ 2]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res['op1[op0+ 3]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res[op0* 'op1[imm]];ap++].to_nat,
5316911983139663648412552867652567041,
'assert_eq[op0:='op0[ap+ -3], 'dst[ap] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'jnz_rel['op1[imm], 'dst[ap];ap++].to_nat,
14,
'assert_eq['dst[ap] === 'res['op1[imm]];ap++].to_nat,
-1,
'assert_eq[op0:='op0[ap], 'dst[ap+ -1] === 'res[op0+ 'op1[fp+ -4]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -8], 'dst[ap+ -1] === 'res[op0+ 'op1[ap+ -4]]].to_nat,
'assert_eq[op0:='op0[ap], 'dst[fp+ -4] === 'res[op0+ 'op1[fp+ -3]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -3], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq[op0:='op0[ap+ -2], 'dst[ap] === 'res[op0* 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -11], 'dst[ap+ -1] === 'res[op0* 'op1[ap+ -7]]].to_nat,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
4,
'ret[].to_nat,
'jnz_rel['op1[imm], 'dst[ap];ap++].to_nat,
12,
'assert_eq['dst[ap] === 'res['op1[imm]];ap++].to_nat,
-1,
'assert_eq[op0:='op0[ap], 'dst[ap+ -1] === 'res[op0+ 'op1[fp+ -3]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -10], 'dst[ap+ -1] === 'res[op0+ 'op1[ap+ -6]]].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0* 'op1[ap+ -2]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -11], 'dst[ap+ -1] === 'res[op0* 'op1[ap+ -7]]].to_nat,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
4,
'ret[].to_nat,
'assert_eq[op0:='op0[ap+ -7], 'dst[fp+ -3] === 'res[op0+ 'op1[ap+ -3]]].to_nat,
'assert_eq[op0:='op0[ap], 'dst[fp+ -3] === 'res[op0+ 'op1[fp+ -4]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0* 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -9], 'dst[ap+ -1] === 'res[op0* 'op1[ap+ -5]]].to_nat,
'ap+=['res['op1[imm]]].to_nat,
2,
'assert_eq[op0:='op0[fp+ -5], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
4,
'ret[].to_nat
]
/- function starkware.cairo.common.math.assert_lt_felt code definition -/
def starkware.cairo.common.math.code_assert_lt_felt : list F := [
'assert_eq[op0:='op0[ap], 'dst[fp+ -4] === 'res[op0+ 'op1[fp+ -3]];ap++].to_nat,
'jnz_rel['op1[imm], 'dst[ap+ -1]].to_nat,
4,
'assert_eq[op0:='op0[fp+ -4], 'dst[fp+ -4] === 'res[op0+ 'op1[imm]]].to_nat,
1,
'assert_eq['dst[ap] === 'res['op1[fp+ -5]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -4]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -3]];ap++].to_nat,
'call_rel['op1[imm]].to_nat,
-53,
'ret[].to_nat
]
/- function starkware.cairo.common.squash_dict.squash_dict_inner code definition -/
def code_squash_dict_inner : list F := [
'ap+=['res['op1[imm]]].to_nat,
2,
'assert_eq[op0:='op0[fp+ -9], 'dst[ap] === 'res['op1[op0]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res[op0* 'op1[imm]];ap++].to_nat,
3,
'assert_eq[op0:='op0[fp+ -8], 'dst[ap+ 1] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap], 'dst[ap+ -1] === 'res['op1[op0+ 2]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -9], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq[op0:='op0[ap+ -2], 'dst[fp+ -6] === 'res['op1[op0]]].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[fp+ -6] === 'res['op1[op0]]].to_nat,
'assert_eq[op0:='op0[ap+ -2], 'dst[fp] === 'res['op1[op0+ 1]]].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[fp] === 'res['op1[op0+ 1]]].to_nat,
'jnz_rel['op1[imm], 'dst[fp+ 1]].to_nat,
15,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res['op1[op0]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res[op0* 'op1[imm]];ap++].to_nat,
3,
'assert_eq[op0:='op0[ap+ -5], 'dst[ap+ 2] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ 1], 'dst[ap+ -7] === 'res['op1[op0+ 1]]].to_nat,
'assert_eq[op0:='op0[ap+ 1], 'dst[ap] === 'res['op1[op0+ 2]];ap++].to_nat,
'assert_eq[op0:='op0[ap], 'dst[fp+ -6] === 'res['op1[op0]]].to_nat,
'assert_eq[op0:='op0[ap+ -6], 'dst[ap+ 1] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'jnz_rel['op1[imm], 'dst[ap+ -3];ap++].to_nat,
-11,
'assert_eq[op0:='op0[ap], 'dst[fp+ -7] === 'res[op0+ 'op1[ap+ -2]]].to_nat,
'assert_eq[op0:='op0[ap+ -1], 'dst[ap] === 'res['op1[op0]];ap++].to_nat,
'assert_eq[op0:='op0[ap], 'dst[ap+ -2] === 'res[op0+ 'op1[fp+ -9]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap+ -5] === 'res['op1[op0+ 2]]].to_nat,
'assert_eq[op0:='op0[ap], 'dst[fp+ -5] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'jnz_rel['op1[imm], 'dst[ap+ -1]].to_nat,
7,
'assert_eq[op0:='op0[ap+ -4], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
3,
'ret[].to_nat,
'ap+=['res['op1[imm]]].to_nat,
1,
'jnz_rel['op1[imm], 'dst[fp+ -3]].to_nat,
14,
'assert_eq[op0:='op0[fp+ -6], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq[op0:='op0[ap], 'dst[ap+ -2] === 'res[op0+ 'op1[ap+ -1]];ap++].to_nat,
'assert_eq[op0:='op0[ap+ -7], 'dst[ap+ -1] === 'res['op1[op0+ 1]]].to_nat,
'assert_eq[op0:='op0[ap+ -7], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
2,
'assert_eq['dst[ap] === 'res['op1[fp+ -8]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -7]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -6]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -8]];ap++].to_nat,
'jmp_rel['op1[imm]].to_nat,
'[#nz 12],
'assert_eq[op0:='op0[ap+ -5], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'assert_eq['dst[ap] === 'res['op1[fp+ -6]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -3]];ap++].to_nat,
'call_rel['op1[imm]].to_nat,
-99,
'assert_eq['dst[ap] === 'res['op1[fp+ -8]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -7]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -29]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -31]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
3,
'assert_eq['dst[ap] === 'res['op1[fp+ -3]];ap++].to_nat,
'call_rel['op1[imm]].to_nat,
-69,
'ret[].to_nat
]
/- function starkware.cairo.common.squash_dict.squash_dict code definition -/
def code_squash_dict : list F := [
'ap+=['res['op1[imm]]].to_nat,
3,
'assert_eq[op0:='op0[fp], 'dst[fp+ -4] === 'res[op0+ 'op1[fp+ -5]]].to_nat,
'jnz_rel['op1[imm], 'dst[fp]].to_nat,
5,
'assert_eq['dst[ap] === 'res['op1[fp+ -6]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -3]];ap++].to_nat,
'ret[].to_nat,
'assert_eq[op0:='op0[fp], 'dst[ap] === 'res[op0* 'op1[imm]];ap++].to_nat,
1206167596222043737899107594365023368541035738443865566657697352045290673494,
'jnz_rel['op1[imm], 'dst[fp+ 2]].to_nat,
7,
'assert_eq[op0:='op0[fp+ -6], 'dst[fp+ 1] === 'res['op1[op0]]].to_nat,
'assert_eq[op0:='op0[fp+ -6], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
1,
'jmp_rel['op1[imm]].to_nat,
'[#nz 3],
'assert_eq['dst[ap] === 'res['op1[fp+ -6]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -5]];ap++].to_nat,
'assert_eq[op0:='op0[fp+ -4], 'dst[ap] === 'res[op0+ 'op1[imm]];ap++].to_nat,
-1,
'assert_eq['dst[ap] === 'res['op1[fp+ 1]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[ap+ -5]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ -3]];ap++].to_nat,
'assert_eq['dst[ap] === 'res['op1[fp+ 2]];ap++].to_nat,
'call_rel['op1[imm]].to_nat,
3,
'ret[].to_nat
]