-
Notifications
You must be signed in to change notification settings - Fork 13
/
constraints_autogen.lean
174 lines (150 loc) · 17.5 KB
/
constraints_autogen.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
/- This file is generated automatically by generate_constraints.py. -/
import algebra.field.power
notation `offset_size` := 2^16
notation `half_offset_size` := 2^15
def column (F : Type*) := nat → F
def column.off {F : Type*} (c : column F) (i j : nat) := c (i + j)
structure input_data (F : Type*) :=
(trace_length : nat)
(initial_ap : nat)
(initial_pc : nat)
(final_ap : nat)
(final_pc : nat)
(m_star : F → option F)
structure public_data (F : Type*) :=
(initial_ecdsa_addr : F)
(initial_pedersen_addr : nat)
(initial_rc_addr : nat)
(memory__multi_column_perm__hash_interaction_elm0 : F)
(memory__multi_column_perm__perm__interaction_elm : F)
(memory__multi_column_perm__perm__public_memory_prod : F)
(rc16__perm__interaction_elm : F)
(rc16__perm__public_memory_prod : F)
(rc_max : nat)
(rc_min : nat)
structure columns (F : Type*) :=
(column0 : column F)
(column1 : column F)
(column10 : column F)
(column11 : column F)
(column12 : column F)
(column13 : column F)
(column14 : column F)
(column15 : column F)
(column16 : column F)
(column17 : column F)
(column18 : column F)
(column19 : column F)
(column2 : column F)
(column20 : column F)
(column21 : column F)
(column22 : column F)
(column3 : column F)
(column4 : column F)
(column5 : column F)
(column6 : column F)
(column7 : column F)
(column8 : column F)
(column9 : column F)
structure columns_inter (F : Type*) :=
(column23_inter1 : column F)
(column24_inter1 : column F)
namespace columns
variables {F : Type*} (c : columns F) (i : nat)
@[simp] def cpu__decode__instruction := c.column19.off i 1
@[simp] def cpu__decode__mem_inst__addr := c.column19.off i 0
@[simp] def cpu__decode__mem_inst__value := c.column19.off i 1
@[simp] def cpu__decode__off0 := c.column0.off i 0
@[simp] def cpu__decode__off1 := c.column0.off i 8
@[simp] def cpu__decode__off2 := c.column0.off i 4
@[simp] def cpu__decode__opcode_rc__column := c.column1.off i 0
@[simp] def cpu__decode__pc := c.column19.off i 0
@[simp] def cpu__operands__mem_dst__addr := c.column19.off i 8
@[simp] def cpu__operands__mem_dst__value := c.column19.off i 9
@[simp] def cpu__operands__mem_op0__addr := c.column19.off i 4
@[simp] def cpu__operands__mem_op0__value := c.column19.off i 5
@[simp] def cpu__operands__mem_op1__addr := c.column19.off i 12
@[simp] def cpu__operands__mem_op1__value := c.column19.off i 13
@[simp] def cpu__operands__ops_mul := c.column21.off i 4
@[simp] def cpu__operands__res := c.column21.off i 12
@[simp] def cpu__registers__ap := c.column21.off i 0
@[simp] def cpu__registers__fp := c.column21.off i 8
@[simp] def cpu__update_registers__update_pc__tmp0 := c.column21.off i 2
@[simp] def cpu__update_registers__update_pc__tmp1 := c.column21.off i 10
@[simp] def mem_pool__addr := c.column19.off i 0
@[simp] def mem_pool__value := c.column19.off i 1
@[simp] def memory__sorted__addr := c.column20.off i 0
@[simp] def memory__sorted__value := c.column20.off i 1
@[simp] def orig__public_memory__addr := c.column19.off i 2
@[simp] def orig__public_memory__value := c.column19.off i 3
@[simp] def rc16__sorted := c.column2.off i 0
@[simp] def rc16_pool := c.column0.off i 0
@[simp] def rc_builtin__inner_rc := c.column0.off i 12
@[simp] def rc_builtin__mem__addr := c.column19.off i 102
@[simp] def rc_builtin__mem__value := c.column19.off i 103
end columns
namespace columns_inter
variables {F : Type*} (ci : columns_inter F) (i : nat)
@[simp] def memory__multi_column_perm__perm__cum_prod0 := ci.column24_inter1.off i 0
@[simp] def rc16__perm__cum_prod0 := ci.column23_inter1.off i 0
end columns_inter
variables {F: Type*} [field F]
structure cpu__decode (c : columns F) : Prop :=
(flag_op1_base_op0_bit : ∀ i: nat, (((i % 16 = 0))) → (1 - ((c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + (c.column1.off i 4) - ((c.column1.off i 5) + (c.column1.off i 5)) + (c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4)))) * (1 - ((c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + (c.column1.off i 4) - ((c.column1.off i 5) + (c.column1.off i 5)) + (c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4)))) - (1 - ((c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + (c.column1.off i 4) - ((c.column1.off i 5) + (c.column1.off i 5)) + (c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4)))) = 0)
(flag_pc_update_regular_bit : ∀ i: nat, (((i % 16 = 0))) → (1 - ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8)) + (c.column1.off i 8) - ((c.column1.off i 9) + (c.column1.off i 9)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * (1 - ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8)) + (c.column1.off i 8) - ((c.column1.off i 9) + (c.column1.off i 9)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) - (1 - ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8)) + (c.column1.off i 8) - ((c.column1.off i 9) + (c.column1.off i 9)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) = 0)
(flag_res_op1_bit : ∀ i: nat, (((i % 16 = 0))) → (1 - ((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6)) + (c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * (1 - ((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6)) + (c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) - (1 - ((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6)) + (c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) = 0)
(fp_update_regular_bit : ∀ i: nat, (((i % 16 = 0))) → (1 - ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + (c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14)))) * (1 - ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + (c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14)))) - (1 - ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + (c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14)))) = 0)
(opcode_rc__bit : ∀ i: nat, (¬ ((i % 16 = 15))) → ((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1))) * ((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1))) - ((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1))) = 0)
(opcode_rc__zero : ∀ i: nat, (((i % 16 = 15))) → c.column1.off i 0 = 0)
(opcode_rc_input : ∀ i: nat, (((i % 16 = 0))) → (c.column19.off i 1) - ((((c.column1.off i 0) * offset_size + (c.column0.off i 4)) * offset_size + (c.column0.off i 8)) * offset_size + (c.column0.off i 0)) = 0)
structure cpu__opcodes (c : columns F) : Prop :=
(assert_eq__assert_eq : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 14) - ((c.column1.off i 15) + (c.column1.off i 15))) * ((c.column19.off i 9) - (c.column21.off i 12)) = 0)
(call__flags : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + (c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + 1 + 1 - ((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1)) + (c.column1.off i 1) - ((c.column1.off i 2) + (c.column1.off i 2)) + 4)) = 0)
(call__off0 : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column0.off i 0) - half_offset_size) = 0)
(call__off1 : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column0.off i 8) - (half_offset_size + 1)) = 0)
(call__push_fp : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column19.off i 9) - (c.column21.off i 8)) = 0)
(call__push_pc : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column19.off i 5) - ((c.column19.off i 0) + (c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + 1)) = 0)
(ret__flags : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14))) * ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8)) + (c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1)) + (c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4)) + 1 - ((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6)) + (c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10))) - 4) = 0)
(ret__off0 : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14))) * ((c.column0.off i 0) + 2 - half_offset_size) = 0)
(ret__off2 : ∀ i: nat, (((i % 16 = 0))) → ((c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14))) * ((c.column0.off i 4) + 1 - half_offset_size) = 0)
structure cpu__operands (c : columns F) : Prop :=
(mem0_addr : ∀ i: nat, (((i % 16 = 0))) → (c.column19.off i 4) + half_offset_size - (((c.column1.off i 1) - ((c.column1.off i 2) + (c.column1.off i 2))) * (c.column21.off i 8) + (1 - ((c.column1.off i 1) - ((c.column1.off i 2) + (c.column1.off i 2)))) * (c.column21.off i 0) + (c.column0.off i 8)) = 0)
(mem1_addr : ∀ i: nat, (((i % 16 = 0))) → (c.column19.off i 12) + half_offset_size - (((c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3))) * (c.column19.off i 0) + ((c.column1.off i 4) - ((c.column1.off i 5) + (c.column1.off i 5))) * (c.column21.off i 0) + ((c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4))) * (c.column21.off i 8) + (1 - ((c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + (c.column1.off i 4) - ((c.column1.off i 5) + (c.column1.off i 5)) + (c.column1.off i 3) - ((c.column1.off i 4) + (c.column1.off i 4)))) * (c.column19.off i 5) + (c.column0.off i 4)) = 0)
(mem_dst_addr : ∀ i: nat, (((i % 16 = 0))) → (c.column19.off i 8) + half_offset_size - (((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1))) * (c.column21.off i 8) + (1 - ((c.column1.off i 0) - ((c.column1.off i 1) + (c.column1.off i 1)))) * (c.column21.off i 0) + (c.column0.off i 0)) = 0)
(ops_mul : ∀ i: nat, (((i % 16 = 0))) → (c.column21.off i 4) - (c.column19.off i 5) * (c.column19.off i 13) = 0)
(res : ∀ i: nat, (((i % 16 = 0))) → (1 - ((c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * (c.column21.off i 12) - (((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6))) * ((c.column19.off i 5) + (c.column19.off i 13)) + ((c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7))) * (c.column21.off i 4) + (1 - ((c.column1.off i 5) - ((c.column1.off i 6) + (c.column1.off i 6)) + (c.column1.off i 6) - ((c.column1.off i 7) + (c.column1.off i 7)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * (c.column19.off i 13)) = 0)
structure cpu__update_registers (inp : input_data F) (c : columns F) : Prop :=
(update_ap__ap_update : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 16) - ((c.column21.off i 0) + ((c.column1.off i 10) - ((c.column1.off i 11) + (c.column1.off i 11))) * (c.column21.off i 12) + (c.column1.off i 11) - ((c.column1.off i 12) + (c.column1.off i 12)) + ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * 2) = 0)
(update_fp__fp_update : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 24) - ((1 - ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13)) + (c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14)))) * (c.column21.off i 8) + ((c.column1.off i 13) - ((c.column1.off i 14) + (c.column1.off i 14))) * (c.column19.off i 9) + ((c.column1.off i 12) - ((c.column1.off i 13) + (c.column1.off i 13))) * ((c.column21.off i 0) + 2)) = 0)
(update_pc__pc_cond_negative : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → (1 - ((c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * (c.column19.off i 16) + (c.column21.off i 2) * ((c.column19.off i 16) - ((c.column19.off i 0) + (c.column19.off i 13))) - ((1 - ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8)) + (c.column1.off i 8) - ((c.column1.off i 9) + (c.column1.off i 9)) + (c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * ((c.column19.off i 0) + (c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + 1) + ((c.column1.off i 7) - ((c.column1.off i 8) + (c.column1.off i 8))) * (c.column21.off i 12) + ((c.column1.off i 8) - ((c.column1.off i 9) + (c.column1.off i 9))) * ((c.column19.off i 0) + (c.column21.off i 12))) = 0)
(update_pc__pc_cond_positive : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → ((c.column21.off i 10) - ((c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10)))) * ((c.column19.off i 16) - ((c.column19.off i 0) + (c.column1.off i 2) - ((c.column1.off i 3) + (c.column1.off i 3)) + 1)) = 0)
(update_pc__tmp0 : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 2) - ((c.column1.off i 9) - ((c.column1.off i 10) + (c.column1.off i 10))) * (c.column19.off i 9) = 0)
(update_pc__tmp1 : ∀ i: nat, (((i % 16 = 0)) ∧ ¬ (i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 10) - (c.column21.off i 2) * (c.column21.off i 12) = 0)
structure memory (inp : input_data F) (pd : public_data F) (c : columns F) (ci : columns_inter F) : Prop :=
(diff_is_bit : ∀ i: nat, (((i % 2 = 0)) ∧ ¬ (i = 2 * (inp.trace_length / 2 - 1))) → ((c.column20.off i 2) - (c.column20.off i 0)) * ((c.column20.off i 2) - (c.column20.off i 0)) - ((c.column20.off i 2) - (c.column20.off i 0)) = 0)
(initial_addr : ∀ i: nat, ((i = 0)) → (c.column20.off i 0) - 1 = 0)
(is_func : ∀ i: nat, (((i % 2 = 0)) ∧ ¬ (i = 2 * (inp.trace_length / 2 - 1))) → ((c.column20.off i 2) - (c.column20.off i 0) - 1) * ((c.column20.off i 1) - (c.column20.off i 3)) = 0)
(multi_column_perm__perm__init0 : ∀ i: nat, ((i = 0)) → (pd.memory__multi_column_perm__perm__interaction_elm - ((c.column20.off i 0) + pd.memory__multi_column_perm__hash_interaction_elm0 * (c.column20.off i 1))) * (ci.column24_inter1.off i 0) + (c.column19.off i 0) + pd.memory__multi_column_perm__hash_interaction_elm0 * (c.column19.off i 1) - pd.memory__multi_column_perm__perm__interaction_elm = 0)
(multi_column_perm__perm__last : ∀ i: nat, ((i = 2 * (inp.trace_length / 2 - 1))) → (ci.column24_inter1.off i 0) - pd.memory__multi_column_perm__perm__public_memory_prod = 0)
(multi_column_perm__perm__step0 : ∀ i: nat, (((i % 2 = 0)) ∧ ¬ (i = 2 * (inp.trace_length / 2 - 1))) → (pd.memory__multi_column_perm__perm__interaction_elm - ((c.column20.off i 2) + pd.memory__multi_column_perm__hash_interaction_elm0 * (c.column20.off i 3))) * (ci.column24_inter1.off i 2) - (pd.memory__multi_column_perm__perm__interaction_elm - ((c.column19.off i 2) + pd.memory__multi_column_perm__hash_interaction_elm0 * (c.column19.off i 3))) * (ci.column24_inter1.off i 0) = 0)
structure public_memory (c : columns F) : Prop :=
(addr_zero : ∀ i: nat, (((i % 8 = 0))) → c.column19.off i 2 = 0)
(value_zero : ∀ i: nat, (((i % 8 = 0))) → c.column19.off i 3 = 0)
structure rc16 (inp : input_data F) (pd : public_data F) (c : columns F) (ci : columns_inter F) : Prop :=
(diff_is_bit : ∀ i: nat, (¬ (i = inp.trace_length - 1)) → ((c.column2.off i 1) - (c.column2.off i 0)) * ((c.column2.off i 1) - (c.column2.off i 0)) - ((c.column2.off i 1) - (c.column2.off i 0)) = 0)
(maximum : ∀ i: nat, ((i = inp.trace_length - 1)) → (c.column2.off i 0) - pd.rc_max = 0)
(minimum : ∀ i: nat, ((i = 0)) → (c.column2.off i 0) - pd.rc_min = 0)
(perm__init0 : ∀ i: nat, ((i = 0)) → (pd.rc16__perm__interaction_elm - (c.column2.off i 0)) * (ci.column23_inter1.off i 0) + (c.column0.off i 0) - pd.rc16__perm__interaction_elm = 0)
(perm__last : ∀ i: nat, ((i = inp.trace_length - 1)) → (ci.column23_inter1.off i 0) - pd.rc16__perm__public_memory_prod = 0)
(perm__step0 : ∀ i: nat, (¬ (i = inp.trace_length - 1)) → (pd.rc16__perm__interaction_elm - (c.column2.off i 1)) * (ci.column23_inter1.off i 1) - (pd.rc16__perm__interaction_elm - (c.column0.off i 1)) * (ci.column23_inter1.off i 0) = 0)
structure rc_builtin (inp : input_data F) (pd : public_data F) (c : columns F) : Prop :=
(addr_step : ∀ i: nat, (((i % 128 = 0)) ∧ ¬ (i = 128 * (inp.trace_length / 128 - 1))) → (c.column19.off i 230) - ((c.column19.off i 102) + 1) = 0)
(init_addr : ∀ i: nat, ((i = 0)) → (c.column19.off i 102) - pd.initial_rc_addr = 0)
(value : ∀ i: nat, (((i % 128 = 0))) → (((((((c.column0.off i 12) * offset_size + (c.column0.off i 28)) * offset_size + (c.column0.off i 44)) * offset_size + (c.column0.off i 60)) * offset_size + (c.column0.off i 76)) * offset_size + (c.column0.off i 92)) * offset_size + (c.column0.off i 108)) * offset_size + (c.column0.off i 124) - (c.column19.off i 103) = 0)
structure toplevel_constraints (inp : input_data F) (c : columns F) : Prop :=
(final_ap : ∀ i: nat, ((i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 0) - inp.final_ap = 0)
(final_fp : ∀ i: nat, ((i = 16 * (inp.trace_length / 16 - 1))) → (c.column21.off i 8) - inp.initial_ap = 0)
(final_pc : ∀ i: nat, ((i = 16 * (inp.trace_length / 16 - 1))) → (c.column19.off i 0) - inp.final_pc = 0)
(initial_ap : ∀ i: nat, ((i = 0)) → (c.column21.off i 0) - inp.initial_ap = 0)
(initial_fp : ∀ i: nat, ((i = 0)) → (c.column21.off i 8) - inp.initial_ap = 0)
(initial_pc : ∀ i: nat, ((i = 0)) → (c.column19.off i 0) - inp.initial_pc = 0)