Hacl_Chacha20Poly1305_128.c (70201B)
1 /* MIT License 2 * 3 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation 4 * Copyright (c) 2022-2023 HACL* Contributors 5 * 6 * Permission is hereby granted, free of charge, to any person obtaining a copy 7 * of this software and associated documentation files (the "Software"), to deal 8 * in the Software without restriction, including without limitation the rights 9 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 10 * copies of the Software, and to permit persons to whom the Software is 11 * furnished to do so, subject to the following conditions: 12 * 13 * The above copyright notice and this permission notice shall be included in all 14 * copies or substantial portions of the Software. 15 * 16 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 21 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE 22 * SOFTWARE. 23 */ 24 25 #include "Hacl_Chacha20Poly1305_128.h" 26 27 #include "internal/Hacl_Poly1305_128.h" 28 #include "internal/Hacl_Krmllib.h" 29 #include "libintvector.h" 30 31 static inline void 32 poly1305_padded_128(Lib_IntVector_Intrinsics_vec128 *ctx, uint32_t len, uint8_t *text) 33 { 34 uint32_t n = len / (uint32_t)16U; 35 uint32_t r = len % (uint32_t)16U; 36 uint8_t *blocks = text; 37 uint8_t *rem = text + n * (uint32_t)16U; 38 Lib_IntVector_Intrinsics_vec128 *pre0 = ctx + (uint32_t)5U; 39 Lib_IntVector_Intrinsics_vec128 *acc0 = ctx; 40 uint32_t sz_block = (uint32_t)32U; 41 uint32_t len0 = n * (uint32_t)16U / sz_block * sz_block; 42 uint8_t *t00 = blocks; 43 if (len0 > (uint32_t)0U) { 44 uint32_t bs = (uint32_t)32U; 45 uint8_t *text0 = t00; 46 Hacl_Impl_Poly1305_Field32xN_128_load_acc2(acc0, text0); 47 uint32_t len1 = len0 - bs; 48 uint8_t *text1 = t00 + bs; 49 uint32_t nb = len1 / bs; 50 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 51 uint8_t *block = text1 + i * bs; 52 KRML_PRE_ALIGN(16) 53 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 54 Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(block); 55 Lib_IntVector_Intrinsics_vec128 56 b2 = Lib_IntVector_Intrinsics_vec128_load64_le(block + (uint32_t)16U); 57 Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2); 58 Lib_IntVector_Intrinsics_vec128 59 hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2); 60 Lib_IntVector_Intrinsics_vec128 61 f00 = 62 Lib_IntVector_Intrinsics_vec128_and(lo, 63 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 64 Lib_IntVector_Intrinsics_vec128 65 f15 = 66 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 67 (uint32_t)26U), 68 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 69 Lib_IntVector_Intrinsics_vec128 70 f25 = 71 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, 72 (uint32_t)52U), 73 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(hi, 74 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 75 (uint32_t)12U)); 76 Lib_IntVector_Intrinsics_vec128 77 f30 = 78 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(hi, 79 (uint32_t)14U), 80 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 81 Lib_IntVector_Intrinsics_vec128 82 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(hi, (uint32_t)40U); 83 Lib_IntVector_Intrinsics_vec128 f0 = f00; 84 Lib_IntVector_Intrinsics_vec128 f1 = f15; 85 Lib_IntVector_Intrinsics_vec128 f2 = f25; 86 Lib_IntVector_Intrinsics_vec128 f3 = f30; 87 Lib_IntVector_Intrinsics_vec128 f41 = f40; 88 e[0U] = f0; 89 e[1U] = f1; 90 e[2U] = f2; 91 e[3U] = f3; 92 e[4U] = f41; 93 uint64_t b = (uint64_t)0x1000000U; 94 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 95 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 96 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 97 Lib_IntVector_Intrinsics_vec128 *rn = pre0 + (uint32_t)10U; 98 Lib_IntVector_Intrinsics_vec128 *rn5 = pre0 + (uint32_t)15U; 99 Lib_IntVector_Intrinsics_vec128 r0 = rn[0U]; 100 Lib_IntVector_Intrinsics_vec128 r1 = rn[1U]; 101 Lib_IntVector_Intrinsics_vec128 r2 = rn[2U]; 102 Lib_IntVector_Intrinsics_vec128 r3 = rn[3U]; 103 Lib_IntVector_Intrinsics_vec128 r4 = rn[4U]; 104 Lib_IntVector_Intrinsics_vec128 r51 = rn5[1U]; 105 Lib_IntVector_Intrinsics_vec128 r52 = rn5[2U]; 106 Lib_IntVector_Intrinsics_vec128 r53 = rn5[3U]; 107 Lib_IntVector_Intrinsics_vec128 r54 = rn5[4U]; 108 Lib_IntVector_Intrinsics_vec128 f10 = acc0[0U]; 109 Lib_IntVector_Intrinsics_vec128 f110 = acc0[1U]; 110 Lib_IntVector_Intrinsics_vec128 f120 = acc0[2U]; 111 Lib_IntVector_Intrinsics_vec128 f130 = acc0[3U]; 112 Lib_IntVector_Intrinsics_vec128 f140 = acc0[4U]; 113 Lib_IntVector_Intrinsics_vec128 a0 = Lib_IntVector_Intrinsics_vec128_mul64(r0, f10); 114 Lib_IntVector_Intrinsics_vec128 a1 = Lib_IntVector_Intrinsics_vec128_mul64(r1, f10); 115 Lib_IntVector_Intrinsics_vec128 a2 = Lib_IntVector_Intrinsics_vec128_mul64(r2, f10); 116 Lib_IntVector_Intrinsics_vec128 a3 = Lib_IntVector_Intrinsics_vec128_mul64(r3, f10); 117 Lib_IntVector_Intrinsics_vec128 a4 = Lib_IntVector_Intrinsics_vec128_mul64(r4, f10); 118 Lib_IntVector_Intrinsics_vec128 119 a01 = 120 Lib_IntVector_Intrinsics_vec128_add64(a0, 121 Lib_IntVector_Intrinsics_vec128_mul64(r54, f110)); 122 Lib_IntVector_Intrinsics_vec128 123 a11 = 124 Lib_IntVector_Intrinsics_vec128_add64(a1, 125 Lib_IntVector_Intrinsics_vec128_mul64(r0, f110)); 126 Lib_IntVector_Intrinsics_vec128 127 a21 = 128 Lib_IntVector_Intrinsics_vec128_add64(a2, 129 Lib_IntVector_Intrinsics_vec128_mul64(r1, f110)); 130 Lib_IntVector_Intrinsics_vec128 131 a31 = 132 Lib_IntVector_Intrinsics_vec128_add64(a3, 133 Lib_IntVector_Intrinsics_vec128_mul64(r2, f110)); 134 Lib_IntVector_Intrinsics_vec128 135 a41 = 136 Lib_IntVector_Intrinsics_vec128_add64(a4, 137 Lib_IntVector_Intrinsics_vec128_mul64(r3, f110)); 138 Lib_IntVector_Intrinsics_vec128 139 a02 = 140 Lib_IntVector_Intrinsics_vec128_add64(a01, 141 Lib_IntVector_Intrinsics_vec128_mul64(r53, f120)); 142 Lib_IntVector_Intrinsics_vec128 143 a12 = 144 Lib_IntVector_Intrinsics_vec128_add64(a11, 145 Lib_IntVector_Intrinsics_vec128_mul64(r54, f120)); 146 Lib_IntVector_Intrinsics_vec128 147 a22 = 148 Lib_IntVector_Intrinsics_vec128_add64(a21, 149 Lib_IntVector_Intrinsics_vec128_mul64(r0, f120)); 150 Lib_IntVector_Intrinsics_vec128 151 a32 = 152 Lib_IntVector_Intrinsics_vec128_add64(a31, 153 Lib_IntVector_Intrinsics_vec128_mul64(r1, f120)); 154 Lib_IntVector_Intrinsics_vec128 155 a42 = 156 Lib_IntVector_Intrinsics_vec128_add64(a41, 157 Lib_IntVector_Intrinsics_vec128_mul64(r2, f120)); 158 Lib_IntVector_Intrinsics_vec128 159 a03 = 160 Lib_IntVector_Intrinsics_vec128_add64(a02, 161 Lib_IntVector_Intrinsics_vec128_mul64(r52, f130)); 162 Lib_IntVector_Intrinsics_vec128 163 a13 = 164 Lib_IntVector_Intrinsics_vec128_add64(a12, 165 Lib_IntVector_Intrinsics_vec128_mul64(r53, f130)); 166 Lib_IntVector_Intrinsics_vec128 167 a23 = 168 Lib_IntVector_Intrinsics_vec128_add64(a22, 169 Lib_IntVector_Intrinsics_vec128_mul64(r54, f130)); 170 Lib_IntVector_Intrinsics_vec128 171 a33 = 172 Lib_IntVector_Intrinsics_vec128_add64(a32, 173 Lib_IntVector_Intrinsics_vec128_mul64(r0, f130)); 174 Lib_IntVector_Intrinsics_vec128 175 a43 = 176 Lib_IntVector_Intrinsics_vec128_add64(a42, 177 Lib_IntVector_Intrinsics_vec128_mul64(r1, f130)); 178 Lib_IntVector_Intrinsics_vec128 179 a04 = 180 Lib_IntVector_Intrinsics_vec128_add64(a03, 181 Lib_IntVector_Intrinsics_vec128_mul64(r51, f140)); 182 Lib_IntVector_Intrinsics_vec128 183 a14 = 184 Lib_IntVector_Intrinsics_vec128_add64(a13, 185 Lib_IntVector_Intrinsics_vec128_mul64(r52, f140)); 186 Lib_IntVector_Intrinsics_vec128 187 a24 = 188 Lib_IntVector_Intrinsics_vec128_add64(a23, 189 Lib_IntVector_Intrinsics_vec128_mul64(r53, f140)); 190 Lib_IntVector_Intrinsics_vec128 191 a34 = 192 Lib_IntVector_Intrinsics_vec128_add64(a33, 193 Lib_IntVector_Intrinsics_vec128_mul64(r54, f140)); 194 Lib_IntVector_Intrinsics_vec128 195 a44 = 196 Lib_IntVector_Intrinsics_vec128_add64(a43, 197 Lib_IntVector_Intrinsics_vec128_mul64(r0, f140)); 198 Lib_IntVector_Intrinsics_vec128 t01 = a04; 199 Lib_IntVector_Intrinsics_vec128 t1 = a14; 200 Lib_IntVector_Intrinsics_vec128 t2 = a24; 201 Lib_IntVector_Intrinsics_vec128 t3 = a34; 202 Lib_IntVector_Intrinsics_vec128 t4 = a44; 203 Lib_IntVector_Intrinsics_vec128 204 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 205 Lib_IntVector_Intrinsics_vec128 206 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 207 Lib_IntVector_Intrinsics_vec128 208 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 209 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 210 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 211 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 212 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 213 Lib_IntVector_Intrinsics_vec128 214 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 215 Lib_IntVector_Intrinsics_vec128 216 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 217 Lib_IntVector_Intrinsics_vec128 218 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 219 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 220 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 221 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 222 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 223 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 224 Lib_IntVector_Intrinsics_vec128 225 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 226 Lib_IntVector_Intrinsics_vec128 227 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 228 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 229 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 230 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 231 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 232 Lib_IntVector_Intrinsics_vec128 233 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 234 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 235 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 236 Lib_IntVector_Intrinsics_vec128 o00 = x02; 237 Lib_IntVector_Intrinsics_vec128 o10 = x12; 238 Lib_IntVector_Intrinsics_vec128 o20 = x21; 239 Lib_IntVector_Intrinsics_vec128 o30 = x32; 240 Lib_IntVector_Intrinsics_vec128 o40 = x42; 241 acc0[0U] = o00; 242 acc0[1U] = o10; 243 acc0[2U] = o20; 244 acc0[3U] = o30; 245 acc0[4U] = o40; 246 Lib_IntVector_Intrinsics_vec128 f100 = acc0[0U]; 247 Lib_IntVector_Intrinsics_vec128 f11 = acc0[1U]; 248 Lib_IntVector_Intrinsics_vec128 f12 = acc0[2U]; 249 Lib_IntVector_Intrinsics_vec128 f13 = acc0[3U]; 250 Lib_IntVector_Intrinsics_vec128 f14 = acc0[4U]; 251 Lib_IntVector_Intrinsics_vec128 f20 = e[0U]; 252 Lib_IntVector_Intrinsics_vec128 f21 = e[1U]; 253 Lib_IntVector_Intrinsics_vec128 f22 = e[2U]; 254 Lib_IntVector_Intrinsics_vec128 f23 = e[3U]; 255 Lib_IntVector_Intrinsics_vec128 f24 = e[4U]; 256 Lib_IntVector_Intrinsics_vec128 o0 = Lib_IntVector_Intrinsics_vec128_add64(f100, f20); 257 Lib_IntVector_Intrinsics_vec128 o1 = Lib_IntVector_Intrinsics_vec128_add64(f11, f21); 258 Lib_IntVector_Intrinsics_vec128 o2 = Lib_IntVector_Intrinsics_vec128_add64(f12, f22); 259 Lib_IntVector_Intrinsics_vec128 o3 = Lib_IntVector_Intrinsics_vec128_add64(f13, f23); 260 Lib_IntVector_Intrinsics_vec128 o4 = Lib_IntVector_Intrinsics_vec128_add64(f14, f24); 261 acc0[0U] = o0; 262 acc0[1U] = o1; 263 acc0[2U] = o2; 264 acc0[3U] = o3; 265 acc0[4U] = o4; 266 } 267 Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize(acc0, pre0); 268 } 269 uint32_t len1 = n * (uint32_t)16U - len0; 270 uint8_t *t10 = blocks + len0; 271 uint32_t nb = len1 / (uint32_t)16U; 272 uint32_t rem1 = len1 % (uint32_t)16U; 273 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 274 uint8_t *block = t10 + i * (uint32_t)16U; 275 KRML_PRE_ALIGN(16) 276 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 277 uint64_t u0 = load64_le(block); 278 uint64_t lo = u0; 279 uint64_t u = load64_le(block + (uint32_t)8U); 280 uint64_t hi = u; 281 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 282 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 283 Lib_IntVector_Intrinsics_vec128 284 f010 = 285 Lib_IntVector_Intrinsics_vec128_and(f0, 286 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 287 Lib_IntVector_Intrinsics_vec128 288 f110 = 289 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 290 (uint32_t)26U), 291 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 292 Lib_IntVector_Intrinsics_vec128 293 f20 = 294 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 295 (uint32_t)52U), 296 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 297 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 298 (uint32_t)12U)); 299 Lib_IntVector_Intrinsics_vec128 300 f30 = 301 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 302 (uint32_t)14U), 303 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 304 Lib_IntVector_Intrinsics_vec128 305 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 306 Lib_IntVector_Intrinsics_vec128 f01 = f010; 307 Lib_IntVector_Intrinsics_vec128 f111 = f110; 308 Lib_IntVector_Intrinsics_vec128 f2 = f20; 309 Lib_IntVector_Intrinsics_vec128 f3 = f30; 310 Lib_IntVector_Intrinsics_vec128 f41 = f40; 311 e[0U] = f01; 312 e[1U] = f111; 313 e[2U] = f2; 314 e[3U] = f3; 315 e[4U] = f41; 316 uint64_t b = (uint64_t)0x1000000U; 317 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 318 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 319 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 320 Lib_IntVector_Intrinsics_vec128 *r1 = pre0; 321 Lib_IntVector_Intrinsics_vec128 *r5 = pre0 + (uint32_t)5U; 322 Lib_IntVector_Intrinsics_vec128 r0 = r1[0U]; 323 Lib_IntVector_Intrinsics_vec128 r11 = r1[1U]; 324 Lib_IntVector_Intrinsics_vec128 r2 = r1[2U]; 325 Lib_IntVector_Intrinsics_vec128 r3 = r1[3U]; 326 Lib_IntVector_Intrinsics_vec128 r4 = r1[4U]; 327 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 328 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 329 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 330 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 331 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 332 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 333 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 334 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 335 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 336 Lib_IntVector_Intrinsics_vec128 a0 = acc0[0U]; 337 Lib_IntVector_Intrinsics_vec128 a1 = acc0[1U]; 338 Lib_IntVector_Intrinsics_vec128 a2 = acc0[2U]; 339 Lib_IntVector_Intrinsics_vec128 a3 = acc0[3U]; 340 Lib_IntVector_Intrinsics_vec128 a4 = acc0[4U]; 341 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 342 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 343 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 344 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 345 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 346 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 347 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r11, a01); 348 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 349 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 350 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 351 Lib_IntVector_Intrinsics_vec128 352 a03 = 353 Lib_IntVector_Intrinsics_vec128_add64(a02, 354 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 355 Lib_IntVector_Intrinsics_vec128 356 a13 = 357 Lib_IntVector_Intrinsics_vec128_add64(a12, 358 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 359 Lib_IntVector_Intrinsics_vec128 360 a23 = 361 Lib_IntVector_Intrinsics_vec128_add64(a22, 362 Lib_IntVector_Intrinsics_vec128_mul64(r11, a11)); 363 Lib_IntVector_Intrinsics_vec128 364 a33 = 365 Lib_IntVector_Intrinsics_vec128_add64(a32, 366 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 367 Lib_IntVector_Intrinsics_vec128 368 a43 = 369 Lib_IntVector_Intrinsics_vec128_add64(a42, 370 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 371 Lib_IntVector_Intrinsics_vec128 372 a04 = 373 Lib_IntVector_Intrinsics_vec128_add64(a03, 374 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 375 Lib_IntVector_Intrinsics_vec128 376 a14 = 377 Lib_IntVector_Intrinsics_vec128_add64(a13, 378 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 379 Lib_IntVector_Intrinsics_vec128 380 a24 = 381 Lib_IntVector_Intrinsics_vec128_add64(a23, 382 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 383 Lib_IntVector_Intrinsics_vec128 384 a34 = 385 Lib_IntVector_Intrinsics_vec128_add64(a33, 386 Lib_IntVector_Intrinsics_vec128_mul64(r11, a21)); 387 Lib_IntVector_Intrinsics_vec128 388 a44 = 389 Lib_IntVector_Intrinsics_vec128_add64(a43, 390 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 391 Lib_IntVector_Intrinsics_vec128 392 a05 = 393 Lib_IntVector_Intrinsics_vec128_add64(a04, 394 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 395 Lib_IntVector_Intrinsics_vec128 396 a15 = 397 Lib_IntVector_Intrinsics_vec128_add64(a14, 398 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 399 Lib_IntVector_Intrinsics_vec128 400 a25 = 401 Lib_IntVector_Intrinsics_vec128_add64(a24, 402 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 403 Lib_IntVector_Intrinsics_vec128 404 a35 = 405 Lib_IntVector_Intrinsics_vec128_add64(a34, 406 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 407 Lib_IntVector_Intrinsics_vec128 408 a45 = 409 Lib_IntVector_Intrinsics_vec128_add64(a44, 410 Lib_IntVector_Intrinsics_vec128_mul64(r11, a31)); 411 Lib_IntVector_Intrinsics_vec128 412 a06 = 413 Lib_IntVector_Intrinsics_vec128_add64(a05, 414 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 415 Lib_IntVector_Intrinsics_vec128 416 a16 = 417 Lib_IntVector_Intrinsics_vec128_add64(a15, 418 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 419 Lib_IntVector_Intrinsics_vec128 420 a26 = 421 Lib_IntVector_Intrinsics_vec128_add64(a25, 422 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 423 Lib_IntVector_Intrinsics_vec128 424 a36 = 425 Lib_IntVector_Intrinsics_vec128_add64(a35, 426 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 427 Lib_IntVector_Intrinsics_vec128 428 a46 = 429 Lib_IntVector_Intrinsics_vec128_add64(a45, 430 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 431 Lib_IntVector_Intrinsics_vec128 t01 = a06; 432 Lib_IntVector_Intrinsics_vec128 t11 = a16; 433 Lib_IntVector_Intrinsics_vec128 t2 = a26; 434 Lib_IntVector_Intrinsics_vec128 t3 = a36; 435 Lib_IntVector_Intrinsics_vec128 t4 = a46; 436 Lib_IntVector_Intrinsics_vec128 437 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 438 Lib_IntVector_Intrinsics_vec128 439 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 440 Lib_IntVector_Intrinsics_vec128 441 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 442 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 443 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 444 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); 445 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 446 Lib_IntVector_Intrinsics_vec128 447 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 448 Lib_IntVector_Intrinsics_vec128 449 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 450 Lib_IntVector_Intrinsics_vec128 451 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 452 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 453 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 454 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 455 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 456 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 457 Lib_IntVector_Intrinsics_vec128 458 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 459 Lib_IntVector_Intrinsics_vec128 460 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 461 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 462 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 463 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 464 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 465 Lib_IntVector_Intrinsics_vec128 466 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 467 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 468 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 469 Lib_IntVector_Intrinsics_vec128 o0 = x02; 470 Lib_IntVector_Intrinsics_vec128 o1 = x12; 471 Lib_IntVector_Intrinsics_vec128 o2 = x21; 472 Lib_IntVector_Intrinsics_vec128 o3 = x32; 473 Lib_IntVector_Intrinsics_vec128 o4 = x42; 474 acc0[0U] = o0; 475 acc0[1U] = o1; 476 acc0[2U] = o2; 477 acc0[3U] = o3; 478 acc0[4U] = o4; 479 } 480 if (rem1 > (uint32_t)0U) { 481 uint8_t *last = t10 + nb * (uint32_t)16U; 482 KRML_PRE_ALIGN(16) 483 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 484 uint8_t tmp[16U] = { 0U }; 485 memcpy(tmp, last, rem1 * sizeof(uint8_t)); 486 uint64_t u0 = load64_le(tmp); 487 uint64_t lo = u0; 488 uint64_t u = load64_le(tmp + (uint32_t)8U); 489 uint64_t hi = u; 490 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 491 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 492 Lib_IntVector_Intrinsics_vec128 493 f010 = 494 Lib_IntVector_Intrinsics_vec128_and(f0, 495 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 496 Lib_IntVector_Intrinsics_vec128 497 f110 = 498 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 499 (uint32_t)26U), 500 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 501 Lib_IntVector_Intrinsics_vec128 502 f20 = 503 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 504 (uint32_t)52U), 505 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 506 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 507 (uint32_t)12U)); 508 Lib_IntVector_Intrinsics_vec128 509 f30 = 510 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 511 (uint32_t)14U), 512 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 513 Lib_IntVector_Intrinsics_vec128 514 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 515 Lib_IntVector_Intrinsics_vec128 f01 = f010; 516 Lib_IntVector_Intrinsics_vec128 f111 = f110; 517 Lib_IntVector_Intrinsics_vec128 f2 = f20; 518 Lib_IntVector_Intrinsics_vec128 f3 = f30; 519 Lib_IntVector_Intrinsics_vec128 f4 = f40; 520 e[0U] = f01; 521 e[1U] = f111; 522 e[2U] = f2; 523 e[3U] = f3; 524 e[4U] = f4; 525 uint64_t b = (uint64_t)1U << rem1 * (uint32_t)8U % (uint32_t)26U; 526 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 527 Lib_IntVector_Intrinsics_vec128 fi = e[rem1 * (uint32_t)8U / (uint32_t)26U]; 528 e[rem1 * (uint32_t)8U / (uint32_t)26U] = Lib_IntVector_Intrinsics_vec128_or(fi, mask); 529 Lib_IntVector_Intrinsics_vec128 *r1 = pre0; 530 Lib_IntVector_Intrinsics_vec128 *r5 = pre0 + (uint32_t)5U; 531 Lib_IntVector_Intrinsics_vec128 r0 = r1[0U]; 532 Lib_IntVector_Intrinsics_vec128 r11 = r1[1U]; 533 Lib_IntVector_Intrinsics_vec128 r2 = r1[2U]; 534 Lib_IntVector_Intrinsics_vec128 r3 = r1[3U]; 535 Lib_IntVector_Intrinsics_vec128 r4 = r1[4U]; 536 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 537 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 538 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 539 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 540 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 541 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 542 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 543 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 544 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 545 Lib_IntVector_Intrinsics_vec128 a0 = acc0[0U]; 546 Lib_IntVector_Intrinsics_vec128 a1 = acc0[1U]; 547 Lib_IntVector_Intrinsics_vec128 a2 = acc0[2U]; 548 Lib_IntVector_Intrinsics_vec128 a3 = acc0[3U]; 549 Lib_IntVector_Intrinsics_vec128 a4 = acc0[4U]; 550 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 551 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 552 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 553 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 554 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 555 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 556 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r11, a01); 557 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 558 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 559 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 560 Lib_IntVector_Intrinsics_vec128 561 a03 = 562 Lib_IntVector_Intrinsics_vec128_add64(a02, 563 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 564 Lib_IntVector_Intrinsics_vec128 565 a13 = 566 Lib_IntVector_Intrinsics_vec128_add64(a12, 567 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 568 Lib_IntVector_Intrinsics_vec128 569 a23 = 570 Lib_IntVector_Intrinsics_vec128_add64(a22, 571 Lib_IntVector_Intrinsics_vec128_mul64(r11, a11)); 572 Lib_IntVector_Intrinsics_vec128 573 a33 = 574 Lib_IntVector_Intrinsics_vec128_add64(a32, 575 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 576 Lib_IntVector_Intrinsics_vec128 577 a43 = 578 Lib_IntVector_Intrinsics_vec128_add64(a42, 579 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 580 Lib_IntVector_Intrinsics_vec128 581 a04 = 582 Lib_IntVector_Intrinsics_vec128_add64(a03, 583 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 584 Lib_IntVector_Intrinsics_vec128 585 a14 = 586 Lib_IntVector_Intrinsics_vec128_add64(a13, 587 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 588 Lib_IntVector_Intrinsics_vec128 589 a24 = 590 Lib_IntVector_Intrinsics_vec128_add64(a23, 591 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 592 Lib_IntVector_Intrinsics_vec128 593 a34 = 594 Lib_IntVector_Intrinsics_vec128_add64(a33, 595 Lib_IntVector_Intrinsics_vec128_mul64(r11, a21)); 596 Lib_IntVector_Intrinsics_vec128 597 a44 = 598 Lib_IntVector_Intrinsics_vec128_add64(a43, 599 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 600 Lib_IntVector_Intrinsics_vec128 601 a05 = 602 Lib_IntVector_Intrinsics_vec128_add64(a04, 603 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 604 Lib_IntVector_Intrinsics_vec128 605 a15 = 606 Lib_IntVector_Intrinsics_vec128_add64(a14, 607 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 608 Lib_IntVector_Intrinsics_vec128 609 a25 = 610 Lib_IntVector_Intrinsics_vec128_add64(a24, 611 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 612 Lib_IntVector_Intrinsics_vec128 613 a35 = 614 Lib_IntVector_Intrinsics_vec128_add64(a34, 615 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 616 Lib_IntVector_Intrinsics_vec128 617 a45 = 618 Lib_IntVector_Intrinsics_vec128_add64(a44, 619 Lib_IntVector_Intrinsics_vec128_mul64(r11, a31)); 620 Lib_IntVector_Intrinsics_vec128 621 a06 = 622 Lib_IntVector_Intrinsics_vec128_add64(a05, 623 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 624 Lib_IntVector_Intrinsics_vec128 625 a16 = 626 Lib_IntVector_Intrinsics_vec128_add64(a15, 627 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 628 Lib_IntVector_Intrinsics_vec128 629 a26 = 630 Lib_IntVector_Intrinsics_vec128_add64(a25, 631 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 632 Lib_IntVector_Intrinsics_vec128 633 a36 = 634 Lib_IntVector_Intrinsics_vec128_add64(a35, 635 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 636 Lib_IntVector_Intrinsics_vec128 637 a46 = 638 Lib_IntVector_Intrinsics_vec128_add64(a45, 639 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 640 Lib_IntVector_Intrinsics_vec128 t01 = a06; 641 Lib_IntVector_Intrinsics_vec128 t11 = a16; 642 Lib_IntVector_Intrinsics_vec128 t2 = a26; 643 Lib_IntVector_Intrinsics_vec128 t3 = a36; 644 Lib_IntVector_Intrinsics_vec128 t4 = a46; 645 Lib_IntVector_Intrinsics_vec128 646 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 647 Lib_IntVector_Intrinsics_vec128 648 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); 649 Lib_IntVector_Intrinsics_vec128 650 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 651 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); 652 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 653 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); 654 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 655 Lib_IntVector_Intrinsics_vec128 656 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 657 Lib_IntVector_Intrinsics_vec128 658 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 659 Lib_IntVector_Intrinsics_vec128 660 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 661 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 662 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 663 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 664 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 665 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 666 Lib_IntVector_Intrinsics_vec128 667 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 668 Lib_IntVector_Intrinsics_vec128 669 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 670 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 671 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 672 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 673 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 674 Lib_IntVector_Intrinsics_vec128 675 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 676 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 677 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 678 Lib_IntVector_Intrinsics_vec128 o0 = x02; 679 Lib_IntVector_Intrinsics_vec128 o1 = x12; 680 Lib_IntVector_Intrinsics_vec128 o2 = x21; 681 Lib_IntVector_Intrinsics_vec128 o3 = x32; 682 Lib_IntVector_Intrinsics_vec128 o4 = x42; 683 acc0[0U] = o0; 684 acc0[1U] = o1; 685 acc0[2U] = o2; 686 acc0[3U] = o3; 687 acc0[4U] = o4; 688 } 689 uint8_t tmp[16U] = { 0U }; 690 memcpy(tmp, rem, r * sizeof(uint8_t)); 691 if (r > (uint32_t)0U) { 692 Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; 693 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 694 KRML_PRE_ALIGN(16) 695 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 696 uint64_t u0 = load64_le(tmp); 697 uint64_t lo = u0; 698 uint64_t u = load64_le(tmp + (uint32_t)8U); 699 uint64_t hi = u; 700 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 701 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 702 Lib_IntVector_Intrinsics_vec128 703 f010 = 704 Lib_IntVector_Intrinsics_vec128_and(f0, 705 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 706 Lib_IntVector_Intrinsics_vec128 707 f110 = 708 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 709 (uint32_t)26U), 710 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 711 Lib_IntVector_Intrinsics_vec128 712 f20 = 713 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 714 (uint32_t)52U), 715 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 716 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 717 (uint32_t)12U)); 718 Lib_IntVector_Intrinsics_vec128 719 f30 = 720 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 721 (uint32_t)14U), 722 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 723 Lib_IntVector_Intrinsics_vec128 724 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 725 Lib_IntVector_Intrinsics_vec128 f01 = f010; 726 Lib_IntVector_Intrinsics_vec128 f111 = f110; 727 Lib_IntVector_Intrinsics_vec128 f2 = f20; 728 Lib_IntVector_Intrinsics_vec128 f3 = f30; 729 Lib_IntVector_Intrinsics_vec128 f41 = f40; 730 e[0U] = f01; 731 e[1U] = f111; 732 e[2U] = f2; 733 e[3U] = f3; 734 e[4U] = f41; 735 uint64_t b = (uint64_t)0x1000000U; 736 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 737 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 738 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 739 Lib_IntVector_Intrinsics_vec128 *r1 = pre; 740 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 741 Lib_IntVector_Intrinsics_vec128 r0 = r1[0U]; 742 Lib_IntVector_Intrinsics_vec128 r11 = r1[1U]; 743 Lib_IntVector_Intrinsics_vec128 r2 = r1[2U]; 744 Lib_IntVector_Intrinsics_vec128 r3 = r1[3U]; 745 Lib_IntVector_Intrinsics_vec128 r4 = r1[4U]; 746 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 747 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 748 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 749 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 750 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 751 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 752 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 753 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 754 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 755 Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; 756 Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; 757 Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; 758 Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; 759 Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; 760 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 761 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 762 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 763 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 764 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 765 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 766 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r11, a01); 767 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 768 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 769 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 770 Lib_IntVector_Intrinsics_vec128 771 a03 = 772 Lib_IntVector_Intrinsics_vec128_add64(a02, 773 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 774 Lib_IntVector_Intrinsics_vec128 775 a13 = 776 Lib_IntVector_Intrinsics_vec128_add64(a12, 777 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 778 Lib_IntVector_Intrinsics_vec128 779 a23 = 780 Lib_IntVector_Intrinsics_vec128_add64(a22, 781 Lib_IntVector_Intrinsics_vec128_mul64(r11, a11)); 782 Lib_IntVector_Intrinsics_vec128 783 a33 = 784 Lib_IntVector_Intrinsics_vec128_add64(a32, 785 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 786 Lib_IntVector_Intrinsics_vec128 787 a43 = 788 Lib_IntVector_Intrinsics_vec128_add64(a42, 789 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 790 Lib_IntVector_Intrinsics_vec128 791 a04 = 792 Lib_IntVector_Intrinsics_vec128_add64(a03, 793 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 794 Lib_IntVector_Intrinsics_vec128 795 a14 = 796 Lib_IntVector_Intrinsics_vec128_add64(a13, 797 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 798 Lib_IntVector_Intrinsics_vec128 799 a24 = 800 Lib_IntVector_Intrinsics_vec128_add64(a23, 801 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 802 Lib_IntVector_Intrinsics_vec128 803 a34 = 804 Lib_IntVector_Intrinsics_vec128_add64(a33, 805 Lib_IntVector_Intrinsics_vec128_mul64(r11, a21)); 806 Lib_IntVector_Intrinsics_vec128 807 a44 = 808 Lib_IntVector_Intrinsics_vec128_add64(a43, 809 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 810 Lib_IntVector_Intrinsics_vec128 811 a05 = 812 Lib_IntVector_Intrinsics_vec128_add64(a04, 813 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 814 Lib_IntVector_Intrinsics_vec128 815 a15 = 816 Lib_IntVector_Intrinsics_vec128_add64(a14, 817 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 818 Lib_IntVector_Intrinsics_vec128 819 a25 = 820 Lib_IntVector_Intrinsics_vec128_add64(a24, 821 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 822 Lib_IntVector_Intrinsics_vec128 823 a35 = 824 Lib_IntVector_Intrinsics_vec128_add64(a34, 825 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 826 Lib_IntVector_Intrinsics_vec128 827 a45 = 828 Lib_IntVector_Intrinsics_vec128_add64(a44, 829 Lib_IntVector_Intrinsics_vec128_mul64(r11, a31)); 830 Lib_IntVector_Intrinsics_vec128 831 a06 = 832 Lib_IntVector_Intrinsics_vec128_add64(a05, 833 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 834 Lib_IntVector_Intrinsics_vec128 835 a16 = 836 Lib_IntVector_Intrinsics_vec128_add64(a15, 837 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 838 Lib_IntVector_Intrinsics_vec128 839 a26 = 840 Lib_IntVector_Intrinsics_vec128_add64(a25, 841 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 842 Lib_IntVector_Intrinsics_vec128 843 a36 = 844 Lib_IntVector_Intrinsics_vec128_add64(a35, 845 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 846 Lib_IntVector_Intrinsics_vec128 847 a46 = 848 Lib_IntVector_Intrinsics_vec128_add64(a45, 849 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 850 Lib_IntVector_Intrinsics_vec128 t0 = a06; 851 Lib_IntVector_Intrinsics_vec128 t1 = a16; 852 Lib_IntVector_Intrinsics_vec128 t2 = a26; 853 Lib_IntVector_Intrinsics_vec128 t3 = a36; 854 Lib_IntVector_Intrinsics_vec128 t4 = a46; 855 Lib_IntVector_Intrinsics_vec128 856 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 857 Lib_IntVector_Intrinsics_vec128 858 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); 859 Lib_IntVector_Intrinsics_vec128 860 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 861 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); 862 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 863 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 864 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 865 Lib_IntVector_Intrinsics_vec128 866 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 867 Lib_IntVector_Intrinsics_vec128 868 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 869 Lib_IntVector_Intrinsics_vec128 870 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 871 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 872 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 873 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 874 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 875 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 876 Lib_IntVector_Intrinsics_vec128 877 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 878 Lib_IntVector_Intrinsics_vec128 879 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 880 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 881 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 882 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 883 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 884 Lib_IntVector_Intrinsics_vec128 885 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 886 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 887 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 888 Lib_IntVector_Intrinsics_vec128 o0 = x02; 889 Lib_IntVector_Intrinsics_vec128 o1 = x12; 890 Lib_IntVector_Intrinsics_vec128 o2 = x21; 891 Lib_IntVector_Intrinsics_vec128 o3 = x32; 892 Lib_IntVector_Intrinsics_vec128 o4 = x42; 893 acc[0U] = o0; 894 acc[1U] = o1; 895 acc[2U] = o2; 896 acc[3U] = o3; 897 acc[4U] = o4; 898 return; 899 } 900 } 901 902 static inline void 903 poly1305_do_128( 904 uint8_t *k, 905 uint32_t aadlen, 906 uint8_t *aad, 907 uint32_t mlen, 908 uint8_t *m, 909 uint8_t *out) 910 { 911 KRML_PRE_ALIGN(16) 912 Lib_IntVector_Intrinsics_vec128 ctx[25U] KRML_POST_ALIGN(16) = { 0U }; 913 uint8_t block[16U] = { 0U }; 914 Hacl_Poly1305_128_poly1305_init(ctx, k); 915 if (aadlen != (uint32_t)0U) { 916 poly1305_padded_128(ctx, aadlen, aad); 917 } 918 if (mlen != (uint32_t)0U) { 919 poly1305_padded_128(ctx, mlen, m); 920 } 921 store64_le(block, (uint64_t)aadlen); 922 store64_le(block + (uint32_t)8U, (uint64_t)mlen); 923 Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; 924 Lib_IntVector_Intrinsics_vec128 *acc = ctx; 925 KRML_PRE_ALIGN(16) 926 Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; 927 uint64_t u0 = load64_le(block); 928 uint64_t lo = u0; 929 uint64_t u = load64_le(block + (uint32_t)8U); 930 uint64_t hi = u; 931 Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); 932 Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); 933 Lib_IntVector_Intrinsics_vec128 934 f010 = 935 Lib_IntVector_Intrinsics_vec128_and(f0, 936 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 937 Lib_IntVector_Intrinsics_vec128 938 f110 = 939 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 940 (uint32_t)26U), 941 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 942 Lib_IntVector_Intrinsics_vec128 943 f20 = 944 Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, 945 (uint32_t)52U), 946 Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, 947 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), 948 (uint32_t)12U)); 949 Lib_IntVector_Intrinsics_vec128 950 f30 = 951 Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, 952 (uint32_t)14U), 953 Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); 954 Lib_IntVector_Intrinsics_vec128 955 f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); 956 Lib_IntVector_Intrinsics_vec128 f01 = f010; 957 Lib_IntVector_Intrinsics_vec128 f111 = f110; 958 Lib_IntVector_Intrinsics_vec128 f2 = f20; 959 Lib_IntVector_Intrinsics_vec128 f3 = f30; 960 Lib_IntVector_Intrinsics_vec128 f41 = f40; 961 e[0U] = f01; 962 e[1U] = f111; 963 e[2U] = f2; 964 e[3U] = f3; 965 e[4U] = f41; 966 uint64_t b = (uint64_t)0x1000000U; 967 Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); 968 Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; 969 e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); 970 Lib_IntVector_Intrinsics_vec128 *r = pre; 971 Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; 972 Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; 973 Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; 974 Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; 975 Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; 976 Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; 977 Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; 978 Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; 979 Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; 980 Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; 981 Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; 982 Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; 983 Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; 984 Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; 985 Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; 986 Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; 987 Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; 988 Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; 989 Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; 990 Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; 991 Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); 992 Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); 993 Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); 994 Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); 995 Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); 996 Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); 997 Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); 998 Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); 999 Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); 1000 Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); 1001 Lib_IntVector_Intrinsics_vec128 1002 a03 = 1003 Lib_IntVector_Intrinsics_vec128_add64(a02, 1004 Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); 1005 Lib_IntVector_Intrinsics_vec128 1006 a13 = 1007 Lib_IntVector_Intrinsics_vec128_add64(a12, 1008 Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); 1009 Lib_IntVector_Intrinsics_vec128 1010 a23 = 1011 Lib_IntVector_Intrinsics_vec128_add64(a22, 1012 Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); 1013 Lib_IntVector_Intrinsics_vec128 1014 a33 = 1015 Lib_IntVector_Intrinsics_vec128_add64(a32, 1016 Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); 1017 Lib_IntVector_Intrinsics_vec128 1018 a43 = 1019 Lib_IntVector_Intrinsics_vec128_add64(a42, 1020 Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); 1021 Lib_IntVector_Intrinsics_vec128 1022 a04 = 1023 Lib_IntVector_Intrinsics_vec128_add64(a03, 1024 Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); 1025 Lib_IntVector_Intrinsics_vec128 1026 a14 = 1027 Lib_IntVector_Intrinsics_vec128_add64(a13, 1028 Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); 1029 Lib_IntVector_Intrinsics_vec128 1030 a24 = 1031 Lib_IntVector_Intrinsics_vec128_add64(a23, 1032 Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); 1033 Lib_IntVector_Intrinsics_vec128 1034 a34 = 1035 Lib_IntVector_Intrinsics_vec128_add64(a33, 1036 Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); 1037 Lib_IntVector_Intrinsics_vec128 1038 a44 = 1039 Lib_IntVector_Intrinsics_vec128_add64(a43, 1040 Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); 1041 Lib_IntVector_Intrinsics_vec128 1042 a05 = 1043 Lib_IntVector_Intrinsics_vec128_add64(a04, 1044 Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); 1045 Lib_IntVector_Intrinsics_vec128 1046 a15 = 1047 Lib_IntVector_Intrinsics_vec128_add64(a14, 1048 Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); 1049 Lib_IntVector_Intrinsics_vec128 1050 a25 = 1051 Lib_IntVector_Intrinsics_vec128_add64(a24, 1052 Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); 1053 Lib_IntVector_Intrinsics_vec128 1054 a35 = 1055 Lib_IntVector_Intrinsics_vec128_add64(a34, 1056 Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); 1057 Lib_IntVector_Intrinsics_vec128 1058 a45 = 1059 Lib_IntVector_Intrinsics_vec128_add64(a44, 1060 Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); 1061 Lib_IntVector_Intrinsics_vec128 1062 a06 = 1063 Lib_IntVector_Intrinsics_vec128_add64(a05, 1064 Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); 1065 Lib_IntVector_Intrinsics_vec128 1066 a16 = 1067 Lib_IntVector_Intrinsics_vec128_add64(a15, 1068 Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); 1069 Lib_IntVector_Intrinsics_vec128 1070 a26 = 1071 Lib_IntVector_Intrinsics_vec128_add64(a25, 1072 Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); 1073 Lib_IntVector_Intrinsics_vec128 1074 a36 = 1075 Lib_IntVector_Intrinsics_vec128_add64(a35, 1076 Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); 1077 Lib_IntVector_Intrinsics_vec128 1078 a46 = 1079 Lib_IntVector_Intrinsics_vec128_add64(a45, 1080 Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); 1081 Lib_IntVector_Intrinsics_vec128 t0 = a06; 1082 Lib_IntVector_Intrinsics_vec128 t1 = a16; 1083 Lib_IntVector_Intrinsics_vec128 t2 = a26; 1084 Lib_IntVector_Intrinsics_vec128 t3 = a36; 1085 Lib_IntVector_Intrinsics_vec128 t4 = a46; 1086 Lib_IntVector_Intrinsics_vec128 1087 mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); 1088 Lib_IntVector_Intrinsics_vec128 1089 z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); 1090 Lib_IntVector_Intrinsics_vec128 1091 z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); 1092 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); 1093 Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); 1094 Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); 1095 Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); 1096 Lib_IntVector_Intrinsics_vec128 1097 z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); 1098 Lib_IntVector_Intrinsics_vec128 1099 z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); 1100 Lib_IntVector_Intrinsics_vec128 1101 t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); 1102 Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); 1103 Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); 1104 Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); 1105 Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); 1106 Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); 1107 Lib_IntVector_Intrinsics_vec128 1108 z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); 1109 Lib_IntVector_Intrinsics_vec128 1110 z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); 1111 Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); 1112 Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); 1113 Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); 1114 Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); 1115 Lib_IntVector_Intrinsics_vec128 1116 z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); 1117 Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); 1118 Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); 1119 Lib_IntVector_Intrinsics_vec128 o0 = x02; 1120 Lib_IntVector_Intrinsics_vec128 o1 = x12; 1121 Lib_IntVector_Intrinsics_vec128 o2 = x21; 1122 Lib_IntVector_Intrinsics_vec128 o3 = x32; 1123 Lib_IntVector_Intrinsics_vec128 o4 = x42; 1124 acc[0U] = o0; 1125 acc[1U] = o1; 1126 acc[2U] = o2; 1127 acc[3U] = o3; 1128 acc[4U] = o4; 1129 Hacl_Poly1305_128_poly1305_finish(out, k, ctx); 1130 } 1131 1132 /** 1133 Encrypt a message `m` with key `k`. 1134 1135 The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption. 1136 Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory. 1137 1138 @param k Pointer to 32 bytes of memory where the AEAD key is read from. 1139 @param n Pointer to 12 bytes of memory where the AEAD nonce is read from. 1140 @param aadlen Length of the associated data. 1141 @param aad Pointer to `aadlen` bytes of memory where the associated data is read from. 1142 1143 @param mlen Length of the message. 1144 @param m Pointer to `mlen` bytes of memory where the message is read from. 1145 @param cipher Pointer to `mlen` bytes of memory where the ciphertext is written to. 1146 @param mac Pointer to 16 bytes of memory where the mac is written to. 1147 */ 1148 void 1149 Hacl_Chacha20Poly1305_128_aead_encrypt( 1150 uint8_t *k, 1151 uint8_t *n, 1152 uint32_t aadlen, 1153 uint8_t *aad, 1154 uint32_t mlen, 1155 uint8_t *m, 1156 uint8_t *cipher, 1157 uint8_t *mac) 1158 { 1159 Hacl_Chacha20_Vec128_chacha20_encrypt_128(mlen, cipher, m, k, n, (uint32_t)1U); 1160 uint8_t tmp[64U] = { 0U }; 1161 Hacl_Chacha20_Vec128_chacha20_encrypt_128((uint32_t)64U, tmp, tmp, k, n, (uint32_t)0U); 1162 uint8_t *key = tmp; 1163 poly1305_do_128(key, aadlen, aad, mlen, cipher, mac); 1164 } 1165 1166 /** 1167 Decrypt a ciphertext `cipher` with key `k`. 1168 1169 The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption. 1170 Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory. 1171 1172 If decryption succeeds, the resulting plaintext is stored in `m` and the function returns the success code 0. 1173 If decryption fails, the array `m` remains unchanged and the function returns the error code 1. 1174 1175 @param k Pointer to 32 bytes of memory where the AEAD key is read from. 1176 @param n Pointer to 12 bytes of memory where the AEAD nonce is read from. 1177 @param aadlen Length of the associated data. 1178 @param aad Pointer to `aadlen` bytes of memory where the associated data is read from. 1179 1180 @param mlen Length of the ciphertext. 1181 @param m Pointer to `mlen` bytes of memory where the message is written to. 1182 @param cipher Pointer to `mlen` bytes of memory where the ciphertext is read from. 1183 @param mac Pointer to 16 bytes of memory where the mac is read from. 1184 1185 @returns 0 on succeess; 1 on failure. 1186 */ 1187 uint32_t 1188 Hacl_Chacha20Poly1305_128_aead_decrypt( 1189 uint8_t *k, 1190 uint8_t *n, 1191 uint32_t aadlen, 1192 uint8_t *aad, 1193 uint32_t mlen, 1194 uint8_t *m, 1195 uint8_t *cipher, 1196 uint8_t *mac) 1197 { 1198 uint8_t computed_mac[16U] = { 0U }; 1199 uint8_t tmp[64U] = { 0U }; 1200 Hacl_Chacha20_Vec128_chacha20_encrypt_128((uint32_t)64U, tmp, tmp, k, n, (uint32_t)0U); 1201 uint8_t *key = tmp; 1202 poly1305_do_128(key, aadlen, aad, mlen, cipher, computed_mac); 1203 uint8_t res = (uint8_t)255U; 1204 KRML_MAYBE_FOR16(i, 1205 (uint32_t)0U, 1206 (uint32_t)16U, 1207 (uint32_t)1U, 1208 uint8_t uu____0 = FStar_UInt8_eq_mask(computed_mac[i], mac[i]); 1209 res = uu____0 & res;); 1210 uint8_t z = res; 1211 if (z == (uint8_t)255U) { 1212 Hacl_Chacha20_Vec128_chacha20_encrypt_128(mlen, m, cipher, k, n, (uint32_t)1U); 1213 return (uint32_t)0U; 1214 } 1215 return (uint32_t)1U; 1216 }