Hacl_Poly1305_128.c (93046B)
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_128.h" 26 27 void 28 Hacl_Impl_Poly1305_Field32xN_128_load_acc2(Lib_IntVector_Intrinsics_vec128 *acc, uint8_t *b) 29 { 30 KRML_PRE_ALIGN(16) 31 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 32 Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(b); 33 Lib_IntVector_Intrinsics_vec128 34 b2 = Lib_IntVector_Intrinsics_vec128_load64_le(b + (uint32_t)16U); 35 Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2); 36 Lib_IntVector_Intrinsics_vec128 hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2); 37 Lib_IntVector_Intrinsics_vec128 38 f00 = 39 Lib_IntVector_Intrinsics_vec128_and(lo, 40 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 41 Lib_IntVector_Intrinsics_vec128 42 f10 = 43 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 44 (uint32_t)26U), 45 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 46 Lib_IntVector_Intrinsics_vec128 47 f20 = 48 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 49 (uint32_t)52U), 50 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(hi, 51 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 52 (uint32_t)12U)); 53 Lib_IntVector_Intrinsics_vec128 54 f30 = 55 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(hi, 56 (uint32_t)14U), 57 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 58 Lib_IntVector_Intrinsics_vec128 59 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(hi, (uint32_t)40U); 60 Lib_IntVector_Intrinsics_vec128 f02 = f00; 61 Lib_IntVector_Intrinsics_vec128 f12 = f10; 62 Lib_IntVector_Intrinsics_vec128 f22 = f20; 63 Lib_IntVector_Intrinsics_vec128 f32 = f30; 64 Lib_IntVector_Intrinsics_vec128 f42 = f40; 65 e[0U] = f02; 66 e[1U] = f12; 67 e[2U] = f22; 68 e[3U] = f32; 69 e[4U] = f42; 70 uint64_t b10 = (uint64_t)0x1000000U; 71 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b10); 72 Lib_IntVector_Intrinsics_vec128 f43 = e[4U]; 73 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f43, mask); 74 Lib_IntVector_Intrinsics_vec128 acc0 = acc[0U]; 75 Lib_IntVector_Intrinsics_vec128 acc1 = acc[1U]; 76 Lib_IntVector_Intrinsics_vec128 acc2 = acc[2U]; 77 Lib_IntVector_Intrinsics_vec128 acc3 = acc[3U]; 78 Lib_IntVector_Intrinsics_vec128 acc4 = acc[4U]; 79 Lib_IntVector_Intrinsics_vec128 e0 = e[0U]; 80 Lib_IntVector_Intrinsics_vec128 e1 = e[1U]; 81 Lib_IntVector_Intrinsics_vec128 e2 = e[2U]; 82 Lib_IntVector_Intrinsics_vec128 e3 = e[3U]; 83 Lib_IntVector_Intrinsics_vec128 e4 = e[4U]; 84 Lib_IntVector_Intrinsics_vec128 85 f0 = Lib_IntVector_Intrinsics_vec128_insert64(acc0, (uint64_t)0U, (uint32_t)1U); 86 Lib_IntVector_Intrinsics_vec128 87 f1 = Lib_IntVector_Intrinsics_vec128_insert64(acc1, (uint64_t)0U, (uint32_t)1U); 88 Lib_IntVector_Intrinsics_vec128 89 f2 = Lib_IntVector_Intrinsics_vec128_insert64(acc2, (uint64_t)0U, (uint32_t)1U); 90 Lib_IntVector_Intrinsics_vec128 91 f3 = Lib_IntVector_Intrinsics_vec128_insert64(acc3, (uint64_t)0U, (uint32_t)1U); 92 Lib_IntVector_Intrinsics_vec128 93 f4 = Lib_IntVector_Intrinsics_vec128_insert64(acc4, (uint64_t)0U, (uint32_t)1U); 94 Lib_IntVector_Intrinsics_vec128 f01 = Lib_IntVector_Intrinsics_vec128_add64(f0, e0); 95 Lib_IntVector_Intrinsics_vec128 f11 = Lib_IntVector_Intrinsics_vec128_add64(f1, e1); 96 Lib_IntVector_Intrinsics_vec128 f21 = Lib_IntVector_Intrinsics_vec128_add64(f2, e2); 97 Lib_IntVector_Intrinsics_vec128 f31 = Lib_IntVector_Intrinsics_vec128_add64(f3, e3); 98 Lib_IntVector_Intrinsics_vec128 f41 = Lib_IntVector_Intrinsics_vec128_add64(f4, e4); 99 Lib_IntVector_Intrinsics_vec128 acc01 = f01; 100 Lib_IntVector_Intrinsics_vec128 acc11 = f11; 101 Lib_IntVector_Intrinsics_vec128 acc21 = f21; 102 Lib_IntVector_Intrinsics_vec128 acc31 = f31; 103 Lib_IntVector_Intrinsics_vec128 acc41 = f41; 104 acc[0U] = acc01; 105 acc[1U] = acc11; 106 acc[2U] = acc21; 107 acc[3U] = acc31; 108 acc[4U] = acc41; 109 } 110 111 void 112 Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize( 113 Lib_IntVector_Intrinsics_vec128 *out, 114 Lib_IntVector_Intrinsics_vec128 *p) 115 { 116 Lib_IntVector_Intrinsics_vec128 *r = p; 117 Lib_IntVector_Intrinsics_vec128 *r2 = p + (uint32_t)10U; 118 Lib_IntVector_Intrinsics_vec128 a0 = out[0U]; 119 Lib_IntVector_Intrinsics_vec128 a1 = out[1U]; 120 Lib_IntVector_Intrinsics_vec128 a2 = out[2U]; 121 Lib_IntVector_Intrinsics_vec128 a3 = out[3U]; 122 Lib_IntVector_Intrinsics_vec128 a4 = out[4U]; 123 Lib_IntVector_Intrinsics_vec128 r10 = r[0U]; 124 Lib_IntVector_Intrinsics_vec128 r11 = r[1U]; 125 Lib_IntVector_Intrinsics_vec128 r12 = r[2U]; 126 Lib_IntVector_Intrinsics_vec128 r13 = r[3U]; 127 Lib_IntVector_Intrinsics_vec128 r14 = r[4U]; 128 Lib_IntVector_Intrinsics_vec128 r20 = r2[0U]; 129 Lib_IntVector_Intrinsics_vec128 r21 = r2[1U]; 130 Lib_IntVector_Intrinsics_vec128 r22 = r2[2U]; 131 Lib_IntVector_Intrinsics_vec128 r23 = r2[3U]; 132 Lib_IntVector_Intrinsics_vec128 r24 = r2[4U]; 133 Lib_IntVector_Intrinsics_vec128 134 r201 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r20, r10); 135 Lib_IntVector_Intrinsics_vec128 136 r211 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r21, r11); 137 Lib_IntVector_Intrinsics_vec128 138 r221 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r22, r12); 139 Lib_IntVector_Intrinsics_vec128 140 r231 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r23, r13); 141 Lib_IntVector_Intrinsics_vec128 142 r241 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r24, r14); 143 Lib_IntVector_Intrinsics_vec128 144 r251 = Lib_IntVector_Intrinsics_vec128_smul64(r211, (uint64_t)5U); 145 Lib_IntVector_Intrinsics_vec128 146 r252 = Lib_IntVector_Intrinsics_vec128_smul64(r221, (uint64_t)5U); 147 Lib_IntVector_Intrinsics_vec128 148 r253 = Lib_IntVector_Intrinsics_vec128_smul64(r231, (uint64_t)5U); 149 Lib_IntVector_Intrinsics_vec128 150 r254 = Lib_IntVector_Intrinsics_vec128_smul64(r241, (uint64_t)5U); 151 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_mul64(r201, a0); 152 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_mul64(r211, a0); 153 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_mul64(r221, a0); 154 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_mul64(r231, a0); 155 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_mul64(r241, a0); 156 Lib_IntVector_Intrinsics_vec128 157 a02 = 158 Lib_IntVector_Intrinsics_vec128_add64(a01, 159 Lib_IntVector_Intrinsics_vec128_mul64(r254, a1)); 160 Lib_IntVector_Intrinsics_vec128 161 a12 = 162 Lib_IntVector_Intrinsics_vec128_add64(a11, 163 Lib_IntVector_Intrinsics_vec128_mul64(r201, a1)); 164 Lib_IntVector_Intrinsics_vec128 165 a22 = 166 Lib_IntVector_Intrinsics_vec128_add64(a21, 167 Lib_IntVector_Intrinsics_vec128_mul64(r211, a1)); 168 Lib_IntVector_Intrinsics_vec128 169 a32 = 170 Lib_IntVector_Intrinsics_vec128_add64(a31, 171 Lib_IntVector_Intrinsics_vec128_mul64(r221, a1)); 172 Lib_IntVector_Intrinsics_vec128 173 a42 = 174 Lib_IntVector_Intrinsics_vec128_add64(a41, 175 Lib_IntVector_Intrinsics_vec128_mul64(r231, a1)); 176 Lib_IntVector_Intrinsics_vec128 177 a03 = 178 Lib_IntVector_Intrinsics_vec128_add64(a02, 179 Lib_IntVector_Intrinsics_vec128_mul64(r253, a2)); 180 Lib_IntVector_Intrinsics_vec128 181 a13 = 182 Lib_IntVector_Intrinsics_vec128_add64(a12, 183 Lib_IntVector_Intrinsics_vec128_mul64(r254, a2)); 184 Lib_IntVector_Intrinsics_vec128 185 a23 = 186 Lib_IntVector_Intrinsics_vec128_add64(a22, 187 Lib_IntVector_Intrinsics_vec128_mul64(r201, a2)); 188 Lib_IntVector_Intrinsics_vec128 189 a33 = 190 Lib_IntVector_Intrinsics_vec128_add64(a32, 191 Lib_IntVector_Intrinsics_vec128_mul64(r211, a2)); 192 Lib_IntVector_Intrinsics_vec128 193 a43 = 194 Lib_IntVector_Intrinsics_vec128_add64(a42, 195 Lib_IntVector_Intrinsics_vec128_mul64(r221, a2)); 196 Lib_IntVector_Intrinsics_vec128 197 a04 = 198 Lib_IntVector_Intrinsics_vec128_add64(a03, 199 Lib_IntVector_Intrinsics_vec128_mul64(r252, a3)); 200 Lib_IntVector_Intrinsics_vec128 201 a14 = 202 Lib_IntVector_Intrinsics_vec128_add64(a13, 203 Lib_IntVector_Intrinsics_vec128_mul64(r253, a3)); 204 Lib_IntVector_Intrinsics_vec128 205 a24 = 206 Lib_IntVector_Intrinsics_vec128_add64(a23, 207 Lib_IntVector_Intrinsics_vec128_mul64(r254, a3)); 208 Lib_IntVector_Intrinsics_vec128 209 a34 = 210 Lib_IntVector_Intrinsics_vec128_add64(a33, 211 Lib_IntVector_Intrinsics_vec128_mul64(r201, a3)); 212 Lib_IntVector_Intrinsics_vec128 213 a44 = 214 Lib_IntVector_Intrinsics_vec128_add64(a43, 215 Lib_IntVector_Intrinsics_vec128_mul64(r211, a3)); 216 Lib_IntVector_Intrinsics_vec128 217 a05 = 218 Lib_IntVector_Intrinsics_vec128_add64(a04, 219 Lib_IntVector_Intrinsics_vec128_mul64(r251, a4)); 220 Lib_IntVector_Intrinsics_vec128 221 a15 = 222 Lib_IntVector_Intrinsics_vec128_add64(a14, 223 Lib_IntVector_Intrinsics_vec128_mul64(r252, a4)); 224 Lib_IntVector_Intrinsics_vec128 225 a25 = 226 Lib_IntVector_Intrinsics_vec128_add64(a24, 227 Lib_IntVector_Intrinsics_vec128_mul64(r253, a4)); 228 Lib_IntVector_Intrinsics_vec128 229 a35 = 230 Lib_IntVector_Intrinsics_vec128_add64(a34, 231 Lib_IntVector_Intrinsics_vec128_mul64(r254, a4)); 232 Lib_IntVector_Intrinsics_vec128 233 a45 = 234 Lib_IntVector_Intrinsics_vec128_add64(a44, 235 Lib_IntVector_Intrinsics_vec128_mul64(r201, a4)); 236 Lib_IntVector_Intrinsics_vec128 t0 = a05; 237 Lib_IntVector_Intrinsics_vec128 t1 = a15; 238 Lib_IntVector_Intrinsics_vec128 t2 = a25; 239 Lib_IntVector_Intrinsics_vec128 t3 = a35; 240 Lib_IntVector_Intrinsics_vec128 t4 = a45; 241 Lib_IntVector_Intrinsics_vec128 242 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 243 Lib_IntVector_Intrinsics_vec128 244 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); 245 Lib_IntVector_Intrinsics_vec128 246 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 247 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); 248 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 249 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 250 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 251 Lib_IntVector_Intrinsics_vec128 252 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 253 Lib_IntVector_Intrinsics_vec128 254 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 255 Lib_IntVector_Intrinsics_vec128 256 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 257 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 258 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 259 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 260 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 261 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 262 Lib_IntVector_Intrinsics_vec128 263 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 264 Lib_IntVector_Intrinsics_vec128 265 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 266 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 267 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 268 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 269 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 270 Lib_IntVector_Intrinsics_vec128 271 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 272 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 273 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 274 Lib_IntVector_Intrinsics_vec128 o0 = x02; 275 Lib_IntVector_Intrinsics_vec128 o10 = x12; 276 Lib_IntVector_Intrinsics_vec128 o20 = x21; 277 Lib_IntVector_Intrinsics_vec128 o30 = x32; 278 Lib_IntVector_Intrinsics_vec128 o40 = x42; 279 Lib_IntVector_Intrinsics_vec128 280 o01 = 281 Lib_IntVector_Intrinsics_vec128_add64(o0, 282 Lib_IntVector_Intrinsics_vec128_interleave_high64(o0, o0)); 283 Lib_IntVector_Intrinsics_vec128 284 o11 = 285 Lib_IntVector_Intrinsics_vec128_add64(o10, 286 Lib_IntVector_Intrinsics_vec128_interleave_high64(o10, o10)); 287 Lib_IntVector_Intrinsics_vec128 288 o21 = 289 Lib_IntVector_Intrinsics_vec128_add64(o20, 290 Lib_IntVector_Intrinsics_vec128_interleave_high64(o20, o20)); 291 Lib_IntVector_Intrinsics_vec128 292 o31 = 293 Lib_IntVector_Intrinsics_vec128_add64(o30, 294 Lib_IntVector_Intrinsics_vec128_interleave_high64(o30, o30)); 295 Lib_IntVector_Intrinsics_vec128 296 o41 = 297 Lib_IntVector_Intrinsics_vec128_add64(o40, 298 Lib_IntVector_Intrinsics_vec128_interleave_high64(o40, o40)); 299 Lib_IntVector_Intrinsics_vec128 300 l = Lib_IntVector_Intrinsics_vec128_add64(o01, Lib_IntVector_Intrinsics_vec128_zero); 301 Lib_IntVector_Intrinsics_vec128 302 tmp0 = 303 Lib_IntVector_Intrinsics_vec128_and(l, 304 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 305 Lib_IntVector_Intrinsics_vec128 306 c0 = Lib_IntVector_Intrinsics_vec128_shift_right64(l, (uint32_t)26U); 307 Lib_IntVector_Intrinsics_vec128 l0 = Lib_IntVector_Intrinsics_vec128_add64(o11, c0); 308 Lib_IntVector_Intrinsics_vec128 309 tmp1 = 310 Lib_IntVector_Intrinsics_vec128_and(l0, 311 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 312 Lib_IntVector_Intrinsics_vec128 313 c1 = Lib_IntVector_Intrinsics_vec128_shift_right64(l0, (uint32_t)26U); 314 Lib_IntVector_Intrinsics_vec128 l1 = Lib_IntVector_Intrinsics_vec128_add64(o21, c1); 315 Lib_IntVector_Intrinsics_vec128 316 tmp2 = 317 Lib_IntVector_Intrinsics_vec128_and(l1, 318 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 319 Lib_IntVector_Intrinsics_vec128 320 c2 = Lib_IntVector_Intrinsics_vec128_shift_right64(l1, (uint32_t)26U); 321 Lib_IntVector_Intrinsics_vec128 l2 = Lib_IntVector_Intrinsics_vec128_add64(o31, c2); 322 Lib_IntVector_Intrinsics_vec128 323 tmp3 = 324 Lib_IntVector_Intrinsics_vec128_and(l2, 325 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 326 Lib_IntVector_Intrinsics_vec128 327 c3 = Lib_IntVector_Intrinsics_vec128_shift_right64(l2, (uint32_t)26U); 328 Lib_IntVector_Intrinsics_vec128 l3 = Lib_IntVector_Intrinsics_vec128_add64(o41, c3); 329 Lib_IntVector_Intrinsics_vec128 330 tmp4 = 331 Lib_IntVector_Intrinsics_vec128_and(l3, 332 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 333 Lib_IntVector_Intrinsics_vec128 334 c4 = Lib_IntVector_Intrinsics_vec128_shift_right64(l3, (uint32_t)26U); 335 Lib_IntVector_Intrinsics_vec128 336 o00 = 337 Lib_IntVector_Intrinsics_vec128_add64(tmp0, 338 Lib_IntVector_Intrinsics_vec128_smul64(c4, (uint64_t)5U)); 339 Lib_IntVector_Intrinsics_vec128 o1 = tmp1; 340 Lib_IntVector_Intrinsics_vec128 o2 = tmp2; 341 Lib_IntVector_Intrinsics_vec128 o3 = tmp3; 342 Lib_IntVector_Intrinsics_vec128 o4 = tmp4; 343 out[0U] = o00; 344 out[1U] = o1; 345 out[2U] = o2; 346 out[3U] = o3; 347 out[4U] = o4; 348 } 349 350 void 351 Hacl_Poly1305_128_poly1305_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key) 352 { 353 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 354 Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; 355 uint8_t *kr = key; 356 acc[0U] = Lib_IntVector_Intrinsics_vec128_zero; 357 acc[1U] = Lib_IntVector_Intrinsics_vec128_zero; 358 acc[2U] = Lib_IntVector_Intrinsics_vec128_zero; 359 acc[3U] = Lib_IntVector_Intrinsics_vec128_zero; 360 acc[4U] = Lib_IntVector_Intrinsics_vec128_zero; 361 uint64_t u0 = load64_le(kr); 362 uint64_t lo = u0; 363 uint64_t u = load64_le(kr + (uint32_t)8U); 364 uint64_t hi = u; 365 uint64_t mask0 = (uint64_t)0x0ffffffc0fffffffU; 366 uint64_t mask1 = (uint64_t)0x0ffffffc0ffffffcU; 367 uint64_t lo1 = lo & mask0; 368 uint64_t hi1 = hi & mask1; 369 Lib_IntVector_Intrinsics_vec128 *r = pre; 370 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 371 Lib_IntVector_Intrinsics_vec128 *rn = pre + (uint32_t)10U; 372 Lib_IntVector_Intrinsics_vec128 *rn_5 = pre + (uint32_t)15U; 373 Lib_IntVector_Intrinsics_vec128 r_vec0 = Lib_IntVector_Intrinsics_vec128_load64(lo1); 374 Lib_IntVector_Intrinsics_vec128 r_vec1 = Lib_IntVector_Intrinsics_vec128_load64(hi1); 375 Lib_IntVector_Intrinsics_vec128 376 f00 = 377 Lib_IntVector_Intrinsics_vec128_and(r_vec0, 378 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 379 Lib_IntVector_Intrinsics_vec128 380 f15 = 381 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec0, 382 (uint32_t)26U), 383 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 384 Lib_IntVector_Intrinsics_vec128 385 f20 = 386 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec0, 387 (uint32_t)52U), 388 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(r_vec1, 389 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 390 (uint32_t)12U)); 391 Lib_IntVector_Intrinsics_vec128 392 f30 = 393 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec1, 394 (uint32_t)14U), 395 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 396 Lib_IntVector_Intrinsics_vec128 397 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec1, (uint32_t)40U); 398 Lib_IntVector_Intrinsics_vec128 f0 = f00; 399 Lib_IntVector_Intrinsics_vec128 f1 = f15; 400 Lib_IntVector_Intrinsics_vec128 f2 = f20; 401 Lib_IntVector_Intrinsics_vec128 f3 = f30; 402 Lib_IntVector_Intrinsics_vec128 f4 = f40; 403 r[0U] = f0; 404 r[1U] = f1; 405 r[2U] = f2; 406 r[3U] = f3; 407 r[4U] = f4; 408 Lib_IntVector_Intrinsics_vec128 f200 = r[0U]; 409 Lib_IntVector_Intrinsics_vec128 f210 = r[1U]; 410 Lib_IntVector_Intrinsics_vec128 f220 = r[2U]; 411 Lib_IntVector_Intrinsics_vec128 f230 = r[3U]; 412 Lib_IntVector_Intrinsics_vec128 f240 = r[4U]; 413 r5[0U] = Lib_IntVector_Intrinsics_vec128_smul64(f200, (uint64_t)5U); 414 r5[1U] = Lib_IntVector_Intrinsics_vec128_smul64(f210, (uint64_t)5U); 415 r5[2U] = Lib_IntVector_Intrinsics_vec128_smul64(f220, (uint64_t)5U); 416 r5[3U] = Lib_IntVector_Intrinsics_vec128_smul64(f230, (uint64_t)5U); 417 r5[4U] = Lib_IntVector_Intrinsics_vec128_smul64(f240, (uint64_t)5U); 418 Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; 419 Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; 420 Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; 421 Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; 422 Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; 423 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 424 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 425 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 426 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 427 Lib_IntVector_Intrinsics_vec128 f10 = r[0U]; 428 Lib_IntVector_Intrinsics_vec128 f11 = r[1U]; 429 Lib_IntVector_Intrinsics_vec128 f12 = r[2U]; 430 Lib_IntVector_Intrinsics_vec128 f13 = r[3U]; 431 Lib_IntVector_Intrinsics_vec128 f14 = r[4U]; 432 Lib_IntVector_Intrinsics_vec128 a0 = Lib_IntVector_Intrinsics_vec128_mul64(r0, f10); 433 Lib_IntVector_Intrinsics_vec128 a1 = Lib_IntVector_Intrinsics_vec128_mul64(r1, f10); 434 Lib_IntVector_Intrinsics_vec128 a2 = Lib_IntVector_Intrinsics_vec128_mul64(r2, f10); 435 Lib_IntVector_Intrinsics_vec128 a3 = Lib_IntVector_Intrinsics_vec128_mul64(r3, f10); 436 Lib_IntVector_Intrinsics_vec128 a4 = Lib_IntVector_Intrinsics_vec128_mul64(r4, f10); 437 Lib_IntVector_Intrinsics_vec128 438 a01 = 439 Lib_IntVector_Intrinsics_vec128_add64(a0, 440 Lib_IntVector_Intrinsics_vec128_mul64(r54, f11)); 441 Lib_IntVector_Intrinsics_vec128 442 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, Lib_IntVector_Intrinsics_vec128_mul64(r0, f11)); 443 Lib_IntVector_Intrinsics_vec128 444 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, Lib_IntVector_Intrinsics_vec128_mul64(r1, f11)); 445 Lib_IntVector_Intrinsics_vec128 446 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, Lib_IntVector_Intrinsics_vec128_mul64(r2, f11)); 447 Lib_IntVector_Intrinsics_vec128 448 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, Lib_IntVector_Intrinsics_vec128_mul64(r3, f11)); 449 Lib_IntVector_Intrinsics_vec128 450 a02 = 451 Lib_IntVector_Intrinsics_vec128_add64(a01, 452 Lib_IntVector_Intrinsics_vec128_mul64(r53, f12)); 453 Lib_IntVector_Intrinsics_vec128 454 a12 = 455 Lib_IntVector_Intrinsics_vec128_add64(a11, 456 Lib_IntVector_Intrinsics_vec128_mul64(r54, f12)); 457 Lib_IntVector_Intrinsics_vec128 458 a22 = 459 Lib_IntVector_Intrinsics_vec128_add64(a21, 460 Lib_IntVector_Intrinsics_vec128_mul64(r0, f12)); 461 Lib_IntVector_Intrinsics_vec128 462 a32 = 463 Lib_IntVector_Intrinsics_vec128_add64(a31, 464 Lib_IntVector_Intrinsics_vec128_mul64(r1, f12)); 465 Lib_IntVector_Intrinsics_vec128 466 a42 = 467 Lib_IntVector_Intrinsics_vec128_add64(a41, 468 Lib_IntVector_Intrinsics_vec128_mul64(r2, f12)); 469 Lib_IntVector_Intrinsics_vec128 470 a03 = 471 Lib_IntVector_Intrinsics_vec128_add64(a02, 472 Lib_IntVector_Intrinsics_vec128_mul64(r52, f13)); 473 Lib_IntVector_Intrinsics_vec128 474 a13 = 475 Lib_IntVector_Intrinsics_vec128_add64(a12, 476 Lib_IntVector_Intrinsics_vec128_mul64(r53, f13)); 477 Lib_IntVector_Intrinsics_vec128 478 a23 = 479 Lib_IntVector_Intrinsics_vec128_add64(a22, 480 Lib_IntVector_Intrinsics_vec128_mul64(r54, f13)); 481 Lib_IntVector_Intrinsics_vec128 482 a33 = 483 Lib_IntVector_Intrinsics_vec128_add64(a32, 484 Lib_IntVector_Intrinsics_vec128_mul64(r0, f13)); 485 Lib_IntVector_Intrinsics_vec128 486 a43 = 487 Lib_IntVector_Intrinsics_vec128_add64(a42, 488 Lib_IntVector_Intrinsics_vec128_mul64(r1, f13)); 489 Lib_IntVector_Intrinsics_vec128 490 a04 = 491 Lib_IntVector_Intrinsics_vec128_add64(a03, 492 Lib_IntVector_Intrinsics_vec128_mul64(r51, f14)); 493 Lib_IntVector_Intrinsics_vec128 494 a14 = 495 Lib_IntVector_Intrinsics_vec128_add64(a13, 496 Lib_IntVector_Intrinsics_vec128_mul64(r52, f14)); 497 Lib_IntVector_Intrinsics_vec128 498 a24 = 499 Lib_IntVector_Intrinsics_vec128_add64(a23, 500 Lib_IntVector_Intrinsics_vec128_mul64(r53, f14)); 501 Lib_IntVector_Intrinsics_vec128 502 a34 = 503 Lib_IntVector_Intrinsics_vec128_add64(a33, 504 Lib_IntVector_Intrinsics_vec128_mul64(r54, f14)); 505 Lib_IntVector_Intrinsics_vec128 506 a44 = 507 Lib_IntVector_Intrinsics_vec128_add64(a43, 508 Lib_IntVector_Intrinsics_vec128_mul64(r0, f14)); 509 Lib_IntVector_Intrinsics_vec128 t0 = a04; 510 Lib_IntVector_Intrinsics_vec128 t1 = a14; 511 Lib_IntVector_Intrinsics_vec128 t2 = a24; 512 Lib_IntVector_Intrinsics_vec128 t3 = a34; 513 Lib_IntVector_Intrinsics_vec128 t4 = a44; 514 Lib_IntVector_Intrinsics_vec128 515 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 516 Lib_IntVector_Intrinsics_vec128 517 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); 518 Lib_IntVector_Intrinsics_vec128 519 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 520 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); 521 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 522 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 523 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 524 Lib_IntVector_Intrinsics_vec128 525 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 526 Lib_IntVector_Intrinsics_vec128 527 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 528 Lib_IntVector_Intrinsics_vec128 529 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 530 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 531 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 532 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 533 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 534 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 535 Lib_IntVector_Intrinsics_vec128 536 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 537 Lib_IntVector_Intrinsics_vec128 538 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 539 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 540 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 541 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 542 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 543 Lib_IntVector_Intrinsics_vec128 544 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 545 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 546 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 547 Lib_IntVector_Intrinsics_vec128 o0 = x02; 548 Lib_IntVector_Intrinsics_vec128 o1 = x12; 549 Lib_IntVector_Intrinsics_vec128 o2 = x21; 550 Lib_IntVector_Intrinsics_vec128 o3 = x32; 551 Lib_IntVector_Intrinsics_vec128 o4 = x42; 552 rn[0U] = o0; 553 rn[1U] = o1; 554 rn[2U] = o2; 555 rn[3U] = o3; 556 rn[4U] = o4; 557 Lib_IntVector_Intrinsics_vec128 f201 = rn[0U]; 558 Lib_IntVector_Intrinsics_vec128 f21 = rn[1U]; 559 Lib_IntVector_Intrinsics_vec128 f22 = rn[2U]; 560 Lib_IntVector_Intrinsics_vec128 f23 = rn[3U]; 561 Lib_IntVector_Intrinsics_vec128 f24 = rn[4U]; 562 rn_5[0U] = Lib_IntVector_Intrinsics_vec128_smul64(f201, (uint64_t)5U); 563 rn_5[1U] = Lib_IntVector_Intrinsics_vec128_smul64(f21, (uint64_t)5U); 564 rn_5[2U] = Lib_IntVector_Intrinsics_vec128_smul64(f22, (uint64_t)5U); 565 rn_5[3U] = Lib_IntVector_Intrinsics_vec128_smul64(f23, (uint64_t)5U); 566 rn_5[4U] = Lib_IntVector_Intrinsics_vec128_smul64(f24, (uint64_t)5U); 567 } 568 569 void 570 Hacl_Poly1305_128_poly1305_update1(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *text) 571 { 572 Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; 573 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 574 KRML_PRE_ALIGN(16) 575 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 576 uint64_t u0 = load64_le(text); 577 uint64_t lo = u0; 578 uint64_t u = load64_le(text + (uint32_t)8U); 579 uint64_t hi = u; 580 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 581 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 582 Lib_IntVector_Intrinsics_vec128 583 f010 = 584 Lib_IntVector_Intrinsics_vec128_and(f0, 585 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 586 Lib_IntVector_Intrinsics_vec128 587 f110 = 588 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 589 (uint32_t)26U), 590 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 591 Lib_IntVector_Intrinsics_vec128 592 f20 = 593 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 594 (uint32_t)52U), 595 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 596 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 597 (uint32_t)12U)); 598 Lib_IntVector_Intrinsics_vec128 599 f30 = 600 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 601 (uint32_t)14U), 602 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 603 Lib_IntVector_Intrinsics_vec128 604 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 605 Lib_IntVector_Intrinsics_vec128 f01 = f010; 606 Lib_IntVector_Intrinsics_vec128 f111 = f110; 607 Lib_IntVector_Intrinsics_vec128 f2 = f20; 608 Lib_IntVector_Intrinsics_vec128 f3 = f30; 609 Lib_IntVector_Intrinsics_vec128 f41 = f40; 610 e[0U] = f01; 611 e[1U] = f111; 612 e[2U] = f2; 613 e[3U] = f3; 614 e[4U] = f41; 615 uint64_t b = (uint64_t)0x1000000U; 616 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 617 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 618 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 619 Lib_IntVector_Intrinsics_vec128 *r = pre; 620 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 621 Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; 622 Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; 623 Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; 624 Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; 625 Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; 626 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 627 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 628 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 629 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 630 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 631 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 632 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 633 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 634 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 635 Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; 636 Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; 637 Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; 638 Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; 639 Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; 640 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 641 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 642 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 643 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 644 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 645 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 646 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); 647 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 648 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 649 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 650 Lib_IntVector_Intrinsics_vec128 651 a03 = 652 Lib_IntVector_Intrinsics_vec128_add64(a02, 653 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 654 Lib_IntVector_Intrinsics_vec128 655 a13 = 656 Lib_IntVector_Intrinsics_vec128_add64(a12, 657 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 658 Lib_IntVector_Intrinsics_vec128 659 a23 = 660 Lib_IntVector_Intrinsics_vec128_add64(a22, 661 Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); 662 Lib_IntVector_Intrinsics_vec128 663 a33 = 664 Lib_IntVector_Intrinsics_vec128_add64(a32, 665 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 666 Lib_IntVector_Intrinsics_vec128 667 a43 = 668 Lib_IntVector_Intrinsics_vec128_add64(a42, 669 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 670 Lib_IntVector_Intrinsics_vec128 671 a04 = 672 Lib_IntVector_Intrinsics_vec128_add64(a03, 673 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 674 Lib_IntVector_Intrinsics_vec128 675 a14 = 676 Lib_IntVector_Intrinsics_vec128_add64(a13, 677 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 678 Lib_IntVector_Intrinsics_vec128 679 a24 = 680 Lib_IntVector_Intrinsics_vec128_add64(a23, 681 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 682 Lib_IntVector_Intrinsics_vec128 683 a34 = 684 Lib_IntVector_Intrinsics_vec128_add64(a33, 685 Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); 686 Lib_IntVector_Intrinsics_vec128 687 a44 = 688 Lib_IntVector_Intrinsics_vec128_add64(a43, 689 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 690 Lib_IntVector_Intrinsics_vec128 691 a05 = 692 Lib_IntVector_Intrinsics_vec128_add64(a04, 693 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 694 Lib_IntVector_Intrinsics_vec128 695 a15 = 696 Lib_IntVector_Intrinsics_vec128_add64(a14, 697 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 698 Lib_IntVector_Intrinsics_vec128 699 a25 = 700 Lib_IntVector_Intrinsics_vec128_add64(a24, 701 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 702 Lib_IntVector_Intrinsics_vec128 703 a35 = 704 Lib_IntVector_Intrinsics_vec128_add64(a34, 705 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 706 Lib_IntVector_Intrinsics_vec128 707 a45 = 708 Lib_IntVector_Intrinsics_vec128_add64(a44, 709 Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); 710 Lib_IntVector_Intrinsics_vec128 711 a06 = 712 Lib_IntVector_Intrinsics_vec128_add64(a05, 713 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 714 Lib_IntVector_Intrinsics_vec128 715 a16 = 716 Lib_IntVector_Intrinsics_vec128_add64(a15, 717 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 718 Lib_IntVector_Intrinsics_vec128 719 a26 = 720 Lib_IntVector_Intrinsics_vec128_add64(a25, 721 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 722 Lib_IntVector_Intrinsics_vec128 723 a36 = 724 Lib_IntVector_Intrinsics_vec128_add64(a35, 725 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 726 Lib_IntVector_Intrinsics_vec128 727 a46 = 728 Lib_IntVector_Intrinsics_vec128_add64(a45, 729 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 730 Lib_IntVector_Intrinsics_vec128 t0 = a06; 731 Lib_IntVector_Intrinsics_vec128 t1 = a16; 732 Lib_IntVector_Intrinsics_vec128 t2 = a26; 733 Lib_IntVector_Intrinsics_vec128 t3 = a36; 734 Lib_IntVector_Intrinsics_vec128 t4 = a46; 735 Lib_IntVector_Intrinsics_vec128 736 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 737 Lib_IntVector_Intrinsics_vec128 738 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); 739 Lib_IntVector_Intrinsics_vec128 740 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 741 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); 742 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 743 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 744 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 745 Lib_IntVector_Intrinsics_vec128 746 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 747 Lib_IntVector_Intrinsics_vec128 748 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 749 Lib_IntVector_Intrinsics_vec128 750 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 751 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 752 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 753 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 754 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 755 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 756 Lib_IntVector_Intrinsics_vec128 757 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 758 Lib_IntVector_Intrinsics_vec128 759 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 760 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 761 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 762 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 763 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 764 Lib_IntVector_Intrinsics_vec128 765 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 766 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 767 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 768 Lib_IntVector_Intrinsics_vec128 o0 = x02; 769 Lib_IntVector_Intrinsics_vec128 o1 = x12; 770 Lib_IntVector_Intrinsics_vec128 o2 = x21; 771 Lib_IntVector_Intrinsics_vec128 o3 = x32; 772 Lib_IntVector_Intrinsics_vec128 o4 = x42; 773 acc[0U] = o0; 774 acc[1U] = o1; 775 acc[2U] = o2; 776 acc[3U] = o3; 777 acc[4U] = o4; 778 } 779 780 void 781 Hacl_Poly1305_128_poly1305_update( 782 Lib_IntVector_Intrinsics_vec128 *ctx, 783 uint32_t len, 784 uint8_t *text) 785 { 786 Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; 787 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 788 uint32_t sz_block = (uint32_t)32U; 789 uint32_t len0 = len / sz_block * sz_block; 790 uint8_t *t0 = text; 791 if (len0 > (uint32_t)0U) { 792 uint32_t bs = (uint32_t)32U; 793 uint8_t *text0 = t0; 794 Hacl_Impl_Poly1305_Field32xN_128_load_acc2(acc, text0); 795 uint32_t len1 = len0 - bs; 796 uint8_t *text1 = t0 + bs; 797 uint32_t nb = len1 / bs; 798 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 799 uint8_t *block = text1 + i * bs; 800 KRML_PRE_ALIGN(16) 801 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 802 Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(block); 803 Lib_IntVector_Intrinsics_vec128 804 b2 = Lib_IntVector_Intrinsics_vec128_load64_le(block + (uint32_t)16U); 805 Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2); 806 Lib_IntVector_Intrinsics_vec128 807 hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2); 808 Lib_IntVector_Intrinsics_vec128 809 f00 = 810 Lib_IntVector_Intrinsics_vec128_and(lo, 811 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 812 Lib_IntVector_Intrinsics_vec128 813 f15 = 814 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 815 (uint32_t)26U), 816 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 817 Lib_IntVector_Intrinsics_vec128 818 f25 = 819 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 820 (uint32_t)52U), 821 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(hi, 822 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 823 (uint32_t)12U)); 824 Lib_IntVector_Intrinsics_vec128 825 f30 = 826 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(hi, 827 (uint32_t)14U), 828 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 829 Lib_IntVector_Intrinsics_vec128 830 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(hi, (uint32_t)40U); 831 Lib_IntVector_Intrinsics_vec128 f0 = f00; 832 Lib_IntVector_Intrinsics_vec128 f1 = f15; 833 Lib_IntVector_Intrinsics_vec128 f2 = f25; 834 Lib_IntVector_Intrinsics_vec128 f3 = f30; 835 Lib_IntVector_Intrinsics_vec128 f41 = f40; 836 e[0U] = f0; 837 e[1U] = f1; 838 e[2U] = f2; 839 e[3U] = f3; 840 e[4U] = f41; 841 uint64_t b = (uint64_t)0x1000000U; 842 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 843 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 844 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 845 Lib_IntVector_Intrinsics_vec128 *rn = pre + (uint32_t)10U; 846 Lib_IntVector_Intrinsics_vec128 *rn5 = pre + (uint32_t)15U; 847 Lib_IntVector_Intrinsics_vec128 r0 = rn[0U]; 848 Lib_IntVector_Intrinsics_vec128 r1 = rn[1U]; 849 Lib_IntVector_Intrinsics_vec128 r2 = rn[2U]; 850 Lib_IntVector_Intrinsics_vec128 r3 = rn[3U]; 851 Lib_IntVector_Intrinsics_vec128 r4 = rn[4U]; 852 Lib_IntVector_Intrinsics_vec128 r51 = rn5[1U]; 853 Lib_IntVector_Intrinsics_vec128 r52 = rn5[2U]; 854 Lib_IntVector_Intrinsics_vec128 r53 = rn5[3U]; 855 Lib_IntVector_Intrinsics_vec128 r54 = rn5[4U]; 856 Lib_IntVector_Intrinsics_vec128 f10 = acc[0U]; 857 Lib_IntVector_Intrinsics_vec128 f110 = acc[1U]; 858 Lib_IntVector_Intrinsics_vec128 f120 = acc[2U]; 859 Lib_IntVector_Intrinsics_vec128 f130 = acc[3U]; 860 Lib_IntVector_Intrinsics_vec128 f140 = acc[4U]; 861 Lib_IntVector_Intrinsics_vec128 a0 = Lib_IntVector_Intrinsics_vec128_mul64(r0, f10); 862 Lib_IntVector_Intrinsics_vec128 a1 = Lib_IntVector_Intrinsics_vec128_mul64(r1, f10); 863 Lib_IntVector_Intrinsics_vec128 a2 = Lib_IntVector_Intrinsics_vec128_mul64(r2, f10); 864 Lib_IntVector_Intrinsics_vec128 a3 = Lib_IntVector_Intrinsics_vec128_mul64(r3, f10); 865 Lib_IntVector_Intrinsics_vec128 a4 = Lib_IntVector_Intrinsics_vec128_mul64(r4, f10); 866 Lib_IntVector_Intrinsics_vec128 867 a01 = 868 Lib_IntVector_Intrinsics_vec128_add64(a0, 869 Lib_IntVector_Intrinsics_vec128_mul64(r54, f110)); 870 Lib_IntVector_Intrinsics_vec128 871 a11 = 872 Lib_IntVector_Intrinsics_vec128_add64(a1, 873 Lib_IntVector_Intrinsics_vec128_mul64(r0, f110)); 874 Lib_IntVector_Intrinsics_vec128 875 a21 = 876 Lib_IntVector_Intrinsics_vec128_add64(a2, 877 Lib_IntVector_Intrinsics_vec128_mul64(r1, f110)); 878 Lib_IntVector_Intrinsics_vec128 879 a31 = 880 Lib_IntVector_Intrinsics_vec128_add64(a3, 881 Lib_IntVector_Intrinsics_vec128_mul64(r2, f110)); 882 Lib_IntVector_Intrinsics_vec128 883 a41 = 884 Lib_IntVector_Intrinsics_vec128_add64(a4, 885 Lib_IntVector_Intrinsics_vec128_mul64(r3, f110)); 886 Lib_IntVector_Intrinsics_vec128 887 a02 = 888 Lib_IntVector_Intrinsics_vec128_add64(a01, 889 Lib_IntVector_Intrinsics_vec128_mul64(r53, f120)); 890 Lib_IntVector_Intrinsics_vec128 891 a12 = 892 Lib_IntVector_Intrinsics_vec128_add64(a11, 893 Lib_IntVector_Intrinsics_vec128_mul64(r54, f120)); 894 Lib_IntVector_Intrinsics_vec128 895 a22 = 896 Lib_IntVector_Intrinsics_vec128_add64(a21, 897 Lib_IntVector_Intrinsics_vec128_mul64(r0, f120)); 898 Lib_IntVector_Intrinsics_vec128 899 a32 = 900 Lib_IntVector_Intrinsics_vec128_add64(a31, 901 Lib_IntVector_Intrinsics_vec128_mul64(r1, f120)); 902 Lib_IntVector_Intrinsics_vec128 903 a42 = 904 Lib_IntVector_Intrinsics_vec128_add64(a41, 905 Lib_IntVector_Intrinsics_vec128_mul64(r2, f120)); 906 Lib_IntVector_Intrinsics_vec128 907 a03 = 908 Lib_IntVector_Intrinsics_vec128_add64(a02, 909 Lib_IntVector_Intrinsics_vec128_mul64(r52, f130)); 910 Lib_IntVector_Intrinsics_vec128 911 a13 = 912 Lib_IntVector_Intrinsics_vec128_add64(a12, 913 Lib_IntVector_Intrinsics_vec128_mul64(r53, f130)); 914 Lib_IntVector_Intrinsics_vec128 915 a23 = 916 Lib_IntVector_Intrinsics_vec128_add64(a22, 917 Lib_IntVector_Intrinsics_vec128_mul64(r54, f130)); 918 Lib_IntVector_Intrinsics_vec128 919 a33 = 920 Lib_IntVector_Intrinsics_vec128_add64(a32, 921 Lib_IntVector_Intrinsics_vec128_mul64(r0, f130)); 922 Lib_IntVector_Intrinsics_vec128 923 a43 = 924 Lib_IntVector_Intrinsics_vec128_add64(a42, 925 Lib_IntVector_Intrinsics_vec128_mul64(r1, f130)); 926 Lib_IntVector_Intrinsics_vec128 927 a04 = 928 Lib_IntVector_Intrinsics_vec128_add64(a03, 929 Lib_IntVector_Intrinsics_vec128_mul64(r51, f140)); 930 Lib_IntVector_Intrinsics_vec128 931 a14 = 932 Lib_IntVector_Intrinsics_vec128_add64(a13, 933 Lib_IntVector_Intrinsics_vec128_mul64(r52, f140)); 934 Lib_IntVector_Intrinsics_vec128 935 a24 = 936 Lib_IntVector_Intrinsics_vec128_add64(a23, 937 Lib_IntVector_Intrinsics_vec128_mul64(r53, f140)); 938 Lib_IntVector_Intrinsics_vec128 939 a34 = 940 Lib_IntVector_Intrinsics_vec128_add64(a33, 941 Lib_IntVector_Intrinsics_vec128_mul64(r54, f140)); 942 Lib_IntVector_Intrinsics_vec128 943 a44 = 944 Lib_IntVector_Intrinsics_vec128_add64(a43, 945 Lib_IntVector_Intrinsics_vec128_mul64(r0, f140)); 946 Lib_IntVector_Intrinsics_vec128 t01 = a04; 947 Lib_IntVector_Intrinsics_vec128 t1 = a14; 948 Lib_IntVector_Intrinsics_vec128 t2 = a24; 949 Lib_IntVector_Intrinsics_vec128 t3 = a34; 950 Lib_IntVector_Intrinsics_vec128 t4 = a44; 951 Lib_IntVector_Intrinsics_vec128 952 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 953 Lib_IntVector_Intrinsics_vec128 954 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 955 Lib_IntVector_Intrinsics_vec128 956 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 957 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 958 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 959 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 960 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 961 Lib_IntVector_Intrinsics_vec128 962 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 963 Lib_IntVector_Intrinsics_vec128 964 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 965 Lib_IntVector_Intrinsics_vec128 966 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 967 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 968 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 969 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 970 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 971 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 972 Lib_IntVector_Intrinsics_vec128 973 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 974 Lib_IntVector_Intrinsics_vec128 975 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 976 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 977 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 978 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 979 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 980 Lib_IntVector_Intrinsics_vec128 981 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 982 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 983 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 984 Lib_IntVector_Intrinsics_vec128 o00 = x02; 985 Lib_IntVector_Intrinsics_vec128 o10 = x12; 986 Lib_IntVector_Intrinsics_vec128 o20 = x21; 987 Lib_IntVector_Intrinsics_vec128 o30 = x32; 988 Lib_IntVector_Intrinsics_vec128 o40 = x42; 989 acc[0U] = o00; 990 acc[1U] = o10; 991 acc[2U] = o20; 992 acc[3U] = o30; 993 acc[4U] = o40; 994 Lib_IntVector_Intrinsics_vec128 f100 = acc[0U]; 995 Lib_IntVector_Intrinsics_vec128 f11 = acc[1U]; 996 Lib_IntVector_Intrinsics_vec128 f12 = acc[2U]; 997 Lib_IntVector_Intrinsics_vec128 f13 = acc[3U]; 998 Lib_IntVector_Intrinsics_vec128 f14 = acc[4U]; 999 Lib_IntVector_Intrinsics_vec128 f20 = e[0U]; 1000 Lib_IntVector_Intrinsics_vec128 f21 = e[1U]; 1001 Lib_IntVector_Intrinsics_vec128 f22 = e[2U]; 1002 Lib_IntVector_Intrinsics_vec128 f23 = e[3U]; 1003 Lib_IntVector_Intrinsics_vec128 f24 = e[4U]; 1004 Lib_IntVector_Intrinsics_vec128 o0 = Lib_IntVector_Intrinsics_vec128_add64(f100, f20); 1005 Lib_IntVector_Intrinsics_vec128 o1 = Lib_IntVector_Intrinsics_vec128_add64(f11, f21); 1006 Lib_IntVector_Intrinsics_vec128 o2 = Lib_IntVector_Intrinsics_vec128_add64(f12, f22); 1007 Lib_IntVector_Intrinsics_vec128 o3 = Lib_IntVector_Intrinsics_vec128_add64(f13, f23); 1008 Lib_IntVector_Intrinsics_vec128 o4 = Lib_IntVector_Intrinsics_vec128_add64(f14, f24); 1009 acc[0U] = o0; 1010 acc[1U] = o1; 1011 acc[2U] = o2; 1012 acc[3U] = o3; 1013 acc[4U] = o4; 1014 } 1015 Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize(acc, pre); 1016 } 1017 uint32_t len1 = len - len0; 1018 uint8_t *t1 = text + len0; 1019 uint32_t nb = len1 / (uint32_t)16U; 1020 uint32_t rem = len1 % (uint32_t)16U; 1021 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 1022 uint8_t *block = t1 + i * (uint32_t)16U; 1023 KRML_PRE_ALIGN(16) 1024 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 1025 uint64_t u0 = load64_le(block); 1026 uint64_t lo = u0; 1027 uint64_t u = load64_le(block + (uint32_t)8U); 1028 uint64_t hi = u; 1029 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 1030 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 1031 Lib_IntVector_Intrinsics_vec128 1032 f010 = 1033 Lib_IntVector_Intrinsics_vec128_and(f0, 1034 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1035 Lib_IntVector_Intrinsics_vec128 1036 f110 = 1037 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 1038 (uint32_t)26U), 1039 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1040 Lib_IntVector_Intrinsics_vec128 1041 f20 = 1042 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 1043 (uint32_t)52U), 1044 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 1045 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 1046 (uint32_t)12U)); 1047 Lib_IntVector_Intrinsics_vec128 1048 f30 = 1049 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 1050 (uint32_t)14U), 1051 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1052 Lib_IntVector_Intrinsics_vec128 1053 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 1054 Lib_IntVector_Intrinsics_vec128 f01 = f010; 1055 Lib_IntVector_Intrinsics_vec128 f111 = f110; 1056 Lib_IntVector_Intrinsics_vec128 f2 = f20; 1057 Lib_IntVector_Intrinsics_vec128 f3 = f30; 1058 Lib_IntVector_Intrinsics_vec128 f41 = f40; 1059 e[0U] = f01; 1060 e[1U] = f111; 1061 e[2U] = f2; 1062 e[3U] = f3; 1063 e[4U] = f41; 1064 uint64_t b = (uint64_t)0x1000000U; 1065 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 1066 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 1067 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 1068 Lib_IntVector_Intrinsics_vec128 *r = pre; 1069 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 1070 Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; 1071 Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; 1072 Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; 1073 Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; 1074 Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; 1075 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 1076 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 1077 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 1078 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 1079 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 1080 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 1081 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 1082 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 1083 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 1084 Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; 1085 Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; 1086 Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; 1087 Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; 1088 Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; 1089 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 1090 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 1091 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 1092 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 1093 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 1094 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 1095 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); 1096 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 1097 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 1098 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 1099 Lib_IntVector_Intrinsics_vec128 1100 a03 = 1101 Lib_IntVector_Intrinsics_vec128_add64(a02, 1102 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 1103 Lib_IntVector_Intrinsics_vec128 1104 a13 = 1105 Lib_IntVector_Intrinsics_vec128_add64(a12, 1106 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 1107 Lib_IntVector_Intrinsics_vec128 1108 a23 = 1109 Lib_IntVector_Intrinsics_vec128_add64(a22, 1110 Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); 1111 Lib_IntVector_Intrinsics_vec128 1112 a33 = 1113 Lib_IntVector_Intrinsics_vec128_add64(a32, 1114 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 1115 Lib_IntVector_Intrinsics_vec128 1116 a43 = 1117 Lib_IntVector_Intrinsics_vec128_add64(a42, 1118 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 1119 Lib_IntVector_Intrinsics_vec128 1120 a04 = 1121 Lib_IntVector_Intrinsics_vec128_add64(a03, 1122 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 1123 Lib_IntVector_Intrinsics_vec128 1124 a14 = 1125 Lib_IntVector_Intrinsics_vec128_add64(a13, 1126 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 1127 Lib_IntVector_Intrinsics_vec128 1128 a24 = 1129 Lib_IntVector_Intrinsics_vec128_add64(a23, 1130 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 1131 Lib_IntVector_Intrinsics_vec128 1132 a34 = 1133 Lib_IntVector_Intrinsics_vec128_add64(a33, 1134 Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); 1135 Lib_IntVector_Intrinsics_vec128 1136 a44 = 1137 Lib_IntVector_Intrinsics_vec128_add64(a43, 1138 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 1139 Lib_IntVector_Intrinsics_vec128 1140 a05 = 1141 Lib_IntVector_Intrinsics_vec128_add64(a04, 1142 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 1143 Lib_IntVector_Intrinsics_vec128 1144 a15 = 1145 Lib_IntVector_Intrinsics_vec128_add64(a14, 1146 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 1147 Lib_IntVector_Intrinsics_vec128 1148 a25 = 1149 Lib_IntVector_Intrinsics_vec128_add64(a24, 1150 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 1151 Lib_IntVector_Intrinsics_vec128 1152 a35 = 1153 Lib_IntVector_Intrinsics_vec128_add64(a34, 1154 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 1155 Lib_IntVector_Intrinsics_vec128 1156 a45 = 1157 Lib_IntVector_Intrinsics_vec128_add64(a44, 1158 Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); 1159 Lib_IntVector_Intrinsics_vec128 1160 a06 = 1161 Lib_IntVector_Intrinsics_vec128_add64(a05, 1162 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 1163 Lib_IntVector_Intrinsics_vec128 1164 a16 = 1165 Lib_IntVector_Intrinsics_vec128_add64(a15, 1166 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 1167 Lib_IntVector_Intrinsics_vec128 1168 a26 = 1169 Lib_IntVector_Intrinsics_vec128_add64(a25, 1170 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 1171 Lib_IntVector_Intrinsics_vec128 1172 a36 = 1173 Lib_IntVector_Intrinsics_vec128_add64(a35, 1174 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 1175 Lib_IntVector_Intrinsics_vec128 1176 a46 = 1177 Lib_IntVector_Intrinsics_vec128_add64(a45, 1178 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 1179 Lib_IntVector_Intrinsics_vec128 t01 = a06; 1180 Lib_IntVector_Intrinsics_vec128 t11 = a16; 1181 Lib_IntVector_Intrinsics_vec128 t2 = a26; 1182 Lib_IntVector_Intrinsics_vec128 t3 = a36; 1183 Lib_IntVector_Intrinsics_vec128 t4 = a46; 1184 Lib_IntVector_Intrinsics_vec128 1185 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 1186 Lib_IntVector_Intrinsics_vec128 1187 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 1188 Lib_IntVector_Intrinsics_vec128 1189 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 1190 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 1191 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 1192 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); 1193 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 1194 Lib_IntVector_Intrinsics_vec128 1195 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 1196 Lib_IntVector_Intrinsics_vec128 1197 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 1198 Lib_IntVector_Intrinsics_vec128 1199 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 1200 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 1201 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 1202 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 1203 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 1204 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 1205 Lib_IntVector_Intrinsics_vec128 1206 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 1207 Lib_IntVector_Intrinsics_vec128 1208 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 1209 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 1210 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 1211 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 1212 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 1213 Lib_IntVector_Intrinsics_vec128 1214 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 1215 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 1216 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 1217 Lib_IntVector_Intrinsics_vec128 o0 = x02; 1218 Lib_IntVector_Intrinsics_vec128 o1 = x12; 1219 Lib_IntVector_Intrinsics_vec128 o2 = x21; 1220 Lib_IntVector_Intrinsics_vec128 o3 = x32; 1221 Lib_IntVector_Intrinsics_vec128 o4 = x42; 1222 acc[0U] = o0; 1223 acc[1U] = o1; 1224 acc[2U] = o2; 1225 acc[3U] = o3; 1226 acc[4U] = o4; 1227 } 1228 if (rem > (uint32_t)0U) { 1229 uint8_t *last = t1 + nb * (uint32_t)16U; 1230 KRML_PRE_ALIGN(16) 1231 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 1232 uint8_t tmp[16U] = { 0U }; 1233 memcpy(tmp, last, rem * sizeof(uint8_t)); 1234 uint64_t u0 = load64_le(tmp); 1235 uint64_t lo = u0; 1236 uint64_t u = load64_le(tmp + (uint32_t)8U); 1237 uint64_t hi = u; 1238 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 1239 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 1240 Lib_IntVector_Intrinsics_vec128 1241 f010 = 1242 Lib_IntVector_Intrinsics_vec128_and(f0, 1243 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1244 Lib_IntVector_Intrinsics_vec128 1245 f110 = 1246 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 1247 (uint32_t)26U), 1248 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1249 Lib_IntVector_Intrinsics_vec128 1250 f20 = 1251 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 1252 (uint32_t)52U), 1253 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 1254 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 1255 (uint32_t)12U)); 1256 Lib_IntVector_Intrinsics_vec128 1257 f30 = 1258 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 1259 (uint32_t)14U), 1260 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1261 Lib_IntVector_Intrinsics_vec128 1262 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 1263 Lib_IntVector_Intrinsics_vec128 f01 = f010; 1264 Lib_IntVector_Intrinsics_vec128 f111 = f110; 1265 Lib_IntVector_Intrinsics_vec128 f2 = f20; 1266 Lib_IntVector_Intrinsics_vec128 f3 = f30; 1267 Lib_IntVector_Intrinsics_vec128 f4 = f40; 1268 e[0U] = f01; 1269 e[1U] = f111; 1270 e[2U] = f2; 1271 e[3U] = f3; 1272 e[4U] = f4; 1273 uint64_t b = (uint64_t)1U << rem * (uint32_t)8U % (uint32_t)26U; 1274 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 1275 Lib_IntVector_Intrinsics_vec128 fi = e[rem * (uint32_t)8U / (uint32_t)26U]; 1276 e[rem * (uint32_t)8U / (uint32_t)26U] = Lib_IntVector_Intrinsics_vec128_or(fi, mask); 1277 Lib_IntVector_Intrinsics_vec128 *r = pre; 1278 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 1279 Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; 1280 Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; 1281 Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; 1282 Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; 1283 Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; 1284 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 1285 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 1286 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 1287 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 1288 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 1289 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 1290 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 1291 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 1292 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 1293 Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; 1294 Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; 1295 Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; 1296 Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; 1297 Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; 1298 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 1299 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 1300 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 1301 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 1302 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 1303 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 1304 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); 1305 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 1306 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 1307 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 1308 Lib_IntVector_Intrinsics_vec128 1309 a03 = 1310 Lib_IntVector_Intrinsics_vec128_add64(a02, 1311 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 1312 Lib_IntVector_Intrinsics_vec128 1313 a13 = 1314 Lib_IntVector_Intrinsics_vec128_add64(a12, 1315 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 1316 Lib_IntVector_Intrinsics_vec128 1317 a23 = 1318 Lib_IntVector_Intrinsics_vec128_add64(a22, 1319 Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); 1320 Lib_IntVector_Intrinsics_vec128 1321 a33 = 1322 Lib_IntVector_Intrinsics_vec128_add64(a32, 1323 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 1324 Lib_IntVector_Intrinsics_vec128 1325 a43 = 1326 Lib_IntVector_Intrinsics_vec128_add64(a42, 1327 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 1328 Lib_IntVector_Intrinsics_vec128 1329 a04 = 1330 Lib_IntVector_Intrinsics_vec128_add64(a03, 1331 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 1332 Lib_IntVector_Intrinsics_vec128 1333 a14 = 1334 Lib_IntVector_Intrinsics_vec128_add64(a13, 1335 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 1336 Lib_IntVector_Intrinsics_vec128 1337 a24 = 1338 Lib_IntVector_Intrinsics_vec128_add64(a23, 1339 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 1340 Lib_IntVector_Intrinsics_vec128 1341 a34 = 1342 Lib_IntVector_Intrinsics_vec128_add64(a33, 1343 Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); 1344 Lib_IntVector_Intrinsics_vec128 1345 a44 = 1346 Lib_IntVector_Intrinsics_vec128_add64(a43, 1347 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 1348 Lib_IntVector_Intrinsics_vec128 1349 a05 = 1350 Lib_IntVector_Intrinsics_vec128_add64(a04, 1351 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 1352 Lib_IntVector_Intrinsics_vec128 1353 a15 = 1354 Lib_IntVector_Intrinsics_vec128_add64(a14, 1355 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 1356 Lib_IntVector_Intrinsics_vec128 1357 a25 = 1358 Lib_IntVector_Intrinsics_vec128_add64(a24, 1359 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 1360 Lib_IntVector_Intrinsics_vec128 1361 a35 = 1362 Lib_IntVector_Intrinsics_vec128_add64(a34, 1363 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 1364 Lib_IntVector_Intrinsics_vec128 1365 a45 = 1366 Lib_IntVector_Intrinsics_vec128_add64(a44, 1367 Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); 1368 Lib_IntVector_Intrinsics_vec128 1369 a06 = 1370 Lib_IntVector_Intrinsics_vec128_add64(a05, 1371 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 1372 Lib_IntVector_Intrinsics_vec128 1373 a16 = 1374 Lib_IntVector_Intrinsics_vec128_add64(a15, 1375 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 1376 Lib_IntVector_Intrinsics_vec128 1377 a26 = 1378 Lib_IntVector_Intrinsics_vec128_add64(a25, 1379 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 1380 Lib_IntVector_Intrinsics_vec128 1381 a36 = 1382 Lib_IntVector_Intrinsics_vec128_add64(a35, 1383 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 1384 Lib_IntVector_Intrinsics_vec128 1385 a46 = 1386 Lib_IntVector_Intrinsics_vec128_add64(a45, 1387 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 1388 Lib_IntVector_Intrinsics_vec128 t01 = a06; 1389 Lib_IntVector_Intrinsics_vec128 t11 = a16; 1390 Lib_IntVector_Intrinsics_vec128 t2 = a26; 1391 Lib_IntVector_Intrinsics_vec128 t3 = a36; 1392 Lib_IntVector_Intrinsics_vec128 t4 = a46; 1393 Lib_IntVector_Intrinsics_vec128 1394 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 1395 Lib_IntVector_Intrinsics_vec128 1396 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 1397 Lib_IntVector_Intrinsics_vec128 1398 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 1399 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 1400 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 1401 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); 1402 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 1403 Lib_IntVector_Intrinsics_vec128 1404 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 1405 Lib_IntVector_Intrinsics_vec128 1406 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 1407 Lib_IntVector_Intrinsics_vec128 1408 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 1409 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 1410 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 1411 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 1412 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 1413 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 1414 Lib_IntVector_Intrinsics_vec128 1415 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 1416 Lib_IntVector_Intrinsics_vec128 1417 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 1418 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 1419 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 1420 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 1421 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 1422 Lib_IntVector_Intrinsics_vec128 1423 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 1424 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 1425 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 1426 Lib_IntVector_Intrinsics_vec128 o0 = x02; 1427 Lib_IntVector_Intrinsics_vec128 o1 = x12; 1428 Lib_IntVector_Intrinsics_vec128 o2 = x21; 1429 Lib_IntVector_Intrinsics_vec128 o3 = x32; 1430 Lib_IntVector_Intrinsics_vec128 o4 = x42; 1431 acc[0U] = o0; 1432 acc[1U] = o1; 1433 acc[2U] = o2; 1434 acc[3U] = o3; 1435 acc[4U] = o4; 1436 return; 1437 } 1438 } 1439 1440 void 1441 Hacl_Poly1305_128_poly1305_finish( 1442 uint8_t *tag, 1443 uint8_t *key, 1444 Lib_IntVector_Intrinsics_vec128 *ctx) 1445 { 1446 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 1447 uint8_t *ks = key + (uint32_t)16U; 1448 Lib_IntVector_Intrinsics_vec128 f0 = acc[0U]; 1449 Lib_IntVector_Intrinsics_vec128 f13 = acc[1U]; 1450 Lib_IntVector_Intrinsics_vec128 f23 = acc[2U]; 1451 Lib_IntVector_Intrinsics_vec128 f33 = acc[3U]; 1452 Lib_IntVector_Intrinsics_vec128 f40 = acc[4U]; 1453 Lib_IntVector_Intrinsics_vec128 1454 l0 = Lib_IntVector_Intrinsics_vec128_add64(f0, Lib_IntVector_Intrinsics_vec128_zero); 1455 Lib_IntVector_Intrinsics_vec128 1456 tmp00 = 1457 Lib_IntVector_Intrinsics_vec128_and(l0, 1458 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1459 Lib_IntVector_Intrinsics_vec128 1460 c00 = Lib_IntVector_Intrinsics_vec128_shift_right64(l0, (uint32_t)26U); 1461 Lib_IntVector_Intrinsics_vec128 l1 = Lib_IntVector_Intrinsics_vec128_add64(f13, c00); 1462 Lib_IntVector_Intrinsics_vec128 1463 tmp10 = 1464 Lib_IntVector_Intrinsics_vec128_and(l1, 1465 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1466 Lib_IntVector_Intrinsics_vec128 1467 c10 = Lib_IntVector_Intrinsics_vec128_shift_right64(l1, (uint32_t)26U); 1468 Lib_IntVector_Intrinsics_vec128 l2 = Lib_IntVector_Intrinsics_vec128_add64(f23, c10); 1469 Lib_IntVector_Intrinsics_vec128 1470 tmp20 = 1471 Lib_IntVector_Intrinsics_vec128_and(l2, 1472 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1473 Lib_IntVector_Intrinsics_vec128 1474 c20 = Lib_IntVector_Intrinsics_vec128_shift_right64(l2, (uint32_t)26U); 1475 Lib_IntVector_Intrinsics_vec128 l3 = Lib_IntVector_Intrinsics_vec128_add64(f33, c20); 1476 Lib_IntVector_Intrinsics_vec128 1477 tmp30 = 1478 Lib_IntVector_Intrinsics_vec128_and(l3, 1479 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1480 Lib_IntVector_Intrinsics_vec128 1481 c30 = Lib_IntVector_Intrinsics_vec128_shift_right64(l3, (uint32_t)26U); 1482 Lib_IntVector_Intrinsics_vec128 l4 = Lib_IntVector_Intrinsics_vec128_add64(f40, c30); 1483 Lib_IntVector_Intrinsics_vec128 1484 tmp40 = 1485 Lib_IntVector_Intrinsics_vec128_and(l4, 1486 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1487 Lib_IntVector_Intrinsics_vec128 1488 c40 = Lib_IntVector_Intrinsics_vec128_shift_right64(l4, (uint32_t)26U); 1489 Lib_IntVector_Intrinsics_vec128 1490 f010 = 1491 Lib_IntVector_Intrinsics_vec128_add64(tmp00, 1492 Lib_IntVector_Intrinsics_vec128_smul64(c40, (uint64_t)5U)); 1493 Lib_IntVector_Intrinsics_vec128 f110 = tmp10; 1494 Lib_IntVector_Intrinsics_vec128 f210 = tmp20; 1495 Lib_IntVector_Intrinsics_vec128 f310 = tmp30; 1496 Lib_IntVector_Intrinsics_vec128 f410 = tmp40; 1497 Lib_IntVector_Intrinsics_vec128 1498 l = Lib_IntVector_Intrinsics_vec128_add64(f010, Lib_IntVector_Intrinsics_vec128_zero); 1499 Lib_IntVector_Intrinsics_vec128 1500 tmp0 = 1501 Lib_IntVector_Intrinsics_vec128_and(l, 1502 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1503 Lib_IntVector_Intrinsics_vec128 1504 c0 = Lib_IntVector_Intrinsics_vec128_shift_right64(l, (uint32_t)26U); 1505 Lib_IntVector_Intrinsics_vec128 l5 = Lib_IntVector_Intrinsics_vec128_add64(f110, c0); 1506 Lib_IntVector_Intrinsics_vec128 1507 tmp1 = 1508 Lib_IntVector_Intrinsics_vec128_and(l5, 1509 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1510 Lib_IntVector_Intrinsics_vec128 1511 c1 = Lib_IntVector_Intrinsics_vec128_shift_right64(l5, (uint32_t)26U); 1512 Lib_IntVector_Intrinsics_vec128 l6 = Lib_IntVector_Intrinsics_vec128_add64(f210, c1); 1513 Lib_IntVector_Intrinsics_vec128 1514 tmp2 = 1515 Lib_IntVector_Intrinsics_vec128_and(l6, 1516 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1517 Lib_IntVector_Intrinsics_vec128 1518 c2 = Lib_IntVector_Intrinsics_vec128_shift_right64(l6, (uint32_t)26U); 1519 Lib_IntVector_Intrinsics_vec128 l7 = Lib_IntVector_Intrinsics_vec128_add64(f310, c2); 1520 Lib_IntVector_Intrinsics_vec128 1521 tmp3 = 1522 Lib_IntVector_Intrinsics_vec128_and(l7, 1523 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1524 Lib_IntVector_Intrinsics_vec128 1525 c3 = Lib_IntVector_Intrinsics_vec128_shift_right64(l7, (uint32_t)26U); 1526 Lib_IntVector_Intrinsics_vec128 l8 = Lib_IntVector_Intrinsics_vec128_add64(f410, c3); 1527 Lib_IntVector_Intrinsics_vec128 1528 tmp4 = 1529 Lib_IntVector_Intrinsics_vec128_and(l8, 1530 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 1531 Lib_IntVector_Intrinsics_vec128 1532 c4 = Lib_IntVector_Intrinsics_vec128_shift_right64(l8, (uint32_t)26U); 1533 Lib_IntVector_Intrinsics_vec128 1534 f02 = 1535 Lib_IntVector_Intrinsics_vec128_add64(tmp0, 1536 Lib_IntVector_Intrinsics_vec128_smul64(c4, (uint64_t)5U)); 1537 Lib_IntVector_Intrinsics_vec128 f12 = tmp1; 1538 Lib_IntVector_Intrinsics_vec128 f22 = tmp2; 1539 Lib_IntVector_Intrinsics_vec128 f32 = tmp3; 1540 Lib_IntVector_Intrinsics_vec128 f42 = tmp4; 1541 Lib_IntVector_Intrinsics_vec128 1542 mh = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 1543 Lib_IntVector_Intrinsics_vec128 1544 ml = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffffbU); 1545 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_eq64(f42, mh); 1546 Lib_IntVector_Intrinsics_vec128 1547 mask1 = 1548 Lib_IntVector_Intrinsics_vec128_and(mask, 1549 Lib_IntVector_Intrinsics_vec128_eq64(f32, mh)); 1550 Lib_IntVector_Intrinsics_vec128 1551 mask2 = 1552 Lib_IntVector_Intrinsics_vec128_and(mask1, 1553 Lib_IntVector_Intrinsics_vec128_eq64(f22, mh)); 1554 Lib_IntVector_Intrinsics_vec128 1555 mask3 = 1556 Lib_IntVector_Intrinsics_vec128_and(mask2, 1557 Lib_IntVector_Intrinsics_vec128_eq64(f12, mh)); 1558 Lib_IntVector_Intrinsics_vec128 1559 mask4 = 1560 Lib_IntVector_Intrinsics_vec128_and(mask3, 1561 Lib_IntVector_Intrinsics_vec128_lognot(Lib_IntVector_Intrinsics_vec128_gt64(ml, f02))); 1562 Lib_IntVector_Intrinsics_vec128 ph = Lib_IntVector_Intrinsics_vec128_and(mask4, mh); 1563 Lib_IntVector_Intrinsics_vec128 pl = Lib_IntVector_Intrinsics_vec128_and(mask4, ml); 1564 Lib_IntVector_Intrinsics_vec128 o0 = Lib_IntVector_Intrinsics_vec128_sub64(f02, pl); 1565 Lib_IntVector_Intrinsics_vec128 o1 = Lib_IntVector_Intrinsics_vec128_sub64(f12, ph); 1566 Lib_IntVector_Intrinsics_vec128 o2 = Lib_IntVector_Intrinsics_vec128_sub64(f22, ph); 1567 Lib_IntVector_Intrinsics_vec128 o3 = Lib_IntVector_Intrinsics_vec128_sub64(f32, ph); 1568 Lib_IntVector_Intrinsics_vec128 o4 = Lib_IntVector_Intrinsics_vec128_sub64(f42, ph); 1569 Lib_IntVector_Intrinsics_vec128 f011 = o0; 1570 Lib_IntVector_Intrinsics_vec128 f111 = o1; 1571 Lib_IntVector_Intrinsics_vec128 f211 = o2; 1572 Lib_IntVector_Intrinsics_vec128 f311 = o3; 1573 Lib_IntVector_Intrinsics_vec128 f411 = o4; 1574 acc[0U] = f011; 1575 acc[1U] = f111; 1576 acc[2U] = f211; 1577 acc[3U] = f311; 1578 acc[4U] = f411; 1579 Lib_IntVector_Intrinsics_vec128 f00 = acc[0U]; 1580 Lib_IntVector_Intrinsics_vec128 f1 = acc[1U]; 1581 Lib_IntVector_Intrinsics_vec128 f2 = acc[2U]; 1582 Lib_IntVector_Intrinsics_vec128 f3 = acc[3U]; 1583 Lib_IntVector_Intrinsics_vec128 f4 = acc[4U]; 1584 uint64_t f01 = Lib_IntVector_Intrinsics_vec128_extract64(f00, (uint32_t)0U); 1585 uint64_t f112 = Lib_IntVector_Intrinsics_vec128_extract64(f1, (uint32_t)0U); 1586 uint64_t f212 = Lib_IntVector_Intrinsics_vec128_extract64(f2, (uint32_t)0U); 1587 uint64_t f312 = Lib_IntVector_Intrinsics_vec128_extract64(f3, (uint32_t)0U); 1588 uint64_t f41 = Lib_IntVector_Intrinsics_vec128_extract64(f4, (uint32_t)0U); 1589 uint64_t lo = (f01 | f112 << (uint32_t)26U) | f212 << (uint32_t)52U; 1590 uint64_t hi = (f212 >> (uint32_t)12U | f312 << (uint32_t)14U) | f41 << (uint32_t)40U; 1591 uint64_t f10 = lo; 1592 uint64_t f11 = hi; 1593 uint64_t u0 = load64_le(ks); 1594 uint64_t lo0 = u0; 1595 uint64_t u = load64_le(ks + (uint32_t)8U); 1596 uint64_t hi0 = u; 1597 uint64_t f20 = lo0; 1598 uint64_t f21 = hi0; 1599 uint64_t r0 = f10 + f20; 1600 uint64_t r1 = f11 + f21; 1601 uint64_t c = (r0 ^ ((r0 ^ f20) | ((r0 - f20) ^ f20))) >> (uint32_t)63U; 1602 uint64_t r11 = r1 + c; 1603 uint64_t f30 = r0; 1604 uint64_t f31 = r11; 1605 store64_le(tag, f30); 1606 store64_le(tag + (uint32_t)8U, f31); 1607 } 1608 1609 void 1610 Hacl_Poly1305_128_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key) 1611 { 1612 KRML_PRE_ALIGN(16) 1613 Lib_IntVector_Intrinsics_vec128 ctx[25U] KRML_POST_ALIGN(16) = { 0U }; 1614 Hacl_Poly1305_128_poly1305_init(ctx, key); 1615 Hacl_Poly1305_128_poly1305_update(ctx, len, text); 1616 Hacl_Poly1305_128_poly1305_finish(tag, key, ctx); 1617 }