Hacl_Poly1305_256.c (120385B)
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 "internal/Hacl_Poly1305_256.h" 26 27 void 28 Hacl_Impl_Poly1305_Field32xN_256_load_acc4(Lib_IntVector_Intrinsics_vec256 *acc, uint8_t *b) 29 { 30 KRML_PRE_ALIGN(32) 31 Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; 32 Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(b); 33 Lib_IntVector_Intrinsics_vec256 34 hi = Lib_IntVector_Intrinsics_vec256_load64_le(b + (uint32_t)32U); 35 Lib_IntVector_Intrinsics_vec256 36 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 37 Lib_IntVector_Intrinsics_vec256 m0 = Lib_IntVector_Intrinsics_vec256_interleave_low128(lo, hi); 38 Lib_IntVector_Intrinsics_vec256 39 m1 = Lib_IntVector_Intrinsics_vec256_interleave_high128(lo, hi); 40 Lib_IntVector_Intrinsics_vec256 41 m2 = Lib_IntVector_Intrinsics_vec256_shift_right(m0, (uint32_t)48U); 42 Lib_IntVector_Intrinsics_vec256 43 m3 = Lib_IntVector_Intrinsics_vec256_shift_right(m1, (uint32_t)48U); 44 Lib_IntVector_Intrinsics_vec256 m4 = Lib_IntVector_Intrinsics_vec256_interleave_high64(m0, m1); 45 Lib_IntVector_Intrinsics_vec256 t0 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m0, m1); 46 Lib_IntVector_Intrinsics_vec256 t3 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m2, m3); 47 Lib_IntVector_Intrinsics_vec256 48 t2 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)4U); 49 Lib_IntVector_Intrinsics_vec256 o20 = Lib_IntVector_Intrinsics_vec256_and(t2, mask26); 50 Lib_IntVector_Intrinsics_vec256 51 t1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); 52 Lib_IntVector_Intrinsics_vec256 o10 = Lib_IntVector_Intrinsics_vec256_and(t1, mask26); 53 Lib_IntVector_Intrinsics_vec256 o5 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); 54 Lib_IntVector_Intrinsics_vec256 55 t31 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)30U); 56 Lib_IntVector_Intrinsics_vec256 o30 = Lib_IntVector_Intrinsics_vec256_and(t31, mask26); 57 Lib_IntVector_Intrinsics_vec256 58 o40 = Lib_IntVector_Intrinsics_vec256_shift_right64(m4, (uint32_t)40U); 59 Lib_IntVector_Intrinsics_vec256 o0 = o5; 60 Lib_IntVector_Intrinsics_vec256 o1 = o10; 61 Lib_IntVector_Intrinsics_vec256 o2 = o20; 62 Lib_IntVector_Intrinsics_vec256 o3 = o30; 63 Lib_IntVector_Intrinsics_vec256 o4 = o40; 64 e[0U] = o0; 65 e[1U] = o1; 66 e[2U] = o2; 67 e[3U] = o3; 68 e[4U] = o4; 69 uint64_t b1 = (uint64_t)0x1000000U; 70 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b1); 71 Lib_IntVector_Intrinsics_vec256 f40 = e[4U]; 72 e[4U] = Lib_IntVector_Intrinsics_vec256_or(f40, mask); 73 Lib_IntVector_Intrinsics_vec256 acc0 = acc[0U]; 74 Lib_IntVector_Intrinsics_vec256 acc1 = acc[1U]; 75 Lib_IntVector_Intrinsics_vec256 acc2 = acc[2U]; 76 Lib_IntVector_Intrinsics_vec256 acc3 = acc[3U]; 77 Lib_IntVector_Intrinsics_vec256 acc4 = acc[4U]; 78 Lib_IntVector_Intrinsics_vec256 e0 = e[0U]; 79 Lib_IntVector_Intrinsics_vec256 e1 = e[1U]; 80 Lib_IntVector_Intrinsics_vec256 e2 = e[2U]; 81 Lib_IntVector_Intrinsics_vec256 e3 = e[3U]; 82 Lib_IntVector_Intrinsics_vec256 e4 = e[4U]; 83 Lib_IntVector_Intrinsics_vec256 r0 = Lib_IntVector_Intrinsics_vec256_zero; 84 Lib_IntVector_Intrinsics_vec256 r1 = Lib_IntVector_Intrinsics_vec256_zero; 85 Lib_IntVector_Intrinsics_vec256 r2 = Lib_IntVector_Intrinsics_vec256_zero; 86 Lib_IntVector_Intrinsics_vec256 r3 = Lib_IntVector_Intrinsics_vec256_zero; 87 Lib_IntVector_Intrinsics_vec256 r4 = Lib_IntVector_Intrinsics_vec256_zero; 88 Lib_IntVector_Intrinsics_vec256 89 r01 = 90 Lib_IntVector_Intrinsics_vec256_insert64(r0, 91 Lib_IntVector_Intrinsics_vec256_extract64(acc0, (uint32_t)0U), 92 (uint32_t)0U); 93 Lib_IntVector_Intrinsics_vec256 94 r11 = 95 Lib_IntVector_Intrinsics_vec256_insert64(r1, 96 Lib_IntVector_Intrinsics_vec256_extract64(acc1, (uint32_t)0U), 97 (uint32_t)0U); 98 Lib_IntVector_Intrinsics_vec256 99 r21 = 100 Lib_IntVector_Intrinsics_vec256_insert64(r2, 101 Lib_IntVector_Intrinsics_vec256_extract64(acc2, (uint32_t)0U), 102 (uint32_t)0U); 103 Lib_IntVector_Intrinsics_vec256 104 r31 = 105 Lib_IntVector_Intrinsics_vec256_insert64(r3, 106 Lib_IntVector_Intrinsics_vec256_extract64(acc3, (uint32_t)0U), 107 (uint32_t)0U); 108 Lib_IntVector_Intrinsics_vec256 109 r41 = 110 Lib_IntVector_Intrinsics_vec256_insert64(r4, 111 Lib_IntVector_Intrinsics_vec256_extract64(acc4, (uint32_t)0U), 112 (uint32_t)0U); 113 Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_add64(r01, e0); 114 Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_add64(r11, e1); 115 Lib_IntVector_Intrinsics_vec256 f2 = Lib_IntVector_Intrinsics_vec256_add64(r21, e2); 116 Lib_IntVector_Intrinsics_vec256 f3 = Lib_IntVector_Intrinsics_vec256_add64(r31, e3); 117 Lib_IntVector_Intrinsics_vec256 f4 = Lib_IntVector_Intrinsics_vec256_add64(r41, e4); 118 Lib_IntVector_Intrinsics_vec256 acc01 = f0; 119 Lib_IntVector_Intrinsics_vec256 acc11 = f1; 120 Lib_IntVector_Intrinsics_vec256 acc21 = f2; 121 Lib_IntVector_Intrinsics_vec256 acc31 = f3; 122 Lib_IntVector_Intrinsics_vec256 acc41 = f4; 123 acc[0U] = acc01; 124 acc[1U] = acc11; 125 acc[2U] = acc21; 126 acc[3U] = acc31; 127 acc[4U] = acc41; 128 } 129 130 void 131 Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize( 132 Lib_IntVector_Intrinsics_vec256 *out, 133 Lib_IntVector_Intrinsics_vec256 *p) 134 { 135 Lib_IntVector_Intrinsics_vec256 *r = p; 136 Lib_IntVector_Intrinsics_vec256 *r_5 = p + (uint32_t)5U; 137 Lib_IntVector_Intrinsics_vec256 *r4 = p + (uint32_t)10U; 138 Lib_IntVector_Intrinsics_vec256 a0 = out[0U]; 139 Lib_IntVector_Intrinsics_vec256 a1 = out[1U]; 140 Lib_IntVector_Intrinsics_vec256 a2 = out[2U]; 141 Lib_IntVector_Intrinsics_vec256 a3 = out[3U]; 142 Lib_IntVector_Intrinsics_vec256 a4 = out[4U]; 143 Lib_IntVector_Intrinsics_vec256 r10 = r[0U]; 144 Lib_IntVector_Intrinsics_vec256 r11 = r[1U]; 145 Lib_IntVector_Intrinsics_vec256 r12 = r[2U]; 146 Lib_IntVector_Intrinsics_vec256 r13 = r[3U]; 147 Lib_IntVector_Intrinsics_vec256 r14 = r[4U]; 148 Lib_IntVector_Intrinsics_vec256 r151 = r_5[1U]; 149 Lib_IntVector_Intrinsics_vec256 r152 = r_5[2U]; 150 Lib_IntVector_Intrinsics_vec256 r153 = r_5[3U]; 151 Lib_IntVector_Intrinsics_vec256 r154 = r_5[4U]; 152 Lib_IntVector_Intrinsics_vec256 r40 = r4[0U]; 153 Lib_IntVector_Intrinsics_vec256 r41 = r4[1U]; 154 Lib_IntVector_Intrinsics_vec256 r42 = r4[2U]; 155 Lib_IntVector_Intrinsics_vec256 r43 = r4[3U]; 156 Lib_IntVector_Intrinsics_vec256 r44 = r4[4U]; 157 Lib_IntVector_Intrinsics_vec256 a010 = Lib_IntVector_Intrinsics_vec256_mul64(r10, r10); 158 Lib_IntVector_Intrinsics_vec256 a110 = Lib_IntVector_Intrinsics_vec256_mul64(r11, r10); 159 Lib_IntVector_Intrinsics_vec256 a210 = Lib_IntVector_Intrinsics_vec256_mul64(r12, r10); 160 Lib_IntVector_Intrinsics_vec256 a310 = Lib_IntVector_Intrinsics_vec256_mul64(r13, r10); 161 Lib_IntVector_Intrinsics_vec256 a410 = Lib_IntVector_Intrinsics_vec256_mul64(r14, r10); 162 Lib_IntVector_Intrinsics_vec256 163 a020 = 164 Lib_IntVector_Intrinsics_vec256_add64(a010, 165 Lib_IntVector_Intrinsics_vec256_mul64(r154, r11)); 166 Lib_IntVector_Intrinsics_vec256 167 a120 = 168 Lib_IntVector_Intrinsics_vec256_add64(a110, 169 Lib_IntVector_Intrinsics_vec256_mul64(r10, r11)); 170 Lib_IntVector_Intrinsics_vec256 171 a220 = 172 Lib_IntVector_Intrinsics_vec256_add64(a210, 173 Lib_IntVector_Intrinsics_vec256_mul64(r11, r11)); 174 Lib_IntVector_Intrinsics_vec256 175 a320 = 176 Lib_IntVector_Intrinsics_vec256_add64(a310, 177 Lib_IntVector_Intrinsics_vec256_mul64(r12, r11)); 178 Lib_IntVector_Intrinsics_vec256 179 a420 = 180 Lib_IntVector_Intrinsics_vec256_add64(a410, 181 Lib_IntVector_Intrinsics_vec256_mul64(r13, r11)); 182 Lib_IntVector_Intrinsics_vec256 183 a030 = 184 Lib_IntVector_Intrinsics_vec256_add64(a020, 185 Lib_IntVector_Intrinsics_vec256_mul64(r153, r12)); 186 Lib_IntVector_Intrinsics_vec256 187 a130 = 188 Lib_IntVector_Intrinsics_vec256_add64(a120, 189 Lib_IntVector_Intrinsics_vec256_mul64(r154, r12)); 190 Lib_IntVector_Intrinsics_vec256 191 a230 = 192 Lib_IntVector_Intrinsics_vec256_add64(a220, 193 Lib_IntVector_Intrinsics_vec256_mul64(r10, r12)); 194 Lib_IntVector_Intrinsics_vec256 195 a330 = 196 Lib_IntVector_Intrinsics_vec256_add64(a320, 197 Lib_IntVector_Intrinsics_vec256_mul64(r11, r12)); 198 Lib_IntVector_Intrinsics_vec256 199 a430 = 200 Lib_IntVector_Intrinsics_vec256_add64(a420, 201 Lib_IntVector_Intrinsics_vec256_mul64(r12, r12)); 202 Lib_IntVector_Intrinsics_vec256 203 a040 = 204 Lib_IntVector_Intrinsics_vec256_add64(a030, 205 Lib_IntVector_Intrinsics_vec256_mul64(r152, r13)); 206 Lib_IntVector_Intrinsics_vec256 207 a140 = 208 Lib_IntVector_Intrinsics_vec256_add64(a130, 209 Lib_IntVector_Intrinsics_vec256_mul64(r153, r13)); 210 Lib_IntVector_Intrinsics_vec256 211 a240 = 212 Lib_IntVector_Intrinsics_vec256_add64(a230, 213 Lib_IntVector_Intrinsics_vec256_mul64(r154, r13)); 214 Lib_IntVector_Intrinsics_vec256 215 a340 = 216 Lib_IntVector_Intrinsics_vec256_add64(a330, 217 Lib_IntVector_Intrinsics_vec256_mul64(r10, r13)); 218 Lib_IntVector_Intrinsics_vec256 219 a440 = 220 Lib_IntVector_Intrinsics_vec256_add64(a430, 221 Lib_IntVector_Intrinsics_vec256_mul64(r11, r13)); 222 Lib_IntVector_Intrinsics_vec256 223 a050 = 224 Lib_IntVector_Intrinsics_vec256_add64(a040, 225 Lib_IntVector_Intrinsics_vec256_mul64(r151, r14)); 226 Lib_IntVector_Intrinsics_vec256 227 a150 = 228 Lib_IntVector_Intrinsics_vec256_add64(a140, 229 Lib_IntVector_Intrinsics_vec256_mul64(r152, r14)); 230 Lib_IntVector_Intrinsics_vec256 231 a250 = 232 Lib_IntVector_Intrinsics_vec256_add64(a240, 233 Lib_IntVector_Intrinsics_vec256_mul64(r153, r14)); 234 Lib_IntVector_Intrinsics_vec256 235 a350 = 236 Lib_IntVector_Intrinsics_vec256_add64(a340, 237 Lib_IntVector_Intrinsics_vec256_mul64(r154, r14)); 238 Lib_IntVector_Intrinsics_vec256 239 a450 = 240 Lib_IntVector_Intrinsics_vec256_add64(a440, 241 Lib_IntVector_Intrinsics_vec256_mul64(r10, r14)); 242 Lib_IntVector_Intrinsics_vec256 t00 = a050; 243 Lib_IntVector_Intrinsics_vec256 t10 = a150; 244 Lib_IntVector_Intrinsics_vec256 t20 = a250; 245 Lib_IntVector_Intrinsics_vec256 t30 = a350; 246 Lib_IntVector_Intrinsics_vec256 t40 = a450; 247 Lib_IntVector_Intrinsics_vec256 248 mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 249 Lib_IntVector_Intrinsics_vec256 250 z00 = Lib_IntVector_Intrinsics_vec256_shift_right64(t00, (uint32_t)26U); 251 Lib_IntVector_Intrinsics_vec256 252 z10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)26U); 253 Lib_IntVector_Intrinsics_vec256 x00 = Lib_IntVector_Intrinsics_vec256_and(t00, mask260); 254 Lib_IntVector_Intrinsics_vec256 x30 = Lib_IntVector_Intrinsics_vec256_and(t30, mask260); 255 Lib_IntVector_Intrinsics_vec256 x10 = Lib_IntVector_Intrinsics_vec256_add64(t10, z00); 256 Lib_IntVector_Intrinsics_vec256 x40 = Lib_IntVector_Intrinsics_vec256_add64(t40, z10); 257 Lib_IntVector_Intrinsics_vec256 258 z010 = Lib_IntVector_Intrinsics_vec256_shift_right64(x10, (uint32_t)26U); 259 Lib_IntVector_Intrinsics_vec256 260 z110 = Lib_IntVector_Intrinsics_vec256_shift_right64(x40, (uint32_t)26U); 261 Lib_IntVector_Intrinsics_vec256 262 t5 = Lib_IntVector_Intrinsics_vec256_shift_left64(z110, (uint32_t)2U); 263 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z110, t5); 264 Lib_IntVector_Intrinsics_vec256 x110 = Lib_IntVector_Intrinsics_vec256_and(x10, mask260); 265 Lib_IntVector_Intrinsics_vec256 x410 = Lib_IntVector_Intrinsics_vec256_and(x40, mask260); 266 Lib_IntVector_Intrinsics_vec256 x20 = Lib_IntVector_Intrinsics_vec256_add64(t20, z010); 267 Lib_IntVector_Intrinsics_vec256 x010 = Lib_IntVector_Intrinsics_vec256_add64(x00, z12); 268 Lib_IntVector_Intrinsics_vec256 269 z020 = Lib_IntVector_Intrinsics_vec256_shift_right64(x20, (uint32_t)26U); 270 Lib_IntVector_Intrinsics_vec256 271 z130 = Lib_IntVector_Intrinsics_vec256_shift_right64(x010, (uint32_t)26U); 272 Lib_IntVector_Intrinsics_vec256 x210 = Lib_IntVector_Intrinsics_vec256_and(x20, mask260); 273 Lib_IntVector_Intrinsics_vec256 x020 = Lib_IntVector_Intrinsics_vec256_and(x010, mask260); 274 Lib_IntVector_Intrinsics_vec256 x310 = Lib_IntVector_Intrinsics_vec256_add64(x30, z020); 275 Lib_IntVector_Intrinsics_vec256 x120 = Lib_IntVector_Intrinsics_vec256_add64(x110, z130); 276 Lib_IntVector_Intrinsics_vec256 277 z030 = Lib_IntVector_Intrinsics_vec256_shift_right64(x310, (uint32_t)26U); 278 Lib_IntVector_Intrinsics_vec256 x320 = Lib_IntVector_Intrinsics_vec256_and(x310, mask260); 279 Lib_IntVector_Intrinsics_vec256 x420 = Lib_IntVector_Intrinsics_vec256_add64(x410, z030); 280 Lib_IntVector_Intrinsics_vec256 r20 = x020; 281 Lib_IntVector_Intrinsics_vec256 r21 = x120; 282 Lib_IntVector_Intrinsics_vec256 r22 = x210; 283 Lib_IntVector_Intrinsics_vec256 r23 = x320; 284 Lib_IntVector_Intrinsics_vec256 r24 = x420; 285 Lib_IntVector_Intrinsics_vec256 a011 = Lib_IntVector_Intrinsics_vec256_mul64(r10, r20); 286 Lib_IntVector_Intrinsics_vec256 a111 = Lib_IntVector_Intrinsics_vec256_mul64(r11, r20); 287 Lib_IntVector_Intrinsics_vec256 a211 = Lib_IntVector_Intrinsics_vec256_mul64(r12, r20); 288 Lib_IntVector_Intrinsics_vec256 a311 = Lib_IntVector_Intrinsics_vec256_mul64(r13, r20); 289 Lib_IntVector_Intrinsics_vec256 a411 = Lib_IntVector_Intrinsics_vec256_mul64(r14, r20); 290 Lib_IntVector_Intrinsics_vec256 291 a021 = 292 Lib_IntVector_Intrinsics_vec256_add64(a011, 293 Lib_IntVector_Intrinsics_vec256_mul64(r154, r21)); 294 Lib_IntVector_Intrinsics_vec256 295 a121 = 296 Lib_IntVector_Intrinsics_vec256_add64(a111, 297 Lib_IntVector_Intrinsics_vec256_mul64(r10, r21)); 298 Lib_IntVector_Intrinsics_vec256 299 a221 = 300 Lib_IntVector_Intrinsics_vec256_add64(a211, 301 Lib_IntVector_Intrinsics_vec256_mul64(r11, r21)); 302 Lib_IntVector_Intrinsics_vec256 303 a321 = 304 Lib_IntVector_Intrinsics_vec256_add64(a311, 305 Lib_IntVector_Intrinsics_vec256_mul64(r12, r21)); 306 Lib_IntVector_Intrinsics_vec256 307 a421 = 308 Lib_IntVector_Intrinsics_vec256_add64(a411, 309 Lib_IntVector_Intrinsics_vec256_mul64(r13, r21)); 310 Lib_IntVector_Intrinsics_vec256 311 a031 = 312 Lib_IntVector_Intrinsics_vec256_add64(a021, 313 Lib_IntVector_Intrinsics_vec256_mul64(r153, r22)); 314 Lib_IntVector_Intrinsics_vec256 315 a131 = 316 Lib_IntVector_Intrinsics_vec256_add64(a121, 317 Lib_IntVector_Intrinsics_vec256_mul64(r154, r22)); 318 Lib_IntVector_Intrinsics_vec256 319 a231 = 320 Lib_IntVector_Intrinsics_vec256_add64(a221, 321 Lib_IntVector_Intrinsics_vec256_mul64(r10, r22)); 322 Lib_IntVector_Intrinsics_vec256 323 a331 = 324 Lib_IntVector_Intrinsics_vec256_add64(a321, 325 Lib_IntVector_Intrinsics_vec256_mul64(r11, r22)); 326 Lib_IntVector_Intrinsics_vec256 327 a431 = 328 Lib_IntVector_Intrinsics_vec256_add64(a421, 329 Lib_IntVector_Intrinsics_vec256_mul64(r12, r22)); 330 Lib_IntVector_Intrinsics_vec256 331 a041 = 332 Lib_IntVector_Intrinsics_vec256_add64(a031, 333 Lib_IntVector_Intrinsics_vec256_mul64(r152, r23)); 334 Lib_IntVector_Intrinsics_vec256 335 a141 = 336 Lib_IntVector_Intrinsics_vec256_add64(a131, 337 Lib_IntVector_Intrinsics_vec256_mul64(r153, r23)); 338 Lib_IntVector_Intrinsics_vec256 339 a241 = 340 Lib_IntVector_Intrinsics_vec256_add64(a231, 341 Lib_IntVector_Intrinsics_vec256_mul64(r154, r23)); 342 Lib_IntVector_Intrinsics_vec256 343 a341 = 344 Lib_IntVector_Intrinsics_vec256_add64(a331, 345 Lib_IntVector_Intrinsics_vec256_mul64(r10, r23)); 346 Lib_IntVector_Intrinsics_vec256 347 a441 = 348 Lib_IntVector_Intrinsics_vec256_add64(a431, 349 Lib_IntVector_Intrinsics_vec256_mul64(r11, r23)); 350 Lib_IntVector_Intrinsics_vec256 351 a051 = 352 Lib_IntVector_Intrinsics_vec256_add64(a041, 353 Lib_IntVector_Intrinsics_vec256_mul64(r151, r24)); 354 Lib_IntVector_Intrinsics_vec256 355 a151 = 356 Lib_IntVector_Intrinsics_vec256_add64(a141, 357 Lib_IntVector_Intrinsics_vec256_mul64(r152, r24)); 358 Lib_IntVector_Intrinsics_vec256 359 a251 = 360 Lib_IntVector_Intrinsics_vec256_add64(a241, 361 Lib_IntVector_Intrinsics_vec256_mul64(r153, r24)); 362 Lib_IntVector_Intrinsics_vec256 363 a351 = 364 Lib_IntVector_Intrinsics_vec256_add64(a341, 365 Lib_IntVector_Intrinsics_vec256_mul64(r154, r24)); 366 Lib_IntVector_Intrinsics_vec256 367 a451 = 368 Lib_IntVector_Intrinsics_vec256_add64(a441, 369 Lib_IntVector_Intrinsics_vec256_mul64(r10, r24)); 370 Lib_IntVector_Intrinsics_vec256 t01 = a051; 371 Lib_IntVector_Intrinsics_vec256 t11 = a151; 372 Lib_IntVector_Intrinsics_vec256 t21 = a251; 373 Lib_IntVector_Intrinsics_vec256 t31 = a351; 374 Lib_IntVector_Intrinsics_vec256 t41 = a451; 375 Lib_IntVector_Intrinsics_vec256 376 mask261 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 377 Lib_IntVector_Intrinsics_vec256 378 z04 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); 379 Lib_IntVector_Intrinsics_vec256 380 z14 = Lib_IntVector_Intrinsics_vec256_shift_right64(t31, (uint32_t)26U); 381 Lib_IntVector_Intrinsics_vec256 x03 = Lib_IntVector_Intrinsics_vec256_and(t01, mask261); 382 Lib_IntVector_Intrinsics_vec256 x33 = Lib_IntVector_Intrinsics_vec256_and(t31, mask261); 383 Lib_IntVector_Intrinsics_vec256 x13 = Lib_IntVector_Intrinsics_vec256_add64(t11, z04); 384 Lib_IntVector_Intrinsics_vec256 x43 = Lib_IntVector_Intrinsics_vec256_add64(t41, z14); 385 Lib_IntVector_Intrinsics_vec256 386 z011 = Lib_IntVector_Intrinsics_vec256_shift_right64(x13, (uint32_t)26U); 387 Lib_IntVector_Intrinsics_vec256 388 z111 = Lib_IntVector_Intrinsics_vec256_shift_right64(x43, (uint32_t)26U); 389 Lib_IntVector_Intrinsics_vec256 390 t6 = Lib_IntVector_Intrinsics_vec256_shift_left64(z111, (uint32_t)2U); 391 Lib_IntVector_Intrinsics_vec256 z120 = Lib_IntVector_Intrinsics_vec256_add64(z111, t6); 392 Lib_IntVector_Intrinsics_vec256 x111 = Lib_IntVector_Intrinsics_vec256_and(x13, mask261); 393 Lib_IntVector_Intrinsics_vec256 x411 = Lib_IntVector_Intrinsics_vec256_and(x43, mask261); 394 Lib_IntVector_Intrinsics_vec256 x22 = Lib_IntVector_Intrinsics_vec256_add64(t21, z011); 395 Lib_IntVector_Intrinsics_vec256 x011 = Lib_IntVector_Intrinsics_vec256_add64(x03, z120); 396 Lib_IntVector_Intrinsics_vec256 397 z021 = Lib_IntVector_Intrinsics_vec256_shift_right64(x22, (uint32_t)26U); 398 Lib_IntVector_Intrinsics_vec256 399 z131 = Lib_IntVector_Intrinsics_vec256_shift_right64(x011, (uint32_t)26U); 400 Lib_IntVector_Intrinsics_vec256 x211 = Lib_IntVector_Intrinsics_vec256_and(x22, mask261); 401 Lib_IntVector_Intrinsics_vec256 x021 = Lib_IntVector_Intrinsics_vec256_and(x011, mask261); 402 Lib_IntVector_Intrinsics_vec256 x311 = Lib_IntVector_Intrinsics_vec256_add64(x33, z021); 403 Lib_IntVector_Intrinsics_vec256 x121 = Lib_IntVector_Intrinsics_vec256_add64(x111, z131); 404 Lib_IntVector_Intrinsics_vec256 405 z031 = Lib_IntVector_Intrinsics_vec256_shift_right64(x311, (uint32_t)26U); 406 Lib_IntVector_Intrinsics_vec256 x321 = Lib_IntVector_Intrinsics_vec256_and(x311, mask261); 407 Lib_IntVector_Intrinsics_vec256 x421 = Lib_IntVector_Intrinsics_vec256_add64(x411, z031); 408 Lib_IntVector_Intrinsics_vec256 r30 = x021; 409 Lib_IntVector_Intrinsics_vec256 r31 = x121; 410 Lib_IntVector_Intrinsics_vec256 r32 = x211; 411 Lib_IntVector_Intrinsics_vec256 r33 = x321; 412 Lib_IntVector_Intrinsics_vec256 r34 = x421; 413 Lib_IntVector_Intrinsics_vec256 414 v12120 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r20, r10); 415 Lib_IntVector_Intrinsics_vec256 416 v34340 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r40, r30); 417 Lib_IntVector_Intrinsics_vec256 418 r12340 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34340, v12120); 419 Lib_IntVector_Intrinsics_vec256 420 v12121 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r21, r11); 421 Lib_IntVector_Intrinsics_vec256 422 v34341 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r41, r31); 423 Lib_IntVector_Intrinsics_vec256 424 r12341 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34341, v12121); 425 Lib_IntVector_Intrinsics_vec256 426 v12122 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r22, r12); 427 Lib_IntVector_Intrinsics_vec256 428 v34342 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r42, r32); 429 Lib_IntVector_Intrinsics_vec256 430 r12342 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34342, v12122); 431 Lib_IntVector_Intrinsics_vec256 432 v12123 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r23, r13); 433 Lib_IntVector_Intrinsics_vec256 434 v34343 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r43, r33); 435 Lib_IntVector_Intrinsics_vec256 436 r12343 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34343, v12123); 437 Lib_IntVector_Intrinsics_vec256 438 v12124 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r24, r14); 439 Lib_IntVector_Intrinsics_vec256 440 v34344 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r44, r34); 441 Lib_IntVector_Intrinsics_vec256 442 r12344 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34344, v12124); 443 Lib_IntVector_Intrinsics_vec256 444 r123451 = Lib_IntVector_Intrinsics_vec256_smul64(r12341, (uint64_t)5U); 445 Lib_IntVector_Intrinsics_vec256 446 r123452 = Lib_IntVector_Intrinsics_vec256_smul64(r12342, (uint64_t)5U); 447 Lib_IntVector_Intrinsics_vec256 448 r123453 = Lib_IntVector_Intrinsics_vec256_smul64(r12343, (uint64_t)5U); 449 Lib_IntVector_Intrinsics_vec256 450 r123454 = Lib_IntVector_Intrinsics_vec256_smul64(r12344, (uint64_t)5U); 451 Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_mul64(r12340, a0); 452 Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_mul64(r12341, a0); 453 Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_mul64(r12342, a0); 454 Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_mul64(r12343, a0); 455 Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_mul64(r12344, a0); 456 Lib_IntVector_Intrinsics_vec256 457 a02 = 458 Lib_IntVector_Intrinsics_vec256_add64(a01, 459 Lib_IntVector_Intrinsics_vec256_mul64(r123454, a1)); 460 Lib_IntVector_Intrinsics_vec256 461 a12 = 462 Lib_IntVector_Intrinsics_vec256_add64(a11, 463 Lib_IntVector_Intrinsics_vec256_mul64(r12340, a1)); 464 Lib_IntVector_Intrinsics_vec256 465 a22 = 466 Lib_IntVector_Intrinsics_vec256_add64(a21, 467 Lib_IntVector_Intrinsics_vec256_mul64(r12341, a1)); 468 Lib_IntVector_Intrinsics_vec256 469 a32 = 470 Lib_IntVector_Intrinsics_vec256_add64(a31, 471 Lib_IntVector_Intrinsics_vec256_mul64(r12342, a1)); 472 Lib_IntVector_Intrinsics_vec256 473 a42 = 474 Lib_IntVector_Intrinsics_vec256_add64(a41, 475 Lib_IntVector_Intrinsics_vec256_mul64(r12343, a1)); 476 Lib_IntVector_Intrinsics_vec256 477 a03 = 478 Lib_IntVector_Intrinsics_vec256_add64(a02, 479 Lib_IntVector_Intrinsics_vec256_mul64(r123453, a2)); 480 Lib_IntVector_Intrinsics_vec256 481 a13 = 482 Lib_IntVector_Intrinsics_vec256_add64(a12, 483 Lib_IntVector_Intrinsics_vec256_mul64(r123454, a2)); 484 Lib_IntVector_Intrinsics_vec256 485 a23 = 486 Lib_IntVector_Intrinsics_vec256_add64(a22, 487 Lib_IntVector_Intrinsics_vec256_mul64(r12340, a2)); 488 Lib_IntVector_Intrinsics_vec256 489 a33 = 490 Lib_IntVector_Intrinsics_vec256_add64(a32, 491 Lib_IntVector_Intrinsics_vec256_mul64(r12341, a2)); 492 Lib_IntVector_Intrinsics_vec256 493 a43 = 494 Lib_IntVector_Intrinsics_vec256_add64(a42, 495 Lib_IntVector_Intrinsics_vec256_mul64(r12342, a2)); 496 Lib_IntVector_Intrinsics_vec256 497 a04 = 498 Lib_IntVector_Intrinsics_vec256_add64(a03, 499 Lib_IntVector_Intrinsics_vec256_mul64(r123452, a3)); 500 Lib_IntVector_Intrinsics_vec256 501 a14 = 502 Lib_IntVector_Intrinsics_vec256_add64(a13, 503 Lib_IntVector_Intrinsics_vec256_mul64(r123453, a3)); 504 Lib_IntVector_Intrinsics_vec256 505 a24 = 506 Lib_IntVector_Intrinsics_vec256_add64(a23, 507 Lib_IntVector_Intrinsics_vec256_mul64(r123454, a3)); 508 Lib_IntVector_Intrinsics_vec256 509 a34 = 510 Lib_IntVector_Intrinsics_vec256_add64(a33, 511 Lib_IntVector_Intrinsics_vec256_mul64(r12340, a3)); 512 Lib_IntVector_Intrinsics_vec256 513 a44 = 514 Lib_IntVector_Intrinsics_vec256_add64(a43, 515 Lib_IntVector_Intrinsics_vec256_mul64(r12341, a3)); 516 Lib_IntVector_Intrinsics_vec256 517 a05 = 518 Lib_IntVector_Intrinsics_vec256_add64(a04, 519 Lib_IntVector_Intrinsics_vec256_mul64(r123451, a4)); 520 Lib_IntVector_Intrinsics_vec256 521 a15 = 522 Lib_IntVector_Intrinsics_vec256_add64(a14, 523 Lib_IntVector_Intrinsics_vec256_mul64(r123452, a4)); 524 Lib_IntVector_Intrinsics_vec256 525 a25 = 526 Lib_IntVector_Intrinsics_vec256_add64(a24, 527 Lib_IntVector_Intrinsics_vec256_mul64(r123453, a4)); 528 Lib_IntVector_Intrinsics_vec256 529 a35 = 530 Lib_IntVector_Intrinsics_vec256_add64(a34, 531 Lib_IntVector_Intrinsics_vec256_mul64(r123454, a4)); 532 Lib_IntVector_Intrinsics_vec256 533 a45 = 534 Lib_IntVector_Intrinsics_vec256_add64(a44, 535 Lib_IntVector_Intrinsics_vec256_mul64(r12340, a4)); 536 Lib_IntVector_Intrinsics_vec256 t0 = a05; 537 Lib_IntVector_Intrinsics_vec256 t1 = a15; 538 Lib_IntVector_Intrinsics_vec256 t2 = a25; 539 Lib_IntVector_Intrinsics_vec256 t3 = a35; 540 Lib_IntVector_Intrinsics_vec256 t4 = a45; 541 Lib_IntVector_Intrinsics_vec256 542 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 543 Lib_IntVector_Intrinsics_vec256 544 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); 545 Lib_IntVector_Intrinsics_vec256 546 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 547 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); 548 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 549 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); 550 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 551 Lib_IntVector_Intrinsics_vec256 552 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 553 Lib_IntVector_Intrinsics_vec256 554 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 555 Lib_IntVector_Intrinsics_vec256 556 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 557 Lib_IntVector_Intrinsics_vec256 z121 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 558 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 559 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 560 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 561 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z121); 562 Lib_IntVector_Intrinsics_vec256 563 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 564 Lib_IntVector_Intrinsics_vec256 565 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 566 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 567 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 568 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 569 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 570 Lib_IntVector_Intrinsics_vec256 571 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 572 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 573 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 574 Lib_IntVector_Intrinsics_vec256 o0 = x02; 575 Lib_IntVector_Intrinsics_vec256 o10 = x12; 576 Lib_IntVector_Intrinsics_vec256 o20 = x21; 577 Lib_IntVector_Intrinsics_vec256 o30 = x32; 578 Lib_IntVector_Intrinsics_vec256 o40 = x42; 579 Lib_IntVector_Intrinsics_vec256 580 v00 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o0, o0); 581 Lib_IntVector_Intrinsics_vec256 v10 = Lib_IntVector_Intrinsics_vec256_add64(o0, v00); 582 Lib_IntVector_Intrinsics_vec256 583 v10h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v10, v10); 584 Lib_IntVector_Intrinsics_vec256 v20 = Lib_IntVector_Intrinsics_vec256_add64(v10, v10h); 585 Lib_IntVector_Intrinsics_vec256 586 v01 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o10, o10); 587 Lib_IntVector_Intrinsics_vec256 v11 = Lib_IntVector_Intrinsics_vec256_add64(o10, v01); 588 Lib_IntVector_Intrinsics_vec256 589 v11h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v11, v11); 590 Lib_IntVector_Intrinsics_vec256 v21 = Lib_IntVector_Intrinsics_vec256_add64(v11, v11h); 591 Lib_IntVector_Intrinsics_vec256 592 v02 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o20, o20); 593 Lib_IntVector_Intrinsics_vec256 v12 = Lib_IntVector_Intrinsics_vec256_add64(o20, v02); 594 Lib_IntVector_Intrinsics_vec256 595 v12h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v12, v12); 596 Lib_IntVector_Intrinsics_vec256 v22 = Lib_IntVector_Intrinsics_vec256_add64(v12, v12h); 597 Lib_IntVector_Intrinsics_vec256 598 v03 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o30, o30); 599 Lib_IntVector_Intrinsics_vec256 v13 = Lib_IntVector_Intrinsics_vec256_add64(o30, v03); 600 Lib_IntVector_Intrinsics_vec256 601 v13h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v13, v13); 602 Lib_IntVector_Intrinsics_vec256 v23 = Lib_IntVector_Intrinsics_vec256_add64(v13, v13h); 603 Lib_IntVector_Intrinsics_vec256 604 v04 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o40, o40); 605 Lib_IntVector_Intrinsics_vec256 v14 = Lib_IntVector_Intrinsics_vec256_add64(o40, v04); 606 Lib_IntVector_Intrinsics_vec256 607 v14h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v14, v14); 608 Lib_IntVector_Intrinsics_vec256 v24 = Lib_IntVector_Intrinsics_vec256_add64(v14, v14h); 609 Lib_IntVector_Intrinsics_vec256 610 l = Lib_IntVector_Intrinsics_vec256_add64(v20, Lib_IntVector_Intrinsics_vec256_zero); 611 Lib_IntVector_Intrinsics_vec256 612 tmp0 = 613 Lib_IntVector_Intrinsics_vec256_and(l, 614 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 615 Lib_IntVector_Intrinsics_vec256 616 c0 = Lib_IntVector_Intrinsics_vec256_shift_right64(l, (uint32_t)26U); 617 Lib_IntVector_Intrinsics_vec256 l0 = Lib_IntVector_Intrinsics_vec256_add64(v21, c0); 618 Lib_IntVector_Intrinsics_vec256 619 tmp1 = 620 Lib_IntVector_Intrinsics_vec256_and(l0, 621 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 622 Lib_IntVector_Intrinsics_vec256 623 c1 = Lib_IntVector_Intrinsics_vec256_shift_right64(l0, (uint32_t)26U); 624 Lib_IntVector_Intrinsics_vec256 l1 = Lib_IntVector_Intrinsics_vec256_add64(v22, c1); 625 Lib_IntVector_Intrinsics_vec256 626 tmp2 = 627 Lib_IntVector_Intrinsics_vec256_and(l1, 628 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 629 Lib_IntVector_Intrinsics_vec256 630 c2 = Lib_IntVector_Intrinsics_vec256_shift_right64(l1, (uint32_t)26U); 631 Lib_IntVector_Intrinsics_vec256 l2 = Lib_IntVector_Intrinsics_vec256_add64(v23, c2); 632 Lib_IntVector_Intrinsics_vec256 633 tmp3 = 634 Lib_IntVector_Intrinsics_vec256_and(l2, 635 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 636 Lib_IntVector_Intrinsics_vec256 637 c3 = Lib_IntVector_Intrinsics_vec256_shift_right64(l2, (uint32_t)26U); 638 Lib_IntVector_Intrinsics_vec256 l3 = Lib_IntVector_Intrinsics_vec256_add64(v24, c3); 639 Lib_IntVector_Intrinsics_vec256 640 tmp4 = 641 Lib_IntVector_Intrinsics_vec256_and(l3, 642 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 643 Lib_IntVector_Intrinsics_vec256 644 c4 = Lib_IntVector_Intrinsics_vec256_shift_right64(l3, (uint32_t)26U); 645 Lib_IntVector_Intrinsics_vec256 646 o00 = 647 Lib_IntVector_Intrinsics_vec256_add64(tmp0, 648 Lib_IntVector_Intrinsics_vec256_smul64(c4, (uint64_t)5U)); 649 Lib_IntVector_Intrinsics_vec256 o1 = tmp1; 650 Lib_IntVector_Intrinsics_vec256 o2 = tmp2; 651 Lib_IntVector_Intrinsics_vec256 o3 = tmp3; 652 Lib_IntVector_Intrinsics_vec256 o4 = tmp4; 653 out[0U] = o00; 654 out[1U] = o1; 655 out[2U] = o2; 656 out[3U] = o3; 657 out[4U] = o4; 658 } 659 660 void 661 Hacl_Poly1305_256_poly1305_init(Lib_IntVector_Intrinsics_vec256 *ctx, uint8_t *key) 662 { 663 Lib_IntVector_Intrinsics_vec256 *acc = ctx; 664 Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; 665 uint8_t *kr = key; 666 acc[0U] = Lib_IntVector_Intrinsics_vec256_zero; 667 acc[1U] = Lib_IntVector_Intrinsics_vec256_zero; 668 acc[2U] = Lib_IntVector_Intrinsics_vec256_zero; 669 acc[3U] = Lib_IntVector_Intrinsics_vec256_zero; 670 acc[4U] = Lib_IntVector_Intrinsics_vec256_zero; 671 uint64_t u0 = load64_le(kr); 672 uint64_t lo = u0; 673 uint64_t u = load64_le(kr + (uint32_t)8U); 674 uint64_t hi = u; 675 uint64_t mask0 = (uint64_t)0x0ffffffc0fffffffU; 676 uint64_t mask1 = (uint64_t)0x0ffffffc0ffffffcU; 677 uint64_t lo1 = lo & mask0; 678 uint64_t hi1 = hi & mask1; 679 Lib_IntVector_Intrinsics_vec256 *r = pre; 680 Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; 681 Lib_IntVector_Intrinsics_vec256 *rn = pre + (uint32_t)10U; 682 Lib_IntVector_Intrinsics_vec256 *rn_5 = pre + (uint32_t)15U; 683 Lib_IntVector_Intrinsics_vec256 r_vec0 = Lib_IntVector_Intrinsics_vec256_load64(lo1); 684 Lib_IntVector_Intrinsics_vec256 r_vec1 = Lib_IntVector_Intrinsics_vec256_load64(hi1); 685 Lib_IntVector_Intrinsics_vec256 686 f00 = 687 Lib_IntVector_Intrinsics_vec256_and(r_vec0, 688 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 689 Lib_IntVector_Intrinsics_vec256 690 f15 = 691 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec0, 692 (uint32_t)26U), 693 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 694 Lib_IntVector_Intrinsics_vec256 695 f20 = 696 Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec0, 697 (uint32_t)52U), 698 Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(r_vec1, 699 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), 700 (uint32_t)12U)); 701 Lib_IntVector_Intrinsics_vec256 702 f30 = 703 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec1, 704 (uint32_t)14U), 705 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 706 Lib_IntVector_Intrinsics_vec256 707 f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec1, (uint32_t)40U); 708 Lib_IntVector_Intrinsics_vec256 f0 = f00; 709 Lib_IntVector_Intrinsics_vec256 f1 = f15; 710 Lib_IntVector_Intrinsics_vec256 f2 = f20; 711 Lib_IntVector_Intrinsics_vec256 f3 = f30; 712 Lib_IntVector_Intrinsics_vec256 f4 = f40; 713 r[0U] = f0; 714 r[1U] = f1; 715 r[2U] = f2; 716 r[3U] = f3; 717 r[4U] = f4; 718 Lib_IntVector_Intrinsics_vec256 f200 = r[0U]; 719 Lib_IntVector_Intrinsics_vec256 f210 = r[1U]; 720 Lib_IntVector_Intrinsics_vec256 f220 = r[2U]; 721 Lib_IntVector_Intrinsics_vec256 f230 = r[3U]; 722 Lib_IntVector_Intrinsics_vec256 f240 = r[4U]; 723 r5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f200, (uint64_t)5U); 724 r5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f210, (uint64_t)5U); 725 r5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f220, (uint64_t)5U); 726 r5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f230, (uint64_t)5U); 727 r5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f240, (uint64_t)5U); 728 Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; 729 Lib_IntVector_Intrinsics_vec256 r10 = r[1U]; 730 Lib_IntVector_Intrinsics_vec256 r20 = r[2U]; 731 Lib_IntVector_Intrinsics_vec256 r30 = r[3U]; 732 Lib_IntVector_Intrinsics_vec256 r40 = r[4U]; 733 Lib_IntVector_Intrinsics_vec256 r510 = r5[1U]; 734 Lib_IntVector_Intrinsics_vec256 r520 = r5[2U]; 735 Lib_IntVector_Intrinsics_vec256 r530 = r5[3U]; 736 Lib_IntVector_Intrinsics_vec256 r540 = r5[4U]; 737 Lib_IntVector_Intrinsics_vec256 f100 = r[0U]; 738 Lib_IntVector_Intrinsics_vec256 f110 = r[1U]; 739 Lib_IntVector_Intrinsics_vec256 f120 = r[2U]; 740 Lib_IntVector_Intrinsics_vec256 f130 = r[3U]; 741 Lib_IntVector_Intrinsics_vec256 f140 = r[4U]; 742 Lib_IntVector_Intrinsics_vec256 a00 = Lib_IntVector_Intrinsics_vec256_mul64(r0, f100); 743 Lib_IntVector_Intrinsics_vec256 a10 = Lib_IntVector_Intrinsics_vec256_mul64(r10, f100); 744 Lib_IntVector_Intrinsics_vec256 a20 = Lib_IntVector_Intrinsics_vec256_mul64(r20, f100); 745 Lib_IntVector_Intrinsics_vec256 a30 = Lib_IntVector_Intrinsics_vec256_mul64(r30, f100); 746 Lib_IntVector_Intrinsics_vec256 a40 = Lib_IntVector_Intrinsics_vec256_mul64(r40, f100); 747 Lib_IntVector_Intrinsics_vec256 748 a010 = 749 Lib_IntVector_Intrinsics_vec256_add64(a00, 750 Lib_IntVector_Intrinsics_vec256_mul64(r540, f110)); 751 Lib_IntVector_Intrinsics_vec256 752 a110 = 753 Lib_IntVector_Intrinsics_vec256_add64(a10, 754 Lib_IntVector_Intrinsics_vec256_mul64(r0, f110)); 755 Lib_IntVector_Intrinsics_vec256 756 a210 = 757 Lib_IntVector_Intrinsics_vec256_add64(a20, 758 Lib_IntVector_Intrinsics_vec256_mul64(r10, f110)); 759 Lib_IntVector_Intrinsics_vec256 760 a310 = 761 Lib_IntVector_Intrinsics_vec256_add64(a30, 762 Lib_IntVector_Intrinsics_vec256_mul64(r20, f110)); 763 Lib_IntVector_Intrinsics_vec256 764 a410 = 765 Lib_IntVector_Intrinsics_vec256_add64(a40, 766 Lib_IntVector_Intrinsics_vec256_mul64(r30, f110)); 767 Lib_IntVector_Intrinsics_vec256 768 a020 = 769 Lib_IntVector_Intrinsics_vec256_add64(a010, 770 Lib_IntVector_Intrinsics_vec256_mul64(r530, f120)); 771 Lib_IntVector_Intrinsics_vec256 772 a120 = 773 Lib_IntVector_Intrinsics_vec256_add64(a110, 774 Lib_IntVector_Intrinsics_vec256_mul64(r540, f120)); 775 Lib_IntVector_Intrinsics_vec256 776 a220 = 777 Lib_IntVector_Intrinsics_vec256_add64(a210, 778 Lib_IntVector_Intrinsics_vec256_mul64(r0, f120)); 779 Lib_IntVector_Intrinsics_vec256 780 a320 = 781 Lib_IntVector_Intrinsics_vec256_add64(a310, 782 Lib_IntVector_Intrinsics_vec256_mul64(r10, f120)); 783 Lib_IntVector_Intrinsics_vec256 784 a420 = 785 Lib_IntVector_Intrinsics_vec256_add64(a410, 786 Lib_IntVector_Intrinsics_vec256_mul64(r20, f120)); 787 Lib_IntVector_Intrinsics_vec256 788 a030 = 789 Lib_IntVector_Intrinsics_vec256_add64(a020, 790 Lib_IntVector_Intrinsics_vec256_mul64(r520, f130)); 791 Lib_IntVector_Intrinsics_vec256 792 a130 = 793 Lib_IntVector_Intrinsics_vec256_add64(a120, 794 Lib_IntVector_Intrinsics_vec256_mul64(r530, f130)); 795 Lib_IntVector_Intrinsics_vec256 796 a230 = 797 Lib_IntVector_Intrinsics_vec256_add64(a220, 798 Lib_IntVector_Intrinsics_vec256_mul64(r540, f130)); 799 Lib_IntVector_Intrinsics_vec256 800 a330 = 801 Lib_IntVector_Intrinsics_vec256_add64(a320, 802 Lib_IntVector_Intrinsics_vec256_mul64(r0, f130)); 803 Lib_IntVector_Intrinsics_vec256 804 a430 = 805 Lib_IntVector_Intrinsics_vec256_add64(a420, 806 Lib_IntVector_Intrinsics_vec256_mul64(r10, f130)); 807 Lib_IntVector_Intrinsics_vec256 808 a040 = 809 Lib_IntVector_Intrinsics_vec256_add64(a030, 810 Lib_IntVector_Intrinsics_vec256_mul64(r510, f140)); 811 Lib_IntVector_Intrinsics_vec256 812 a140 = 813 Lib_IntVector_Intrinsics_vec256_add64(a130, 814 Lib_IntVector_Intrinsics_vec256_mul64(r520, f140)); 815 Lib_IntVector_Intrinsics_vec256 816 a240 = 817 Lib_IntVector_Intrinsics_vec256_add64(a230, 818 Lib_IntVector_Intrinsics_vec256_mul64(r530, f140)); 819 Lib_IntVector_Intrinsics_vec256 820 a340 = 821 Lib_IntVector_Intrinsics_vec256_add64(a330, 822 Lib_IntVector_Intrinsics_vec256_mul64(r540, f140)); 823 Lib_IntVector_Intrinsics_vec256 824 a440 = 825 Lib_IntVector_Intrinsics_vec256_add64(a430, 826 Lib_IntVector_Intrinsics_vec256_mul64(r0, f140)); 827 Lib_IntVector_Intrinsics_vec256 t00 = a040; 828 Lib_IntVector_Intrinsics_vec256 t10 = a140; 829 Lib_IntVector_Intrinsics_vec256 t20 = a240; 830 Lib_IntVector_Intrinsics_vec256 t30 = a340; 831 Lib_IntVector_Intrinsics_vec256 t40 = a440; 832 Lib_IntVector_Intrinsics_vec256 833 mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 834 Lib_IntVector_Intrinsics_vec256 835 z00 = Lib_IntVector_Intrinsics_vec256_shift_right64(t00, (uint32_t)26U); 836 Lib_IntVector_Intrinsics_vec256 837 z10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)26U); 838 Lib_IntVector_Intrinsics_vec256 x00 = Lib_IntVector_Intrinsics_vec256_and(t00, mask260); 839 Lib_IntVector_Intrinsics_vec256 x30 = Lib_IntVector_Intrinsics_vec256_and(t30, mask260); 840 Lib_IntVector_Intrinsics_vec256 x10 = Lib_IntVector_Intrinsics_vec256_add64(t10, z00); 841 Lib_IntVector_Intrinsics_vec256 x40 = Lib_IntVector_Intrinsics_vec256_add64(t40, z10); 842 Lib_IntVector_Intrinsics_vec256 843 z010 = Lib_IntVector_Intrinsics_vec256_shift_right64(x10, (uint32_t)26U); 844 Lib_IntVector_Intrinsics_vec256 845 z110 = Lib_IntVector_Intrinsics_vec256_shift_right64(x40, (uint32_t)26U); 846 Lib_IntVector_Intrinsics_vec256 847 t5 = Lib_IntVector_Intrinsics_vec256_shift_left64(z110, (uint32_t)2U); 848 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z110, t5); 849 Lib_IntVector_Intrinsics_vec256 x110 = Lib_IntVector_Intrinsics_vec256_and(x10, mask260); 850 Lib_IntVector_Intrinsics_vec256 x410 = Lib_IntVector_Intrinsics_vec256_and(x40, mask260); 851 Lib_IntVector_Intrinsics_vec256 x20 = Lib_IntVector_Intrinsics_vec256_add64(t20, z010); 852 Lib_IntVector_Intrinsics_vec256 x010 = Lib_IntVector_Intrinsics_vec256_add64(x00, z12); 853 Lib_IntVector_Intrinsics_vec256 854 z020 = Lib_IntVector_Intrinsics_vec256_shift_right64(x20, (uint32_t)26U); 855 Lib_IntVector_Intrinsics_vec256 856 z130 = Lib_IntVector_Intrinsics_vec256_shift_right64(x010, (uint32_t)26U); 857 Lib_IntVector_Intrinsics_vec256 x210 = Lib_IntVector_Intrinsics_vec256_and(x20, mask260); 858 Lib_IntVector_Intrinsics_vec256 x020 = Lib_IntVector_Intrinsics_vec256_and(x010, mask260); 859 Lib_IntVector_Intrinsics_vec256 x310 = Lib_IntVector_Intrinsics_vec256_add64(x30, z020); 860 Lib_IntVector_Intrinsics_vec256 x120 = Lib_IntVector_Intrinsics_vec256_add64(x110, z130); 861 Lib_IntVector_Intrinsics_vec256 862 z030 = Lib_IntVector_Intrinsics_vec256_shift_right64(x310, (uint32_t)26U); 863 Lib_IntVector_Intrinsics_vec256 x320 = Lib_IntVector_Intrinsics_vec256_and(x310, mask260); 864 Lib_IntVector_Intrinsics_vec256 x420 = Lib_IntVector_Intrinsics_vec256_add64(x410, z030); 865 Lib_IntVector_Intrinsics_vec256 o00 = x020; 866 Lib_IntVector_Intrinsics_vec256 o10 = x120; 867 Lib_IntVector_Intrinsics_vec256 o20 = x210; 868 Lib_IntVector_Intrinsics_vec256 o30 = x320; 869 Lib_IntVector_Intrinsics_vec256 o40 = x420; 870 rn[0U] = o00; 871 rn[1U] = o10; 872 rn[2U] = o20; 873 rn[3U] = o30; 874 rn[4U] = o40; 875 Lib_IntVector_Intrinsics_vec256 f201 = rn[0U]; 876 Lib_IntVector_Intrinsics_vec256 f211 = rn[1U]; 877 Lib_IntVector_Intrinsics_vec256 f221 = rn[2U]; 878 Lib_IntVector_Intrinsics_vec256 f231 = rn[3U]; 879 Lib_IntVector_Intrinsics_vec256 f241 = rn[4U]; 880 rn_5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f201, (uint64_t)5U); 881 rn_5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f211, (uint64_t)5U); 882 rn_5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f221, (uint64_t)5U); 883 rn_5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f231, (uint64_t)5U); 884 rn_5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f241, (uint64_t)5U); 885 Lib_IntVector_Intrinsics_vec256 r00 = rn[0U]; 886 Lib_IntVector_Intrinsics_vec256 r1 = rn[1U]; 887 Lib_IntVector_Intrinsics_vec256 r2 = rn[2U]; 888 Lib_IntVector_Intrinsics_vec256 r3 = rn[3U]; 889 Lib_IntVector_Intrinsics_vec256 r4 = rn[4U]; 890 Lib_IntVector_Intrinsics_vec256 r51 = rn_5[1U]; 891 Lib_IntVector_Intrinsics_vec256 r52 = rn_5[2U]; 892 Lib_IntVector_Intrinsics_vec256 r53 = rn_5[3U]; 893 Lib_IntVector_Intrinsics_vec256 r54 = rn_5[4U]; 894 Lib_IntVector_Intrinsics_vec256 f10 = rn[0U]; 895 Lib_IntVector_Intrinsics_vec256 f11 = rn[1U]; 896 Lib_IntVector_Intrinsics_vec256 f12 = rn[2U]; 897 Lib_IntVector_Intrinsics_vec256 f13 = rn[3U]; 898 Lib_IntVector_Intrinsics_vec256 f14 = rn[4U]; 899 Lib_IntVector_Intrinsics_vec256 a0 = Lib_IntVector_Intrinsics_vec256_mul64(r00, f10); 900 Lib_IntVector_Intrinsics_vec256 a1 = Lib_IntVector_Intrinsics_vec256_mul64(r1, f10); 901 Lib_IntVector_Intrinsics_vec256 a2 = Lib_IntVector_Intrinsics_vec256_mul64(r2, f10); 902 Lib_IntVector_Intrinsics_vec256 a3 = Lib_IntVector_Intrinsics_vec256_mul64(r3, f10); 903 Lib_IntVector_Intrinsics_vec256 a4 = Lib_IntVector_Intrinsics_vec256_mul64(r4, f10); 904 Lib_IntVector_Intrinsics_vec256 905 a01 = 906 Lib_IntVector_Intrinsics_vec256_add64(a0, 907 Lib_IntVector_Intrinsics_vec256_mul64(r54, f11)); 908 Lib_IntVector_Intrinsics_vec256 909 a11 = 910 Lib_IntVector_Intrinsics_vec256_add64(a1, 911 Lib_IntVector_Intrinsics_vec256_mul64(r00, f11)); 912 Lib_IntVector_Intrinsics_vec256 913 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, Lib_IntVector_Intrinsics_vec256_mul64(r1, f11)); 914 Lib_IntVector_Intrinsics_vec256 915 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, Lib_IntVector_Intrinsics_vec256_mul64(r2, f11)); 916 Lib_IntVector_Intrinsics_vec256 917 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, Lib_IntVector_Intrinsics_vec256_mul64(r3, f11)); 918 Lib_IntVector_Intrinsics_vec256 919 a02 = 920 Lib_IntVector_Intrinsics_vec256_add64(a01, 921 Lib_IntVector_Intrinsics_vec256_mul64(r53, f12)); 922 Lib_IntVector_Intrinsics_vec256 923 a12 = 924 Lib_IntVector_Intrinsics_vec256_add64(a11, 925 Lib_IntVector_Intrinsics_vec256_mul64(r54, f12)); 926 Lib_IntVector_Intrinsics_vec256 927 a22 = 928 Lib_IntVector_Intrinsics_vec256_add64(a21, 929 Lib_IntVector_Intrinsics_vec256_mul64(r00, f12)); 930 Lib_IntVector_Intrinsics_vec256 931 a32 = 932 Lib_IntVector_Intrinsics_vec256_add64(a31, 933 Lib_IntVector_Intrinsics_vec256_mul64(r1, f12)); 934 Lib_IntVector_Intrinsics_vec256 935 a42 = 936 Lib_IntVector_Intrinsics_vec256_add64(a41, 937 Lib_IntVector_Intrinsics_vec256_mul64(r2, f12)); 938 Lib_IntVector_Intrinsics_vec256 939 a03 = 940 Lib_IntVector_Intrinsics_vec256_add64(a02, 941 Lib_IntVector_Intrinsics_vec256_mul64(r52, f13)); 942 Lib_IntVector_Intrinsics_vec256 943 a13 = 944 Lib_IntVector_Intrinsics_vec256_add64(a12, 945 Lib_IntVector_Intrinsics_vec256_mul64(r53, f13)); 946 Lib_IntVector_Intrinsics_vec256 947 a23 = 948 Lib_IntVector_Intrinsics_vec256_add64(a22, 949 Lib_IntVector_Intrinsics_vec256_mul64(r54, f13)); 950 Lib_IntVector_Intrinsics_vec256 951 a33 = 952 Lib_IntVector_Intrinsics_vec256_add64(a32, 953 Lib_IntVector_Intrinsics_vec256_mul64(r00, f13)); 954 Lib_IntVector_Intrinsics_vec256 955 a43 = 956 Lib_IntVector_Intrinsics_vec256_add64(a42, 957 Lib_IntVector_Intrinsics_vec256_mul64(r1, f13)); 958 Lib_IntVector_Intrinsics_vec256 959 a04 = 960 Lib_IntVector_Intrinsics_vec256_add64(a03, 961 Lib_IntVector_Intrinsics_vec256_mul64(r51, f14)); 962 Lib_IntVector_Intrinsics_vec256 963 a14 = 964 Lib_IntVector_Intrinsics_vec256_add64(a13, 965 Lib_IntVector_Intrinsics_vec256_mul64(r52, f14)); 966 Lib_IntVector_Intrinsics_vec256 967 a24 = 968 Lib_IntVector_Intrinsics_vec256_add64(a23, 969 Lib_IntVector_Intrinsics_vec256_mul64(r53, f14)); 970 Lib_IntVector_Intrinsics_vec256 971 a34 = 972 Lib_IntVector_Intrinsics_vec256_add64(a33, 973 Lib_IntVector_Intrinsics_vec256_mul64(r54, f14)); 974 Lib_IntVector_Intrinsics_vec256 975 a44 = 976 Lib_IntVector_Intrinsics_vec256_add64(a43, 977 Lib_IntVector_Intrinsics_vec256_mul64(r00, f14)); 978 Lib_IntVector_Intrinsics_vec256 t0 = a04; 979 Lib_IntVector_Intrinsics_vec256 t1 = a14; 980 Lib_IntVector_Intrinsics_vec256 t2 = a24; 981 Lib_IntVector_Intrinsics_vec256 t3 = a34; 982 Lib_IntVector_Intrinsics_vec256 t4 = a44; 983 Lib_IntVector_Intrinsics_vec256 984 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 985 Lib_IntVector_Intrinsics_vec256 986 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); 987 Lib_IntVector_Intrinsics_vec256 988 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 989 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); 990 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 991 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); 992 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 993 Lib_IntVector_Intrinsics_vec256 994 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 995 Lib_IntVector_Intrinsics_vec256 996 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 997 Lib_IntVector_Intrinsics_vec256 998 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 999 Lib_IntVector_Intrinsics_vec256 z120 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 1000 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 1001 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 1002 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 1003 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z120); 1004 Lib_IntVector_Intrinsics_vec256 1005 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 1006 Lib_IntVector_Intrinsics_vec256 1007 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 1008 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 1009 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 1010 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 1011 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 1012 Lib_IntVector_Intrinsics_vec256 1013 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 1014 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 1015 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 1016 Lib_IntVector_Intrinsics_vec256 o0 = x02; 1017 Lib_IntVector_Intrinsics_vec256 o1 = x12; 1018 Lib_IntVector_Intrinsics_vec256 o2 = x21; 1019 Lib_IntVector_Intrinsics_vec256 o3 = x32; 1020 Lib_IntVector_Intrinsics_vec256 o4 = x42; 1021 rn[0U] = o0; 1022 rn[1U] = o1; 1023 rn[2U] = o2; 1024 rn[3U] = o3; 1025 rn[4U] = o4; 1026 Lib_IntVector_Intrinsics_vec256 f202 = rn[0U]; 1027 Lib_IntVector_Intrinsics_vec256 f21 = rn[1U]; 1028 Lib_IntVector_Intrinsics_vec256 f22 = rn[2U]; 1029 Lib_IntVector_Intrinsics_vec256 f23 = rn[3U]; 1030 Lib_IntVector_Intrinsics_vec256 f24 = rn[4U]; 1031 rn_5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f202, (uint64_t)5U); 1032 rn_5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f21, (uint64_t)5U); 1033 rn_5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f22, (uint64_t)5U); 1034 rn_5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f23, (uint64_t)5U); 1035 rn_5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f24, (uint64_t)5U); 1036 } 1037 1038 void 1039 Hacl_Poly1305_256_poly1305_update1(Lib_IntVector_Intrinsics_vec256 *ctx, uint8_t *text) 1040 { 1041 Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; 1042 Lib_IntVector_Intrinsics_vec256 *acc = ctx; 1043 KRML_PRE_ALIGN(32) 1044 Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; 1045 uint64_t u0 = load64_le(text); 1046 uint64_t lo = u0; 1047 uint64_t u = load64_le(text + (uint32_t)8U); 1048 uint64_t hi = u; 1049 Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); 1050 Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); 1051 Lib_IntVector_Intrinsics_vec256 1052 f010 = 1053 Lib_IntVector_Intrinsics_vec256_and(f0, 1054 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1055 Lib_IntVector_Intrinsics_vec256 1056 f110 = 1057 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1058 (uint32_t)26U), 1059 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1060 Lib_IntVector_Intrinsics_vec256 1061 f20 = 1062 Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1063 (uint32_t)52U), 1064 Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, 1065 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), 1066 (uint32_t)12U)); 1067 Lib_IntVector_Intrinsics_vec256 1068 f30 = 1069 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, 1070 (uint32_t)14U), 1071 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1072 Lib_IntVector_Intrinsics_vec256 1073 f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); 1074 Lib_IntVector_Intrinsics_vec256 f01 = f010; 1075 Lib_IntVector_Intrinsics_vec256 f111 = f110; 1076 Lib_IntVector_Intrinsics_vec256 f2 = f20; 1077 Lib_IntVector_Intrinsics_vec256 f3 = f30; 1078 Lib_IntVector_Intrinsics_vec256 f41 = f40; 1079 e[0U] = f01; 1080 e[1U] = f111; 1081 e[2U] = f2; 1082 e[3U] = f3; 1083 e[4U] = f41; 1084 uint64_t b = (uint64_t)0x1000000U; 1085 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); 1086 Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; 1087 e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); 1088 Lib_IntVector_Intrinsics_vec256 *r = pre; 1089 Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; 1090 Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; 1091 Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; 1092 Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; 1093 Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; 1094 Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; 1095 Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; 1096 Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; 1097 Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; 1098 Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; 1099 Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; 1100 Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; 1101 Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; 1102 Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; 1103 Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; 1104 Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; 1105 Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; 1106 Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; 1107 Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; 1108 Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; 1109 Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); 1110 Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); 1111 Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); 1112 Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); 1113 Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); 1114 Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); 1115 Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); 1116 Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); 1117 Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); 1118 Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); 1119 Lib_IntVector_Intrinsics_vec256 1120 a03 = 1121 Lib_IntVector_Intrinsics_vec256_add64(a02, 1122 Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); 1123 Lib_IntVector_Intrinsics_vec256 1124 a13 = 1125 Lib_IntVector_Intrinsics_vec256_add64(a12, 1126 Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); 1127 Lib_IntVector_Intrinsics_vec256 1128 a23 = 1129 Lib_IntVector_Intrinsics_vec256_add64(a22, 1130 Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); 1131 Lib_IntVector_Intrinsics_vec256 1132 a33 = 1133 Lib_IntVector_Intrinsics_vec256_add64(a32, 1134 Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); 1135 Lib_IntVector_Intrinsics_vec256 1136 a43 = 1137 Lib_IntVector_Intrinsics_vec256_add64(a42, 1138 Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); 1139 Lib_IntVector_Intrinsics_vec256 1140 a04 = 1141 Lib_IntVector_Intrinsics_vec256_add64(a03, 1142 Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); 1143 Lib_IntVector_Intrinsics_vec256 1144 a14 = 1145 Lib_IntVector_Intrinsics_vec256_add64(a13, 1146 Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); 1147 Lib_IntVector_Intrinsics_vec256 1148 a24 = 1149 Lib_IntVector_Intrinsics_vec256_add64(a23, 1150 Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); 1151 Lib_IntVector_Intrinsics_vec256 1152 a34 = 1153 Lib_IntVector_Intrinsics_vec256_add64(a33, 1154 Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); 1155 Lib_IntVector_Intrinsics_vec256 1156 a44 = 1157 Lib_IntVector_Intrinsics_vec256_add64(a43, 1158 Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); 1159 Lib_IntVector_Intrinsics_vec256 1160 a05 = 1161 Lib_IntVector_Intrinsics_vec256_add64(a04, 1162 Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); 1163 Lib_IntVector_Intrinsics_vec256 1164 a15 = 1165 Lib_IntVector_Intrinsics_vec256_add64(a14, 1166 Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); 1167 Lib_IntVector_Intrinsics_vec256 1168 a25 = 1169 Lib_IntVector_Intrinsics_vec256_add64(a24, 1170 Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); 1171 Lib_IntVector_Intrinsics_vec256 1172 a35 = 1173 Lib_IntVector_Intrinsics_vec256_add64(a34, 1174 Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); 1175 Lib_IntVector_Intrinsics_vec256 1176 a45 = 1177 Lib_IntVector_Intrinsics_vec256_add64(a44, 1178 Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); 1179 Lib_IntVector_Intrinsics_vec256 1180 a06 = 1181 Lib_IntVector_Intrinsics_vec256_add64(a05, 1182 Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); 1183 Lib_IntVector_Intrinsics_vec256 1184 a16 = 1185 Lib_IntVector_Intrinsics_vec256_add64(a15, 1186 Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); 1187 Lib_IntVector_Intrinsics_vec256 1188 a26 = 1189 Lib_IntVector_Intrinsics_vec256_add64(a25, 1190 Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); 1191 Lib_IntVector_Intrinsics_vec256 1192 a36 = 1193 Lib_IntVector_Intrinsics_vec256_add64(a35, 1194 Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); 1195 Lib_IntVector_Intrinsics_vec256 1196 a46 = 1197 Lib_IntVector_Intrinsics_vec256_add64(a45, 1198 Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); 1199 Lib_IntVector_Intrinsics_vec256 t0 = a06; 1200 Lib_IntVector_Intrinsics_vec256 t1 = a16; 1201 Lib_IntVector_Intrinsics_vec256 t2 = a26; 1202 Lib_IntVector_Intrinsics_vec256 t3 = a36; 1203 Lib_IntVector_Intrinsics_vec256 t4 = a46; 1204 Lib_IntVector_Intrinsics_vec256 1205 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 1206 Lib_IntVector_Intrinsics_vec256 1207 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); 1208 Lib_IntVector_Intrinsics_vec256 1209 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 1210 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); 1211 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 1212 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); 1213 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 1214 Lib_IntVector_Intrinsics_vec256 1215 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 1216 Lib_IntVector_Intrinsics_vec256 1217 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 1218 Lib_IntVector_Intrinsics_vec256 1219 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 1220 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 1221 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 1222 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 1223 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 1224 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); 1225 Lib_IntVector_Intrinsics_vec256 1226 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 1227 Lib_IntVector_Intrinsics_vec256 1228 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 1229 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 1230 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 1231 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 1232 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 1233 Lib_IntVector_Intrinsics_vec256 1234 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 1235 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 1236 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 1237 Lib_IntVector_Intrinsics_vec256 o0 = x02; 1238 Lib_IntVector_Intrinsics_vec256 o1 = x12; 1239 Lib_IntVector_Intrinsics_vec256 o2 = x21; 1240 Lib_IntVector_Intrinsics_vec256 o3 = x32; 1241 Lib_IntVector_Intrinsics_vec256 o4 = x42; 1242 acc[0U] = o0; 1243 acc[1U] = o1; 1244 acc[2U] = o2; 1245 acc[3U] = o3; 1246 acc[4U] = o4; 1247 } 1248 1249 void 1250 Hacl_Poly1305_256_poly1305_update( 1251 Lib_IntVector_Intrinsics_vec256 *ctx, 1252 uint32_t len, 1253 uint8_t *text) 1254 { 1255 Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; 1256 Lib_IntVector_Intrinsics_vec256 *acc = ctx; 1257 uint32_t sz_block = (uint32_t)64U; 1258 uint32_t len0 = len / sz_block * sz_block; 1259 uint8_t *t0 = text; 1260 if (len0 > (uint32_t)0U) { 1261 uint32_t bs = (uint32_t)64U; 1262 uint8_t *text0 = t0; 1263 Hacl_Impl_Poly1305_Field32xN_256_load_acc4(acc, text0); 1264 uint32_t len1 = len0 - bs; 1265 uint8_t *text1 = t0 + bs; 1266 uint32_t nb = len1 / bs; 1267 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 1268 uint8_t *block = text1 + i * bs; 1269 KRML_PRE_ALIGN(32) 1270 Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; 1271 Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(block); 1272 Lib_IntVector_Intrinsics_vec256 1273 hi = Lib_IntVector_Intrinsics_vec256_load64_le(block + (uint32_t)32U); 1274 Lib_IntVector_Intrinsics_vec256 1275 mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 1276 Lib_IntVector_Intrinsics_vec256 1277 m0 = Lib_IntVector_Intrinsics_vec256_interleave_low128(lo, hi); 1278 Lib_IntVector_Intrinsics_vec256 1279 m1 = Lib_IntVector_Intrinsics_vec256_interleave_high128(lo, hi); 1280 Lib_IntVector_Intrinsics_vec256 1281 m2 = Lib_IntVector_Intrinsics_vec256_shift_right(m0, (uint32_t)48U); 1282 Lib_IntVector_Intrinsics_vec256 1283 m3 = Lib_IntVector_Intrinsics_vec256_shift_right(m1, (uint32_t)48U); 1284 Lib_IntVector_Intrinsics_vec256 1285 m4 = Lib_IntVector_Intrinsics_vec256_interleave_high64(m0, m1); 1286 Lib_IntVector_Intrinsics_vec256 1287 t010 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m0, m1); 1288 Lib_IntVector_Intrinsics_vec256 1289 t30 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m2, m3); 1290 Lib_IntVector_Intrinsics_vec256 1291 t20 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)4U); 1292 Lib_IntVector_Intrinsics_vec256 o20 = Lib_IntVector_Intrinsics_vec256_and(t20, mask260); 1293 Lib_IntVector_Intrinsics_vec256 1294 t10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t010, (uint32_t)26U); 1295 Lib_IntVector_Intrinsics_vec256 o10 = Lib_IntVector_Intrinsics_vec256_and(t10, mask260); 1296 Lib_IntVector_Intrinsics_vec256 o5 = Lib_IntVector_Intrinsics_vec256_and(t010, mask260); 1297 Lib_IntVector_Intrinsics_vec256 1298 t31 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)30U); 1299 Lib_IntVector_Intrinsics_vec256 o30 = Lib_IntVector_Intrinsics_vec256_and(t31, mask260); 1300 Lib_IntVector_Intrinsics_vec256 1301 o40 = Lib_IntVector_Intrinsics_vec256_shift_right64(m4, (uint32_t)40U); 1302 Lib_IntVector_Intrinsics_vec256 o00 = o5; 1303 Lib_IntVector_Intrinsics_vec256 o11 = o10; 1304 Lib_IntVector_Intrinsics_vec256 o21 = o20; 1305 Lib_IntVector_Intrinsics_vec256 o31 = o30; 1306 Lib_IntVector_Intrinsics_vec256 o41 = o40; 1307 e[0U] = o00; 1308 e[1U] = o11; 1309 e[2U] = o21; 1310 e[3U] = o31; 1311 e[4U] = o41; 1312 uint64_t b = (uint64_t)0x1000000U; 1313 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); 1314 Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; 1315 e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); 1316 Lib_IntVector_Intrinsics_vec256 *rn = pre + (uint32_t)10U; 1317 Lib_IntVector_Intrinsics_vec256 *rn5 = pre + (uint32_t)15U; 1318 Lib_IntVector_Intrinsics_vec256 r0 = rn[0U]; 1319 Lib_IntVector_Intrinsics_vec256 r1 = rn[1U]; 1320 Lib_IntVector_Intrinsics_vec256 r2 = rn[2U]; 1321 Lib_IntVector_Intrinsics_vec256 r3 = rn[3U]; 1322 Lib_IntVector_Intrinsics_vec256 r4 = rn[4U]; 1323 Lib_IntVector_Intrinsics_vec256 r51 = rn5[1U]; 1324 Lib_IntVector_Intrinsics_vec256 r52 = rn5[2U]; 1325 Lib_IntVector_Intrinsics_vec256 r53 = rn5[3U]; 1326 Lib_IntVector_Intrinsics_vec256 r54 = rn5[4U]; 1327 Lib_IntVector_Intrinsics_vec256 f10 = acc[0U]; 1328 Lib_IntVector_Intrinsics_vec256 f110 = acc[1U]; 1329 Lib_IntVector_Intrinsics_vec256 f120 = acc[2U]; 1330 Lib_IntVector_Intrinsics_vec256 f130 = acc[3U]; 1331 Lib_IntVector_Intrinsics_vec256 f140 = acc[4U]; 1332 Lib_IntVector_Intrinsics_vec256 a0 = Lib_IntVector_Intrinsics_vec256_mul64(r0, f10); 1333 Lib_IntVector_Intrinsics_vec256 a1 = Lib_IntVector_Intrinsics_vec256_mul64(r1, f10); 1334 Lib_IntVector_Intrinsics_vec256 a2 = Lib_IntVector_Intrinsics_vec256_mul64(r2, f10); 1335 Lib_IntVector_Intrinsics_vec256 a3 = Lib_IntVector_Intrinsics_vec256_mul64(r3, f10); 1336 Lib_IntVector_Intrinsics_vec256 a4 = Lib_IntVector_Intrinsics_vec256_mul64(r4, f10); 1337 Lib_IntVector_Intrinsics_vec256 1338 a01 = 1339 Lib_IntVector_Intrinsics_vec256_add64(a0, 1340 Lib_IntVector_Intrinsics_vec256_mul64(r54, f110)); 1341 Lib_IntVector_Intrinsics_vec256 1342 a11 = 1343 Lib_IntVector_Intrinsics_vec256_add64(a1, 1344 Lib_IntVector_Intrinsics_vec256_mul64(r0, f110)); 1345 Lib_IntVector_Intrinsics_vec256 1346 a21 = 1347 Lib_IntVector_Intrinsics_vec256_add64(a2, 1348 Lib_IntVector_Intrinsics_vec256_mul64(r1, f110)); 1349 Lib_IntVector_Intrinsics_vec256 1350 a31 = 1351 Lib_IntVector_Intrinsics_vec256_add64(a3, 1352 Lib_IntVector_Intrinsics_vec256_mul64(r2, f110)); 1353 Lib_IntVector_Intrinsics_vec256 1354 a41 = 1355 Lib_IntVector_Intrinsics_vec256_add64(a4, 1356 Lib_IntVector_Intrinsics_vec256_mul64(r3, f110)); 1357 Lib_IntVector_Intrinsics_vec256 1358 a02 = 1359 Lib_IntVector_Intrinsics_vec256_add64(a01, 1360 Lib_IntVector_Intrinsics_vec256_mul64(r53, f120)); 1361 Lib_IntVector_Intrinsics_vec256 1362 a12 = 1363 Lib_IntVector_Intrinsics_vec256_add64(a11, 1364 Lib_IntVector_Intrinsics_vec256_mul64(r54, f120)); 1365 Lib_IntVector_Intrinsics_vec256 1366 a22 = 1367 Lib_IntVector_Intrinsics_vec256_add64(a21, 1368 Lib_IntVector_Intrinsics_vec256_mul64(r0, f120)); 1369 Lib_IntVector_Intrinsics_vec256 1370 a32 = 1371 Lib_IntVector_Intrinsics_vec256_add64(a31, 1372 Lib_IntVector_Intrinsics_vec256_mul64(r1, f120)); 1373 Lib_IntVector_Intrinsics_vec256 1374 a42 = 1375 Lib_IntVector_Intrinsics_vec256_add64(a41, 1376 Lib_IntVector_Intrinsics_vec256_mul64(r2, f120)); 1377 Lib_IntVector_Intrinsics_vec256 1378 a03 = 1379 Lib_IntVector_Intrinsics_vec256_add64(a02, 1380 Lib_IntVector_Intrinsics_vec256_mul64(r52, f130)); 1381 Lib_IntVector_Intrinsics_vec256 1382 a13 = 1383 Lib_IntVector_Intrinsics_vec256_add64(a12, 1384 Lib_IntVector_Intrinsics_vec256_mul64(r53, f130)); 1385 Lib_IntVector_Intrinsics_vec256 1386 a23 = 1387 Lib_IntVector_Intrinsics_vec256_add64(a22, 1388 Lib_IntVector_Intrinsics_vec256_mul64(r54, f130)); 1389 Lib_IntVector_Intrinsics_vec256 1390 a33 = 1391 Lib_IntVector_Intrinsics_vec256_add64(a32, 1392 Lib_IntVector_Intrinsics_vec256_mul64(r0, f130)); 1393 Lib_IntVector_Intrinsics_vec256 1394 a43 = 1395 Lib_IntVector_Intrinsics_vec256_add64(a42, 1396 Lib_IntVector_Intrinsics_vec256_mul64(r1, f130)); 1397 Lib_IntVector_Intrinsics_vec256 1398 a04 = 1399 Lib_IntVector_Intrinsics_vec256_add64(a03, 1400 Lib_IntVector_Intrinsics_vec256_mul64(r51, f140)); 1401 Lib_IntVector_Intrinsics_vec256 1402 a14 = 1403 Lib_IntVector_Intrinsics_vec256_add64(a13, 1404 Lib_IntVector_Intrinsics_vec256_mul64(r52, f140)); 1405 Lib_IntVector_Intrinsics_vec256 1406 a24 = 1407 Lib_IntVector_Intrinsics_vec256_add64(a23, 1408 Lib_IntVector_Intrinsics_vec256_mul64(r53, f140)); 1409 Lib_IntVector_Intrinsics_vec256 1410 a34 = 1411 Lib_IntVector_Intrinsics_vec256_add64(a33, 1412 Lib_IntVector_Intrinsics_vec256_mul64(r54, f140)); 1413 Lib_IntVector_Intrinsics_vec256 1414 a44 = 1415 Lib_IntVector_Intrinsics_vec256_add64(a43, 1416 Lib_IntVector_Intrinsics_vec256_mul64(r0, f140)); 1417 Lib_IntVector_Intrinsics_vec256 t01 = a04; 1418 Lib_IntVector_Intrinsics_vec256 t1 = a14; 1419 Lib_IntVector_Intrinsics_vec256 t2 = a24; 1420 Lib_IntVector_Intrinsics_vec256 t3 = a34; 1421 Lib_IntVector_Intrinsics_vec256 t4 = a44; 1422 Lib_IntVector_Intrinsics_vec256 1423 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 1424 Lib_IntVector_Intrinsics_vec256 1425 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); 1426 Lib_IntVector_Intrinsics_vec256 1427 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 1428 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); 1429 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 1430 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); 1431 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 1432 Lib_IntVector_Intrinsics_vec256 1433 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 1434 Lib_IntVector_Intrinsics_vec256 1435 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 1436 Lib_IntVector_Intrinsics_vec256 1437 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 1438 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 1439 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 1440 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 1441 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 1442 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); 1443 Lib_IntVector_Intrinsics_vec256 1444 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 1445 Lib_IntVector_Intrinsics_vec256 1446 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 1447 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 1448 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 1449 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 1450 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 1451 Lib_IntVector_Intrinsics_vec256 1452 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 1453 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 1454 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 1455 Lib_IntVector_Intrinsics_vec256 o01 = x02; 1456 Lib_IntVector_Intrinsics_vec256 o12 = x12; 1457 Lib_IntVector_Intrinsics_vec256 o22 = x21; 1458 Lib_IntVector_Intrinsics_vec256 o32 = x32; 1459 Lib_IntVector_Intrinsics_vec256 o42 = x42; 1460 acc[0U] = o01; 1461 acc[1U] = o12; 1462 acc[2U] = o22; 1463 acc[3U] = o32; 1464 acc[4U] = o42; 1465 Lib_IntVector_Intrinsics_vec256 f100 = acc[0U]; 1466 Lib_IntVector_Intrinsics_vec256 f11 = acc[1U]; 1467 Lib_IntVector_Intrinsics_vec256 f12 = acc[2U]; 1468 Lib_IntVector_Intrinsics_vec256 f13 = acc[3U]; 1469 Lib_IntVector_Intrinsics_vec256 f14 = acc[4U]; 1470 Lib_IntVector_Intrinsics_vec256 f20 = e[0U]; 1471 Lib_IntVector_Intrinsics_vec256 f21 = e[1U]; 1472 Lib_IntVector_Intrinsics_vec256 f22 = e[2U]; 1473 Lib_IntVector_Intrinsics_vec256 f23 = e[3U]; 1474 Lib_IntVector_Intrinsics_vec256 f24 = e[4U]; 1475 Lib_IntVector_Intrinsics_vec256 o0 = Lib_IntVector_Intrinsics_vec256_add64(f100, f20); 1476 Lib_IntVector_Intrinsics_vec256 o1 = Lib_IntVector_Intrinsics_vec256_add64(f11, f21); 1477 Lib_IntVector_Intrinsics_vec256 o2 = Lib_IntVector_Intrinsics_vec256_add64(f12, f22); 1478 Lib_IntVector_Intrinsics_vec256 o3 = Lib_IntVector_Intrinsics_vec256_add64(f13, f23); 1479 Lib_IntVector_Intrinsics_vec256 o4 = Lib_IntVector_Intrinsics_vec256_add64(f14, f24); 1480 acc[0U] = o0; 1481 acc[1U] = o1; 1482 acc[2U] = o2; 1483 acc[3U] = o3; 1484 acc[4U] = o4; 1485 } 1486 Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize(acc, pre); 1487 } 1488 uint32_t len1 = len - len0; 1489 uint8_t *t1 = text + len0; 1490 uint32_t nb = len1 / (uint32_t)16U; 1491 uint32_t rem = len1 % (uint32_t)16U; 1492 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 1493 uint8_t *block = t1 + i * (uint32_t)16U; 1494 KRML_PRE_ALIGN(32) 1495 Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; 1496 uint64_t u0 = load64_le(block); 1497 uint64_t lo = u0; 1498 uint64_t u = load64_le(block + (uint32_t)8U); 1499 uint64_t hi = u; 1500 Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); 1501 Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); 1502 Lib_IntVector_Intrinsics_vec256 1503 f010 = 1504 Lib_IntVector_Intrinsics_vec256_and(f0, 1505 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1506 Lib_IntVector_Intrinsics_vec256 1507 f110 = 1508 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1509 (uint32_t)26U), 1510 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1511 Lib_IntVector_Intrinsics_vec256 1512 f20 = 1513 Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1514 (uint32_t)52U), 1515 Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, 1516 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), 1517 (uint32_t)12U)); 1518 Lib_IntVector_Intrinsics_vec256 1519 f30 = 1520 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, 1521 (uint32_t)14U), 1522 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1523 Lib_IntVector_Intrinsics_vec256 1524 f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); 1525 Lib_IntVector_Intrinsics_vec256 f01 = f010; 1526 Lib_IntVector_Intrinsics_vec256 f111 = f110; 1527 Lib_IntVector_Intrinsics_vec256 f2 = f20; 1528 Lib_IntVector_Intrinsics_vec256 f3 = f30; 1529 Lib_IntVector_Intrinsics_vec256 f41 = f40; 1530 e[0U] = f01; 1531 e[1U] = f111; 1532 e[2U] = f2; 1533 e[3U] = f3; 1534 e[4U] = f41; 1535 uint64_t b = (uint64_t)0x1000000U; 1536 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); 1537 Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; 1538 e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); 1539 Lib_IntVector_Intrinsics_vec256 *r = pre; 1540 Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; 1541 Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; 1542 Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; 1543 Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; 1544 Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; 1545 Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; 1546 Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; 1547 Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; 1548 Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; 1549 Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; 1550 Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; 1551 Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; 1552 Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; 1553 Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; 1554 Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; 1555 Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; 1556 Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; 1557 Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; 1558 Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; 1559 Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; 1560 Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); 1561 Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); 1562 Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); 1563 Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); 1564 Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); 1565 Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); 1566 Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); 1567 Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); 1568 Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); 1569 Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); 1570 Lib_IntVector_Intrinsics_vec256 1571 a03 = 1572 Lib_IntVector_Intrinsics_vec256_add64(a02, 1573 Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); 1574 Lib_IntVector_Intrinsics_vec256 1575 a13 = 1576 Lib_IntVector_Intrinsics_vec256_add64(a12, 1577 Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); 1578 Lib_IntVector_Intrinsics_vec256 1579 a23 = 1580 Lib_IntVector_Intrinsics_vec256_add64(a22, 1581 Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); 1582 Lib_IntVector_Intrinsics_vec256 1583 a33 = 1584 Lib_IntVector_Intrinsics_vec256_add64(a32, 1585 Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); 1586 Lib_IntVector_Intrinsics_vec256 1587 a43 = 1588 Lib_IntVector_Intrinsics_vec256_add64(a42, 1589 Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); 1590 Lib_IntVector_Intrinsics_vec256 1591 a04 = 1592 Lib_IntVector_Intrinsics_vec256_add64(a03, 1593 Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); 1594 Lib_IntVector_Intrinsics_vec256 1595 a14 = 1596 Lib_IntVector_Intrinsics_vec256_add64(a13, 1597 Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); 1598 Lib_IntVector_Intrinsics_vec256 1599 a24 = 1600 Lib_IntVector_Intrinsics_vec256_add64(a23, 1601 Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); 1602 Lib_IntVector_Intrinsics_vec256 1603 a34 = 1604 Lib_IntVector_Intrinsics_vec256_add64(a33, 1605 Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); 1606 Lib_IntVector_Intrinsics_vec256 1607 a44 = 1608 Lib_IntVector_Intrinsics_vec256_add64(a43, 1609 Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); 1610 Lib_IntVector_Intrinsics_vec256 1611 a05 = 1612 Lib_IntVector_Intrinsics_vec256_add64(a04, 1613 Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); 1614 Lib_IntVector_Intrinsics_vec256 1615 a15 = 1616 Lib_IntVector_Intrinsics_vec256_add64(a14, 1617 Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); 1618 Lib_IntVector_Intrinsics_vec256 1619 a25 = 1620 Lib_IntVector_Intrinsics_vec256_add64(a24, 1621 Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); 1622 Lib_IntVector_Intrinsics_vec256 1623 a35 = 1624 Lib_IntVector_Intrinsics_vec256_add64(a34, 1625 Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); 1626 Lib_IntVector_Intrinsics_vec256 1627 a45 = 1628 Lib_IntVector_Intrinsics_vec256_add64(a44, 1629 Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); 1630 Lib_IntVector_Intrinsics_vec256 1631 a06 = 1632 Lib_IntVector_Intrinsics_vec256_add64(a05, 1633 Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); 1634 Lib_IntVector_Intrinsics_vec256 1635 a16 = 1636 Lib_IntVector_Intrinsics_vec256_add64(a15, 1637 Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); 1638 Lib_IntVector_Intrinsics_vec256 1639 a26 = 1640 Lib_IntVector_Intrinsics_vec256_add64(a25, 1641 Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); 1642 Lib_IntVector_Intrinsics_vec256 1643 a36 = 1644 Lib_IntVector_Intrinsics_vec256_add64(a35, 1645 Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); 1646 Lib_IntVector_Intrinsics_vec256 1647 a46 = 1648 Lib_IntVector_Intrinsics_vec256_add64(a45, 1649 Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); 1650 Lib_IntVector_Intrinsics_vec256 t01 = a06; 1651 Lib_IntVector_Intrinsics_vec256 t11 = a16; 1652 Lib_IntVector_Intrinsics_vec256 t2 = a26; 1653 Lib_IntVector_Intrinsics_vec256 t3 = a36; 1654 Lib_IntVector_Intrinsics_vec256 t4 = a46; 1655 Lib_IntVector_Intrinsics_vec256 1656 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 1657 Lib_IntVector_Intrinsics_vec256 1658 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); 1659 Lib_IntVector_Intrinsics_vec256 1660 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 1661 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); 1662 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 1663 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t11, z0); 1664 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 1665 Lib_IntVector_Intrinsics_vec256 1666 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 1667 Lib_IntVector_Intrinsics_vec256 1668 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 1669 Lib_IntVector_Intrinsics_vec256 1670 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 1671 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 1672 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 1673 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 1674 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 1675 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); 1676 Lib_IntVector_Intrinsics_vec256 1677 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 1678 Lib_IntVector_Intrinsics_vec256 1679 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 1680 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 1681 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 1682 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 1683 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 1684 Lib_IntVector_Intrinsics_vec256 1685 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 1686 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 1687 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 1688 Lib_IntVector_Intrinsics_vec256 o0 = x02; 1689 Lib_IntVector_Intrinsics_vec256 o1 = x12; 1690 Lib_IntVector_Intrinsics_vec256 o2 = x21; 1691 Lib_IntVector_Intrinsics_vec256 o3 = x32; 1692 Lib_IntVector_Intrinsics_vec256 o4 = x42; 1693 acc[0U] = o0; 1694 acc[1U] = o1; 1695 acc[2U] = o2; 1696 acc[3U] = o3; 1697 acc[4U] = o4; 1698 } 1699 if (rem > (uint32_t)0U) { 1700 uint8_t *last = t1 + nb * (uint32_t)16U; 1701 KRML_PRE_ALIGN(32) 1702 Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; 1703 uint8_t tmp[16U] = { 0U }; 1704 memcpy(tmp, last, rem * sizeof(uint8_t)); 1705 uint64_t u0 = load64_le(tmp); 1706 uint64_t lo = u0; 1707 uint64_t u = load64_le(tmp + (uint32_t)8U); 1708 uint64_t hi = u; 1709 Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); 1710 Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); 1711 Lib_IntVector_Intrinsics_vec256 1712 f010 = 1713 Lib_IntVector_Intrinsics_vec256_and(f0, 1714 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1715 Lib_IntVector_Intrinsics_vec256 1716 f110 = 1717 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1718 (uint32_t)26U), 1719 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1720 Lib_IntVector_Intrinsics_vec256 1721 f20 = 1722 Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, 1723 (uint32_t)52U), 1724 Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, 1725 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), 1726 (uint32_t)12U)); 1727 Lib_IntVector_Intrinsics_vec256 1728 f30 = 1729 Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, 1730 (uint32_t)14U), 1731 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1732 Lib_IntVector_Intrinsics_vec256 1733 f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); 1734 Lib_IntVector_Intrinsics_vec256 f01 = f010; 1735 Lib_IntVector_Intrinsics_vec256 f111 = f110; 1736 Lib_IntVector_Intrinsics_vec256 f2 = f20; 1737 Lib_IntVector_Intrinsics_vec256 f3 = f30; 1738 Lib_IntVector_Intrinsics_vec256 f4 = f40; 1739 e[0U] = f01; 1740 e[1U] = f111; 1741 e[2U] = f2; 1742 e[3U] = f3; 1743 e[4U] = f4; 1744 uint64_t b = (uint64_t)1U << rem * (uint32_t)8U % (uint32_t)26U; 1745 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); 1746 Lib_IntVector_Intrinsics_vec256 fi = e[rem * (uint32_t)8U / (uint32_t)26U]; 1747 e[rem * (uint32_t)8U / (uint32_t)26U] = Lib_IntVector_Intrinsics_vec256_or(fi, mask); 1748 Lib_IntVector_Intrinsics_vec256 *r = pre; 1749 Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; 1750 Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; 1751 Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; 1752 Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; 1753 Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; 1754 Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; 1755 Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; 1756 Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; 1757 Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; 1758 Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; 1759 Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; 1760 Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; 1761 Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; 1762 Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; 1763 Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; 1764 Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; 1765 Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; 1766 Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; 1767 Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; 1768 Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; 1769 Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); 1770 Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); 1771 Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); 1772 Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); 1773 Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); 1774 Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); 1775 Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); 1776 Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); 1777 Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); 1778 Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); 1779 Lib_IntVector_Intrinsics_vec256 1780 a03 = 1781 Lib_IntVector_Intrinsics_vec256_add64(a02, 1782 Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); 1783 Lib_IntVector_Intrinsics_vec256 1784 a13 = 1785 Lib_IntVector_Intrinsics_vec256_add64(a12, 1786 Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); 1787 Lib_IntVector_Intrinsics_vec256 1788 a23 = 1789 Lib_IntVector_Intrinsics_vec256_add64(a22, 1790 Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); 1791 Lib_IntVector_Intrinsics_vec256 1792 a33 = 1793 Lib_IntVector_Intrinsics_vec256_add64(a32, 1794 Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); 1795 Lib_IntVector_Intrinsics_vec256 1796 a43 = 1797 Lib_IntVector_Intrinsics_vec256_add64(a42, 1798 Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); 1799 Lib_IntVector_Intrinsics_vec256 1800 a04 = 1801 Lib_IntVector_Intrinsics_vec256_add64(a03, 1802 Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); 1803 Lib_IntVector_Intrinsics_vec256 1804 a14 = 1805 Lib_IntVector_Intrinsics_vec256_add64(a13, 1806 Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); 1807 Lib_IntVector_Intrinsics_vec256 1808 a24 = 1809 Lib_IntVector_Intrinsics_vec256_add64(a23, 1810 Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); 1811 Lib_IntVector_Intrinsics_vec256 1812 a34 = 1813 Lib_IntVector_Intrinsics_vec256_add64(a33, 1814 Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); 1815 Lib_IntVector_Intrinsics_vec256 1816 a44 = 1817 Lib_IntVector_Intrinsics_vec256_add64(a43, 1818 Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); 1819 Lib_IntVector_Intrinsics_vec256 1820 a05 = 1821 Lib_IntVector_Intrinsics_vec256_add64(a04, 1822 Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); 1823 Lib_IntVector_Intrinsics_vec256 1824 a15 = 1825 Lib_IntVector_Intrinsics_vec256_add64(a14, 1826 Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); 1827 Lib_IntVector_Intrinsics_vec256 1828 a25 = 1829 Lib_IntVector_Intrinsics_vec256_add64(a24, 1830 Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); 1831 Lib_IntVector_Intrinsics_vec256 1832 a35 = 1833 Lib_IntVector_Intrinsics_vec256_add64(a34, 1834 Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); 1835 Lib_IntVector_Intrinsics_vec256 1836 a45 = 1837 Lib_IntVector_Intrinsics_vec256_add64(a44, 1838 Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); 1839 Lib_IntVector_Intrinsics_vec256 1840 a06 = 1841 Lib_IntVector_Intrinsics_vec256_add64(a05, 1842 Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); 1843 Lib_IntVector_Intrinsics_vec256 1844 a16 = 1845 Lib_IntVector_Intrinsics_vec256_add64(a15, 1846 Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); 1847 Lib_IntVector_Intrinsics_vec256 1848 a26 = 1849 Lib_IntVector_Intrinsics_vec256_add64(a25, 1850 Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); 1851 Lib_IntVector_Intrinsics_vec256 1852 a36 = 1853 Lib_IntVector_Intrinsics_vec256_add64(a35, 1854 Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); 1855 Lib_IntVector_Intrinsics_vec256 1856 a46 = 1857 Lib_IntVector_Intrinsics_vec256_add64(a45, 1858 Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); 1859 Lib_IntVector_Intrinsics_vec256 t01 = a06; 1860 Lib_IntVector_Intrinsics_vec256 t11 = a16; 1861 Lib_IntVector_Intrinsics_vec256 t2 = a26; 1862 Lib_IntVector_Intrinsics_vec256 t3 = a36; 1863 Lib_IntVector_Intrinsics_vec256 t4 = a46; 1864 Lib_IntVector_Intrinsics_vec256 1865 mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 1866 Lib_IntVector_Intrinsics_vec256 1867 z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); 1868 Lib_IntVector_Intrinsics_vec256 1869 z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); 1870 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); 1871 Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); 1872 Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t11, z0); 1873 Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); 1874 Lib_IntVector_Intrinsics_vec256 1875 z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); 1876 Lib_IntVector_Intrinsics_vec256 1877 z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); 1878 Lib_IntVector_Intrinsics_vec256 1879 t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); 1880 Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); 1881 Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); 1882 Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); 1883 Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); 1884 Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); 1885 Lib_IntVector_Intrinsics_vec256 1886 z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); 1887 Lib_IntVector_Intrinsics_vec256 1888 z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); 1889 Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); 1890 Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); 1891 Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); 1892 Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); 1893 Lib_IntVector_Intrinsics_vec256 1894 z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); 1895 Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); 1896 Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); 1897 Lib_IntVector_Intrinsics_vec256 o0 = x02; 1898 Lib_IntVector_Intrinsics_vec256 o1 = x12; 1899 Lib_IntVector_Intrinsics_vec256 o2 = x21; 1900 Lib_IntVector_Intrinsics_vec256 o3 = x32; 1901 Lib_IntVector_Intrinsics_vec256 o4 = x42; 1902 acc[0U] = o0; 1903 acc[1U] = o1; 1904 acc[2U] = o2; 1905 acc[3U] = o3; 1906 acc[4U] = o4; 1907 return; 1908 } 1909 } 1910 1911 void 1912 Hacl_Poly1305_256_poly1305_finish( 1913 uint8_t *tag, 1914 uint8_t *key, 1915 Lib_IntVector_Intrinsics_vec256 *ctx) 1916 { 1917 Lib_IntVector_Intrinsics_vec256 *acc = ctx; 1918 uint8_t *ks = key + (uint32_t)16U; 1919 Lib_IntVector_Intrinsics_vec256 f0 = acc[0U]; 1920 Lib_IntVector_Intrinsics_vec256 f13 = acc[1U]; 1921 Lib_IntVector_Intrinsics_vec256 f23 = acc[2U]; 1922 Lib_IntVector_Intrinsics_vec256 f33 = acc[3U]; 1923 Lib_IntVector_Intrinsics_vec256 f40 = acc[4U]; 1924 Lib_IntVector_Intrinsics_vec256 1925 l0 = Lib_IntVector_Intrinsics_vec256_add64(f0, Lib_IntVector_Intrinsics_vec256_zero); 1926 Lib_IntVector_Intrinsics_vec256 1927 tmp00 = 1928 Lib_IntVector_Intrinsics_vec256_and(l0, 1929 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1930 Lib_IntVector_Intrinsics_vec256 1931 c00 = Lib_IntVector_Intrinsics_vec256_shift_right64(l0, (uint32_t)26U); 1932 Lib_IntVector_Intrinsics_vec256 l1 = Lib_IntVector_Intrinsics_vec256_add64(f13, c00); 1933 Lib_IntVector_Intrinsics_vec256 1934 tmp10 = 1935 Lib_IntVector_Intrinsics_vec256_and(l1, 1936 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1937 Lib_IntVector_Intrinsics_vec256 1938 c10 = Lib_IntVector_Intrinsics_vec256_shift_right64(l1, (uint32_t)26U); 1939 Lib_IntVector_Intrinsics_vec256 l2 = Lib_IntVector_Intrinsics_vec256_add64(f23, c10); 1940 Lib_IntVector_Intrinsics_vec256 1941 tmp20 = 1942 Lib_IntVector_Intrinsics_vec256_and(l2, 1943 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1944 Lib_IntVector_Intrinsics_vec256 1945 c20 = Lib_IntVector_Intrinsics_vec256_shift_right64(l2, (uint32_t)26U); 1946 Lib_IntVector_Intrinsics_vec256 l3 = Lib_IntVector_Intrinsics_vec256_add64(f33, c20); 1947 Lib_IntVector_Intrinsics_vec256 1948 tmp30 = 1949 Lib_IntVector_Intrinsics_vec256_and(l3, 1950 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1951 Lib_IntVector_Intrinsics_vec256 1952 c30 = Lib_IntVector_Intrinsics_vec256_shift_right64(l3, (uint32_t)26U); 1953 Lib_IntVector_Intrinsics_vec256 l4 = Lib_IntVector_Intrinsics_vec256_add64(f40, c30); 1954 Lib_IntVector_Intrinsics_vec256 1955 tmp40 = 1956 Lib_IntVector_Intrinsics_vec256_and(l4, 1957 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1958 Lib_IntVector_Intrinsics_vec256 1959 c40 = Lib_IntVector_Intrinsics_vec256_shift_right64(l4, (uint32_t)26U); 1960 Lib_IntVector_Intrinsics_vec256 1961 f010 = 1962 Lib_IntVector_Intrinsics_vec256_add64(tmp00, 1963 Lib_IntVector_Intrinsics_vec256_smul64(c40, (uint64_t)5U)); 1964 Lib_IntVector_Intrinsics_vec256 f110 = tmp10; 1965 Lib_IntVector_Intrinsics_vec256 f210 = tmp20; 1966 Lib_IntVector_Intrinsics_vec256 f310 = tmp30; 1967 Lib_IntVector_Intrinsics_vec256 f410 = tmp40; 1968 Lib_IntVector_Intrinsics_vec256 1969 l = Lib_IntVector_Intrinsics_vec256_add64(f010, Lib_IntVector_Intrinsics_vec256_zero); 1970 Lib_IntVector_Intrinsics_vec256 1971 tmp0 = 1972 Lib_IntVector_Intrinsics_vec256_and(l, 1973 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1974 Lib_IntVector_Intrinsics_vec256 1975 c0 = Lib_IntVector_Intrinsics_vec256_shift_right64(l, (uint32_t)26U); 1976 Lib_IntVector_Intrinsics_vec256 l5 = Lib_IntVector_Intrinsics_vec256_add64(f110, c0); 1977 Lib_IntVector_Intrinsics_vec256 1978 tmp1 = 1979 Lib_IntVector_Intrinsics_vec256_and(l5, 1980 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1981 Lib_IntVector_Intrinsics_vec256 1982 c1 = Lib_IntVector_Intrinsics_vec256_shift_right64(l5, (uint32_t)26U); 1983 Lib_IntVector_Intrinsics_vec256 l6 = Lib_IntVector_Intrinsics_vec256_add64(f210, c1); 1984 Lib_IntVector_Intrinsics_vec256 1985 tmp2 = 1986 Lib_IntVector_Intrinsics_vec256_and(l6, 1987 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1988 Lib_IntVector_Intrinsics_vec256 1989 c2 = Lib_IntVector_Intrinsics_vec256_shift_right64(l6, (uint32_t)26U); 1990 Lib_IntVector_Intrinsics_vec256 l7 = Lib_IntVector_Intrinsics_vec256_add64(f310, c2); 1991 Lib_IntVector_Intrinsics_vec256 1992 tmp3 = 1993 Lib_IntVector_Intrinsics_vec256_and(l7, 1994 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 1995 Lib_IntVector_Intrinsics_vec256 1996 c3 = Lib_IntVector_Intrinsics_vec256_shift_right64(l7, (uint32_t)26U); 1997 Lib_IntVector_Intrinsics_vec256 l8 = Lib_IntVector_Intrinsics_vec256_add64(f410, c3); 1998 Lib_IntVector_Intrinsics_vec256 1999 tmp4 = 2000 Lib_IntVector_Intrinsics_vec256_and(l8, 2001 Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); 2002 Lib_IntVector_Intrinsics_vec256 2003 c4 = Lib_IntVector_Intrinsics_vec256_shift_right64(l8, (uint32_t)26U); 2004 Lib_IntVector_Intrinsics_vec256 2005 f02 = 2006 Lib_IntVector_Intrinsics_vec256_add64(tmp0, 2007 Lib_IntVector_Intrinsics_vec256_smul64(c4, (uint64_t)5U)); 2008 Lib_IntVector_Intrinsics_vec256 f12 = tmp1; 2009 Lib_IntVector_Intrinsics_vec256 f22 = tmp2; 2010 Lib_IntVector_Intrinsics_vec256 f32 = tmp3; 2011 Lib_IntVector_Intrinsics_vec256 f42 = tmp4; 2012 Lib_IntVector_Intrinsics_vec256 2013 mh = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); 2014 Lib_IntVector_Intrinsics_vec256 2015 ml = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffffbU); 2016 Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_eq64(f42, mh); 2017 Lib_IntVector_Intrinsics_vec256 2018 mask1 = 2019 Lib_IntVector_Intrinsics_vec256_and(mask, 2020 Lib_IntVector_Intrinsics_vec256_eq64(f32, mh)); 2021 Lib_IntVector_Intrinsics_vec256 2022 mask2 = 2023 Lib_IntVector_Intrinsics_vec256_and(mask1, 2024 Lib_IntVector_Intrinsics_vec256_eq64(f22, mh)); 2025 Lib_IntVector_Intrinsics_vec256 2026 mask3 = 2027 Lib_IntVector_Intrinsics_vec256_and(mask2, 2028 Lib_IntVector_Intrinsics_vec256_eq64(f12, mh)); 2029 Lib_IntVector_Intrinsics_vec256 2030 mask4 = 2031 Lib_IntVector_Intrinsics_vec256_and(mask3, 2032 Lib_IntVector_Intrinsics_vec256_lognot(Lib_IntVector_Intrinsics_vec256_gt64(ml, f02))); 2033 Lib_IntVector_Intrinsics_vec256 ph = Lib_IntVector_Intrinsics_vec256_and(mask4, mh); 2034 Lib_IntVector_Intrinsics_vec256 pl = Lib_IntVector_Intrinsics_vec256_and(mask4, ml); 2035 Lib_IntVector_Intrinsics_vec256 o0 = Lib_IntVector_Intrinsics_vec256_sub64(f02, pl); 2036 Lib_IntVector_Intrinsics_vec256 o1 = Lib_IntVector_Intrinsics_vec256_sub64(f12, ph); 2037 Lib_IntVector_Intrinsics_vec256 o2 = Lib_IntVector_Intrinsics_vec256_sub64(f22, ph); 2038 Lib_IntVector_Intrinsics_vec256 o3 = Lib_IntVector_Intrinsics_vec256_sub64(f32, ph); 2039 Lib_IntVector_Intrinsics_vec256 o4 = Lib_IntVector_Intrinsics_vec256_sub64(f42, ph); 2040 Lib_IntVector_Intrinsics_vec256 f011 = o0; 2041 Lib_IntVector_Intrinsics_vec256 f111 = o1; 2042 Lib_IntVector_Intrinsics_vec256 f211 = o2; 2043 Lib_IntVector_Intrinsics_vec256 f311 = o3; 2044 Lib_IntVector_Intrinsics_vec256 f411 = o4; 2045 acc[0U] = f011; 2046 acc[1U] = f111; 2047 acc[2U] = f211; 2048 acc[3U] = f311; 2049 acc[4U] = f411; 2050 Lib_IntVector_Intrinsics_vec256 f00 = acc[0U]; 2051 Lib_IntVector_Intrinsics_vec256 f1 = acc[1U]; 2052 Lib_IntVector_Intrinsics_vec256 f2 = acc[2U]; 2053 Lib_IntVector_Intrinsics_vec256 f3 = acc[3U]; 2054 Lib_IntVector_Intrinsics_vec256 f4 = acc[4U]; 2055 uint64_t f01 = Lib_IntVector_Intrinsics_vec256_extract64(f00, (uint32_t)0U); 2056 uint64_t f112 = Lib_IntVector_Intrinsics_vec256_extract64(f1, (uint32_t)0U); 2057 uint64_t f212 = Lib_IntVector_Intrinsics_vec256_extract64(f2, (uint32_t)0U); 2058 uint64_t f312 = Lib_IntVector_Intrinsics_vec256_extract64(f3, (uint32_t)0U); 2059 uint64_t f41 = Lib_IntVector_Intrinsics_vec256_extract64(f4, (uint32_t)0U); 2060 uint64_t lo = (f01 | f112 << (uint32_t)26U) | f212 << (uint32_t)52U; 2061 uint64_t hi = (f212 >> (uint32_t)12U | f312 << (uint32_t)14U) | f41 << (uint32_t)40U; 2062 uint64_t f10 = lo; 2063 uint64_t f11 = hi; 2064 uint64_t u0 = load64_le(ks); 2065 uint64_t lo0 = u0; 2066 uint64_t u = load64_le(ks + (uint32_t)8U); 2067 uint64_t hi0 = u; 2068 uint64_t f20 = lo0; 2069 uint64_t f21 = hi0; 2070 uint64_t r0 = f10 + f20; 2071 uint64_t r1 = f11 + f21; 2072 uint64_t c = (r0 ^ ((r0 ^ f20) | ((r0 - f20) ^ f20))) >> (uint32_t)63U; 2073 uint64_t r11 = r1 + c; 2074 uint64_t f30 = r0; 2075 uint64_t f31 = r11; 2076 store64_le(tag, f30); 2077 store64_le(tag + (uint32_t)8U, f31); 2078 } 2079 2080 void 2081 Hacl_Poly1305_256_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key) 2082 { 2083 KRML_PRE_ALIGN(32) 2084 Lib_IntVector_Intrinsics_vec256 ctx[25U] KRML_POST_ALIGN(32) = { 0U }; 2085 Hacl_Poly1305_256_poly1305_init(ctx, key); 2086 Hacl_Poly1305_256_poly1305_update(ctx, len, text); 2087 Hacl_Poly1305_256_poly1305_finish(tag, key, ctx); 2088 }