Hacl_Chacha20Poly1305_32.c (21574B)
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_Chacha20Poly1305_32.h" 26 27 #include "internal/Hacl_Krmllib.h" 28 29 static inline void 30 poly1305_padded_32(uint64_t *ctx, uint32_t len, uint8_t *text) 31 { 32 uint32_t n = len / (uint32_t)16U; 33 uint32_t r = len % (uint32_t)16U; 34 uint8_t *blocks = text; 35 uint8_t *rem = text + n * (uint32_t)16U; 36 uint64_t *pre0 = ctx + (uint32_t)5U; 37 uint64_t *acc0 = ctx; 38 uint32_t nb = n * (uint32_t)16U / (uint32_t)16U; 39 uint32_t rem1 = n * (uint32_t)16U % (uint32_t)16U; 40 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 41 uint8_t *block = blocks + i * (uint32_t)16U; 42 uint64_t e[5U] = { 0U }; 43 uint64_t u0 = load64_le(block); 44 uint64_t lo = u0; 45 uint64_t u = load64_le(block + (uint32_t)8U); 46 uint64_t hi = u; 47 uint64_t f0 = lo; 48 uint64_t f1 = hi; 49 uint64_t f010 = f0 & (uint64_t)0x3ffffffU; 50 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU; 51 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U; 52 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU; 53 uint64_t f40 = f1 >> (uint32_t)40U; 54 uint64_t f01 = f010; 55 uint64_t f111 = f110; 56 uint64_t f2 = f20; 57 uint64_t f3 = f30; 58 uint64_t f41 = f40; 59 e[0U] = f01; 60 e[1U] = f111; 61 e[2U] = f2; 62 e[3U] = f3; 63 e[4U] = f41; 64 uint64_t b = (uint64_t)0x1000000U; 65 uint64_t mask = b; 66 uint64_t f4 = e[4U]; 67 e[4U] = f4 | mask; 68 uint64_t *r1 = pre0; 69 uint64_t *r5 = pre0 + (uint32_t)5U; 70 uint64_t r0 = r1[0U]; 71 uint64_t r11 = r1[1U]; 72 uint64_t r2 = r1[2U]; 73 uint64_t r3 = r1[3U]; 74 uint64_t r4 = r1[4U]; 75 uint64_t r51 = r5[1U]; 76 uint64_t r52 = r5[2U]; 77 uint64_t r53 = r5[3U]; 78 uint64_t r54 = r5[4U]; 79 uint64_t f10 = e[0U]; 80 uint64_t f11 = e[1U]; 81 uint64_t f12 = e[2U]; 82 uint64_t f13 = e[3U]; 83 uint64_t f14 = e[4U]; 84 uint64_t a0 = acc0[0U]; 85 uint64_t a1 = acc0[1U]; 86 uint64_t a2 = acc0[2U]; 87 uint64_t a3 = acc0[3U]; 88 uint64_t a4 = acc0[4U]; 89 uint64_t a01 = a0 + f10; 90 uint64_t a11 = a1 + f11; 91 uint64_t a21 = a2 + f12; 92 uint64_t a31 = a3 + f13; 93 uint64_t a41 = a4 + f14; 94 uint64_t a02 = r0 * a01; 95 uint64_t a12 = r11 * a01; 96 uint64_t a22 = r2 * a01; 97 uint64_t a32 = r3 * a01; 98 uint64_t a42 = r4 * a01; 99 uint64_t a03 = a02 + r54 * a11; 100 uint64_t a13 = a12 + r0 * a11; 101 uint64_t a23 = a22 + r11 * a11; 102 uint64_t a33 = a32 + r2 * a11; 103 uint64_t a43 = a42 + r3 * a11; 104 uint64_t a04 = a03 + r53 * a21; 105 uint64_t a14 = a13 + r54 * a21; 106 uint64_t a24 = a23 + r0 * a21; 107 uint64_t a34 = a33 + r11 * a21; 108 uint64_t a44 = a43 + r2 * a21; 109 uint64_t a05 = a04 + r52 * a31; 110 uint64_t a15 = a14 + r53 * a31; 111 uint64_t a25 = a24 + r54 * a31; 112 uint64_t a35 = a34 + r0 * a31; 113 uint64_t a45 = a44 + r11 * a31; 114 uint64_t a06 = a05 + r51 * a41; 115 uint64_t a16 = a15 + r52 * a41; 116 uint64_t a26 = a25 + r53 * a41; 117 uint64_t a36 = a35 + r54 * a41; 118 uint64_t a46 = a45 + r0 * a41; 119 uint64_t t0 = a06; 120 uint64_t t1 = a16; 121 uint64_t t2 = a26; 122 uint64_t t3 = a36; 123 uint64_t t4 = a46; 124 uint64_t mask26 = (uint64_t)0x3ffffffU; 125 uint64_t z0 = t0 >> (uint32_t)26U; 126 uint64_t z1 = t3 >> (uint32_t)26U; 127 uint64_t x0 = t0 & mask26; 128 uint64_t x3 = t3 & mask26; 129 uint64_t x1 = t1 + z0; 130 uint64_t x4 = t4 + z1; 131 uint64_t z01 = x1 >> (uint32_t)26U; 132 uint64_t z11 = x4 >> (uint32_t)26U; 133 uint64_t t = z11 << (uint32_t)2U; 134 uint64_t z12 = z11 + t; 135 uint64_t x11 = x1 & mask26; 136 uint64_t x41 = x4 & mask26; 137 uint64_t x2 = t2 + z01; 138 uint64_t x01 = x0 + z12; 139 uint64_t z02 = x2 >> (uint32_t)26U; 140 uint64_t z13 = x01 >> (uint32_t)26U; 141 uint64_t x21 = x2 & mask26; 142 uint64_t x02 = x01 & mask26; 143 uint64_t x31 = x3 + z02; 144 uint64_t x12 = x11 + z13; 145 uint64_t z03 = x31 >> (uint32_t)26U; 146 uint64_t x32 = x31 & mask26; 147 uint64_t x42 = x41 + z03; 148 uint64_t o0 = x02; 149 uint64_t o1 = x12; 150 uint64_t o2 = x21; 151 uint64_t o3 = x32; 152 uint64_t o4 = x42; 153 acc0[0U] = o0; 154 acc0[1U] = o1; 155 acc0[2U] = o2; 156 acc0[3U] = o3; 157 acc0[4U] = o4; 158 } 159 if (rem1 > (uint32_t)0U) { 160 uint8_t *last = blocks + nb * (uint32_t)16U; 161 uint64_t e[5U] = { 0U }; 162 uint8_t tmp[16U] = { 0U }; 163 memcpy(tmp, last, rem1 * sizeof(uint8_t)); 164 uint64_t u0 = load64_le(tmp); 165 uint64_t lo = u0; 166 uint64_t u = load64_le(tmp + (uint32_t)8U); 167 uint64_t hi = u; 168 uint64_t f0 = lo; 169 uint64_t f1 = hi; 170 uint64_t f010 = f0 & (uint64_t)0x3ffffffU; 171 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU; 172 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U; 173 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU; 174 uint64_t f40 = f1 >> (uint32_t)40U; 175 uint64_t f01 = f010; 176 uint64_t f111 = f110; 177 uint64_t f2 = f20; 178 uint64_t f3 = f30; 179 uint64_t f4 = f40; 180 e[0U] = f01; 181 e[1U] = f111; 182 e[2U] = f2; 183 e[3U] = f3; 184 e[4U] = f4; 185 uint64_t b = (uint64_t)1U << rem1 * (uint32_t)8U % (uint32_t)26U; 186 uint64_t mask = b; 187 uint64_t fi = e[rem1 * (uint32_t)8U / (uint32_t)26U]; 188 e[rem1 * (uint32_t)8U / (uint32_t)26U] = fi | mask; 189 uint64_t *r1 = pre0; 190 uint64_t *r5 = pre0 + (uint32_t)5U; 191 uint64_t r0 = r1[0U]; 192 uint64_t r11 = r1[1U]; 193 uint64_t r2 = r1[2U]; 194 uint64_t r3 = r1[3U]; 195 uint64_t r4 = r1[4U]; 196 uint64_t r51 = r5[1U]; 197 uint64_t r52 = r5[2U]; 198 uint64_t r53 = r5[3U]; 199 uint64_t r54 = r5[4U]; 200 uint64_t f10 = e[0U]; 201 uint64_t f11 = e[1U]; 202 uint64_t f12 = e[2U]; 203 uint64_t f13 = e[3U]; 204 uint64_t f14 = e[4U]; 205 uint64_t a0 = acc0[0U]; 206 uint64_t a1 = acc0[1U]; 207 uint64_t a2 = acc0[2U]; 208 uint64_t a3 = acc0[3U]; 209 uint64_t a4 = acc0[4U]; 210 uint64_t a01 = a0 + f10; 211 uint64_t a11 = a1 + f11; 212 uint64_t a21 = a2 + f12; 213 uint64_t a31 = a3 + f13; 214 uint64_t a41 = a4 + f14; 215 uint64_t a02 = r0 * a01; 216 uint64_t a12 = r11 * a01; 217 uint64_t a22 = r2 * a01; 218 uint64_t a32 = r3 * a01; 219 uint64_t a42 = r4 * a01; 220 uint64_t a03 = a02 + r54 * a11; 221 uint64_t a13 = a12 + r0 * a11; 222 uint64_t a23 = a22 + r11 * a11; 223 uint64_t a33 = a32 + r2 * a11; 224 uint64_t a43 = a42 + r3 * a11; 225 uint64_t a04 = a03 + r53 * a21; 226 uint64_t a14 = a13 + r54 * a21; 227 uint64_t a24 = a23 + r0 * a21; 228 uint64_t a34 = a33 + r11 * a21; 229 uint64_t a44 = a43 + r2 * a21; 230 uint64_t a05 = a04 + r52 * a31; 231 uint64_t a15 = a14 + r53 * a31; 232 uint64_t a25 = a24 + r54 * a31; 233 uint64_t a35 = a34 + r0 * a31; 234 uint64_t a45 = a44 + r11 * a31; 235 uint64_t a06 = a05 + r51 * a41; 236 uint64_t a16 = a15 + r52 * a41; 237 uint64_t a26 = a25 + r53 * a41; 238 uint64_t a36 = a35 + r54 * a41; 239 uint64_t a46 = a45 + r0 * a41; 240 uint64_t t0 = a06; 241 uint64_t t1 = a16; 242 uint64_t t2 = a26; 243 uint64_t t3 = a36; 244 uint64_t t4 = a46; 245 uint64_t mask26 = (uint64_t)0x3ffffffU; 246 uint64_t z0 = t0 >> (uint32_t)26U; 247 uint64_t z1 = t3 >> (uint32_t)26U; 248 uint64_t x0 = t0 & mask26; 249 uint64_t x3 = t3 & mask26; 250 uint64_t x1 = t1 + z0; 251 uint64_t x4 = t4 + z1; 252 uint64_t z01 = x1 >> (uint32_t)26U; 253 uint64_t z11 = x4 >> (uint32_t)26U; 254 uint64_t t = z11 << (uint32_t)2U; 255 uint64_t z12 = z11 + t; 256 uint64_t x11 = x1 & mask26; 257 uint64_t x41 = x4 & mask26; 258 uint64_t x2 = t2 + z01; 259 uint64_t x01 = x0 + z12; 260 uint64_t z02 = x2 >> (uint32_t)26U; 261 uint64_t z13 = x01 >> (uint32_t)26U; 262 uint64_t x21 = x2 & mask26; 263 uint64_t x02 = x01 & mask26; 264 uint64_t x31 = x3 + z02; 265 uint64_t x12 = x11 + z13; 266 uint64_t z03 = x31 >> (uint32_t)26U; 267 uint64_t x32 = x31 & mask26; 268 uint64_t x42 = x41 + z03; 269 uint64_t o0 = x02; 270 uint64_t o1 = x12; 271 uint64_t o2 = x21; 272 uint64_t o3 = x32; 273 uint64_t o4 = x42; 274 acc0[0U] = o0; 275 acc0[1U] = o1; 276 acc0[2U] = o2; 277 acc0[3U] = o3; 278 acc0[4U] = o4; 279 } 280 uint8_t tmp[16U] = { 0U }; 281 memcpy(tmp, rem, r * sizeof(uint8_t)); 282 if (r > (uint32_t)0U) { 283 uint64_t *pre = ctx + (uint32_t)5U; 284 uint64_t *acc = ctx; 285 uint64_t e[5U] = { 0U }; 286 uint64_t u0 = load64_le(tmp); 287 uint64_t lo = u0; 288 uint64_t u = load64_le(tmp + (uint32_t)8U); 289 uint64_t hi = u; 290 uint64_t f0 = lo; 291 uint64_t f1 = hi; 292 uint64_t f010 = f0 & (uint64_t)0x3ffffffU; 293 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU; 294 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U; 295 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU; 296 uint64_t f40 = f1 >> (uint32_t)40U; 297 uint64_t f01 = f010; 298 uint64_t f111 = f110; 299 uint64_t f2 = f20; 300 uint64_t f3 = f30; 301 uint64_t f41 = f40; 302 e[0U] = f01; 303 e[1U] = f111; 304 e[2U] = f2; 305 e[3U] = f3; 306 e[4U] = f41; 307 uint64_t b = (uint64_t)0x1000000U; 308 uint64_t mask = b; 309 uint64_t f4 = e[4U]; 310 e[4U] = f4 | mask; 311 uint64_t *r1 = pre; 312 uint64_t *r5 = pre + (uint32_t)5U; 313 uint64_t r0 = r1[0U]; 314 uint64_t r11 = r1[1U]; 315 uint64_t r2 = r1[2U]; 316 uint64_t r3 = r1[3U]; 317 uint64_t r4 = r1[4U]; 318 uint64_t r51 = r5[1U]; 319 uint64_t r52 = r5[2U]; 320 uint64_t r53 = r5[3U]; 321 uint64_t r54 = r5[4U]; 322 uint64_t f10 = e[0U]; 323 uint64_t f11 = e[1U]; 324 uint64_t f12 = e[2U]; 325 uint64_t f13 = e[3U]; 326 uint64_t f14 = e[4U]; 327 uint64_t a0 = acc[0U]; 328 uint64_t a1 = acc[1U]; 329 uint64_t a2 = acc[2U]; 330 uint64_t a3 = acc[3U]; 331 uint64_t a4 = acc[4U]; 332 uint64_t a01 = a0 + f10; 333 uint64_t a11 = a1 + f11; 334 uint64_t a21 = a2 + f12; 335 uint64_t a31 = a3 + f13; 336 uint64_t a41 = a4 + f14; 337 uint64_t a02 = r0 * a01; 338 uint64_t a12 = r11 * a01; 339 uint64_t a22 = r2 * a01; 340 uint64_t a32 = r3 * a01; 341 uint64_t a42 = r4 * a01; 342 uint64_t a03 = a02 + r54 * a11; 343 uint64_t a13 = a12 + r0 * a11; 344 uint64_t a23 = a22 + r11 * a11; 345 uint64_t a33 = a32 + r2 * a11; 346 uint64_t a43 = a42 + r3 * a11; 347 uint64_t a04 = a03 + r53 * a21; 348 uint64_t a14 = a13 + r54 * a21; 349 uint64_t a24 = a23 + r0 * a21; 350 uint64_t a34 = a33 + r11 * a21; 351 uint64_t a44 = a43 + r2 * a21; 352 uint64_t a05 = a04 + r52 * a31; 353 uint64_t a15 = a14 + r53 * a31; 354 uint64_t a25 = a24 + r54 * a31; 355 uint64_t a35 = a34 + r0 * a31; 356 uint64_t a45 = a44 + r11 * a31; 357 uint64_t a06 = a05 + r51 * a41; 358 uint64_t a16 = a15 + r52 * a41; 359 uint64_t a26 = a25 + r53 * a41; 360 uint64_t a36 = a35 + r54 * a41; 361 uint64_t a46 = a45 + r0 * a41; 362 uint64_t t0 = a06; 363 uint64_t t1 = a16; 364 uint64_t t2 = a26; 365 uint64_t t3 = a36; 366 uint64_t t4 = a46; 367 uint64_t mask26 = (uint64_t)0x3ffffffU; 368 uint64_t z0 = t0 >> (uint32_t)26U; 369 uint64_t z1 = t3 >> (uint32_t)26U; 370 uint64_t x0 = t0 & mask26; 371 uint64_t x3 = t3 & mask26; 372 uint64_t x1 = t1 + z0; 373 uint64_t x4 = t4 + z1; 374 uint64_t z01 = x1 >> (uint32_t)26U; 375 uint64_t z11 = x4 >> (uint32_t)26U; 376 uint64_t t = z11 << (uint32_t)2U; 377 uint64_t z12 = z11 + t; 378 uint64_t x11 = x1 & mask26; 379 uint64_t x41 = x4 & mask26; 380 uint64_t x2 = t2 + z01; 381 uint64_t x01 = x0 + z12; 382 uint64_t z02 = x2 >> (uint32_t)26U; 383 uint64_t z13 = x01 >> (uint32_t)26U; 384 uint64_t x21 = x2 & mask26; 385 uint64_t x02 = x01 & mask26; 386 uint64_t x31 = x3 + z02; 387 uint64_t x12 = x11 + z13; 388 uint64_t z03 = x31 >> (uint32_t)26U; 389 uint64_t x32 = x31 & mask26; 390 uint64_t x42 = x41 + z03; 391 uint64_t o0 = x02; 392 uint64_t o1 = x12; 393 uint64_t o2 = x21; 394 uint64_t o3 = x32; 395 uint64_t o4 = x42; 396 acc[0U] = o0; 397 acc[1U] = o1; 398 acc[2U] = o2; 399 acc[3U] = o3; 400 acc[4U] = o4; 401 return; 402 } 403 } 404 405 static inline void 406 poly1305_do_32( 407 uint8_t *k, 408 uint32_t aadlen, 409 uint8_t *aad, 410 uint32_t mlen, 411 uint8_t *m, 412 uint8_t *out) 413 { 414 uint64_t ctx[25U] = { 0U }; 415 uint8_t block[16U] = { 0U }; 416 Hacl_Poly1305_32_poly1305_init(ctx, k); 417 if (aadlen != (uint32_t)0U) { 418 poly1305_padded_32(ctx, aadlen, aad); 419 } 420 if (mlen != (uint32_t)0U) { 421 poly1305_padded_32(ctx, mlen, m); 422 } 423 store64_le(block, (uint64_t)aadlen); 424 store64_le(block + (uint32_t)8U, (uint64_t)mlen); 425 uint64_t *pre = ctx + (uint32_t)5U; 426 uint64_t *acc = ctx; 427 uint64_t e[5U] = { 0U }; 428 uint64_t u0 = load64_le(block); 429 uint64_t lo = u0; 430 uint64_t u = load64_le(block + (uint32_t)8U); 431 uint64_t hi = u; 432 uint64_t f0 = lo; 433 uint64_t f1 = hi; 434 uint64_t f010 = f0 & (uint64_t)0x3ffffffU; 435 uint64_t f110 = f0 >> (uint32_t)26U & (uint64_t)0x3ffffffU; 436 uint64_t f20 = f0 >> (uint32_t)52U | (f1 & (uint64_t)0x3fffU) << (uint32_t)12U; 437 uint64_t f30 = f1 >> (uint32_t)14U & (uint64_t)0x3ffffffU; 438 uint64_t f40 = f1 >> (uint32_t)40U; 439 uint64_t f01 = f010; 440 uint64_t f111 = f110; 441 uint64_t f2 = f20; 442 uint64_t f3 = f30; 443 uint64_t f41 = f40; 444 e[0U] = f01; 445 e[1U] = f111; 446 e[2U] = f2; 447 e[3U] = f3; 448 e[4U] = f41; 449 uint64_t b = (uint64_t)0x1000000U; 450 uint64_t mask = b; 451 uint64_t f4 = e[4U]; 452 e[4U] = f4 | mask; 453 uint64_t *r = pre; 454 uint64_t *r5 = pre + (uint32_t)5U; 455 uint64_t r0 = r[0U]; 456 uint64_t r1 = r[1U]; 457 uint64_t r2 = r[2U]; 458 uint64_t r3 = r[3U]; 459 uint64_t r4 = r[4U]; 460 uint64_t r51 = r5[1U]; 461 uint64_t r52 = r5[2U]; 462 uint64_t r53 = r5[3U]; 463 uint64_t r54 = r5[4U]; 464 uint64_t f10 = e[0U]; 465 uint64_t f11 = e[1U]; 466 uint64_t f12 = e[2U]; 467 uint64_t f13 = e[3U]; 468 uint64_t f14 = e[4U]; 469 uint64_t a0 = acc[0U]; 470 uint64_t a1 = acc[1U]; 471 uint64_t a2 = acc[2U]; 472 uint64_t a3 = acc[3U]; 473 uint64_t a4 = acc[4U]; 474 uint64_t a01 = a0 + f10; 475 uint64_t a11 = a1 + f11; 476 uint64_t a21 = a2 + f12; 477 uint64_t a31 = a3 + f13; 478 uint64_t a41 = a4 + f14; 479 uint64_t a02 = r0 * a01; 480 uint64_t a12 = r1 * a01; 481 uint64_t a22 = r2 * a01; 482 uint64_t a32 = r3 * a01; 483 uint64_t a42 = r4 * a01; 484 uint64_t a03 = a02 + r54 * a11; 485 uint64_t a13 = a12 + r0 * a11; 486 uint64_t a23 = a22 + r1 * a11; 487 uint64_t a33 = a32 + r2 * a11; 488 uint64_t a43 = a42 + r3 * a11; 489 uint64_t a04 = a03 + r53 * a21; 490 uint64_t a14 = a13 + r54 * a21; 491 uint64_t a24 = a23 + r0 * a21; 492 uint64_t a34 = a33 + r1 * a21; 493 uint64_t a44 = a43 + r2 * a21; 494 uint64_t a05 = a04 + r52 * a31; 495 uint64_t a15 = a14 + r53 * a31; 496 uint64_t a25 = a24 + r54 * a31; 497 uint64_t a35 = a34 + r0 * a31; 498 uint64_t a45 = a44 + r1 * a31; 499 uint64_t a06 = a05 + r51 * a41; 500 uint64_t a16 = a15 + r52 * a41; 501 uint64_t a26 = a25 + r53 * a41; 502 uint64_t a36 = a35 + r54 * a41; 503 uint64_t a46 = a45 + r0 * a41; 504 uint64_t t0 = a06; 505 uint64_t t1 = a16; 506 uint64_t t2 = a26; 507 uint64_t t3 = a36; 508 uint64_t t4 = a46; 509 uint64_t mask26 = (uint64_t)0x3ffffffU; 510 uint64_t z0 = t0 >> (uint32_t)26U; 511 uint64_t z1 = t3 >> (uint32_t)26U; 512 uint64_t x0 = t0 & mask26; 513 uint64_t x3 = t3 & mask26; 514 uint64_t x1 = t1 + z0; 515 uint64_t x4 = t4 + z1; 516 uint64_t z01 = x1 >> (uint32_t)26U; 517 uint64_t z11 = x4 >> (uint32_t)26U; 518 uint64_t t = z11 << (uint32_t)2U; 519 uint64_t z12 = z11 + t; 520 uint64_t x11 = x1 & mask26; 521 uint64_t x41 = x4 & mask26; 522 uint64_t x2 = t2 + z01; 523 uint64_t x01 = x0 + z12; 524 uint64_t z02 = x2 >> (uint32_t)26U; 525 uint64_t z13 = x01 >> (uint32_t)26U; 526 uint64_t x21 = x2 & mask26; 527 uint64_t x02 = x01 & mask26; 528 uint64_t x31 = x3 + z02; 529 uint64_t x12 = x11 + z13; 530 uint64_t z03 = x31 >> (uint32_t)26U; 531 uint64_t x32 = x31 & mask26; 532 uint64_t x42 = x41 + z03; 533 uint64_t o0 = x02; 534 uint64_t o1 = x12; 535 uint64_t o2 = x21; 536 uint64_t o3 = x32; 537 uint64_t o4 = x42; 538 acc[0U] = o0; 539 acc[1U] = o1; 540 acc[2U] = o2; 541 acc[3U] = o3; 542 acc[4U] = o4; 543 Hacl_Poly1305_32_poly1305_finish(out, k, ctx); 544 } 545 546 /** 547 Encrypt a message `m` with key `k`. 548 549 The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption. 550 Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory. 551 552 @param k Pointer to 32 bytes of memory where the AEAD key is read from. 553 @param n Pointer to 12 bytes of memory where the AEAD nonce is read from. 554 @param aadlen Length of the associated data. 555 @param aad Pointer to `aadlen` bytes of memory where the associated data is read from. 556 557 @param mlen Length of the message. 558 @param m Pointer to `mlen` bytes of memory where the message is read from. 559 @param cipher Pointer to `mlen` bytes of memory where the ciphertext is written to. 560 @param mac Pointer to 16 bytes of memory where the mac is written to. 561 */ 562 void 563 Hacl_Chacha20Poly1305_32_aead_encrypt( 564 uint8_t *k, 565 uint8_t *n, 566 uint32_t aadlen, 567 uint8_t *aad, 568 uint32_t mlen, 569 uint8_t *m, 570 uint8_t *cipher, 571 uint8_t *mac) 572 { 573 Hacl_Chacha20_chacha20_encrypt(mlen, cipher, m, k, n, (uint32_t)1U); 574 uint8_t tmp[64U] = { 0U }; 575 Hacl_Chacha20_chacha20_encrypt((uint32_t)64U, tmp, tmp, k, n, (uint32_t)0U); 576 uint8_t *key = tmp; 577 poly1305_do_32(key, aadlen, aad, mlen, cipher, mac); 578 } 579 580 /** 581 Decrypt a ciphertext `cipher` with key `k`. 582 583 The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption. 584 Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory. 585 586 If decryption succeeds, the resulting plaintext is stored in `m` and the function returns the success code 0. 587 If decryption fails, the array `m` remains unchanged and the function returns the error code 1. 588 589 @param k Pointer to 32 bytes of memory where the AEAD key is read from. 590 @param n Pointer to 12 bytes of memory where the AEAD nonce is read from. 591 @param aadlen Length of the associated data. 592 @param aad Pointer to `aadlen` bytes of memory where the associated data is read from. 593 594 @param mlen Length of the ciphertext. 595 @param m Pointer to `mlen` bytes of memory where the message is written to. 596 @param cipher Pointer to `mlen` bytes of memory where the ciphertext is read from. 597 @param mac Pointer to 16 bytes of memory where the mac is read from. 598 599 @returns 0 on succeess; 1 on failure. 600 */ 601 uint32_t 602 Hacl_Chacha20Poly1305_32_aead_decrypt( 603 uint8_t *k, 604 uint8_t *n, 605 uint32_t aadlen, 606 uint8_t *aad, 607 uint32_t mlen, 608 uint8_t *m, 609 uint8_t *cipher, 610 uint8_t *mac) 611 { 612 uint8_t computed_mac[16U] = { 0U }; 613 uint8_t tmp[64U] = { 0U }; 614 Hacl_Chacha20_chacha20_encrypt((uint32_t)64U, tmp, tmp, k, n, (uint32_t)0U); 615 uint8_t *key = tmp; 616 poly1305_do_32(key, aadlen, aad, mlen, cipher, computed_mac); 617 uint8_t res = (uint8_t)255U; 618 KRML_MAYBE_FOR16(i, 619 (uint32_t)0U, 620 (uint32_t)16U, 621 (uint32_t)1U, 622 uint8_t uu____0 = FStar_UInt8_eq_mask(computed_mac[i], mac[i]); 623 res = uu____0 & res;); 624 uint8_t z = res; 625 if (z == (uint8_t)255U) { 626 Hacl_Chacha20_chacha20_encrypt(mlen, m, cipher, k, n, (uint32_t)1U); 627 return (uint32_t)0U; 628 } 629 return (uint32_t)1U; 630 }