1 /* Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --inline --static --use-value-barrier --no-wide-int 25519 64 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666 */
2 /* curve description: 25519 */
3 /* machine_wordsize = 64 (from "64") */
4 /* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666 */
5 /* n = 5 (from "(auto)") */
6 /* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */
7 /* tight_bounds_multiplier = 1 (from "") */
8 /* */
9 /* Computed values: */
10 /* carry_chain = [0, 1, 2, 3, 4, 0, 1] */
11 /* eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204) */
12 /* 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) */
13 /* balance = [0xfffffffffffda, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */
14
15 #include <stdint.h>
16 #include <intrin.h>
17 #if defined(_M_X64)
18 #include <immintrin.h>
19 #endif
20
21 typedef unsigned char fiat_25519_uint1;
22 typedef signed char fiat_25519_int1;
23
24 #define FIAT_25519_FIAT_INLINE inline
25
26 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */
27 /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */
28 typedef uint64_t fiat_25519_loose_field_element[5];
29
30 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */
31 /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */
32 typedef uint64_t fiat_25519_tight_field_element[5];
33
34 #if (-1 & 3) != 3
35 #error "This code only works on a two's complement system"
36 #endif
37
38 #define fiat_25519_value_barrier_u64(x) (x)
39
40 /*
41 * The function fiat_25519_addcarryx_u64 is an addition with carry.
42 *
43 * Postconditions:
44 * out1 = (arg1 + arg2 + arg3) mod 2^64
45 * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
46 *
47 * Input Bounds:
48 * arg1: [0x0 ~> 0x1]
49 * arg2: [0x0 ~> 0xffffffffffffffff]
50 * arg3: [0x0 ~> 0xffffffffffffffff]
51 * Output Bounds:
52 * out1: [0x0 ~> 0xffffffffffffffff]
53 * out2: [0x0 ~> 0x1]
54 */
fiat_25519_addcarryx_u64(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)55 static FIAT_25519_FIAT_INLINE void fiat_25519_addcarryx_u64(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
56 // NOTE: edited after generation
57 #if defined(_M_X64)
58 *out2 = _addcarry_u64(arg1, arg2, arg3, out1);
59 #else
60 arg2 += arg1;
61 arg1 = arg2 < arg1;
62 arg3 += arg2;
63 arg1 += arg3 < arg2;
64 *out1 = arg3;
65 *out2 = arg1;
66 #endif
67 }
68
69 /*
70 * The function fiat_25519_subborrowx_u64 is a subtraction with borrow.
71 *
72 * Postconditions:
73 * out1 = (-arg1 + arg2 + -arg3) mod 2^64
74 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
75 *
76 * Input Bounds:
77 * arg1: [0x0 ~> 0x1]
78 * arg2: [0x0 ~> 0xffffffffffffffff]
79 * arg3: [0x0 ~> 0xffffffffffffffff]
80 * Output Bounds:
81 * out1: [0x0 ~> 0xffffffffffffffff]
82 * out2: [0x0 ~> 0x1]
83 */
fiat_25519_subborrowx_u64(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)84 static FIAT_25519_FIAT_INLINE void fiat_25519_subborrowx_u64(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
85 #if defined(_M_X64)
86 *out2 = _subborrow_u64(arg1, arg2, arg3, out1); // NOTE: edited after generation
87 #else
88 *out1 = arg2 - arg3 - arg1;
89 *out2 = (arg2 < arg3) | ((arg2 == arg3) & arg1);
90 #endif
91 }
92
93 /*
94 * The function fiat_25519_addcarryx_u51 is an addition with carry.
95 *
96 * Postconditions:
97 * out1 = (arg1 + arg2 + arg3) mod 2^51
98 * out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
99 *
100 * Input Bounds:
101 * arg1: [0x0 ~> 0x1]
102 * arg2: [0x0 ~> 0x7ffffffffffff]
103 * arg3: [0x0 ~> 0x7ffffffffffff]
104 * Output Bounds:
105 * out1: [0x0 ~> 0x7ffffffffffff]
106 * out2: [0x0 ~> 0x1]
107 */
fiat_25519_addcarryx_u51(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)108 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) {
109 uint64_t x1;
110 uint64_t x2;
111 fiat_25519_uint1 x3;
112 x1 = ((arg1 + arg2) + arg3);
113 x2 = (x1 & UINT64_C(0x7ffffffffffff));
114 x3 = (fiat_25519_uint1)(x1 >> 51);
115 *out1 = x2;
116 *out2 = x3;
117 }
118
119 /*
120 * The function fiat_25519_subborrowx_u51 is a subtraction with borrow.
121 *
122 * Postconditions:
123 * out1 = (-arg1 + arg2 + -arg3) mod 2^51
124 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋
125 *
126 * Input Bounds:
127 * arg1: [0x0 ~> 0x1]
128 * arg2: [0x0 ~> 0x7ffffffffffff]
129 * arg3: [0x0 ~> 0x7ffffffffffff]
130 * Output Bounds:
131 * out1: [0x0 ~> 0x7ffffffffffff]
132 * out2: [0x0 ~> 0x1]
133 */
fiat_25519_subborrowx_u51(uint64_t * out1,fiat_25519_uint1 * out2,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)134 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) {
135 int64_t x1;
136 fiat_25519_int1 x2;
137 uint64_t x3;
138 x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
139 x2 = (fiat_25519_int1)(x1 >> 51);
140 x3 = (x1 & UINT64_C(0x7ffffffffffff));
141 *out1 = x3;
142 *out2 = (fiat_25519_uint1)(0x0 - x2);
143 }
144
145 /*
146 * The function fiat_25519_mulx_u64 is a multiplication, returning the full double-width result.
147 *
148 * Postconditions:
149 * out1 = (arg1 * arg2) mod 2^64
150 * out2 = ⌊arg1 * arg2 / 2^64⌋
151 *
152 * Input Bounds:
153 * arg1: [0x0 ~> 0xffffffffffffffff]
154 * arg2: [0x0 ~> 0xffffffffffffffff]
155 * Output Bounds:
156 * out1: [0x0 ~> 0xffffffffffffffff]
157 * out2: [0x0 ~> 0xffffffffffffffff]
158 */
fiat_25519_mulx_u64(uint64_t * out1,uint64_t * out2,uint64_t arg1,uint64_t arg2)159 static FIAT_25519_FIAT_INLINE void fiat_25519_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, uint64_t arg2) {
160 // NOTE: edited after generation
161 #if defined(_M_X64)
162 *out1 = _umul128(arg1, arg2, out2);
163 #elif defined(_M_ARM64)
164 *out1 = arg1 * arg2;
165 *out2 = __umulh(arg1, arg2);
166 #else
167 #error "This file is intended for MSVC on X64 or ARM64"
168 #endif
169 }
170
171 /*
172 * The function fiat_25519_cmovznz_u64 is a single-word conditional move.
173 *
174 * Postconditions:
175 * out1 = (if arg1 = 0 then arg2 else arg3)
176 *
177 * Input Bounds:
178 * arg1: [0x0 ~> 0x1]
179 * arg2: [0x0 ~> 0xffffffffffffffff]
180 * arg3: [0x0 ~> 0xffffffffffffffff]
181 * Output Bounds:
182 * out1: [0x0 ~> 0xffffffffffffffff]
183 */
fiat_25519_cmovznz_u64(uint64_t * out1,fiat_25519_uint1 arg1,uint64_t arg2,uint64_t arg3)184 static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
185 fiat_25519_uint1 x1;
186 uint64_t x2;
187 uint64_t x3;
188 x1 = (!(!arg1));
189 x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
190 x3 = ((fiat_25519_value_barrier_u64(x2) & arg3) | (fiat_25519_value_barrier_u64((~x2)) & arg2));
191 *out1 = x3;
192 }
193
194 /*
195 * The function fiat_25519_carry_mul multiplies two field elements and reduces the result.
196 *
197 * Postconditions:
198 * eval out1 mod m = (eval arg1 * eval arg2) mod m
199 *
200 */
fiat_25519_carry_mul(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1,const fiat_25519_loose_field_element arg2)201 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) {
202 uint64_t x1;
203 uint64_t x2;
204 uint64_t x3;
205 uint64_t x4;
206 uint64_t x5;
207 uint64_t x6;
208 uint64_t x7;
209 uint64_t x8;
210 uint64_t x9;
211 uint64_t x10;
212 uint64_t x11;
213 uint64_t x12;
214 uint64_t x13;
215 uint64_t x14;
216 uint64_t x15;
217 uint64_t x16;
218 uint64_t x17;
219 uint64_t x18;
220 uint64_t x19;
221 uint64_t x20;
222 uint64_t x21;
223 uint64_t x22;
224 uint64_t x23;
225 uint64_t x24;
226 uint64_t x25;
227 uint64_t x26;
228 uint64_t x27;
229 uint64_t x28;
230 uint64_t x29;
231 uint64_t x30;
232 uint64_t x31;
233 uint64_t x32;
234 uint64_t x33;
235 uint64_t x34;
236 uint64_t x35;
237 uint64_t x36;
238 uint64_t x37;
239 uint64_t x38;
240 uint64_t x39;
241 uint64_t x40;
242 uint64_t x41;
243 uint64_t x42;
244 uint64_t x43;
245 uint64_t x44;
246 uint64_t x45;
247 uint64_t x46;
248 uint64_t x47;
249 uint64_t x48;
250 uint64_t x49;
251 uint64_t x50;
252 uint64_t x51;
253 fiat_25519_uint1 x52;
254 uint64_t x53;
255 fiat_25519_uint1 x54;
256 uint64_t x55;
257 fiat_25519_uint1 x56;
258 uint64_t x57;
259 fiat_25519_uint1 x58;
260 uint64_t x59;
261 fiat_25519_uint1 x60;
262 uint64_t x61;
263 fiat_25519_uint1 x62;
264 uint64_t x63;
265 fiat_25519_uint1 x64;
266 uint64_t x65;
267 fiat_25519_uint1 x66;
268 uint64_t x67;
269 uint64_t x68;
270 uint64_t x69;
271 fiat_25519_uint1 x70;
272 uint64_t x71;
273 fiat_25519_uint1 x72;
274 uint64_t x73;
275 fiat_25519_uint1 x74;
276 uint64_t x75;
277 fiat_25519_uint1 x76;
278 uint64_t x77;
279 fiat_25519_uint1 x78;
280 uint64_t x79;
281 fiat_25519_uint1 x80;
282 uint64_t x81;
283 fiat_25519_uint1 x82;
284 uint64_t x83;
285 fiat_25519_uint1 x84;
286 uint64_t x85;
287 fiat_25519_uint1 x86;
288 uint64_t x87;
289 fiat_25519_uint1 x88;
290 uint64_t x89;
291 fiat_25519_uint1 x90;
292 uint64_t x91;
293 fiat_25519_uint1 x92;
294 uint64_t x93;
295 fiat_25519_uint1 x94;
296 uint64_t x95;
297 fiat_25519_uint1 x96;
298 uint64_t x97;
299 fiat_25519_uint1 x98;
300 uint64_t x99;
301 fiat_25519_uint1 x100;
302 uint64_t x101;
303 fiat_25519_uint1 x102;
304 uint64_t x103;
305 fiat_25519_uint1 x104;
306 uint64_t x105;
307 fiat_25519_uint1 x106;
308 uint64_t x107;
309 fiat_25519_uint1 x108;
310 uint64_t x109;
311 fiat_25519_uint1 x110;
312 uint64_t x111;
313 fiat_25519_uint1 x112;
314 uint64_t x113;
315 fiat_25519_uint1 x114;
316 uint64_t x115;
317 fiat_25519_uint1 x116;
318 uint64_t x117;
319 fiat_25519_uint1 x118;
320 uint64_t x119;
321 fiat_25519_uint1 x120;
322 uint64_t x121;
323 fiat_25519_uint1 x122;
324 uint64_t x123;
325 fiat_25519_uint1 x124;
326 uint64_t x125;
327 fiat_25519_uint1 x126;
328 uint64_t x127;
329 fiat_25519_uint1 x128;
330 uint64_t x129;
331 fiat_25519_uint1 x130;
332 uint64_t x131;
333 fiat_25519_uint1 x132;
334 uint64_t x133;
335 fiat_25519_uint1 x134;
336 uint64_t x135;
337 uint64_t x136;
338 uint64_t x137;
339 uint64_t x138;
340 fiat_25519_uint1 x139;
341 uint64_t x140;
342 uint64_t x141;
343 uint64_t x142;
344 uint64_t x143;
345 fiat_25519_uint1 x144;
346 uint64_t x145;
347 uint64_t x146;
348 uint64_t x147;
349 uint64_t x148;
350 fiat_25519_uint1 x149;
351 uint64_t x150;
352 uint64_t x151;
353 uint64_t x152;
354 uint64_t x153;
355 uint64_t x154;
356 uint64_t x155;
357 uint64_t x156;
358 uint64_t x157;
359 fiat_25519_uint1 x158;
360 uint64_t x159;
361 uint64_t x160;
362 fiat_25519_mulx_u64(&x1, &x2, (arg1[4]), ((arg2[4]) * UINT8_C(0x13)));
363 fiat_25519_mulx_u64(&x3, &x4, (arg1[4]), ((arg2[3]) * UINT8_C(0x13)));
364 fiat_25519_mulx_u64(&x5, &x6, (arg1[4]), ((arg2[2]) * UINT8_C(0x13)));
365 fiat_25519_mulx_u64(&x7, &x8, (arg1[4]), ((arg2[1]) * UINT8_C(0x13)));
366 fiat_25519_mulx_u64(&x9, &x10, (arg1[3]), ((arg2[4]) * UINT8_C(0x13)));
367 fiat_25519_mulx_u64(&x11, &x12, (arg1[3]), ((arg2[3]) * UINT8_C(0x13)));
368 fiat_25519_mulx_u64(&x13, &x14, (arg1[3]), ((arg2[2]) * UINT8_C(0x13)));
369 fiat_25519_mulx_u64(&x15, &x16, (arg1[2]), ((arg2[4]) * UINT8_C(0x13)));
370 fiat_25519_mulx_u64(&x17, &x18, (arg1[2]), ((arg2[3]) * UINT8_C(0x13)));
371 fiat_25519_mulx_u64(&x19, &x20, (arg1[1]), ((arg2[4]) * UINT8_C(0x13)));
372 fiat_25519_mulx_u64(&x21, &x22, (arg1[4]), (arg2[0]));
373 fiat_25519_mulx_u64(&x23, &x24, (arg1[3]), (arg2[1]));
374 fiat_25519_mulx_u64(&x25, &x26, (arg1[3]), (arg2[0]));
375 fiat_25519_mulx_u64(&x27, &x28, (arg1[2]), (arg2[2]));
376 fiat_25519_mulx_u64(&x29, &x30, (arg1[2]), (arg2[1]));
377 fiat_25519_mulx_u64(&x31, &x32, (arg1[2]), (arg2[0]));
378 fiat_25519_mulx_u64(&x33, &x34, (arg1[1]), (arg2[3]));
379 fiat_25519_mulx_u64(&x35, &x36, (arg1[1]), (arg2[2]));
380 fiat_25519_mulx_u64(&x37, &x38, (arg1[1]), (arg2[1]));
381 fiat_25519_mulx_u64(&x39, &x40, (arg1[1]), (arg2[0]));
382 fiat_25519_mulx_u64(&x41, &x42, (arg1[0]), (arg2[4]));
383 fiat_25519_mulx_u64(&x43, &x44, (arg1[0]), (arg2[3]));
384 fiat_25519_mulx_u64(&x45, &x46, (arg1[0]), (arg2[2]));
385 fiat_25519_mulx_u64(&x47, &x48, (arg1[0]), (arg2[1]));
386 fiat_25519_mulx_u64(&x49, &x50, (arg1[0]), (arg2[0]));
387 fiat_25519_addcarryx_u64(&x51, &x52, 0x0, x13, x7);
388 fiat_25519_addcarryx_u64(&x53, &x54, x52, x14, x8);
389 fiat_25519_addcarryx_u64(&x55, &x56, 0x0, x17, x51);
390 fiat_25519_addcarryx_u64(&x57, &x58, x56, x18, x53);
391 fiat_25519_addcarryx_u64(&x59, &x60, 0x0, x19, x55);
392 fiat_25519_addcarryx_u64(&x61, &x62, x60, x20, x57);
393 fiat_25519_addcarryx_u64(&x63, &x64, 0x0, x49, x59);
394 fiat_25519_addcarryx_u64(&x65, &x66, x64, x50, x61);
395 x67 = ((x63 >> 51) | ((x65 << 13) & UINT64_C(0xffffffffffffffff)));
396 x68 = (x63 & UINT64_C(0x7ffffffffffff));
397 fiat_25519_addcarryx_u64(&x69, &x70, 0x0, x23, x21);
398 fiat_25519_addcarryx_u64(&x71, &x72, x70, x24, x22);
399 fiat_25519_addcarryx_u64(&x73, &x74, 0x0, x27, x69);
400 fiat_25519_addcarryx_u64(&x75, &x76, x74, x28, x71);
401 fiat_25519_addcarryx_u64(&x77, &x78, 0x0, x33, x73);
402 fiat_25519_addcarryx_u64(&x79, &x80, x78, x34, x75);
403 fiat_25519_addcarryx_u64(&x81, &x82, 0x0, x41, x77);
404 fiat_25519_addcarryx_u64(&x83, &x84, x82, x42, x79);
405 fiat_25519_addcarryx_u64(&x85, &x86, 0x0, x25, x1);
406 fiat_25519_addcarryx_u64(&x87, &x88, x86, x26, x2);
407 fiat_25519_addcarryx_u64(&x89, &x90, 0x0, x29, x85);
408 fiat_25519_addcarryx_u64(&x91, &x92, x90, x30, x87);
409 fiat_25519_addcarryx_u64(&x93, &x94, 0x0, x35, x89);
410 fiat_25519_addcarryx_u64(&x95, &x96, x94, x36, x91);
411 fiat_25519_addcarryx_u64(&x97, &x98, 0x0, x43, x93);
412 fiat_25519_addcarryx_u64(&x99, &x100, x98, x44, x95);
413 fiat_25519_addcarryx_u64(&x101, &x102, 0x0, x9, x3);
414 fiat_25519_addcarryx_u64(&x103, &x104, x102, x10, x4);
415 fiat_25519_addcarryx_u64(&x105, &x106, 0x0, x31, x101);
416 fiat_25519_addcarryx_u64(&x107, &x108, x106, x32, x103);
417 fiat_25519_addcarryx_u64(&x109, &x110, 0x0, x37, x105);
418 fiat_25519_addcarryx_u64(&x111, &x112, x110, x38, x107);
419 fiat_25519_addcarryx_u64(&x113, &x114, 0x0, x45, x109);
420 fiat_25519_addcarryx_u64(&x115, &x116, x114, x46, x111);
421 fiat_25519_addcarryx_u64(&x117, &x118, 0x0, x11, x5);
422 fiat_25519_addcarryx_u64(&x119, &x120, x118, x12, x6);
423 fiat_25519_addcarryx_u64(&x121, &x122, 0x0, x15, x117);
424 fiat_25519_addcarryx_u64(&x123, &x124, x122, x16, x119);
425 fiat_25519_addcarryx_u64(&x125, &x126, 0x0, x39, x121);
426 fiat_25519_addcarryx_u64(&x127, &x128, x126, x40, x123);
427 fiat_25519_addcarryx_u64(&x129, &x130, 0x0, x47, x125);
428 fiat_25519_addcarryx_u64(&x131, &x132, x130, x48, x127);
429 fiat_25519_addcarryx_u64(&x133, &x134, 0x0, x67, x129);
430 x135 = (x134 + x131);
431 x136 = ((x133 >> 51) | ((x135 << 13) & UINT64_C(0xffffffffffffffff)));
432 x137 = (x133 & UINT64_C(0x7ffffffffffff));
433 fiat_25519_addcarryx_u64(&x138, &x139, 0x0, x136, x113);
434 x140 = (x139 + x115);
435 x141 = ((x138 >> 51) | ((x140 << 13) & UINT64_C(0xffffffffffffffff)));
436 x142 = (x138 & UINT64_C(0x7ffffffffffff));
437 fiat_25519_addcarryx_u64(&x143, &x144, 0x0, x141, x97);
438 x145 = (x144 + x99);
439 x146 = ((x143 >> 51) | ((x145 << 13) & UINT64_C(0xffffffffffffffff)));
440 x147 = (x143 & UINT64_C(0x7ffffffffffff));
441 fiat_25519_addcarryx_u64(&x148, &x149, 0x0, x146, x81);
442 x150 = (x149 + x83);
443 x151 = ((x148 >> 51) | ((x150 << 13) & UINT64_C(0xffffffffffffffff)));
444 x152 = (x148 & UINT64_C(0x7ffffffffffff));
445 x153 = (x151 * UINT8_C(0x13));
446 x154 = (x68 + x153);
447 x155 = (x154 >> 51);
448 x156 = (x154 & UINT64_C(0x7ffffffffffff));
449 x157 = (x155 + x137);
450 x158 = (fiat_25519_uint1)(x157 >> 51);
451 x159 = (x157 & UINT64_C(0x7ffffffffffff));
452 x160 = (x158 + x142);
453 out1[0] = x156;
454 out1[1] = x159;
455 out1[2] = x160;
456 out1[3] = x147;
457 out1[4] = x152;
458 }
459
460 /*
461 * The function fiat_25519_carry_square squares a field element and reduces the result.
462 *
463 * Postconditions:
464 * eval out1 mod m = (eval arg1 * eval arg1) mod m
465 *
466 */
fiat_25519_carry_square(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)467 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
468 uint64_t x1;
469 uint64_t x2;
470 uint64_t x3;
471 uint64_t x4;
472 uint64_t x5;
473 uint64_t x6;
474 uint64_t x7;
475 uint64_t x8;
476 uint64_t x9;
477 uint64_t x10;
478 uint64_t x11;
479 uint64_t x12;
480 uint64_t x13;
481 uint64_t x14;
482 uint64_t x15;
483 uint64_t x16;
484 uint64_t x17;
485 uint64_t x18;
486 uint64_t x19;
487 uint64_t x20;
488 uint64_t x21;
489 uint64_t x22;
490 uint64_t x23;
491 uint64_t x24;
492 uint64_t x25;
493 uint64_t x26;
494 uint64_t x27;
495 uint64_t x28;
496 uint64_t x29;
497 uint64_t x30;
498 uint64_t x31;
499 uint64_t x32;
500 uint64_t x33;
501 uint64_t x34;
502 uint64_t x35;
503 uint64_t x36;
504 uint64_t x37;
505 uint64_t x38;
506 uint64_t x39;
507 fiat_25519_uint1 x40;
508 uint64_t x41;
509 fiat_25519_uint1 x42;
510 uint64_t x43;
511 fiat_25519_uint1 x44;
512 uint64_t x45;
513 fiat_25519_uint1 x46;
514 uint64_t x47;
515 uint64_t x48;
516 uint64_t x49;
517 fiat_25519_uint1 x50;
518 uint64_t x51;
519 fiat_25519_uint1 x52;
520 uint64_t x53;
521 fiat_25519_uint1 x54;
522 uint64_t x55;
523 fiat_25519_uint1 x56;
524 uint64_t x57;
525 fiat_25519_uint1 x58;
526 uint64_t x59;
527 fiat_25519_uint1 x60;
528 uint64_t x61;
529 fiat_25519_uint1 x62;
530 uint64_t x63;
531 fiat_25519_uint1 x64;
532 uint64_t x65;
533 fiat_25519_uint1 x66;
534 uint64_t x67;
535 fiat_25519_uint1 x68;
536 uint64_t x69;
537 fiat_25519_uint1 x70;
538 uint64_t x71;
539 fiat_25519_uint1 x72;
540 uint64_t x73;
541 fiat_25519_uint1 x74;
542 uint64_t x75;
543 fiat_25519_uint1 x76;
544 uint64_t x77;
545 fiat_25519_uint1 x78;
546 uint64_t x79;
547 fiat_25519_uint1 x80;
548 uint64_t x81;
549 fiat_25519_uint1 x82;
550 uint64_t x83;
551 uint64_t x84;
552 uint64_t x85;
553 uint64_t x86;
554 fiat_25519_uint1 x87;
555 uint64_t x88;
556 uint64_t x89;
557 uint64_t x90;
558 uint64_t x91;
559 fiat_25519_uint1 x92;
560 uint64_t x93;
561 uint64_t x94;
562 uint64_t x95;
563 uint64_t x96;
564 fiat_25519_uint1 x97;
565 uint64_t x98;
566 uint64_t x99;
567 uint64_t x100;
568 uint64_t x101;
569 uint64_t x102;
570 uint64_t x103;
571 uint64_t x104;
572 uint64_t x105;
573 fiat_25519_uint1 x106;
574 uint64_t x107;
575 uint64_t x108;
576 x1 = ((arg1[4]) * UINT8_C(0x13));
577 x2 = (x1 * 0x2);
578 x3 = ((arg1[4]) * 0x2);
579 x4 = ((arg1[3]) * UINT8_C(0x13));
580 x5 = (x4 * 0x2);
581 x6 = ((arg1[3]) * 0x2);
582 x7 = ((arg1[2]) * 0x2);
583 x8 = ((arg1[1]) * 0x2);
584 fiat_25519_mulx_u64(&x9, &x10, (arg1[4]), x1);
585 fiat_25519_mulx_u64(&x11, &x12, (arg1[3]), x2);
586 fiat_25519_mulx_u64(&x13, &x14, (arg1[3]), x4);
587 fiat_25519_mulx_u64(&x15, &x16, (arg1[2]), x2);
588 fiat_25519_mulx_u64(&x17, &x18, (arg1[2]), x5);
589 fiat_25519_mulx_u64(&x19, &x20, (arg1[2]), (arg1[2]));
590 fiat_25519_mulx_u64(&x21, &x22, (arg1[1]), x2);
591 fiat_25519_mulx_u64(&x23, &x24, (arg1[1]), x6);
592 fiat_25519_mulx_u64(&x25, &x26, (arg1[1]), x7);
593 fiat_25519_mulx_u64(&x27, &x28, (arg1[1]), (arg1[1]));
594 fiat_25519_mulx_u64(&x29, &x30, (arg1[0]), x3);
595 fiat_25519_mulx_u64(&x31, &x32, (arg1[0]), x6);
596 fiat_25519_mulx_u64(&x33, &x34, (arg1[0]), x7);
597 fiat_25519_mulx_u64(&x35, &x36, (arg1[0]), x8);
598 fiat_25519_mulx_u64(&x37, &x38, (arg1[0]), (arg1[0]));
599 fiat_25519_addcarryx_u64(&x39, &x40, 0x0, x21, x17);
600 fiat_25519_addcarryx_u64(&x41, &x42, x40, x22, x18);
601 fiat_25519_addcarryx_u64(&x43, &x44, 0x0, x37, x39);
602 fiat_25519_addcarryx_u64(&x45, &x46, x44, x38, x41);
603 x47 = ((x43 >> 51) | ((x45 << 13) & UINT64_C(0xffffffffffffffff)));
604 x48 = (x43 & UINT64_C(0x7ffffffffffff));
605 fiat_25519_addcarryx_u64(&x49, &x50, 0x0, x23, x19);
606 fiat_25519_addcarryx_u64(&x51, &x52, x50, x24, x20);
607 fiat_25519_addcarryx_u64(&x53, &x54, 0x0, x29, x49);
608 fiat_25519_addcarryx_u64(&x55, &x56, x54, x30, x51);
609 fiat_25519_addcarryx_u64(&x57, &x58, 0x0, x25, x9);
610 fiat_25519_addcarryx_u64(&x59, &x60, x58, x26, x10);
611 fiat_25519_addcarryx_u64(&x61, &x62, 0x0, x31, x57);
612 fiat_25519_addcarryx_u64(&x63, &x64, x62, x32, x59);
613 fiat_25519_addcarryx_u64(&x65, &x66, 0x0, x27, x11);
614 fiat_25519_addcarryx_u64(&x67, &x68, x66, x28, x12);
615 fiat_25519_addcarryx_u64(&x69, &x70, 0x0, x33, x65);
616 fiat_25519_addcarryx_u64(&x71, &x72, x70, x34, x67);
617 fiat_25519_addcarryx_u64(&x73, &x74, 0x0, x15, x13);
618 fiat_25519_addcarryx_u64(&x75, &x76, x74, x16, x14);
619 fiat_25519_addcarryx_u64(&x77, &x78, 0x0, x35, x73);
620 fiat_25519_addcarryx_u64(&x79, &x80, x78, x36, x75);
621 fiat_25519_addcarryx_u64(&x81, &x82, 0x0, x47, x77);
622 x83 = (x82 + x79);
623 x84 = ((x81 >> 51) | ((x83 << 13) & UINT64_C(0xffffffffffffffff)));
624 x85 = (x81 & UINT64_C(0x7ffffffffffff));
625 fiat_25519_addcarryx_u64(&x86, &x87, 0x0, x84, x69);
626 x88 = (x87 + x71);
627 x89 = ((x86 >> 51) | ((x88 << 13) & UINT64_C(0xffffffffffffffff)));
628 x90 = (x86 & UINT64_C(0x7ffffffffffff));
629 fiat_25519_addcarryx_u64(&x91, &x92, 0x0, x89, x61);
630 x93 = (x92 + x63);
631 x94 = ((x91 >> 51) | ((x93 << 13) & UINT64_C(0xffffffffffffffff)));
632 x95 = (x91 & UINT64_C(0x7ffffffffffff));
633 fiat_25519_addcarryx_u64(&x96, &x97, 0x0, x94, x53);
634 x98 = (x97 + x55);
635 x99 = ((x96 >> 51) | ((x98 << 13) & UINT64_C(0xffffffffffffffff)));
636 x100 = (x96 & UINT64_C(0x7ffffffffffff));
637 x101 = (x99 * UINT8_C(0x13));
638 x102 = (x48 + x101);
639 x103 = (x102 >> 51);
640 x104 = (x102 & UINT64_C(0x7ffffffffffff));
641 x105 = (x103 + x85);
642 x106 = (fiat_25519_uint1)(x105 >> 51);
643 x107 = (x105 & UINT64_C(0x7ffffffffffff));
644 x108 = (x106 + x90);
645 out1[0] = x104;
646 out1[1] = x107;
647 out1[2] = x108;
648 out1[3] = x95;
649 out1[4] = x100;
650 }
651
652 /*
653 * The function fiat_25519_carry reduces a field element.
654 *
655 * Postconditions:
656 * eval out1 mod m = eval arg1 mod m
657 *
658 */
fiat_25519_carry(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)659 static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
660 uint64_t x1;
661 uint64_t x2;
662 uint64_t x3;
663 uint64_t x4;
664 uint64_t x5;
665 uint64_t x6;
666 uint64_t x7;
667 uint64_t x8;
668 uint64_t x9;
669 uint64_t x10;
670 uint64_t x11;
671 uint64_t x12;
672 x1 = (arg1[0]);
673 x2 = ((x1 >> 51) + (arg1[1]));
674 x3 = ((x2 >> 51) + (arg1[2]));
675 x4 = ((x3 >> 51) + (arg1[3]));
676 x5 = ((x4 >> 51) + (arg1[4]));
677 x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * UINT8_C(0x13)));
678 x7 = ((fiat_25519_uint1)(x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff)));
679 x8 = (x6 & UINT64_C(0x7ffffffffffff));
680 x9 = (x7 & UINT64_C(0x7ffffffffffff));
681 x10 = ((fiat_25519_uint1)(x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff)));
682 x11 = (x4 & UINT64_C(0x7ffffffffffff));
683 x12 = (x5 & UINT64_C(0x7ffffffffffff));
684 out1[0] = x8;
685 out1[1] = x9;
686 out1[2] = x10;
687 out1[3] = x11;
688 out1[4] = x12;
689 }
690
691 /*
692 * The function fiat_25519_add adds two field elements.
693 *
694 * Postconditions:
695 * eval out1 mod m = (eval arg1 + eval arg2) mod m
696 *
697 */
fiat_25519_add(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)698 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) {
699 uint64_t x1;
700 uint64_t x2;
701 uint64_t x3;
702 uint64_t x4;
703 uint64_t x5;
704 x1 = ((arg1[0]) + (arg2[0]));
705 x2 = ((arg1[1]) + (arg2[1]));
706 x3 = ((arg1[2]) + (arg2[2]));
707 x4 = ((arg1[3]) + (arg2[3]));
708 x5 = ((arg1[4]) + (arg2[4]));
709 out1[0] = x1;
710 out1[1] = x2;
711 out1[2] = x3;
712 out1[3] = x4;
713 out1[4] = x5;
714 }
715
716 /*
717 * The function fiat_25519_sub subtracts two field elements.
718 *
719 * Postconditions:
720 * eval out1 mod m = (eval arg1 - eval arg2) mod m
721 *
722 */
fiat_25519_sub(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1,const fiat_25519_tight_field_element arg2)723 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) {
724 uint64_t x1;
725 uint64_t x2;
726 uint64_t x3;
727 uint64_t x4;
728 uint64_t x5;
729 x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0]));
730 x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1]));
731 x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2]));
732 x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3]));
733 x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4]));
734 out1[0] = x1;
735 out1[1] = x2;
736 out1[2] = x3;
737 out1[3] = x4;
738 out1[4] = x5;
739 }
740
741 /*
742 * The function fiat_25519_opp negates a field element.
743 *
744 * Postconditions:
745 * eval out1 mod m = -eval arg1 mod m
746 *
747 */
fiat_25519_opp(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1)748 static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) {
749 uint64_t x1;
750 uint64_t x2;
751 uint64_t x3;
752 uint64_t x4;
753 uint64_t x5;
754 x1 = (UINT64_C(0xfffffffffffda) - (arg1[0]));
755 x2 = (UINT64_C(0xffffffffffffe) - (arg1[1]));
756 x3 = (UINT64_C(0xffffffffffffe) - (arg1[2]));
757 x4 = (UINT64_C(0xffffffffffffe) - (arg1[3]));
758 x5 = (UINT64_C(0xffffffffffffe) - (arg1[4]));
759 out1[0] = x1;
760 out1[1] = x2;
761 out1[2] = x3;
762 out1[3] = x4;
763 out1[4] = x5;
764 }
765
766 /*
767 * The function fiat_25519_selectznz is a multi-limb conditional select.
768 *
769 * Postconditions:
770 * out1 = (if arg1 = 0 then arg2 else arg3)
771 *
772 * Input Bounds:
773 * arg1: [0x0 ~> 0x1]
774 * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
775 * arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
776 * Output Bounds:
777 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
778 */
fiat_25519_selectznz(uint64_t out1[5],fiat_25519_uint1 arg1,const uint64_t arg2[5],const uint64_t arg3[5])779 static FIAT_25519_FIAT_INLINE void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const uint64_t arg2[5], const uint64_t arg3[5]) {
780 uint64_t x1;
781 uint64_t x2;
782 uint64_t x3;
783 uint64_t x4;
784 uint64_t x5;
785 fiat_25519_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0]));
786 fiat_25519_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1]));
787 fiat_25519_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2]));
788 fiat_25519_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3]));
789 fiat_25519_cmovznz_u64(&x5, arg1, (arg2[4]), (arg3[4]));
790 out1[0] = x1;
791 out1[1] = x2;
792 out1[2] = x3;
793 out1[3] = x4;
794 out1[4] = x5;
795 }
796
797 /*
798 * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
799 *
800 * Postconditions:
801 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
802 *
803 * Output Bounds:
804 * 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]]
805 */
fiat_25519_to_bytes(uint8_t out1[32],const fiat_25519_tight_field_element arg1)806 static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) {
807 uint64_t x1;
808 fiat_25519_uint1 x2;
809 uint64_t x3;
810 fiat_25519_uint1 x4;
811 uint64_t x5;
812 fiat_25519_uint1 x6;
813 uint64_t x7;
814 fiat_25519_uint1 x8;
815 uint64_t x9;
816 fiat_25519_uint1 x10;
817 uint64_t x11;
818 uint64_t x12;
819 fiat_25519_uint1 x13;
820 uint64_t x14;
821 fiat_25519_uint1 x15;
822 uint64_t x16;
823 fiat_25519_uint1 x17;
824 uint64_t x18;
825 fiat_25519_uint1 x19;
826 uint64_t x20;
827 fiat_25519_uint1 x21;
828 uint64_t x22;
829 uint64_t x23;
830 uint64_t x24;
831 uint64_t x25;
832 uint8_t x26;
833 uint64_t x27;
834 uint8_t x28;
835 uint64_t x29;
836 uint8_t x30;
837 uint64_t x31;
838 uint8_t x32;
839 uint64_t x33;
840 uint8_t x34;
841 uint64_t x35;
842 uint8_t x36;
843 uint8_t x37;
844 uint64_t x38;
845 uint8_t x39;
846 uint64_t x40;
847 uint8_t x41;
848 uint64_t x42;
849 uint8_t x43;
850 uint64_t x44;
851 uint8_t x45;
852 uint64_t x46;
853 uint8_t x47;
854 uint64_t x48;
855 uint8_t x49;
856 uint8_t x50;
857 uint64_t x51;
858 uint8_t x52;
859 uint64_t x53;
860 uint8_t x54;
861 uint64_t x55;
862 uint8_t x56;
863 uint64_t x57;
864 uint8_t x58;
865 uint64_t x59;
866 uint8_t x60;
867 uint64_t x61;
868 uint8_t x62;
869 uint64_t x63;
870 uint8_t x64;
871 fiat_25519_uint1 x65;
872 uint64_t x66;
873 uint8_t x67;
874 uint64_t x68;
875 uint8_t x69;
876 uint64_t x70;
877 uint8_t x71;
878 uint64_t x72;
879 uint8_t x73;
880 uint64_t x74;
881 uint8_t x75;
882 uint64_t x76;
883 uint8_t x77;
884 uint8_t x78;
885 uint64_t x79;
886 uint8_t x80;
887 uint64_t x81;
888 uint8_t x82;
889 uint64_t x83;
890 uint8_t x84;
891 uint64_t x85;
892 uint8_t x86;
893 uint64_t x87;
894 uint8_t x88;
895 uint64_t x89;
896 uint8_t x90;
897 uint8_t x91;
898 fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed));
899 fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff));
900 fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff));
901 fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff));
902 fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff));
903 fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff));
904 fiat_25519_addcarryx_u51(&x12, &x13, 0x0, x1, (x11 & UINT64_C(0x7ffffffffffed)));
905 fiat_25519_addcarryx_u51(&x14, &x15, x13, x3, (x11 & UINT64_C(0x7ffffffffffff)));
906 fiat_25519_addcarryx_u51(&x16, &x17, x15, x5, (x11 & UINT64_C(0x7ffffffffffff)));
907 fiat_25519_addcarryx_u51(&x18, &x19, x17, x7, (x11 & UINT64_C(0x7ffffffffffff)));
908 fiat_25519_addcarryx_u51(&x20, &x21, x19, x9, (x11 & UINT64_C(0x7ffffffffffff)));
909 x22 = (x20 << 4);
910 x23 = (x18 * (uint64_t)0x2);
911 x24 = (x16 << 6);
912 x25 = (x14 << 3);
913 x26 = (uint8_t)(x12 & UINT8_C(0xff));
914 x27 = (x12 >> 8);
915 x28 = (uint8_t)(x27 & UINT8_C(0xff));
916 x29 = (x27 >> 8);
917 x30 = (uint8_t)(x29 & UINT8_C(0xff));
918 x31 = (x29 >> 8);
919 x32 = (uint8_t)(x31 & UINT8_C(0xff));
920 x33 = (x31 >> 8);
921 x34 = (uint8_t)(x33 & UINT8_C(0xff));
922 x35 = (x33 >> 8);
923 x36 = (uint8_t)(x35 & UINT8_C(0xff));
924 x37 = (uint8_t)(x35 >> 8);
925 x38 = (x25 + (uint64_t)x37);
926 x39 = (uint8_t)(x38 & UINT8_C(0xff));
927 x40 = (x38 >> 8);
928 x41 = (uint8_t)(x40 & UINT8_C(0xff));
929 x42 = (x40 >> 8);
930 x43 = (uint8_t)(x42 & UINT8_C(0xff));
931 x44 = (x42 >> 8);
932 x45 = (uint8_t)(x44 & UINT8_C(0xff));
933 x46 = (x44 >> 8);
934 x47 = (uint8_t)(x46 & UINT8_C(0xff));
935 x48 = (x46 >> 8);
936 x49 = (uint8_t)(x48 & UINT8_C(0xff));
937 x50 = (uint8_t)(x48 >> 8);
938 x51 = (x24 + (uint64_t)x50);
939 x52 = (uint8_t)(x51 & UINT8_C(0xff));
940 x53 = (x51 >> 8);
941 x54 = (uint8_t)(x53 & UINT8_C(0xff));
942 x55 = (x53 >> 8);
943 x56 = (uint8_t)(x55 & UINT8_C(0xff));
944 x57 = (x55 >> 8);
945 x58 = (uint8_t)(x57 & UINT8_C(0xff));
946 x59 = (x57 >> 8);
947 x60 = (uint8_t)(x59 & UINT8_C(0xff));
948 x61 = (x59 >> 8);
949 x62 = (uint8_t)(x61 & UINT8_C(0xff));
950 x63 = (x61 >> 8);
951 x64 = (uint8_t)(x63 & UINT8_C(0xff));
952 x65 = (fiat_25519_uint1)(x63 >> 8);
953 x66 = (x23 + (uint64_t)x65);
954 x67 = (uint8_t)(x66 & UINT8_C(0xff));
955 x68 = (x66 >> 8);
956 x69 = (uint8_t)(x68 & UINT8_C(0xff));
957 x70 = (x68 >> 8);
958 x71 = (uint8_t)(x70 & UINT8_C(0xff));
959 x72 = (x70 >> 8);
960 x73 = (uint8_t)(x72 & UINT8_C(0xff));
961 x74 = (x72 >> 8);
962 x75 = (uint8_t)(x74 & UINT8_C(0xff));
963 x76 = (x74 >> 8);
964 x77 = (uint8_t)(x76 & UINT8_C(0xff));
965 x78 = (uint8_t)(x76 >> 8);
966 x79 = (x22 + (uint64_t)x78);
967 x80 = (uint8_t)(x79 & UINT8_C(0xff));
968 x81 = (x79 >> 8);
969 x82 = (uint8_t)(x81 & UINT8_C(0xff));
970 x83 = (x81 >> 8);
971 x84 = (uint8_t)(x83 & UINT8_C(0xff));
972 x85 = (x83 >> 8);
973 x86 = (uint8_t)(x85 & UINT8_C(0xff));
974 x87 = (x85 >> 8);
975 x88 = (uint8_t)(x87 & UINT8_C(0xff));
976 x89 = (x87 >> 8);
977 x90 = (uint8_t)(x89 & UINT8_C(0xff));
978 x91 = (uint8_t)(x89 >> 8);
979 out1[0] = x26;
980 out1[1] = x28;
981 out1[2] = x30;
982 out1[3] = x32;
983 out1[4] = x34;
984 out1[5] = x36;
985 out1[6] = x39;
986 out1[7] = x41;
987 out1[8] = x43;
988 out1[9] = x45;
989 out1[10] = x47;
990 out1[11] = x49;
991 out1[12] = x52;
992 out1[13] = x54;
993 out1[14] = x56;
994 out1[15] = x58;
995 out1[16] = x60;
996 out1[17] = x62;
997 out1[18] = x64;
998 out1[19] = x67;
999 out1[20] = x69;
1000 out1[21] = x71;
1001 out1[22] = x73;
1002 out1[23] = x75;
1003 out1[24] = x77;
1004 out1[25] = x80;
1005 out1[26] = x82;
1006 out1[27] = x84;
1007 out1[28] = x86;
1008 out1[29] = x88;
1009 out1[30] = x90;
1010 out1[31] = x91;
1011 }
1012
1013 /*
1014 * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
1015 *
1016 * Postconditions:
1017 * eval out1 mod m = bytes_eval arg1 mod m
1018 *
1019 * Input Bounds:
1020 * 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]]
1021 */
fiat_25519_from_bytes(fiat_25519_tight_field_element out1,const uint8_t arg1[32])1022 static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) {
1023 uint64_t x1;
1024 uint64_t x2;
1025 uint64_t x3;
1026 uint64_t x4;
1027 uint64_t x5;
1028 uint64_t x6;
1029 uint64_t x7;
1030 uint64_t x8;
1031 uint64_t x9;
1032 uint64_t x10;
1033 uint64_t x11;
1034 uint64_t x12;
1035 uint64_t x13;
1036 uint64_t x14;
1037 uint64_t x15;
1038 uint64_t x16;
1039 uint64_t x17;
1040 uint64_t x18;
1041 uint64_t x19;
1042 uint64_t x20;
1043 uint64_t x21;
1044 uint64_t x22;
1045 uint64_t x23;
1046 uint64_t x24;
1047 uint64_t x25;
1048 uint64_t x26;
1049 uint64_t x27;
1050 uint64_t x28;
1051 uint64_t x29;
1052 uint64_t x30;
1053 uint64_t x31;
1054 uint8_t x32;
1055 uint64_t x33;
1056 uint64_t x34;
1057 uint64_t x35;
1058 uint64_t x36;
1059 uint64_t x37;
1060 uint64_t x38;
1061 uint64_t x39;
1062 uint8_t x40;
1063 uint64_t x41;
1064 uint64_t x42;
1065 uint64_t x43;
1066 uint64_t x44;
1067 uint64_t x45;
1068 uint64_t x46;
1069 uint64_t x47;
1070 uint8_t x48;
1071 uint64_t x49;
1072 uint64_t x50;
1073 uint64_t x51;
1074 uint64_t x52;
1075 uint64_t x53;
1076 uint64_t x54;
1077 uint64_t x55;
1078 uint64_t x56;
1079 uint8_t x57;
1080 uint64_t x58;
1081 uint64_t x59;
1082 uint64_t x60;
1083 uint64_t x61;
1084 uint64_t x62;
1085 uint64_t x63;
1086 uint64_t x64;
1087 uint8_t x65;
1088 uint64_t x66;
1089 uint64_t x67;
1090 uint64_t x68;
1091 uint64_t x69;
1092 uint64_t x70;
1093 uint64_t x71;
1094 x1 = ((uint64_t)(arg1[31]) << 44);
1095 x2 = ((uint64_t)(arg1[30]) << 36);
1096 x3 = ((uint64_t)(arg1[29]) << 28);
1097 x4 = ((uint64_t)(arg1[28]) << 20);
1098 x5 = ((uint64_t)(arg1[27]) << 12);
1099 x6 = ((uint64_t)(arg1[26]) << 4);
1100 x7 = ((uint64_t)(arg1[25]) << 47);
1101 x8 = ((uint64_t)(arg1[24]) << 39);
1102 x9 = ((uint64_t)(arg1[23]) << 31);
1103 x10 = ((uint64_t)(arg1[22]) << 23);
1104 x11 = ((uint64_t)(arg1[21]) << 15);
1105 x12 = ((uint64_t)(arg1[20]) << 7);
1106 x13 = ((uint64_t)(arg1[19]) << 50);
1107 x14 = ((uint64_t)(arg1[18]) << 42);
1108 x15 = ((uint64_t)(arg1[17]) << 34);
1109 x16 = ((uint64_t)(arg1[16]) << 26);
1110 x17 = ((uint64_t)(arg1[15]) << 18);
1111 x18 = ((uint64_t)(arg1[14]) << 10);
1112 x19 = ((uint64_t)(arg1[13]) << 2);
1113 x20 = ((uint64_t)(arg1[12]) << 45);
1114 x21 = ((uint64_t)(arg1[11]) << 37);
1115 x22 = ((uint64_t)(arg1[10]) << 29);
1116 x23 = ((uint64_t)(arg1[9]) << 21);
1117 x24 = ((uint64_t)(arg1[8]) << 13);
1118 x25 = ((uint64_t)(arg1[7]) << 5);
1119 x26 = ((uint64_t)(arg1[6]) << 48);
1120 x27 = ((uint64_t)(arg1[5]) << 40);
1121 x28 = ((uint64_t)(arg1[4]) << 32);
1122 x29 = ((uint64_t)(arg1[3]) << 24);
1123 x30 = ((uint64_t)(arg1[2]) << 16);
1124 x31 = ((uint64_t)(arg1[1]) << 8);
1125 x32 = (arg1[0]);
1126 x33 = (x31 + (uint64_t)x32);
1127 x34 = (x30 + x33);
1128 x35 = (x29 + x34);
1129 x36 = (x28 + x35);
1130 x37 = (x27 + x36);
1131 x38 = (x26 + x37);
1132 x39 = (x38 & UINT64_C(0x7ffffffffffff));
1133 x40 = (uint8_t)(x38 >> 51);
1134 x41 = (x25 + (uint64_t)x40);
1135 x42 = (x24 + x41);
1136 x43 = (x23 + x42);
1137 x44 = (x22 + x43);
1138 x45 = (x21 + x44);
1139 x46 = (x20 + x45);
1140 x47 = (x46 & UINT64_C(0x7ffffffffffff));
1141 x48 = (uint8_t)(x46 >> 51);
1142 x49 = (x19 + (uint64_t)x48);
1143 x50 = (x18 + x49);
1144 x51 = (x17 + x50);
1145 x52 = (x16 + x51);
1146 x53 = (x15 + x52);
1147 x54 = (x14 + x53);
1148 x55 = (x13 + x54);
1149 x56 = (x55 & UINT64_C(0x7ffffffffffff));
1150 x57 = (uint8_t)(x55 >> 51);
1151 x58 = (x12 + (uint64_t)x57);
1152 x59 = (x11 + x58);
1153 x60 = (x10 + x59);
1154 x61 = (x9 + x60);
1155 x62 = (x8 + x61);
1156 x63 = (x7 + x62);
1157 x64 = (x63 & UINT64_C(0x7ffffffffffff));
1158 x65 = (uint8_t)(x63 >> 51);
1159 x66 = (x6 + (uint64_t)x65);
1160 x67 = (x5 + x66);
1161 x68 = (x4 + x67);
1162 x69 = (x3 + x68);
1163 x70 = (x2 + x69);
1164 x71 = (x1 + x70);
1165 out1[0] = x39;
1166 out1[1] = x47;
1167 out1[2] = x56;
1168 out1[3] = x64;
1169 out1[4] = x71;
1170 }
1171
1172 /*
1173 * The function fiat_25519_relax is the identity function converting from tight field elements to loose field elements.
1174 *
1175 * Postconditions:
1176 * out1 = arg1
1177 *
1178 */
fiat_25519_relax(fiat_25519_loose_field_element out1,const fiat_25519_tight_field_element arg1)1179 static FIAT_25519_FIAT_INLINE void fiat_25519_relax(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) {
1180 uint64_t x1;
1181 uint64_t x2;
1182 uint64_t x3;
1183 uint64_t x4;
1184 uint64_t x5;
1185 x1 = (arg1[0]);
1186 x2 = (arg1[1]);
1187 x3 = (arg1[2]);
1188 x4 = (arg1[3]);
1189 x5 = (arg1[4]);
1190 out1[0] = x1;
1191 out1[1] = x2;
1192 out1[2] = x3;
1193 out1[3] = x4;
1194 out1[4] = x5;
1195 }
1196
1197 /*
1198 * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
1199 *
1200 * Postconditions:
1201 * eval out1 mod m = (121666 * eval arg1) mod m
1202 *
1203 */
fiat_25519_carry_scmul_121666(fiat_25519_tight_field_element out1,const fiat_25519_loose_field_element arg1)1204 static FIAT_25519_FIAT_INLINE void fiat_25519_carry_scmul_121666(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) {
1205 uint64_t x1;
1206 uint64_t x2;
1207 uint64_t x3;
1208 uint64_t x4;
1209 uint64_t x5;
1210 uint64_t x6;
1211 uint64_t x7;
1212 uint64_t x8;
1213 uint64_t x9;
1214 uint64_t x10;
1215 uint64_t x11;
1216 uint64_t x12;
1217 uint64_t x13;
1218 fiat_25519_uint1 x14;
1219 uint64_t x15;
1220 uint64_t x16;
1221 uint64_t x17;
1222 uint64_t x18;
1223 fiat_25519_uint1 x19;
1224 uint64_t x20;
1225 uint64_t x21;
1226 uint64_t x22;
1227 uint64_t x23;
1228 fiat_25519_uint1 x24;
1229 uint64_t x25;
1230 uint64_t x26;
1231 uint64_t x27;
1232 uint64_t x28;
1233 fiat_25519_uint1 x29;
1234 uint64_t x30;
1235 uint64_t x31;
1236 uint64_t x32;
1237 uint64_t x33;
1238 uint64_t x34;
1239 fiat_25519_uint1 x35;
1240 uint64_t x36;
1241 uint64_t x37;
1242 fiat_25519_uint1 x38;
1243 uint64_t x39;
1244 uint64_t x40;
1245 fiat_25519_mulx_u64(&x1, &x2, UINT32_C(0x1db42), (arg1[4]));
1246 fiat_25519_mulx_u64(&x3, &x4, UINT32_C(0x1db42), (arg1[3]));
1247 fiat_25519_mulx_u64(&x5, &x6, UINT32_C(0x1db42), (arg1[2]));
1248 fiat_25519_mulx_u64(&x7, &x8, UINT32_C(0x1db42), (arg1[1]));
1249 fiat_25519_mulx_u64(&x9, &x10, UINT32_C(0x1db42), (arg1[0]));
1250 x11 = ((x9 >> 51) | ((x10 << 13) & UINT64_C(0xffffffffffffffff)));
1251 x12 = (x9 & UINT64_C(0x7ffffffffffff));
1252 fiat_25519_addcarryx_u64(&x13, &x14, 0x0, x11, x7);
1253 x15 = (x14 + x8);
1254 x16 = ((x13 >> 51) | ((x15 << 13) & UINT64_C(0xffffffffffffffff)));
1255 x17 = (x13 & UINT64_C(0x7ffffffffffff));
1256 fiat_25519_addcarryx_u64(&x18, &x19, 0x0, x16, x5);
1257 x20 = (x19 + x6);
1258 x21 = ((x18 >> 51) | ((x20 << 13) & UINT64_C(0xffffffffffffffff)));
1259 x22 = (x18 & UINT64_C(0x7ffffffffffff));
1260 fiat_25519_addcarryx_u64(&x23, &x24, 0x0, x21, x3);
1261 x25 = (x24 + x4);
1262 x26 = ((x23 >> 51) | ((x25 << 13) & UINT64_C(0xffffffffffffffff)));
1263 x27 = (x23 & UINT64_C(0x7ffffffffffff));
1264 fiat_25519_addcarryx_u64(&x28, &x29, 0x0, x26, x1);
1265 x30 = (x29 + x2);
1266 x31 = ((x28 >> 51) | ((x30 << 13) & UINT64_C(0xffffffffffffffff)));
1267 x32 = (x28 & UINT64_C(0x7ffffffffffff));
1268 x33 = (x31 * UINT8_C(0x13));
1269 x34 = (x12 + x33);
1270 x35 = (fiat_25519_uint1)(x34 >> 51);
1271 x36 = (x34 & UINT64_C(0x7ffffffffffff));
1272 x37 = (x35 + x17);
1273 x38 = (fiat_25519_uint1)(x37 >> 51);
1274 x39 = (x37 & UINT64_C(0x7ffffffffffff));
1275 x40 = (x38 + x22);
1276 out1[0] = x36;
1277 out1[1] = x39;
1278 out1[2] = x40;
1279 out1[3] = x27;
1280 out1[4] = x32;
1281 }
1282