1 /* MIT License
2 *
3 * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
4 *
5 * Permission is hereby granted, free of charge, to any person obtaining a copy
6 * of this software and associated documentation files (the "Software"), to deal
7 * in the Software without restriction, including without limitation the rights
8 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9 * copies of the Software, and to permit persons to whom the Software is
10 * furnished to do so, subject to the following conditions:
11 *
12 * The above copyright notice and this permission notice shall be included in all
13 * copies or substantial portions of the Software.
14 *
15 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21 * SOFTWARE.
22 */
23
24 #include "Hacl_Poly1305_32.h"
25
26 uint32_t Hacl_Poly1305_32_blocklen = (uint32_t)16U;
27
28 void
Hacl_Poly1305_32_poly1305_init(uint64_t * ctx,uint8_t * key)29 Hacl_Poly1305_32_poly1305_init(uint64_t *ctx, uint8_t *key)
30 {
31 uint64_t *acc = ctx;
32 uint64_t *pre = ctx + (uint32_t)5U;
33 uint8_t *kr = key;
34 acc[0U] = (uint64_t)0U;
35 acc[1U] = (uint64_t)0U;
36 acc[2U] = (uint64_t)0U;
37 acc[3U] = (uint64_t)0U;
38 acc[4U] = (uint64_t)0U;
39 uint64_t u0 = load64_le(kr);
40 uint64_t lo = u0;
41 uint64_t u = load64_le(kr + (uint32_t)8U);
42 uint64_t hi = u;
43 uint64_t mask0 = (uint64_t)0x0ffffffc0fffffffU;
44 uint64_t mask1 = (uint64_t)0x0ffffffc0ffffffcU;
45 uint64_t lo1 = lo & mask0;
46 uint64_t hi1 = hi & mask1;
47 uint64_t *r = pre;
48 uint64_t *r5 = pre + (uint32_t)5U;
49 uint64_t *rn = pre + (uint32_t)10U;
50 uint64_t *rn_5 = pre + (uint32_t)15U;
51 uint64_t r_vec0 = lo1;
52 uint64_t r_vec1 = hi1;
53 uint64_t f00 = r_vec0 & (uint64_t)0x3ffffffU;
54 uint64_t f10 = r_vec0 >> (uint32_t)26U & (uint64_t)0x3ffffffU;
55 uint64_t f20 = r_vec0 >> (uint32_t)52U | (r_vec1 & (uint64_t)0x3fffU) << (uint32_t)12U;
56 uint64_t f30 = r_vec1 >> (uint32_t)14U & (uint64_t)0x3ffffffU;
57 uint64_t f40 = r_vec1 >> (uint32_t)40U;
58 uint64_t f0 = f00;
59 uint64_t f1 = f10;
60 uint64_t f2 = f20;
61 uint64_t f3 = f30;
62 uint64_t f4 = f40;
63 r[0U] = f0;
64 r[1U] = f1;
65 r[2U] = f2;
66 r[3U] = f3;
67 r[4U] = f4;
68 uint64_t f200 = r[0U];
69 uint64_t f21 = r[1U];
70 uint64_t f22 = r[2U];
71 uint64_t f23 = r[3U];
72 uint64_t f24 = r[4U];
73 r5[0U] = f200 * (uint64_t)5U;
74 r5[1U] = f21 * (uint64_t)5U;
75 r5[2U] = f22 * (uint64_t)5U;
76 r5[3U] = f23 * (uint64_t)5U;
77 r5[4U] = f24 * (uint64_t)5U;
78 rn[0U] = r[0U];
79 rn[1U] = r[1U];
80 rn[2U] = r[2U];
81 rn[3U] = r[3U];
82 rn[4U] = r[4U];
83 rn_5[0U] = r5[0U];
84 rn_5[1U] = r5[1U];
85 rn_5[2U] = r5[2U];
86 rn_5[3U] = r5[3U];
87 rn_5[4U] = r5[4U];
88 }
89
90 void
Hacl_Poly1305_32_poly1305_update1(uint64_t * ctx,uint8_t * text)91 Hacl_Poly1305_32_poly1305_update1(uint64_t *ctx, uint8_t *text)
92 {
93 uint64_t *pre = ctx + (uint32_t)5U;
94 uint64_t *acc = ctx;
95 uint64_t e[5U] = { 0U };
96 uint64_t u0 = load64_le(text);
97 uint64_t lo = u0;
98 uint64_t u = load64_le(text + (uint32_t)8U);
99 uint64_t hi = u;
100 uint64_t f0 = lo;
101 uint64_t f1 = hi;
102 uint64_t f010 = f0 & (uint64_t)0x3ffffffU;
103 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU;
104 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U;
105 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU;
106 uint64_t f40 = f1 >> (uint32_t)40U;
107 uint64_t f01 = f010;
108 uint64_t f111 = f110;
109 uint64_t f2 = f20;
110 uint64_t f3 = f30;
111 uint64_t f41 = f40;
112 e[0U] = f01;
113 e[1U] = f111;
114 e[2U] = f2;
115 e[3U] = f3;
116 e[4U] = f41;
117 uint64_t b = (uint64_t)0x1000000U;
118 uint64_t mask = b;
119 uint64_t f4 = e[4U];
120 e[4U] = f4 | mask;
121 uint64_t *r = pre;
122 uint64_t *r5 = pre + (uint32_t)5U;
123 uint64_t r0 = r[0U];
124 uint64_t r1 = r[1U];
125 uint64_t r2 = r[2U];
126 uint64_t r3 = r[3U];
127 uint64_t r4 = r[4U];
128 uint64_t r51 = r5[1U];
129 uint64_t r52 = r5[2U];
130 uint64_t r53 = r5[3U];
131 uint64_t r54 = r5[4U];
132 uint64_t f10 = e[0U];
133 uint64_t f11 = e[1U];
134 uint64_t f12 = e[2U];
135 uint64_t f13 = e[3U];
136 uint64_t f14 = e[4U];
137 uint64_t a0 = acc[0U];
138 uint64_t a1 = acc[1U];
139 uint64_t a2 = acc[2U];
140 uint64_t a3 = acc[3U];
141 uint64_t a4 = acc[4U];
142 uint64_t a01 = a0 + f10;
143 uint64_t a11 = a1 + f11;
144 uint64_t a21 = a2 + f12;
145 uint64_t a31 = a3 + f13;
146 uint64_t a41 = a4 + f14;
147 uint64_t a02 = r0 * a01;
148 uint64_t a12 = r1 * a01;
149 uint64_t a22 = r2 * a01;
150 uint64_t a32 = r3 * a01;
151 uint64_t a42 = r4 * a01;
152 uint64_t a03 = a02 + r54 * a11;
153 uint64_t a13 = a12 + r0 * a11;
154 uint64_t a23 = a22 + r1 * a11;
155 uint64_t a33 = a32 + r2 * a11;
156 uint64_t a43 = a42 + r3 * a11;
157 uint64_t a04 = a03 + r53 * a21;
158 uint64_t a14 = a13 + r54 * a21;
159 uint64_t a24 = a23 + r0 * a21;
160 uint64_t a34 = a33 + r1 * a21;
161 uint64_t a44 = a43 + r2 * a21;
162 uint64_t a05 = a04 + r52 * a31;
163 uint64_t a15 = a14 + r53 * a31;
164 uint64_t a25 = a24 + r54 * a31;
165 uint64_t a35 = a34 + r0 * a31;
166 uint64_t a45 = a44 + r1 * a31;
167 uint64_t a06 = a05 + r51 * a41;
168 uint64_t a16 = a15 + r52 * a41;
169 uint64_t a26 = a25 + r53 * a41;
170 uint64_t a36 = a35 + r54 * a41;
171 uint64_t a46 = a45 + r0 * a41;
172 uint64_t t0 = a06;
173 uint64_t t1 = a16;
174 uint64_t t2 = a26;
175 uint64_t t3 = a36;
176 uint64_t t4 = a46;
177 uint64_t mask26 = (uint64_t)0x3ffffffU;
178 uint64_t z0 = t0 >> (uint32_t)26U;
179 uint64_t z1 = t3 >> (uint32_t)26U;
180 uint64_t x0 = t0 & mask26;
181 uint64_t x3 = t3 & mask26;
182 uint64_t x1 = t1 + z0;
183 uint64_t x4 = t4 + z1;
184 uint64_t z01 = x1 >> (uint32_t)26U;
185 uint64_t z11 = x4 >> (uint32_t)26U;
186 uint64_t t = z11 << (uint32_t)2U;
187 uint64_t z12 = z11 + t;
188 uint64_t x11 = x1 & mask26;
189 uint64_t x41 = x4 & mask26;
190 uint64_t x2 = t2 + z01;
191 uint64_t x01 = x0 + z12;
192 uint64_t z02 = x2 >> (uint32_t)26U;
193 uint64_t z13 = x01 >> (uint32_t)26U;
194 uint64_t x21 = x2 & mask26;
195 uint64_t x02 = x01 & mask26;
196 uint64_t x31 = x3 + z02;
197 uint64_t x12 = x11 + z13;
198 uint64_t z03 = x31 >> (uint32_t)26U;
199 uint64_t x32 = x31 & mask26;
200 uint64_t x42 = x41 + z03;
201 uint64_t o0 = x02;
202 uint64_t o1 = x12;
203 uint64_t o2 = x21;
204 uint64_t o3 = x32;
205 uint64_t o4 = x42;
206 acc[0U] = o0;
207 acc[1U] = o1;
208 acc[2U] = o2;
209 acc[3U] = o3;
210 acc[4U] = o4;
211 }
212
213 void
Hacl_Poly1305_32_poly1305_update(uint64_t * ctx,uint32_t len,uint8_t * text)214 Hacl_Poly1305_32_poly1305_update(uint64_t *ctx, uint32_t len, uint8_t *text)
215 {
216 uint64_t *pre = ctx + (uint32_t)5U;
217 uint64_t *acc = ctx;
218 uint32_t nb = len / (uint32_t)16U;
219 uint32_t rem = len % (uint32_t)16U;
220 for (uint32_t i = (uint32_t)0U; i < nb; i++) {
221 uint8_t *block = text + i * (uint32_t)16U;
222 uint64_t e[5U] = { 0U };
223 uint64_t u0 = load64_le(block);
224 uint64_t lo = u0;
225 uint64_t u = load64_le(block + (uint32_t)8U);
226 uint64_t hi = u;
227 uint64_t f0 = lo;
228 uint64_t f1 = hi;
229 uint64_t f010 = f0 & (uint64_t)0x3ffffffU;
230 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU;
231 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U;
232 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU;
233 uint64_t f40 = f1 >> (uint32_t)40U;
234 uint64_t f01 = f010;
235 uint64_t f111 = f110;
236 uint64_t f2 = f20;
237 uint64_t f3 = f30;
238 uint64_t f41 = f40;
239 e[0U] = f01;
240 e[1U] = f111;
241 e[2U] = f2;
242 e[3U] = f3;
243 e[4U] = f41;
244 uint64_t b = (uint64_t)0x1000000U;
245 uint64_t mask = b;
246 uint64_t f4 = e[4U];
247 e[4U] = f4 | mask;
248 uint64_t *r = pre;
249 uint64_t *r5 = pre + (uint32_t)5U;
250 uint64_t r0 = r[0U];
251 uint64_t r1 = r[1U];
252 uint64_t r2 = r[2U];
253 uint64_t r3 = r[3U];
254 uint64_t r4 = r[4U];
255 uint64_t r51 = r5[1U];
256 uint64_t r52 = r5[2U];
257 uint64_t r53 = r5[3U];
258 uint64_t r54 = r5[4U];
259 uint64_t f10 = e[0U];
260 uint64_t f11 = e[1U];
261 uint64_t f12 = e[2U];
262 uint64_t f13 = e[3U];
263 uint64_t f14 = e[4U];
264 uint64_t a0 = acc[0U];
265 uint64_t a1 = acc[1U];
266 uint64_t a2 = acc[2U];
267 uint64_t a3 = acc[3U];
268 uint64_t a4 = acc[4U];
269 uint64_t a01 = a0 + f10;
270 uint64_t a11 = a1 + f11;
271 uint64_t a21 = a2 + f12;
272 uint64_t a31 = a3 + f13;
273 uint64_t a41 = a4 + f14;
274 uint64_t a02 = r0 * a01;
275 uint64_t a12 = r1 * a01;
276 uint64_t a22 = r2 * a01;
277 uint64_t a32 = r3 * a01;
278 uint64_t a42 = r4 * a01;
279 uint64_t a03 = a02 + r54 * a11;
280 uint64_t a13 = a12 + r0 * a11;
281 uint64_t a23 = a22 + r1 * a11;
282 uint64_t a33 = a32 + r2 * a11;
283 uint64_t a43 = a42 + r3 * a11;
284 uint64_t a04 = a03 + r53 * a21;
285 uint64_t a14 = a13 + r54 * a21;
286 uint64_t a24 = a23 + r0 * a21;
287 uint64_t a34 = a33 + r1 * a21;
288 uint64_t a44 = a43 + r2 * a21;
289 uint64_t a05 = a04 + r52 * a31;
290 uint64_t a15 = a14 + r53 * a31;
291 uint64_t a25 = a24 + r54 * a31;
292 uint64_t a35 = a34 + r0 * a31;
293 uint64_t a45 = a44 + r1 * a31;
294 uint64_t a06 = a05 + r51 * a41;
295 uint64_t a16 = a15 + r52 * a41;
296 uint64_t a26 = a25 + r53 * a41;
297 uint64_t a36 = a35 + r54 * a41;
298 uint64_t a46 = a45 + r0 * a41;
299 uint64_t t0 = a06;
300 uint64_t t1 = a16;
301 uint64_t t2 = a26;
302 uint64_t t3 = a36;
303 uint64_t t4 = a46;
304 uint64_t mask26 = (uint64_t)0x3ffffffU;
305 uint64_t z0 = t0 >> (uint32_t)26U;
306 uint64_t z1 = t3 >> (uint32_t)26U;
307 uint64_t x0 = t0 & mask26;
308 uint64_t x3 = t3 & mask26;
309 uint64_t x1 = t1 + z0;
310 uint64_t x4 = t4 + z1;
311 uint64_t z01 = x1 >> (uint32_t)26U;
312 uint64_t z11 = x4 >> (uint32_t)26U;
313 uint64_t t = z11 << (uint32_t)2U;
314 uint64_t z12 = z11 + t;
315 uint64_t x11 = x1 & mask26;
316 uint64_t x41 = x4 & mask26;
317 uint64_t x2 = t2 + z01;
318 uint64_t x01 = x0 + z12;
319 uint64_t z02 = x2 >> (uint32_t)26U;
320 uint64_t z13 = x01 >> (uint32_t)26U;
321 uint64_t x21 = x2 & mask26;
322 uint64_t x02 = x01 & mask26;
323 uint64_t x31 = x3 + z02;
324 uint64_t x12 = x11 + z13;
325 uint64_t z03 = x31 >> (uint32_t)26U;
326 uint64_t x32 = x31 & mask26;
327 uint64_t x42 = x41 + z03;
328 uint64_t o0 = x02;
329 uint64_t o1 = x12;
330 uint64_t o2 = x21;
331 uint64_t o3 = x32;
332 uint64_t o4 = x42;
333 acc[0U] = o0;
334 acc[1U] = o1;
335 acc[2U] = o2;
336 acc[3U] = o3;
337 acc[4U] = o4;
338 }
339 if (rem > (uint32_t)0U) {
340 uint8_t *last = text + nb * (uint32_t)16U;
341 uint64_t e[5U] = { 0U };
342 uint8_t tmp[16U] = { 0U };
343 memcpy(tmp, last, rem * sizeof(uint8_t));
344 uint64_t u0 = load64_le(tmp);
345 uint64_t lo = u0;
346 uint64_t u = load64_le(tmp + (uint32_t)8U);
347 uint64_t hi = u;
348 uint64_t f0 = lo;
349 uint64_t f1 = hi;
350 uint64_t f010 = f0 & (uint64_t)0x3ffffffU;
351 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU;
352 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U;
353 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU;
354 uint64_t f40 = f1 >> (uint32_t)40U;
355 uint64_t f01 = f010;
356 uint64_t f111 = f110;
357 uint64_t f2 = f20;
358 uint64_t f3 = f30;
359 uint64_t f4 = f40;
360 e[0U] = f01;
361 e[1U] = f111;
362 e[2U] = f2;
363 e[3U] = f3;
364 e[4U] = f4;
365 uint64_t b = (uint64_t)1U << rem * (uint32_t)8U % (uint32_t)26U;
366 uint64_t mask = b;
367 uint64_t fi = e[rem * (uint32_t)8U / (uint32_t)26U];
368 e[rem * (uint32_t)8U / (uint32_t)26U] = fi | mask;
369 uint64_t *r = pre;
370 uint64_t *r5 = pre + (uint32_t)5U;
371 uint64_t r0 = r[0U];
372 uint64_t r1 = r[1U];
373 uint64_t r2 = r[2U];
374 uint64_t r3 = r[3U];
375 uint64_t r4 = r[4U];
376 uint64_t r51 = r5[1U];
377 uint64_t r52 = r5[2U];
378 uint64_t r53 = r5[3U];
379 uint64_t r54 = r5[4U];
380 uint64_t f10 = e[0U];
381 uint64_t f11 = e[1U];
382 uint64_t f12 = e[2U];
383 uint64_t f13 = e[3U];
384 uint64_t f14 = e[4U];
385 uint64_t a0 = acc[0U];
386 uint64_t a1 = acc[1U];
387 uint64_t a2 = acc[2U];
388 uint64_t a3 = acc[3U];
389 uint64_t a4 = acc[4U];
390 uint64_t a01 = a0 + f10;
391 uint64_t a11 = a1 + f11;
392 uint64_t a21 = a2 + f12;
393 uint64_t a31 = a3 + f13;
394 uint64_t a41 = a4 + f14;
395 uint64_t a02 = r0 * a01;
396 uint64_t a12 = r1 * a01;
397 uint64_t a22 = r2 * a01;
398 uint64_t a32 = r3 * a01;
399 uint64_t a42 = r4 * a01;
400 uint64_t a03 = a02 + r54 * a11;
401 uint64_t a13 = a12 + r0 * a11;
402 uint64_t a23 = a22 + r1 * a11;
403 uint64_t a33 = a32 + r2 * a11;
404 uint64_t a43 = a42 + r3 * a11;
405 uint64_t a04 = a03 + r53 * a21;
406 uint64_t a14 = a13 + r54 * a21;
407 uint64_t a24 = a23 + r0 * a21;
408 uint64_t a34 = a33 + r1 * a21;
409 uint64_t a44 = a43 + r2 * a21;
410 uint64_t a05 = a04 + r52 * a31;
411 uint64_t a15 = a14 + r53 * a31;
412 uint64_t a25 = a24 + r54 * a31;
413 uint64_t a35 = a34 + r0 * a31;
414 uint64_t a45 = a44 + r1 * a31;
415 uint64_t a06 = a05 + r51 * a41;
416 uint64_t a16 = a15 + r52 * a41;
417 uint64_t a26 = a25 + r53 * a41;
418 uint64_t a36 = a35 + r54 * a41;
419 uint64_t a46 = a45 + r0 * a41;
420 uint64_t t0 = a06;
421 uint64_t t1 = a16;
422 uint64_t t2 = a26;
423 uint64_t t3 = a36;
424 uint64_t t4 = a46;
425 uint64_t mask26 = (uint64_t)0x3ffffffU;
426 uint64_t z0 = t0 >> (uint32_t)26U;
427 uint64_t z1 = t3 >> (uint32_t)26U;
428 uint64_t x0 = t0 & mask26;
429 uint64_t x3 = t3 & mask26;
430 uint64_t x1 = t1 + z0;
431 uint64_t x4 = t4 + z1;
432 uint64_t z01 = x1 >> (uint32_t)26U;
433 uint64_t z11 = x4 >> (uint32_t)26U;
434 uint64_t t = z11 << (uint32_t)2U;
435 uint64_t z12 = z11 + t;
436 uint64_t x11 = x1 & mask26;
437 uint64_t x41 = x4 & mask26;
438 uint64_t x2 = t2 + z01;
439 uint64_t x01 = x0 + z12;
440 uint64_t z02 = x2 >> (uint32_t)26U;
441 uint64_t z13 = x01 >> (uint32_t)26U;
442 uint64_t x21 = x2 & mask26;
443 uint64_t x02 = x01 & mask26;
444 uint64_t x31 = x3 + z02;
445 uint64_t x12 = x11 + z13;
446 uint64_t z03 = x31 >> (uint32_t)26U;
447 uint64_t x32 = x31 & mask26;
448 uint64_t x42 = x41 + z03;
449 uint64_t o0 = x02;
450 uint64_t o1 = x12;
451 uint64_t o2 = x21;
452 uint64_t o3 = x32;
453 uint64_t o4 = x42;
454 acc[0U] = o0;
455 acc[1U] = o1;
456 acc[2U] = o2;
457 acc[3U] = o3;
458 acc[4U] = o4;
459 return;
460 }
461 }
462
463 void
Hacl_Poly1305_32_poly1305_finish(uint8_t * tag,uint8_t * key,uint64_t * ctx)464 Hacl_Poly1305_32_poly1305_finish(uint8_t *tag, uint8_t *key, uint64_t *ctx)
465 {
466 uint64_t *acc = ctx;
467 uint8_t *ks = key + (uint32_t)16U;
468 uint64_t f0 = acc[0U];
469 uint64_t f13 = acc[1U];
470 uint64_t f23 = acc[2U];
471 uint64_t f33 = acc[3U];
472 uint64_t f40 = acc[4U];
473 uint64_t l0 = f0 + (uint64_t)0U;
474 uint64_t tmp00 = l0 & (uint64_t)0x3ffffffU;
475 uint64_t c00 = l0 >> (uint32_t)26U;
476 uint64_t l1 = f13 + c00;
477 uint64_t tmp10 = l1 & (uint64_t)0x3ffffffU;
478 uint64_t c10 = l1 >> (uint32_t)26U;
479 uint64_t l2 = f23 + c10;
480 uint64_t tmp20 = l2 & (uint64_t)0x3ffffffU;
481 uint64_t c20 = l2 >> (uint32_t)26U;
482 uint64_t l3 = f33 + c20;
483 uint64_t tmp30 = l3 & (uint64_t)0x3ffffffU;
484 uint64_t c30 = l3 >> (uint32_t)26U;
485 uint64_t l4 = f40 + c30;
486 uint64_t tmp40 = l4 & (uint64_t)0x3ffffffU;
487 uint64_t c40 = l4 >> (uint32_t)26U;
488 uint64_t f010 = tmp00 + c40 * (uint64_t)5U;
489 uint64_t f110 = tmp10;
490 uint64_t f210 = tmp20;
491 uint64_t f310 = tmp30;
492 uint64_t f410 = tmp40;
493 uint64_t l = f010 + (uint64_t)0U;
494 uint64_t tmp0 = l & (uint64_t)0x3ffffffU;
495 uint64_t c0 = l >> (uint32_t)26U;
496 uint64_t l5 = f110 + c0;
497 uint64_t tmp1 = l5 & (uint64_t)0x3ffffffU;
498 uint64_t c1 = l5 >> (uint32_t)26U;
499 uint64_t l6 = f210 + c1;
500 uint64_t tmp2 = l6 & (uint64_t)0x3ffffffU;
501 uint64_t c2 = l6 >> (uint32_t)26U;
502 uint64_t l7 = f310 + c2;
503 uint64_t tmp3 = l7 & (uint64_t)0x3ffffffU;
504 uint64_t c3 = l7 >> (uint32_t)26U;
505 uint64_t l8 = f410 + c3;
506 uint64_t tmp4 = l8 & (uint64_t)0x3ffffffU;
507 uint64_t c4 = l8 >> (uint32_t)26U;
508 uint64_t f02 = tmp0 + c4 * (uint64_t)5U;
509 uint64_t f12 = tmp1;
510 uint64_t f22 = tmp2;
511 uint64_t f32 = tmp3;
512 uint64_t f42 = tmp4;
513 uint64_t mh = (uint64_t)0x3ffffffU;
514 uint64_t ml = (uint64_t)0x3fffffbU;
515 uint64_t mask = FStar_UInt64_eq_mask(f42, mh);
516 uint64_t mask1 = mask & FStar_UInt64_eq_mask(f32, mh);
517 uint64_t mask2 = mask1 & FStar_UInt64_eq_mask(f22, mh);
518 uint64_t mask3 = mask2 & FStar_UInt64_eq_mask(f12, mh);
519 uint64_t mask4 = mask3 & ~~FStar_UInt64_gte_mask(f02, ml);
520 uint64_t ph = mask4 & mh;
521 uint64_t pl = mask4 & ml;
522 uint64_t o0 = f02 - pl;
523 uint64_t o1 = f12 - ph;
524 uint64_t o2 = f22 - ph;
525 uint64_t o3 = f32 - ph;
526 uint64_t o4 = f42 - ph;
527 uint64_t f011 = o0;
528 uint64_t f111 = o1;
529 uint64_t f211 = o2;
530 uint64_t f311 = o3;
531 uint64_t f411 = o4;
532 acc[0U] = f011;
533 acc[1U] = f111;
534 acc[2U] = f211;
535 acc[3U] = f311;
536 acc[4U] = f411;
537 uint64_t f00 = acc[0U];
538 uint64_t f1 = acc[1U];
539 uint64_t f2 = acc[2U];
540 uint64_t f3 = acc[3U];
541 uint64_t f4 = acc[4U];
542 uint64_t f01 = f00;
543 uint64_t f112 = f1;
544 uint64_t f212 = f2;
545 uint64_t f312 = f3;
546 uint64_t f41 = f4;
547 uint64_t lo = (f01 | f112 << (uint32_t)26U) | f212 << (uint32_t)52U;
548 uint64_t hi = (f212 >> (uint32_t)12U | f312 << (uint32_t)14U) | f41 << (uint32_t)40U;
549 uint64_t f10 = lo;
550 uint64_t f11 = hi;
551 uint64_t u0 = load64_le(ks);
552 uint64_t lo0 = u0;
553 uint64_t u = load64_le(ks + (uint32_t)8U);
554 uint64_t hi0 = u;
555 uint64_t f20 = lo0;
556 uint64_t f21 = hi0;
557 uint64_t r0 = f10 + f20;
558 uint64_t r1 = f11 + f21;
559 uint64_t c = (r0 ^ ((r0 ^ f20) | ((r0 - f20) ^ f20))) >> (uint32_t)63U;
560 uint64_t r11 = r1 + c;
561 uint64_t f30 = r0;
562 uint64_t f31 = r11;
563 store64_le(tag, f30);
564 store64_le(tag + (uint32_t)8U, f31);
565 }
566
567 void
Hacl_Poly1305_32_poly1305_mac(uint8_t * tag,uint32_t len,uint8_t * text,uint8_t * key)568 Hacl_Poly1305_32_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key)
569 {
570 uint64_t ctx[25U] = { 0U };
571 Hacl_Poly1305_32_poly1305_init(ctx, key);
572 Hacl_Poly1305_32_poly1305_update(ctx, len, text);
573 Hacl_Poly1305_32_poly1305_finish(tag, key, ctx);
574 }
575