/src/nss/lib/freebl/verified/Hacl_Poly1305_256.c
Line | Count | Source |
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 "internal/Hacl_Poly1305_256.h" |
26 | | |
27 | | void |
28 | | Hacl_Impl_Poly1305_Field32xN_256_load_acc4(Lib_IntVector_Intrinsics_vec256 *acc, uint8_t *b) |
29 | 8.73k | { |
30 | 8.73k | KRML_PRE_ALIGN(32) |
31 | 8.73k | Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; |
32 | 8.73k | Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(b); |
33 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
34 | 8.73k | hi = Lib_IntVector_Intrinsics_vec256_load64_le(b + (uint32_t)32U); |
35 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
36 | 8.73k | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
37 | 8.73k | Lib_IntVector_Intrinsics_vec256 m0 = Lib_IntVector_Intrinsics_vec256_interleave_low128(lo, hi); |
38 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
39 | 8.73k | m1 = Lib_IntVector_Intrinsics_vec256_interleave_high128(lo, hi); |
40 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
41 | 8.73k | m2 = Lib_IntVector_Intrinsics_vec256_shift_right(m0, (uint32_t)48U); |
42 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
43 | 8.73k | m3 = Lib_IntVector_Intrinsics_vec256_shift_right(m1, (uint32_t)48U); |
44 | 8.73k | Lib_IntVector_Intrinsics_vec256 m4 = Lib_IntVector_Intrinsics_vec256_interleave_high64(m0, m1); |
45 | 8.73k | Lib_IntVector_Intrinsics_vec256 t0 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m0, m1); |
46 | 8.73k | Lib_IntVector_Intrinsics_vec256 t3 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m2, m3); |
47 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
48 | 8.73k | t2 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)4U); |
49 | 8.73k | Lib_IntVector_Intrinsics_vec256 o20 = Lib_IntVector_Intrinsics_vec256_and(t2, mask26); |
50 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
51 | 8.73k | t1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); |
52 | 8.73k | Lib_IntVector_Intrinsics_vec256 o10 = Lib_IntVector_Intrinsics_vec256_and(t1, mask26); |
53 | 8.73k | Lib_IntVector_Intrinsics_vec256 o5 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); |
54 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
55 | 8.73k | t31 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)30U); |
56 | 8.73k | Lib_IntVector_Intrinsics_vec256 o30 = Lib_IntVector_Intrinsics_vec256_and(t31, mask26); |
57 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
58 | 8.73k | o40 = Lib_IntVector_Intrinsics_vec256_shift_right64(m4, (uint32_t)40U); |
59 | 8.73k | Lib_IntVector_Intrinsics_vec256 o0 = o5; |
60 | 8.73k | Lib_IntVector_Intrinsics_vec256 o1 = o10; |
61 | 8.73k | Lib_IntVector_Intrinsics_vec256 o2 = o20; |
62 | 8.73k | Lib_IntVector_Intrinsics_vec256 o3 = o30; |
63 | 8.73k | Lib_IntVector_Intrinsics_vec256 o4 = o40; |
64 | 8.73k | e[0U] = o0; |
65 | 8.73k | e[1U] = o1; |
66 | 8.73k | e[2U] = o2; |
67 | 8.73k | e[3U] = o3; |
68 | 8.73k | e[4U] = o4; |
69 | 8.73k | uint64_t b1 = (uint64_t)0x1000000U; |
70 | 8.73k | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b1); |
71 | 8.73k | Lib_IntVector_Intrinsics_vec256 f40 = e[4U]; |
72 | 8.73k | e[4U] = Lib_IntVector_Intrinsics_vec256_or(f40, mask); |
73 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc0 = acc[0U]; |
74 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc1 = acc[1U]; |
75 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc2 = acc[2U]; |
76 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc3 = acc[3U]; |
77 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc4 = acc[4U]; |
78 | 8.73k | Lib_IntVector_Intrinsics_vec256 e0 = e[0U]; |
79 | 8.73k | Lib_IntVector_Intrinsics_vec256 e1 = e[1U]; |
80 | 8.73k | Lib_IntVector_Intrinsics_vec256 e2 = e[2U]; |
81 | 8.73k | Lib_IntVector_Intrinsics_vec256 e3 = e[3U]; |
82 | 8.73k | Lib_IntVector_Intrinsics_vec256 e4 = e[4U]; |
83 | 8.73k | Lib_IntVector_Intrinsics_vec256 r0 = Lib_IntVector_Intrinsics_vec256_zero; |
84 | 8.73k | Lib_IntVector_Intrinsics_vec256 r1 = Lib_IntVector_Intrinsics_vec256_zero; |
85 | 8.73k | Lib_IntVector_Intrinsics_vec256 r2 = Lib_IntVector_Intrinsics_vec256_zero; |
86 | 8.73k | Lib_IntVector_Intrinsics_vec256 r3 = Lib_IntVector_Intrinsics_vec256_zero; |
87 | 8.73k | Lib_IntVector_Intrinsics_vec256 r4 = Lib_IntVector_Intrinsics_vec256_zero; |
88 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
89 | 8.73k | r01 = |
90 | 8.73k | Lib_IntVector_Intrinsics_vec256_insert64(r0, |
91 | 8.73k | Lib_IntVector_Intrinsics_vec256_extract64(acc0, (uint32_t)0U), |
92 | 8.73k | (uint32_t)0U); |
93 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
94 | 8.73k | r11 = |
95 | 8.73k | Lib_IntVector_Intrinsics_vec256_insert64(r1, |
96 | 8.73k | Lib_IntVector_Intrinsics_vec256_extract64(acc1, (uint32_t)0U), |
97 | 8.73k | (uint32_t)0U); |
98 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
99 | 8.73k | r21 = |
100 | 8.73k | Lib_IntVector_Intrinsics_vec256_insert64(r2, |
101 | 8.73k | Lib_IntVector_Intrinsics_vec256_extract64(acc2, (uint32_t)0U), |
102 | 8.73k | (uint32_t)0U); |
103 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
104 | 8.73k | r31 = |
105 | 8.73k | Lib_IntVector_Intrinsics_vec256_insert64(r3, |
106 | 8.73k | Lib_IntVector_Intrinsics_vec256_extract64(acc3, (uint32_t)0U), |
107 | 8.73k | (uint32_t)0U); |
108 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
109 | 8.73k | r41 = |
110 | 8.73k | Lib_IntVector_Intrinsics_vec256_insert64(r4, |
111 | 8.73k | Lib_IntVector_Intrinsics_vec256_extract64(acc4, (uint32_t)0U), |
112 | 8.73k | (uint32_t)0U); |
113 | 8.73k | Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_add64(r01, e0); |
114 | 8.73k | Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_add64(r11, e1); |
115 | 8.73k | Lib_IntVector_Intrinsics_vec256 f2 = Lib_IntVector_Intrinsics_vec256_add64(r21, e2); |
116 | 8.73k | Lib_IntVector_Intrinsics_vec256 f3 = Lib_IntVector_Intrinsics_vec256_add64(r31, e3); |
117 | 8.73k | Lib_IntVector_Intrinsics_vec256 f4 = Lib_IntVector_Intrinsics_vec256_add64(r41, e4); |
118 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc01 = f0; |
119 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc11 = f1; |
120 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc21 = f2; |
121 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc31 = f3; |
122 | 8.73k | Lib_IntVector_Intrinsics_vec256 acc41 = f4; |
123 | 8.73k | acc[0U] = acc01; |
124 | 8.73k | acc[1U] = acc11; |
125 | 8.73k | acc[2U] = acc21; |
126 | 8.73k | acc[3U] = acc31; |
127 | 8.73k | acc[4U] = acc41; |
128 | 8.73k | } |
129 | | |
130 | | void |
131 | | Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize( |
132 | | Lib_IntVector_Intrinsics_vec256 *out, |
133 | | Lib_IntVector_Intrinsics_vec256 *p) |
134 | 8.73k | { |
135 | 8.73k | Lib_IntVector_Intrinsics_vec256 *r = p; |
136 | 8.73k | Lib_IntVector_Intrinsics_vec256 *r_5 = p + (uint32_t)5U; |
137 | 8.73k | Lib_IntVector_Intrinsics_vec256 *r4 = p + (uint32_t)10U; |
138 | 8.73k | Lib_IntVector_Intrinsics_vec256 a0 = out[0U]; |
139 | 8.73k | Lib_IntVector_Intrinsics_vec256 a1 = out[1U]; |
140 | 8.73k | Lib_IntVector_Intrinsics_vec256 a2 = out[2U]; |
141 | 8.73k | Lib_IntVector_Intrinsics_vec256 a3 = out[3U]; |
142 | 8.73k | Lib_IntVector_Intrinsics_vec256 a4 = out[4U]; |
143 | 8.73k | Lib_IntVector_Intrinsics_vec256 r10 = r[0U]; |
144 | 8.73k | Lib_IntVector_Intrinsics_vec256 r11 = r[1U]; |
145 | 8.73k | Lib_IntVector_Intrinsics_vec256 r12 = r[2U]; |
146 | 8.73k | Lib_IntVector_Intrinsics_vec256 r13 = r[3U]; |
147 | 8.73k | Lib_IntVector_Intrinsics_vec256 r14 = r[4U]; |
148 | 8.73k | Lib_IntVector_Intrinsics_vec256 r151 = r_5[1U]; |
149 | 8.73k | Lib_IntVector_Intrinsics_vec256 r152 = r_5[2U]; |
150 | 8.73k | Lib_IntVector_Intrinsics_vec256 r153 = r_5[3U]; |
151 | 8.73k | Lib_IntVector_Intrinsics_vec256 r154 = r_5[4U]; |
152 | 8.73k | Lib_IntVector_Intrinsics_vec256 r40 = r4[0U]; |
153 | 8.73k | Lib_IntVector_Intrinsics_vec256 r41 = r4[1U]; |
154 | 8.73k | Lib_IntVector_Intrinsics_vec256 r42 = r4[2U]; |
155 | 8.73k | Lib_IntVector_Intrinsics_vec256 r43 = r4[3U]; |
156 | 8.73k | Lib_IntVector_Intrinsics_vec256 r44 = r4[4U]; |
157 | 8.73k | Lib_IntVector_Intrinsics_vec256 a010 = Lib_IntVector_Intrinsics_vec256_mul64(r10, r10); |
158 | 8.73k | Lib_IntVector_Intrinsics_vec256 a110 = Lib_IntVector_Intrinsics_vec256_mul64(r11, r10); |
159 | 8.73k | Lib_IntVector_Intrinsics_vec256 a210 = Lib_IntVector_Intrinsics_vec256_mul64(r12, r10); |
160 | 8.73k | Lib_IntVector_Intrinsics_vec256 a310 = Lib_IntVector_Intrinsics_vec256_mul64(r13, r10); |
161 | 8.73k | Lib_IntVector_Intrinsics_vec256 a410 = Lib_IntVector_Intrinsics_vec256_mul64(r14, r10); |
162 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
163 | 8.73k | a020 = |
164 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a010, |
165 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r11)); |
166 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
167 | 8.73k | a120 = |
168 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a110, |
169 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r11)); |
170 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
171 | 8.73k | a220 = |
172 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a210, |
173 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r11)); |
174 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
175 | 8.73k | a320 = |
176 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a310, |
177 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12, r11)); |
178 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
179 | 8.73k | a420 = |
180 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a410, |
181 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r13, r11)); |
182 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
183 | 8.73k | a030 = |
184 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a020, |
185 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r12)); |
186 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
187 | 8.73k | a130 = |
188 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a120, |
189 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r12)); |
190 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
191 | 8.73k | a230 = |
192 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a220, |
193 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r12)); |
194 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
195 | 8.73k | a330 = |
196 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a320, |
197 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r12)); |
198 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
199 | 8.73k | a430 = |
200 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a420, |
201 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12, r12)); |
202 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
203 | 8.73k | a040 = |
204 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a030, |
205 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r152, r13)); |
206 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
207 | 8.73k | a140 = |
208 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a130, |
209 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r13)); |
210 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
211 | 8.73k | a240 = |
212 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a230, |
213 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r13)); |
214 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
215 | 8.73k | a340 = |
216 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a330, |
217 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r13)); |
218 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
219 | 8.73k | a440 = |
220 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a430, |
221 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r13)); |
222 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
223 | 8.73k | a050 = |
224 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a040, |
225 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r151, r14)); |
226 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
227 | 8.73k | a150 = |
228 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a140, |
229 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r152, r14)); |
230 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
231 | 8.73k | a250 = |
232 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a240, |
233 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r14)); |
234 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
235 | 8.73k | a350 = |
236 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a340, |
237 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r14)); |
238 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
239 | 8.73k | a450 = |
240 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a440, |
241 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r14)); |
242 | 8.73k | Lib_IntVector_Intrinsics_vec256 t00 = a050; |
243 | 8.73k | Lib_IntVector_Intrinsics_vec256 t10 = a150; |
244 | 8.73k | Lib_IntVector_Intrinsics_vec256 t20 = a250; |
245 | 8.73k | Lib_IntVector_Intrinsics_vec256 t30 = a350; |
246 | 8.73k | Lib_IntVector_Intrinsics_vec256 t40 = a450; |
247 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
248 | 8.73k | mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
249 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
250 | 8.73k | z00 = Lib_IntVector_Intrinsics_vec256_shift_right64(t00, (uint32_t)26U); |
251 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
252 | 8.73k | z10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)26U); |
253 | 8.73k | Lib_IntVector_Intrinsics_vec256 x00 = Lib_IntVector_Intrinsics_vec256_and(t00, mask260); |
254 | 8.73k | Lib_IntVector_Intrinsics_vec256 x30 = Lib_IntVector_Intrinsics_vec256_and(t30, mask260); |
255 | 8.73k | Lib_IntVector_Intrinsics_vec256 x10 = Lib_IntVector_Intrinsics_vec256_add64(t10, z00); |
256 | 8.73k | Lib_IntVector_Intrinsics_vec256 x40 = Lib_IntVector_Intrinsics_vec256_add64(t40, z10); |
257 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
258 | 8.73k | z010 = Lib_IntVector_Intrinsics_vec256_shift_right64(x10, (uint32_t)26U); |
259 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
260 | 8.73k | z110 = Lib_IntVector_Intrinsics_vec256_shift_right64(x40, (uint32_t)26U); |
261 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
262 | 8.73k | t5 = Lib_IntVector_Intrinsics_vec256_shift_left64(z110, (uint32_t)2U); |
263 | 8.73k | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z110, t5); |
264 | 8.73k | Lib_IntVector_Intrinsics_vec256 x110 = Lib_IntVector_Intrinsics_vec256_and(x10, mask260); |
265 | 8.73k | Lib_IntVector_Intrinsics_vec256 x410 = Lib_IntVector_Intrinsics_vec256_and(x40, mask260); |
266 | 8.73k | Lib_IntVector_Intrinsics_vec256 x20 = Lib_IntVector_Intrinsics_vec256_add64(t20, z010); |
267 | 8.73k | Lib_IntVector_Intrinsics_vec256 x010 = Lib_IntVector_Intrinsics_vec256_add64(x00, z12); |
268 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
269 | 8.73k | z020 = Lib_IntVector_Intrinsics_vec256_shift_right64(x20, (uint32_t)26U); |
270 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
271 | 8.73k | z130 = Lib_IntVector_Intrinsics_vec256_shift_right64(x010, (uint32_t)26U); |
272 | 8.73k | Lib_IntVector_Intrinsics_vec256 x210 = Lib_IntVector_Intrinsics_vec256_and(x20, mask260); |
273 | 8.73k | Lib_IntVector_Intrinsics_vec256 x020 = Lib_IntVector_Intrinsics_vec256_and(x010, mask260); |
274 | 8.73k | Lib_IntVector_Intrinsics_vec256 x310 = Lib_IntVector_Intrinsics_vec256_add64(x30, z020); |
275 | 8.73k | Lib_IntVector_Intrinsics_vec256 x120 = Lib_IntVector_Intrinsics_vec256_add64(x110, z130); |
276 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
277 | 8.73k | z030 = Lib_IntVector_Intrinsics_vec256_shift_right64(x310, (uint32_t)26U); |
278 | 8.73k | Lib_IntVector_Intrinsics_vec256 x320 = Lib_IntVector_Intrinsics_vec256_and(x310, mask260); |
279 | 8.73k | Lib_IntVector_Intrinsics_vec256 x420 = Lib_IntVector_Intrinsics_vec256_add64(x410, z030); |
280 | 8.73k | Lib_IntVector_Intrinsics_vec256 r20 = x020; |
281 | 8.73k | Lib_IntVector_Intrinsics_vec256 r21 = x120; |
282 | 8.73k | Lib_IntVector_Intrinsics_vec256 r22 = x210; |
283 | 8.73k | Lib_IntVector_Intrinsics_vec256 r23 = x320; |
284 | 8.73k | Lib_IntVector_Intrinsics_vec256 r24 = x420; |
285 | 8.73k | Lib_IntVector_Intrinsics_vec256 a011 = Lib_IntVector_Intrinsics_vec256_mul64(r10, r20); |
286 | 8.73k | Lib_IntVector_Intrinsics_vec256 a111 = Lib_IntVector_Intrinsics_vec256_mul64(r11, r20); |
287 | 8.73k | Lib_IntVector_Intrinsics_vec256 a211 = Lib_IntVector_Intrinsics_vec256_mul64(r12, r20); |
288 | 8.73k | Lib_IntVector_Intrinsics_vec256 a311 = Lib_IntVector_Intrinsics_vec256_mul64(r13, r20); |
289 | 8.73k | Lib_IntVector_Intrinsics_vec256 a411 = Lib_IntVector_Intrinsics_vec256_mul64(r14, r20); |
290 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
291 | 8.73k | a021 = |
292 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a011, |
293 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r21)); |
294 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
295 | 8.73k | a121 = |
296 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a111, |
297 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r21)); |
298 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
299 | 8.73k | a221 = |
300 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a211, |
301 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r21)); |
302 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
303 | 8.73k | a321 = |
304 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a311, |
305 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12, r21)); |
306 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
307 | 8.73k | a421 = |
308 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a411, |
309 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r13, r21)); |
310 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
311 | 8.73k | a031 = |
312 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a021, |
313 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r22)); |
314 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
315 | 8.73k | a131 = |
316 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a121, |
317 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r22)); |
318 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
319 | 8.73k | a231 = |
320 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a221, |
321 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r22)); |
322 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
323 | 8.73k | a331 = |
324 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a321, |
325 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r22)); |
326 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
327 | 8.73k | a431 = |
328 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a421, |
329 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12, r22)); |
330 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
331 | 8.73k | a041 = |
332 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a031, |
333 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r152, r23)); |
334 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
335 | 8.73k | a141 = |
336 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a131, |
337 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r23)); |
338 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
339 | 8.73k | a241 = |
340 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a231, |
341 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r23)); |
342 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
343 | 8.73k | a341 = |
344 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a331, |
345 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r23)); |
346 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
347 | 8.73k | a441 = |
348 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a431, |
349 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r11, r23)); |
350 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
351 | 8.73k | a051 = |
352 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a041, |
353 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r151, r24)); |
354 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
355 | 8.73k | a151 = |
356 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a141, |
357 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r152, r24)); |
358 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
359 | 8.73k | a251 = |
360 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a241, |
361 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r153, r24)); |
362 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
363 | 8.73k | a351 = |
364 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a341, |
365 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r154, r24)); |
366 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
367 | 8.73k | a451 = |
368 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a441, |
369 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r10, r24)); |
370 | 8.73k | Lib_IntVector_Intrinsics_vec256 t01 = a051; |
371 | 8.73k | Lib_IntVector_Intrinsics_vec256 t11 = a151; |
372 | 8.73k | Lib_IntVector_Intrinsics_vec256 t21 = a251; |
373 | 8.73k | Lib_IntVector_Intrinsics_vec256 t31 = a351; |
374 | 8.73k | Lib_IntVector_Intrinsics_vec256 t41 = a451; |
375 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
376 | 8.73k | mask261 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
377 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
378 | 8.73k | z04 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); |
379 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
380 | 8.73k | z14 = Lib_IntVector_Intrinsics_vec256_shift_right64(t31, (uint32_t)26U); |
381 | 8.73k | Lib_IntVector_Intrinsics_vec256 x03 = Lib_IntVector_Intrinsics_vec256_and(t01, mask261); |
382 | 8.73k | Lib_IntVector_Intrinsics_vec256 x33 = Lib_IntVector_Intrinsics_vec256_and(t31, mask261); |
383 | 8.73k | Lib_IntVector_Intrinsics_vec256 x13 = Lib_IntVector_Intrinsics_vec256_add64(t11, z04); |
384 | 8.73k | Lib_IntVector_Intrinsics_vec256 x43 = Lib_IntVector_Intrinsics_vec256_add64(t41, z14); |
385 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
386 | 8.73k | z011 = Lib_IntVector_Intrinsics_vec256_shift_right64(x13, (uint32_t)26U); |
387 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
388 | 8.73k | z111 = Lib_IntVector_Intrinsics_vec256_shift_right64(x43, (uint32_t)26U); |
389 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
390 | 8.73k | t6 = Lib_IntVector_Intrinsics_vec256_shift_left64(z111, (uint32_t)2U); |
391 | 8.73k | Lib_IntVector_Intrinsics_vec256 z120 = Lib_IntVector_Intrinsics_vec256_add64(z111, t6); |
392 | 8.73k | Lib_IntVector_Intrinsics_vec256 x111 = Lib_IntVector_Intrinsics_vec256_and(x13, mask261); |
393 | 8.73k | Lib_IntVector_Intrinsics_vec256 x411 = Lib_IntVector_Intrinsics_vec256_and(x43, mask261); |
394 | 8.73k | Lib_IntVector_Intrinsics_vec256 x22 = Lib_IntVector_Intrinsics_vec256_add64(t21, z011); |
395 | 8.73k | Lib_IntVector_Intrinsics_vec256 x011 = Lib_IntVector_Intrinsics_vec256_add64(x03, z120); |
396 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
397 | 8.73k | z021 = Lib_IntVector_Intrinsics_vec256_shift_right64(x22, (uint32_t)26U); |
398 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
399 | 8.73k | z131 = Lib_IntVector_Intrinsics_vec256_shift_right64(x011, (uint32_t)26U); |
400 | 8.73k | Lib_IntVector_Intrinsics_vec256 x211 = Lib_IntVector_Intrinsics_vec256_and(x22, mask261); |
401 | 8.73k | Lib_IntVector_Intrinsics_vec256 x021 = Lib_IntVector_Intrinsics_vec256_and(x011, mask261); |
402 | 8.73k | Lib_IntVector_Intrinsics_vec256 x311 = Lib_IntVector_Intrinsics_vec256_add64(x33, z021); |
403 | 8.73k | Lib_IntVector_Intrinsics_vec256 x121 = Lib_IntVector_Intrinsics_vec256_add64(x111, z131); |
404 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
405 | 8.73k | z031 = Lib_IntVector_Intrinsics_vec256_shift_right64(x311, (uint32_t)26U); |
406 | 8.73k | Lib_IntVector_Intrinsics_vec256 x321 = Lib_IntVector_Intrinsics_vec256_and(x311, mask261); |
407 | 8.73k | Lib_IntVector_Intrinsics_vec256 x421 = Lib_IntVector_Intrinsics_vec256_add64(x411, z031); |
408 | 8.73k | Lib_IntVector_Intrinsics_vec256 r30 = x021; |
409 | 8.73k | Lib_IntVector_Intrinsics_vec256 r31 = x121; |
410 | 8.73k | Lib_IntVector_Intrinsics_vec256 r32 = x211; |
411 | 8.73k | Lib_IntVector_Intrinsics_vec256 r33 = x321; |
412 | 8.73k | Lib_IntVector_Intrinsics_vec256 r34 = x421; |
413 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
414 | 8.73k | v12120 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r20, r10); |
415 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
416 | 8.73k | v34340 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r40, r30); |
417 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
418 | 8.73k | r12340 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34340, v12120); |
419 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
420 | 8.73k | v12121 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r21, r11); |
421 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
422 | 8.73k | v34341 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r41, r31); |
423 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
424 | 8.73k | r12341 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34341, v12121); |
425 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
426 | 8.73k | v12122 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r22, r12); |
427 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
428 | 8.73k | v34342 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r42, r32); |
429 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
430 | 8.73k | r12342 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34342, v12122); |
431 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
432 | 8.73k | v12123 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r23, r13); |
433 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
434 | 8.73k | v34343 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r43, r33); |
435 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
436 | 8.73k | r12343 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34343, v12123); |
437 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
438 | 8.73k | v12124 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r24, r14); |
439 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
440 | 8.73k | v34344 = Lib_IntVector_Intrinsics_vec256_interleave_low64(r44, r34); |
441 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
442 | 8.73k | r12344 = Lib_IntVector_Intrinsics_vec256_interleave_low128(v34344, v12124); |
443 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
444 | 8.73k | r123451 = Lib_IntVector_Intrinsics_vec256_smul64(r12341, (uint64_t)5U); |
445 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
446 | 8.73k | r123452 = Lib_IntVector_Intrinsics_vec256_smul64(r12342, (uint64_t)5U); |
447 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
448 | 8.73k | r123453 = Lib_IntVector_Intrinsics_vec256_smul64(r12343, (uint64_t)5U); |
449 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
450 | 8.73k | r123454 = Lib_IntVector_Intrinsics_vec256_smul64(r12344, (uint64_t)5U); |
451 | 8.73k | Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_mul64(r12340, a0); |
452 | 8.73k | Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_mul64(r12341, a0); |
453 | 8.73k | Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_mul64(r12342, a0); |
454 | 8.73k | Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_mul64(r12343, a0); |
455 | 8.73k | Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_mul64(r12344, a0); |
456 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
457 | 8.73k | a02 = |
458 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a01, |
459 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123454, a1)); |
460 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
461 | 8.73k | a12 = |
462 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a11, |
463 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12340, a1)); |
464 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
465 | 8.73k | a22 = |
466 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a21, |
467 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12341, a1)); |
468 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
469 | 8.73k | a32 = |
470 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a31, |
471 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12342, a1)); |
472 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
473 | 8.73k | a42 = |
474 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a41, |
475 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12343, a1)); |
476 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
477 | 8.73k | a03 = |
478 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a02, |
479 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123453, a2)); |
480 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
481 | 8.73k | a13 = |
482 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a12, |
483 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123454, a2)); |
484 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
485 | 8.73k | a23 = |
486 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a22, |
487 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12340, a2)); |
488 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
489 | 8.73k | a33 = |
490 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a32, |
491 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12341, a2)); |
492 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
493 | 8.73k | a43 = |
494 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a42, |
495 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12342, a2)); |
496 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
497 | 8.73k | a04 = |
498 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a03, |
499 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123452, a3)); |
500 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
501 | 8.73k | a14 = |
502 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a13, |
503 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123453, a3)); |
504 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
505 | 8.73k | a24 = |
506 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a23, |
507 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123454, a3)); |
508 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
509 | 8.73k | a34 = |
510 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a33, |
511 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12340, a3)); |
512 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
513 | 8.73k | a44 = |
514 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a43, |
515 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12341, a3)); |
516 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
517 | 8.73k | a05 = |
518 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a04, |
519 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123451, a4)); |
520 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
521 | 8.73k | a15 = |
522 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a14, |
523 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123452, a4)); |
524 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
525 | 8.73k | a25 = |
526 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a24, |
527 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123453, a4)); |
528 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
529 | 8.73k | a35 = |
530 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a34, |
531 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r123454, a4)); |
532 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
533 | 8.73k | a45 = |
534 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(a44, |
535 | 8.73k | Lib_IntVector_Intrinsics_vec256_mul64(r12340, a4)); |
536 | 8.73k | Lib_IntVector_Intrinsics_vec256 t0 = a05; |
537 | 8.73k | Lib_IntVector_Intrinsics_vec256 t1 = a15; |
538 | 8.73k | Lib_IntVector_Intrinsics_vec256 t2 = a25; |
539 | 8.73k | Lib_IntVector_Intrinsics_vec256 t3 = a35; |
540 | 8.73k | Lib_IntVector_Intrinsics_vec256 t4 = a45; |
541 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
542 | 8.73k | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
543 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
544 | 8.73k | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); |
545 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
546 | 8.73k | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
547 | 8.73k | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); |
548 | 8.73k | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
549 | 8.73k | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); |
550 | 8.73k | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
551 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
552 | 8.73k | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
553 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
554 | 8.73k | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
555 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
556 | 8.73k | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
557 | 8.73k | Lib_IntVector_Intrinsics_vec256 z121 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
558 | 8.73k | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
559 | 8.73k | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
560 | 8.73k | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
561 | 8.73k | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z121); |
562 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
563 | 8.73k | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
564 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
565 | 8.73k | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
566 | 8.73k | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
567 | 8.73k | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
568 | 8.73k | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
569 | 8.73k | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
570 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
571 | 8.73k | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
572 | 8.73k | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
573 | 8.73k | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
574 | 8.73k | Lib_IntVector_Intrinsics_vec256 o0 = x02; |
575 | 8.73k | Lib_IntVector_Intrinsics_vec256 o10 = x12; |
576 | 8.73k | Lib_IntVector_Intrinsics_vec256 o20 = x21; |
577 | 8.73k | Lib_IntVector_Intrinsics_vec256 o30 = x32; |
578 | 8.73k | Lib_IntVector_Intrinsics_vec256 o40 = x42; |
579 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
580 | 8.73k | v00 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o0, o0); |
581 | 8.73k | Lib_IntVector_Intrinsics_vec256 v10 = Lib_IntVector_Intrinsics_vec256_add64(o0, v00); |
582 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
583 | 8.73k | v10h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v10, v10); |
584 | 8.73k | Lib_IntVector_Intrinsics_vec256 v20 = Lib_IntVector_Intrinsics_vec256_add64(v10, v10h); |
585 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
586 | 8.73k | v01 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o10, o10); |
587 | 8.73k | Lib_IntVector_Intrinsics_vec256 v11 = Lib_IntVector_Intrinsics_vec256_add64(o10, v01); |
588 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
589 | 8.73k | v11h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v11, v11); |
590 | 8.73k | Lib_IntVector_Intrinsics_vec256 v21 = Lib_IntVector_Intrinsics_vec256_add64(v11, v11h); |
591 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
592 | 8.73k | v02 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o20, o20); |
593 | 8.73k | Lib_IntVector_Intrinsics_vec256 v12 = Lib_IntVector_Intrinsics_vec256_add64(o20, v02); |
594 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
595 | 8.73k | v12h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v12, v12); |
596 | 8.73k | Lib_IntVector_Intrinsics_vec256 v22 = Lib_IntVector_Intrinsics_vec256_add64(v12, v12h); |
597 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
598 | 8.73k | v03 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o30, o30); |
599 | 8.73k | Lib_IntVector_Intrinsics_vec256 v13 = Lib_IntVector_Intrinsics_vec256_add64(o30, v03); |
600 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
601 | 8.73k | v13h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v13, v13); |
602 | 8.73k | Lib_IntVector_Intrinsics_vec256 v23 = Lib_IntVector_Intrinsics_vec256_add64(v13, v13h); |
603 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
604 | 8.73k | v04 = Lib_IntVector_Intrinsics_vec256_interleave_high128(o40, o40); |
605 | 8.73k | Lib_IntVector_Intrinsics_vec256 v14 = Lib_IntVector_Intrinsics_vec256_add64(o40, v04); |
606 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
607 | 8.73k | v14h = Lib_IntVector_Intrinsics_vec256_interleave_high64(v14, v14); |
608 | 8.73k | Lib_IntVector_Intrinsics_vec256 v24 = Lib_IntVector_Intrinsics_vec256_add64(v14, v14h); |
609 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
610 | 8.73k | l = Lib_IntVector_Intrinsics_vec256_add64(v20, Lib_IntVector_Intrinsics_vec256_zero); |
611 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
612 | 8.73k | tmp0 = |
613 | 8.73k | Lib_IntVector_Intrinsics_vec256_and(l, |
614 | 8.73k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
615 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
616 | 8.73k | c0 = Lib_IntVector_Intrinsics_vec256_shift_right64(l, (uint32_t)26U); |
617 | 8.73k | Lib_IntVector_Intrinsics_vec256 l0 = Lib_IntVector_Intrinsics_vec256_add64(v21, c0); |
618 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
619 | 8.73k | tmp1 = |
620 | 8.73k | Lib_IntVector_Intrinsics_vec256_and(l0, |
621 | 8.73k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
622 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
623 | 8.73k | c1 = Lib_IntVector_Intrinsics_vec256_shift_right64(l0, (uint32_t)26U); |
624 | 8.73k | Lib_IntVector_Intrinsics_vec256 l1 = Lib_IntVector_Intrinsics_vec256_add64(v22, c1); |
625 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
626 | 8.73k | tmp2 = |
627 | 8.73k | Lib_IntVector_Intrinsics_vec256_and(l1, |
628 | 8.73k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
629 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
630 | 8.73k | c2 = Lib_IntVector_Intrinsics_vec256_shift_right64(l1, (uint32_t)26U); |
631 | 8.73k | Lib_IntVector_Intrinsics_vec256 l2 = Lib_IntVector_Intrinsics_vec256_add64(v23, c2); |
632 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
633 | 8.73k | tmp3 = |
634 | 8.73k | Lib_IntVector_Intrinsics_vec256_and(l2, |
635 | 8.73k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
636 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
637 | 8.73k | c3 = Lib_IntVector_Intrinsics_vec256_shift_right64(l2, (uint32_t)26U); |
638 | 8.73k | Lib_IntVector_Intrinsics_vec256 l3 = Lib_IntVector_Intrinsics_vec256_add64(v24, c3); |
639 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
640 | 8.73k | tmp4 = |
641 | 8.73k | Lib_IntVector_Intrinsics_vec256_and(l3, |
642 | 8.73k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
643 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
644 | 8.73k | c4 = Lib_IntVector_Intrinsics_vec256_shift_right64(l3, (uint32_t)26U); |
645 | 8.73k | Lib_IntVector_Intrinsics_vec256 |
646 | 8.73k | o00 = |
647 | 8.73k | Lib_IntVector_Intrinsics_vec256_add64(tmp0, |
648 | 8.73k | Lib_IntVector_Intrinsics_vec256_smul64(c4, (uint64_t)5U)); |
649 | 8.73k | Lib_IntVector_Intrinsics_vec256 o1 = tmp1; |
650 | 8.73k | Lib_IntVector_Intrinsics_vec256 o2 = tmp2; |
651 | 8.73k | Lib_IntVector_Intrinsics_vec256 o3 = tmp3; |
652 | 8.73k | Lib_IntVector_Intrinsics_vec256 o4 = tmp4; |
653 | 8.73k | out[0U] = o00; |
654 | 8.73k | out[1U] = o1; |
655 | 8.73k | out[2U] = o2; |
656 | 8.73k | out[3U] = o3; |
657 | 8.73k | out[4U] = o4; |
658 | 8.73k | } |
659 | | |
660 | | void |
661 | | Hacl_Poly1305_256_poly1305_init(Lib_IntVector_Intrinsics_vec256 *ctx, uint8_t *key) |
662 | 16.3k | { |
663 | 16.3k | Lib_IntVector_Intrinsics_vec256 *acc = ctx; |
664 | 16.3k | Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; |
665 | 16.3k | uint8_t *kr = key; |
666 | 16.3k | acc[0U] = Lib_IntVector_Intrinsics_vec256_zero; |
667 | 16.3k | acc[1U] = Lib_IntVector_Intrinsics_vec256_zero; |
668 | 16.3k | acc[2U] = Lib_IntVector_Intrinsics_vec256_zero; |
669 | 16.3k | acc[3U] = Lib_IntVector_Intrinsics_vec256_zero; |
670 | 16.3k | acc[4U] = Lib_IntVector_Intrinsics_vec256_zero; |
671 | 16.3k | uint64_t u0 = load64_le(kr); |
672 | 16.3k | uint64_t lo = u0; |
673 | 16.3k | uint64_t u = load64_le(kr + (uint32_t)8U); |
674 | 16.3k | uint64_t hi = u; |
675 | 16.3k | uint64_t mask0 = (uint64_t)0x0ffffffc0fffffffU; |
676 | 16.3k | uint64_t mask1 = (uint64_t)0x0ffffffc0ffffffcU; |
677 | 16.3k | uint64_t lo1 = lo & mask0; |
678 | 16.3k | uint64_t hi1 = hi & mask1; |
679 | 16.3k | Lib_IntVector_Intrinsics_vec256 *r = pre; |
680 | 16.3k | Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; |
681 | 16.3k | Lib_IntVector_Intrinsics_vec256 *rn = pre + (uint32_t)10U; |
682 | 16.3k | Lib_IntVector_Intrinsics_vec256 *rn_5 = pre + (uint32_t)15U; |
683 | 16.3k | Lib_IntVector_Intrinsics_vec256 r_vec0 = Lib_IntVector_Intrinsics_vec256_load64(lo1); |
684 | 16.3k | Lib_IntVector_Intrinsics_vec256 r_vec1 = Lib_IntVector_Intrinsics_vec256_load64(hi1); |
685 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
686 | 16.3k | f00 = |
687 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(r_vec0, |
688 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
689 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
690 | 16.3k | f15 = |
691 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec0, |
692 | 16.3k | (uint32_t)26U), |
693 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
694 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
695 | 16.3k | f20 = |
696 | 16.3k | Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec0, |
697 | 16.3k | (uint32_t)52U), |
698 | 16.3k | Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(r_vec1, |
699 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), |
700 | 16.3k | (uint32_t)12U)); |
701 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
702 | 16.3k | f30 = |
703 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec1, |
704 | 16.3k | (uint32_t)14U), |
705 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
706 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
707 | 16.3k | f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(r_vec1, (uint32_t)40U); |
708 | 16.3k | Lib_IntVector_Intrinsics_vec256 f0 = f00; |
709 | 16.3k | Lib_IntVector_Intrinsics_vec256 f1 = f15; |
710 | 16.3k | Lib_IntVector_Intrinsics_vec256 f2 = f20; |
711 | 16.3k | Lib_IntVector_Intrinsics_vec256 f3 = f30; |
712 | 16.3k | Lib_IntVector_Intrinsics_vec256 f4 = f40; |
713 | 16.3k | r[0U] = f0; |
714 | 16.3k | r[1U] = f1; |
715 | 16.3k | r[2U] = f2; |
716 | 16.3k | r[3U] = f3; |
717 | 16.3k | r[4U] = f4; |
718 | 16.3k | Lib_IntVector_Intrinsics_vec256 f200 = r[0U]; |
719 | 16.3k | Lib_IntVector_Intrinsics_vec256 f210 = r[1U]; |
720 | 16.3k | Lib_IntVector_Intrinsics_vec256 f220 = r[2U]; |
721 | 16.3k | Lib_IntVector_Intrinsics_vec256 f230 = r[3U]; |
722 | 16.3k | Lib_IntVector_Intrinsics_vec256 f240 = r[4U]; |
723 | 16.3k | r5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f200, (uint64_t)5U); |
724 | 16.3k | r5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f210, (uint64_t)5U); |
725 | 16.3k | r5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f220, (uint64_t)5U); |
726 | 16.3k | r5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f230, (uint64_t)5U); |
727 | 16.3k | r5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f240, (uint64_t)5U); |
728 | 16.3k | Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; |
729 | 16.3k | Lib_IntVector_Intrinsics_vec256 r10 = r[1U]; |
730 | 16.3k | Lib_IntVector_Intrinsics_vec256 r20 = r[2U]; |
731 | 16.3k | Lib_IntVector_Intrinsics_vec256 r30 = r[3U]; |
732 | 16.3k | Lib_IntVector_Intrinsics_vec256 r40 = r[4U]; |
733 | 16.3k | Lib_IntVector_Intrinsics_vec256 r510 = r5[1U]; |
734 | 16.3k | Lib_IntVector_Intrinsics_vec256 r520 = r5[2U]; |
735 | 16.3k | Lib_IntVector_Intrinsics_vec256 r530 = r5[3U]; |
736 | 16.3k | Lib_IntVector_Intrinsics_vec256 r540 = r5[4U]; |
737 | 16.3k | Lib_IntVector_Intrinsics_vec256 f100 = r[0U]; |
738 | 16.3k | Lib_IntVector_Intrinsics_vec256 f110 = r[1U]; |
739 | 16.3k | Lib_IntVector_Intrinsics_vec256 f120 = r[2U]; |
740 | 16.3k | Lib_IntVector_Intrinsics_vec256 f130 = r[3U]; |
741 | 16.3k | Lib_IntVector_Intrinsics_vec256 f140 = r[4U]; |
742 | 16.3k | Lib_IntVector_Intrinsics_vec256 a00 = Lib_IntVector_Intrinsics_vec256_mul64(r0, f100); |
743 | 16.3k | Lib_IntVector_Intrinsics_vec256 a10 = Lib_IntVector_Intrinsics_vec256_mul64(r10, f100); |
744 | 16.3k | Lib_IntVector_Intrinsics_vec256 a20 = Lib_IntVector_Intrinsics_vec256_mul64(r20, f100); |
745 | 16.3k | Lib_IntVector_Intrinsics_vec256 a30 = Lib_IntVector_Intrinsics_vec256_mul64(r30, f100); |
746 | 16.3k | Lib_IntVector_Intrinsics_vec256 a40 = Lib_IntVector_Intrinsics_vec256_mul64(r40, f100); |
747 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
748 | 16.3k | a010 = |
749 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a00, |
750 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r540, f110)); |
751 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
752 | 16.3k | a110 = |
753 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a10, |
754 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r0, f110)); |
755 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
756 | 16.3k | a210 = |
757 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a20, |
758 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r10, f110)); |
759 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
760 | 16.3k | a310 = |
761 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a30, |
762 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r20, f110)); |
763 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
764 | 16.3k | a410 = |
765 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a40, |
766 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r30, f110)); |
767 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
768 | 16.3k | a020 = |
769 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a010, |
770 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r530, f120)); |
771 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
772 | 16.3k | a120 = |
773 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a110, |
774 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r540, f120)); |
775 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
776 | 16.3k | a220 = |
777 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a210, |
778 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r0, f120)); |
779 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
780 | 16.3k | a320 = |
781 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a310, |
782 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r10, f120)); |
783 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
784 | 16.3k | a420 = |
785 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a410, |
786 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r20, f120)); |
787 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
788 | 16.3k | a030 = |
789 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a020, |
790 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r520, f130)); |
791 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
792 | 16.3k | a130 = |
793 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a120, |
794 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r530, f130)); |
795 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
796 | 16.3k | a230 = |
797 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a220, |
798 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r540, f130)); |
799 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
800 | 16.3k | a330 = |
801 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a320, |
802 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r0, f130)); |
803 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
804 | 16.3k | a430 = |
805 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a420, |
806 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r10, f130)); |
807 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
808 | 16.3k | a040 = |
809 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a030, |
810 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r510, f140)); |
811 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
812 | 16.3k | a140 = |
813 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a130, |
814 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r520, f140)); |
815 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
816 | 16.3k | a240 = |
817 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a230, |
818 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r530, f140)); |
819 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
820 | 16.3k | a340 = |
821 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a330, |
822 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r540, f140)); |
823 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
824 | 16.3k | a440 = |
825 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a430, |
826 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r0, f140)); |
827 | 16.3k | Lib_IntVector_Intrinsics_vec256 t00 = a040; |
828 | 16.3k | Lib_IntVector_Intrinsics_vec256 t10 = a140; |
829 | 16.3k | Lib_IntVector_Intrinsics_vec256 t20 = a240; |
830 | 16.3k | Lib_IntVector_Intrinsics_vec256 t30 = a340; |
831 | 16.3k | Lib_IntVector_Intrinsics_vec256 t40 = a440; |
832 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
833 | 16.3k | mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
834 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
835 | 16.3k | z00 = Lib_IntVector_Intrinsics_vec256_shift_right64(t00, (uint32_t)26U); |
836 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
837 | 16.3k | z10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)26U); |
838 | 16.3k | Lib_IntVector_Intrinsics_vec256 x00 = Lib_IntVector_Intrinsics_vec256_and(t00, mask260); |
839 | 16.3k | Lib_IntVector_Intrinsics_vec256 x30 = Lib_IntVector_Intrinsics_vec256_and(t30, mask260); |
840 | 16.3k | Lib_IntVector_Intrinsics_vec256 x10 = Lib_IntVector_Intrinsics_vec256_add64(t10, z00); |
841 | 16.3k | Lib_IntVector_Intrinsics_vec256 x40 = Lib_IntVector_Intrinsics_vec256_add64(t40, z10); |
842 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
843 | 16.3k | z010 = Lib_IntVector_Intrinsics_vec256_shift_right64(x10, (uint32_t)26U); |
844 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
845 | 16.3k | z110 = Lib_IntVector_Intrinsics_vec256_shift_right64(x40, (uint32_t)26U); |
846 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
847 | 16.3k | t5 = Lib_IntVector_Intrinsics_vec256_shift_left64(z110, (uint32_t)2U); |
848 | 16.3k | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z110, t5); |
849 | 16.3k | Lib_IntVector_Intrinsics_vec256 x110 = Lib_IntVector_Intrinsics_vec256_and(x10, mask260); |
850 | 16.3k | Lib_IntVector_Intrinsics_vec256 x410 = Lib_IntVector_Intrinsics_vec256_and(x40, mask260); |
851 | 16.3k | Lib_IntVector_Intrinsics_vec256 x20 = Lib_IntVector_Intrinsics_vec256_add64(t20, z010); |
852 | 16.3k | Lib_IntVector_Intrinsics_vec256 x010 = Lib_IntVector_Intrinsics_vec256_add64(x00, z12); |
853 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
854 | 16.3k | z020 = Lib_IntVector_Intrinsics_vec256_shift_right64(x20, (uint32_t)26U); |
855 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
856 | 16.3k | z130 = Lib_IntVector_Intrinsics_vec256_shift_right64(x010, (uint32_t)26U); |
857 | 16.3k | Lib_IntVector_Intrinsics_vec256 x210 = Lib_IntVector_Intrinsics_vec256_and(x20, mask260); |
858 | 16.3k | Lib_IntVector_Intrinsics_vec256 x020 = Lib_IntVector_Intrinsics_vec256_and(x010, mask260); |
859 | 16.3k | Lib_IntVector_Intrinsics_vec256 x310 = Lib_IntVector_Intrinsics_vec256_add64(x30, z020); |
860 | 16.3k | Lib_IntVector_Intrinsics_vec256 x120 = Lib_IntVector_Intrinsics_vec256_add64(x110, z130); |
861 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
862 | 16.3k | z030 = Lib_IntVector_Intrinsics_vec256_shift_right64(x310, (uint32_t)26U); |
863 | 16.3k | Lib_IntVector_Intrinsics_vec256 x320 = Lib_IntVector_Intrinsics_vec256_and(x310, mask260); |
864 | 16.3k | Lib_IntVector_Intrinsics_vec256 x420 = Lib_IntVector_Intrinsics_vec256_add64(x410, z030); |
865 | 16.3k | Lib_IntVector_Intrinsics_vec256 o00 = x020; |
866 | 16.3k | Lib_IntVector_Intrinsics_vec256 o10 = x120; |
867 | 16.3k | Lib_IntVector_Intrinsics_vec256 o20 = x210; |
868 | 16.3k | Lib_IntVector_Intrinsics_vec256 o30 = x320; |
869 | 16.3k | Lib_IntVector_Intrinsics_vec256 o40 = x420; |
870 | 16.3k | rn[0U] = o00; |
871 | 16.3k | rn[1U] = o10; |
872 | 16.3k | rn[2U] = o20; |
873 | 16.3k | rn[3U] = o30; |
874 | 16.3k | rn[4U] = o40; |
875 | 16.3k | Lib_IntVector_Intrinsics_vec256 f201 = rn[0U]; |
876 | 16.3k | Lib_IntVector_Intrinsics_vec256 f211 = rn[1U]; |
877 | 16.3k | Lib_IntVector_Intrinsics_vec256 f221 = rn[2U]; |
878 | 16.3k | Lib_IntVector_Intrinsics_vec256 f231 = rn[3U]; |
879 | 16.3k | Lib_IntVector_Intrinsics_vec256 f241 = rn[4U]; |
880 | 16.3k | rn_5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f201, (uint64_t)5U); |
881 | 16.3k | rn_5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f211, (uint64_t)5U); |
882 | 16.3k | rn_5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f221, (uint64_t)5U); |
883 | 16.3k | rn_5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f231, (uint64_t)5U); |
884 | 16.3k | rn_5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f241, (uint64_t)5U); |
885 | 16.3k | Lib_IntVector_Intrinsics_vec256 r00 = rn[0U]; |
886 | 16.3k | Lib_IntVector_Intrinsics_vec256 r1 = rn[1U]; |
887 | 16.3k | Lib_IntVector_Intrinsics_vec256 r2 = rn[2U]; |
888 | 16.3k | Lib_IntVector_Intrinsics_vec256 r3 = rn[3U]; |
889 | 16.3k | Lib_IntVector_Intrinsics_vec256 r4 = rn[4U]; |
890 | 16.3k | Lib_IntVector_Intrinsics_vec256 r51 = rn_5[1U]; |
891 | 16.3k | Lib_IntVector_Intrinsics_vec256 r52 = rn_5[2U]; |
892 | 16.3k | Lib_IntVector_Intrinsics_vec256 r53 = rn_5[3U]; |
893 | 16.3k | Lib_IntVector_Intrinsics_vec256 r54 = rn_5[4U]; |
894 | 16.3k | Lib_IntVector_Intrinsics_vec256 f10 = rn[0U]; |
895 | 16.3k | Lib_IntVector_Intrinsics_vec256 f11 = rn[1U]; |
896 | 16.3k | Lib_IntVector_Intrinsics_vec256 f12 = rn[2U]; |
897 | 16.3k | Lib_IntVector_Intrinsics_vec256 f13 = rn[3U]; |
898 | 16.3k | Lib_IntVector_Intrinsics_vec256 f14 = rn[4U]; |
899 | 16.3k | Lib_IntVector_Intrinsics_vec256 a0 = Lib_IntVector_Intrinsics_vec256_mul64(r00, f10); |
900 | 16.3k | Lib_IntVector_Intrinsics_vec256 a1 = Lib_IntVector_Intrinsics_vec256_mul64(r1, f10); |
901 | 16.3k | Lib_IntVector_Intrinsics_vec256 a2 = Lib_IntVector_Intrinsics_vec256_mul64(r2, f10); |
902 | 16.3k | Lib_IntVector_Intrinsics_vec256 a3 = Lib_IntVector_Intrinsics_vec256_mul64(r3, f10); |
903 | 16.3k | Lib_IntVector_Intrinsics_vec256 a4 = Lib_IntVector_Intrinsics_vec256_mul64(r4, f10); |
904 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
905 | 16.3k | a01 = |
906 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a0, |
907 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r54, f11)); |
908 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
909 | 16.3k | a11 = |
910 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a1, |
911 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r00, f11)); |
912 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
913 | 16.3k | a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, Lib_IntVector_Intrinsics_vec256_mul64(r1, f11)); |
914 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
915 | 16.3k | a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, Lib_IntVector_Intrinsics_vec256_mul64(r2, f11)); |
916 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
917 | 16.3k | a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, Lib_IntVector_Intrinsics_vec256_mul64(r3, f11)); |
918 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
919 | 16.3k | a02 = |
920 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a01, |
921 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r53, f12)); |
922 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
923 | 16.3k | a12 = |
924 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a11, |
925 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r54, f12)); |
926 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
927 | 16.3k | a22 = |
928 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a21, |
929 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r00, f12)); |
930 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
931 | 16.3k | a32 = |
932 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a31, |
933 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r1, f12)); |
934 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
935 | 16.3k | a42 = |
936 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a41, |
937 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r2, f12)); |
938 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
939 | 16.3k | a03 = |
940 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a02, |
941 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r52, f13)); |
942 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
943 | 16.3k | a13 = |
944 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a12, |
945 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r53, f13)); |
946 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
947 | 16.3k | a23 = |
948 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a22, |
949 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r54, f13)); |
950 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
951 | 16.3k | a33 = |
952 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a32, |
953 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r00, f13)); |
954 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
955 | 16.3k | a43 = |
956 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a42, |
957 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r1, f13)); |
958 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
959 | 16.3k | a04 = |
960 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a03, |
961 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r51, f14)); |
962 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
963 | 16.3k | a14 = |
964 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a13, |
965 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r52, f14)); |
966 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
967 | 16.3k | a24 = |
968 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a23, |
969 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r53, f14)); |
970 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
971 | 16.3k | a34 = |
972 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a33, |
973 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r54, f14)); |
974 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
975 | 16.3k | a44 = |
976 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(a43, |
977 | 16.3k | Lib_IntVector_Intrinsics_vec256_mul64(r00, f14)); |
978 | 16.3k | Lib_IntVector_Intrinsics_vec256 t0 = a04; |
979 | 16.3k | Lib_IntVector_Intrinsics_vec256 t1 = a14; |
980 | 16.3k | Lib_IntVector_Intrinsics_vec256 t2 = a24; |
981 | 16.3k | Lib_IntVector_Intrinsics_vec256 t3 = a34; |
982 | 16.3k | Lib_IntVector_Intrinsics_vec256 t4 = a44; |
983 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
984 | 16.3k | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
985 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
986 | 16.3k | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); |
987 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
988 | 16.3k | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
989 | 16.3k | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); |
990 | 16.3k | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
991 | 16.3k | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); |
992 | 16.3k | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
993 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
994 | 16.3k | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
995 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
996 | 16.3k | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
997 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
998 | 16.3k | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
999 | 16.3k | Lib_IntVector_Intrinsics_vec256 z120 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
1000 | 16.3k | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
1001 | 16.3k | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
1002 | 16.3k | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
1003 | 16.3k | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z120); |
1004 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1005 | 16.3k | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
1006 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1007 | 16.3k | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
1008 | 16.3k | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
1009 | 16.3k | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
1010 | 16.3k | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
1011 | 16.3k | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
1012 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1013 | 16.3k | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
1014 | 16.3k | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
1015 | 16.3k | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
1016 | 16.3k | Lib_IntVector_Intrinsics_vec256 o0 = x02; |
1017 | 16.3k | Lib_IntVector_Intrinsics_vec256 o1 = x12; |
1018 | 16.3k | Lib_IntVector_Intrinsics_vec256 o2 = x21; |
1019 | 16.3k | Lib_IntVector_Intrinsics_vec256 o3 = x32; |
1020 | 16.3k | Lib_IntVector_Intrinsics_vec256 o4 = x42; |
1021 | 16.3k | rn[0U] = o0; |
1022 | 16.3k | rn[1U] = o1; |
1023 | 16.3k | rn[2U] = o2; |
1024 | 16.3k | rn[3U] = o3; |
1025 | 16.3k | rn[4U] = o4; |
1026 | 16.3k | Lib_IntVector_Intrinsics_vec256 f202 = rn[0U]; |
1027 | 16.3k | Lib_IntVector_Intrinsics_vec256 f21 = rn[1U]; |
1028 | 16.3k | Lib_IntVector_Intrinsics_vec256 f22 = rn[2U]; |
1029 | 16.3k | Lib_IntVector_Intrinsics_vec256 f23 = rn[3U]; |
1030 | 16.3k | Lib_IntVector_Intrinsics_vec256 f24 = rn[4U]; |
1031 | 16.3k | rn_5[0U] = Lib_IntVector_Intrinsics_vec256_smul64(f202, (uint64_t)5U); |
1032 | 16.3k | rn_5[1U] = Lib_IntVector_Intrinsics_vec256_smul64(f21, (uint64_t)5U); |
1033 | 16.3k | rn_5[2U] = Lib_IntVector_Intrinsics_vec256_smul64(f22, (uint64_t)5U); |
1034 | 16.3k | rn_5[3U] = Lib_IntVector_Intrinsics_vec256_smul64(f23, (uint64_t)5U); |
1035 | 16.3k | rn_5[4U] = Lib_IntVector_Intrinsics_vec256_smul64(f24, (uint64_t)5U); |
1036 | 16.3k | } |
1037 | | |
1038 | | void |
1039 | | Hacl_Poly1305_256_poly1305_update1(Lib_IntVector_Intrinsics_vec256 *ctx, uint8_t *text) |
1040 | 0 | { |
1041 | 0 | Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; |
1042 | 0 | Lib_IntVector_Intrinsics_vec256 *acc = ctx; |
1043 | 0 | KRML_PRE_ALIGN(32) |
1044 | 0 | Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; |
1045 | 0 | uint64_t u0 = load64_le(text); |
1046 | 0 | uint64_t lo = u0; |
1047 | 0 | uint64_t u = load64_le(text + (uint32_t)8U); |
1048 | 0 | uint64_t hi = u; |
1049 | 0 | Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); |
1050 | 0 | Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); |
1051 | 0 | Lib_IntVector_Intrinsics_vec256 |
1052 | 0 | f010 = |
1053 | 0 | Lib_IntVector_Intrinsics_vec256_and(f0, |
1054 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1055 | 0 | Lib_IntVector_Intrinsics_vec256 |
1056 | 0 | f110 = |
1057 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1058 | 0 | (uint32_t)26U), |
1059 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1060 | 0 | Lib_IntVector_Intrinsics_vec256 |
1061 | 0 | f20 = |
1062 | 0 | Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1063 | 0 | (uint32_t)52U), |
1064 | 0 | Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, |
1065 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), |
1066 | 0 | (uint32_t)12U)); |
1067 | 0 | Lib_IntVector_Intrinsics_vec256 |
1068 | 0 | f30 = |
1069 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, |
1070 | 0 | (uint32_t)14U), |
1071 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1072 | 0 | Lib_IntVector_Intrinsics_vec256 |
1073 | 0 | f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); |
1074 | 0 | Lib_IntVector_Intrinsics_vec256 f01 = f010; |
1075 | 0 | Lib_IntVector_Intrinsics_vec256 f111 = f110; |
1076 | 0 | Lib_IntVector_Intrinsics_vec256 f2 = f20; |
1077 | 0 | Lib_IntVector_Intrinsics_vec256 f3 = f30; |
1078 | 0 | Lib_IntVector_Intrinsics_vec256 f41 = f40; |
1079 | 0 | e[0U] = f01; |
1080 | 0 | e[1U] = f111; |
1081 | 0 | e[2U] = f2; |
1082 | 0 | e[3U] = f3; |
1083 | 0 | e[4U] = f41; |
1084 | 0 | uint64_t b = (uint64_t)0x1000000U; |
1085 | 0 | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); |
1086 | 0 | Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; |
1087 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); |
1088 | 0 | Lib_IntVector_Intrinsics_vec256 *r = pre; |
1089 | 0 | Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; |
1090 | 0 | Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; |
1091 | 0 | Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; |
1092 | 0 | Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; |
1093 | 0 | Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; |
1094 | 0 | Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; |
1095 | 0 | Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; |
1096 | 0 | Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; |
1097 | 0 | Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; |
1098 | 0 | Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; |
1099 | 0 | Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; |
1100 | 0 | Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; |
1101 | 0 | Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; |
1102 | 0 | Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; |
1103 | 0 | Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; |
1104 | 0 | Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; |
1105 | 0 | Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; |
1106 | 0 | Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; |
1107 | 0 | Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; |
1108 | 0 | Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; |
1109 | 0 | Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); |
1110 | 0 | Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); |
1111 | 0 | Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); |
1112 | 0 | Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); |
1113 | 0 | Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); |
1114 | 0 | Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); |
1115 | 0 | Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); |
1116 | 0 | Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); |
1117 | 0 | Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); |
1118 | 0 | Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); |
1119 | 0 | Lib_IntVector_Intrinsics_vec256 |
1120 | 0 | a03 = |
1121 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a02, |
1122 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); |
1123 | 0 | Lib_IntVector_Intrinsics_vec256 |
1124 | 0 | a13 = |
1125 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a12, |
1126 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); |
1127 | 0 | Lib_IntVector_Intrinsics_vec256 |
1128 | 0 | a23 = |
1129 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a22, |
1130 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); |
1131 | 0 | Lib_IntVector_Intrinsics_vec256 |
1132 | 0 | a33 = |
1133 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a32, |
1134 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); |
1135 | 0 | Lib_IntVector_Intrinsics_vec256 |
1136 | 0 | a43 = |
1137 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a42, |
1138 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); |
1139 | 0 | Lib_IntVector_Intrinsics_vec256 |
1140 | 0 | a04 = |
1141 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a03, |
1142 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); |
1143 | 0 | Lib_IntVector_Intrinsics_vec256 |
1144 | 0 | a14 = |
1145 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a13, |
1146 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); |
1147 | 0 | Lib_IntVector_Intrinsics_vec256 |
1148 | 0 | a24 = |
1149 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a23, |
1150 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); |
1151 | 0 | Lib_IntVector_Intrinsics_vec256 |
1152 | 0 | a34 = |
1153 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a33, |
1154 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); |
1155 | 0 | Lib_IntVector_Intrinsics_vec256 |
1156 | 0 | a44 = |
1157 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a43, |
1158 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); |
1159 | 0 | Lib_IntVector_Intrinsics_vec256 |
1160 | 0 | a05 = |
1161 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a04, |
1162 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); |
1163 | 0 | Lib_IntVector_Intrinsics_vec256 |
1164 | 0 | a15 = |
1165 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a14, |
1166 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); |
1167 | 0 | Lib_IntVector_Intrinsics_vec256 |
1168 | 0 | a25 = |
1169 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a24, |
1170 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); |
1171 | 0 | Lib_IntVector_Intrinsics_vec256 |
1172 | 0 | a35 = |
1173 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a34, |
1174 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); |
1175 | 0 | Lib_IntVector_Intrinsics_vec256 |
1176 | 0 | a45 = |
1177 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a44, |
1178 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); |
1179 | 0 | Lib_IntVector_Intrinsics_vec256 |
1180 | 0 | a06 = |
1181 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a05, |
1182 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); |
1183 | 0 | Lib_IntVector_Intrinsics_vec256 |
1184 | 0 | a16 = |
1185 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a15, |
1186 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); |
1187 | 0 | Lib_IntVector_Intrinsics_vec256 |
1188 | 0 | a26 = |
1189 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a25, |
1190 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); |
1191 | 0 | Lib_IntVector_Intrinsics_vec256 |
1192 | 0 | a36 = |
1193 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a35, |
1194 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); |
1195 | 0 | Lib_IntVector_Intrinsics_vec256 |
1196 | 0 | a46 = |
1197 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a45, |
1198 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); |
1199 | 0 | Lib_IntVector_Intrinsics_vec256 t0 = a06; |
1200 | 0 | Lib_IntVector_Intrinsics_vec256 t1 = a16; |
1201 | 0 | Lib_IntVector_Intrinsics_vec256 t2 = a26; |
1202 | 0 | Lib_IntVector_Intrinsics_vec256 t3 = a36; |
1203 | 0 | Lib_IntVector_Intrinsics_vec256 t4 = a46; |
1204 | 0 | Lib_IntVector_Intrinsics_vec256 |
1205 | 0 | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
1206 | 0 | Lib_IntVector_Intrinsics_vec256 |
1207 | 0 | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t0, (uint32_t)26U); |
1208 | 0 | Lib_IntVector_Intrinsics_vec256 |
1209 | 0 | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
1210 | 0 | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t0, mask26); |
1211 | 0 | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
1212 | 0 | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); |
1213 | 0 | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
1214 | 0 | Lib_IntVector_Intrinsics_vec256 |
1215 | 0 | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
1216 | 0 | Lib_IntVector_Intrinsics_vec256 |
1217 | 0 | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
1218 | 0 | Lib_IntVector_Intrinsics_vec256 |
1219 | 0 | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
1220 | 0 | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
1221 | 0 | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
1222 | 0 | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
1223 | 0 | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
1224 | 0 | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); |
1225 | 0 | Lib_IntVector_Intrinsics_vec256 |
1226 | 0 | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
1227 | 0 | Lib_IntVector_Intrinsics_vec256 |
1228 | 0 | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
1229 | 0 | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
1230 | 0 | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
1231 | 0 | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
1232 | 0 | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
1233 | 0 | Lib_IntVector_Intrinsics_vec256 |
1234 | 0 | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
1235 | 0 | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
1236 | 0 | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
1237 | 0 | Lib_IntVector_Intrinsics_vec256 o0 = x02; |
1238 | 0 | Lib_IntVector_Intrinsics_vec256 o1 = x12; |
1239 | 0 | Lib_IntVector_Intrinsics_vec256 o2 = x21; |
1240 | 0 | Lib_IntVector_Intrinsics_vec256 o3 = x32; |
1241 | 0 | Lib_IntVector_Intrinsics_vec256 o4 = x42; |
1242 | 0 | acc[0U] = o0; |
1243 | 0 | acc[1U] = o1; |
1244 | 0 | acc[2U] = o2; |
1245 | 0 | acc[3U] = o3; |
1246 | 0 | acc[4U] = o4; |
1247 | 0 | } |
1248 | | |
1249 | | void |
1250 | | Hacl_Poly1305_256_poly1305_update( |
1251 | | Lib_IntVector_Intrinsics_vec256 *ctx, |
1252 | | uint32_t len, |
1253 | | uint8_t *text) |
1254 | 0 | { |
1255 | 0 | Lib_IntVector_Intrinsics_vec256 *pre = ctx + (uint32_t)5U; |
1256 | 0 | Lib_IntVector_Intrinsics_vec256 *acc = ctx; |
1257 | 0 | uint32_t sz_block = (uint32_t)64U; |
1258 | 0 | uint32_t len0 = len / sz_block * sz_block; |
1259 | 0 | uint8_t *t0 = text; |
1260 | 0 | if (len0 > (uint32_t)0U) { |
1261 | 0 | uint32_t bs = (uint32_t)64U; |
1262 | 0 | uint8_t *text0 = t0; |
1263 | 0 | Hacl_Impl_Poly1305_Field32xN_256_load_acc4(acc, text0); |
1264 | 0 | uint32_t len1 = len0 - bs; |
1265 | 0 | uint8_t *text1 = t0 + bs; |
1266 | 0 | uint32_t nb = len1 / bs; |
1267 | 0 | for (uint32_t i = (uint32_t)0U; i < nb; i++) { |
1268 | 0 | uint8_t *block = text1 + i * bs; |
1269 | 0 | KRML_PRE_ALIGN(32) |
1270 | 0 | Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; |
1271 | 0 | Lib_IntVector_Intrinsics_vec256 lo = Lib_IntVector_Intrinsics_vec256_load64_le(block); |
1272 | 0 | Lib_IntVector_Intrinsics_vec256 |
1273 | 0 | hi = Lib_IntVector_Intrinsics_vec256_load64_le(block + (uint32_t)32U); |
1274 | 0 | Lib_IntVector_Intrinsics_vec256 |
1275 | 0 | mask260 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
1276 | 0 | Lib_IntVector_Intrinsics_vec256 |
1277 | 0 | m0 = Lib_IntVector_Intrinsics_vec256_interleave_low128(lo, hi); |
1278 | 0 | Lib_IntVector_Intrinsics_vec256 |
1279 | 0 | m1 = Lib_IntVector_Intrinsics_vec256_interleave_high128(lo, hi); |
1280 | 0 | Lib_IntVector_Intrinsics_vec256 |
1281 | 0 | m2 = Lib_IntVector_Intrinsics_vec256_shift_right(m0, (uint32_t)48U); |
1282 | 0 | Lib_IntVector_Intrinsics_vec256 |
1283 | 0 | m3 = Lib_IntVector_Intrinsics_vec256_shift_right(m1, (uint32_t)48U); |
1284 | 0 | Lib_IntVector_Intrinsics_vec256 |
1285 | 0 | m4 = Lib_IntVector_Intrinsics_vec256_interleave_high64(m0, m1); |
1286 | 0 | Lib_IntVector_Intrinsics_vec256 |
1287 | 0 | t010 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m0, m1); |
1288 | 0 | Lib_IntVector_Intrinsics_vec256 |
1289 | 0 | t30 = Lib_IntVector_Intrinsics_vec256_interleave_low64(m2, m3); |
1290 | 0 | Lib_IntVector_Intrinsics_vec256 |
1291 | 0 | t20 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)4U); |
1292 | 0 | Lib_IntVector_Intrinsics_vec256 o20 = Lib_IntVector_Intrinsics_vec256_and(t20, mask260); |
1293 | 0 | Lib_IntVector_Intrinsics_vec256 |
1294 | 0 | t10 = Lib_IntVector_Intrinsics_vec256_shift_right64(t010, (uint32_t)26U); |
1295 | 0 | Lib_IntVector_Intrinsics_vec256 o10 = Lib_IntVector_Intrinsics_vec256_and(t10, mask260); |
1296 | 0 | Lib_IntVector_Intrinsics_vec256 o5 = Lib_IntVector_Intrinsics_vec256_and(t010, mask260); |
1297 | 0 | Lib_IntVector_Intrinsics_vec256 |
1298 | 0 | t31 = Lib_IntVector_Intrinsics_vec256_shift_right64(t30, (uint32_t)30U); |
1299 | 0 | Lib_IntVector_Intrinsics_vec256 o30 = Lib_IntVector_Intrinsics_vec256_and(t31, mask260); |
1300 | 0 | Lib_IntVector_Intrinsics_vec256 |
1301 | 0 | o40 = Lib_IntVector_Intrinsics_vec256_shift_right64(m4, (uint32_t)40U); |
1302 | 0 | Lib_IntVector_Intrinsics_vec256 o00 = o5; |
1303 | 0 | Lib_IntVector_Intrinsics_vec256 o11 = o10; |
1304 | 0 | Lib_IntVector_Intrinsics_vec256 o21 = o20; |
1305 | 0 | Lib_IntVector_Intrinsics_vec256 o31 = o30; |
1306 | 0 | Lib_IntVector_Intrinsics_vec256 o41 = o40; |
1307 | 0 | e[0U] = o00; |
1308 | 0 | e[1U] = o11; |
1309 | 0 | e[2U] = o21; |
1310 | 0 | e[3U] = o31; |
1311 | 0 | e[4U] = o41; |
1312 | 0 | uint64_t b = (uint64_t)0x1000000U; |
1313 | 0 | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); |
1314 | 0 | Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; |
1315 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); |
1316 | 0 | Lib_IntVector_Intrinsics_vec256 *rn = pre + (uint32_t)10U; |
1317 | 0 | Lib_IntVector_Intrinsics_vec256 *rn5 = pre + (uint32_t)15U; |
1318 | 0 | Lib_IntVector_Intrinsics_vec256 r0 = rn[0U]; |
1319 | 0 | Lib_IntVector_Intrinsics_vec256 r1 = rn[1U]; |
1320 | 0 | Lib_IntVector_Intrinsics_vec256 r2 = rn[2U]; |
1321 | 0 | Lib_IntVector_Intrinsics_vec256 r3 = rn[3U]; |
1322 | 0 | Lib_IntVector_Intrinsics_vec256 r4 = rn[4U]; |
1323 | 0 | Lib_IntVector_Intrinsics_vec256 r51 = rn5[1U]; |
1324 | 0 | Lib_IntVector_Intrinsics_vec256 r52 = rn5[2U]; |
1325 | 0 | Lib_IntVector_Intrinsics_vec256 r53 = rn5[3U]; |
1326 | 0 | Lib_IntVector_Intrinsics_vec256 r54 = rn5[4U]; |
1327 | 0 | Lib_IntVector_Intrinsics_vec256 f10 = acc[0U]; |
1328 | 0 | Lib_IntVector_Intrinsics_vec256 f110 = acc[1U]; |
1329 | 0 | Lib_IntVector_Intrinsics_vec256 f120 = acc[2U]; |
1330 | 0 | Lib_IntVector_Intrinsics_vec256 f130 = acc[3U]; |
1331 | 0 | Lib_IntVector_Intrinsics_vec256 f140 = acc[4U]; |
1332 | 0 | Lib_IntVector_Intrinsics_vec256 a0 = Lib_IntVector_Intrinsics_vec256_mul64(r0, f10); |
1333 | 0 | Lib_IntVector_Intrinsics_vec256 a1 = Lib_IntVector_Intrinsics_vec256_mul64(r1, f10); |
1334 | 0 | Lib_IntVector_Intrinsics_vec256 a2 = Lib_IntVector_Intrinsics_vec256_mul64(r2, f10); |
1335 | 0 | Lib_IntVector_Intrinsics_vec256 a3 = Lib_IntVector_Intrinsics_vec256_mul64(r3, f10); |
1336 | 0 | Lib_IntVector_Intrinsics_vec256 a4 = Lib_IntVector_Intrinsics_vec256_mul64(r4, f10); |
1337 | 0 | Lib_IntVector_Intrinsics_vec256 |
1338 | 0 | a01 = |
1339 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a0, |
1340 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, f110)); |
1341 | 0 | Lib_IntVector_Intrinsics_vec256 |
1342 | 0 | a11 = |
1343 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a1, |
1344 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, f110)); |
1345 | 0 | Lib_IntVector_Intrinsics_vec256 |
1346 | 0 | a21 = |
1347 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a2, |
1348 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, f110)); |
1349 | 0 | Lib_IntVector_Intrinsics_vec256 |
1350 | 0 | a31 = |
1351 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a3, |
1352 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, f110)); |
1353 | 0 | Lib_IntVector_Intrinsics_vec256 |
1354 | 0 | a41 = |
1355 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a4, |
1356 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r3, f110)); |
1357 | 0 | Lib_IntVector_Intrinsics_vec256 |
1358 | 0 | a02 = |
1359 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a01, |
1360 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, f120)); |
1361 | 0 | Lib_IntVector_Intrinsics_vec256 |
1362 | 0 | a12 = |
1363 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a11, |
1364 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, f120)); |
1365 | 0 | Lib_IntVector_Intrinsics_vec256 |
1366 | 0 | a22 = |
1367 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a21, |
1368 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, f120)); |
1369 | 0 | Lib_IntVector_Intrinsics_vec256 |
1370 | 0 | a32 = |
1371 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a31, |
1372 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, f120)); |
1373 | 0 | Lib_IntVector_Intrinsics_vec256 |
1374 | 0 | a42 = |
1375 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a41, |
1376 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, f120)); |
1377 | 0 | Lib_IntVector_Intrinsics_vec256 |
1378 | 0 | a03 = |
1379 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a02, |
1380 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, f130)); |
1381 | 0 | Lib_IntVector_Intrinsics_vec256 |
1382 | 0 | a13 = |
1383 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a12, |
1384 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, f130)); |
1385 | 0 | Lib_IntVector_Intrinsics_vec256 |
1386 | 0 | a23 = |
1387 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a22, |
1388 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, f130)); |
1389 | 0 | Lib_IntVector_Intrinsics_vec256 |
1390 | 0 | a33 = |
1391 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a32, |
1392 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, f130)); |
1393 | 0 | Lib_IntVector_Intrinsics_vec256 |
1394 | 0 | a43 = |
1395 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a42, |
1396 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, f130)); |
1397 | 0 | Lib_IntVector_Intrinsics_vec256 |
1398 | 0 | a04 = |
1399 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a03, |
1400 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r51, f140)); |
1401 | 0 | Lib_IntVector_Intrinsics_vec256 |
1402 | 0 | a14 = |
1403 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a13, |
1404 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, f140)); |
1405 | 0 | Lib_IntVector_Intrinsics_vec256 |
1406 | 0 | a24 = |
1407 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a23, |
1408 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, f140)); |
1409 | 0 | Lib_IntVector_Intrinsics_vec256 |
1410 | 0 | a34 = |
1411 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a33, |
1412 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, f140)); |
1413 | 0 | Lib_IntVector_Intrinsics_vec256 |
1414 | 0 | a44 = |
1415 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a43, |
1416 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, f140)); |
1417 | 0 | Lib_IntVector_Intrinsics_vec256 t01 = a04; |
1418 | 0 | Lib_IntVector_Intrinsics_vec256 t1 = a14; |
1419 | 0 | Lib_IntVector_Intrinsics_vec256 t2 = a24; |
1420 | 0 | Lib_IntVector_Intrinsics_vec256 t3 = a34; |
1421 | 0 | Lib_IntVector_Intrinsics_vec256 t4 = a44; |
1422 | 0 | Lib_IntVector_Intrinsics_vec256 |
1423 | 0 | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
1424 | 0 | Lib_IntVector_Intrinsics_vec256 |
1425 | 0 | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); |
1426 | 0 | Lib_IntVector_Intrinsics_vec256 |
1427 | 0 | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
1428 | 0 | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); |
1429 | 0 | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
1430 | 0 | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t1, z0); |
1431 | 0 | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
1432 | 0 | Lib_IntVector_Intrinsics_vec256 |
1433 | 0 | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
1434 | 0 | Lib_IntVector_Intrinsics_vec256 |
1435 | 0 | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
1436 | 0 | Lib_IntVector_Intrinsics_vec256 |
1437 | 0 | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
1438 | 0 | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
1439 | 0 | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
1440 | 0 | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
1441 | 0 | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
1442 | 0 | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); |
1443 | 0 | Lib_IntVector_Intrinsics_vec256 |
1444 | 0 | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
1445 | 0 | Lib_IntVector_Intrinsics_vec256 |
1446 | 0 | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
1447 | 0 | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
1448 | 0 | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
1449 | 0 | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
1450 | 0 | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
1451 | 0 | Lib_IntVector_Intrinsics_vec256 |
1452 | 0 | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
1453 | 0 | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
1454 | 0 | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
1455 | 0 | Lib_IntVector_Intrinsics_vec256 o01 = x02; |
1456 | 0 | Lib_IntVector_Intrinsics_vec256 o12 = x12; |
1457 | 0 | Lib_IntVector_Intrinsics_vec256 o22 = x21; |
1458 | 0 | Lib_IntVector_Intrinsics_vec256 o32 = x32; |
1459 | 0 | Lib_IntVector_Intrinsics_vec256 o42 = x42; |
1460 | 0 | acc[0U] = o01; |
1461 | 0 | acc[1U] = o12; |
1462 | 0 | acc[2U] = o22; |
1463 | 0 | acc[3U] = o32; |
1464 | 0 | acc[4U] = o42; |
1465 | 0 | Lib_IntVector_Intrinsics_vec256 f100 = acc[0U]; |
1466 | 0 | Lib_IntVector_Intrinsics_vec256 f11 = acc[1U]; |
1467 | 0 | Lib_IntVector_Intrinsics_vec256 f12 = acc[2U]; |
1468 | 0 | Lib_IntVector_Intrinsics_vec256 f13 = acc[3U]; |
1469 | 0 | Lib_IntVector_Intrinsics_vec256 f14 = acc[4U]; |
1470 | 0 | Lib_IntVector_Intrinsics_vec256 f20 = e[0U]; |
1471 | 0 | Lib_IntVector_Intrinsics_vec256 f21 = e[1U]; |
1472 | 0 | Lib_IntVector_Intrinsics_vec256 f22 = e[2U]; |
1473 | 0 | Lib_IntVector_Intrinsics_vec256 f23 = e[3U]; |
1474 | 0 | Lib_IntVector_Intrinsics_vec256 f24 = e[4U]; |
1475 | 0 | Lib_IntVector_Intrinsics_vec256 o0 = Lib_IntVector_Intrinsics_vec256_add64(f100, f20); |
1476 | 0 | Lib_IntVector_Intrinsics_vec256 o1 = Lib_IntVector_Intrinsics_vec256_add64(f11, f21); |
1477 | 0 | Lib_IntVector_Intrinsics_vec256 o2 = Lib_IntVector_Intrinsics_vec256_add64(f12, f22); |
1478 | 0 | Lib_IntVector_Intrinsics_vec256 o3 = Lib_IntVector_Intrinsics_vec256_add64(f13, f23); |
1479 | 0 | Lib_IntVector_Intrinsics_vec256 o4 = Lib_IntVector_Intrinsics_vec256_add64(f14, f24); |
1480 | 0 | acc[0U] = o0; |
1481 | 0 | acc[1U] = o1; |
1482 | 0 | acc[2U] = o2; |
1483 | 0 | acc[3U] = o3; |
1484 | 0 | acc[4U] = o4; |
1485 | 0 | } |
1486 | 0 | Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize(acc, pre); |
1487 | 0 | } |
1488 | 0 | uint32_t len1 = len - len0; |
1489 | 0 | uint8_t *t1 = text + len0; |
1490 | 0 | uint32_t nb = len1 / (uint32_t)16U; |
1491 | 0 | uint32_t rem = len1 % (uint32_t)16U; |
1492 | 0 | for (uint32_t i = (uint32_t)0U; i < nb; i++) { |
1493 | 0 | uint8_t *block = t1 + i * (uint32_t)16U; |
1494 | 0 | KRML_PRE_ALIGN(32) |
1495 | 0 | Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; |
1496 | 0 | uint64_t u0 = load64_le(block); |
1497 | 0 | uint64_t lo = u0; |
1498 | 0 | uint64_t u = load64_le(block + (uint32_t)8U); |
1499 | 0 | uint64_t hi = u; |
1500 | 0 | Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); |
1501 | 0 | Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); |
1502 | 0 | Lib_IntVector_Intrinsics_vec256 |
1503 | 0 | f010 = |
1504 | 0 | Lib_IntVector_Intrinsics_vec256_and(f0, |
1505 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1506 | 0 | Lib_IntVector_Intrinsics_vec256 |
1507 | 0 | f110 = |
1508 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1509 | 0 | (uint32_t)26U), |
1510 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1511 | 0 | Lib_IntVector_Intrinsics_vec256 |
1512 | 0 | f20 = |
1513 | 0 | Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1514 | 0 | (uint32_t)52U), |
1515 | 0 | Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, |
1516 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), |
1517 | 0 | (uint32_t)12U)); |
1518 | 0 | Lib_IntVector_Intrinsics_vec256 |
1519 | 0 | f30 = |
1520 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, |
1521 | 0 | (uint32_t)14U), |
1522 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1523 | 0 | Lib_IntVector_Intrinsics_vec256 |
1524 | 0 | f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); |
1525 | 0 | Lib_IntVector_Intrinsics_vec256 f01 = f010; |
1526 | 0 | Lib_IntVector_Intrinsics_vec256 f111 = f110; |
1527 | 0 | Lib_IntVector_Intrinsics_vec256 f2 = f20; |
1528 | 0 | Lib_IntVector_Intrinsics_vec256 f3 = f30; |
1529 | 0 | Lib_IntVector_Intrinsics_vec256 f41 = f40; |
1530 | 0 | e[0U] = f01; |
1531 | 0 | e[1U] = f111; |
1532 | 0 | e[2U] = f2; |
1533 | 0 | e[3U] = f3; |
1534 | 0 | e[4U] = f41; |
1535 | 0 | uint64_t b = (uint64_t)0x1000000U; |
1536 | 0 | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); |
1537 | 0 | Lib_IntVector_Intrinsics_vec256 f4 = e[4U]; |
1538 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec256_or(f4, mask); |
1539 | 0 | Lib_IntVector_Intrinsics_vec256 *r = pre; |
1540 | 0 | Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; |
1541 | 0 | Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; |
1542 | 0 | Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; |
1543 | 0 | Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; |
1544 | 0 | Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; |
1545 | 0 | Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; |
1546 | 0 | Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; |
1547 | 0 | Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; |
1548 | 0 | Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; |
1549 | 0 | Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; |
1550 | 0 | Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; |
1551 | 0 | Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; |
1552 | 0 | Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; |
1553 | 0 | Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; |
1554 | 0 | Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; |
1555 | 0 | Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; |
1556 | 0 | Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; |
1557 | 0 | Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; |
1558 | 0 | Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; |
1559 | 0 | Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; |
1560 | 0 | Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); |
1561 | 0 | Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); |
1562 | 0 | Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); |
1563 | 0 | Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); |
1564 | 0 | Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); |
1565 | 0 | Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); |
1566 | 0 | Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); |
1567 | 0 | Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); |
1568 | 0 | Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); |
1569 | 0 | Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); |
1570 | 0 | Lib_IntVector_Intrinsics_vec256 |
1571 | 0 | a03 = |
1572 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a02, |
1573 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); |
1574 | 0 | Lib_IntVector_Intrinsics_vec256 |
1575 | 0 | a13 = |
1576 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a12, |
1577 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); |
1578 | 0 | Lib_IntVector_Intrinsics_vec256 |
1579 | 0 | a23 = |
1580 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a22, |
1581 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); |
1582 | 0 | Lib_IntVector_Intrinsics_vec256 |
1583 | 0 | a33 = |
1584 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a32, |
1585 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); |
1586 | 0 | Lib_IntVector_Intrinsics_vec256 |
1587 | 0 | a43 = |
1588 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a42, |
1589 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); |
1590 | 0 | Lib_IntVector_Intrinsics_vec256 |
1591 | 0 | a04 = |
1592 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a03, |
1593 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); |
1594 | 0 | Lib_IntVector_Intrinsics_vec256 |
1595 | 0 | a14 = |
1596 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a13, |
1597 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); |
1598 | 0 | Lib_IntVector_Intrinsics_vec256 |
1599 | 0 | a24 = |
1600 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a23, |
1601 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); |
1602 | 0 | Lib_IntVector_Intrinsics_vec256 |
1603 | 0 | a34 = |
1604 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a33, |
1605 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); |
1606 | 0 | Lib_IntVector_Intrinsics_vec256 |
1607 | 0 | a44 = |
1608 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a43, |
1609 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); |
1610 | 0 | Lib_IntVector_Intrinsics_vec256 |
1611 | 0 | a05 = |
1612 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a04, |
1613 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); |
1614 | 0 | Lib_IntVector_Intrinsics_vec256 |
1615 | 0 | a15 = |
1616 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a14, |
1617 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); |
1618 | 0 | Lib_IntVector_Intrinsics_vec256 |
1619 | 0 | a25 = |
1620 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a24, |
1621 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); |
1622 | 0 | Lib_IntVector_Intrinsics_vec256 |
1623 | 0 | a35 = |
1624 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a34, |
1625 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); |
1626 | 0 | Lib_IntVector_Intrinsics_vec256 |
1627 | 0 | a45 = |
1628 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a44, |
1629 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); |
1630 | 0 | Lib_IntVector_Intrinsics_vec256 |
1631 | 0 | a06 = |
1632 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a05, |
1633 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); |
1634 | 0 | Lib_IntVector_Intrinsics_vec256 |
1635 | 0 | a16 = |
1636 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a15, |
1637 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); |
1638 | 0 | Lib_IntVector_Intrinsics_vec256 |
1639 | 0 | a26 = |
1640 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a25, |
1641 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); |
1642 | 0 | Lib_IntVector_Intrinsics_vec256 |
1643 | 0 | a36 = |
1644 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a35, |
1645 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); |
1646 | 0 | Lib_IntVector_Intrinsics_vec256 |
1647 | 0 | a46 = |
1648 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a45, |
1649 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); |
1650 | 0 | Lib_IntVector_Intrinsics_vec256 t01 = a06; |
1651 | 0 | Lib_IntVector_Intrinsics_vec256 t11 = a16; |
1652 | 0 | Lib_IntVector_Intrinsics_vec256 t2 = a26; |
1653 | 0 | Lib_IntVector_Intrinsics_vec256 t3 = a36; |
1654 | 0 | Lib_IntVector_Intrinsics_vec256 t4 = a46; |
1655 | 0 | Lib_IntVector_Intrinsics_vec256 |
1656 | 0 | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
1657 | 0 | Lib_IntVector_Intrinsics_vec256 |
1658 | 0 | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); |
1659 | 0 | Lib_IntVector_Intrinsics_vec256 |
1660 | 0 | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
1661 | 0 | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); |
1662 | 0 | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
1663 | 0 | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t11, z0); |
1664 | 0 | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
1665 | 0 | Lib_IntVector_Intrinsics_vec256 |
1666 | 0 | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
1667 | 0 | Lib_IntVector_Intrinsics_vec256 |
1668 | 0 | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
1669 | 0 | Lib_IntVector_Intrinsics_vec256 |
1670 | 0 | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
1671 | 0 | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
1672 | 0 | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
1673 | 0 | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
1674 | 0 | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
1675 | 0 | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); |
1676 | 0 | Lib_IntVector_Intrinsics_vec256 |
1677 | 0 | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
1678 | 0 | Lib_IntVector_Intrinsics_vec256 |
1679 | 0 | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
1680 | 0 | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
1681 | 0 | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
1682 | 0 | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
1683 | 0 | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
1684 | 0 | Lib_IntVector_Intrinsics_vec256 |
1685 | 0 | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
1686 | 0 | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
1687 | 0 | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
1688 | 0 | Lib_IntVector_Intrinsics_vec256 o0 = x02; |
1689 | 0 | Lib_IntVector_Intrinsics_vec256 o1 = x12; |
1690 | 0 | Lib_IntVector_Intrinsics_vec256 o2 = x21; |
1691 | 0 | Lib_IntVector_Intrinsics_vec256 o3 = x32; |
1692 | 0 | Lib_IntVector_Intrinsics_vec256 o4 = x42; |
1693 | 0 | acc[0U] = o0; |
1694 | 0 | acc[1U] = o1; |
1695 | 0 | acc[2U] = o2; |
1696 | 0 | acc[3U] = o3; |
1697 | 0 | acc[4U] = o4; |
1698 | 0 | } |
1699 | 0 | if (rem > (uint32_t)0U) { |
1700 | 0 | uint8_t *last = t1 + nb * (uint32_t)16U; |
1701 | 0 | KRML_PRE_ALIGN(32) |
1702 | 0 | Lib_IntVector_Intrinsics_vec256 e[5U] KRML_POST_ALIGN(32) = { 0U }; |
1703 | 0 | uint8_t tmp[16U] = { 0U }; |
1704 | 0 | memcpy(tmp, last, rem * sizeof(uint8_t)); |
1705 | 0 | uint64_t u0 = load64_le(tmp); |
1706 | 0 | uint64_t lo = u0; |
1707 | 0 | uint64_t u = load64_le(tmp + (uint32_t)8U); |
1708 | 0 | uint64_t hi = u; |
1709 | 0 | Lib_IntVector_Intrinsics_vec256 f0 = Lib_IntVector_Intrinsics_vec256_load64(lo); |
1710 | 0 | Lib_IntVector_Intrinsics_vec256 f1 = Lib_IntVector_Intrinsics_vec256_load64(hi); |
1711 | 0 | Lib_IntVector_Intrinsics_vec256 |
1712 | 0 | f010 = |
1713 | 0 | Lib_IntVector_Intrinsics_vec256_and(f0, |
1714 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1715 | 0 | Lib_IntVector_Intrinsics_vec256 |
1716 | 0 | f110 = |
1717 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1718 | 0 | (uint32_t)26U), |
1719 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1720 | 0 | Lib_IntVector_Intrinsics_vec256 |
1721 | 0 | f20 = |
1722 | 0 | Lib_IntVector_Intrinsics_vec256_or(Lib_IntVector_Intrinsics_vec256_shift_right64(f0, |
1723 | 0 | (uint32_t)52U), |
1724 | 0 | Lib_IntVector_Intrinsics_vec256_shift_left64(Lib_IntVector_Intrinsics_vec256_and(f1, |
1725 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffU)), |
1726 | 0 | (uint32_t)12U)); |
1727 | 0 | Lib_IntVector_Intrinsics_vec256 |
1728 | 0 | f30 = |
1729 | 0 | Lib_IntVector_Intrinsics_vec256_and(Lib_IntVector_Intrinsics_vec256_shift_right64(f1, |
1730 | 0 | (uint32_t)14U), |
1731 | 0 | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1732 | 0 | Lib_IntVector_Intrinsics_vec256 |
1733 | 0 | f40 = Lib_IntVector_Intrinsics_vec256_shift_right64(f1, (uint32_t)40U); |
1734 | 0 | Lib_IntVector_Intrinsics_vec256 f01 = f010; |
1735 | 0 | Lib_IntVector_Intrinsics_vec256 f111 = f110; |
1736 | 0 | Lib_IntVector_Intrinsics_vec256 f2 = f20; |
1737 | 0 | Lib_IntVector_Intrinsics_vec256 f3 = f30; |
1738 | 0 | Lib_IntVector_Intrinsics_vec256 f4 = f40; |
1739 | 0 | e[0U] = f01; |
1740 | 0 | e[1U] = f111; |
1741 | 0 | e[2U] = f2; |
1742 | 0 | e[3U] = f3; |
1743 | 0 | e[4U] = f4; |
1744 | 0 | uint64_t b = (uint64_t)1U << rem * (uint32_t)8U % (uint32_t)26U; |
1745 | 0 | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_load64(b); |
1746 | 0 | Lib_IntVector_Intrinsics_vec256 fi = e[rem * (uint32_t)8U / (uint32_t)26U]; |
1747 | 0 | e[rem * (uint32_t)8U / (uint32_t)26U] = Lib_IntVector_Intrinsics_vec256_or(fi, mask); |
1748 | 0 | Lib_IntVector_Intrinsics_vec256 *r = pre; |
1749 | 0 | Lib_IntVector_Intrinsics_vec256 *r5 = pre + (uint32_t)5U; |
1750 | 0 | Lib_IntVector_Intrinsics_vec256 r0 = r[0U]; |
1751 | 0 | Lib_IntVector_Intrinsics_vec256 r1 = r[1U]; |
1752 | 0 | Lib_IntVector_Intrinsics_vec256 r2 = r[2U]; |
1753 | 0 | Lib_IntVector_Intrinsics_vec256 r3 = r[3U]; |
1754 | 0 | Lib_IntVector_Intrinsics_vec256 r4 = r[4U]; |
1755 | 0 | Lib_IntVector_Intrinsics_vec256 r51 = r5[1U]; |
1756 | 0 | Lib_IntVector_Intrinsics_vec256 r52 = r5[2U]; |
1757 | 0 | Lib_IntVector_Intrinsics_vec256 r53 = r5[3U]; |
1758 | 0 | Lib_IntVector_Intrinsics_vec256 r54 = r5[4U]; |
1759 | 0 | Lib_IntVector_Intrinsics_vec256 f10 = e[0U]; |
1760 | 0 | Lib_IntVector_Intrinsics_vec256 f11 = e[1U]; |
1761 | 0 | Lib_IntVector_Intrinsics_vec256 f12 = e[2U]; |
1762 | 0 | Lib_IntVector_Intrinsics_vec256 f13 = e[3U]; |
1763 | 0 | Lib_IntVector_Intrinsics_vec256 f14 = e[4U]; |
1764 | 0 | Lib_IntVector_Intrinsics_vec256 a0 = acc[0U]; |
1765 | 0 | Lib_IntVector_Intrinsics_vec256 a1 = acc[1U]; |
1766 | 0 | Lib_IntVector_Intrinsics_vec256 a2 = acc[2U]; |
1767 | 0 | Lib_IntVector_Intrinsics_vec256 a3 = acc[3U]; |
1768 | 0 | Lib_IntVector_Intrinsics_vec256 a4 = acc[4U]; |
1769 | 0 | Lib_IntVector_Intrinsics_vec256 a01 = Lib_IntVector_Intrinsics_vec256_add64(a0, f10); |
1770 | 0 | Lib_IntVector_Intrinsics_vec256 a11 = Lib_IntVector_Intrinsics_vec256_add64(a1, f11); |
1771 | 0 | Lib_IntVector_Intrinsics_vec256 a21 = Lib_IntVector_Intrinsics_vec256_add64(a2, f12); |
1772 | 0 | Lib_IntVector_Intrinsics_vec256 a31 = Lib_IntVector_Intrinsics_vec256_add64(a3, f13); |
1773 | 0 | Lib_IntVector_Intrinsics_vec256 a41 = Lib_IntVector_Intrinsics_vec256_add64(a4, f14); |
1774 | 0 | Lib_IntVector_Intrinsics_vec256 a02 = Lib_IntVector_Intrinsics_vec256_mul64(r0, a01); |
1775 | 0 | Lib_IntVector_Intrinsics_vec256 a12 = Lib_IntVector_Intrinsics_vec256_mul64(r1, a01); |
1776 | 0 | Lib_IntVector_Intrinsics_vec256 a22 = Lib_IntVector_Intrinsics_vec256_mul64(r2, a01); |
1777 | 0 | Lib_IntVector_Intrinsics_vec256 a32 = Lib_IntVector_Intrinsics_vec256_mul64(r3, a01); |
1778 | 0 | Lib_IntVector_Intrinsics_vec256 a42 = Lib_IntVector_Intrinsics_vec256_mul64(r4, a01); |
1779 | 0 | Lib_IntVector_Intrinsics_vec256 |
1780 | 0 | a03 = |
1781 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a02, |
1782 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a11)); |
1783 | 0 | Lib_IntVector_Intrinsics_vec256 |
1784 | 0 | a13 = |
1785 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a12, |
1786 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a11)); |
1787 | 0 | Lib_IntVector_Intrinsics_vec256 |
1788 | 0 | a23 = |
1789 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a22, |
1790 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a11)); |
1791 | 0 | Lib_IntVector_Intrinsics_vec256 |
1792 | 0 | a33 = |
1793 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a32, |
1794 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a11)); |
1795 | 0 | Lib_IntVector_Intrinsics_vec256 |
1796 | 0 | a43 = |
1797 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a42, |
1798 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r3, a11)); |
1799 | 0 | Lib_IntVector_Intrinsics_vec256 |
1800 | 0 | a04 = |
1801 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a03, |
1802 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a21)); |
1803 | 0 | Lib_IntVector_Intrinsics_vec256 |
1804 | 0 | a14 = |
1805 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a13, |
1806 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a21)); |
1807 | 0 | Lib_IntVector_Intrinsics_vec256 |
1808 | 0 | a24 = |
1809 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a23, |
1810 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a21)); |
1811 | 0 | Lib_IntVector_Intrinsics_vec256 |
1812 | 0 | a34 = |
1813 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a33, |
1814 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a21)); |
1815 | 0 | Lib_IntVector_Intrinsics_vec256 |
1816 | 0 | a44 = |
1817 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a43, |
1818 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r2, a21)); |
1819 | 0 | Lib_IntVector_Intrinsics_vec256 |
1820 | 0 | a05 = |
1821 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a04, |
1822 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a31)); |
1823 | 0 | Lib_IntVector_Intrinsics_vec256 |
1824 | 0 | a15 = |
1825 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a14, |
1826 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a31)); |
1827 | 0 | Lib_IntVector_Intrinsics_vec256 |
1828 | 0 | a25 = |
1829 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a24, |
1830 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a31)); |
1831 | 0 | Lib_IntVector_Intrinsics_vec256 |
1832 | 0 | a35 = |
1833 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a34, |
1834 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a31)); |
1835 | 0 | Lib_IntVector_Intrinsics_vec256 |
1836 | 0 | a45 = |
1837 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a44, |
1838 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r1, a31)); |
1839 | 0 | Lib_IntVector_Intrinsics_vec256 |
1840 | 0 | a06 = |
1841 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a05, |
1842 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r51, a41)); |
1843 | 0 | Lib_IntVector_Intrinsics_vec256 |
1844 | 0 | a16 = |
1845 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a15, |
1846 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r52, a41)); |
1847 | 0 | Lib_IntVector_Intrinsics_vec256 |
1848 | 0 | a26 = |
1849 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a25, |
1850 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r53, a41)); |
1851 | 0 | Lib_IntVector_Intrinsics_vec256 |
1852 | 0 | a36 = |
1853 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a35, |
1854 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r54, a41)); |
1855 | 0 | Lib_IntVector_Intrinsics_vec256 |
1856 | 0 | a46 = |
1857 | 0 | Lib_IntVector_Intrinsics_vec256_add64(a45, |
1858 | 0 | Lib_IntVector_Intrinsics_vec256_mul64(r0, a41)); |
1859 | 0 | Lib_IntVector_Intrinsics_vec256 t01 = a06; |
1860 | 0 | Lib_IntVector_Intrinsics_vec256 t11 = a16; |
1861 | 0 | Lib_IntVector_Intrinsics_vec256 t2 = a26; |
1862 | 0 | Lib_IntVector_Intrinsics_vec256 t3 = a36; |
1863 | 0 | Lib_IntVector_Intrinsics_vec256 t4 = a46; |
1864 | 0 | Lib_IntVector_Intrinsics_vec256 |
1865 | 0 | mask26 = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
1866 | 0 | Lib_IntVector_Intrinsics_vec256 |
1867 | 0 | z0 = Lib_IntVector_Intrinsics_vec256_shift_right64(t01, (uint32_t)26U); |
1868 | 0 | Lib_IntVector_Intrinsics_vec256 |
1869 | 0 | z1 = Lib_IntVector_Intrinsics_vec256_shift_right64(t3, (uint32_t)26U); |
1870 | 0 | Lib_IntVector_Intrinsics_vec256 x0 = Lib_IntVector_Intrinsics_vec256_and(t01, mask26); |
1871 | 0 | Lib_IntVector_Intrinsics_vec256 x3 = Lib_IntVector_Intrinsics_vec256_and(t3, mask26); |
1872 | 0 | Lib_IntVector_Intrinsics_vec256 x1 = Lib_IntVector_Intrinsics_vec256_add64(t11, z0); |
1873 | 0 | Lib_IntVector_Intrinsics_vec256 x4 = Lib_IntVector_Intrinsics_vec256_add64(t4, z1); |
1874 | 0 | Lib_IntVector_Intrinsics_vec256 |
1875 | 0 | z01 = Lib_IntVector_Intrinsics_vec256_shift_right64(x1, (uint32_t)26U); |
1876 | 0 | Lib_IntVector_Intrinsics_vec256 |
1877 | 0 | z11 = Lib_IntVector_Intrinsics_vec256_shift_right64(x4, (uint32_t)26U); |
1878 | 0 | Lib_IntVector_Intrinsics_vec256 |
1879 | 0 | t = Lib_IntVector_Intrinsics_vec256_shift_left64(z11, (uint32_t)2U); |
1880 | 0 | Lib_IntVector_Intrinsics_vec256 z12 = Lib_IntVector_Intrinsics_vec256_add64(z11, t); |
1881 | 0 | Lib_IntVector_Intrinsics_vec256 x11 = Lib_IntVector_Intrinsics_vec256_and(x1, mask26); |
1882 | 0 | Lib_IntVector_Intrinsics_vec256 x41 = Lib_IntVector_Intrinsics_vec256_and(x4, mask26); |
1883 | 0 | Lib_IntVector_Intrinsics_vec256 x2 = Lib_IntVector_Intrinsics_vec256_add64(t2, z01); |
1884 | 0 | Lib_IntVector_Intrinsics_vec256 x01 = Lib_IntVector_Intrinsics_vec256_add64(x0, z12); |
1885 | 0 | Lib_IntVector_Intrinsics_vec256 |
1886 | 0 | z02 = Lib_IntVector_Intrinsics_vec256_shift_right64(x2, (uint32_t)26U); |
1887 | 0 | Lib_IntVector_Intrinsics_vec256 |
1888 | 0 | z13 = Lib_IntVector_Intrinsics_vec256_shift_right64(x01, (uint32_t)26U); |
1889 | 0 | Lib_IntVector_Intrinsics_vec256 x21 = Lib_IntVector_Intrinsics_vec256_and(x2, mask26); |
1890 | 0 | Lib_IntVector_Intrinsics_vec256 x02 = Lib_IntVector_Intrinsics_vec256_and(x01, mask26); |
1891 | 0 | Lib_IntVector_Intrinsics_vec256 x31 = Lib_IntVector_Intrinsics_vec256_add64(x3, z02); |
1892 | 0 | Lib_IntVector_Intrinsics_vec256 x12 = Lib_IntVector_Intrinsics_vec256_add64(x11, z13); |
1893 | 0 | Lib_IntVector_Intrinsics_vec256 |
1894 | 0 | z03 = Lib_IntVector_Intrinsics_vec256_shift_right64(x31, (uint32_t)26U); |
1895 | 0 | Lib_IntVector_Intrinsics_vec256 x32 = Lib_IntVector_Intrinsics_vec256_and(x31, mask26); |
1896 | 0 | Lib_IntVector_Intrinsics_vec256 x42 = Lib_IntVector_Intrinsics_vec256_add64(x41, z03); |
1897 | 0 | Lib_IntVector_Intrinsics_vec256 o0 = x02; |
1898 | 0 | Lib_IntVector_Intrinsics_vec256 o1 = x12; |
1899 | 0 | Lib_IntVector_Intrinsics_vec256 o2 = x21; |
1900 | 0 | Lib_IntVector_Intrinsics_vec256 o3 = x32; |
1901 | 0 | Lib_IntVector_Intrinsics_vec256 o4 = x42; |
1902 | 0 | acc[0U] = o0; |
1903 | 0 | acc[1U] = o1; |
1904 | 0 | acc[2U] = o2; |
1905 | 0 | acc[3U] = o3; |
1906 | 0 | acc[4U] = o4; |
1907 | 0 | return; |
1908 | 0 | } |
1909 | 0 | } |
1910 | | |
1911 | | void |
1912 | | Hacl_Poly1305_256_poly1305_finish( |
1913 | | uint8_t *tag, |
1914 | | uint8_t *key, |
1915 | | Lib_IntVector_Intrinsics_vec256 *ctx) |
1916 | 16.3k | { |
1917 | 16.3k | Lib_IntVector_Intrinsics_vec256 *acc = ctx; |
1918 | 16.3k | uint8_t *ks = key + (uint32_t)16U; |
1919 | 16.3k | Lib_IntVector_Intrinsics_vec256 f0 = acc[0U]; |
1920 | 16.3k | Lib_IntVector_Intrinsics_vec256 f13 = acc[1U]; |
1921 | 16.3k | Lib_IntVector_Intrinsics_vec256 f23 = acc[2U]; |
1922 | 16.3k | Lib_IntVector_Intrinsics_vec256 f33 = acc[3U]; |
1923 | 16.3k | Lib_IntVector_Intrinsics_vec256 f40 = acc[4U]; |
1924 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1925 | 16.3k | l0 = Lib_IntVector_Intrinsics_vec256_add64(f0, Lib_IntVector_Intrinsics_vec256_zero); |
1926 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1927 | 16.3k | tmp00 = |
1928 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l0, |
1929 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1930 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1931 | 16.3k | c00 = Lib_IntVector_Intrinsics_vec256_shift_right64(l0, (uint32_t)26U); |
1932 | 16.3k | Lib_IntVector_Intrinsics_vec256 l1 = Lib_IntVector_Intrinsics_vec256_add64(f13, c00); |
1933 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1934 | 16.3k | tmp10 = |
1935 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l1, |
1936 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1937 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1938 | 16.3k | c10 = Lib_IntVector_Intrinsics_vec256_shift_right64(l1, (uint32_t)26U); |
1939 | 16.3k | Lib_IntVector_Intrinsics_vec256 l2 = Lib_IntVector_Intrinsics_vec256_add64(f23, c10); |
1940 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1941 | 16.3k | tmp20 = |
1942 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l2, |
1943 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1944 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1945 | 16.3k | c20 = Lib_IntVector_Intrinsics_vec256_shift_right64(l2, (uint32_t)26U); |
1946 | 16.3k | Lib_IntVector_Intrinsics_vec256 l3 = Lib_IntVector_Intrinsics_vec256_add64(f33, c20); |
1947 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1948 | 16.3k | tmp30 = |
1949 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l3, |
1950 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1951 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1952 | 16.3k | c30 = Lib_IntVector_Intrinsics_vec256_shift_right64(l3, (uint32_t)26U); |
1953 | 16.3k | Lib_IntVector_Intrinsics_vec256 l4 = Lib_IntVector_Intrinsics_vec256_add64(f40, c30); |
1954 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1955 | 16.3k | tmp40 = |
1956 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l4, |
1957 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1958 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1959 | 16.3k | c40 = Lib_IntVector_Intrinsics_vec256_shift_right64(l4, (uint32_t)26U); |
1960 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1961 | 16.3k | f010 = |
1962 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(tmp00, |
1963 | 16.3k | Lib_IntVector_Intrinsics_vec256_smul64(c40, (uint64_t)5U)); |
1964 | 16.3k | Lib_IntVector_Intrinsics_vec256 f110 = tmp10; |
1965 | 16.3k | Lib_IntVector_Intrinsics_vec256 f210 = tmp20; |
1966 | 16.3k | Lib_IntVector_Intrinsics_vec256 f310 = tmp30; |
1967 | 16.3k | Lib_IntVector_Intrinsics_vec256 f410 = tmp40; |
1968 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1969 | 16.3k | l = Lib_IntVector_Intrinsics_vec256_add64(f010, Lib_IntVector_Intrinsics_vec256_zero); |
1970 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1971 | 16.3k | tmp0 = |
1972 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l, |
1973 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1974 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1975 | 16.3k | c0 = Lib_IntVector_Intrinsics_vec256_shift_right64(l, (uint32_t)26U); |
1976 | 16.3k | Lib_IntVector_Intrinsics_vec256 l5 = Lib_IntVector_Intrinsics_vec256_add64(f110, c0); |
1977 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1978 | 16.3k | tmp1 = |
1979 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l5, |
1980 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1981 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1982 | 16.3k | c1 = Lib_IntVector_Intrinsics_vec256_shift_right64(l5, (uint32_t)26U); |
1983 | 16.3k | Lib_IntVector_Intrinsics_vec256 l6 = Lib_IntVector_Intrinsics_vec256_add64(f210, c1); |
1984 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1985 | 16.3k | tmp2 = |
1986 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l6, |
1987 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1988 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1989 | 16.3k | c2 = Lib_IntVector_Intrinsics_vec256_shift_right64(l6, (uint32_t)26U); |
1990 | 16.3k | Lib_IntVector_Intrinsics_vec256 l7 = Lib_IntVector_Intrinsics_vec256_add64(f310, c2); |
1991 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1992 | 16.3k | tmp3 = |
1993 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l7, |
1994 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
1995 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1996 | 16.3k | c3 = Lib_IntVector_Intrinsics_vec256_shift_right64(l7, (uint32_t)26U); |
1997 | 16.3k | Lib_IntVector_Intrinsics_vec256 l8 = Lib_IntVector_Intrinsics_vec256_add64(f410, c3); |
1998 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
1999 | 16.3k | tmp4 = |
2000 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(l8, |
2001 | 16.3k | Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU)); |
2002 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2003 | 16.3k | c4 = Lib_IntVector_Intrinsics_vec256_shift_right64(l8, (uint32_t)26U); |
2004 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2005 | 16.3k | f02 = |
2006 | 16.3k | Lib_IntVector_Intrinsics_vec256_add64(tmp0, |
2007 | 16.3k | Lib_IntVector_Intrinsics_vec256_smul64(c4, (uint64_t)5U)); |
2008 | 16.3k | Lib_IntVector_Intrinsics_vec256 f12 = tmp1; |
2009 | 16.3k | Lib_IntVector_Intrinsics_vec256 f22 = tmp2; |
2010 | 16.3k | Lib_IntVector_Intrinsics_vec256 f32 = tmp3; |
2011 | 16.3k | Lib_IntVector_Intrinsics_vec256 f42 = tmp4; |
2012 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2013 | 16.3k | mh = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3ffffffU); |
2014 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2015 | 16.3k | ml = Lib_IntVector_Intrinsics_vec256_load64((uint64_t)0x3fffffbU); |
2016 | 16.3k | Lib_IntVector_Intrinsics_vec256 mask = Lib_IntVector_Intrinsics_vec256_eq64(f42, mh); |
2017 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2018 | 16.3k | mask1 = |
2019 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(mask, |
2020 | 16.3k | Lib_IntVector_Intrinsics_vec256_eq64(f32, mh)); |
2021 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2022 | 16.3k | mask2 = |
2023 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(mask1, |
2024 | 16.3k | Lib_IntVector_Intrinsics_vec256_eq64(f22, mh)); |
2025 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2026 | 16.3k | mask3 = |
2027 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(mask2, |
2028 | 16.3k | Lib_IntVector_Intrinsics_vec256_eq64(f12, mh)); |
2029 | 16.3k | Lib_IntVector_Intrinsics_vec256 |
2030 | 16.3k | mask4 = |
2031 | 16.3k | Lib_IntVector_Intrinsics_vec256_and(mask3, |
2032 | 16.3k | Lib_IntVector_Intrinsics_vec256_lognot(Lib_IntVector_Intrinsics_vec256_gt64(ml, f02))); |
2033 | 16.3k | Lib_IntVector_Intrinsics_vec256 ph = Lib_IntVector_Intrinsics_vec256_and(mask4, mh); |
2034 | 16.3k | Lib_IntVector_Intrinsics_vec256 pl = Lib_IntVector_Intrinsics_vec256_and(mask4, ml); |
2035 | 16.3k | Lib_IntVector_Intrinsics_vec256 o0 = Lib_IntVector_Intrinsics_vec256_sub64(f02, pl); |
2036 | 16.3k | Lib_IntVector_Intrinsics_vec256 o1 = Lib_IntVector_Intrinsics_vec256_sub64(f12, ph); |
2037 | 16.3k | Lib_IntVector_Intrinsics_vec256 o2 = Lib_IntVector_Intrinsics_vec256_sub64(f22, ph); |
2038 | 16.3k | Lib_IntVector_Intrinsics_vec256 o3 = Lib_IntVector_Intrinsics_vec256_sub64(f32, ph); |
2039 | 16.3k | Lib_IntVector_Intrinsics_vec256 o4 = Lib_IntVector_Intrinsics_vec256_sub64(f42, ph); |
2040 | 16.3k | Lib_IntVector_Intrinsics_vec256 f011 = o0; |
2041 | 16.3k | Lib_IntVector_Intrinsics_vec256 f111 = o1; |
2042 | 16.3k | Lib_IntVector_Intrinsics_vec256 f211 = o2; |
2043 | 16.3k | Lib_IntVector_Intrinsics_vec256 f311 = o3; |
2044 | 16.3k | Lib_IntVector_Intrinsics_vec256 f411 = o4; |
2045 | 16.3k | acc[0U] = f011; |
2046 | 16.3k | acc[1U] = f111; |
2047 | 16.3k | acc[2U] = f211; |
2048 | 16.3k | acc[3U] = f311; |
2049 | 16.3k | acc[4U] = f411; |
2050 | 16.3k | Lib_IntVector_Intrinsics_vec256 f00 = acc[0U]; |
2051 | 16.3k | Lib_IntVector_Intrinsics_vec256 f1 = acc[1U]; |
2052 | 16.3k | Lib_IntVector_Intrinsics_vec256 f2 = acc[2U]; |
2053 | 16.3k | Lib_IntVector_Intrinsics_vec256 f3 = acc[3U]; |
2054 | 16.3k | Lib_IntVector_Intrinsics_vec256 f4 = acc[4U]; |
2055 | 16.3k | uint64_t f01 = Lib_IntVector_Intrinsics_vec256_extract64(f00, (uint32_t)0U); |
2056 | 16.3k | uint64_t f112 = Lib_IntVector_Intrinsics_vec256_extract64(f1, (uint32_t)0U); |
2057 | 16.3k | uint64_t f212 = Lib_IntVector_Intrinsics_vec256_extract64(f2, (uint32_t)0U); |
2058 | 16.3k | uint64_t f312 = Lib_IntVector_Intrinsics_vec256_extract64(f3, (uint32_t)0U); |
2059 | 16.3k | uint64_t f41 = Lib_IntVector_Intrinsics_vec256_extract64(f4, (uint32_t)0U); |
2060 | 16.3k | uint64_t lo = (f01 | f112 << (uint32_t)26U) | f212 << (uint32_t)52U; |
2061 | 16.3k | uint64_t hi = (f212 >> (uint32_t)12U | f312 << (uint32_t)14U) | f41 << (uint32_t)40U; |
2062 | 16.3k | uint64_t f10 = lo; |
2063 | 16.3k | uint64_t f11 = hi; |
2064 | 16.3k | uint64_t u0 = load64_le(ks); |
2065 | 16.3k | uint64_t lo0 = u0; |
2066 | 16.3k | uint64_t u = load64_le(ks + (uint32_t)8U); |
2067 | 16.3k | uint64_t hi0 = u; |
2068 | 16.3k | uint64_t f20 = lo0; |
2069 | 16.3k | uint64_t f21 = hi0; |
2070 | 16.3k | uint64_t r0 = f10 + f20; |
2071 | 16.3k | uint64_t r1 = f11 + f21; |
2072 | 16.3k | uint64_t c = (r0 ^ ((r0 ^ f20) | ((r0 - f20) ^ f20))) >> (uint32_t)63U; |
2073 | 16.3k | uint64_t r11 = r1 + c; |
2074 | 16.3k | uint64_t f30 = r0; |
2075 | 16.3k | uint64_t f31 = r11; |
2076 | 16.3k | store64_le(tag, f30); |
2077 | 16.3k | store64_le(tag + (uint32_t)8U, f31); |
2078 | 16.3k | } |
2079 | | |
2080 | | void |
2081 | | Hacl_Poly1305_256_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key) |
2082 | 0 | { |
2083 | 0 | KRML_PRE_ALIGN(32) |
2084 | 0 | Lib_IntVector_Intrinsics_vec256 ctx[25U] KRML_POST_ALIGN(32) = { 0U }; |
2085 | 0 | Hacl_Poly1305_256_poly1305_init(ctx, key); |
2086 | 0 | Hacl_Poly1305_256_poly1305_update(ctx, len, text); |
2087 | 0 | Hacl_Poly1305_256_poly1305_finish(tag, key, ctx); |
2088 | 0 | } |