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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
|
Require Import Crypto.Specific.CurveParameters.
Require Import Crypto.Util.LetIn.
(***
Modulus : 2^255-19
Base: 25.5
***)
Module Curve <: CurveParameters.
Definition sz : nat := 10%nat.
Definition bitwidth : Z := 32.
Definition s : Z := 2^255.
Definition c : list limb := [(1, 19)].
Definition carry_chain1 := Eval vm_compute in Some (seq 0 (pred sz)).
Definition carry_chain2 := Some [0;1]%nat.
Definition a24 := 121665%Z.
Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
:= Some (fun a b =>
(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
let '(in2_9, in2_8, in2_7, in2_6, in2_5, in2_4, in2_3, in2_2, in2_1, in2_0) := b in
dlet output_0 := in2_0 * in_0 in
dlet output_1 := in2_0 * in_1 +
in2_1 * in_0 in
dlet output_2 := 2 * in2_1 * in_1 +
in2_0 * in_2 +
in2_2 * in_0 in
dlet output_3 := in2_1 * in_2 +
in2_2 * in_1 +
in2_0 * in_3 +
in2_3 * in_0 in
dlet output_4 := in2_2 * in_2 +
2 * (in2_1 * in_3 +
in2_3 * in_1) +
in2_0 * in_4 +
in2_4 * in_0 in
dlet output_5 := in2_2 * in_3 +
in2_3 * in_2 +
in2_1 * in_4 +
in2_4 * in_1 +
in2_0 * in_5 +
in2_5 * in_0 in
dlet output_6 := 2 * (in2_3 * in_3 +
in2_1 * in_5 +
in2_5 * in_1) +
in2_2 * in_4 +
in2_4 * in_2 +
in2_0 * in_6 +
in2_6 * in_0 in
dlet output_7 := in2_3 * in_4 +
in2_4 * in_3 +
in2_2 * in_5 +
in2_5 * in_2 +
in2_1 * in_6 +
in2_6 * in_1 +
in2_0 * in_7 +
in2_7 * in_0 in
dlet output_8 := in2_4 * in_4 +
2 * (in2_3 * in_5 +
in2_5 * in_3 +
in2_1 * in_7 +
in2_7 * in_1) +
in2_2 * in_6 +
in2_6 * in_2 +
in2_0 * in_8 +
in2_8 * in_0 in
dlet output_9 := in2_4 * in_5 +
in2_5 * in_4 +
in2_3 * in_6 +
in2_6 * in_3 +
in2_2 * in_7 +
in2_7 * in_2 +
in2_1 * in_8 +
in2_8 * in_1 +
in2_0 * in_9 +
in2_9 * in_0 in
dlet output_10 := 2 * (in2_5 * in_5 +
in2_3 * in_7 +
in2_7 * in_3 +
in2_1 * in_9 +
in2_9 * in_1) +
in2_4 * in_6 +
in2_6 * in_4 +
in2_2 * in_8 +
in2_8 * in_2 in
dlet output_11 := in2_5 * in_6 +
in2_6 * in_5 +
in2_4 * in_7 +
in2_7 * in_4 +
in2_3 * in_8 +
in2_8 * in_3 +
in2_2 * in_9 +
in2_9 * in_2 in
dlet output_12 := in2_6 * in_6 +
2 * (in2_5 * in_7 +
in2_7 * in_5 +
in2_3 * in_9 +
in2_9 * in_3) +
in2_4 * in_8 +
in2_8 * in_4 in
dlet output_13 := in2_6 * in_7 +
in2_7 * in_6 +
in2_5 * in_8 +
in2_8 * in_5 +
in2_4 * in_9 +
in2_9 * in_4 in
dlet output_14 := 2 * (in2_7 * in_7 +
in2_5 * in_9 +
in2_9 * in_5) +
in2_6 * in_8 +
in2_8 * in_6 in
dlet output_15 := in2_7 * in_8 +
in2_8 * in_7 +
in2_6 * in_9 +
in2_9 * in_6 in
dlet output_16 := in2_8 * in_8 +
2 * (in2_7 * in_9 +
in2_9 * in_7) in
dlet output_17 := in2_8 * in_9 +
in2_9 * in_8 in
dlet output_18 := 2 * in2_9 * in_9 in
dlet output_8 := output_8 + output_18 << 4 in
dlet output_8 := output_8 + output_18 << 1 in
dlet output_8 := output_8 + output_18 in
dlet output_7 := output_7 + output_17 << 4 in
dlet output_7 := output_7 + output_17 << 1 in
dlet output_7 := output_7 + output_17 in
dlet output_6 := output_6 + output_16 << 4 in
dlet output_6 := output_6 + output_16 << 1 in
dlet output_6 := output_6 + output_16 in
dlet output_5 := output_5 + output_15 << 4 in
dlet output_5 := output_5 + output_15 << 1 in
dlet output_5 := output_5 + output_15 in
dlet output_4 := output_4 + output_14 << 4 in
dlet output_4 := output_4 + output_14 << 1 in
dlet output_4 := output_4 + output_14 in
dlet output_3 := output_3 + output_13 << 4 in
dlet output_3 := output_3 + output_13 << 1 in
dlet output_3 := output_3 + output_13 in
dlet output_2 := output_2 + output_12 << 4 in
dlet output_2 := output_2 + output_12 << 1 in
dlet output_2 := output_2 + output_12 in
dlet output_1 := output_1 + output_11 << 4 in
dlet output_1 := output_1 + output_11 << 1 in
dlet output_1 := output_1 + output_11 in
dlet output_0 := output_0 + output_10 << 4 in
dlet output_0 := output_0 + output_10 << 1 in
dlet output_0 := output_0 + output_10 in
(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
).
Definition square_code : option (Z^sz -> Z^sz)
:= Some (fun a =>
(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
dlet output_0 := in_0 * in_0 in
dlet output_1 := 2 * in_0 * in_1 in
dlet output_2 := 2 * (in_1 * in_1 +
in_0 * in_2) in
dlet output_3 := 2 * (in_1 * in_2 +
in_0 * in_3) in
dlet output_4 := in_2 * in_2 +
4 * in_1 * in_3 +
2 * in_0 * in_4 in
dlet output_5 := 2 * (in_2 * in_3 +
in_1 * in_4 +
in_0 * in_5) in
dlet output_6 := 2 * (in_3 * in_3 +
in_2 * in_4 +
in_0 * in_6 +
2 * in_1 * in_5) in
dlet output_7 := 2 * (in_3 * in_4 +
in_2 * in_5 +
in_1 * in_6 +
in_0 * in_7) in
dlet output_8 := in_4 * in_4 +
2 * (in_2 * in_6 +
in_0 * in_8 +
2 * (in_1 * in_7 +
in_3 * in_5)) in
dlet output_9 := 2 * (in_4 * in_5 +
in_3 * in_6 +
in_2 * in_7 +
in_1 * in_8 +
in_0 * in_9) in
dlet output_10 := 2 * (in_5 * in_5 +
in_4 * in_6 +
in_2 * in_8 +
2 * (in_3 * in_7 +
in_1 * in_9)) in
dlet output_11 := 2 * (in_5 * in_6 +
in_4 * in_7 +
in_3 * in_8 +
in_2 * in_9) in
dlet output_12 := in_6 * in_6 +
2 * (in_4 * in_8 +
2 * (in_5 * in_7 +
in_3 * in_9)) in
dlet output_13 := 2 * (in_6 * in_7 +
in_5 * in_8 +
in_4 * in_9) in
dlet output_14 := 2 * (in_7 * in_7 +
in_6 * in_8 +
2 * in_5 * in_9) in
dlet output_15 := 2 * (in_7 * in_8 +
in_6 * in_9) in
dlet output_16 := in_8 * in_8 +
4 * in_7 * in_9 in
dlet output_17 := 2 * in_8 * in_9 in
dlet output_18 := 2 * in_9 * in_9 in
dlet output_8 := output_8 + output_18 << 4 in
dlet output_8 := output_8 + output_18 << 1 in
dlet output_8 := output_8 + output_18 in
dlet output_7 := output_7 + output_17 << 4 in
dlet output_7 := output_7 + output_17 << 1 in
dlet output_7 := output_7 + output_17 in
dlet output_6 := output_6 + output_16 << 4 in
dlet output_6 := output_6 + output_16 << 1 in
dlet output_6 := output_6 + output_16 in
dlet output_5 := output_5 + output_15 << 4 in
dlet output_5 := output_5 + output_15 << 1 in
dlet output_5 := output_5 + output_15 in
dlet output_4 := output_4 + output_14 << 4 in
dlet output_4 := output_4 + output_14 << 1 in
dlet output_4 := output_4 + output_14 in
dlet output_3 := output_3 + output_13 << 4 in
dlet output_3 := output_3 + output_13 << 1 in
dlet output_3 := output_3 + output_13 in
dlet output_2 := output_2 + output_12 << 4 in
dlet output_2 := output_2 + output_12 << 1 in
dlet output_2 := output_2 + output_12 in
dlet output_1 := output_1 + output_11 << 4 in
dlet output_1 := output_1 + output_11 << 1 in
dlet output_1 := output_1 + output_11 in
dlet output_0 := output_0 + output_10 << 4 in
dlet output_0 := output_0 + output_10 << 1 in
dlet output_0 := output_0 + output_10 in
(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
).
Definition upper_bound_of_exponent : option (Z -> Z) := None.
Definition allowable_bit_widths : option (list nat) := None.
Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
Ltac extra_prove_mul_eq := idtac.
Ltac extra_prove_square_eq := idtac.
End Curve.
|
