Hacl_Chacha20_Vec256.c (65595B)
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_Vec256.h" 26 27 #include "internal/Hacl_Chacha20.h" 28 #include "libintvector.h" 29 30 static inline void 31 double_round_256(Lib_IntVector_Intrinsics_vec256 *st) 32 { 33 st[0U] = Lib_IntVector_Intrinsics_vec256_add32(st[0U], st[4U]); 34 Lib_IntVector_Intrinsics_vec256 std = Lib_IntVector_Intrinsics_vec256_xor(st[12U], st[0U]); 35 st[12U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std, (uint32_t)16U); 36 st[8U] = Lib_IntVector_Intrinsics_vec256_add32(st[8U], st[12U]); 37 Lib_IntVector_Intrinsics_vec256 std0 = Lib_IntVector_Intrinsics_vec256_xor(st[4U], st[8U]); 38 st[4U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std0, (uint32_t)12U); 39 st[0U] = Lib_IntVector_Intrinsics_vec256_add32(st[0U], st[4U]); 40 Lib_IntVector_Intrinsics_vec256 std1 = Lib_IntVector_Intrinsics_vec256_xor(st[12U], st[0U]); 41 st[12U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std1, (uint32_t)8U); 42 st[8U] = Lib_IntVector_Intrinsics_vec256_add32(st[8U], st[12U]); 43 Lib_IntVector_Intrinsics_vec256 std2 = Lib_IntVector_Intrinsics_vec256_xor(st[4U], st[8U]); 44 st[4U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std2, (uint32_t)7U); 45 st[1U] = Lib_IntVector_Intrinsics_vec256_add32(st[1U], st[5U]); 46 Lib_IntVector_Intrinsics_vec256 std3 = Lib_IntVector_Intrinsics_vec256_xor(st[13U], st[1U]); 47 st[13U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std3, (uint32_t)16U); 48 st[9U] = Lib_IntVector_Intrinsics_vec256_add32(st[9U], st[13U]); 49 Lib_IntVector_Intrinsics_vec256 std4 = Lib_IntVector_Intrinsics_vec256_xor(st[5U], st[9U]); 50 st[5U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std4, (uint32_t)12U); 51 st[1U] = Lib_IntVector_Intrinsics_vec256_add32(st[1U], st[5U]); 52 Lib_IntVector_Intrinsics_vec256 std5 = Lib_IntVector_Intrinsics_vec256_xor(st[13U], st[1U]); 53 st[13U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std5, (uint32_t)8U); 54 st[9U] = Lib_IntVector_Intrinsics_vec256_add32(st[9U], st[13U]); 55 Lib_IntVector_Intrinsics_vec256 std6 = Lib_IntVector_Intrinsics_vec256_xor(st[5U], st[9U]); 56 st[5U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std6, (uint32_t)7U); 57 st[2U] = Lib_IntVector_Intrinsics_vec256_add32(st[2U], st[6U]); 58 Lib_IntVector_Intrinsics_vec256 std7 = Lib_IntVector_Intrinsics_vec256_xor(st[14U], st[2U]); 59 st[14U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std7, (uint32_t)16U); 60 st[10U] = Lib_IntVector_Intrinsics_vec256_add32(st[10U], st[14U]); 61 Lib_IntVector_Intrinsics_vec256 std8 = Lib_IntVector_Intrinsics_vec256_xor(st[6U], st[10U]); 62 st[6U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std8, (uint32_t)12U); 63 st[2U] = Lib_IntVector_Intrinsics_vec256_add32(st[2U], st[6U]); 64 Lib_IntVector_Intrinsics_vec256 std9 = Lib_IntVector_Intrinsics_vec256_xor(st[14U], st[2U]); 65 st[14U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std9, (uint32_t)8U); 66 st[10U] = Lib_IntVector_Intrinsics_vec256_add32(st[10U], st[14U]); 67 Lib_IntVector_Intrinsics_vec256 std10 = Lib_IntVector_Intrinsics_vec256_xor(st[6U], st[10U]); 68 st[6U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std10, (uint32_t)7U); 69 st[3U] = Lib_IntVector_Intrinsics_vec256_add32(st[3U], st[7U]); 70 Lib_IntVector_Intrinsics_vec256 std11 = Lib_IntVector_Intrinsics_vec256_xor(st[15U], st[3U]); 71 st[15U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std11, (uint32_t)16U); 72 st[11U] = Lib_IntVector_Intrinsics_vec256_add32(st[11U], st[15U]); 73 Lib_IntVector_Intrinsics_vec256 std12 = Lib_IntVector_Intrinsics_vec256_xor(st[7U], st[11U]); 74 st[7U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std12, (uint32_t)12U); 75 st[3U] = Lib_IntVector_Intrinsics_vec256_add32(st[3U], st[7U]); 76 Lib_IntVector_Intrinsics_vec256 std13 = Lib_IntVector_Intrinsics_vec256_xor(st[15U], st[3U]); 77 st[15U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std13, (uint32_t)8U); 78 st[11U] = Lib_IntVector_Intrinsics_vec256_add32(st[11U], st[15U]); 79 Lib_IntVector_Intrinsics_vec256 std14 = Lib_IntVector_Intrinsics_vec256_xor(st[7U], st[11U]); 80 st[7U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std14, (uint32_t)7U); 81 st[0U] = Lib_IntVector_Intrinsics_vec256_add32(st[0U], st[5U]); 82 Lib_IntVector_Intrinsics_vec256 std15 = Lib_IntVector_Intrinsics_vec256_xor(st[15U], st[0U]); 83 st[15U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std15, (uint32_t)16U); 84 st[10U] = Lib_IntVector_Intrinsics_vec256_add32(st[10U], st[15U]); 85 Lib_IntVector_Intrinsics_vec256 std16 = Lib_IntVector_Intrinsics_vec256_xor(st[5U], st[10U]); 86 st[5U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std16, (uint32_t)12U); 87 st[0U] = Lib_IntVector_Intrinsics_vec256_add32(st[0U], st[5U]); 88 Lib_IntVector_Intrinsics_vec256 std17 = Lib_IntVector_Intrinsics_vec256_xor(st[15U], st[0U]); 89 st[15U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std17, (uint32_t)8U); 90 st[10U] = Lib_IntVector_Intrinsics_vec256_add32(st[10U], st[15U]); 91 Lib_IntVector_Intrinsics_vec256 std18 = Lib_IntVector_Intrinsics_vec256_xor(st[5U], st[10U]); 92 st[5U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std18, (uint32_t)7U); 93 st[1U] = Lib_IntVector_Intrinsics_vec256_add32(st[1U], st[6U]); 94 Lib_IntVector_Intrinsics_vec256 std19 = Lib_IntVector_Intrinsics_vec256_xor(st[12U], st[1U]); 95 st[12U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std19, (uint32_t)16U); 96 st[11U] = Lib_IntVector_Intrinsics_vec256_add32(st[11U], st[12U]); 97 Lib_IntVector_Intrinsics_vec256 std20 = Lib_IntVector_Intrinsics_vec256_xor(st[6U], st[11U]); 98 st[6U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std20, (uint32_t)12U); 99 st[1U] = Lib_IntVector_Intrinsics_vec256_add32(st[1U], st[6U]); 100 Lib_IntVector_Intrinsics_vec256 std21 = Lib_IntVector_Intrinsics_vec256_xor(st[12U], st[1U]); 101 st[12U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std21, (uint32_t)8U); 102 st[11U] = Lib_IntVector_Intrinsics_vec256_add32(st[11U], st[12U]); 103 Lib_IntVector_Intrinsics_vec256 std22 = Lib_IntVector_Intrinsics_vec256_xor(st[6U], st[11U]); 104 st[6U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std22, (uint32_t)7U); 105 st[2U] = Lib_IntVector_Intrinsics_vec256_add32(st[2U], st[7U]); 106 Lib_IntVector_Intrinsics_vec256 std23 = Lib_IntVector_Intrinsics_vec256_xor(st[13U], st[2U]); 107 st[13U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std23, (uint32_t)16U); 108 st[8U] = Lib_IntVector_Intrinsics_vec256_add32(st[8U], st[13U]); 109 Lib_IntVector_Intrinsics_vec256 std24 = Lib_IntVector_Intrinsics_vec256_xor(st[7U], st[8U]); 110 st[7U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std24, (uint32_t)12U); 111 st[2U] = Lib_IntVector_Intrinsics_vec256_add32(st[2U], st[7U]); 112 Lib_IntVector_Intrinsics_vec256 std25 = Lib_IntVector_Intrinsics_vec256_xor(st[13U], st[2U]); 113 st[13U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std25, (uint32_t)8U); 114 st[8U] = Lib_IntVector_Intrinsics_vec256_add32(st[8U], st[13U]); 115 Lib_IntVector_Intrinsics_vec256 std26 = Lib_IntVector_Intrinsics_vec256_xor(st[7U], st[8U]); 116 st[7U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std26, (uint32_t)7U); 117 st[3U] = Lib_IntVector_Intrinsics_vec256_add32(st[3U], st[4U]); 118 Lib_IntVector_Intrinsics_vec256 std27 = Lib_IntVector_Intrinsics_vec256_xor(st[14U], st[3U]); 119 st[14U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std27, (uint32_t)16U); 120 st[9U] = Lib_IntVector_Intrinsics_vec256_add32(st[9U], st[14U]); 121 Lib_IntVector_Intrinsics_vec256 std28 = Lib_IntVector_Intrinsics_vec256_xor(st[4U], st[9U]); 122 st[4U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std28, (uint32_t)12U); 123 st[3U] = Lib_IntVector_Intrinsics_vec256_add32(st[3U], st[4U]); 124 Lib_IntVector_Intrinsics_vec256 std29 = Lib_IntVector_Intrinsics_vec256_xor(st[14U], st[3U]); 125 st[14U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std29, (uint32_t)8U); 126 st[9U] = Lib_IntVector_Intrinsics_vec256_add32(st[9U], st[14U]); 127 Lib_IntVector_Intrinsics_vec256 std30 = Lib_IntVector_Intrinsics_vec256_xor(st[4U], st[9U]); 128 st[4U] = Lib_IntVector_Intrinsics_vec256_rotate_left32(std30, (uint32_t)7U); 129 } 130 131 static inline void 132 chacha20_core_256( 133 Lib_IntVector_Intrinsics_vec256 *k, 134 Lib_IntVector_Intrinsics_vec256 *ctx, 135 uint32_t ctr) 136 { 137 memcpy(k, ctx, (uint32_t)16U * sizeof(Lib_IntVector_Intrinsics_vec256)); 138 uint32_t ctr_u32 = (uint32_t)8U * ctr; 139 Lib_IntVector_Intrinsics_vec256 cv = Lib_IntVector_Intrinsics_vec256_load32(ctr_u32); 140 k[12U] = Lib_IntVector_Intrinsics_vec256_add32(k[12U], cv); 141 double_round_256(k); 142 double_round_256(k); 143 double_round_256(k); 144 double_round_256(k); 145 double_round_256(k); 146 double_round_256(k); 147 double_round_256(k); 148 double_round_256(k); 149 double_round_256(k); 150 double_round_256(k); 151 KRML_MAYBE_FOR16(i, 152 (uint32_t)0U, 153 (uint32_t)16U, 154 (uint32_t)1U, 155 Lib_IntVector_Intrinsics_vec256 *os = k; 156 Lib_IntVector_Intrinsics_vec256 x = Lib_IntVector_Intrinsics_vec256_add32(k[i], ctx[i]); 157 os[i] = x;); 158 k[12U] = Lib_IntVector_Intrinsics_vec256_add32(k[12U], cv); 159 } 160 161 static inline void 162 chacha20_init_256(Lib_IntVector_Intrinsics_vec256 *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_vec256 *os = ctx; 198 uint32_t x = ctx1[i]; 199 Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_load32(x); 200 os[i] = x0;); 201 Lib_IntVector_Intrinsics_vec256 202 ctr1 = 203 Lib_IntVector_Intrinsics_vec256_load32s((uint32_t)0U, 204 (uint32_t)1U, 205 (uint32_t)2U, 206 (uint32_t)3U, 207 (uint32_t)4U, 208 (uint32_t)5U, 209 (uint32_t)6U, 210 (uint32_t)7U); 211 Lib_IntVector_Intrinsics_vec256 c12 = ctx[12U]; 212 ctx[12U] = Lib_IntVector_Intrinsics_vec256_add32(c12, ctr1); 213 } 214 215 void 216 Hacl_Chacha20_Vec256_chacha20_encrypt_256( 217 uint32_t len, 218 uint8_t *out, 219 uint8_t *text, 220 uint8_t *key, 221 uint8_t *n, 222 uint32_t ctr) 223 { 224 KRML_PRE_ALIGN(32) 225 Lib_IntVector_Intrinsics_vec256 ctx[16U] KRML_POST_ALIGN(32) = { 0U }; 226 chacha20_init_256(ctx, key, n, ctr); 227 uint32_t rem = len % (uint32_t)512U; 228 uint32_t nb = len / (uint32_t)512U; 229 uint32_t rem1 = len % (uint32_t)512U; 230 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 231 uint8_t *uu____0 = out + i * (uint32_t)512U; 232 uint8_t *uu____1 = text + i * (uint32_t)512U; 233 KRML_PRE_ALIGN(32) 234 Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; 235 chacha20_core_256(k, ctx, i); 236 Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; 237 Lib_IntVector_Intrinsics_vec256 st1 = k[1U]; 238 Lib_IntVector_Intrinsics_vec256 st2 = k[2U]; 239 Lib_IntVector_Intrinsics_vec256 st3 = k[3U]; 240 Lib_IntVector_Intrinsics_vec256 st4 = k[4U]; 241 Lib_IntVector_Intrinsics_vec256 st5 = k[5U]; 242 Lib_IntVector_Intrinsics_vec256 st6 = k[6U]; 243 Lib_IntVector_Intrinsics_vec256 st7 = k[7U]; 244 Lib_IntVector_Intrinsics_vec256 st8 = k[8U]; 245 Lib_IntVector_Intrinsics_vec256 st9 = k[9U]; 246 Lib_IntVector_Intrinsics_vec256 st10 = k[10U]; 247 Lib_IntVector_Intrinsics_vec256 st11 = k[11U]; 248 Lib_IntVector_Intrinsics_vec256 st12 = k[12U]; 249 Lib_IntVector_Intrinsics_vec256 st13 = k[13U]; 250 Lib_IntVector_Intrinsics_vec256 st14 = k[14U]; 251 Lib_IntVector_Intrinsics_vec256 st15 = k[15U]; 252 Lib_IntVector_Intrinsics_vec256 v00 = st0; 253 Lib_IntVector_Intrinsics_vec256 v16 = st1; 254 Lib_IntVector_Intrinsics_vec256 v20 = st2; 255 Lib_IntVector_Intrinsics_vec256 v30 = st3; 256 Lib_IntVector_Intrinsics_vec256 v40 = st4; 257 Lib_IntVector_Intrinsics_vec256 v50 = st5; 258 Lib_IntVector_Intrinsics_vec256 v60 = st6; 259 Lib_IntVector_Intrinsics_vec256 v70 = st7; 260 Lib_IntVector_Intrinsics_vec256 261 v0_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v00, v16); 262 Lib_IntVector_Intrinsics_vec256 263 v1_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v00, v16); 264 Lib_IntVector_Intrinsics_vec256 265 v2_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v20, v30); 266 Lib_IntVector_Intrinsics_vec256 267 v3_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v20, v30); 268 Lib_IntVector_Intrinsics_vec256 269 v4_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v40, v50); 270 Lib_IntVector_Intrinsics_vec256 271 v5_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v40, v50); 272 Lib_IntVector_Intrinsics_vec256 273 v6_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v60, v70); 274 Lib_IntVector_Intrinsics_vec256 275 v7_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v60, v70); 276 Lib_IntVector_Intrinsics_vec256 v0_0 = v0_; 277 Lib_IntVector_Intrinsics_vec256 v1_0 = v1_; 278 Lib_IntVector_Intrinsics_vec256 v2_0 = v2_; 279 Lib_IntVector_Intrinsics_vec256 v3_0 = v3_; 280 Lib_IntVector_Intrinsics_vec256 v4_0 = v4_; 281 Lib_IntVector_Intrinsics_vec256 v5_0 = v5_; 282 Lib_IntVector_Intrinsics_vec256 v6_0 = v6_; 283 Lib_IntVector_Intrinsics_vec256 v7_0 = v7_; 284 Lib_IntVector_Intrinsics_vec256 285 v0_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_0, v2_0); 286 Lib_IntVector_Intrinsics_vec256 287 v2_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_0, v2_0); 288 Lib_IntVector_Intrinsics_vec256 289 v1_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_0, v3_0); 290 Lib_IntVector_Intrinsics_vec256 291 v3_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_0, v3_0); 292 Lib_IntVector_Intrinsics_vec256 293 v4_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_0, v6_0); 294 Lib_IntVector_Intrinsics_vec256 295 v6_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_0, v6_0); 296 Lib_IntVector_Intrinsics_vec256 297 v5_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_0, v7_0); 298 Lib_IntVector_Intrinsics_vec256 299 v7_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_0, v7_0); 300 Lib_IntVector_Intrinsics_vec256 v0_10 = v0_1; 301 Lib_IntVector_Intrinsics_vec256 v1_10 = v1_1; 302 Lib_IntVector_Intrinsics_vec256 v2_10 = v2_1; 303 Lib_IntVector_Intrinsics_vec256 v3_10 = v3_1; 304 Lib_IntVector_Intrinsics_vec256 v4_10 = v4_1; 305 Lib_IntVector_Intrinsics_vec256 v5_10 = v5_1; 306 Lib_IntVector_Intrinsics_vec256 v6_10 = v6_1; 307 Lib_IntVector_Intrinsics_vec256 v7_10 = v7_1; 308 Lib_IntVector_Intrinsics_vec256 309 v0_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_10, v4_10); 310 Lib_IntVector_Intrinsics_vec256 311 v4_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_10, v4_10); 312 Lib_IntVector_Intrinsics_vec256 313 v1_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_10, v5_10); 314 Lib_IntVector_Intrinsics_vec256 315 v5_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_10, v5_10); 316 Lib_IntVector_Intrinsics_vec256 317 v2_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_10, v6_10); 318 Lib_IntVector_Intrinsics_vec256 319 v6_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_10, v6_10); 320 Lib_IntVector_Intrinsics_vec256 321 v3_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_10, v7_10); 322 Lib_IntVector_Intrinsics_vec256 323 v7_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_10, v7_10); 324 Lib_IntVector_Intrinsics_vec256 v0_20 = v0_2; 325 Lib_IntVector_Intrinsics_vec256 v1_20 = v1_2; 326 Lib_IntVector_Intrinsics_vec256 v2_20 = v2_2; 327 Lib_IntVector_Intrinsics_vec256 v3_20 = v3_2; 328 Lib_IntVector_Intrinsics_vec256 v4_20 = v4_2; 329 Lib_IntVector_Intrinsics_vec256 v5_20 = v5_2; 330 Lib_IntVector_Intrinsics_vec256 v6_20 = v6_2; 331 Lib_IntVector_Intrinsics_vec256 v7_20 = v7_2; 332 Lib_IntVector_Intrinsics_vec256 v0_3 = v0_20; 333 Lib_IntVector_Intrinsics_vec256 v1_3 = v1_20; 334 Lib_IntVector_Intrinsics_vec256 v2_3 = v2_20; 335 Lib_IntVector_Intrinsics_vec256 v3_3 = v3_20; 336 Lib_IntVector_Intrinsics_vec256 v4_3 = v4_20; 337 Lib_IntVector_Intrinsics_vec256 v5_3 = v5_20; 338 Lib_IntVector_Intrinsics_vec256 v6_3 = v6_20; 339 Lib_IntVector_Intrinsics_vec256 v7_3 = v7_20; 340 Lib_IntVector_Intrinsics_vec256 v0 = v0_3; 341 Lib_IntVector_Intrinsics_vec256 v1 = v2_3; 342 Lib_IntVector_Intrinsics_vec256 v2 = v1_3; 343 Lib_IntVector_Intrinsics_vec256 v3 = v3_3; 344 Lib_IntVector_Intrinsics_vec256 v4 = v4_3; 345 Lib_IntVector_Intrinsics_vec256 v5 = v6_3; 346 Lib_IntVector_Intrinsics_vec256 v6 = v5_3; 347 Lib_IntVector_Intrinsics_vec256 v7 = v7_3; 348 Lib_IntVector_Intrinsics_vec256 v01 = st8; 349 Lib_IntVector_Intrinsics_vec256 v110 = st9; 350 Lib_IntVector_Intrinsics_vec256 v21 = st10; 351 Lib_IntVector_Intrinsics_vec256 v31 = st11; 352 Lib_IntVector_Intrinsics_vec256 v41 = st12; 353 Lib_IntVector_Intrinsics_vec256 v51 = st13; 354 Lib_IntVector_Intrinsics_vec256 v61 = st14; 355 Lib_IntVector_Intrinsics_vec256 v71 = st15; 356 Lib_IntVector_Intrinsics_vec256 357 v0_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v01, v110); 358 Lib_IntVector_Intrinsics_vec256 359 v1_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v01, v110); 360 Lib_IntVector_Intrinsics_vec256 361 v2_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v21, v31); 362 Lib_IntVector_Intrinsics_vec256 363 v3_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v21, v31); 364 Lib_IntVector_Intrinsics_vec256 365 v4_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v41, v51); 366 Lib_IntVector_Intrinsics_vec256 367 v5_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v41, v51); 368 Lib_IntVector_Intrinsics_vec256 369 v6_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v61, v71); 370 Lib_IntVector_Intrinsics_vec256 371 v7_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v61, v71); 372 Lib_IntVector_Intrinsics_vec256 v0_5 = v0_4; 373 Lib_IntVector_Intrinsics_vec256 v1_5 = v1_4; 374 Lib_IntVector_Intrinsics_vec256 v2_5 = v2_4; 375 Lib_IntVector_Intrinsics_vec256 v3_5 = v3_4; 376 Lib_IntVector_Intrinsics_vec256 v4_5 = v4_4; 377 Lib_IntVector_Intrinsics_vec256 v5_5 = v5_4; 378 Lib_IntVector_Intrinsics_vec256 v6_5 = v6_4; 379 Lib_IntVector_Intrinsics_vec256 v7_5 = v7_4; 380 Lib_IntVector_Intrinsics_vec256 381 v0_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_5, v2_5); 382 Lib_IntVector_Intrinsics_vec256 383 v2_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_5, v2_5); 384 Lib_IntVector_Intrinsics_vec256 385 v1_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_5, v3_5); 386 Lib_IntVector_Intrinsics_vec256 387 v3_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_5, v3_5); 388 Lib_IntVector_Intrinsics_vec256 389 v4_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_5, v6_5); 390 Lib_IntVector_Intrinsics_vec256 391 v6_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_5, v6_5); 392 Lib_IntVector_Intrinsics_vec256 393 v5_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_5, v7_5); 394 Lib_IntVector_Intrinsics_vec256 395 v7_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_5, v7_5); 396 Lib_IntVector_Intrinsics_vec256 v0_12 = v0_11; 397 Lib_IntVector_Intrinsics_vec256 v1_12 = v1_11; 398 Lib_IntVector_Intrinsics_vec256 v2_12 = v2_11; 399 Lib_IntVector_Intrinsics_vec256 v3_12 = v3_11; 400 Lib_IntVector_Intrinsics_vec256 v4_12 = v4_11; 401 Lib_IntVector_Intrinsics_vec256 v5_12 = v5_11; 402 Lib_IntVector_Intrinsics_vec256 v6_12 = v6_11; 403 Lib_IntVector_Intrinsics_vec256 v7_12 = v7_11; 404 Lib_IntVector_Intrinsics_vec256 405 v0_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_12, v4_12); 406 Lib_IntVector_Intrinsics_vec256 407 v4_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_12, v4_12); 408 Lib_IntVector_Intrinsics_vec256 409 v1_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_12, v5_12); 410 Lib_IntVector_Intrinsics_vec256 411 v5_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_12, v5_12); 412 Lib_IntVector_Intrinsics_vec256 413 v2_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_12, v6_12); 414 Lib_IntVector_Intrinsics_vec256 415 v6_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_12, v6_12); 416 Lib_IntVector_Intrinsics_vec256 417 v3_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_12, v7_12); 418 Lib_IntVector_Intrinsics_vec256 419 v7_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_12, v7_12); 420 Lib_IntVector_Intrinsics_vec256 v0_22 = v0_21; 421 Lib_IntVector_Intrinsics_vec256 v1_22 = v1_21; 422 Lib_IntVector_Intrinsics_vec256 v2_22 = v2_21; 423 Lib_IntVector_Intrinsics_vec256 v3_22 = v3_21; 424 Lib_IntVector_Intrinsics_vec256 v4_22 = v4_21; 425 Lib_IntVector_Intrinsics_vec256 v5_22 = v5_21; 426 Lib_IntVector_Intrinsics_vec256 v6_22 = v6_21; 427 Lib_IntVector_Intrinsics_vec256 v7_22 = v7_21; 428 Lib_IntVector_Intrinsics_vec256 v0_6 = v0_22; 429 Lib_IntVector_Intrinsics_vec256 v1_6 = v1_22; 430 Lib_IntVector_Intrinsics_vec256 v2_6 = v2_22; 431 Lib_IntVector_Intrinsics_vec256 v3_6 = v3_22; 432 Lib_IntVector_Intrinsics_vec256 v4_6 = v4_22; 433 Lib_IntVector_Intrinsics_vec256 v5_6 = v5_22; 434 Lib_IntVector_Intrinsics_vec256 v6_6 = v6_22; 435 Lib_IntVector_Intrinsics_vec256 v7_6 = v7_22; 436 Lib_IntVector_Intrinsics_vec256 v8 = v0_6; 437 Lib_IntVector_Intrinsics_vec256 v9 = v2_6; 438 Lib_IntVector_Intrinsics_vec256 v10 = v1_6; 439 Lib_IntVector_Intrinsics_vec256 v11 = v3_6; 440 Lib_IntVector_Intrinsics_vec256 v12 = v4_6; 441 Lib_IntVector_Intrinsics_vec256 v13 = v6_6; 442 Lib_IntVector_Intrinsics_vec256 v14 = v5_6; 443 Lib_IntVector_Intrinsics_vec256 v15 = v7_6; 444 k[0U] = v0; 445 k[1U] = v8; 446 k[2U] = v1; 447 k[3U] = v9; 448 k[4U] = v2; 449 k[5U] = v10; 450 k[6U] = v3; 451 k[7U] = v11; 452 k[8U] = v4; 453 k[9U] = v12; 454 k[10U] = v5; 455 k[11U] = v13; 456 k[12U] = v6; 457 k[13U] = v14; 458 k[14U] = v7; 459 k[15U] = v15; 460 KRML_MAYBE_FOR16(i0, 461 (uint32_t)0U, 462 (uint32_t)16U, 463 (uint32_t)1U, 464 Lib_IntVector_Intrinsics_vec256 465 x = Lib_IntVector_Intrinsics_vec256_load32_le(uu____1 + i0 * (uint32_t)32U); 466 Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i0]); 467 Lib_IntVector_Intrinsics_vec256_store32_le(uu____0 + i0 * (uint32_t)32U, y);); 468 } 469 if (rem1 > (uint32_t)0U) { 470 uint8_t *uu____2 = out + nb * (uint32_t)512U; 471 uint8_t plain[512U] = { 0U }; 472 memcpy(plain, text + nb * (uint32_t)512U, rem * sizeof(uint8_t)); 473 KRML_PRE_ALIGN(32) 474 Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; 475 chacha20_core_256(k, ctx, nb); 476 Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; 477 Lib_IntVector_Intrinsics_vec256 st1 = k[1U]; 478 Lib_IntVector_Intrinsics_vec256 st2 = k[2U]; 479 Lib_IntVector_Intrinsics_vec256 st3 = k[3U]; 480 Lib_IntVector_Intrinsics_vec256 st4 = k[4U]; 481 Lib_IntVector_Intrinsics_vec256 st5 = k[5U]; 482 Lib_IntVector_Intrinsics_vec256 st6 = k[6U]; 483 Lib_IntVector_Intrinsics_vec256 st7 = k[7U]; 484 Lib_IntVector_Intrinsics_vec256 st8 = k[8U]; 485 Lib_IntVector_Intrinsics_vec256 st9 = k[9U]; 486 Lib_IntVector_Intrinsics_vec256 st10 = k[10U]; 487 Lib_IntVector_Intrinsics_vec256 st11 = k[11U]; 488 Lib_IntVector_Intrinsics_vec256 st12 = k[12U]; 489 Lib_IntVector_Intrinsics_vec256 st13 = k[13U]; 490 Lib_IntVector_Intrinsics_vec256 st14 = k[14U]; 491 Lib_IntVector_Intrinsics_vec256 st15 = k[15U]; 492 Lib_IntVector_Intrinsics_vec256 v00 = st0; 493 Lib_IntVector_Intrinsics_vec256 v16 = st1; 494 Lib_IntVector_Intrinsics_vec256 v20 = st2; 495 Lib_IntVector_Intrinsics_vec256 v30 = st3; 496 Lib_IntVector_Intrinsics_vec256 v40 = st4; 497 Lib_IntVector_Intrinsics_vec256 v50 = st5; 498 Lib_IntVector_Intrinsics_vec256 v60 = st6; 499 Lib_IntVector_Intrinsics_vec256 v70 = st7; 500 Lib_IntVector_Intrinsics_vec256 501 v0_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v00, v16); 502 Lib_IntVector_Intrinsics_vec256 503 v1_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v00, v16); 504 Lib_IntVector_Intrinsics_vec256 505 v2_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v20, v30); 506 Lib_IntVector_Intrinsics_vec256 507 v3_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v20, v30); 508 Lib_IntVector_Intrinsics_vec256 509 v4_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v40, v50); 510 Lib_IntVector_Intrinsics_vec256 511 v5_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v40, v50); 512 Lib_IntVector_Intrinsics_vec256 513 v6_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v60, v70); 514 Lib_IntVector_Intrinsics_vec256 515 v7_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v60, v70); 516 Lib_IntVector_Intrinsics_vec256 v0_0 = v0_; 517 Lib_IntVector_Intrinsics_vec256 v1_0 = v1_; 518 Lib_IntVector_Intrinsics_vec256 v2_0 = v2_; 519 Lib_IntVector_Intrinsics_vec256 v3_0 = v3_; 520 Lib_IntVector_Intrinsics_vec256 v4_0 = v4_; 521 Lib_IntVector_Intrinsics_vec256 v5_0 = v5_; 522 Lib_IntVector_Intrinsics_vec256 v6_0 = v6_; 523 Lib_IntVector_Intrinsics_vec256 v7_0 = v7_; 524 Lib_IntVector_Intrinsics_vec256 525 v0_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_0, v2_0); 526 Lib_IntVector_Intrinsics_vec256 527 v2_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_0, v2_0); 528 Lib_IntVector_Intrinsics_vec256 529 v1_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_0, v3_0); 530 Lib_IntVector_Intrinsics_vec256 531 v3_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_0, v3_0); 532 Lib_IntVector_Intrinsics_vec256 533 v4_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_0, v6_0); 534 Lib_IntVector_Intrinsics_vec256 535 v6_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_0, v6_0); 536 Lib_IntVector_Intrinsics_vec256 537 v5_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_0, v7_0); 538 Lib_IntVector_Intrinsics_vec256 539 v7_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_0, v7_0); 540 Lib_IntVector_Intrinsics_vec256 v0_10 = v0_1; 541 Lib_IntVector_Intrinsics_vec256 v1_10 = v1_1; 542 Lib_IntVector_Intrinsics_vec256 v2_10 = v2_1; 543 Lib_IntVector_Intrinsics_vec256 v3_10 = v3_1; 544 Lib_IntVector_Intrinsics_vec256 v4_10 = v4_1; 545 Lib_IntVector_Intrinsics_vec256 v5_10 = v5_1; 546 Lib_IntVector_Intrinsics_vec256 v6_10 = v6_1; 547 Lib_IntVector_Intrinsics_vec256 v7_10 = v7_1; 548 Lib_IntVector_Intrinsics_vec256 549 v0_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_10, v4_10); 550 Lib_IntVector_Intrinsics_vec256 551 v4_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_10, v4_10); 552 Lib_IntVector_Intrinsics_vec256 553 v1_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_10, v5_10); 554 Lib_IntVector_Intrinsics_vec256 555 v5_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_10, v5_10); 556 Lib_IntVector_Intrinsics_vec256 557 v2_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_10, v6_10); 558 Lib_IntVector_Intrinsics_vec256 559 v6_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_10, v6_10); 560 Lib_IntVector_Intrinsics_vec256 561 v3_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_10, v7_10); 562 Lib_IntVector_Intrinsics_vec256 563 v7_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_10, v7_10); 564 Lib_IntVector_Intrinsics_vec256 v0_20 = v0_2; 565 Lib_IntVector_Intrinsics_vec256 v1_20 = v1_2; 566 Lib_IntVector_Intrinsics_vec256 v2_20 = v2_2; 567 Lib_IntVector_Intrinsics_vec256 v3_20 = v3_2; 568 Lib_IntVector_Intrinsics_vec256 v4_20 = v4_2; 569 Lib_IntVector_Intrinsics_vec256 v5_20 = v5_2; 570 Lib_IntVector_Intrinsics_vec256 v6_20 = v6_2; 571 Lib_IntVector_Intrinsics_vec256 v7_20 = v7_2; 572 Lib_IntVector_Intrinsics_vec256 v0_3 = v0_20; 573 Lib_IntVector_Intrinsics_vec256 v1_3 = v1_20; 574 Lib_IntVector_Intrinsics_vec256 v2_3 = v2_20; 575 Lib_IntVector_Intrinsics_vec256 v3_3 = v3_20; 576 Lib_IntVector_Intrinsics_vec256 v4_3 = v4_20; 577 Lib_IntVector_Intrinsics_vec256 v5_3 = v5_20; 578 Lib_IntVector_Intrinsics_vec256 v6_3 = v6_20; 579 Lib_IntVector_Intrinsics_vec256 v7_3 = v7_20; 580 Lib_IntVector_Intrinsics_vec256 v0 = v0_3; 581 Lib_IntVector_Intrinsics_vec256 v1 = v2_3; 582 Lib_IntVector_Intrinsics_vec256 v2 = v1_3; 583 Lib_IntVector_Intrinsics_vec256 v3 = v3_3; 584 Lib_IntVector_Intrinsics_vec256 v4 = v4_3; 585 Lib_IntVector_Intrinsics_vec256 v5 = v6_3; 586 Lib_IntVector_Intrinsics_vec256 v6 = v5_3; 587 Lib_IntVector_Intrinsics_vec256 v7 = v7_3; 588 Lib_IntVector_Intrinsics_vec256 v01 = st8; 589 Lib_IntVector_Intrinsics_vec256 v110 = st9; 590 Lib_IntVector_Intrinsics_vec256 v21 = st10; 591 Lib_IntVector_Intrinsics_vec256 v31 = st11; 592 Lib_IntVector_Intrinsics_vec256 v41 = st12; 593 Lib_IntVector_Intrinsics_vec256 v51 = st13; 594 Lib_IntVector_Intrinsics_vec256 v61 = st14; 595 Lib_IntVector_Intrinsics_vec256 v71 = st15; 596 Lib_IntVector_Intrinsics_vec256 597 v0_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v01, v110); 598 Lib_IntVector_Intrinsics_vec256 599 v1_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v01, v110); 600 Lib_IntVector_Intrinsics_vec256 601 v2_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v21, v31); 602 Lib_IntVector_Intrinsics_vec256 603 v3_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v21, v31); 604 Lib_IntVector_Intrinsics_vec256 605 v4_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v41, v51); 606 Lib_IntVector_Intrinsics_vec256 607 v5_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v41, v51); 608 Lib_IntVector_Intrinsics_vec256 609 v6_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v61, v71); 610 Lib_IntVector_Intrinsics_vec256 611 v7_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v61, v71); 612 Lib_IntVector_Intrinsics_vec256 v0_5 = v0_4; 613 Lib_IntVector_Intrinsics_vec256 v1_5 = v1_4; 614 Lib_IntVector_Intrinsics_vec256 v2_5 = v2_4; 615 Lib_IntVector_Intrinsics_vec256 v3_5 = v3_4; 616 Lib_IntVector_Intrinsics_vec256 v4_5 = v4_4; 617 Lib_IntVector_Intrinsics_vec256 v5_5 = v5_4; 618 Lib_IntVector_Intrinsics_vec256 v6_5 = v6_4; 619 Lib_IntVector_Intrinsics_vec256 v7_5 = v7_4; 620 Lib_IntVector_Intrinsics_vec256 621 v0_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_5, v2_5); 622 Lib_IntVector_Intrinsics_vec256 623 v2_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_5, v2_5); 624 Lib_IntVector_Intrinsics_vec256 625 v1_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_5, v3_5); 626 Lib_IntVector_Intrinsics_vec256 627 v3_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_5, v3_5); 628 Lib_IntVector_Intrinsics_vec256 629 v4_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_5, v6_5); 630 Lib_IntVector_Intrinsics_vec256 631 v6_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_5, v6_5); 632 Lib_IntVector_Intrinsics_vec256 633 v5_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_5, v7_5); 634 Lib_IntVector_Intrinsics_vec256 635 v7_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_5, v7_5); 636 Lib_IntVector_Intrinsics_vec256 v0_12 = v0_11; 637 Lib_IntVector_Intrinsics_vec256 v1_12 = v1_11; 638 Lib_IntVector_Intrinsics_vec256 v2_12 = v2_11; 639 Lib_IntVector_Intrinsics_vec256 v3_12 = v3_11; 640 Lib_IntVector_Intrinsics_vec256 v4_12 = v4_11; 641 Lib_IntVector_Intrinsics_vec256 v5_12 = v5_11; 642 Lib_IntVector_Intrinsics_vec256 v6_12 = v6_11; 643 Lib_IntVector_Intrinsics_vec256 v7_12 = v7_11; 644 Lib_IntVector_Intrinsics_vec256 645 v0_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_12, v4_12); 646 Lib_IntVector_Intrinsics_vec256 647 v4_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_12, v4_12); 648 Lib_IntVector_Intrinsics_vec256 649 v1_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_12, v5_12); 650 Lib_IntVector_Intrinsics_vec256 651 v5_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_12, v5_12); 652 Lib_IntVector_Intrinsics_vec256 653 v2_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_12, v6_12); 654 Lib_IntVector_Intrinsics_vec256 655 v6_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_12, v6_12); 656 Lib_IntVector_Intrinsics_vec256 657 v3_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_12, v7_12); 658 Lib_IntVector_Intrinsics_vec256 659 v7_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_12, v7_12); 660 Lib_IntVector_Intrinsics_vec256 v0_22 = v0_21; 661 Lib_IntVector_Intrinsics_vec256 v1_22 = v1_21; 662 Lib_IntVector_Intrinsics_vec256 v2_22 = v2_21; 663 Lib_IntVector_Intrinsics_vec256 v3_22 = v3_21; 664 Lib_IntVector_Intrinsics_vec256 v4_22 = v4_21; 665 Lib_IntVector_Intrinsics_vec256 v5_22 = v5_21; 666 Lib_IntVector_Intrinsics_vec256 v6_22 = v6_21; 667 Lib_IntVector_Intrinsics_vec256 v7_22 = v7_21; 668 Lib_IntVector_Intrinsics_vec256 v0_6 = v0_22; 669 Lib_IntVector_Intrinsics_vec256 v1_6 = v1_22; 670 Lib_IntVector_Intrinsics_vec256 v2_6 = v2_22; 671 Lib_IntVector_Intrinsics_vec256 v3_6 = v3_22; 672 Lib_IntVector_Intrinsics_vec256 v4_6 = v4_22; 673 Lib_IntVector_Intrinsics_vec256 v5_6 = v5_22; 674 Lib_IntVector_Intrinsics_vec256 v6_6 = v6_22; 675 Lib_IntVector_Intrinsics_vec256 v7_6 = v7_22; 676 Lib_IntVector_Intrinsics_vec256 v8 = v0_6; 677 Lib_IntVector_Intrinsics_vec256 v9 = v2_6; 678 Lib_IntVector_Intrinsics_vec256 v10 = v1_6; 679 Lib_IntVector_Intrinsics_vec256 v11 = v3_6; 680 Lib_IntVector_Intrinsics_vec256 v12 = v4_6; 681 Lib_IntVector_Intrinsics_vec256 v13 = v6_6; 682 Lib_IntVector_Intrinsics_vec256 v14 = v5_6; 683 Lib_IntVector_Intrinsics_vec256 v15 = v7_6; 684 k[0U] = v0; 685 k[1U] = v8; 686 k[2U] = v1; 687 k[3U] = v9; 688 k[4U] = v2; 689 k[5U] = v10; 690 k[6U] = v3; 691 k[7U] = v11; 692 k[8U] = v4; 693 k[9U] = v12; 694 k[10U] = v5; 695 k[11U] = v13; 696 k[12U] = v6; 697 k[13U] = v14; 698 k[14U] = v7; 699 k[15U] = v15; 700 KRML_MAYBE_FOR16(i, 701 (uint32_t)0U, 702 (uint32_t)16U, 703 (uint32_t)1U, 704 Lib_IntVector_Intrinsics_vec256 705 x = Lib_IntVector_Intrinsics_vec256_load32_le(plain + i * (uint32_t)32U); 706 Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i]); 707 Lib_IntVector_Intrinsics_vec256_store32_le(plain + i * (uint32_t)32U, y);); 708 memcpy(uu____2, plain, rem * sizeof(uint8_t)); 709 } 710 } 711 712 void 713 Hacl_Chacha20_Vec256_chacha20_decrypt_256( 714 uint32_t len, 715 uint8_t *out, 716 uint8_t *cipher, 717 uint8_t *key, 718 uint8_t *n, 719 uint32_t ctr) 720 { 721 KRML_PRE_ALIGN(32) 722 Lib_IntVector_Intrinsics_vec256 ctx[16U] KRML_POST_ALIGN(32) = { 0U }; 723 chacha20_init_256(ctx, key, n, ctr); 724 uint32_t rem = len % (uint32_t)512U; 725 uint32_t nb = len / (uint32_t)512U; 726 uint32_t rem1 = len % (uint32_t)512U; 727 for (uint32_t i = (uint32_t)0U; i < nb; i++) { 728 uint8_t *uu____0 = out + i * (uint32_t)512U; 729 uint8_t *uu____1 = cipher + i * (uint32_t)512U; 730 KRML_PRE_ALIGN(32) 731 Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; 732 chacha20_core_256(k, ctx, i); 733 Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; 734 Lib_IntVector_Intrinsics_vec256 st1 = k[1U]; 735 Lib_IntVector_Intrinsics_vec256 st2 = k[2U]; 736 Lib_IntVector_Intrinsics_vec256 st3 = k[3U]; 737 Lib_IntVector_Intrinsics_vec256 st4 = k[4U]; 738 Lib_IntVector_Intrinsics_vec256 st5 = k[5U]; 739 Lib_IntVector_Intrinsics_vec256 st6 = k[6U]; 740 Lib_IntVector_Intrinsics_vec256 st7 = k[7U]; 741 Lib_IntVector_Intrinsics_vec256 st8 = k[8U]; 742 Lib_IntVector_Intrinsics_vec256 st9 = k[9U]; 743 Lib_IntVector_Intrinsics_vec256 st10 = k[10U]; 744 Lib_IntVector_Intrinsics_vec256 st11 = k[11U]; 745 Lib_IntVector_Intrinsics_vec256 st12 = k[12U]; 746 Lib_IntVector_Intrinsics_vec256 st13 = k[13U]; 747 Lib_IntVector_Intrinsics_vec256 st14 = k[14U]; 748 Lib_IntVector_Intrinsics_vec256 st15 = k[15U]; 749 Lib_IntVector_Intrinsics_vec256 v00 = st0; 750 Lib_IntVector_Intrinsics_vec256 v16 = st1; 751 Lib_IntVector_Intrinsics_vec256 v20 = st2; 752 Lib_IntVector_Intrinsics_vec256 v30 = st3; 753 Lib_IntVector_Intrinsics_vec256 v40 = st4; 754 Lib_IntVector_Intrinsics_vec256 v50 = st5; 755 Lib_IntVector_Intrinsics_vec256 v60 = st6; 756 Lib_IntVector_Intrinsics_vec256 v70 = st7; 757 Lib_IntVector_Intrinsics_vec256 758 v0_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v00, v16); 759 Lib_IntVector_Intrinsics_vec256 760 v1_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v00, v16); 761 Lib_IntVector_Intrinsics_vec256 762 v2_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v20, v30); 763 Lib_IntVector_Intrinsics_vec256 764 v3_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v20, v30); 765 Lib_IntVector_Intrinsics_vec256 766 v4_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v40, v50); 767 Lib_IntVector_Intrinsics_vec256 768 v5_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v40, v50); 769 Lib_IntVector_Intrinsics_vec256 770 v6_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v60, v70); 771 Lib_IntVector_Intrinsics_vec256 772 v7_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v60, v70); 773 Lib_IntVector_Intrinsics_vec256 v0_0 = v0_; 774 Lib_IntVector_Intrinsics_vec256 v1_0 = v1_; 775 Lib_IntVector_Intrinsics_vec256 v2_0 = v2_; 776 Lib_IntVector_Intrinsics_vec256 v3_0 = v3_; 777 Lib_IntVector_Intrinsics_vec256 v4_0 = v4_; 778 Lib_IntVector_Intrinsics_vec256 v5_0 = v5_; 779 Lib_IntVector_Intrinsics_vec256 v6_0 = v6_; 780 Lib_IntVector_Intrinsics_vec256 v7_0 = v7_; 781 Lib_IntVector_Intrinsics_vec256 782 v0_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_0, v2_0); 783 Lib_IntVector_Intrinsics_vec256 784 v2_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_0, v2_0); 785 Lib_IntVector_Intrinsics_vec256 786 v1_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_0, v3_0); 787 Lib_IntVector_Intrinsics_vec256 788 v3_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_0, v3_0); 789 Lib_IntVector_Intrinsics_vec256 790 v4_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_0, v6_0); 791 Lib_IntVector_Intrinsics_vec256 792 v6_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_0, v6_0); 793 Lib_IntVector_Intrinsics_vec256 794 v5_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_0, v7_0); 795 Lib_IntVector_Intrinsics_vec256 796 v7_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_0, v7_0); 797 Lib_IntVector_Intrinsics_vec256 v0_10 = v0_1; 798 Lib_IntVector_Intrinsics_vec256 v1_10 = v1_1; 799 Lib_IntVector_Intrinsics_vec256 v2_10 = v2_1; 800 Lib_IntVector_Intrinsics_vec256 v3_10 = v3_1; 801 Lib_IntVector_Intrinsics_vec256 v4_10 = v4_1; 802 Lib_IntVector_Intrinsics_vec256 v5_10 = v5_1; 803 Lib_IntVector_Intrinsics_vec256 v6_10 = v6_1; 804 Lib_IntVector_Intrinsics_vec256 v7_10 = v7_1; 805 Lib_IntVector_Intrinsics_vec256 806 v0_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_10, v4_10); 807 Lib_IntVector_Intrinsics_vec256 808 v4_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_10, v4_10); 809 Lib_IntVector_Intrinsics_vec256 810 v1_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_10, v5_10); 811 Lib_IntVector_Intrinsics_vec256 812 v5_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_10, v5_10); 813 Lib_IntVector_Intrinsics_vec256 814 v2_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_10, v6_10); 815 Lib_IntVector_Intrinsics_vec256 816 v6_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_10, v6_10); 817 Lib_IntVector_Intrinsics_vec256 818 v3_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_10, v7_10); 819 Lib_IntVector_Intrinsics_vec256 820 v7_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_10, v7_10); 821 Lib_IntVector_Intrinsics_vec256 v0_20 = v0_2; 822 Lib_IntVector_Intrinsics_vec256 v1_20 = v1_2; 823 Lib_IntVector_Intrinsics_vec256 v2_20 = v2_2; 824 Lib_IntVector_Intrinsics_vec256 v3_20 = v3_2; 825 Lib_IntVector_Intrinsics_vec256 v4_20 = v4_2; 826 Lib_IntVector_Intrinsics_vec256 v5_20 = v5_2; 827 Lib_IntVector_Intrinsics_vec256 v6_20 = v6_2; 828 Lib_IntVector_Intrinsics_vec256 v7_20 = v7_2; 829 Lib_IntVector_Intrinsics_vec256 v0_3 = v0_20; 830 Lib_IntVector_Intrinsics_vec256 v1_3 = v1_20; 831 Lib_IntVector_Intrinsics_vec256 v2_3 = v2_20; 832 Lib_IntVector_Intrinsics_vec256 v3_3 = v3_20; 833 Lib_IntVector_Intrinsics_vec256 v4_3 = v4_20; 834 Lib_IntVector_Intrinsics_vec256 v5_3 = v5_20; 835 Lib_IntVector_Intrinsics_vec256 v6_3 = v6_20; 836 Lib_IntVector_Intrinsics_vec256 v7_3 = v7_20; 837 Lib_IntVector_Intrinsics_vec256 v0 = v0_3; 838 Lib_IntVector_Intrinsics_vec256 v1 = v2_3; 839 Lib_IntVector_Intrinsics_vec256 v2 = v1_3; 840 Lib_IntVector_Intrinsics_vec256 v3 = v3_3; 841 Lib_IntVector_Intrinsics_vec256 v4 = v4_3; 842 Lib_IntVector_Intrinsics_vec256 v5 = v6_3; 843 Lib_IntVector_Intrinsics_vec256 v6 = v5_3; 844 Lib_IntVector_Intrinsics_vec256 v7 = v7_3; 845 Lib_IntVector_Intrinsics_vec256 v01 = st8; 846 Lib_IntVector_Intrinsics_vec256 v110 = st9; 847 Lib_IntVector_Intrinsics_vec256 v21 = st10; 848 Lib_IntVector_Intrinsics_vec256 v31 = st11; 849 Lib_IntVector_Intrinsics_vec256 v41 = st12; 850 Lib_IntVector_Intrinsics_vec256 v51 = st13; 851 Lib_IntVector_Intrinsics_vec256 v61 = st14; 852 Lib_IntVector_Intrinsics_vec256 v71 = st15; 853 Lib_IntVector_Intrinsics_vec256 854 v0_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v01, v110); 855 Lib_IntVector_Intrinsics_vec256 856 v1_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v01, v110); 857 Lib_IntVector_Intrinsics_vec256 858 v2_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v21, v31); 859 Lib_IntVector_Intrinsics_vec256 860 v3_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v21, v31); 861 Lib_IntVector_Intrinsics_vec256 862 v4_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v41, v51); 863 Lib_IntVector_Intrinsics_vec256 864 v5_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v41, v51); 865 Lib_IntVector_Intrinsics_vec256 866 v6_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v61, v71); 867 Lib_IntVector_Intrinsics_vec256 868 v7_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v61, v71); 869 Lib_IntVector_Intrinsics_vec256 v0_5 = v0_4; 870 Lib_IntVector_Intrinsics_vec256 v1_5 = v1_4; 871 Lib_IntVector_Intrinsics_vec256 v2_5 = v2_4; 872 Lib_IntVector_Intrinsics_vec256 v3_5 = v3_4; 873 Lib_IntVector_Intrinsics_vec256 v4_5 = v4_4; 874 Lib_IntVector_Intrinsics_vec256 v5_5 = v5_4; 875 Lib_IntVector_Intrinsics_vec256 v6_5 = v6_4; 876 Lib_IntVector_Intrinsics_vec256 v7_5 = v7_4; 877 Lib_IntVector_Intrinsics_vec256 878 v0_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_5, v2_5); 879 Lib_IntVector_Intrinsics_vec256 880 v2_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_5, v2_5); 881 Lib_IntVector_Intrinsics_vec256 882 v1_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_5, v3_5); 883 Lib_IntVector_Intrinsics_vec256 884 v3_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_5, v3_5); 885 Lib_IntVector_Intrinsics_vec256 886 v4_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_5, v6_5); 887 Lib_IntVector_Intrinsics_vec256 888 v6_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_5, v6_5); 889 Lib_IntVector_Intrinsics_vec256 890 v5_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_5, v7_5); 891 Lib_IntVector_Intrinsics_vec256 892 v7_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_5, v7_5); 893 Lib_IntVector_Intrinsics_vec256 v0_12 = v0_11; 894 Lib_IntVector_Intrinsics_vec256 v1_12 = v1_11; 895 Lib_IntVector_Intrinsics_vec256 v2_12 = v2_11; 896 Lib_IntVector_Intrinsics_vec256 v3_12 = v3_11; 897 Lib_IntVector_Intrinsics_vec256 v4_12 = v4_11; 898 Lib_IntVector_Intrinsics_vec256 v5_12 = v5_11; 899 Lib_IntVector_Intrinsics_vec256 v6_12 = v6_11; 900 Lib_IntVector_Intrinsics_vec256 v7_12 = v7_11; 901 Lib_IntVector_Intrinsics_vec256 902 v0_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_12, v4_12); 903 Lib_IntVector_Intrinsics_vec256 904 v4_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_12, v4_12); 905 Lib_IntVector_Intrinsics_vec256 906 v1_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_12, v5_12); 907 Lib_IntVector_Intrinsics_vec256 908 v5_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_12, v5_12); 909 Lib_IntVector_Intrinsics_vec256 910 v2_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_12, v6_12); 911 Lib_IntVector_Intrinsics_vec256 912 v6_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_12, v6_12); 913 Lib_IntVector_Intrinsics_vec256 914 v3_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_12, v7_12); 915 Lib_IntVector_Intrinsics_vec256 916 v7_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_12, v7_12); 917 Lib_IntVector_Intrinsics_vec256 v0_22 = v0_21; 918 Lib_IntVector_Intrinsics_vec256 v1_22 = v1_21; 919 Lib_IntVector_Intrinsics_vec256 v2_22 = v2_21; 920 Lib_IntVector_Intrinsics_vec256 v3_22 = v3_21; 921 Lib_IntVector_Intrinsics_vec256 v4_22 = v4_21; 922 Lib_IntVector_Intrinsics_vec256 v5_22 = v5_21; 923 Lib_IntVector_Intrinsics_vec256 v6_22 = v6_21; 924 Lib_IntVector_Intrinsics_vec256 v7_22 = v7_21; 925 Lib_IntVector_Intrinsics_vec256 v0_6 = v0_22; 926 Lib_IntVector_Intrinsics_vec256 v1_6 = v1_22; 927 Lib_IntVector_Intrinsics_vec256 v2_6 = v2_22; 928 Lib_IntVector_Intrinsics_vec256 v3_6 = v3_22; 929 Lib_IntVector_Intrinsics_vec256 v4_6 = v4_22; 930 Lib_IntVector_Intrinsics_vec256 v5_6 = v5_22; 931 Lib_IntVector_Intrinsics_vec256 v6_6 = v6_22; 932 Lib_IntVector_Intrinsics_vec256 v7_6 = v7_22; 933 Lib_IntVector_Intrinsics_vec256 v8 = v0_6; 934 Lib_IntVector_Intrinsics_vec256 v9 = v2_6; 935 Lib_IntVector_Intrinsics_vec256 v10 = v1_6; 936 Lib_IntVector_Intrinsics_vec256 v11 = v3_6; 937 Lib_IntVector_Intrinsics_vec256 v12 = v4_6; 938 Lib_IntVector_Intrinsics_vec256 v13 = v6_6; 939 Lib_IntVector_Intrinsics_vec256 v14 = v5_6; 940 Lib_IntVector_Intrinsics_vec256 v15 = v7_6; 941 k[0U] = v0; 942 k[1U] = v8; 943 k[2U] = v1; 944 k[3U] = v9; 945 k[4U] = v2; 946 k[5U] = v10; 947 k[6U] = v3; 948 k[7U] = v11; 949 k[8U] = v4; 950 k[9U] = v12; 951 k[10U] = v5; 952 k[11U] = v13; 953 k[12U] = v6; 954 k[13U] = v14; 955 k[14U] = v7; 956 k[15U] = v15; 957 KRML_MAYBE_FOR16(i0, 958 (uint32_t)0U, 959 (uint32_t)16U, 960 (uint32_t)1U, 961 Lib_IntVector_Intrinsics_vec256 962 x = Lib_IntVector_Intrinsics_vec256_load32_le(uu____1 + i0 * (uint32_t)32U); 963 Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i0]); 964 Lib_IntVector_Intrinsics_vec256_store32_le(uu____0 + i0 * (uint32_t)32U, y);); 965 } 966 if (rem1 > (uint32_t)0U) { 967 uint8_t *uu____2 = out + nb * (uint32_t)512U; 968 uint8_t plain[512U] = { 0U }; 969 memcpy(plain, cipher + nb * (uint32_t)512U, rem * sizeof(uint8_t)); 970 KRML_PRE_ALIGN(32) 971 Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U }; 972 chacha20_core_256(k, ctx, nb); 973 Lib_IntVector_Intrinsics_vec256 st0 = k[0U]; 974 Lib_IntVector_Intrinsics_vec256 st1 = k[1U]; 975 Lib_IntVector_Intrinsics_vec256 st2 = k[2U]; 976 Lib_IntVector_Intrinsics_vec256 st3 = k[3U]; 977 Lib_IntVector_Intrinsics_vec256 st4 = k[4U]; 978 Lib_IntVector_Intrinsics_vec256 st5 = k[5U]; 979 Lib_IntVector_Intrinsics_vec256 st6 = k[6U]; 980 Lib_IntVector_Intrinsics_vec256 st7 = k[7U]; 981 Lib_IntVector_Intrinsics_vec256 st8 = k[8U]; 982 Lib_IntVector_Intrinsics_vec256 st9 = k[9U]; 983 Lib_IntVector_Intrinsics_vec256 st10 = k[10U]; 984 Lib_IntVector_Intrinsics_vec256 st11 = k[11U]; 985 Lib_IntVector_Intrinsics_vec256 st12 = k[12U]; 986 Lib_IntVector_Intrinsics_vec256 st13 = k[13U]; 987 Lib_IntVector_Intrinsics_vec256 st14 = k[14U]; 988 Lib_IntVector_Intrinsics_vec256 st15 = k[15U]; 989 Lib_IntVector_Intrinsics_vec256 v00 = st0; 990 Lib_IntVector_Intrinsics_vec256 v16 = st1; 991 Lib_IntVector_Intrinsics_vec256 v20 = st2; 992 Lib_IntVector_Intrinsics_vec256 v30 = st3; 993 Lib_IntVector_Intrinsics_vec256 v40 = st4; 994 Lib_IntVector_Intrinsics_vec256 v50 = st5; 995 Lib_IntVector_Intrinsics_vec256 v60 = st6; 996 Lib_IntVector_Intrinsics_vec256 v70 = st7; 997 Lib_IntVector_Intrinsics_vec256 998 v0_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v00, v16); 999 Lib_IntVector_Intrinsics_vec256 1000 v1_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v00, v16); 1001 Lib_IntVector_Intrinsics_vec256 1002 v2_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v20, v30); 1003 Lib_IntVector_Intrinsics_vec256 1004 v3_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v20, v30); 1005 Lib_IntVector_Intrinsics_vec256 1006 v4_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v40, v50); 1007 Lib_IntVector_Intrinsics_vec256 1008 v5_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v40, v50); 1009 Lib_IntVector_Intrinsics_vec256 1010 v6_ = Lib_IntVector_Intrinsics_vec256_interleave_low32(v60, v70); 1011 Lib_IntVector_Intrinsics_vec256 1012 v7_ = Lib_IntVector_Intrinsics_vec256_interleave_high32(v60, v70); 1013 Lib_IntVector_Intrinsics_vec256 v0_0 = v0_; 1014 Lib_IntVector_Intrinsics_vec256 v1_0 = v1_; 1015 Lib_IntVector_Intrinsics_vec256 v2_0 = v2_; 1016 Lib_IntVector_Intrinsics_vec256 v3_0 = v3_; 1017 Lib_IntVector_Intrinsics_vec256 v4_0 = v4_; 1018 Lib_IntVector_Intrinsics_vec256 v5_0 = v5_; 1019 Lib_IntVector_Intrinsics_vec256 v6_0 = v6_; 1020 Lib_IntVector_Intrinsics_vec256 v7_0 = v7_; 1021 Lib_IntVector_Intrinsics_vec256 1022 v0_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_0, v2_0); 1023 Lib_IntVector_Intrinsics_vec256 1024 v2_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_0, v2_0); 1025 Lib_IntVector_Intrinsics_vec256 1026 v1_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_0, v3_0); 1027 Lib_IntVector_Intrinsics_vec256 1028 v3_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_0, v3_0); 1029 Lib_IntVector_Intrinsics_vec256 1030 v4_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_0, v6_0); 1031 Lib_IntVector_Intrinsics_vec256 1032 v6_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_0, v6_0); 1033 Lib_IntVector_Intrinsics_vec256 1034 v5_1 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_0, v7_0); 1035 Lib_IntVector_Intrinsics_vec256 1036 v7_1 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_0, v7_0); 1037 Lib_IntVector_Intrinsics_vec256 v0_10 = v0_1; 1038 Lib_IntVector_Intrinsics_vec256 v1_10 = v1_1; 1039 Lib_IntVector_Intrinsics_vec256 v2_10 = v2_1; 1040 Lib_IntVector_Intrinsics_vec256 v3_10 = v3_1; 1041 Lib_IntVector_Intrinsics_vec256 v4_10 = v4_1; 1042 Lib_IntVector_Intrinsics_vec256 v5_10 = v5_1; 1043 Lib_IntVector_Intrinsics_vec256 v6_10 = v6_1; 1044 Lib_IntVector_Intrinsics_vec256 v7_10 = v7_1; 1045 Lib_IntVector_Intrinsics_vec256 1046 v0_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_10, v4_10); 1047 Lib_IntVector_Intrinsics_vec256 1048 v4_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_10, v4_10); 1049 Lib_IntVector_Intrinsics_vec256 1050 v1_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_10, v5_10); 1051 Lib_IntVector_Intrinsics_vec256 1052 v5_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_10, v5_10); 1053 Lib_IntVector_Intrinsics_vec256 1054 v2_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_10, v6_10); 1055 Lib_IntVector_Intrinsics_vec256 1056 v6_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_10, v6_10); 1057 Lib_IntVector_Intrinsics_vec256 1058 v3_2 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_10, v7_10); 1059 Lib_IntVector_Intrinsics_vec256 1060 v7_2 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_10, v7_10); 1061 Lib_IntVector_Intrinsics_vec256 v0_20 = v0_2; 1062 Lib_IntVector_Intrinsics_vec256 v1_20 = v1_2; 1063 Lib_IntVector_Intrinsics_vec256 v2_20 = v2_2; 1064 Lib_IntVector_Intrinsics_vec256 v3_20 = v3_2; 1065 Lib_IntVector_Intrinsics_vec256 v4_20 = v4_2; 1066 Lib_IntVector_Intrinsics_vec256 v5_20 = v5_2; 1067 Lib_IntVector_Intrinsics_vec256 v6_20 = v6_2; 1068 Lib_IntVector_Intrinsics_vec256 v7_20 = v7_2; 1069 Lib_IntVector_Intrinsics_vec256 v0_3 = v0_20; 1070 Lib_IntVector_Intrinsics_vec256 v1_3 = v1_20; 1071 Lib_IntVector_Intrinsics_vec256 v2_3 = v2_20; 1072 Lib_IntVector_Intrinsics_vec256 v3_3 = v3_20; 1073 Lib_IntVector_Intrinsics_vec256 v4_3 = v4_20; 1074 Lib_IntVector_Intrinsics_vec256 v5_3 = v5_20; 1075 Lib_IntVector_Intrinsics_vec256 v6_3 = v6_20; 1076 Lib_IntVector_Intrinsics_vec256 v7_3 = v7_20; 1077 Lib_IntVector_Intrinsics_vec256 v0 = v0_3; 1078 Lib_IntVector_Intrinsics_vec256 v1 = v2_3; 1079 Lib_IntVector_Intrinsics_vec256 v2 = v1_3; 1080 Lib_IntVector_Intrinsics_vec256 v3 = v3_3; 1081 Lib_IntVector_Intrinsics_vec256 v4 = v4_3; 1082 Lib_IntVector_Intrinsics_vec256 v5 = v6_3; 1083 Lib_IntVector_Intrinsics_vec256 v6 = v5_3; 1084 Lib_IntVector_Intrinsics_vec256 v7 = v7_3; 1085 Lib_IntVector_Intrinsics_vec256 v01 = st8; 1086 Lib_IntVector_Intrinsics_vec256 v110 = st9; 1087 Lib_IntVector_Intrinsics_vec256 v21 = st10; 1088 Lib_IntVector_Intrinsics_vec256 v31 = st11; 1089 Lib_IntVector_Intrinsics_vec256 v41 = st12; 1090 Lib_IntVector_Intrinsics_vec256 v51 = st13; 1091 Lib_IntVector_Intrinsics_vec256 v61 = st14; 1092 Lib_IntVector_Intrinsics_vec256 v71 = st15; 1093 Lib_IntVector_Intrinsics_vec256 1094 v0_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v01, v110); 1095 Lib_IntVector_Intrinsics_vec256 1096 v1_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v01, v110); 1097 Lib_IntVector_Intrinsics_vec256 1098 v2_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v21, v31); 1099 Lib_IntVector_Intrinsics_vec256 1100 v3_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v21, v31); 1101 Lib_IntVector_Intrinsics_vec256 1102 v4_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v41, v51); 1103 Lib_IntVector_Intrinsics_vec256 1104 v5_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v41, v51); 1105 Lib_IntVector_Intrinsics_vec256 1106 v6_4 = Lib_IntVector_Intrinsics_vec256_interleave_low32(v61, v71); 1107 Lib_IntVector_Intrinsics_vec256 1108 v7_4 = Lib_IntVector_Intrinsics_vec256_interleave_high32(v61, v71); 1109 Lib_IntVector_Intrinsics_vec256 v0_5 = v0_4; 1110 Lib_IntVector_Intrinsics_vec256 v1_5 = v1_4; 1111 Lib_IntVector_Intrinsics_vec256 v2_5 = v2_4; 1112 Lib_IntVector_Intrinsics_vec256 v3_5 = v3_4; 1113 Lib_IntVector_Intrinsics_vec256 v4_5 = v4_4; 1114 Lib_IntVector_Intrinsics_vec256 v5_5 = v5_4; 1115 Lib_IntVector_Intrinsics_vec256 v6_5 = v6_4; 1116 Lib_IntVector_Intrinsics_vec256 v7_5 = v7_4; 1117 Lib_IntVector_Intrinsics_vec256 1118 v0_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v0_5, v2_5); 1119 Lib_IntVector_Intrinsics_vec256 1120 v2_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v0_5, v2_5); 1121 Lib_IntVector_Intrinsics_vec256 1122 v1_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v1_5, v3_5); 1123 Lib_IntVector_Intrinsics_vec256 1124 v3_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v1_5, v3_5); 1125 Lib_IntVector_Intrinsics_vec256 1126 v4_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v4_5, v6_5); 1127 Lib_IntVector_Intrinsics_vec256 1128 v6_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v4_5, v6_5); 1129 Lib_IntVector_Intrinsics_vec256 1130 v5_11 = Lib_IntVector_Intrinsics_vec256_interleave_low64(v5_5, v7_5); 1131 Lib_IntVector_Intrinsics_vec256 1132 v7_11 = Lib_IntVector_Intrinsics_vec256_interleave_high64(v5_5, v7_5); 1133 Lib_IntVector_Intrinsics_vec256 v0_12 = v0_11; 1134 Lib_IntVector_Intrinsics_vec256 v1_12 = v1_11; 1135 Lib_IntVector_Intrinsics_vec256 v2_12 = v2_11; 1136 Lib_IntVector_Intrinsics_vec256 v3_12 = v3_11; 1137 Lib_IntVector_Intrinsics_vec256 v4_12 = v4_11; 1138 Lib_IntVector_Intrinsics_vec256 v5_12 = v5_11; 1139 Lib_IntVector_Intrinsics_vec256 v6_12 = v6_11; 1140 Lib_IntVector_Intrinsics_vec256 v7_12 = v7_11; 1141 Lib_IntVector_Intrinsics_vec256 1142 v0_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v0_12, v4_12); 1143 Lib_IntVector_Intrinsics_vec256 1144 v4_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v0_12, v4_12); 1145 Lib_IntVector_Intrinsics_vec256 1146 v1_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v1_12, v5_12); 1147 Lib_IntVector_Intrinsics_vec256 1148 v5_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v1_12, v5_12); 1149 Lib_IntVector_Intrinsics_vec256 1150 v2_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v2_12, v6_12); 1151 Lib_IntVector_Intrinsics_vec256 1152 v6_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v2_12, v6_12); 1153 Lib_IntVector_Intrinsics_vec256 1154 v3_21 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v3_12, v7_12); 1155 Lib_IntVector_Intrinsics_vec256 1156 v7_21 = Lib_IntVector_Intrinsics_vec256_interleave_high128(v3_12, v7_12); 1157 Lib_IntVector_Intrinsics_vec256 v0_22 = v0_21; 1158 Lib_IntVector_Intrinsics_vec256 v1_22 = v1_21; 1159 Lib_IntVector_Intrinsics_vec256 v2_22 = v2_21; 1160 Lib_IntVector_Intrinsics_vec256 v3_22 = v3_21; 1161 Lib_IntVector_Intrinsics_vec256 v4_22 = v4_21; 1162 Lib_IntVector_Intrinsics_vec256 v5_22 = v5_21; 1163 Lib_IntVector_Intrinsics_vec256 v6_22 = v6_21; 1164 Lib_IntVector_Intrinsics_vec256 v7_22 = v7_21; 1165 Lib_IntVector_Intrinsics_vec256 v0_6 = v0_22; 1166 Lib_IntVector_Intrinsics_vec256 v1_6 = v1_22; 1167 Lib_IntVector_Intrinsics_vec256 v2_6 = v2_22; 1168 Lib_IntVector_Intrinsics_vec256 v3_6 = v3_22; 1169 Lib_IntVector_Intrinsics_vec256 v4_6 = v4_22; 1170 Lib_IntVector_Intrinsics_vec256 v5_6 = v5_22; 1171 Lib_IntVector_Intrinsics_vec256 v6_6 = v6_22; 1172 Lib_IntVector_Intrinsics_vec256 v7_6 = v7_22; 1173 Lib_IntVector_Intrinsics_vec256 v8 = v0_6; 1174 Lib_IntVector_Intrinsics_vec256 v9 = v2_6; 1175 Lib_IntVector_Intrinsics_vec256 v10 = v1_6; 1176 Lib_IntVector_Intrinsics_vec256 v11 = v3_6; 1177 Lib_IntVector_Intrinsics_vec256 v12 = v4_6; 1178 Lib_IntVector_Intrinsics_vec256 v13 = v6_6; 1179 Lib_IntVector_Intrinsics_vec256 v14 = v5_6; 1180 Lib_IntVector_Intrinsics_vec256 v15 = v7_6; 1181 k[0U] = v0; 1182 k[1U] = v8; 1183 k[2U] = v1; 1184 k[3U] = v9; 1185 k[4U] = v2; 1186 k[5U] = v10; 1187 k[6U] = v3; 1188 k[7U] = v11; 1189 k[8U] = v4; 1190 k[9U] = v12; 1191 k[10U] = v5; 1192 k[11U] = v13; 1193 k[12U] = v6; 1194 k[13U] = v14; 1195 k[14U] = v7; 1196 k[15U] = v15; 1197 KRML_MAYBE_FOR16(i, 1198 (uint32_t)0U, 1199 (uint32_t)16U, 1200 (uint32_t)1U, 1201 Lib_IntVector_Intrinsics_vec256 1202 x = Lib_IntVector_Intrinsics_vec256_load32_le(plain + i * (uint32_t)32U); 1203 Lib_IntVector_Intrinsics_vec256 y = Lib_IntVector_Intrinsics_vec256_xor(x, k[i]); 1204 Lib_IntVector_Intrinsics_vec256_store32_le(plain + i * (uint32_t)32U, y);); 1205 memcpy(uu____2, plain, rem * sizeof(uint8_t)); 1206 } 1207 }