/src/boringssl/third_party/fiat/curve25519_64.h
Line | Count | Source (jump to first uncovered line) |
1 | | /* 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 */ |
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 | | typedef unsigned char fiat_25519_uint1; |
17 | | typedef signed char fiat_25519_int1; |
18 | | #if defined(__GNUC__) || defined(__clang__) |
19 | | # define FIAT_25519_FIAT_EXTENSION __extension__ |
20 | | # define FIAT_25519_FIAT_INLINE __inline__ |
21 | | #else |
22 | | # define FIAT_25519_FIAT_EXTENSION |
23 | | # define FIAT_25519_FIAT_INLINE |
24 | | #endif |
25 | | |
26 | | FIAT_25519_FIAT_EXTENSION typedef signed __int128 fiat_25519_int128; |
27 | | FIAT_25519_FIAT_EXTENSION typedef unsigned __int128 fiat_25519_uint128; |
28 | | |
29 | | /* The type fiat_25519_loose_field_element is a field element with loose bounds. */ |
30 | | /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */ |
31 | | typedef uint64_t fiat_25519_loose_field_element[5]; |
32 | | |
33 | | /* The type fiat_25519_tight_field_element is a field element with tight bounds. */ |
34 | | /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */ |
35 | | typedef uint64_t fiat_25519_tight_field_element[5]; |
36 | | |
37 | | #if (-1 & 3) != 3 |
38 | | #error "This code only works on a two's complement system" |
39 | | #endif |
40 | | |
41 | | #if !defined(FIAT_25519_NO_ASM) && (defined(__GNUC__) || defined(__clang__)) |
42 | 2 | static __inline__ uint64_t fiat_25519_value_barrier_u64(uint64_t a) { |
43 | 2 | __asm__("" : "+r"(a) : /* no inputs */); |
44 | 2 | return a; |
45 | 2 | } |
46 | | #else |
47 | | # define fiat_25519_value_barrier_u64(x) (x) |
48 | | #endif |
49 | | |
50 | | |
51 | | /* |
52 | | * The function fiat_25519_addcarryx_u51 is an addition with carry. |
53 | | * |
54 | | * Postconditions: |
55 | | * out1 = (arg1 + arg2 + arg3) mod 2^51 |
56 | | * out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋ |
57 | | * |
58 | | * Input Bounds: |
59 | | * arg1: [0x0 ~> 0x1] |
60 | | * arg2: [0x0 ~> 0x7ffffffffffff] |
61 | | * arg3: [0x0 ~> 0x7ffffffffffff] |
62 | | * Output Bounds: |
63 | | * out1: [0x0 ~> 0x7ffffffffffff] |
64 | | * out2: [0x0 ~> 0x1] |
65 | | */ |
66 | 5 | 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) { |
67 | 5 | uint64_t x1; |
68 | 5 | uint64_t x2; |
69 | 5 | fiat_25519_uint1 x3; |
70 | 5 | x1 = ((arg1 + arg2) + arg3); |
71 | 5 | x2 = (x1 & UINT64_C(0x7ffffffffffff)); |
72 | 5 | x3 = (fiat_25519_uint1)(x1 >> 51); |
73 | 5 | *out1 = x2; |
74 | 5 | *out2 = x3; |
75 | 5 | } |
76 | | |
77 | | /* |
78 | | * The function fiat_25519_subborrowx_u51 is a subtraction with borrow. |
79 | | * |
80 | | * Postconditions: |
81 | | * out1 = (-arg1 + arg2 + -arg3) mod 2^51 |
82 | | * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋ |
83 | | * |
84 | | * Input Bounds: |
85 | | * arg1: [0x0 ~> 0x1] |
86 | | * arg2: [0x0 ~> 0x7ffffffffffff] |
87 | | * arg3: [0x0 ~> 0x7ffffffffffff] |
88 | | * Output Bounds: |
89 | | * out1: [0x0 ~> 0x7ffffffffffff] |
90 | | * out2: [0x0 ~> 0x1] |
91 | | */ |
92 | 5 | 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) { |
93 | 5 | int64_t x1; |
94 | 5 | fiat_25519_int1 x2; |
95 | 5 | uint64_t x3; |
96 | 5 | x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3); |
97 | 5 | x2 = (fiat_25519_int1)(x1 >> 51); |
98 | 5 | x3 = (x1 & UINT64_C(0x7ffffffffffff)); |
99 | 5 | *out1 = x3; |
100 | 5 | *out2 = (fiat_25519_uint1)(0x0 - x2); |
101 | 5 | } |
102 | | |
103 | | /* |
104 | | * The function fiat_25519_cmovznz_u64 is a single-word conditional move. |
105 | | * |
106 | | * Postconditions: |
107 | | * out1 = (if arg1 = 0 then arg2 else arg3) |
108 | | * |
109 | | * Input Bounds: |
110 | | * arg1: [0x0 ~> 0x1] |
111 | | * arg2: [0x0 ~> 0xffffffffffffffff] |
112 | | * arg3: [0x0 ~> 0xffffffffffffffff] |
113 | | * Output Bounds: |
114 | | * out1: [0x0 ~> 0xffffffffffffffff] |
115 | | */ |
116 | 1 | static FIAT_25519_FIAT_INLINE void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { |
117 | 1 | fiat_25519_uint1 x1; |
118 | 1 | uint64_t x2; |
119 | 1 | uint64_t x3; |
120 | 1 | x1 = (!(!arg1)); |
121 | 1 | x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); |
122 | 1 | x3 = ((fiat_25519_value_barrier_u64(x2) & arg3) | (fiat_25519_value_barrier_u64((~x2)) & arg2)); |
123 | 1 | *out1 = x3; |
124 | 1 | } |
125 | | |
126 | | /* |
127 | | * The function fiat_25519_carry_mul multiplies two field elements and reduces the result. |
128 | | * |
129 | | * Postconditions: |
130 | | * eval out1 mod m = (eval arg1 * eval arg2) mod m |
131 | | * |
132 | | */ |
133 | 473 | 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) { |
134 | 473 | fiat_25519_uint128 x1; |
135 | 473 | fiat_25519_uint128 x2; |
136 | 473 | fiat_25519_uint128 x3; |
137 | 473 | fiat_25519_uint128 x4; |
138 | 473 | fiat_25519_uint128 x5; |
139 | 473 | fiat_25519_uint128 x6; |
140 | 473 | fiat_25519_uint128 x7; |
141 | 473 | fiat_25519_uint128 x8; |
142 | 473 | fiat_25519_uint128 x9; |
143 | 473 | fiat_25519_uint128 x10; |
144 | 473 | fiat_25519_uint128 x11; |
145 | 473 | fiat_25519_uint128 x12; |
146 | 473 | fiat_25519_uint128 x13; |
147 | 473 | fiat_25519_uint128 x14; |
148 | 473 | fiat_25519_uint128 x15; |
149 | 473 | fiat_25519_uint128 x16; |
150 | 473 | fiat_25519_uint128 x17; |
151 | 473 | fiat_25519_uint128 x18; |
152 | 473 | fiat_25519_uint128 x19; |
153 | 473 | fiat_25519_uint128 x20; |
154 | 473 | fiat_25519_uint128 x21; |
155 | 473 | fiat_25519_uint128 x22; |
156 | 473 | fiat_25519_uint128 x23; |
157 | 473 | fiat_25519_uint128 x24; |
158 | 473 | fiat_25519_uint128 x25; |
159 | 473 | fiat_25519_uint128 x26; |
160 | 473 | uint64_t x27; |
161 | 473 | uint64_t x28; |
162 | 473 | fiat_25519_uint128 x29; |
163 | 473 | fiat_25519_uint128 x30; |
164 | 473 | fiat_25519_uint128 x31; |
165 | 473 | fiat_25519_uint128 x32; |
166 | 473 | fiat_25519_uint128 x33; |
167 | 473 | uint64_t x34; |
168 | 473 | uint64_t x35; |
169 | 473 | fiat_25519_uint128 x36; |
170 | 473 | uint64_t x37; |
171 | 473 | uint64_t x38; |
172 | 473 | fiat_25519_uint128 x39; |
173 | 473 | uint64_t x40; |
174 | 473 | uint64_t x41; |
175 | 473 | fiat_25519_uint128 x42; |
176 | 473 | uint64_t x43; |
177 | 473 | uint64_t x44; |
178 | 473 | uint64_t x45; |
179 | 473 | uint64_t x46; |
180 | 473 | uint64_t x47; |
181 | 473 | uint64_t x48; |
182 | 473 | uint64_t x49; |
183 | 473 | fiat_25519_uint1 x50; |
184 | 473 | uint64_t x51; |
185 | 473 | uint64_t x52; |
186 | 473 | x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * UINT8_C(0x13))); |
187 | 473 | x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * UINT8_C(0x13))); |
188 | 473 | x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * UINT8_C(0x13))); |
189 | 473 | x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * UINT8_C(0x13))); |
190 | 473 | x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * UINT8_C(0x13))); |
191 | 473 | x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * UINT8_C(0x13))); |
192 | 473 | x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * UINT8_C(0x13))); |
193 | 473 | x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * UINT8_C(0x13))); |
194 | 473 | x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * UINT8_C(0x13))); |
195 | 473 | x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * UINT8_C(0x13))); |
196 | 473 | x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0])); |
197 | 473 | x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1])); |
198 | 473 | x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0])); |
199 | 473 | x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2])); |
200 | 473 | x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1])); |
201 | 473 | x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0])); |
202 | 473 | x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3])); |
203 | 473 | x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2])); |
204 | 473 | x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1])); |
205 | 473 | x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0])); |
206 | 473 | x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4])); |
207 | 473 | x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3])); |
208 | 473 | x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2])); |
209 | 473 | x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1])); |
210 | 473 | x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0])); |
211 | 473 | x26 = (x25 + (x10 + (x9 + (x7 + x4)))); |
212 | 473 | x27 = (uint64_t)(x26 >> 51); |
213 | 473 | x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff)); |
214 | 473 | x29 = (x21 + (x17 + (x14 + (x12 + x11)))); |
215 | 473 | x30 = (x22 + (x18 + (x15 + (x13 + x1)))); |
216 | 473 | x31 = (x23 + (x19 + (x16 + (x5 + x2)))); |
217 | 473 | x32 = (x24 + (x20 + (x8 + (x6 + x3)))); |
218 | 473 | x33 = (x27 + x32); |
219 | 473 | x34 = (uint64_t)(x33 >> 51); |
220 | 473 | x35 = (uint64_t)(x33 & UINT64_C(0x7ffffffffffff)); |
221 | 473 | x36 = (x34 + x31); |
222 | 473 | x37 = (uint64_t)(x36 >> 51); |
223 | 473 | x38 = (uint64_t)(x36 & UINT64_C(0x7ffffffffffff)); |
224 | 473 | x39 = (x37 + x30); |
225 | 473 | x40 = (uint64_t)(x39 >> 51); |
226 | 473 | x41 = (uint64_t)(x39 & UINT64_C(0x7ffffffffffff)); |
227 | 473 | x42 = (x40 + x29); |
228 | 473 | x43 = (uint64_t)(x42 >> 51); |
229 | 473 | x44 = (uint64_t)(x42 & UINT64_C(0x7ffffffffffff)); |
230 | 473 | x45 = (x43 * UINT8_C(0x13)); |
231 | 473 | x46 = (x28 + x45); |
232 | 473 | x47 = (x46 >> 51); |
233 | 473 | x48 = (x46 & UINT64_C(0x7ffffffffffff)); |
234 | 473 | x49 = (x47 + x35); |
235 | 473 | x50 = (fiat_25519_uint1)(x49 >> 51); |
236 | 473 | x51 = (x49 & UINT64_C(0x7ffffffffffff)); |
237 | 473 | x52 = (x50 + x38); |
238 | 473 | out1[0] = x48; |
239 | 473 | out1[1] = x51; |
240 | 473 | out1[2] = x52; |
241 | 473 | out1[3] = x41; |
242 | 473 | out1[4] = x44; |
243 | 473 | } |
244 | | |
245 | | /* |
246 | | * The function fiat_25519_carry_square squares a field element and reduces the result. |
247 | | * |
248 | | * Postconditions: |
249 | | * eval out1 mod m = (eval arg1 * eval arg1) mod m |
250 | | * |
251 | | */ |
252 | 270 | static FIAT_25519_FIAT_INLINE void fiat_25519_carry_square(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { |
253 | 270 | uint64_t x1; |
254 | 270 | uint64_t x2; |
255 | 270 | uint64_t x3; |
256 | 270 | uint64_t x4; |
257 | 270 | uint64_t x5; |
258 | 270 | uint64_t x6; |
259 | 270 | uint64_t x7; |
260 | 270 | uint64_t x8; |
261 | 270 | fiat_25519_uint128 x9; |
262 | 270 | fiat_25519_uint128 x10; |
263 | 270 | fiat_25519_uint128 x11; |
264 | 270 | fiat_25519_uint128 x12; |
265 | 270 | fiat_25519_uint128 x13; |
266 | 270 | fiat_25519_uint128 x14; |
267 | 270 | fiat_25519_uint128 x15; |
268 | 270 | fiat_25519_uint128 x16; |
269 | 270 | fiat_25519_uint128 x17; |
270 | 270 | fiat_25519_uint128 x18; |
271 | 270 | fiat_25519_uint128 x19; |
272 | 270 | fiat_25519_uint128 x20; |
273 | 270 | fiat_25519_uint128 x21; |
274 | 270 | fiat_25519_uint128 x22; |
275 | 270 | fiat_25519_uint128 x23; |
276 | 270 | fiat_25519_uint128 x24; |
277 | 270 | uint64_t x25; |
278 | 270 | uint64_t x26; |
279 | 270 | fiat_25519_uint128 x27; |
280 | 270 | fiat_25519_uint128 x28; |
281 | 270 | fiat_25519_uint128 x29; |
282 | 270 | fiat_25519_uint128 x30; |
283 | 270 | fiat_25519_uint128 x31; |
284 | 270 | uint64_t x32; |
285 | 270 | uint64_t x33; |
286 | 270 | fiat_25519_uint128 x34; |
287 | 270 | uint64_t x35; |
288 | 270 | uint64_t x36; |
289 | 270 | fiat_25519_uint128 x37; |
290 | 270 | uint64_t x38; |
291 | 270 | uint64_t x39; |
292 | 270 | fiat_25519_uint128 x40; |
293 | 270 | uint64_t x41; |
294 | 270 | uint64_t x42; |
295 | 270 | uint64_t x43; |
296 | 270 | uint64_t x44; |
297 | 270 | uint64_t x45; |
298 | 270 | uint64_t x46; |
299 | 270 | uint64_t x47; |
300 | 270 | fiat_25519_uint1 x48; |
301 | 270 | uint64_t x49; |
302 | 270 | uint64_t x50; |
303 | 270 | x1 = ((arg1[4]) * UINT8_C(0x13)); |
304 | 270 | x2 = (x1 * 0x2); |
305 | 270 | x3 = ((arg1[4]) * 0x2); |
306 | 270 | x4 = ((arg1[3]) * UINT8_C(0x13)); |
307 | 270 | x5 = (x4 * 0x2); |
308 | 270 | x6 = ((arg1[3]) * 0x2); |
309 | 270 | x7 = ((arg1[2]) * 0x2); |
310 | 270 | x8 = ((arg1[1]) * 0x2); |
311 | 270 | x9 = ((fiat_25519_uint128)(arg1[4]) * x1); |
312 | 270 | x10 = ((fiat_25519_uint128)(arg1[3]) * x2); |
313 | 270 | x11 = ((fiat_25519_uint128)(arg1[3]) * x4); |
314 | 270 | x12 = ((fiat_25519_uint128)(arg1[2]) * x2); |
315 | 270 | x13 = ((fiat_25519_uint128)(arg1[2]) * x5); |
316 | 270 | x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2])); |
317 | 270 | x15 = ((fiat_25519_uint128)(arg1[1]) * x2); |
318 | 270 | x16 = ((fiat_25519_uint128)(arg1[1]) * x6); |
319 | 270 | x17 = ((fiat_25519_uint128)(arg1[1]) * x7); |
320 | 270 | x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1])); |
321 | 270 | x19 = ((fiat_25519_uint128)(arg1[0]) * x3); |
322 | 270 | x20 = ((fiat_25519_uint128)(arg1[0]) * x6); |
323 | 270 | x21 = ((fiat_25519_uint128)(arg1[0]) * x7); |
324 | 270 | x22 = ((fiat_25519_uint128)(arg1[0]) * x8); |
325 | 270 | x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0])); |
326 | 270 | x24 = (x23 + (x15 + x13)); |
327 | 270 | x25 = (uint64_t)(x24 >> 51); |
328 | 270 | x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff)); |
329 | 270 | x27 = (x19 + (x16 + x14)); |
330 | 270 | x28 = (x20 + (x17 + x9)); |
331 | 270 | x29 = (x21 + (x18 + x10)); |
332 | 270 | x30 = (x22 + (x12 + x11)); |
333 | 270 | x31 = (x25 + x30); |
334 | 270 | x32 = (uint64_t)(x31 >> 51); |
335 | 270 | x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff)); |
336 | 270 | x34 = (x32 + x29); |
337 | 270 | x35 = (uint64_t)(x34 >> 51); |
338 | 270 | x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff)); |
339 | 270 | x37 = (x35 + x28); |
340 | 270 | x38 = (uint64_t)(x37 >> 51); |
341 | 270 | x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff)); |
342 | 270 | x40 = (x38 + x27); |
343 | 270 | x41 = (uint64_t)(x40 >> 51); |
344 | 270 | x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff)); |
345 | 270 | x43 = (x41 * UINT8_C(0x13)); |
346 | 270 | x44 = (x26 + x43); |
347 | 270 | x45 = (x44 >> 51); |
348 | 270 | x46 = (x44 & UINT64_C(0x7ffffffffffff)); |
349 | 270 | x47 = (x45 + x33); |
350 | 270 | x48 = (fiat_25519_uint1)(x47 >> 51); |
351 | 270 | x49 = (x47 & UINT64_C(0x7ffffffffffff)); |
352 | 270 | x50 = (x48 + x36); |
353 | 270 | out1[0] = x46; |
354 | 270 | out1[1] = x49; |
355 | 270 | out1[2] = x50; |
356 | 270 | out1[3] = x39; |
357 | 270 | out1[4] = x42; |
358 | 270 | } |
359 | | |
360 | | /* |
361 | | * The function fiat_25519_carry reduces a field element. |
362 | | * |
363 | | * Postconditions: |
364 | | * eval out1 mod m = eval arg1 mod m |
365 | | * |
366 | | */ |
367 | 76 | static FIAT_25519_FIAT_INLINE void fiat_25519_carry(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { |
368 | 76 | uint64_t x1; |
369 | 76 | uint64_t x2; |
370 | 76 | uint64_t x3; |
371 | 76 | uint64_t x4; |
372 | 76 | uint64_t x5; |
373 | 76 | uint64_t x6; |
374 | 76 | uint64_t x7; |
375 | 76 | uint64_t x8; |
376 | 76 | uint64_t x9; |
377 | 76 | uint64_t x10; |
378 | 76 | uint64_t x11; |
379 | 76 | uint64_t x12; |
380 | 76 | x1 = (arg1[0]); |
381 | 76 | x2 = ((x1 >> 51) + (arg1[1])); |
382 | 76 | x3 = ((x2 >> 51) + (arg1[2])); |
383 | 76 | x4 = ((x3 >> 51) + (arg1[3])); |
384 | 76 | x5 = ((x4 >> 51) + (arg1[4])); |
385 | 76 | x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * UINT8_C(0x13))); |
386 | 76 | x7 = ((fiat_25519_uint1)(x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff))); |
387 | 76 | x8 = (x6 & UINT64_C(0x7ffffffffffff)); |
388 | 76 | x9 = (x7 & UINT64_C(0x7ffffffffffff)); |
389 | 76 | x10 = ((fiat_25519_uint1)(x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff))); |
390 | 76 | x11 = (x4 & UINT64_C(0x7ffffffffffff)); |
391 | 76 | x12 = (x5 & UINT64_C(0x7ffffffffffff)); |
392 | 76 | out1[0] = x8; |
393 | 76 | out1[1] = x9; |
394 | 76 | out1[2] = x10; |
395 | 76 | out1[3] = x11; |
396 | 76 | out1[4] = x12; |
397 | 76 | } |
398 | | |
399 | | /* |
400 | | * The function fiat_25519_add adds two field elements. |
401 | | * |
402 | | * Postconditions: |
403 | | * eval out1 mod m = (eval arg1 + eval arg2) mod m |
404 | | * |
405 | | */ |
406 | 269 | 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) { |
407 | 269 | uint64_t x1; |
408 | 269 | uint64_t x2; |
409 | 269 | uint64_t x3; |
410 | 269 | uint64_t x4; |
411 | 269 | uint64_t x5; |
412 | 269 | x1 = ((arg1[0]) + (arg2[0])); |
413 | 269 | x2 = ((arg1[1]) + (arg2[1])); |
414 | 269 | x3 = ((arg1[2]) + (arg2[2])); |
415 | 269 | x4 = ((arg1[3]) + (arg2[3])); |
416 | 269 | x5 = ((arg1[4]) + (arg2[4])); |
417 | 269 | out1[0] = x1; |
418 | 269 | out1[1] = x2; |
419 | 269 | out1[2] = x3; |
420 | 269 | out1[3] = x4; |
421 | 269 | out1[4] = x5; |
422 | 269 | } |
423 | | |
424 | | /* |
425 | | * The function fiat_25519_sub subtracts two field elements. |
426 | | * |
427 | | * Postconditions: |
428 | | * eval out1 mod m = (eval arg1 - eval arg2) mod m |
429 | | * |
430 | | */ |
431 | 205 | 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) { |
432 | 205 | uint64_t x1; |
433 | 205 | uint64_t x2; |
434 | 205 | uint64_t x3; |
435 | 205 | uint64_t x4; |
436 | 205 | uint64_t x5; |
437 | 205 | x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0])); |
438 | 205 | x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1])); |
439 | 205 | x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2])); |
440 | 205 | x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3])); |
441 | 205 | x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4])); |
442 | 205 | out1[0] = x1; |
443 | 205 | out1[1] = x2; |
444 | 205 | out1[2] = x3; |
445 | 205 | out1[3] = x4; |
446 | 205 | out1[4] = x5; |
447 | 205 | } |
448 | | |
449 | | /* |
450 | | * The function fiat_25519_opp negates a field element. |
451 | | * |
452 | | * Postconditions: |
453 | | * eval out1 mod m = -eval arg1 mod m |
454 | | * |
455 | | */ |
456 | 64 | static FIAT_25519_FIAT_INLINE void fiat_25519_opp(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) { |
457 | 64 | uint64_t x1; |
458 | 64 | uint64_t x2; |
459 | 64 | uint64_t x3; |
460 | 64 | uint64_t x4; |
461 | 64 | uint64_t x5; |
462 | 64 | x1 = (UINT64_C(0xfffffffffffda) - (arg1[0])); |
463 | 64 | x2 = (UINT64_C(0xffffffffffffe) - (arg1[1])); |
464 | 64 | x3 = (UINT64_C(0xffffffffffffe) - (arg1[2])); |
465 | 64 | x4 = (UINT64_C(0xffffffffffffe) - (arg1[3])); |
466 | 64 | x5 = (UINT64_C(0xffffffffffffe) - (arg1[4])); |
467 | 64 | out1[0] = x1; |
468 | 64 | out1[1] = x2; |
469 | 64 | out1[2] = x3; |
470 | 64 | out1[3] = x4; |
471 | 64 | out1[4] = x5; |
472 | 64 | } |
473 | | |
474 | | /* |
475 | | * The function fiat_25519_selectznz is a multi-limb conditional select. |
476 | | * |
477 | | * Postconditions: |
478 | | * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) |
479 | | * |
480 | | * Input Bounds: |
481 | | * arg1: [0x0 ~> 0x1] |
482 | | * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
483 | | * arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
484 | | * Output Bounds: |
485 | | * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] |
486 | | */ |
487 | 0 | 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]) { |
488 | 0 | uint64_t x1; |
489 | 0 | uint64_t x2; |
490 | 0 | uint64_t x3; |
491 | 0 | uint64_t x4; |
492 | 0 | uint64_t x5; |
493 | 0 | fiat_25519_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0])); |
494 | 0 | fiat_25519_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1])); |
495 | 0 | fiat_25519_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2])); |
496 | 0 | fiat_25519_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3])); |
497 | 0 | fiat_25519_cmovznz_u64(&x5, arg1, (arg2[4]), (arg3[4])); |
498 | 0 | out1[0] = x1; |
499 | 0 | out1[1] = x2; |
500 | 0 | out1[2] = x3; |
501 | 0 | out1[3] = x4; |
502 | 0 | out1[4] = x5; |
503 | 0 | } |
504 | | |
505 | | /* |
506 | | * The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order. |
507 | | * |
508 | | * Postconditions: |
509 | | * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] |
510 | | * |
511 | | * Output Bounds: |
512 | | * 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]] |
513 | | */ |
514 | 1 | static FIAT_25519_FIAT_INLINE void fiat_25519_to_bytes(uint8_t out1[32], const fiat_25519_tight_field_element arg1) { |
515 | 1 | uint64_t x1; |
516 | 1 | fiat_25519_uint1 x2; |
517 | 1 | uint64_t x3; |
518 | 1 | fiat_25519_uint1 x4; |
519 | 1 | uint64_t x5; |
520 | 1 | fiat_25519_uint1 x6; |
521 | 1 | uint64_t x7; |
522 | 1 | fiat_25519_uint1 x8; |
523 | 1 | uint64_t x9; |
524 | 1 | fiat_25519_uint1 x10; |
525 | 1 | uint64_t x11; |
526 | 1 | uint64_t x12; |
527 | 1 | fiat_25519_uint1 x13; |
528 | 1 | uint64_t x14; |
529 | 1 | fiat_25519_uint1 x15; |
530 | 1 | uint64_t x16; |
531 | 1 | fiat_25519_uint1 x17; |
532 | 1 | uint64_t x18; |
533 | 1 | fiat_25519_uint1 x19; |
534 | 1 | uint64_t x20; |
535 | 1 | fiat_25519_uint1 x21; |
536 | 1 | uint64_t x22; |
537 | 1 | uint64_t x23; |
538 | 1 | uint64_t x24; |
539 | 1 | uint64_t x25; |
540 | 1 | uint8_t x26; |
541 | 1 | uint64_t x27; |
542 | 1 | uint8_t x28; |
543 | 1 | uint64_t x29; |
544 | 1 | uint8_t x30; |
545 | 1 | uint64_t x31; |
546 | 1 | uint8_t x32; |
547 | 1 | uint64_t x33; |
548 | 1 | uint8_t x34; |
549 | 1 | uint64_t x35; |
550 | 1 | uint8_t x36; |
551 | 1 | uint8_t x37; |
552 | 1 | uint64_t x38; |
553 | 1 | uint8_t x39; |
554 | 1 | uint64_t x40; |
555 | 1 | uint8_t x41; |
556 | 1 | uint64_t x42; |
557 | 1 | uint8_t x43; |
558 | 1 | uint64_t x44; |
559 | 1 | uint8_t x45; |
560 | 1 | uint64_t x46; |
561 | 1 | uint8_t x47; |
562 | 1 | uint64_t x48; |
563 | 1 | uint8_t x49; |
564 | 1 | uint8_t x50; |
565 | 1 | uint64_t x51; |
566 | 1 | uint8_t x52; |
567 | 1 | uint64_t x53; |
568 | 1 | uint8_t x54; |
569 | 1 | uint64_t x55; |
570 | 1 | uint8_t x56; |
571 | 1 | uint64_t x57; |
572 | 1 | uint8_t x58; |
573 | 1 | uint64_t x59; |
574 | 1 | uint8_t x60; |
575 | 1 | uint64_t x61; |
576 | 1 | uint8_t x62; |
577 | 1 | uint64_t x63; |
578 | 1 | uint8_t x64; |
579 | 1 | fiat_25519_uint1 x65; |
580 | 1 | uint64_t x66; |
581 | 1 | uint8_t x67; |
582 | 1 | uint64_t x68; |
583 | 1 | uint8_t x69; |
584 | 1 | uint64_t x70; |
585 | 1 | uint8_t x71; |
586 | 1 | uint64_t x72; |
587 | 1 | uint8_t x73; |
588 | 1 | uint64_t x74; |
589 | 1 | uint8_t x75; |
590 | 1 | uint64_t x76; |
591 | 1 | uint8_t x77; |
592 | 1 | uint8_t x78; |
593 | 1 | uint64_t x79; |
594 | 1 | uint8_t x80; |
595 | 1 | uint64_t x81; |
596 | 1 | uint8_t x82; |
597 | 1 | uint64_t x83; |
598 | 1 | uint8_t x84; |
599 | 1 | uint64_t x85; |
600 | 1 | uint8_t x86; |
601 | 1 | uint64_t x87; |
602 | 1 | uint8_t x88; |
603 | 1 | uint64_t x89; |
604 | 1 | uint8_t x90; |
605 | 1 | uint8_t x91; |
606 | 1 | fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed)); |
607 | 1 | fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff)); |
608 | 1 | fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff)); |
609 | 1 | fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff)); |
610 | 1 | fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff)); |
611 | 1 | fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff)); |
612 | 1 | fiat_25519_addcarryx_u51(&x12, &x13, 0x0, x1, (x11 & UINT64_C(0x7ffffffffffed))); |
613 | 1 | fiat_25519_addcarryx_u51(&x14, &x15, x13, x3, (x11 & UINT64_C(0x7ffffffffffff))); |
614 | 1 | fiat_25519_addcarryx_u51(&x16, &x17, x15, x5, (x11 & UINT64_C(0x7ffffffffffff))); |
615 | 1 | fiat_25519_addcarryx_u51(&x18, &x19, x17, x7, (x11 & UINT64_C(0x7ffffffffffff))); |
616 | 1 | fiat_25519_addcarryx_u51(&x20, &x21, x19, x9, (x11 & UINT64_C(0x7ffffffffffff))); |
617 | 1 | x22 = (x20 << 4); |
618 | 1 | x23 = (x18 * (uint64_t)0x2); |
619 | 1 | x24 = (x16 << 6); |
620 | 1 | x25 = (x14 << 3); |
621 | 1 | x26 = (uint8_t)(x12 & UINT8_C(0xff)); |
622 | 1 | x27 = (x12 >> 8); |
623 | 1 | x28 = (uint8_t)(x27 & UINT8_C(0xff)); |
624 | 1 | x29 = (x27 >> 8); |
625 | 1 | x30 = (uint8_t)(x29 & UINT8_C(0xff)); |
626 | 1 | x31 = (x29 >> 8); |
627 | 1 | x32 = (uint8_t)(x31 & UINT8_C(0xff)); |
628 | 1 | x33 = (x31 >> 8); |
629 | 1 | x34 = (uint8_t)(x33 & UINT8_C(0xff)); |
630 | 1 | x35 = (x33 >> 8); |
631 | 1 | x36 = (uint8_t)(x35 & UINT8_C(0xff)); |
632 | 1 | x37 = (uint8_t)(x35 >> 8); |
633 | 1 | x38 = (x25 + (uint64_t)x37); |
634 | 1 | x39 = (uint8_t)(x38 & UINT8_C(0xff)); |
635 | 1 | x40 = (x38 >> 8); |
636 | 1 | x41 = (uint8_t)(x40 & UINT8_C(0xff)); |
637 | 1 | x42 = (x40 >> 8); |
638 | 1 | x43 = (uint8_t)(x42 & UINT8_C(0xff)); |
639 | 1 | x44 = (x42 >> 8); |
640 | 1 | x45 = (uint8_t)(x44 & UINT8_C(0xff)); |
641 | 1 | x46 = (x44 >> 8); |
642 | 1 | x47 = (uint8_t)(x46 & UINT8_C(0xff)); |
643 | 1 | x48 = (x46 >> 8); |
644 | 1 | x49 = (uint8_t)(x48 & UINT8_C(0xff)); |
645 | 1 | x50 = (uint8_t)(x48 >> 8); |
646 | 1 | x51 = (x24 + (uint64_t)x50); |
647 | 1 | x52 = (uint8_t)(x51 & UINT8_C(0xff)); |
648 | 1 | x53 = (x51 >> 8); |
649 | 1 | x54 = (uint8_t)(x53 & UINT8_C(0xff)); |
650 | 1 | x55 = (x53 >> 8); |
651 | 1 | x56 = (uint8_t)(x55 & UINT8_C(0xff)); |
652 | 1 | x57 = (x55 >> 8); |
653 | 1 | x58 = (uint8_t)(x57 & UINT8_C(0xff)); |
654 | 1 | x59 = (x57 >> 8); |
655 | 1 | x60 = (uint8_t)(x59 & UINT8_C(0xff)); |
656 | 1 | x61 = (x59 >> 8); |
657 | 1 | x62 = (uint8_t)(x61 & UINT8_C(0xff)); |
658 | 1 | x63 = (x61 >> 8); |
659 | 1 | x64 = (uint8_t)(x63 & UINT8_C(0xff)); |
660 | 1 | x65 = (fiat_25519_uint1)(x63 >> 8); |
661 | 1 | x66 = (x23 + (uint64_t)x65); |
662 | 1 | x67 = (uint8_t)(x66 & UINT8_C(0xff)); |
663 | 1 | x68 = (x66 >> 8); |
664 | 1 | x69 = (uint8_t)(x68 & UINT8_C(0xff)); |
665 | 1 | x70 = (x68 >> 8); |
666 | 1 | x71 = (uint8_t)(x70 & UINT8_C(0xff)); |
667 | 1 | x72 = (x70 >> 8); |
668 | 1 | x73 = (uint8_t)(x72 & UINT8_C(0xff)); |
669 | 1 | x74 = (x72 >> 8); |
670 | 1 | x75 = (uint8_t)(x74 & UINT8_C(0xff)); |
671 | 1 | x76 = (x74 >> 8); |
672 | 1 | x77 = (uint8_t)(x76 & UINT8_C(0xff)); |
673 | 1 | x78 = (uint8_t)(x76 >> 8); |
674 | 1 | x79 = (x22 + (uint64_t)x78); |
675 | 1 | x80 = (uint8_t)(x79 & UINT8_C(0xff)); |
676 | 1 | x81 = (x79 >> 8); |
677 | 1 | x82 = (uint8_t)(x81 & UINT8_C(0xff)); |
678 | 1 | x83 = (x81 >> 8); |
679 | 1 | x84 = (uint8_t)(x83 & UINT8_C(0xff)); |
680 | 1 | x85 = (x83 >> 8); |
681 | 1 | x86 = (uint8_t)(x85 & UINT8_C(0xff)); |
682 | 1 | x87 = (x85 >> 8); |
683 | 1 | x88 = (uint8_t)(x87 & UINT8_C(0xff)); |
684 | 1 | x89 = (x87 >> 8); |
685 | 1 | x90 = (uint8_t)(x89 & UINT8_C(0xff)); |
686 | 1 | x91 = (uint8_t)(x89 >> 8); |
687 | 1 | out1[0] = x26; |
688 | 1 | out1[1] = x28; |
689 | 1 | out1[2] = x30; |
690 | 1 | out1[3] = x32; |
691 | 1 | out1[4] = x34; |
692 | 1 | out1[5] = x36; |
693 | 1 | out1[6] = x39; |
694 | 1 | out1[7] = x41; |
695 | 1 | out1[8] = x43; |
696 | 1 | out1[9] = x45; |
697 | 1 | out1[10] = x47; |
698 | 1 | out1[11] = x49; |
699 | 1 | out1[12] = x52; |
700 | 1 | out1[13] = x54; |
701 | 1 | out1[14] = x56; |
702 | 1 | out1[15] = x58; |
703 | 1 | out1[16] = x60; |
704 | 1 | out1[17] = x62; |
705 | 1 | out1[18] = x64; |
706 | 1 | out1[19] = x67; |
707 | 1 | out1[20] = x69; |
708 | 1 | out1[21] = x71; |
709 | 1 | out1[22] = x73; |
710 | 1 | out1[23] = x75; |
711 | 1 | out1[24] = x77; |
712 | 1 | out1[25] = x80; |
713 | 1 | out1[26] = x82; |
714 | 1 | out1[27] = x84; |
715 | 1 | out1[28] = x86; |
716 | 1 | out1[29] = x88; |
717 | 1 | out1[30] = x90; |
718 | 1 | out1[31] = x91; |
719 | 1 | } |
720 | | |
721 | | /* |
722 | | * The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order. |
723 | | * |
724 | | * Postconditions: |
725 | | * eval out1 mod m = bytes_eval arg1 mod m |
726 | | * |
727 | | * Input Bounds: |
728 | | * 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]] |
729 | | */ |
730 | 192 | static FIAT_25519_FIAT_INLINE void fiat_25519_from_bytes(fiat_25519_tight_field_element out1, const uint8_t arg1[32]) { |
731 | 192 | uint64_t x1; |
732 | 192 | uint64_t x2; |
733 | 192 | uint64_t x3; |
734 | 192 | uint64_t x4; |
735 | 192 | uint64_t x5; |
736 | 192 | uint64_t x6; |
737 | 192 | uint64_t x7; |
738 | 192 | uint64_t x8; |
739 | 192 | uint64_t x9; |
740 | 192 | uint64_t x10; |
741 | 192 | uint64_t x11; |
742 | 192 | uint64_t x12; |
743 | 192 | uint64_t x13; |
744 | 192 | uint64_t x14; |
745 | 192 | uint64_t x15; |
746 | 192 | uint64_t x16; |
747 | 192 | uint64_t x17; |
748 | 192 | uint64_t x18; |
749 | 192 | uint64_t x19; |
750 | 192 | uint64_t x20; |
751 | 192 | uint64_t x21; |
752 | 192 | uint64_t x22; |
753 | 192 | uint64_t x23; |
754 | 192 | uint64_t x24; |
755 | 192 | uint64_t x25; |
756 | 192 | uint64_t x26; |
757 | 192 | uint64_t x27; |
758 | 192 | uint64_t x28; |
759 | 192 | uint64_t x29; |
760 | 192 | uint64_t x30; |
761 | 192 | uint64_t x31; |
762 | 192 | uint8_t x32; |
763 | 192 | uint64_t x33; |
764 | 192 | uint64_t x34; |
765 | 192 | uint64_t x35; |
766 | 192 | uint64_t x36; |
767 | 192 | uint64_t x37; |
768 | 192 | uint64_t x38; |
769 | 192 | uint64_t x39; |
770 | 192 | uint8_t x40; |
771 | 192 | uint64_t x41; |
772 | 192 | uint64_t x42; |
773 | 192 | uint64_t x43; |
774 | 192 | uint64_t x44; |
775 | 192 | uint64_t x45; |
776 | 192 | uint64_t x46; |
777 | 192 | uint64_t x47; |
778 | 192 | uint8_t x48; |
779 | 192 | uint64_t x49; |
780 | 192 | uint64_t x50; |
781 | 192 | uint64_t x51; |
782 | 192 | uint64_t x52; |
783 | 192 | uint64_t x53; |
784 | 192 | uint64_t x54; |
785 | 192 | uint64_t x55; |
786 | 192 | uint64_t x56; |
787 | 192 | uint8_t x57; |
788 | 192 | uint64_t x58; |
789 | 192 | uint64_t x59; |
790 | 192 | uint64_t x60; |
791 | 192 | uint64_t x61; |
792 | 192 | uint64_t x62; |
793 | 192 | uint64_t x63; |
794 | 192 | uint64_t x64; |
795 | 192 | uint8_t x65; |
796 | 192 | uint64_t x66; |
797 | 192 | uint64_t x67; |
798 | 192 | uint64_t x68; |
799 | 192 | uint64_t x69; |
800 | 192 | uint64_t x70; |
801 | 192 | uint64_t x71; |
802 | 192 | x1 = ((uint64_t)(arg1[31]) << 44); |
803 | 192 | x2 = ((uint64_t)(arg1[30]) << 36); |
804 | 192 | x3 = ((uint64_t)(arg1[29]) << 28); |
805 | 192 | x4 = ((uint64_t)(arg1[28]) << 20); |
806 | 192 | x5 = ((uint64_t)(arg1[27]) << 12); |
807 | 192 | x6 = ((uint64_t)(arg1[26]) << 4); |
808 | 192 | x7 = ((uint64_t)(arg1[25]) << 47); |
809 | 192 | x8 = ((uint64_t)(arg1[24]) << 39); |
810 | 192 | x9 = ((uint64_t)(arg1[23]) << 31); |
811 | 192 | x10 = ((uint64_t)(arg1[22]) << 23); |
812 | 192 | x11 = ((uint64_t)(arg1[21]) << 15); |
813 | 192 | x12 = ((uint64_t)(arg1[20]) << 7); |
814 | 192 | x13 = ((uint64_t)(arg1[19]) << 50); |
815 | 192 | x14 = ((uint64_t)(arg1[18]) << 42); |
816 | 192 | x15 = ((uint64_t)(arg1[17]) << 34); |
817 | 192 | x16 = ((uint64_t)(arg1[16]) << 26); |
818 | 192 | x17 = ((uint64_t)(arg1[15]) << 18); |
819 | 192 | x18 = ((uint64_t)(arg1[14]) << 10); |
820 | 192 | x19 = ((uint64_t)(arg1[13]) << 2); |
821 | 192 | x20 = ((uint64_t)(arg1[12]) << 45); |
822 | 192 | x21 = ((uint64_t)(arg1[11]) << 37); |
823 | 192 | x22 = ((uint64_t)(arg1[10]) << 29); |
824 | 192 | x23 = ((uint64_t)(arg1[9]) << 21); |
825 | 192 | x24 = ((uint64_t)(arg1[8]) << 13); |
826 | 192 | x25 = ((uint64_t)(arg1[7]) << 5); |
827 | 192 | x26 = ((uint64_t)(arg1[6]) << 48); |
828 | 192 | x27 = ((uint64_t)(arg1[5]) << 40); |
829 | 192 | x28 = ((uint64_t)(arg1[4]) << 32); |
830 | 192 | x29 = ((uint64_t)(arg1[3]) << 24); |
831 | 192 | x30 = ((uint64_t)(arg1[2]) << 16); |
832 | 192 | x31 = ((uint64_t)(arg1[1]) << 8); |
833 | 192 | x32 = (arg1[0]); |
834 | 192 | x33 = (x31 + (uint64_t)x32); |
835 | 192 | x34 = (x30 + x33); |
836 | 192 | x35 = (x29 + x34); |
837 | 192 | x36 = (x28 + x35); |
838 | 192 | x37 = (x27 + x36); |
839 | 192 | x38 = (x26 + x37); |
840 | 192 | x39 = (x38 & UINT64_C(0x7ffffffffffff)); |
841 | 192 | x40 = (uint8_t)(x38 >> 51); |
842 | 192 | x41 = (x25 + (uint64_t)x40); |
843 | 192 | x42 = (x24 + x41); |
844 | 192 | x43 = (x23 + x42); |
845 | 192 | x44 = (x22 + x43); |
846 | 192 | x45 = (x21 + x44); |
847 | 192 | x46 = (x20 + x45); |
848 | 192 | x47 = (x46 & UINT64_C(0x7ffffffffffff)); |
849 | 192 | x48 = (uint8_t)(x46 >> 51); |
850 | 192 | x49 = (x19 + (uint64_t)x48); |
851 | 192 | x50 = (x18 + x49); |
852 | 192 | x51 = (x17 + x50); |
853 | 192 | x52 = (x16 + x51); |
854 | 192 | x53 = (x15 + x52); |
855 | 192 | x54 = (x14 + x53); |
856 | 192 | x55 = (x13 + x54); |
857 | 192 | x56 = (x55 & UINT64_C(0x7ffffffffffff)); |
858 | 192 | x57 = (uint8_t)(x55 >> 51); |
859 | 192 | x58 = (x12 + (uint64_t)x57); |
860 | 192 | x59 = (x11 + x58); |
861 | 192 | x60 = (x10 + x59); |
862 | 192 | x61 = (x9 + x60); |
863 | 192 | x62 = (x8 + x61); |
864 | 192 | x63 = (x7 + x62); |
865 | 192 | x64 = (x63 & UINT64_C(0x7ffffffffffff)); |
866 | 192 | x65 = (uint8_t)(x63 >> 51); |
867 | 192 | x66 = (x6 + (uint64_t)x65); |
868 | 192 | x67 = (x5 + x66); |
869 | 192 | x68 = (x4 + x67); |
870 | 192 | x69 = (x3 + x68); |
871 | 192 | x70 = (x2 + x69); |
872 | 192 | x71 = (x1 + x70); |
873 | 192 | out1[0] = x39; |
874 | 192 | out1[1] = x47; |
875 | 192 | out1[2] = x56; |
876 | 192 | out1[3] = x64; |
877 | 192 | out1[4] = x71; |
878 | 192 | } |
879 | | |
880 | | /* |
881 | | * The function fiat_25519_relax is the identity function converting from tight field elements to loose field elements. |
882 | | * |
883 | | * Postconditions: |
884 | | * out1 = arg1 |
885 | | * |
886 | | */ |
887 | 0 | static FIAT_25519_FIAT_INLINE void fiat_25519_relax(fiat_25519_loose_field_element out1, const fiat_25519_tight_field_element arg1) { |
888 | 0 | uint64_t x1; |
889 | 0 | uint64_t x2; |
890 | 0 | uint64_t x3; |
891 | 0 | uint64_t x4; |
892 | 0 | uint64_t x5; |
893 | 0 | x1 = (arg1[0]); |
894 | 0 | x2 = (arg1[1]); |
895 | 0 | x3 = (arg1[2]); |
896 | 0 | x4 = (arg1[3]); |
897 | 0 | x5 = (arg1[4]); |
898 | 0 | out1[0] = x1; |
899 | 0 | out1[1] = x2; |
900 | 0 | out1[2] = x3; |
901 | 0 | out1[3] = x4; |
902 | 0 | out1[4] = x5; |
903 | 0 | } |
904 | | |
905 | | /* |
906 | | * The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result. |
907 | | * |
908 | | * Postconditions: |
909 | | * eval out1 mod m = (121666 * eval arg1) mod m |
910 | | * |
911 | | */ |
912 | 0 | static FIAT_25519_FIAT_INLINE void fiat_25519_carry_scmul_121666(fiat_25519_tight_field_element out1, const fiat_25519_loose_field_element arg1) { |
913 | 0 | fiat_25519_uint128 x1; |
914 | 0 | fiat_25519_uint128 x2; |
915 | 0 | fiat_25519_uint128 x3; |
916 | 0 | fiat_25519_uint128 x4; |
917 | 0 | fiat_25519_uint128 x5; |
918 | 0 | uint64_t x6; |
919 | 0 | uint64_t x7; |
920 | 0 | fiat_25519_uint128 x8; |
921 | 0 | uint64_t x9; |
922 | 0 | uint64_t x10; |
923 | 0 | fiat_25519_uint128 x11; |
924 | 0 | uint64_t x12; |
925 | 0 | uint64_t x13; |
926 | 0 | fiat_25519_uint128 x14; |
927 | 0 | uint64_t x15; |
928 | 0 | uint64_t x16; |
929 | 0 | fiat_25519_uint128 x17; |
930 | 0 | uint64_t x18; |
931 | 0 | uint64_t x19; |
932 | 0 | uint64_t x20; |
933 | 0 | uint64_t x21; |
934 | 0 | fiat_25519_uint1 x22; |
935 | 0 | uint64_t x23; |
936 | 0 | uint64_t x24; |
937 | 0 | fiat_25519_uint1 x25; |
938 | 0 | uint64_t x26; |
939 | 0 | uint64_t x27; |
940 | 0 | x1 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[4])); |
941 | 0 | x2 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[3])); |
942 | 0 | x3 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[2])); |
943 | 0 | x4 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[1])); |
944 | 0 | x5 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[0])); |
945 | 0 | x6 = (uint64_t)(x5 >> 51); |
946 | 0 | x7 = (uint64_t)(x5 & UINT64_C(0x7ffffffffffff)); |
947 | 0 | x8 = (x6 + x4); |
948 | 0 | x9 = (uint64_t)(x8 >> 51); |
949 | 0 | x10 = (uint64_t)(x8 & UINT64_C(0x7ffffffffffff)); |
950 | 0 | x11 = (x9 + x3); |
951 | 0 | x12 = (uint64_t)(x11 >> 51); |
952 | 0 | x13 = (uint64_t)(x11 & UINT64_C(0x7ffffffffffff)); |
953 | 0 | x14 = (x12 + x2); |
954 | 0 | x15 = (uint64_t)(x14 >> 51); |
955 | 0 | x16 = (uint64_t)(x14 & UINT64_C(0x7ffffffffffff)); |
956 | 0 | x17 = (x15 + x1); |
957 | 0 | x18 = (uint64_t)(x17 >> 51); |
958 | 0 | x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff)); |
959 | 0 | x20 = (x18 * UINT8_C(0x13)); |
960 | 0 | x21 = (x7 + x20); |
961 | 0 | x22 = (fiat_25519_uint1)(x21 >> 51); |
962 | 0 | x23 = (x21 & UINT64_C(0x7ffffffffffff)); |
963 | 0 | x24 = (x22 + x10); |
964 | 0 | x25 = (fiat_25519_uint1)(x24 >> 51); |
965 | 0 | x26 = (x24 & UINT64_C(0x7ffffffffffff)); |
966 | 0 | x27 = (x25 + x13); |
967 | 0 | out1[0] = x23; |
968 | 0 | out1[1] = x26; |
969 | 0 | out1[2] = x27; |
970 | 0 | out1[3] = x16; |
971 | 0 | out1[4] = x19; |
972 | 0 | } |