Hacl_Chacha20_Vec128.c (43855B)
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_Chacha20_Vec128.h" 26 27 #include "internal/Hacl_Chacha20.h" 28 #include "libintvector.h" 29 30 static inline void 31 double_round_128(Lib_IntVector_Intrinsics_vec128 *st) 32 { 33 st[0U] = Lib_IntVector_Intrinsics_vec128_add32(st[0U], st[4U]); 34 Lib_IntVector_Intrinsics_vec128 std = Lib_IntVector_Intrinsics_vec128_xor(st[12U], st[0U]); 35 st[12U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std, (uint32_t)16U); 36 st[8U] = Lib_IntVector_Intrinsics_vec128_add32(st[8U], st[12U]); 37 Lib_IntVector_Intrinsics_vec128 std0 = Lib_IntVector_Intrinsics_vec128_xor(st[4U], st[8U]); 38 st[4U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std0, (uint32_t)12U); 39 st[0U] = Lib_IntVector_Intrinsics_vec128_add32(st[0U], st[4U]); 40 Lib_IntVector_Intrinsics_vec128 std1 = Lib_IntVector_Intrinsics_vec128_xor(st[12U], st[0U]); 41 st[12U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std1, (uint32_t)8U); 42 st[8U] = Lib_IntVector_Intrinsics_vec128_add32(st[8U], st[12U]); 43 Lib_IntVector_Intrinsics_vec128 std2 = Lib_IntVector_Intrinsics_vec128_xor(st[4U], st[8U]); 44 st[4U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std2, (uint32_t)7U); 45 st[1U] = Lib_IntVector_Intrinsics_vec128_add32(st[1U], st[5U]); 46 Lib_IntVector_Intrinsics_vec128 std3 = Lib_IntVector_Intrinsics_vec128_xor(st[13U], st[1U]); 47 st[13U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std3, (uint32_t)16U); 48 st[9U] = Lib_IntVector_Intrinsics_vec128_add32(st[9U], st[13U]); 49 Lib_IntVector_Intrinsics_vec128 std4 = Lib_IntVector_Intrinsics_vec128_xor(st[5U], st[9U]); 50 st[5U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std4, (uint32_t)12U); 51 st[1U] = Lib_IntVector_Intrinsics_vec128_add32(st[1U], st[5U]); 52 Lib_IntVector_Intrinsics_vec128 std5 = Lib_IntVector_Intrinsics_vec128_xor(st[13U], st[1U]); 53 st[13U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std5, (uint32_t)8U); 54 st[9U] = Lib_IntVector_Intrinsics_vec128_add32(st[9U], st[13U]); 55 Lib_IntVector_Intrinsics_vec128 std6 = Lib_IntVector_Intrinsics_vec128_xor(st[5U], st[9U]); 56 st[5U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std6, (uint32_t)7U); 57 st[2U] = Lib_IntVector_Intrinsics_vec128_add32(st[2U], st[6U]); 58 Lib_IntVector_Intrinsics_vec128 std7 = Lib_IntVector_Intrinsics_vec128_xor(st[14U], st[2U]); 59 st[14U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std7, (uint32_t)16U); 60 st[10U] = Lib_IntVector_Intrinsics_vec128_add32(st[10U], st[14U]); 61 Lib_IntVector_Intrinsics_vec128 std8 = Lib_IntVector_Intrinsics_vec128_xor(st[6U], st[10U]); 62 st[6U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std8, (uint32_t)12U); 63 st[2U] = Lib_IntVector_Intrinsics_vec128_add32(st[2U], st[6U]); 64 Lib_IntVector_Intrinsics_vec128 std9 = Lib_IntVector_Intrinsics_vec128_xor(st[14U], st[2U]); 65 st[14U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std9, (uint32_t)8U); 66 st[10U] = Lib_IntVector_Intrinsics_vec128_add32(st[10U], st[14U]); 67 Lib_IntVector_Intrinsics_vec128 std10 = Lib_IntVector_Intrinsics_vec128_xor(st[6U], st[10U]); 68 st[6U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std10, (uint32_t)7U); 69 st[3U] = Lib_IntVector_Intrinsics_vec128_add32(st[3U], st[7U]); 70 Lib_IntVector_Intrinsics_vec128 std11 = Lib_IntVector_Intrinsics_vec128_xor(st[15U], st[3U]); 71 st[15U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std11, (uint32_t)16U); 72 st[11U] = Lib_IntVector_Intrinsics_vec128_add32(st[11U], st[15U]); 73 Lib_IntVector_Intrinsics_vec128 std12 = Lib_IntVector_Intrinsics_vec128_xor(st[7U], st[11U]); 74 st[7U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std12, (uint32_t)12U); 75 st[3U] = Lib_IntVector_Intrinsics_vec128_add32(st[3U], st[7U]); 76 Lib_IntVector_Intrinsics_vec128 std13 = Lib_IntVector_Intrinsics_vec128_xor(st[15U], st[3U]); 77 st[15U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std13, (uint32_t)8U); 78 st[11U] = Lib_IntVector_Intrinsics_vec128_add32(st[11U], st[15U]); 79 Lib_IntVector_Intrinsics_vec128 std14 = Lib_IntVector_Intrinsics_vec128_xor(st[7U], st[11U]); 80 st[7U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std14, (uint32_t)7U); 81 st[0U] = Lib_IntVector_Intrinsics_vec128_add32(st[0U], st[5U]); 82 Lib_IntVector_Intrinsics_vec128 std15 = Lib_IntVector_Intrinsics_vec128_xor(st[15U], st[0U]); 83 st[15U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std15, (uint32_t)16U); 84 st[10U] = Lib_IntVector_Intrinsics_vec128_add32(st[10U], st[15U]); 85 Lib_IntVector_Intrinsics_vec128 std16 = Lib_IntVector_Intrinsics_vec128_xor(st[5U], st[10U]); 86 st[5U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std16, (uint32_t)12U); 87 st[0U] = Lib_IntVector_Intrinsics_vec128_add32(st[0U], st[5U]); 88 Lib_IntVector_Intrinsics_vec128 std17 = Lib_IntVector_Intrinsics_vec128_xor(st[15U], st[0U]); 89 st[15U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std17, (uint32_t)8U); 90 st[10U] = Lib_IntVector_Intrinsics_vec128_add32(st[10U], st[15U]); 91 Lib_IntVector_Intrinsics_vec128 std18 = Lib_IntVector_Intrinsics_vec128_xor(st[5U], st[10U]); 92 st[5U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std18, (uint32_t)7U); 93 st[1U] = Lib_IntVector_Intrinsics_vec128_add32(st[1U], st[6U]); 94 Lib_IntVector_Intrinsics_vec128 std19 = Lib_IntVector_Intrinsics_vec128_xor(st[12U], st[1U]); 95 st[12U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std19, (uint32_t)16U); 96 st[11U] = Lib_IntVector_Intrinsics_vec128_add32(st[11U], st[12U]); 97 Lib_IntVector_Intrinsics_vec128 std20 = Lib_IntVector_Intrinsics_vec128_xor(st[6U], st[11U]); 98 st[6U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std20, (uint32_t)12U); 99 st[1U] = Lib_IntVector_Intrinsics_vec128_add32(st[1U], st[6U]); 100 Lib_IntVector_Intrinsics_vec128 std21 = Lib_IntVector_Intrinsics_vec128_xor(st[12U], st[1U]); 101 st[12U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std21, (uint32_t)8U); 102 st[11U] = Lib_IntVector_Intrinsics_vec128_add32(st[11U], st[12U]); 103 Lib_IntVector_Intrinsics_vec128 std22 = Lib_IntVector_Intrinsics_vec128_xor(st[6U], st[11U]); 104 st[6U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std22, (uint32_t)7U); 105 st[2U] = Lib_IntVector_Intrinsics_vec128_add32(st[2U], st[7U]); 106 Lib_IntVector_Intrinsics_vec128 std23 = Lib_IntVector_Intrinsics_vec128_xor(st[13U], st[2U]); 107 st[13U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std23, (uint32_t)16U); 108 st[8U] = Lib_IntVector_Intrinsics_vec128_add32(st[8U], st[13U]); 109 Lib_IntVector_Intrinsics_vec128 std24 = Lib_IntVector_Intrinsics_vec128_xor(st[7U], st[8U]); 110 st[7U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std24, (uint32_t)12U); 111 st[2U] = Lib_IntVector_Intrinsics_vec128_add32(st[2U], st[7U]); 112 Lib_IntVector_Intrinsics_vec128 std25 = Lib_IntVector_Intrinsics_vec128_xor(st[13U], st[2U]); 113 st[13U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std25, (uint32_t)8U); 114 st[8U] = Lib_IntVector_Intrinsics_vec128_add32(st[8U], st[13U]); 115 Lib_IntVector_Intrinsics_vec128 std26 = Lib_IntVector_Intrinsics_vec128_xor(st[7U], st[8U]); 116 st[7U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std26, (uint32_t)7U); 117 st[3U] = Lib_IntVector_Intrinsics_vec128_add32(st[3U], st[4U]); 118 Lib_IntVector_Intrinsics_vec128 std27 = Lib_IntVector_Intrinsics_vec128_xor(st[14U], st[3U]); 119 st[14U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std27, (uint32_t)16U); 120 st[9U] = Lib_IntVector_Intrinsics_vec128_add32(st[9U], st[14U]); 121 Lib_IntVector_Intrinsics_vec128 std28 = Lib_IntVector_Intrinsics_vec128_xor(st[4U], st[9U]); 122 st[4U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std28, (uint32_t)12U); 123 st[3U] = Lib_IntVector_Intrinsics_vec128_add32(st[3U], st[4U]); 124 Lib_IntVector_Intrinsics_vec128 std29 = Lib_IntVector_Intrinsics_vec128_xor(st[14U], st[3U]); 125 st[14U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std29, (uint32_t)8U); 126 st[9U] = Lib_IntVector_Intrinsics_vec128_add32(st[9U], st[14U]); 127 Lib_IntVector_Intrinsics_vec128 std30 = Lib_IntVector_Intrinsics_vec128_xor(st[4U], st[9U]); 128 st[4U] = Lib_IntVector_Intrinsics_vec128_rotate_left32(std30, (uint32_t)7U); 129 } 130 131 static inline void 132 chacha20_core_128( 133 Lib_IntVector_Intrinsics_vec128 *k, 134 Lib_IntVector_Intrinsics_vec128 *ctx, 135 uint32_t ctr) 136 { 137 memcpy(k, ctx, (uint32_t)16U * sizeof(Lib_IntVector_Intrinsics_vec128)); 138 uint32_t ctr_u32 = (uint32_t)4U * ctr; 139 Lib_IntVector_Intrinsics_vec128 cv = Lib_IntVector_Intrinsics_vec128_load32(ctr_u32); 140 k[12U] = Lib_IntVector_Intrinsics_vec128_add32(k[12U], cv); 141 double_round_128(k); 142 double_round_128(k); 143 double_round_128(k); 144 double_round_128(k); 145 double_round_128(k); 146 double_round_128(k); 147 double_round_128(k); 148 double_round_128(k); 149 double_round_128(k); 150 double_round_128(k); 151 KRML_MAYBE_FOR16(i, 152 (uint32_t)0U, 153 (uint32_t)16U, 154 (uint32_t)1U, 155 Lib_IntVector_Intrinsics_vec128 *os = k; 156 Lib_IntVector_Intrinsics_vec128 x = Lib_IntVector_Intrinsics_vec128_add32(k[i], ctx[i]); 157 os[i] = x;); 158 k[12U] = Lib_IntVector_Intrinsics_vec128_add32(k[12U], cv); 159 } 160 161 static inline void 162 chacha20_init_128(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *k, uint8_t *n, uint32_t ctr) 163 { 164 uint32_t ctx1[16U] = { 0U }; 165 KRML_MAYBE_FOR4(i, 166 (uint32_t)0U, 167 (uint32_t)4U, 168 (uint32_t)1U, 169 uint32_t *os = ctx1; 170 uint32_t x = Hacl_Impl_Chacha20_Vec_chacha20_constants[i]; 171 os[i] = x;); 172 KRML_MAYBE_FOR8(i, 173 (uint32_t)0U, 174 (uint32_t)8U, 175 (uint32_t)1U, 176 uint32_t *os = ctx1 + (uint32_t)4U; 177 uint8_t *bj = k + i * (uint32_t)4U; 178 uint32_t u = load32_le(bj); 179 uint32_t r = u; 180 uint32_t x = r; 181 os[i] = x;); 182 ctx1[12U] = ctr; 183 KRML_MAYBE_FOR3(i, 184 (uint32_t)0U, 185 (uint32_t)3U, 186 (uint32_t)1U, 187 uint32_t *os = ctx1 + (uint32_t)13U; 188 uint8_t *bj = n + i * (uint32_t)4U; 189 uint32_t u = load32_le(bj); 190 uint32_t r = u; 191 uint32_t x = r; 192 os[i] = x;); 193 KRML_MAYBE_FOR16(i, 194 (uint32_t)0U, 195 (uint32_t)16U, 196 (uint32_t)1U, 197 Lib_IntVector_Intrinsics_vec128 *os = ctx; 198 uint32_t x = ctx1[i]; 199 Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_load32(x); 200 os[i] = x0;); 201 Lib_IntVector_Intrinsics_vec128 202 ctr1 = 203 Lib_IntVector_Intrinsics_vec128_load32s((uint32_t)0U, 204 (uint32_t)1U, 205 (uint32_t)2U, 206 (uint32_t)3U); 207 Lib_IntVector_Intrinsics_vec128 c12 = ctx[12U]; 208 ctx[12U] = Lib_IntVector_Intrinsics_vec128_add32(c12, ctr1); 209 } 210 211 void 212 Hacl_Chacha20_Vec128_chacha20_encrypt_128( 213 uint32_t len, 214 uint8_t *out, 215 uint8_t *text, 216 uint8_t *key, 217 uint8_t *n, 218 uint32_t ctr) 219 { 220 KRML_PRE_ALIGN(16) 221 Lib_IntVector_Intrinsics_vec128 ctx[16U] KRML_POST_ALIGN(16) = { 0U }; 222 chacha20_init_128(ctx, key, n, ctr); 223 uint32_t rem = len % (uint32_t)256U; 224 uint32_t nb = len / (uint32_t)256U; 225 uint32_t rem1 = len % (uint32_t)256U; 226 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 227 uint8_t *uu____0 = out + i * (uint32_t)256U; 228 uint8_t *uu____1 = text + i * (uint32_t)256U; 229 KRML_PRE_ALIGN(16) 230 Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; 231 chacha20_core_128(k, ctx, i); 232 Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; 233 Lib_IntVector_Intrinsics_vec128 st1 = k[1U]; 234 Lib_IntVector_Intrinsics_vec128 st2 = k[2U]; 235 Lib_IntVector_Intrinsics_vec128 st3 = k[3U]; 236 Lib_IntVector_Intrinsics_vec128 st4 = k[4U]; 237 Lib_IntVector_Intrinsics_vec128 st5 = k[5U]; 238 Lib_IntVector_Intrinsics_vec128 st6 = k[6U]; 239 Lib_IntVector_Intrinsics_vec128 st7 = k[7U]; 240 Lib_IntVector_Intrinsics_vec128 st8 = k[8U]; 241 Lib_IntVector_Intrinsics_vec128 st9 = k[9U]; 242 Lib_IntVector_Intrinsics_vec128 st10 = k[10U]; 243 Lib_IntVector_Intrinsics_vec128 st11 = k[11U]; 244 Lib_IntVector_Intrinsics_vec128 st12 = k[12U]; 245 Lib_IntVector_Intrinsics_vec128 st13 = k[13U]; 246 Lib_IntVector_Intrinsics_vec128 st14 = k[14U]; 247 Lib_IntVector_Intrinsics_vec128 st15 = k[15U]; 248 Lib_IntVector_Intrinsics_vec128 249 v0_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st0, st1); 250 Lib_IntVector_Intrinsics_vec128 251 v1_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st0, st1); 252 Lib_IntVector_Intrinsics_vec128 253 v2_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st2, st3); 254 Lib_IntVector_Intrinsics_vec128 255 v3_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st2, st3); 256 Lib_IntVector_Intrinsics_vec128 257 v0__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_, v2_); 258 Lib_IntVector_Intrinsics_vec128 259 v1__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_, v2_); 260 Lib_IntVector_Intrinsics_vec128 261 v2__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_, v3_); 262 Lib_IntVector_Intrinsics_vec128 263 v3__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_, v3_); 264 Lib_IntVector_Intrinsics_vec128 v0__0 = v0__; 265 Lib_IntVector_Intrinsics_vec128 v2__0 = v2__; 266 Lib_IntVector_Intrinsics_vec128 v1__0 = v1__; 267 Lib_IntVector_Intrinsics_vec128 v3__0 = v3__; 268 Lib_IntVector_Intrinsics_vec128 v0 = v0__0; 269 Lib_IntVector_Intrinsics_vec128 v1 = v1__0; 270 Lib_IntVector_Intrinsics_vec128 v2 = v2__0; 271 Lib_IntVector_Intrinsics_vec128 v3 = v3__0; 272 Lib_IntVector_Intrinsics_vec128 273 v0_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st4, st5); 274 Lib_IntVector_Intrinsics_vec128 275 v1_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st4, st5); 276 Lib_IntVector_Intrinsics_vec128 277 v2_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st6, st7); 278 Lib_IntVector_Intrinsics_vec128 279 v3_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st6, st7); 280 Lib_IntVector_Intrinsics_vec128 281 v0__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_0, v2_0); 282 Lib_IntVector_Intrinsics_vec128 283 v1__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_0, v2_0); 284 Lib_IntVector_Intrinsics_vec128 285 v2__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_0, v3_0); 286 Lib_IntVector_Intrinsics_vec128 287 v3__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_0, v3_0); 288 Lib_IntVector_Intrinsics_vec128 v0__2 = v0__1; 289 Lib_IntVector_Intrinsics_vec128 v2__2 = v2__1; 290 Lib_IntVector_Intrinsics_vec128 v1__2 = v1__1; 291 Lib_IntVector_Intrinsics_vec128 v3__2 = v3__1; 292 Lib_IntVector_Intrinsics_vec128 v4 = v0__2; 293 Lib_IntVector_Intrinsics_vec128 v5 = v1__2; 294 Lib_IntVector_Intrinsics_vec128 v6 = v2__2; 295 Lib_IntVector_Intrinsics_vec128 v7 = v3__2; 296 Lib_IntVector_Intrinsics_vec128 297 v0_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st8, st9); 298 Lib_IntVector_Intrinsics_vec128 299 v1_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st8, st9); 300 Lib_IntVector_Intrinsics_vec128 301 v2_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st10, st11); 302 Lib_IntVector_Intrinsics_vec128 303 v3_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st10, st11); 304 Lib_IntVector_Intrinsics_vec128 305 v0__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_1, v2_1); 306 Lib_IntVector_Intrinsics_vec128 307 v1__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_1, v2_1); 308 Lib_IntVector_Intrinsics_vec128 309 v2__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_1, v3_1); 310 Lib_IntVector_Intrinsics_vec128 311 v3__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_1, v3_1); 312 Lib_IntVector_Intrinsics_vec128 v0__4 = v0__3; 313 Lib_IntVector_Intrinsics_vec128 v2__4 = v2__3; 314 Lib_IntVector_Intrinsics_vec128 v1__4 = v1__3; 315 Lib_IntVector_Intrinsics_vec128 v3__4 = v3__3; 316 Lib_IntVector_Intrinsics_vec128 v8 = v0__4; 317 Lib_IntVector_Intrinsics_vec128 v9 = v1__4; 318 Lib_IntVector_Intrinsics_vec128 v10 = v2__4; 319 Lib_IntVector_Intrinsics_vec128 v11 = v3__4; 320 Lib_IntVector_Intrinsics_vec128 321 v0_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st12, st13); 322 Lib_IntVector_Intrinsics_vec128 323 v1_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st12, st13); 324 Lib_IntVector_Intrinsics_vec128 325 v2_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st14, st15); 326 Lib_IntVector_Intrinsics_vec128 327 v3_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st14, st15); 328 Lib_IntVector_Intrinsics_vec128 329 v0__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_2, v2_2); 330 Lib_IntVector_Intrinsics_vec128 331 v1__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_2, v2_2); 332 Lib_IntVector_Intrinsics_vec128 333 v2__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_2, v3_2); 334 Lib_IntVector_Intrinsics_vec128 335 v3__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_2, v3_2); 336 Lib_IntVector_Intrinsics_vec128 v0__6 = v0__5; 337 Lib_IntVector_Intrinsics_vec128 v2__6 = v2__5; 338 Lib_IntVector_Intrinsics_vec128 v1__6 = v1__5; 339 Lib_IntVector_Intrinsics_vec128 v3__6 = v3__5; 340 Lib_IntVector_Intrinsics_vec128 v12 = v0__6; 341 Lib_IntVector_Intrinsics_vec128 v13 = v1__6; 342 Lib_IntVector_Intrinsics_vec128 v14 = v2__6; 343 Lib_IntVector_Intrinsics_vec128 v15 = v3__6; 344 k[0U] = v0; 345 k[1U] = v4; 346 k[2U] = v8; 347 k[3U] = v12; 348 k[4U] = v1; 349 k[5U] = v5; 350 k[6U] = v9; 351 k[7U] = v13; 352 k[8U] = v2; 353 k[9U] = v6; 354 k[10U] = v10; 355 k[11U] = v14; 356 k[12U] = v3; 357 k[13U] = v7; 358 k[14U] = v11; 359 k[15U] = v15; 360 KRML_MAYBE_FOR16(i0, 361 (uint32_t)0U, 362 (uint32_t)16U, 363 (uint32_t)1U, 364 Lib_IntVector_Intrinsics_vec128 365 x = Lib_IntVector_Intrinsics_vec128_load32_le(uu____1 + i0 * (uint32_t)16U); 366 Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i0]); 367 Lib_IntVector_Intrinsics_vec128_store32_le(uu____0 + i0 * (uint32_t)16U, y);); 368 } 369 if (rem1 > (uint32_t)0U) { 370 uint8_t *uu____2 = out + nb * (uint32_t)256U; 371 uint8_t plain[256U] = { 0U }; 372 memcpy(plain, text + nb * (uint32_t)256U, rem * sizeof(uint8_t)); 373 KRML_PRE_ALIGN(16) 374 Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; 375 chacha20_core_128(k, ctx, nb); 376 Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; 377 Lib_IntVector_Intrinsics_vec128 st1 = k[1U]; 378 Lib_IntVector_Intrinsics_vec128 st2 = k[2U]; 379 Lib_IntVector_Intrinsics_vec128 st3 = k[3U]; 380 Lib_IntVector_Intrinsics_vec128 st4 = k[4U]; 381 Lib_IntVector_Intrinsics_vec128 st5 = k[5U]; 382 Lib_IntVector_Intrinsics_vec128 st6 = k[6U]; 383 Lib_IntVector_Intrinsics_vec128 st7 = k[7U]; 384 Lib_IntVector_Intrinsics_vec128 st8 = k[8U]; 385 Lib_IntVector_Intrinsics_vec128 st9 = k[9U]; 386 Lib_IntVector_Intrinsics_vec128 st10 = k[10U]; 387 Lib_IntVector_Intrinsics_vec128 st11 = k[11U]; 388 Lib_IntVector_Intrinsics_vec128 st12 = k[12U]; 389 Lib_IntVector_Intrinsics_vec128 st13 = k[13U]; 390 Lib_IntVector_Intrinsics_vec128 st14 = k[14U]; 391 Lib_IntVector_Intrinsics_vec128 st15 = k[15U]; 392 Lib_IntVector_Intrinsics_vec128 393 v0_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st0, st1); 394 Lib_IntVector_Intrinsics_vec128 395 v1_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st0, st1); 396 Lib_IntVector_Intrinsics_vec128 397 v2_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st2, st3); 398 Lib_IntVector_Intrinsics_vec128 399 v3_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st2, st3); 400 Lib_IntVector_Intrinsics_vec128 401 v0__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_, v2_); 402 Lib_IntVector_Intrinsics_vec128 403 v1__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_, v2_); 404 Lib_IntVector_Intrinsics_vec128 405 v2__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_, v3_); 406 Lib_IntVector_Intrinsics_vec128 407 v3__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_, v3_); 408 Lib_IntVector_Intrinsics_vec128 v0__0 = v0__; 409 Lib_IntVector_Intrinsics_vec128 v2__0 = v2__; 410 Lib_IntVector_Intrinsics_vec128 v1__0 = v1__; 411 Lib_IntVector_Intrinsics_vec128 v3__0 = v3__; 412 Lib_IntVector_Intrinsics_vec128 v0 = v0__0; 413 Lib_IntVector_Intrinsics_vec128 v1 = v1__0; 414 Lib_IntVector_Intrinsics_vec128 v2 = v2__0; 415 Lib_IntVector_Intrinsics_vec128 v3 = v3__0; 416 Lib_IntVector_Intrinsics_vec128 417 v0_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st4, st5); 418 Lib_IntVector_Intrinsics_vec128 419 v1_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st4, st5); 420 Lib_IntVector_Intrinsics_vec128 421 v2_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st6, st7); 422 Lib_IntVector_Intrinsics_vec128 423 v3_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st6, st7); 424 Lib_IntVector_Intrinsics_vec128 425 v0__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_0, v2_0); 426 Lib_IntVector_Intrinsics_vec128 427 v1__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_0, v2_0); 428 Lib_IntVector_Intrinsics_vec128 429 v2__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_0, v3_0); 430 Lib_IntVector_Intrinsics_vec128 431 v3__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_0, v3_0); 432 Lib_IntVector_Intrinsics_vec128 v0__2 = v0__1; 433 Lib_IntVector_Intrinsics_vec128 v2__2 = v2__1; 434 Lib_IntVector_Intrinsics_vec128 v1__2 = v1__1; 435 Lib_IntVector_Intrinsics_vec128 v3__2 = v3__1; 436 Lib_IntVector_Intrinsics_vec128 v4 = v0__2; 437 Lib_IntVector_Intrinsics_vec128 v5 = v1__2; 438 Lib_IntVector_Intrinsics_vec128 v6 = v2__2; 439 Lib_IntVector_Intrinsics_vec128 v7 = v3__2; 440 Lib_IntVector_Intrinsics_vec128 441 v0_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st8, st9); 442 Lib_IntVector_Intrinsics_vec128 443 v1_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st8, st9); 444 Lib_IntVector_Intrinsics_vec128 445 v2_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st10, st11); 446 Lib_IntVector_Intrinsics_vec128 447 v3_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st10, st11); 448 Lib_IntVector_Intrinsics_vec128 449 v0__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_1, v2_1); 450 Lib_IntVector_Intrinsics_vec128 451 v1__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_1, v2_1); 452 Lib_IntVector_Intrinsics_vec128 453 v2__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_1, v3_1); 454 Lib_IntVector_Intrinsics_vec128 455 v3__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_1, v3_1); 456 Lib_IntVector_Intrinsics_vec128 v0__4 = v0__3; 457 Lib_IntVector_Intrinsics_vec128 v2__4 = v2__3; 458 Lib_IntVector_Intrinsics_vec128 v1__4 = v1__3; 459 Lib_IntVector_Intrinsics_vec128 v3__4 = v3__3; 460 Lib_IntVector_Intrinsics_vec128 v8 = v0__4; 461 Lib_IntVector_Intrinsics_vec128 v9 = v1__4; 462 Lib_IntVector_Intrinsics_vec128 v10 = v2__4; 463 Lib_IntVector_Intrinsics_vec128 v11 = v3__4; 464 Lib_IntVector_Intrinsics_vec128 465 v0_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st12, st13); 466 Lib_IntVector_Intrinsics_vec128 467 v1_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st12, st13); 468 Lib_IntVector_Intrinsics_vec128 469 v2_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st14, st15); 470 Lib_IntVector_Intrinsics_vec128 471 v3_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st14, st15); 472 Lib_IntVector_Intrinsics_vec128 473 v0__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_2, v2_2); 474 Lib_IntVector_Intrinsics_vec128 475 v1__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_2, v2_2); 476 Lib_IntVector_Intrinsics_vec128 477 v2__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_2, v3_2); 478 Lib_IntVector_Intrinsics_vec128 479 v3__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_2, v3_2); 480 Lib_IntVector_Intrinsics_vec128 v0__6 = v0__5; 481 Lib_IntVector_Intrinsics_vec128 v2__6 = v2__5; 482 Lib_IntVector_Intrinsics_vec128 v1__6 = v1__5; 483 Lib_IntVector_Intrinsics_vec128 v3__6 = v3__5; 484 Lib_IntVector_Intrinsics_vec128 v12 = v0__6; 485 Lib_IntVector_Intrinsics_vec128 v13 = v1__6; 486 Lib_IntVector_Intrinsics_vec128 v14 = v2__6; 487 Lib_IntVector_Intrinsics_vec128 v15 = v3__6; 488 k[0U] = v0; 489 k[1U] = v4; 490 k[2U] = v8; 491 k[3U] = v12; 492 k[4U] = v1; 493 k[5U] = v5; 494 k[6U] = v9; 495 k[7U] = v13; 496 k[8U] = v2; 497 k[9U] = v6; 498 k[10U] = v10; 499 k[11U] = v14; 500 k[12U] = v3; 501 k[13U] = v7; 502 k[14U] = v11; 503 k[15U] = v15; 504 KRML_MAYBE_FOR16(i, 505 (uint32_t)0U, 506 (uint32_t)16U, 507 (uint32_t)1U, 508 Lib_IntVector_Intrinsics_vec128 509 x = Lib_IntVector_Intrinsics_vec128_load32_le(plain + i * (uint32_t)16U); 510 Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i]); 511 Lib_IntVector_Intrinsics_vec128_store32_le(plain + i * (uint32_t)16U, y);); 512 memcpy(uu____2, plain, rem * sizeof(uint8_t)); 513 } 514 } 515 516 void 517 Hacl_Chacha20_Vec128_chacha20_decrypt_128( 518 uint32_t len, 519 uint8_t *out, 520 uint8_t *cipher, 521 uint8_t *key, 522 uint8_t *n, 523 uint32_t ctr) 524 { 525 KRML_PRE_ALIGN(16) 526 Lib_IntVector_Intrinsics_vec128 ctx[16U] KRML_POST_ALIGN(16) = { 0U }; 527 chacha20_init_128(ctx, key, n, ctr); 528 uint32_t rem = len % (uint32_t)256U; 529 uint32_t nb = len / (uint32_t)256U; 530 uint32_t rem1 = len % (uint32_t)256U; 531 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 532 uint8_t *uu____0 = out + i * (uint32_t)256U; 533 uint8_t *uu____1 = cipher + i * (uint32_t)256U; 534 KRML_PRE_ALIGN(16) 535 Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; 536 chacha20_core_128(k, ctx, i); 537 Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; 538 Lib_IntVector_Intrinsics_vec128 st1 = k[1U]; 539 Lib_IntVector_Intrinsics_vec128 st2 = k[2U]; 540 Lib_IntVector_Intrinsics_vec128 st3 = k[3U]; 541 Lib_IntVector_Intrinsics_vec128 st4 = k[4U]; 542 Lib_IntVector_Intrinsics_vec128 st5 = k[5U]; 543 Lib_IntVector_Intrinsics_vec128 st6 = k[6U]; 544 Lib_IntVector_Intrinsics_vec128 st7 = k[7U]; 545 Lib_IntVector_Intrinsics_vec128 st8 = k[8U]; 546 Lib_IntVector_Intrinsics_vec128 st9 = k[9U]; 547 Lib_IntVector_Intrinsics_vec128 st10 = k[10U]; 548 Lib_IntVector_Intrinsics_vec128 st11 = k[11U]; 549 Lib_IntVector_Intrinsics_vec128 st12 = k[12U]; 550 Lib_IntVector_Intrinsics_vec128 st13 = k[13U]; 551 Lib_IntVector_Intrinsics_vec128 st14 = k[14U]; 552 Lib_IntVector_Intrinsics_vec128 st15 = k[15U]; 553 Lib_IntVector_Intrinsics_vec128 554 v0_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st0, st1); 555 Lib_IntVector_Intrinsics_vec128 556 v1_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st0, st1); 557 Lib_IntVector_Intrinsics_vec128 558 v2_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st2, st3); 559 Lib_IntVector_Intrinsics_vec128 560 v3_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st2, st3); 561 Lib_IntVector_Intrinsics_vec128 562 v0__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_, v2_); 563 Lib_IntVector_Intrinsics_vec128 564 v1__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_, v2_); 565 Lib_IntVector_Intrinsics_vec128 566 v2__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_, v3_); 567 Lib_IntVector_Intrinsics_vec128 568 v3__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_, v3_); 569 Lib_IntVector_Intrinsics_vec128 v0__0 = v0__; 570 Lib_IntVector_Intrinsics_vec128 v2__0 = v2__; 571 Lib_IntVector_Intrinsics_vec128 v1__0 = v1__; 572 Lib_IntVector_Intrinsics_vec128 v3__0 = v3__; 573 Lib_IntVector_Intrinsics_vec128 v0 = v0__0; 574 Lib_IntVector_Intrinsics_vec128 v1 = v1__0; 575 Lib_IntVector_Intrinsics_vec128 v2 = v2__0; 576 Lib_IntVector_Intrinsics_vec128 v3 = v3__0; 577 Lib_IntVector_Intrinsics_vec128 578 v0_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st4, st5); 579 Lib_IntVector_Intrinsics_vec128 580 v1_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st4, st5); 581 Lib_IntVector_Intrinsics_vec128 582 v2_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st6, st7); 583 Lib_IntVector_Intrinsics_vec128 584 v3_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st6, st7); 585 Lib_IntVector_Intrinsics_vec128 586 v0__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_0, v2_0); 587 Lib_IntVector_Intrinsics_vec128 588 v1__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_0, v2_0); 589 Lib_IntVector_Intrinsics_vec128 590 v2__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_0, v3_0); 591 Lib_IntVector_Intrinsics_vec128 592 v3__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_0, v3_0); 593 Lib_IntVector_Intrinsics_vec128 v0__2 = v0__1; 594 Lib_IntVector_Intrinsics_vec128 v2__2 = v2__1; 595 Lib_IntVector_Intrinsics_vec128 v1__2 = v1__1; 596 Lib_IntVector_Intrinsics_vec128 v3__2 = v3__1; 597 Lib_IntVector_Intrinsics_vec128 v4 = v0__2; 598 Lib_IntVector_Intrinsics_vec128 v5 = v1__2; 599 Lib_IntVector_Intrinsics_vec128 v6 = v2__2; 600 Lib_IntVector_Intrinsics_vec128 v7 = v3__2; 601 Lib_IntVector_Intrinsics_vec128 602 v0_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st8, st9); 603 Lib_IntVector_Intrinsics_vec128 604 v1_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st8, st9); 605 Lib_IntVector_Intrinsics_vec128 606 v2_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st10, st11); 607 Lib_IntVector_Intrinsics_vec128 608 v3_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st10, st11); 609 Lib_IntVector_Intrinsics_vec128 610 v0__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_1, v2_1); 611 Lib_IntVector_Intrinsics_vec128 612 v1__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_1, v2_1); 613 Lib_IntVector_Intrinsics_vec128 614 v2__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_1, v3_1); 615 Lib_IntVector_Intrinsics_vec128 616 v3__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_1, v3_1); 617 Lib_IntVector_Intrinsics_vec128 v0__4 = v0__3; 618 Lib_IntVector_Intrinsics_vec128 v2__4 = v2__3; 619 Lib_IntVector_Intrinsics_vec128 v1__4 = v1__3; 620 Lib_IntVector_Intrinsics_vec128 v3__4 = v3__3; 621 Lib_IntVector_Intrinsics_vec128 v8 = v0__4; 622 Lib_IntVector_Intrinsics_vec128 v9 = v1__4; 623 Lib_IntVector_Intrinsics_vec128 v10 = v2__4; 624 Lib_IntVector_Intrinsics_vec128 v11 = v3__4; 625 Lib_IntVector_Intrinsics_vec128 626 v0_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st12, st13); 627 Lib_IntVector_Intrinsics_vec128 628 v1_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st12, st13); 629 Lib_IntVector_Intrinsics_vec128 630 v2_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st14, st15); 631 Lib_IntVector_Intrinsics_vec128 632 v3_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st14, st15); 633 Lib_IntVector_Intrinsics_vec128 634 v0__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_2, v2_2); 635 Lib_IntVector_Intrinsics_vec128 636 v1__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_2, v2_2); 637 Lib_IntVector_Intrinsics_vec128 638 v2__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_2, v3_2); 639 Lib_IntVector_Intrinsics_vec128 640 v3__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_2, v3_2); 641 Lib_IntVector_Intrinsics_vec128 v0__6 = v0__5; 642 Lib_IntVector_Intrinsics_vec128 v2__6 = v2__5; 643 Lib_IntVector_Intrinsics_vec128 v1__6 = v1__5; 644 Lib_IntVector_Intrinsics_vec128 v3__6 = v3__5; 645 Lib_IntVector_Intrinsics_vec128 v12 = v0__6; 646 Lib_IntVector_Intrinsics_vec128 v13 = v1__6; 647 Lib_IntVector_Intrinsics_vec128 v14 = v2__6; 648 Lib_IntVector_Intrinsics_vec128 v15 = v3__6; 649 k[0U] = v0; 650 k[1U] = v4; 651 k[2U] = v8; 652 k[3U] = v12; 653 k[4U] = v1; 654 k[5U] = v5; 655 k[6U] = v9; 656 k[7U] = v13; 657 k[8U] = v2; 658 k[9U] = v6; 659 k[10U] = v10; 660 k[11U] = v14; 661 k[12U] = v3; 662 k[13U] = v7; 663 k[14U] = v11; 664 k[15U] = v15; 665 KRML_MAYBE_FOR16(i0, 666 (uint32_t)0U, 667 (uint32_t)16U, 668 (uint32_t)1U, 669 Lib_IntVector_Intrinsics_vec128 670 x = Lib_IntVector_Intrinsics_vec128_load32_le(uu____1 + i0 * (uint32_t)16U); 671 Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i0]); 672 Lib_IntVector_Intrinsics_vec128_store32_le(uu____0 + i0 * (uint32_t)16U, y);); 673 } 674 if (rem1 > (uint32_t)0U) { 675 uint8_t *uu____2 = out + nb * (uint32_t)256U; 676 uint8_t plain[256U] = { 0U }; 677 memcpy(plain, cipher + nb * (uint32_t)256U, rem * sizeof(uint8_t)); 678 KRML_PRE_ALIGN(16) 679 Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U }; 680 chacha20_core_128(k, ctx, nb); 681 Lib_IntVector_Intrinsics_vec128 st0 = k[0U]; 682 Lib_IntVector_Intrinsics_vec128 st1 = k[1U]; 683 Lib_IntVector_Intrinsics_vec128 st2 = k[2U]; 684 Lib_IntVector_Intrinsics_vec128 st3 = k[3U]; 685 Lib_IntVector_Intrinsics_vec128 st4 = k[4U]; 686 Lib_IntVector_Intrinsics_vec128 st5 = k[5U]; 687 Lib_IntVector_Intrinsics_vec128 st6 = k[6U]; 688 Lib_IntVector_Intrinsics_vec128 st7 = k[7U]; 689 Lib_IntVector_Intrinsics_vec128 st8 = k[8U]; 690 Lib_IntVector_Intrinsics_vec128 st9 = k[9U]; 691 Lib_IntVector_Intrinsics_vec128 st10 = k[10U]; 692 Lib_IntVector_Intrinsics_vec128 st11 = k[11U]; 693 Lib_IntVector_Intrinsics_vec128 st12 = k[12U]; 694 Lib_IntVector_Intrinsics_vec128 st13 = k[13U]; 695 Lib_IntVector_Intrinsics_vec128 st14 = k[14U]; 696 Lib_IntVector_Intrinsics_vec128 st15 = k[15U]; 697 Lib_IntVector_Intrinsics_vec128 698 v0_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st0, st1); 699 Lib_IntVector_Intrinsics_vec128 700 v1_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st0, st1); 701 Lib_IntVector_Intrinsics_vec128 702 v2_ = Lib_IntVector_Intrinsics_vec128_interleave_low32(st2, st3); 703 Lib_IntVector_Intrinsics_vec128 704 v3_ = Lib_IntVector_Intrinsics_vec128_interleave_high32(st2, st3); 705 Lib_IntVector_Intrinsics_vec128 706 v0__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_, v2_); 707 Lib_IntVector_Intrinsics_vec128 708 v1__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_, v2_); 709 Lib_IntVector_Intrinsics_vec128 710 v2__ = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_, v3_); 711 Lib_IntVector_Intrinsics_vec128 712 v3__ = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_, v3_); 713 Lib_IntVector_Intrinsics_vec128 v0__0 = v0__; 714 Lib_IntVector_Intrinsics_vec128 v2__0 = v2__; 715 Lib_IntVector_Intrinsics_vec128 v1__0 = v1__; 716 Lib_IntVector_Intrinsics_vec128 v3__0 = v3__; 717 Lib_IntVector_Intrinsics_vec128 v0 = v0__0; 718 Lib_IntVector_Intrinsics_vec128 v1 = v1__0; 719 Lib_IntVector_Intrinsics_vec128 v2 = v2__0; 720 Lib_IntVector_Intrinsics_vec128 v3 = v3__0; 721 Lib_IntVector_Intrinsics_vec128 722 v0_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st4, st5); 723 Lib_IntVector_Intrinsics_vec128 724 v1_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st4, st5); 725 Lib_IntVector_Intrinsics_vec128 726 v2_0 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st6, st7); 727 Lib_IntVector_Intrinsics_vec128 728 v3_0 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st6, st7); 729 Lib_IntVector_Intrinsics_vec128 730 v0__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_0, v2_0); 731 Lib_IntVector_Intrinsics_vec128 732 v1__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_0, v2_0); 733 Lib_IntVector_Intrinsics_vec128 734 v2__1 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_0, v3_0); 735 Lib_IntVector_Intrinsics_vec128 736 v3__1 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_0, v3_0); 737 Lib_IntVector_Intrinsics_vec128 v0__2 = v0__1; 738 Lib_IntVector_Intrinsics_vec128 v2__2 = v2__1; 739 Lib_IntVector_Intrinsics_vec128 v1__2 = v1__1; 740 Lib_IntVector_Intrinsics_vec128 v3__2 = v3__1; 741 Lib_IntVector_Intrinsics_vec128 v4 = v0__2; 742 Lib_IntVector_Intrinsics_vec128 v5 = v1__2; 743 Lib_IntVector_Intrinsics_vec128 v6 = v2__2; 744 Lib_IntVector_Intrinsics_vec128 v7 = v3__2; 745 Lib_IntVector_Intrinsics_vec128 746 v0_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st8, st9); 747 Lib_IntVector_Intrinsics_vec128 748 v1_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st8, st9); 749 Lib_IntVector_Intrinsics_vec128 750 v2_1 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st10, st11); 751 Lib_IntVector_Intrinsics_vec128 752 v3_1 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st10, st11); 753 Lib_IntVector_Intrinsics_vec128 754 v0__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_1, v2_1); 755 Lib_IntVector_Intrinsics_vec128 756 v1__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_1, v2_1); 757 Lib_IntVector_Intrinsics_vec128 758 v2__3 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_1, v3_1); 759 Lib_IntVector_Intrinsics_vec128 760 v3__3 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_1, v3_1); 761 Lib_IntVector_Intrinsics_vec128 v0__4 = v0__3; 762 Lib_IntVector_Intrinsics_vec128 v2__4 = v2__3; 763 Lib_IntVector_Intrinsics_vec128 v1__4 = v1__3; 764 Lib_IntVector_Intrinsics_vec128 v3__4 = v3__3; 765 Lib_IntVector_Intrinsics_vec128 v8 = v0__4; 766 Lib_IntVector_Intrinsics_vec128 v9 = v1__4; 767 Lib_IntVector_Intrinsics_vec128 v10 = v2__4; 768 Lib_IntVector_Intrinsics_vec128 v11 = v3__4; 769 Lib_IntVector_Intrinsics_vec128 770 v0_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st12, st13); 771 Lib_IntVector_Intrinsics_vec128 772 v1_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st12, st13); 773 Lib_IntVector_Intrinsics_vec128 774 v2_2 = Lib_IntVector_Intrinsics_vec128_interleave_low32(st14, st15); 775 Lib_IntVector_Intrinsics_vec128 776 v3_2 = Lib_IntVector_Intrinsics_vec128_interleave_high32(st14, st15); 777 Lib_IntVector_Intrinsics_vec128 778 v0__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v0_2, v2_2); 779 Lib_IntVector_Intrinsics_vec128 780 v1__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v0_2, v2_2); 781 Lib_IntVector_Intrinsics_vec128 782 v2__5 = Lib_IntVector_Intrinsics_vec128_interleave_low64(v1_2, v3_2); 783 Lib_IntVector_Intrinsics_vec128 784 v3__5 = Lib_IntVector_Intrinsics_vec128_interleave_high64(v1_2, v3_2); 785 Lib_IntVector_Intrinsics_vec128 v0__6 = v0__5; 786 Lib_IntVector_Intrinsics_vec128 v2__6 = v2__5; 787 Lib_IntVector_Intrinsics_vec128 v1__6 = v1__5; 788 Lib_IntVector_Intrinsics_vec128 v3__6 = v3__5; 789 Lib_IntVector_Intrinsics_vec128 v12 = v0__6; 790 Lib_IntVector_Intrinsics_vec128 v13 = v1__6; 791 Lib_IntVector_Intrinsics_vec128 v14 = v2__6; 792 Lib_IntVector_Intrinsics_vec128 v15 = v3__6; 793 k[0U] = v0; 794 k[1U] = v4; 795 k[2U] = v8; 796 k[3U] = v12; 797 k[4U] = v1; 798 k[5U] = v5; 799 k[6U] = v9; 800 k[7U] = v13; 801 k[8U] = v2; 802 k[9U] = v6; 803 k[10U] = v10; 804 k[11U] = v14; 805 k[12U] = v3; 806 k[13U] = v7; 807 k[14U] = v11; 808 k[15U] = v15; 809 KRML_MAYBE_FOR16(i, 810 (uint32_t)0U, 811 (uint32_t)16U, 812 (uint32_t)1U, 813 Lib_IntVector_Intrinsics_vec128 814 x = Lib_IntVector_Intrinsics_vec128_load32_le(plain + i * (uint32_t)16U); 815 Lib_IntVector_Intrinsics_vec128 y = Lib_IntVector_Intrinsics_vec128_xor(x, k[i]); 816 Lib_IntVector_Intrinsics_vec128_store32_le(plain + i * (uint32_t)16U, y);); 817 memcpy(uu____2, plain, rem * sizeof(uint8_t)); 818 } 819 }