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