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