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