1 #if defined(BORINGSSL_CURVE25519_64BIT)
2
3 /* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier 25519 64 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 */
4 /* curve description: 25519 */
5 /* machine_wordsize = 64 (from "64") */
6 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 */
7 /* n = 5 (from "(auto)") */
8 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */
9 /* tight_bounds_multiplier = 1 (from "") */
10 /* */
11 /* Computed values: */
12 /* carry_chain = [0, 1, 2, 3, 4, 0, 1] */
13 /* eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204) */
14 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
15 /* balance = [0xfffffffffffda, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */
16
17 #include <stdint.h>
18 typedef unsigned char fiat_25519_uint1;
19 typedef signed char fiat_25519_int1;
20 #if defined(__GNUC__) || defined(__clang__)
21 # define FIAT_25519_FIAT_EXTENSION __extension__
22 # define FIAT_25519_FIAT_INLINE __inline__
23 #else
24 # define FIAT_25519_FIAT_EXTENSION
25 # define FIAT_25519_FIAT_INLINE
26 #endif
27
28 FIAT_25519_FIAT_EXTENSION typedef int128_t fiat_25519_int128;
29 FIAT_25519_FIAT_EXTENSION typedef uint128_t fiat_25519_uint128;
30
31 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */
32 /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */
33 typedef uint64_t fiat_25519_loose_field_element[5];
34
35 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */
36 /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */
37 typedef uint64_t fiat_25519_tight_field_element[5];
38
39 #if (-1 & 3) != 3
40 #error "This code only works on a two's complement system"
41 #endif
42
43 #if !defined(FIAT_25519_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
fiat_25519_value_barrier_u64(uint64_t a)44 static __inline__ uint64_t fiat_25519_value_barrier_u64(uint64_t a) {
45 __asm__("" : "+r"(a) : /* no inputs */);
46 return a;
47 }
48 #else
49 # define fiat_25519_value_barrier_u64(x) (x)
50 #endif
51
52
53 /*
54 * The function fiat_25519_addcarryx_u51 is an addition with carry.
55 *
56 * Postconditions:
57 * out1 = (arg1 + arg2 + arg3) mod 2^51
58 * out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
59 *
60 * Input Bounds:
61 * arg1: [0x0 ~> 0x1]
62 * arg2: [0x0 ~> 0x7ffffffffffff]
63 * arg3: [0x0 ~> 0x7ffffffffffff]
64 * Output Bounds:
65 * out1: [0x0 ~> 0x7ffffffffffff]
66 * out2: [0x0 ~> 0x1]
67 */
fiat_25519_addcarryx_u51(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)68 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
69 uint64_t x1;
70 uint64_t x2;
71 fiat_25519_uint1 x3;
72 x1 = ((arg1 + arg2) + arg3);
73 x2 = (x1 & UINT64_C(0x7ffffffffffff));
74 x3 = (fiat_25519_uint1)(x1 >> 51);
75 *out1 = x2;
76 *out2 = x3;
77 }
78
79 /*
80 * The function fiat_25519_subborrowx_u51 is a subtraction with borrow.
81 *
82 * Postconditions:
83 * out1 = (-arg1 + arg2 + -arg3) mod 2^51
84 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋
85 *
86 * Input Bounds:
87 * arg1: [0x0 ~> 0x1]
88 * arg2: [0x0 ~> 0x7ffffffffffff]
89 * arg3: [0x0 ~> 0x7ffffffffffff]
90 * Output Bounds:
91 * out1: [0x0 ~> 0x7ffffffffffff]
92 * out2: [0x0 ~> 0x1]
93 */
fiat_25519_subborrowx_u51(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)94 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
95 int64_t x1;
96 fiat_25519_int1 x2;
97 uint64_t x3;
98 x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
99 x2 = (fiat_25519_int1)(x1 >> 51);
100 x3 = (x1 & UINT64_C(0x7ffffffffffff));
101 *out1 = x3;
102 *out2 = (fiat_25519_uint1)(0x0 - x2);
103 }
104
105 /*
106 * The function fiat_25519_cmovznz_u64 is a single-word conditional move.
107 *
108 * Postconditions:
109 * out1 = (if arg1 = 0 then arg2 else arg3)
110 *
111 * Input Bounds:
112 * arg1: [0x0 ~> 0x1]
113 * arg2: [0x0 ~> 0xffffffffffffffff]
114 * arg3: [0x0 ~> 0xffffffffffffffff]
115 * Output Bounds:
116 * out1: [0x0 ~> 0xffffffffffffffff]
117 */
fiat_25519_cmovznz_u64(uint64_t * out1,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)118 static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
119 fiat_25519_uint1 x1;
120 uint64_t x2;
121 uint64_t x3;
122 x1 = (!(!arg1));
123 x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
124 x3 = ((fiat_25519_value_barrier_u64(x2) & arg3) | (fiat_25519_value_barrier_u64((~x2)) & arg2));
125 *out1 = x3;
126 }
127
128 /*
129 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
130 *
131 * Postconditions:
132 * eval out1 mod m = (eval arg1 * eval arg2) mod m
133 *
134 */
fiat_25519_carry_mul(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1,const fiat_25519_loose_field_element arg2)135 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_mul(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1, const fiat_25519_loose_field_element arg2) {
136 fiat_25519_uint128 x1;
137 fiat_25519_uint128 x2;
138 fiat_25519_uint128 x3;
139 fiat_25519_uint128 x4;
140 fiat_25519_uint128 x5;
141 fiat_25519_uint128 x6;
142 fiat_25519_uint128 x7;
143 fiat_25519_uint128 x8;
144 fiat_25519_uint128 x9;
145 fiat_25519_uint128 x10;
146 fiat_25519_uint128 x11;
147 fiat_25519_uint128 x12;
148 fiat_25519_uint128 x13;
149 fiat_25519_uint128 x14;
150 fiat_25519_uint128 x15;
151 fiat_25519_uint128 x16;
152 fiat_25519_uint128 x17;
153 fiat_25519_uint128 x18;
154 fiat_25519_uint128 x19;
155 fiat_25519_uint128 x20;
156 fiat_25519_uint128 x21;
157 fiat_25519_uint128 x22;
158 fiat_25519_uint128 x23;
159 fiat_25519_uint128 x24;
160 fiat_25519_uint128 x25;
161 fiat_25519_uint128 x26;
162 uint64_t x27;
163 uint64_t x28;
164 fiat_25519_uint128 x29;
165 fiat_25519_uint128 x30;
166 fiat_25519_uint128 x31;
167 fiat_25519_uint128 x32;
168 fiat_25519_uint128 x33;
169 uint64_t x34;
170 uint64_t x35;
171 fiat_25519_uint128 x36;
172 uint64_t x37;
173 uint64_t x38;
174 fiat_25519_uint128 x39;
175 uint64_t x40;
176 uint64_t x41;
177 fiat_25519_uint128 x42;
178 uint64_t x43;
179 uint64_t x44;
180 uint64_t x45;
181 uint64_t x46;
182 uint64_t x47;
183 uint64_t x48;
184 uint64_t x49;
185 fiat_25519_uint1 x50;
186 uint64_t x51;
187 uint64_t x52;
188 x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * UINT8_C(0x13)));
189 x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * UINT8_C(0x13)));
190 x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * UINT8_C(0x13)));
191 x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * UINT8_C(0x13)));
192 x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * UINT8_C(0x13)));
193 x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * UINT8_C(0x13)));
194 x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13)));
195 x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * UINT8_C(0x13)));
196 x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13)));
197 x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13)));
198 x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0]));
199 x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1]));
200 x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0]));
201 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2]));
202 x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1]));
203 x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0]));
204 x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3]));
205 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2]));
206 x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1]));
207 x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0]));
208 x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4]));
209 x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3]));
210 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2]));
211 x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1]));
212 x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0]));
213 x26 = (x25 + (x10 + (x9 + (x7 + x4))));
214 x27 = (uint64_t)(x26 >> 51);
215 x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff));
216 x29 = (x21 + (x17 + (x14 + (x12 + x11))));
217 x30 = (x22 + (x18 + (x15 + (x13 + x1))));
218 x31 = (x23 + (x19 + (x16 + (x5 + x2))));
219 x32 = (x24 + (x20 + (x8 + (x6 + x3))));
220 x33 = (x27 + x32);
221 x34 = (uint64_t)(x33 >> 51);
222 x35 = (uint64_t)(x33 & UINT64_C(0x7ffffffffffff));
223 x36 = (x34 + x31);
224 x37 = (uint64_t)(x36 >> 51);
225 x38 = (uint64_t)(x36 & UINT64_C(0x7ffffffffffff));
226 x39 = (x37 + x30);
227 x40 = (uint64_t)(x39 >> 51);
228 x41 = (uint64_t)(x39 & UINT64_C(0x7ffffffffffff));
229 x42 = (x40 + x29);
230 x43 = (uint64_t)(x42 >> 51);
231 x44 = (uint64_t)(x42 & UINT64_C(0x7ffffffffffff));
232 x45 = (x43 * UINT8_C(0x13));
233 x46 = (x28 + x45);
234 x47 = (x46 >> 51);
235 x48 = (x46 & UINT64_C(0x7ffffffffffff));
236 x49 = (x47 + x35);
237 x50 = (fiat_25519_uint1)(x49 >> 51);
238 x51 = (x49 & UINT64_C(0x7ffffffffffff));
239 x52 = (x50 + x38);
240 out1[0] = x48;
241 out1[1] = x51;
242 out1[2] = x52;
243 out1[3] = x41;
244 out1[4] = x44;
245 }
246
247 /*
248 * The function fiat_25519_carry_square squares a field element and reduces the result.
249 *
250 * Postconditions:
251 * eval out1 mod m = (eval arg1 * eval arg1) mod m
252 *
253 */
fiat_25519_carry_square(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)254 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
255 uint64_t x1;
256 uint64_t x2;
257 uint64_t x3;
258 uint64_t x4;
259 uint64_t x5;
260 uint64_t x6;
261 uint64_t x7;
262 uint64_t x8;
263 fiat_25519_uint128 x9;
264 fiat_25519_uint128 x10;
265 fiat_25519_uint128 x11;
266 fiat_25519_uint128 x12;
267 fiat_25519_uint128 x13;
268 fiat_25519_uint128 x14;
269 fiat_25519_uint128 x15;
270 fiat_25519_uint128 x16;
271 fiat_25519_uint128 x17;
272 fiat_25519_uint128 x18;
273 fiat_25519_uint128 x19;
274 fiat_25519_uint128 x20;
275 fiat_25519_uint128 x21;
276 fiat_25519_uint128 x22;
277 fiat_25519_uint128 x23;
278 fiat_25519_uint128 x24;
279 uint64_t x25;
280 uint64_t x26;
281 fiat_25519_uint128 x27;
282 fiat_25519_uint128 x28;
283 fiat_25519_uint128 x29;
284 fiat_25519_uint128 x30;
285 fiat_25519_uint128 x31;
286 uint64_t x32;
287 uint64_t x33;
288 fiat_25519_uint128 x34;
289 uint64_t x35;
290 uint64_t x36;
291 fiat_25519_uint128 x37;
292 uint64_t x38;
293 uint64_t x39;
294 fiat_25519_uint128 x40;
295 uint64_t x41;
296 uint64_t x42;
297 uint64_t x43;
298 uint64_t x44;
299 uint64_t x45;
300 uint64_t x46;
301 uint64_t x47;
302 fiat_25519_uint1 x48;
303 uint64_t x49;
304 uint64_t x50;
305 x1 = ((arg1[4]) * UINT8_C(0x13));
306 x2 = (x1 * 0x2);
307 x3 = ((arg1[4]) * 0x2);
308 x4 = ((arg1[3]) * UINT8_C(0x13));
309 x5 = (x4 * 0x2);
310 x6 = ((arg1[3]) * 0x2);
311 x7 = ((arg1[2]) * 0x2);
312 x8 = ((arg1[1]) * 0x2);
313 x9 = ((fiat_25519_uint128)(arg1[4]) * x1);
314 x10 = ((fiat_25519_uint128)(arg1[3]) * x2);
315 x11 = ((fiat_25519_uint128)(arg1[3]) * x4);
316 x12 = ((fiat_25519_uint128)(arg1[2]) * x2);
317 x13 = ((fiat_25519_uint128)(arg1[2]) * x5);
318 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2]));
319 x15 = ((fiat_25519_uint128)(arg1[1]) * x2);
320 x16 = ((fiat_25519_uint128)(arg1[1]) * x6);
321 x17 = ((fiat_25519_uint128)(arg1[1]) * x7);
322 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1]));
323 x19 = ((fiat_25519_uint128)(arg1[0]) * x3);
324 x20 = ((fiat_25519_uint128)(arg1[0]) * x6);
325 x21 = ((fiat_25519_uint128)(arg1[0]) * x7);
326 x22 = ((fiat_25519_uint128)(arg1[0]) * x8);
327 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0]));
328 x24 = (x23 + (x15 + x13));
329 x25 = (uint64_t)(x24 >> 51);
330 x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff));
331 x27 = (x19 + (x16 + x14));
332 x28 = (x20 + (x17 + x9));
333 x29 = (x21 + (x18 + x10));
334 x30 = (x22 + (x12 + x11));
335 x31 = (x25 + x30);
336 x32 = (uint64_t)(x31 >> 51);
337 x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff));
338 x34 = (x32 + x29);
339 x35 = (uint64_t)(x34 >> 51);
340 x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff));
341 x37 = (x35 + x28);
342 x38 = (uint64_t)(x37 >> 51);
343 x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff));
344 x40 = (x38 + x27);
345 x41 = (uint64_t)(x40 >> 51);
346 x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff));
347 x43 = (x41 * UINT8_C(0x13));
348 x44 = (x26 + x43);
349 x45 = (x44 >> 51);
350 x46 = (x44 & UINT64_C(0x7ffffffffffff));
351 x47 = (x45 + x33);
352 x48 = (fiat_25519_uint1)(x47 >> 51);
353 x49 = (x47 & UINT64_C(0x7ffffffffffff));
354 x50 = (x48 + x36);
355 out1[0] = x46;
356 out1[1] = x49;
357 out1[2] = x50;
358 out1[3] = x39;
359 out1[4] = x42;
360 }
361
362 /*
363 * The function fiat_25519_carry reduces a field element.
364 *
365 * Postconditions:
366 * eval out1 mod m = eval arg1 mod m
367 *
368 */
fiat_25519_carry(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)369 static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
370 uint64_t x1;
371 uint64_t x2;
372 uint64_t x3;
373 uint64_t x4;
374 uint64_t x5;
375 uint64_t x6;
376 uint64_t x7;
377 uint64_t x8;
378 uint64_t x9;
379 uint64_t x10;
380 uint64_t x11;
381 uint64_t x12;
382 x1 = (arg1[0]);
383 x2 = ((x1 >> 51) + (arg1[1]));
384 x3 = ((x2 >> 51) + (arg1[2]));
385 x4 = ((x3 >> 51) + (arg1[3]));
386 x5 = ((x4 >> 51) + (arg1[4]));
387 x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * UINT8_C(0x13)));
388 x7 = ((fiat_25519_uint1)(x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff)));
389 x8 = (x6 & UINT64_C(0x7ffffffffffff));
390 x9 = (x7 & UINT64_C(0x7ffffffffffff));
391 x10 = ((fiat_25519_uint1)(x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff)));
392 x11 = (x4 & UINT64_C(0x7ffffffffffff));
393 x12 = (x5 & UINT64_C(0x7ffffffffffff));
394 out1[0] = x8;
395 out1[1] = x9;
396 out1[2] = x10;
397 out1[3] = x11;
398 out1[4] = x12;
399 }
400
401 /*
402 * The function fiat_25519_add adds two field elements.
403 *
404 * Postconditions:
405 * eval out1 mod m = (eval arg1 + eval arg2) mod m
406 *
407 */
fiat_25519_add(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)408 static FIAT_25519_FIAT_INLINE void fiat_25519_add(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) {
409 uint64_t x1;
410 uint64_t x2;
411 uint64_t x3;
412 uint64_t x4;
413 uint64_t x5;
414 x1 = ((arg1[0]) + (arg2[0]));
415 x2 = ((arg1[1]) + (arg2[1]));
416 x3 = ((arg1[2]) + (arg2[2]));
417 x4 = ((arg1[3]) + (arg2[3]));
418 x5 = ((arg1[4]) + (arg2[4]));
419 out1[0] = x1;
420 out1[1] = x2;
421 out1[2] = x3;
422 out1[3] = x4;
423 out1[4] = x5;
424 }
425
426 /*
427 * The function fiat_25519_sub subtracts two field elements.
428 *
429 * Postconditions:
430 * eval out1 mod m = (eval arg1 - eval arg2) mod m
431 *
432 */
fiat_25519_sub(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)433 static FIAT_25519_FIAT_INLINE void fiat_25519_sub(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) {
434 uint64_t x1;
435 uint64_t x2;
436 uint64_t x3;
437 uint64_t x4;
438 uint64_t x5;
439 x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0]));
440 x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1]));
441 x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2]));
442 x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3]));
443 x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4]));
444 out1[0] = x1;
445 out1[1] = x2;
446 out1[2] = x3;
447 out1[3] = x4;
448 out1[4] = x5;
449 }
450
451 /*
452 * The function fiat_25519_opp negates a field element.
453 *
454 * Postconditions:
455 * eval out1 mod m = -eval arg1 mod m
456 *
457 */
fiat_25519_opp(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1)458 static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) {
459 uint64_t x1;
460 uint64_t x2;
461 uint64_t x3;
462 uint64_t x4;
463 uint64_t x5;
464 x1 = (UINT64_C(0xfffffffffffda) - (arg1[0]));
465 x2 = (UINT64_C(0xffffffffffffe) - (arg1[1]));
466 x3 = (UINT64_C(0xffffffffffffe) - (arg1[2]));
467 x4 = (UINT64_C(0xffffffffffffe) - (arg1[3]));
468 x5 = (UINT64_C(0xffffffffffffe) - (arg1[4]));
469 out1[0] = x1;
470 out1[1] = x2;
471 out1[2] = x3;
472 out1[3] = x4;
473 out1[4] = x5;
474 }
475
476 /*
477 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
478 *
479 * Postconditions:
480 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
481 *
482 * Output Bounds:
483 * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
484 */
fiat_25519_to_bytes(uint8_t out1[32],const fiat_25519_tight_field_element arg1)485 static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) {
486 uint64_t x1;
487 fiat_25519_uint1 x2;
488 uint64_t x3;
489 fiat_25519_uint1 x4;
490 uint64_t x5;
491 fiat_25519_uint1 x6;
492 uint64_t x7;
493 fiat_25519_uint1 x8;
494 uint64_t x9;
495 fiat_25519_uint1 x10;
496 uint64_t x11;
497 uint64_t x12;
498 fiat_25519_uint1 x13;
499 uint64_t x14;
500 fiat_25519_uint1 x15;
501 uint64_t x16;
502 fiat_25519_uint1 x17;
503 uint64_t x18;
504 fiat_25519_uint1 x19;
505 uint64_t x20;
506 fiat_25519_uint1 x21;
507 uint64_t x22;
508 uint64_t x23;
509 uint64_t x24;
510 uint64_t x25;
511 uint8_t x26;
512 uint64_t x27;
513 uint8_t x28;
514 uint64_t x29;
515 uint8_t x30;
516 uint64_t x31;
517 uint8_t x32;
518 uint64_t x33;
519 uint8_t x34;
520 uint64_t x35;
521 uint8_t x36;
522 uint8_t x37;
523 uint64_t x38;
524 uint8_t x39;
525 uint64_t x40;
526 uint8_t x41;
527 uint64_t x42;
528 uint8_t x43;
529 uint64_t x44;
530 uint8_t x45;
531 uint64_t x46;
532 uint8_t x47;
533 uint64_t x48;
534 uint8_t x49;
535 uint8_t x50;
536 uint64_t x51;
537 uint8_t x52;
538 uint64_t x53;
539 uint8_t x54;
540 uint64_t x55;
541 uint8_t x56;
542 uint64_t x57;
543 uint8_t x58;
544 uint64_t x59;
545 uint8_t x60;
546 uint64_t x61;
547 uint8_t x62;
548 uint64_t x63;
549 uint8_t x64;
550 fiat_25519_uint1 x65;
551 uint64_t x66;
552 uint8_t x67;
553 uint64_t x68;
554 uint8_t x69;
555 uint64_t x70;
556 uint8_t x71;
557 uint64_t x72;
558 uint8_t x73;
559 uint64_t x74;
560 uint8_t x75;
561 uint64_t x76;
562 uint8_t x77;
563 uint8_t x78;
564 uint64_t x79;
565 uint8_t x80;
566 uint64_t x81;
567 uint8_t x82;
568 uint64_t x83;
569 uint8_t x84;
570 uint64_t x85;
571 uint8_t x86;
572 uint64_t x87;
573 uint8_t x88;
574 uint64_t x89;
575 uint8_t x90;
576 uint8_t x91;
577 fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed));
578 fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff));
579 fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff));
580 fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff));
581 fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff));
582 fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff));
583 fiat_25519_addcarryx_u51(&x12, &x13, 0x0, x1, (x11 & UINT64_C(0x7ffffffffffed)));
584 fiat_25519_addcarryx_u51(&x14, &x15, x13, x3, (x11 & UINT64_C(0x7ffffffffffff)));
585 fiat_25519_addcarryx_u51(&x16, &x17, x15, x5, (x11 & UINT64_C(0x7ffffffffffff)));
586 fiat_25519_addcarryx_u51(&x18, &x19, x17, x7, (x11 & UINT64_C(0x7ffffffffffff)));
587 fiat_25519_addcarryx_u51(&x20, &x21, x19, x9, (x11 & UINT64_C(0x7ffffffffffff)));
588 x22 = (x20 << 4);
589 x23 = (x18 * (uint64_t)0x2);
590 x24 = (x16 << 6);
591 x25 = (x14 << 3);
592 x26 = (uint8_t)(x12 & UINT8_C(0xff));
593 x27 = (x12 >> 8);
594 x28 = (uint8_t)(x27 & UINT8_C(0xff));
595 x29 = (x27 >> 8);
596 x30 = (uint8_t)(x29 & UINT8_C(0xff));
597 x31 = (x29 >> 8);
598 x32 = (uint8_t)(x31 & UINT8_C(0xff));
599 x33 = (x31 >> 8);
600 x34 = (uint8_t)(x33 & UINT8_C(0xff));
601 x35 = (x33 >> 8);
602 x36 = (uint8_t)(x35 & UINT8_C(0xff));
603 x37 = (uint8_t)(x35 >> 8);
604 x38 = (x25 + (uint64_t)x37);
605 x39 = (uint8_t)(x38 & UINT8_C(0xff));
606 x40 = (x38 >> 8);
607 x41 = (uint8_t)(x40 & UINT8_C(0xff));
608 x42 = (x40 >> 8);
609 x43 = (uint8_t)(x42 & UINT8_C(0xff));
610 x44 = (x42 >> 8);
611 x45 = (uint8_t)(x44 & UINT8_C(0xff));
612 x46 = (x44 >> 8);
613 x47 = (uint8_t)(x46 & UINT8_C(0xff));
614 x48 = (x46 >> 8);
615 x49 = (uint8_t)(x48 & UINT8_C(0xff));
616 x50 = (uint8_t)(x48 >> 8);
617 x51 = (x24 + (uint64_t)x50);
618 x52 = (uint8_t)(x51 & UINT8_C(0xff));
619 x53 = (x51 >> 8);
620 x54 = (uint8_t)(x53 & UINT8_C(0xff));
621 x55 = (x53 >> 8);
622 x56 = (uint8_t)(x55 & UINT8_C(0xff));
623 x57 = (x55 >> 8);
624 x58 = (uint8_t)(x57 & UINT8_C(0xff));
625 x59 = (x57 >> 8);
626 x60 = (uint8_t)(x59 & UINT8_C(0xff));
627 x61 = (x59 >> 8);
628 x62 = (uint8_t)(x61 & UINT8_C(0xff));
629 x63 = (x61 >> 8);
630 x64 = (uint8_t)(x63 & UINT8_C(0xff));
631 x65 = (fiat_25519_uint1)(x63 >> 8);
632 x66 = (x23 + (uint64_t)x65);
633 x67 = (uint8_t)(x66 & UINT8_C(0xff));
634 x68 = (x66 >> 8);
635 x69 = (uint8_t)(x68 & UINT8_C(0xff));
636 x70 = (x68 >> 8);
637 x71 = (uint8_t)(x70 & UINT8_C(0xff));
638 x72 = (x70 >> 8);
639 x73 = (uint8_t)(x72 & UINT8_C(0xff));
640 x74 = (x72 >> 8);
641 x75 = (uint8_t)(x74 & UINT8_C(0xff));
642 x76 = (x74 >> 8);
643 x77 = (uint8_t)(x76 & UINT8_C(0xff));
644 x78 = (uint8_t)(x76 >> 8);
645 x79 = (x22 + (uint64_t)x78);
646 x80 = (uint8_t)(x79 & UINT8_C(0xff));
647 x81 = (x79 >> 8);
648 x82 = (uint8_t)(x81 & UINT8_C(0xff));
649 x83 = (x81 >> 8);
650 x84 = (uint8_t)(x83 & UINT8_C(0xff));
651 x85 = (x83 >> 8);
652 x86 = (uint8_t)(x85 & UINT8_C(0xff));
653 x87 = (x85 >> 8);
654 x88 = (uint8_t)(x87 & UINT8_C(0xff));
655 x89 = (x87 >> 8);
656 x90 = (uint8_t)(x89 & UINT8_C(0xff));
657 x91 = (uint8_t)(x89 >> 8);
658 out1[0] = x26;
659 out1[1] = x28;
660 out1[2] = x30;
661 out1[3] = x32;
662 out1[4] = x34;
663 out1[5] = x36;
664 out1[6] = x39;
665 out1[7] = x41;
666 out1[8] = x43;
667 out1[9] = x45;
668 out1[10] = x47;
669 out1[11] = x49;
670 out1[12] = x52;
671 out1[13] = x54;
672 out1[14] = x56;
673 out1[15] = x58;
674 out1[16] = x60;
675 out1[17] = x62;
676 out1[18] = x64;
677 out1[19] = x67;
678 out1[20] = x69;
679 out1[21] = x71;
680 out1[22] = x73;
681 out1[23] = x75;
682 out1[24] = x77;
683 out1[25] = x80;
684 out1[26] = x82;
685 out1[27] = x84;
686 out1[28] = x86;
687 out1[29] = x88;
688 out1[30] = x90;
689 out1[31] = x91;
690 }
691
692 /*
693 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
694 *
695 * Postconditions:
696 * eval out1 mod m = bytes_eval arg1 mod m
697 *
698 * Input Bounds:
699 * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
700 */
fiat_25519_from_bytes(fiat_25519_tight_field_element out1,const uint8_t arg1[32])701 static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) {
702 uint64_t x1;
703 uint64_t x2;
704 uint64_t x3;
705 uint64_t x4;
706 uint64_t x5;
707 uint64_t x6;
708 uint64_t x7;
709 uint64_t x8;
710 uint64_t x9;
711 uint64_t x10;
712 uint64_t x11;
713 uint64_t x12;
714 uint64_t x13;
715 uint64_t x14;
716 uint64_t x15;
717 uint64_t x16;
718 uint64_t x17;
719 uint64_t x18;
720 uint64_t x19;
721 uint64_t x20;
722 uint64_t x21;
723 uint64_t x22;
724 uint64_t x23;
725 uint64_t x24;
726 uint64_t x25;
727 uint64_t x26;
728 uint64_t x27;
729 uint64_t x28;
730 uint64_t x29;
731 uint64_t x30;
732 uint64_t x31;
733 uint8_t x32;
734 uint64_t x33;
735 uint64_t x34;
736 uint64_t x35;
737 uint64_t x36;
738 uint64_t x37;
739 uint64_t x38;
740 uint64_t x39;
741 uint8_t x40;
742 uint64_t x41;
743 uint64_t x42;
744 uint64_t x43;
745 uint64_t x44;
746 uint64_t x45;
747 uint64_t x46;
748 uint64_t x47;
749 uint8_t x48;
750 uint64_t x49;
751 uint64_t x50;
752 uint64_t x51;
753 uint64_t x52;
754 uint64_t x53;
755 uint64_t x54;
756 uint64_t x55;
757 uint64_t x56;
758 uint8_t x57;
759 uint64_t x58;
760 uint64_t x59;
761 uint64_t x60;
762 uint64_t x61;
763 uint64_t x62;
764 uint64_t x63;
765 uint64_t x64;
766 uint8_t x65;
767 uint64_t x66;
768 uint64_t x67;
769 uint64_t x68;
770 uint64_t x69;
771 uint64_t x70;
772 uint64_t x71;
773 x1 = ((uint64_t)(arg1[31]) << 44);
774 x2 = ((uint64_t)(arg1[30]) << 36);
775 x3 = ((uint64_t)(arg1[29]) << 28);
776 x4 = ((uint64_t)(arg1[28]) << 20);
777 x5 = ((uint64_t)(arg1[27]) << 12);
778 x6 = ((uint64_t)(arg1[26]) << 4);
779 x7 = ((uint64_t)(arg1[25]) << 47);
780 x8 = ((uint64_t)(arg1[24]) << 39);
781 x9 = ((uint64_t)(arg1[23]) << 31);
782 x10 = ((uint64_t)(arg1[22]) << 23);
783 x11 = ((uint64_t)(arg1[21]) << 15);
784 x12 = ((uint64_t)(arg1[20]) << 7);
785 x13 = ((uint64_t)(arg1[19]) << 50);
786 x14 = ((uint64_t)(arg1[18]) << 42);
787 x15 = ((uint64_t)(arg1[17]) << 34);
788 x16 = ((uint64_t)(arg1[16]) << 26);
789 x17 = ((uint64_t)(arg1[15]) << 18);
790 x18 = ((uint64_t)(arg1[14]) << 10);
791 x19 = ((uint64_t)(arg1[13]) << 2);
792 x20 = ((uint64_t)(arg1[12]) << 45);
793 x21 = ((uint64_t)(arg1[11]) << 37);
794 x22 = ((uint64_t)(arg1[10]) << 29);
795 x23 = ((uint64_t)(arg1[9]) << 21);
796 x24 = ((uint64_t)(arg1[8]) << 13);
797 x25 = ((uint64_t)(arg1[7]) << 5);
798 x26 = ((uint64_t)(arg1[6]) << 48);
799 x27 = ((uint64_t)(arg1[5]) << 40);
800 x28 = ((uint64_t)(arg1[4]) << 32);
801 x29 = ((uint64_t)(arg1[3]) << 24);
802 x30 = ((uint64_t)(arg1[2]) << 16);
803 x31 = ((uint64_t)(arg1[1]) << 8);
804 x32 = (arg1[0]);
805 x33 = (x31 + (uint64_t)x32);
806 x34 = (x30 + x33);
807 x35 = (x29 + x34);
808 x36 = (x28 + x35);
809 x37 = (x27 + x36);
810 x38 = (x26 + x37);
811 x39 = (x38 & UINT64_C(0x7ffffffffffff));
812 x40 = (uint8_t)(x38 >> 51);
813 x41 = (x25 + (uint64_t)x40);
814 x42 = (x24 + x41);
815 x43 = (x23 + x42);
816 x44 = (x22 + x43);
817 x45 = (x21 + x44);
818 x46 = (x20 + x45);
819 x47 = (x46 & UINT64_C(0x7ffffffffffff));
820 x48 = (uint8_t)(x46 >> 51);
821 x49 = (x19 + (uint64_t)x48);
822 x50 = (x18 + x49);
823 x51 = (x17 + x50);
824 x52 = (x16 + x51);
825 x53 = (x15 + x52);
826 x54 = (x14 + x53);
827 x55 = (x13 + x54);
828 x56 = (x55 & UINT64_C(0x7ffffffffffff));
829 x57 = (uint8_t)(x55 >> 51);
830 x58 = (x12 + (uint64_t)x57);
831 x59 = (x11 + x58);
832 x60 = (x10 + x59);
833 x61 = (x9 + x60);
834 x62 = (x8 + x61);
835 x63 = (x7 + x62);
836 x64 = (x63 & UINT64_C(0x7ffffffffffff));
837 x65 = (uint8_t)(x63 >> 51);
838 x66 = (x6 + (uint64_t)x65);
839 x67 = (x5 + x66);
840 x68 = (x4 + x67);
841 x69 = (x3 + x68);
842 x70 = (x2 + x69);
843 x71 = (x1 + x70);
844 out1[0] = x39;
845 out1[1] = x47;
846 out1[2] = x56;
847 out1[3] = x64;
848 out1[4] = x71;
849 }
850
851 #else /* defined(BORINGSSL_CURVE25519_64BIT) */
852
853 /* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier 25519 32 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 */
854 /* curve description: 25519 */
855 /* machine_wordsize = 32 (from "32") */
856 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 */
857 /* n = 10 (from "(auto)") */
858 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */
859 /* tight_bounds_multiplier = 1 (from "") */
860 /* */
861 /* Computed values: */
862 /* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */
863 /* eval z = z[0] + (z[1] << 26) + (z[2] << 51) + (z[3] << 77) + (z[4] << 102) + (z[5] << 128) + (z[6] << 153) + (z[7] << 179) + (z[8] << 204) + (z[9] << 230) */
864 /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
865 /* balance = [0x7ffffda, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe, 0x7fffffe, 0x3fffffe] */
866
867 #include <stdint.h>
868 typedef unsigned char fiat_25519_uint1;
869 typedef signed char fiat_25519_int1;
870 #if defined(__GNUC__) || defined(__clang__)
871 # define FIAT_25519_FIAT_INLINE __inline__
872 #else
873 # define FIAT_25519_FIAT_INLINE
874 #endif
875
876 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */
877 /* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */
878 typedef uint32_t fiat_25519_loose_field_element[10];
879
880 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */
881 /* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */
882 typedef uint32_t fiat_25519_tight_field_element[10];
883
884 #if (-1 & 3) != 3
885 #error "This code only works on a two's complement system"
886 #endif
887
888 #if !defined(FIAT_25519_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
fiat_25519_value_barrier_u32(uint32_t a)889 static __inline__ uint32_t fiat_25519_value_barrier_u32(uint32_t a) {
890 __asm__("" : "+r"(a) : /* no inputs */);
891 return a;
892 }
893 #else
894 # define fiat_25519_value_barrier_u32(x) (x)
895 #endif
896
897
898 /*
899 * The function fiat_25519_addcarryx_u26 is an addition with carry.
900 *
901 * Postconditions:
902 * out1 = (arg1 + arg2 + arg3) mod 2^26
903 * out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋
904 *
905 * Input Bounds:
906 * arg1: [0x0 ~> 0x1]
907 * arg2: [0x0 ~> 0x3ffffff]
908 * arg3: [0x0 ~> 0x3ffffff]
909 * Output Bounds:
910 * out1: [0x0 ~> 0x3ffffff]
911 * out2: [0x0 ~> 0x1]
912 */
fiat_25519_addcarryx_u26(uint32_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint32_t arg2,uint32_t arg3)913 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
914 uint32_t x1;
915 uint32_t x2;
916 fiat_25519_uint1 x3;
917 x1 = ((arg1 + arg2) + arg3);
918 x2 = (x1 & UINT32_C(0x3ffffff));
919 x3 = (fiat_25519_uint1)(x1 >> 26);
920 *out1 = x2;
921 *out2 = x3;
922 }
923
924 /*
925 * The function fiat_25519_subborrowx_u26 is a subtraction with borrow.
926 *
927 * Postconditions:
928 * out1 = (-arg1 + arg2 + -arg3) mod 2^26
929 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋
930 *
931 * Input Bounds:
932 * arg1: [0x0 ~> 0x1]
933 * arg2: [0x0 ~> 0x3ffffff]
934 * arg3: [0x0 ~> 0x3ffffff]
935 * Output Bounds:
936 * out1: [0x0 ~> 0x3ffffff]
937 * out2: [0x0 ~> 0x1]
938 */
fiat_25519_subborrowx_u26(uint32_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint32_t arg2,uint32_t arg3)939 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
940 int32_t x1;
941 fiat_25519_int1 x2;
942 uint32_t x3;
943 x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
944 x2 = (fiat_25519_int1)(x1 >> 26);
945 x3 = (x1 & UINT32_C(0x3ffffff));
946 *out1 = x3;
947 *out2 = (fiat_25519_uint1)(0x0 - x2);
948 }
949
950 /*
951 * The function fiat_25519_addcarryx_u25 is an addition with carry.
952 *
953 * Postconditions:
954 * out1 = (arg1 + arg2 + arg3) mod 2^25
955 * out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋
956 *
957 * Input Bounds:
958 * arg1: [0x0 ~> 0x1]
959 * arg2: [0x0 ~> 0x1ffffff]
960 * arg3: [0x0 ~> 0x1ffffff]
961 * Output Bounds:
962 * out1: [0x0 ~> 0x1ffffff]
963 * out2: [0x0 ~> 0x1]
964 */
fiat_25519_addcarryx_u25(uint32_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint32_t arg2,uint32_t arg3)965 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
966 uint32_t x1;
967 uint32_t x2;
968 fiat_25519_uint1 x3;
969 x1 = ((arg1 + arg2) + arg3);
970 x2 = (x1 & UINT32_C(0x1ffffff));
971 x3 = (fiat_25519_uint1)(x1 >> 25);
972 *out1 = x2;
973 *out2 = x3;
974 }
975
976 /*
977 * The function fiat_25519_subborrowx_u25 is a subtraction with borrow.
978 *
979 * Postconditions:
980 * out1 = (-arg1 + arg2 + -arg3) mod 2^25
981 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋
982 *
983 * Input Bounds:
984 * arg1: [0x0 ~> 0x1]
985 * arg2: [0x0 ~> 0x1ffffff]
986 * arg3: [0x0 ~> 0x1ffffff]
987 * Output Bounds:
988 * out1: [0x0 ~> 0x1ffffff]
989 * out2: [0x0 ~> 0x1]
990 */
fiat_25519_subborrowx_u25(uint32_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint32_t arg2,uint32_t arg3)991 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
992 int32_t x1;
993 fiat_25519_int1 x2;
994 uint32_t x3;
995 x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
996 x2 = (fiat_25519_int1)(x1 >> 25);
997 x3 = (x1 & UINT32_C(0x1ffffff));
998 *out1 = x3;
999 *out2 = (fiat_25519_uint1)(0x0 - x2);
1000 }
1001
1002 /*
1003 * The function fiat_25519_cmovznz_u32 is a single-word conditional move.
1004 *
1005 * Postconditions:
1006 * out1 = (if arg1 = 0 then arg2 else arg3)
1007 *
1008 * Input Bounds:
1009 * arg1: [0x0 ~> 0x1]
1010 * arg2: [0x0 ~> 0xffffffff]
1011 * arg3: [0x0 ~> 0xffffffff]
1012 * Output Bounds:
1013 * out1: [0x0 ~> 0xffffffff]
1014 */
fiat_25519_cmovznz_u32(uint32_t * out1,fiat_25519_uint1 arg1,uint32_t arg2,uint32_t arg3)1015 static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
1016 fiat_25519_uint1 x1;
1017 uint32_t x2;
1018 uint32_t x3;
1019 x1 = (!(!arg1));
1020 x2 = ((fiat_25519_int1)(0x0 - x1) & UINT32_C(0xffffffff));
1021 x3 = ((fiat_25519_value_barrier_u32(x2) & arg3) | (fiat_25519_value_barrier_u32((~x2)) & arg2));
1022 *out1 = x3;
1023 }
1024
1025 /*
1026 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
1027 *
1028 * Postconditions:
1029 * eval out1 mod m = (eval arg1 * eval arg2) mod m
1030 *
1031 */
fiat_25519_carry_mul(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1,const fiat_25519_loose_field_element arg2)1032 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_mul(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1, const fiat_25519_loose_field_element arg2) {
1033 uint64_t x1;
1034 uint64_t x2;
1035 uint64_t x3;
1036 uint64_t x4;
1037 uint64_t x5;
1038 uint64_t x6;
1039 uint64_t x7;
1040 uint64_t x8;
1041 uint64_t x9;
1042 uint64_t x10;
1043 uint64_t x11;
1044 uint64_t x12;
1045 uint64_t x13;
1046 uint64_t x14;
1047 uint64_t x15;
1048 uint64_t x16;
1049 uint64_t x17;
1050 uint64_t x18;
1051 uint64_t x19;
1052 uint64_t x20;
1053 uint64_t x21;
1054 uint64_t x22;
1055 uint64_t x23;
1056 uint64_t x24;
1057 uint64_t x25;
1058 uint64_t x26;
1059 uint64_t x27;
1060 uint64_t x28;
1061 uint64_t x29;
1062 uint64_t x30;
1063 uint64_t x31;
1064 uint64_t x32;
1065 uint64_t x33;
1066 uint64_t x34;
1067 uint64_t x35;
1068 uint64_t x36;
1069 uint64_t x37;
1070 uint64_t x38;
1071 uint64_t x39;
1072 uint64_t x40;
1073 uint64_t x41;
1074 uint64_t x42;
1075 uint64_t x43;
1076 uint64_t x44;
1077 uint64_t x45;
1078 uint64_t x46;
1079 uint64_t x47;
1080 uint64_t x48;
1081 uint64_t x49;
1082 uint64_t x50;
1083 uint64_t x51;
1084 uint64_t x52;
1085 uint64_t x53;
1086 uint64_t x54;
1087 uint64_t x55;
1088 uint64_t x56;
1089 uint64_t x57;
1090 uint64_t x58;
1091 uint64_t x59;
1092 uint64_t x60;
1093 uint64_t x61;
1094 uint64_t x62;
1095 uint64_t x63;
1096 uint64_t x64;
1097 uint64_t x65;
1098 uint64_t x66;
1099 uint64_t x67;
1100 uint64_t x68;
1101 uint64_t x69;
1102 uint64_t x70;
1103 uint64_t x71;
1104 uint64_t x72;
1105 uint64_t x73;
1106 uint64_t x74;
1107 uint64_t x75;
1108 uint64_t x76;
1109 uint64_t x77;
1110 uint64_t x78;
1111 uint64_t x79;
1112 uint64_t x80;
1113 uint64_t x81;
1114 uint64_t x82;
1115 uint64_t x83;
1116 uint64_t x84;
1117 uint64_t x85;
1118 uint64_t x86;
1119 uint64_t x87;
1120 uint64_t x88;
1121 uint64_t x89;
1122 uint64_t x90;
1123 uint64_t x91;
1124 uint64_t x92;
1125 uint64_t x93;
1126 uint64_t x94;
1127 uint64_t x95;
1128 uint64_t x96;
1129 uint64_t x97;
1130 uint64_t x98;
1131 uint64_t x99;
1132 uint64_t x100;
1133 uint64_t x101;
1134 uint64_t x102;
1135 uint32_t x103;
1136 uint64_t x104;
1137 uint64_t x105;
1138 uint64_t x106;
1139 uint64_t x107;
1140 uint64_t x108;
1141 uint64_t x109;
1142 uint64_t x110;
1143 uint64_t x111;
1144 uint64_t x112;
1145 uint64_t x113;
1146 uint64_t x114;
1147 uint32_t x115;
1148 uint64_t x116;
1149 uint64_t x117;
1150 uint32_t x118;
1151 uint64_t x119;
1152 uint64_t x120;
1153 uint32_t x121;
1154 uint64_t x122;
1155 uint64_t x123;
1156 uint32_t x124;
1157 uint64_t x125;
1158 uint64_t x126;
1159 uint32_t x127;
1160 uint64_t x128;
1161 uint64_t x129;
1162 uint32_t x130;
1163 uint64_t x131;
1164 uint64_t x132;
1165 uint32_t x133;
1166 uint64_t x134;
1167 uint64_t x135;
1168 uint32_t x136;
1169 uint64_t x137;
1170 uint64_t x138;
1171 uint32_t x139;
1172 uint64_t x140;
1173 uint64_t x141;
1174 uint32_t x142;
1175 uint32_t x143;
1176 uint32_t x144;
1177 fiat_25519_uint1 x145;
1178 uint32_t x146;
1179 uint32_t x147;
1180 x1 = ((uint64_t)(arg1[9]) * ((arg2[9]) * UINT8_C(0x26)));
1181 x2 = ((uint64_t)(arg1[9]) * ((arg2[8]) * UINT8_C(0x13)));
1182 x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * UINT8_C(0x26)));
1183 x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * UINT8_C(0x13)));
1184 x5 = ((uint64_t)(arg1[9]) * ((arg2[5]) * UINT8_C(0x26)));
1185 x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * UINT8_C(0x13)));
1186 x7 = ((uint64_t)(arg1[9]) * ((arg2[3]) * UINT8_C(0x26)));
1187 x8 = ((uint64_t)(arg1[9]) * ((arg2[2]) * UINT8_C(0x13)));
1188 x9 = ((uint64_t)(arg1[9]) * ((arg2[1]) * UINT8_C(0x26)));
1189 x10 = ((uint64_t)(arg1[8]) * ((arg2[9]) * UINT8_C(0x13)));
1190 x11 = ((uint64_t)(arg1[8]) * ((arg2[8]) * UINT8_C(0x13)));
1191 x12 = ((uint64_t)(arg1[8]) * ((arg2[7]) * UINT8_C(0x13)));
1192 x13 = ((uint64_t)(arg1[8]) * ((arg2[6]) * UINT8_C(0x13)));
1193 x14 = ((uint64_t)(arg1[8]) * ((arg2[5]) * UINT8_C(0x13)));
1194 x15 = ((uint64_t)(arg1[8]) * ((arg2[4]) * UINT8_C(0x13)));
1195 x16 = ((uint64_t)(arg1[8]) * ((arg2[3]) * UINT8_C(0x13)));
1196 x17 = ((uint64_t)(arg1[8]) * ((arg2[2]) * UINT8_C(0x13)));
1197 x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * UINT8_C(0x26)));
1198 x19 = ((uint64_t)(arg1[7]) * ((arg2[8]) * UINT8_C(0x13)));
1199 x20 = ((uint64_t)(arg1[7]) * ((arg2[7]) * UINT8_C(0x26)));
1200 x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * UINT8_C(0x13)));
1201 x22 = ((uint64_t)(arg1[7]) * ((arg2[5]) * UINT8_C(0x26)));
1202 x23 = ((uint64_t)(arg1[7]) * ((arg2[4]) * UINT8_C(0x13)));
1203 x24 = ((uint64_t)(arg1[7]) * ((arg2[3]) * UINT8_C(0x26)));
1204 x25 = ((uint64_t)(arg1[6]) * ((arg2[9]) * UINT8_C(0x13)));
1205 x26 = ((uint64_t)(arg1[6]) * ((arg2[8]) * UINT8_C(0x13)));
1206 x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * UINT8_C(0x13)));
1207 x28 = ((uint64_t)(arg1[6]) * ((arg2[6]) * UINT8_C(0x13)));
1208 x29 = ((uint64_t)(arg1[6]) * ((arg2[5]) * UINT8_C(0x13)));
1209 x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * UINT8_C(0x13)));
1210 x31 = ((uint64_t)(arg1[5]) * ((arg2[9]) * UINT8_C(0x26)));
1211 x32 = ((uint64_t)(arg1[5]) * ((arg2[8]) * UINT8_C(0x13)));
1212 x33 = ((uint64_t)(arg1[5]) * ((arg2[7]) * UINT8_C(0x26)));
1213 x34 = ((uint64_t)(arg1[5]) * ((arg2[6]) * UINT8_C(0x13)));
1214 x35 = ((uint64_t)(arg1[5]) * ((arg2[5]) * UINT8_C(0x26)));
1215 x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * UINT8_C(0x13)));
1216 x37 = ((uint64_t)(arg1[4]) * ((arg2[8]) * UINT8_C(0x13)));
1217 x38 = ((uint64_t)(arg1[4]) * ((arg2[7]) * UINT8_C(0x13)));
1218 x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * UINT8_C(0x13)));
1219 x40 = ((uint64_t)(arg1[3]) * ((arg2[9]) * UINT8_C(0x26)));
1220 x41 = ((uint64_t)(arg1[3]) * ((arg2[8]) * UINT8_C(0x13)));
1221 x42 = ((uint64_t)(arg1[3]) * ((arg2[7]) * UINT8_C(0x26)));
1222 x43 = ((uint64_t)(arg1[2]) * ((arg2[9]) * UINT8_C(0x13)));
1223 x44 = ((uint64_t)(arg1[2]) * ((arg2[8]) * UINT8_C(0x13)));
1224 x45 = ((uint64_t)(arg1[1]) * ((arg2[9]) * UINT8_C(0x26)));
1225 x46 = ((uint64_t)(arg1[9]) * (arg2[0]));
1226 x47 = ((uint64_t)(arg1[8]) * (arg2[1]));
1227 x48 = ((uint64_t)(arg1[8]) * (arg2[0]));
1228 x49 = ((uint64_t)(arg1[7]) * (arg2[2]));
1229 x50 = ((uint64_t)(arg1[7]) * ((arg2[1]) * 0x2));
1230 x51 = ((uint64_t)(arg1[7]) * (arg2[0]));
1231 x52 = ((uint64_t)(arg1[6]) * (arg2[3]));
1232 x53 = ((uint64_t)(arg1[6]) * (arg2[2]));
1233 x54 = ((uint64_t)(arg1[6]) * (arg2[1]));
1234 x55 = ((uint64_t)(arg1[6]) * (arg2[0]));
1235 x56 = ((uint64_t)(arg1[5]) * (arg2[4]));
1236 x57 = ((uint64_t)(arg1[5]) * ((arg2[3]) * 0x2));
1237 x58 = ((uint64_t)(arg1[5]) * (arg2[2]));
1238 x59 = ((uint64_t)(arg1[5]) * ((arg2[1]) * 0x2));
1239 x60 = ((uint64_t)(arg1[5]) * (arg2[0]));
1240 x61 = ((uint64_t)(arg1[4]) * (arg2[5]));
1241 x62 = ((uint64_t)(arg1[4]) * (arg2[4]));
1242 x63 = ((uint64_t)(arg1[4]) * (arg2[3]));
1243 x64 = ((uint64_t)(arg1[4]) * (arg2[2]));
1244 x65 = ((uint64_t)(arg1[4]) * (arg2[1]));
1245 x66 = ((uint64_t)(arg1[4]) * (arg2[0]));
1246 x67 = ((uint64_t)(arg1[3]) * (arg2[6]));
1247 x68 = ((uint64_t)(arg1[3]) * ((arg2[5]) * 0x2));
1248 x69 = ((uint64_t)(arg1[3]) * (arg2[4]));
1249 x70 = ((uint64_t)(arg1[3]) * ((arg2[3]) * 0x2));
1250 x71 = ((uint64_t)(arg1[3]) * (arg2[2]));
1251 x72 = ((uint64_t)(arg1[3]) * ((arg2[1]) * 0x2));
1252 x73 = ((uint64_t)(arg1[3]) * (arg2[0]));
1253 x74 = ((uint64_t)(arg1[2]) * (arg2[7]));
1254 x75 = ((uint64_t)(arg1[2]) * (arg2[6]));
1255 x76 = ((uint64_t)(arg1[2]) * (arg2[5]));
1256 x77 = ((uint64_t)(arg1[2]) * (arg2[4]));
1257 x78 = ((uint64_t)(arg1[2]) * (arg2[3]));
1258 x79 = ((uint64_t)(arg1[2]) * (arg2[2]));
1259 x80 = ((uint64_t)(arg1[2]) * (arg2[1]));
1260 x81 = ((uint64_t)(arg1[2]) * (arg2[0]));
1261 x82 = ((uint64_t)(arg1[1]) * (arg2[8]));
1262 x83 = ((uint64_t)(arg1[1]) * ((arg2[7]) * 0x2));
1263 x84 = ((uint64_t)(arg1[1]) * (arg2[6]));
1264 x85 = ((uint64_t)(arg1[1]) * ((arg2[5]) * 0x2));
1265 x86 = ((uint64_t)(arg1[1]) * (arg2[4]));
1266 x87 = ((uint64_t)(arg1[1]) * ((arg2[3]) * 0x2));
1267 x88 = ((uint64_t)(arg1[1]) * (arg2[2]));
1268 x89 = ((uint64_t)(arg1[1]) * ((arg2[1]) * 0x2));
1269 x90 = ((uint64_t)(arg1[1]) * (arg2[0]));
1270 x91 = ((uint64_t)(arg1[0]) * (arg2[9]));
1271 x92 = ((uint64_t)(arg1[0]) * (arg2[8]));
1272 x93 = ((uint64_t)(arg1[0]) * (arg2[7]));
1273 x94 = ((uint64_t)(arg1[0]) * (arg2[6]));
1274 x95 = ((uint64_t)(arg1[0]) * (arg2[5]));
1275 x96 = ((uint64_t)(arg1[0]) * (arg2[4]));
1276 x97 = ((uint64_t)(arg1[0]) * (arg2[3]));
1277 x98 = ((uint64_t)(arg1[0]) * (arg2[2]));
1278 x99 = ((uint64_t)(arg1[0]) * (arg2[1]));
1279 x100 = ((uint64_t)(arg1[0]) * (arg2[0]));
1280 x101 = (x100 + (x45 + (x44 + (x42 + (x39 + (x35 + (x30 + (x24 + (x17 + x9)))))))));
1281 x102 = (x101 >> 26);
1282 x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff));
1283 x104 = (x91 + (x82 + (x74 + (x67 + (x61 + (x56 + (x52 + (x49 + (x47 + x46)))))))));
1284 x105 = (x92 + (x83 + (x75 + (x68 + (x62 + (x57 + (x53 + (x50 + (x48 + x1)))))))));
1285 x106 = (x93 + (x84 + (x76 + (x69 + (x63 + (x58 + (x54 + (x51 + (x10 + x2)))))))));
1286 x107 = (x94 + (x85 + (x77 + (x70 + (x64 + (x59 + (x55 + (x18 + (x11 + x3)))))))));
1287 x108 = (x95 + (x86 + (x78 + (x71 + (x65 + (x60 + (x25 + (x19 + (x12 + x4)))))))));
1288 x109 = (x96 + (x87 + (x79 + (x72 + (x66 + (x31 + (x26 + (x20 + (x13 + x5)))))))));
1289 x110 = (x97 + (x88 + (x80 + (x73 + (x36 + (x32 + (x27 + (x21 + (x14 + x6)))))))));
1290 x111 = (x98 + (x89 + (x81 + (x40 + (x37 + (x33 + (x28 + (x22 + (x15 + x7)))))))));
1291 x112 = (x99 + (x90 + (x43 + (x41 + (x38 + (x34 + (x29 + (x23 + (x16 + x8)))))))));
1292 x113 = (x102 + x112);
1293 x114 = (x113 >> 25);
1294 x115 = (uint32_t)(x113 & UINT32_C(0x1ffffff));
1295 x116 = (x114 + x111);
1296 x117 = (x116 >> 26);
1297 x118 = (uint32_t)(x116 & UINT32_C(0x3ffffff));
1298 x119 = (x117 + x110);
1299 x120 = (x119 >> 25);
1300 x121 = (uint32_t)(x119 & UINT32_C(0x1ffffff));
1301 x122 = (x120 + x109);
1302 x123 = (x122 >> 26);
1303 x124 = (uint32_t)(x122 & UINT32_C(0x3ffffff));
1304 x125 = (x123 + x108);
1305 x126 = (x125 >> 25);
1306 x127 = (uint32_t)(x125 & UINT32_C(0x1ffffff));
1307 x128 = (x126 + x107);
1308 x129 = (x128 >> 26);
1309 x130 = (uint32_t)(x128 & UINT32_C(0x3ffffff));
1310 x131 = (x129 + x106);
1311 x132 = (x131 >> 25);
1312 x133 = (uint32_t)(x131 & UINT32_C(0x1ffffff));
1313 x134 = (x132 + x105);
1314 x135 = (x134 >> 26);
1315 x136 = (uint32_t)(x134 & UINT32_C(0x3ffffff));
1316 x137 = (x135 + x104);
1317 x138 = (x137 >> 25);
1318 x139 = (uint32_t)(x137 & UINT32_C(0x1ffffff));
1319 x140 = (x138 * UINT8_C(0x13));
1320 x141 = (x103 + x140);
1321 x142 = (uint32_t)(x141 >> 26);
1322 x143 = (uint32_t)(x141 & UINT32_C(0x3ffffff));
1323 x144 = (x142 + x115);
1324 x145 = (fiat_25519_uint1)(x144 >> 25);
1325 x146 = (x144 & UINT32_C(0x1ffffff));
1326 x147 = (x145 + x118);
1327 out1[0] = x143;
1328 out1[1] = x146;
1329 out1[2] = x147;
1330 out1[3] = x121;
1331 out1[4] = x124;
1332 out1[5] = x127;
1333 out1[6] = x130;
1334 out1[7] = x133;
1335 out1[8] = x136;
1336 out1[9] = x139;
1337 }
1338
1339 /*
1340 * The function fiat_25519_carry_square squares a field element and reduces the result.
1341 *
1342 * Postconditions:
1343 * eval out1 mod m = (eval arg1 * eval arg1) mod m
1344 *
1345 */
fiat_25519_carry_square(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)1346 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
1347 uint32_t x1;
1348 uint32_t x2;
1349 uint32_t x3;
1350 uint32_t x4;
1351 uint64_t x5;
1352 uint32_t x6;
1353 uint32_t x7;
1354 uint32_t x8;
1355 uint32_t x9;
1356 uint32_t x10;
1357 uint64_t x11;
1358 uint32_t x12;
1359 uint32_t x13;
1360 uint32_t x14;
1361 uint32_t x15;
1362 uint32_t x16;
1363 uint32_t x17;
1364 uint32_t x18;
1365 uint64_t x19;
1366 uint64_t x20;
1367 uint64_t x21;
1368 uint64_t x22;
1369 uint64_t x23;
1370 uint64_t x24;
1371 uint64_t x25;
1372 uint64_t x26;
1373 uint64_t x27;
1374 uint64_t x28;
1375 uint64_t x29;
1376 uint64_t x30;
1377 uint64_t x31;
1378 uint64_t x32;
1379 uint64_t x33;
1380 uint64_t x34;
1381 uint64_t x35;
1382 uint64_t x36;
1383 uint64_t x37;
1384 uint64_t x38;
1385 uint64_t x39;
1386 uint64_t x40;
1387 uint64_t x41;
1388 uint64_t x42;
1389 uint64_t x43;
1390 uint64_t x44;
1391 uint64_t x45;
1392 uint64_t x46;
1393 uint64_t x47;
1394 uint64_t x48;
1395 uint64_t x49;
1396 uint64_t x50;
1397 uint64_t x51;
1398 uint64_t x52;
1399 uint64_t x53;
1400 uint64_t x54;
1401 uint64_t x55;
1402 uint64_t x56;
1403 uint64_t x57;
1404 uint64_t x58;
1405 uint64_t x59;
1406 uint64_t x60;
1407 uint64_t x61;
1408 uint64_t x62;
1409 uint64_t x63;
1410 uint64_t x64;
1411 uint64_t x65;
1412 uint64_t x66;
1413 uint64_t x67;
1414 uint64_t x68;
1415 uint64_t x69;
1416 uint64_t x70;
1417 uint64_t x71;
1418 uint64_t x72;
1419 uint64_t x73;
1420 uint64_t x74;
1421 uint64_t x75;
1422 uint32_t x76;
1423 uint64_t x77;
1424 uint64_t x78;
1425 uint64_t x79;
1426 uint64_t x80;
1427 uint64_t x81;
1428 uint64_t x82;
1429 uint64_t x83;
1430 uint64_t x84;
1431 uint64_t x85;
1432 uint64_t x86;
1433 uint64_t x87;
1434 uint32_t x88;
1435 uint64_t x89;
1436 uint64_t x90;
1437 uint32_t x91;
1438 uint64_t x92;
1439 uint64_t x93;
1440 uint32_t x94;
1441 uint64_t x95;
1442 uint64_t x96;
1443 uint32_t x97;
1444 uint64_t x98;
1445 uint64_t x99;
1446 uint32_t x100;
1447 uint64_t x101;
1448 uint64_t x102;
1449 uint32_t x103;
1450 uint64_t x104;
1451 uint64_t x105;
1452 uint32_t x106;
1453 uint64_t x107;
1454 uint64_t x108;
1455 uint32_t x109;
1456 uint64_t x110;
1457 uint64_t x111;
1458 uint32_t x112;
1459 uint64_t x113;
1460 uint64_t x114;
1461 uint32_t x115;
1462 uint32_t x116;
1463 uint32_t x117;
1464 fiat_25519_uint1 x118;
1465 uint32_t x119;
1466 uint32_t x120;
1467 x1 = ((arg1[9]) * UINT8_C(0x13));
1468 x2 = (x1 * 0x2);
1469 x3 = ((arg1[9]) * 0x2);
1470 x4 = ((arg1[8]) * UINT8_C(0x13));
1471 x5 = ((uint64_t)x4 * 0x2);
1472 x6 = ((arg1[8]) * 0x2);
1473 x7 = ((arg1[7]) * UINT8_C(0x13));
1474 x8 = (x7 * 0x2);
1475 x9 = ((arg1[7]) * 0x2);
1476 x10 = ((arg1[6]) * UINT8_C(0x13));
1477 x11 = ((uint64_t)x10 * 0x2);
1478 x12 = ((arg1[6]) * 0x2);
1479 x13 = ((arg1[5]) * UINT8_C(0x13));
1480 x14 = ((arg1[5]) * 0x2);
1481 x15 = ((arg1[4]) * 0x2);
1482 x16 = ((arg1[3]) * 0x2);
1483 x17 = ((arg1[2]) * 0x2);
1484 x18 = ((arg1[1]) * 0x2);
1485 x19 = ((uint64_t)(arg1[9]) * (x1 * 0x2));
1486 x20 = ((uint64_t)(arg1[8]) * x2);
1487 x21 = ((uint64_t)(arg1[8]) * x4);
1488 x22 = ((arg1[7]) * ((uint64_t)x2 * 0x2));
1489 x23 = ((arg1[7]) * x5);
1490 x24 = ((uint64_t)(arg1[7]) * (x7 * 0x2));
1491 x25 = ((uint64_t)(arg1[6]) * x2);
1492 x26 = ((arg1[6]) * x5);
1493 x27 = ((uint64_t)(arg1[6]) * x8);
1494 x28 = ((uint64_t)(arg1[6]) * x10);
1495 x29 = ((arg1[5]) * ((uint64_t)x2 * 0x2));
1496 x30 = ((arg1[5]) * x5);
1497 x31 = ((arg1[5]) * ((uint64_t)x8 * 0x2));
1498 x32 = ((arg1[5]) * x11);
1499 x33 = ((uint64_t)(arg1[5]) * (x13 * 0x2));
1500 x34 = ((uint64_t)(arg1[4]) * x2);
1501 x35 = ((arg1[4]) * x5);
1502 x36 = ((uint64_t)(arg1[4]) * x8);
1503 x37 = ((arg1[4]) * x11);
1504 x38 = ((uint64_t)(arg1[4]) * x14);
1505 x39 = ((uint64_t)(arg1[4]) * (arg1[4]));
1506 x40 = ((arg1[3]) * ((uint64_t)x2 * 0x2));
1507 x41 = ((arg1[3]) * x5);
1508 x42 = ((arg1[3]) * ((uint64_t)x8 * 0x2));
1509 x43 = ((uint64_t)(arg1[3]) * x12);
1510 x44 = ((uint64_t)(arg1[3]) * (x14 * 0x2));
1511 x45 = ((uint64_t)(arg1[3]) * x15);
1512 x46 = ((uint64_t)(arg1[3]) * ((arg1[3]) * 0x2));
1513 x47 = ((uint64_t)(arg1[2]) * x2);
1514 x48 = ((arg1[2]) * x5);
1515 x49 = ((uint64_t)(arg1[2]) * x9);
1516 x50 = ((uint64_t)(arg1[2]) * x12);
1517 x51 = ((uint64_t)(arg1[2]) * x14);
1518 x52 = ((uint64_t)(arg1[2]) * x15);
1519 x53 = ((uint64_t)(arg1[2]) * x16);
1520 x54 = ((uint64_t)(arg1[2]) * (arg1[2]));
1521 x55 = ((arg1[1]) * ((uint64_t)x2 * 0x2));
1522 x56 = ((uint64_t)(arg1[1]) * x6);
1523 x57 = ((uint64_t)(arg1[1]) * (x9 * 0x2));
1524 x58 = ((uint64_t)(arg1[1]) * x12);
1525 x59 = ((uint64_t)(arg1[1]) * (x14 * 0x2));
1526 x60 = ((uint64_t)(arg1[1]) * x15);
1527 x61 = ((uint64_t)(arg1[1]) * (x16 * 0x2));
1528 x62 = ((uint64_t)(arg1[1]) * x17);
1529 x63 = ((uint64_t)(arg1[1]) * ((arg1[1]) * 0x2));
1530 x64 = ((uint64_t)(arg1[0]) * x3);
1531 x65 = ((uint64_t)(arg1[0]) * x6);
1532 x66 = ((uint64_t)(arg1[0]) * x9);
1533 x67 = ((uint64_t)(arg1[0]) * x12);
1534 x68 = ((uint64_t)(arg1[0]) * x14);
1535 x69 = ((uint64_t)(arg1[0]) * x15);
1536 x70 = ((uint64_t)(arg1[0]) * x16);
1537 x71 = ((uint64_t)(arg1[0]) * x17);
1538 x72 = ((uint64_t)(arg1[0]) * x18);
1539 x73 = ((uint64_t)(arg1[0]) * (arg1[0]));
1540 x74 = (x73 + (x55 + (x48 + (x42 + (x37 + x33)))));
1541 x75 = (x74 >> 26);
1542 x76 = (uint32_t)(x74 & UINT32_C(0x3ffffff));
1543 x77 = (x64 + (x56 + (x49 + (x43 + x38))));
1544 x78 = (x65 + (x57 + (x50 + (x44 + (x39 + x19)))));
1545 x79 = (x66 + (x58 + (x51 + (x45 + x20))));
1546 x80 = (x67 + (x59 + (x52 + (x46 + (x22 + x21)))));
1547 x81 = (x68 + (x60 + (x53 + (x25 + x23))));
1548 x82 = (x69 + (x61 + (x54 + (x29 + (x26 + x24)))));
1549 x83 = (x70 + (x62 + (x34 + (x30 + x27))));
1550 x84 = (x71 + (x63 + (x40 + (x35 + (x31 + x28)))));
1551 x85 = (x72 + (x47 + (x41 + (x36 + x32))));
1552 x86 = (x75 + x85);
1553 x87 = (x86 >> 25);
1554 x88 = (uint32_t)(x86 & UINT32_C(0x1ffffff));
1555 x89 = (x87 + x84);
1556 x90 = (x89 >> 26);
1557 x91 = (uint32_t)(x89 & UINT32_C(0x3ffffff));
1558 x92 = (x90 + x83);
1559 x93 = (x92 >> 25);
1560 x94 = (uint32_t)(x92 & UINT32_C(0x1ffffff));
1561 x95 = (x93 + x82);
1562 x96 = (x95 >> 26);
1563 x97 = (uint32_t)(x95 & UINT32_C(0x3ffffff));
1564 x98 = (x96 + x81);
1565 x99 = (x98 >> 25);
1566 x100 = (uint32_t)(x98 & UINT32_C(0x1ffffff));
1567 x101 = (x99 + x80);
1568 x102 = (x101 >> 26);
1569 x103 = (uint32_t)(x101 & UINT32_C(0x3ffffff));
1570 x104 = (x102 + x79);
1571 x105 = (x104 >> 25);
1572 x106 = (uint32_t)(x104 & UINT32_C(0x1ffffff));
1573 x107 = (x105 + x78);
1574 x108 = (x107 >> 26);
1575 x109 = (uint32_t)(x107 & UINT32_C(0x3ffffff));
1576 x110 = (x108 + x77);
1577 x111 = (x110 >> 25);
1578 x112 = (uint32_t)(x110 & UINT32_C(0x1ffffff));
1579 x113 = (x111 * UINT8_C(0x13));
1580 x114 = (x76 + x113);
1581 x115 = (uint32_t)(x114 >> 26);
1582 x116 = (uint32_t)(x114 & UINT32_C(0x3ffffff));
1583 x117 = (x115 + x88);
1584 x118 = (fiat_25519_uint1)(x117 >> 25);
1585 x119 = (x117 & UINT32_C(0x1ffffff));
1586 x120 = (x118 + x91);
1587 out1[0] = x116;
1588 out1[1] = x119;
1589 out1[2] = x120;
1590 out1[3] = x94;
1591 out1[4] = x97;
1592 out1[5] = x100;
1593 out1[6] = x103;
1594 out1[7] = x106;
1595 out1[8] = x109;
1596 out1[9] = x112;
1597 }
1598
1599 /*
1600 * The function fiat_25519_carry reduces a field element.
1601 *
1602 * Postconditions:
1603 * eval out1 mod m = eval arg1 mod m
1604 *
1605 */
fiat_25519_carry(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)1606 static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
1607 uint32_t x1;
1608 uint32_t x2;
1609 uint32_t x3;
1610 uint32_t x4;
1611 uint32_t x5;
1612 uint32_t x6;
1613 uint32_t x7;
1614 uint32_t x8;
1615 uint32_t x9;
1616 uint32_t x10;
1617 uint32_t x11;
1618 uint32_t x12;
1619 uint32_t x13;
1620 uint32_t x14;
1621 uint32_t x15;
1622 uint32_t x16;
1623 uint32_t x17;
1624 uint32_t x18;
1625 uint32_t x19;
1626 uint32_t x20;
1627 uint32_t x21;
1628 uint32_t x22;
1629 x1 = (arg1[0]);
1630 x2 = ((x1 >> 26) + (arg1[1]));
1631 x3 = ((x2 >> 25) + (arg1[2]));
1632 x4 = ((x3 >> 26) + (arg1[3]));
1633 x5 = ((x4 >> 25) + (arg1[4]));
1634 x6 = ((x5 >> 26) + (arg1[5]));
1635 x7 = ((x6 >> 25) + (arg1[6]));
1636 x8 = ((x7 >> 26) + (arg1[7]));
1637 x9 = ((x8 >> 25) + (arg1[8]));
1638 x10 = ((x9 >> 26) + (arg1[9]));
1639 x11 = ((x1 & UINT32_C(0x3ffffff)) + ((x10 >> 25) * UINT8_C(0x13)));
1640 x12 = ((fiat_25519_uint1)(x11 >> 26) + (x2 & UINT32_C(0x1ffffff)));
1641 x13 = (x11 & UINT32_C(0x3ffffff));
1642 x14 = (x12 & UINT32_C(0x1ffffff));
1643 x15 = ((fiat_25519_uint1)(x12 >> 25) + (x3 & UINT32_C(0x3ffffff)));
1644 x16 = (x4 & UINT32_C(0x1ffffff));
1645 x17 = (x5 & UINT32_C(0x3ffffff));
1646 x18 = (x6 & UINT32_C(0x1ffffff));
1647 x19 = (x7 & UINT32_C(0x3ffffff));
1648 x20 = (x8 & UINT32_C(0x1ffffff));
1649 x21 = (x9 & UINT32_C(0x3ffffff));
1650 x22 = (x10 & UINT32_C(0x1ffffff));
1651 out1[0] = x13;
1652 out1[1] = x14;
1653 out1[2] = x15;
1654 out1[3] = x16;
1655 out1[4] = x17;
1656 out1[5] = x18;
1657 out1[6] = x19;
1658 out1[7] = x20;
1659 out1[8] = x21;
1660 out1[9] = x22;
1661 }
1662
1663 /*
1664 * The function fiat_25519_add adds two field elements.
1665 *
1666 * Postconditions:
1667 * eval out1 mod m = (eval arg1 + eval arg2) mod m
1668 *
1669 */
fiat_25519_add(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)1670 static FIAT_25519_FIAT_INLINE void fiat_25519_add(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) {
1671 uint32_t x1;
1672 uint32_t x2;
1673 uint32_t x3;
1674 uint32_t x4;
1675 uint32_t x5;
1676 uint32_t x6;
1677 uint32_t x7;
1678 uint32_t x8;
1679 uint32_t x9;
1680 uint32_t x10;
1681 x1 = ((arg1[0]) + (arg2[0]));
1682 x2 = ((arg1[1]) + (arg2[1]));
1683 x3 = ((arg1[2]) + (arg2[2]));
1684 x4 = ((arg1[3]) + (arg2[3]));
1685 x5 = ((arg1[4]) + (arg2[4]));
1686 x6 = ((arg1[5]) + (arg2[5]));
1687 x7 = ((arg1[6]) + (arg2[6]));
1688 x8 = ((arg1[7]) + (arg2[7]));
1689 x9 = ((arg1[8]) + (arg2[8]));
1690 x10 = ((arg1[9]) + (arg2[9]));
1691 out1[0] = x1;
1692 out1[1] = x2;
1693 out1[2] = x3;
1694 out1[3] = x4;
1695 out1[4] = x5;
1696 out1[5] = x6;
1697 out1[6] = x7;
1698 out1[7] = x8;
1699 out1[8] = x9;
1700 out1[9] = x10;
1701 }
1702
1703 /*
1704 * The function fiat_25519_sub subtracts two field elements.
1705 *
1706 * Postconditions:
1707 * eval out1 mod m = (eval arg1 - eval arg2) mod m
1708 *
1709 */
fiat_25519_sub(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)1710 static FIAT_25519_FIAT_INLINE void fiat_25519_sub(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1, const fiat_25519_tight_field_element arg2) {
1711 uint32_t x1;
1712 uint32_t x2;
1713 uint32_t x3;
1714 uint32_t x4;
1715 uint32_t x5;
1716 uint32_t x6;
1717 uint32_t x7;
1718 uint32_t x8;
1719 uint32_t x9;
1720 uint32_t x10;
1721 x1 = ((UINT32_C(0x7ffffda) + (arg1[0])) - (arg2[0]));
1722 x2 = ((UINT32_C(0x3fffffe) + (arg1[1])) - (arg2[1]));
1723 x3 = ((UINT32_C(0x7fffffe) + (arg1[2])) - (arg2[2]));
1724 x4 = ((UINT32_C(0x3fffffe) + (arg1[3])) - (arg2[3]));
1725 x5 = ((UINT32_C(0x7fffffe) + (arg1[4])) - (arg2[4]));
1726 x6 = ((UINT32_C(0x3fffffe) + (arg1[5])) - (arg2[5]));
1727 x7 = ((UINT32_C(0x7fffffe) + (arg1[6])) - (arg2[6]));
1728 x8 = ((UINT32_C(0x3fffffe) + (arg1[7])) - (arg2[7]));
1729 x9 = ((UINT32_C(0x7fffffe) + (arg1[8])) - (arg2[8]));
1730 x10 = ((UINT32_C(0x3fffffe) + (arg1[9])) - (arg2[9]));
1731 out1[0] = x1;
1732 out1[1] = x2;
1733 out1[2] = x3;
1734 out1[3] = x4;
1735 out1[4] = x5;
1736 out1[5] = x6;
1737 out1[6] = x7;
1738 out1[7] = x8;
1739 out1[8] = x9;
1740 out1[9] = x10;
1741 }
1742
1743 /*
1744 * The function fiat_25519_opp negates a field element.
1745 *
1746 * Postconditions:
1747 * eval out1 mod m = -eval arg1 mod m
1748 *
1749 */
fiat_25519_opp(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1)1750 static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) {
1751 uint32_t x1;
1752 uint32_t x2;
1753 uint32_t x3;
1754 uint32_t x4;
1755 uint32_t x5;
1756 uint32_t x6;
1757 uint32_t x7;
1758 uint32_t x8;
1759 uint32_t x9;
1760 uint32_t x10;
1761 x1 = (UINT32_C(0x7ffffda) - (arg1[0]));
1762 x2 = (UINT32_C(0x3fffffe) - (arg1[1]));
1763 x3 = (UINT32_C(0x7fffffe) - (arg1[2]));
1764 x4 = (UINT32_C(0x3fffffe) - (arg1[3]));
1765 x5 = (UINT32_C(0x7fffffe) - (arg1[4]));
1766 x6 = (UINT32_C(0x3fffffe) - (arg1[5]));
1767 x7 = (UINT32_C(0x7fffffe) - (arg1[6]));
1768 x8 = (UINT32_C(0x3fffffe) - (arg1[7]));
1769 x9 = (UINT32_C(0x7fffffe) - (arg1[8]));
1770 x10 = (UINT32_C(0x3fffffe) - (arg1[9]));
1771 out1[0] = x1;
1772 out1[1] = x2;
1773 out1[2] = x3;
1774 out1[3] = x4;
1775 out1[4] = x5;
1776 out1[5] = x6;
1777 out1[6] = x7;
1778 out1[7] = x8;
1779 out1[8] = x9;
1780 out1[9] = x10;
1781 }
1782
1783 /*
1784 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
1785 *
1786 * Postconditions:
1787 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
1788 *
1789 * Output Bounds:
1790 * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
1791 */
fiat_25519_to_bytes(uint8_t out1[32],const fiat_25519_tight_field_element arg1)1792 static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) {
1793 uint32_t x1;
1794 fiat_25519_uint1 x2;
1795 uint32_t x3;
1796 fiat_25519_uint1 x4;
1797 uint32_t x5;
1798 fiat_25519_uint1 x6;
1799 uint32_t x7;
1800 fiat_25519_uint1 x8;
1801 uint32_t x9;
1802 fiat_25519_uint1 x10;
1803 uint32_t x11;
1804 fiat_25519_uint1 x12;
1805 uint32_t x13;
1806 fiat_25519_uint1 x14;
1807 uint32_t x15;
1808 fiat_25519_uint1 x16;
1809 uint32_t x17;
1810 fiat_25519_uint1 x18;
1811 uint32_t x19;
1812 fiat_25519_uint1 x20;
1813 uint32_t x21;
1814 uint32_t x22;
1815 fiat_25519_uint1 x23;
1816 uint32_t x24;
1817 fiat_25519_uint1 x25;
1818 uint32_t x26;
1819 fiat_25519_uint1 x27;
1820 uint32_t x28;
1821 fiat_25519_uint1 x29;
1822 uint32_t x30;
1823 fiat_25519_uint1 x31;
1824 uint32_t x32;
1825 fiat_25519_uint1 x33;
1826 uint32_t x34;
1827 fiat_25519_uint1 x35;
1828 uint32_t x36;
1829 fiat_25519_uint1 x37;
1830 uint32_t x38;
1831 fiat_25519_uint1 x39;
1832 uint32_t x40;
1833 fiat_25519_uint1 x41;
1834 uint32_t x42;
1835 uint32_t x43;
1836 uint32_t x44;
1837 uint32_t x45;
1838 uint32_t x46;
1839 uint32_t x47;
1840 uint32_t x48;
1841 uint32_t x49;
1842 uint8_t x50;
1843 uint32_t x51;
1844 uint8_t x52;
1845 uint32_t x53;
1846 uint8_t x54;
1847 uint8_t x55;
1848 uint32_t x56;
1849 uint8_t x57;
1850 uint32_t x58;
1851 uint8_t x59;
1852 uint32_t x60;
1853 uint8_t x61;
1854 uint8_t x62;
1855 uint32_t x63;
1856 uint8_t x64;
1857 uint32_t x65;
1858 uint8_t x66;
1859 uint32_t x67;
1860 uint8_t x68;
1861 uint8_t x69;
1862 uint32_t x70;
1863 uint8_t x71;
1864 uint32_t x72;
1865 uint8_t x73;
1866 uint32_t x74;
1867 uint8_t x75;
1868 uint8_t x76;
1869 uint32_t x77;
1870 uint8_t x78;
1871 uint32_t x79;
1872 uint8_t x80;
1873 uint32_t x81;
1874 uint8_t x82;
1875 uint8_t x83;
1876 uint8_t x84;
1877 uint32_t x85;
1878 uint8_t x86;
1879 uint32_t x87;
1880 uint8_t x88;
1881 fiat_25519_uint1 x89;
1882 uint32_t x90;
1883 uint8_t x91;
1884 uint32_t x92;
1885 uint8_t x93;
1886 uint32_t x94;
1887 uint8_t x95;
1888 uint8_t x96;
1889 uint32_t x97;
1890 uint8_t x98;
1891 uint32_t x99;
1892 uint8_t x100;
1893 uint32_t x101;
1894 uint8_t x102;
1895 uint8_t x103;
1896 uint32_t x104;
1897 uint8_t x105;
1898 uint32_t x106;
1899 uint8_t x107;
1900 uint32_t x108;
1901 uint8_t x109;
1902 uint8_t x110;
1903 uint32_t x111;
1904 uint8_t x112;
1905 uint32_t x113;
1906 uint8_t x114;
1907 uint32_t x115;
1908 uint8_t x116;
1909 uint8_t x117;
1910 fiat_25519_subborrowx_u26(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0x3ffffed));
1911 fiat_25519_subborrowx_u25(&x3, &x4, x2, (arg1[1]), UINT32_C(0x1ffffff));
1912 fiat_25519_subborrowx_u26(&x5, &x6, x4, (arg1[2]), UINT32_C(0x3ffffff));
1913 fiat_25519_subborrowx_u25(&x7, &x8, x6, (arg1[3]), UINT32_C(0x1ffffff));
1914 fiat_25519_subborrowx_u26(&x9, &x10, x8, (arg1[4]), UINT32_C(0x3ffffff));
1915 fiat_25519_subborrowx_u25(&x11, &x12, x10, (arg1[5]), UINT32_C(0x1ffffff));
1916 fiat_25519_subborrowx_u26(&x13, &x14, x12, (arg1[6]), UINT32_C(0x3ffffff));
1917 fiat_25519_subborrowx_u25(&x15, &x16, x14, (arg1[7]), UINT32_C(0x1ffffff));
1918 fiat_25519_subborrowx_u26(&x17, &x18, x16, (arg1[8]), UINT32_C(0x3ffffff));
1919 fiat_25519_subborrowx_u25(&x19, &x20, x18, (arg1[9]), UINT32_C(0x1ffffff));
1920 fiat_25519_cmovznz_u32(&x21, x20, 0x0, UINT32_C(0xffffffff));
1921 fiat_25519_addcarryx_u26(&x22, &x23, 0x0, x1, (x21 & UINT32_C(0x3ffffed)));
1922 fiat_25519_addcarryx_u25(&x24, &x25, x23, x3, (x21 & UINT32_C(0x1ffffff)));
1923 fiat_25519_addcarryx_u26(&x26, &x27, x25, x5, (x21 & UINT32_C(0x3ffffff)));
1924 fiat_25519_addcarryx_u25(&x28, &x29, x27, x7, (x21 & UINT32_C(0x1ffffff)));
1925 fiat_25519_addcarryx_u26(&x30, &x31, x29, x9, (x21 & UINT32_C(0x3ffffff)));
1926 fiat_25519_addcarryx_u25(&x32, &x33, x31, x11, (x21 & UINT32_C(0x1ffffff)));
1927 fiat_25519_addcarryx_u26(&x34, &x35, x33, x13, (x21 & UINT32_C(0x3ffffff)));
1928 fiat_25519_addcarryx_u25(&x36, &x37, x35, x15, (x21 & UINT32_C(0x1ffffff)));
1929 fiat_25519_addcarryx_u26(&x38, &x39, x37, x17, (x21 & UINT32_C(0x3ffffff)));
1930 fiat_25519_addcarryx_u25(&x40, &x41, x39, x19, (x21 & UINT32_C(0x1ffffff)));
1931 x42 = (x40 << 6);
1932 x43 = (x38 << 4);
1933 x44 = (x36 << 3);
1934 x45 = (x34 * (uint32_t)0x2);
1935 x46 = (x30 << 6);
1936 x47 = (x28 << 5);
1937 x48 = (x26 << 3);
1938 x49 = (x24 << 2);
1939 x50 = (uint8_t)(x22 & UINT8_C(0xff));
1940 x51 = (x22 >> 8);
1941 x52 = (uint8_t)(x51 & UINT8_C(0xff));
1942 x53 = (x51 >> 8);
1943 x54 = (uint8_t)(x53 & UINT8_C(0xff));
1944 x55 = (uint8_t)(x53 >> 8);
1945 x56 = (x49 + (uint32_t)x55);
1946 x57 = (uint8_t)(x56 & UINT8_C(0xff));
1947 x58 = (x56 >> 8);
1948 x59 = (uint8_t)(x58 & UINT8_C(0xff));
1949 x60 = (x58 >> 8);
1950 x61 = (uint8_t)(x60 & UINT8_C(0xff));
1951 x62 = (uint8_t)(x60 >> 8);
1952 x63 = (x48 + (uint32_t)x62);
1953 x64 = (uint8_t)(x63 & UINT8_C(0xff));
1954 x65 = (x63 >> 8);
1955 x66 = (uint8_t)(x65 & UINT8_C(0xff));
1956 x67 = (x65 >> 8);
1957 x68 = (uint8_t)(x67 & UINT8_C(0xff));
1958 x69 = (uint8_t)(x67 >> 8);
1959 x70 = (x47 + (uint32_t)x69);
1960 x71 = (uint8_t)(x70 & UINT8_C(0xff));
1961 x72 = (x70 >> 8);
1962 x73 = (uint8_t)(x72 & UINT8_C(0xff));
1963 x74 = (x72 >> 8);
1964 x75 = (uint8_t)(x74 & UINT8_C(0xff));
1965 x76 = (uint8_t)(x74 >> 8);
1966 x77 = (x46 + (uint32_t)x76);
1967 x78 = (uint8_t)(x77 & UINT8_C(0xff));
1968 x79 = (x77 >> 8);
1969 x80 = (uint8_t)(x79 & UINT8_C(0xff));
1970 x81 = (x79 >> 8);
1971 x82 = (uint8_t)(x81 & UINT8_C(0xff));
1972 x83 = (uint8_t)(x81 >> 8);
1973 x84 = (uint8_t)(x32 & UINT8_C(0xff));
1974 x85 = (x32 >> 8);
1975 x86 = (uint8_t)(x85 & UINT8_C(0xff));
1976 x87 = (x85 >> 8);
1977 x88 = (uint8_t)(x87 & UINT8_C(0xff));
1978 x89 = (fiat_25519_uint1)(x87 >> 8);
1979 x90 = (x45 + (uint32_t)x89);
1980 x91 = (uint8_t)(x90 & UINT8_C(0xff));
1981 x92 = (x90 >> 8);
1982 x93 = (uint8_t)(x92 & UINT8_C(0xff));
1983 x94 = (x92 >> 8);
1984 x95 = (uint8_t)(x94 & UINT8_C(0xff));
1985 x96 = (uint8_t)(x94 >> 8);
1986 x97 = (x44 + (uint32_t)x96);
1987 x98 = (uint8_t)(x97 & UINT8_C(0xff));
1988 x99 = (x97 >> 8);
1989 x100 = (uint8_t)(x99 & UINT8_C(0xff));
1990 x101 = (x99 >> 8);
1991 x102 = (uint8_t)(x101 & UINT8_C(0xff));
1992 x103 = (uint8_t)(x101 >> 8);
1993 x104 = (x43 + (uint32_t)x103);
1994 x105 = (uint8_t)(x104 & UINT8_C(0xff));
1995 x106 = (x104 >> 8);
1996 x107 = (uint8_t)(x106 & UINT8_C(0xff));
1997 x108 = (x106 >> 8);
1998 x109 = (uint8_t)(x108 & UINT8_C(0xff));
1999 x110 = (uint8_t)(x108 >> 8);
2000 x111 = (x42 + (uint32_t)x110);
2001 x112 = (uint8_t)(x111 & UINT8_C(0xff));
2002 x113 = (x111 >> 8);
2003 x114 = (uint8_t)(x113 & UINT8_C(0xff));
2004 x115 = (x113 >> 8);
2005 x116 = (uint8_t)(x115 & UINT8_C(0xff));
2006 x117 = (uint8_t)(x115 >> 8);
2007 out1[0] = x50;
2008 out1[1] = x52;
2009 out1[2] = x54;
2010 out1[3] = x57;
2011 out1[4] = x59;
2012 out1[5] = x61;
2013 out1[6] = x64;
2014 out1[7] = x66;
2015 out1[8] = x68;
2016 out1[9] = x71;
2017 out1[10] = x73;
2018 out1[11] = x75;
2019 out1[12] = x78;
2020 out1[13] = x80;
2021 out1[14] = x82;
2022 out1[15] = x83;
2023 out1[16] = x84;
2024 out1[17] = x86;
2025 out1[18] = x88;
2026 out1[19] = x91;
2027 out1[20] = x93;
2028 out1[21] = x95;
2029 out1[22] = x98;
2030 out1[23] = x100;
2031 out1[24] = x102;
2032 out1[25] = x105;
2033 out1[26] = x107;
2034 out1[27] = x109;
2035 out1[28] = x112;
2036 out1[29] = x114;
2037 out1[30] = x116;
2038 out1[31] = x117;
2039 }
2040
2041 /*
2042 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
2043 *
2044 * Postconditions:
2045 * eval out1 mod m = bytes_eval arg1 mod m
2046 *
2047 * Input Bounds:
2048 * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x7f]]
2049 */
fiat_25519_from_bytes(fiat_25519_tight_field_element out1,const uint8_t arg1[32])2050 static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) {
2051 uint32_t x1;
2052 uint32_t x2;
2053 uint32_t x3;
2054 uint32_t x4;
2055 uint32_t x5;
2056 uint32_t x6;
2057 uint32_t x7;
2058 uint32_t x8;
2059 uint32_t x9;
2060 uint32_t x10;
2061 uint32_t x11;
2062 uint32_t x12;
2063 uint32_t x13;
2064 uint32_t x14;
2065 uint32_t x15;
2066 uint8_t x16;
2067 uint32_t x17;
2068 uint32_t x18;
2069 uint32_t x19;
2070 uint32_t x20;
2071 uint32_t x21;
2072 uint32_t x22;
2073 uint32_t x23;
2074 uint32_t x24;
2075 uint32_t x25;
2076 uint32_t x26;
2077 uint32_t x27;
2078 uint32_t x28;
2079 uint32_t x29;
2080 uint32_t x30;
2081 uint32_t x31;
2082 uint8_t x32;
2083 uint32_t x33;
2084 uint32_t x34;
2085 uint32_t x35;
2086 uint32_t x36;
2087 uint8_t x37;
2088 uint32_t x38;
2089 uint32_t x39;
2090 uint32_t x40;
2091 uint32_t x41;
2092 uint8_t x42;
2093 uint32_t x43;
2094 uint32_t x44;
2095 uint32_t x45;
2096 uint32_t x46;
2097 uint8_t x47;
2098 uint32_t x48;
2099 uint32_t x49;
2100 uint32_t x50;
2101 uint32_t x51;
2102 uint8_t x52;
2103 uint32_t x53;
2104 uint32_t x54;
2105 uint32_t x55;
2106 uint32_t x56;
2107 uint32_t x57;
2108 uint32_t x58;
2109 uint32_t x59;
2110 uint8_t x60;
2111 uint32_t x61;
2112 uint32_t x62;
2113 uint32_t x63;
2114 uint32_t x64;
2115 uint8_t x65;
2116 uint32_t x66;
2117 uint32_t x67;
2118 uint32_t x68;
2119 uint32_t x69;
2120 uint8_t x70;
2121 uint32_t x71;
2122 uint32_t x72;
2123 uint32_t x73;
2124 uint32_t x74;
2125 uint8_t x75;
2126 uint32_t x76;
2127 uint32_t x77;
2128 uint32_t x78;
2129 x1 = ((uint32_t)(arg1[31]) << 18);
2130 x2 = ((uint32_t)(arg1[30]) << 10);
2131 x3 = ((uint32_t)(arg1[29]) << 2);
2132 x4 = ((uint32_t)(arg1[28]) << 20);
2133 x5 = ((uint32_t)(arg1[27]) << 12);
2134 x6 = ((uint32_t)(arg1[26]) << 4);
2135 x7 = ((uint32_t)(arg1[25]) << 21);
2136 x8 = ((uint32_t)(arg1[24]) << 13);
2137 x9 = ((uint32_t)(arg1[23]) << 5);
2138 x10 = ((uint32_t)(arg1[22]) << 23);
2139 x11 = ((uint32_t)(arg1[21]) << 15);
2140 x12 = ((uint32_t)(arg1[20]) << 7);
2141 x13 = ((uint32_t)(arg1[19]) << 24);
2142 x14 = ((uint32_t)(arg1[18]) << 16);
2143 x15 = ((uint32_t)(arg1[17]) << 8);
2144 x16 = (arg1[16]);
2145 x17 = ((uint32_t)(arg1[15]) << 18);
2146 x18 = ((uint32_t)(arg1[14]) << 10);
2147 x19 = ((uint32_t)(arg1[13]) << 2);
2148 x20 = ((uint32_t)(arg1[12]) << 19);
2149 x21 = ((uint32_t)(arg1[11]) << 11);
2150 x22 = ((uint32_t)(arg1[10]) << 3);
2151 x23 = ((uint32_t)(arg1[9]) << 21);
2152 x24 = ((uint32_t)(arg1[8]) << 13);
2153 x25 = ((uint32_t)(arg1[7]) << 5);
2154 x26 = ((uint32_t)(arg1[6]) << 22);
2155 x27 = ((uint32_t)(arg1[5]) << 14);
2156 x28 = ((uint32_t)(arg1[4]) << 6);
2157 x29 = ((uint32_t)(arg1[3]) << 24);
2158 x30 = ((uint32_t)(arg1[2]) << 16);
2159 x31 = ((uint32_t)(arg1[1]) << 8);
2160 x32 = (arg1[0]);
2161 x33 = (x31 + (uint32_t)x32);
2162 x34 = (x30 + x33);
2163 x35 = (x29 + x34);
2164 x36 = (x35 & UINT32_C(0x3ffffff));
2165 x37 = (uint8_t)(x35 >> 26);
2166 x38 = (x28 + (uint32_t)x37);
2167 x39 = (x27 + x38);
2168 x40 = (x26 + x39);
2169 x41 = (x40 & UINT32_C(0x1ffffff));
2170 x42 = (uint8_t)(x40 >> 25);
2171 x43 = (x25 + (uint32_t)x42);
2172 x44 = (x24 + x43);
2173 x45 = (x23 + x44);
2174 x46 = (x45 & UINT32_C(0x3ffffff));
2175 x47 = (uint8_t)(x45 >> 26);
2176 x48 = (x22 + (uint32_t)x47);
2177 x49 = (x21 + x48);
2178 x50 = (x20 + x49);
2179 x51 = (x50 & UINT32_C(0x1ffffff));
2180 x52 = (uint8_t)(x50 >> 25);
2181 x53 = (x19 + (uint32_t)x52);
2182 x54 = (x18 + x53);
2183 x55 = (x17 + x54);
2184 x56 = (x15 + (uint32_t)x16);
2185 x57 = (x14 + x56);
2186 x58 = (x13 + x57);
2187 x59 = (x58 & UINT32_C(0x1ffffff));
2188 x60 = (uint8_t)(x58 >> 25);
2189 x61 = (x12 + (uint32_t)x60);
2190 x62 = (x11 + x61);
2191 x63 = (x10 + x62);
2192 x64 = (x63 & UINT32_C(0x3ffffff));
2193 x65 = (uint8_t)(x63 >> 26);
2194 x66 = (x9 + (uint32_t)x65);
2195 x67 = (x8 + x66);
2196 x68 = (x7 + x67);
2197 x69 = (x68 & UINT32_C(0x1ffffff));
2198 x70 = (uint8_t)(x68 >> 25);
2199 x71 = (x6 + (uint32_t)x70);
2200 x72 = (x5 + x71);
2201 x73 = (x4 + x72);
2202 x74 = (x73 & UINT32_C(0x3ffffff));
2203 x75 = (uint8_t)(x73 >> 26);
2204 x76 = (x3 + (uint32_t)x75);
2205 x77 = (x2 + x76);
2206 x78 = (x1 + x77);
2207 out1[0] = x36;
2208 out1[1] = x41;
2209 out1[2] = x46;
2210 out1[3] = x51;
2211 out1[4] = x55;
2212 out1[5] = x59;
2213 out1[6] = x64;
2214 out1[7] = x69;
2215 out1[8] = x74;
2216 out1[9] = x78;
2217 }
2218
2219 #endif /* not defined(BORINGSSL_CURVE25519_64BIT) */
2220