/src/nss/lib/freebl/verified/Hacl_Poly1305_128.c
Line | Count | Source (jump to first uncovered line) |
1 | | /* MIT License |
2 | | * |
3 | | * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation |
4 | | * Copyright (c) 2022-2023 HACL* Contributors |
5 | | * |
6 | | * Permission is hereby granted, free of charge, to any person obtaining a copy |
7 | | * of this software and associated documentation files (the "Software"), to deal |
8 | | * in the Software without restriction, including without limitation the rights |
9 | | * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
10 | | * copies of the Software, and to permit persons to whom the Software is |
11 | | * furnished to do so, subject to the following conditions: |
12 | | * |
13 | | * The above copyright notice and this permission notice shall be included in all |
14 | | * copies or substantial portions of the Software. |
15 | | * |
16 | | * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
17 | | * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
18 | | * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
19 | | * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
20 | | * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
21 | | * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE |
22 | | * SOFTWARE. |
23 | | */ |
24 | | |
25 | | #include "internal/Hacl_Poly1305_128.h" |
26 | | |
27 | | void |
28 | | Hacl_Impl_Poly1305_Field32xN_128_load_acc2(Lib_IntVector_Intrinsics_vec128 *acc, uint8_t *b) |
29 | 0 | { |
30 | 0 | KRML_PRE_ALIGN(16) |
31 | 0 | Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; |
32 | 0 | Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(b); |
33 | 0 | Lib_IntVector_Intrinsics_vec128 |
34 | 0 | b2 = Lib_IntVector_Intrinsics_vec128_load64_le(b + (uint32_t)16U); |
35 | 0 | Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2); |
36 | 0 | Lib_IntVector_Intrinsics_vec128 hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2); |
37 | 0 | Lib_IntVector_Intrinsics_vec128 |
38 | 0 | f00 = |
39 | 0 | Lib_IntVector_Intrinsics_vec128_and(lo, |
40 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
41 | 0 | Lib_IntVector_Intrinsics_vec128 |
42 | 0 | f10 = |
43 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, |
44 | 0 | (uint32_t)26U), |
45 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
46 | 0 | Lib_IntVector_Intrinsics_vec128 |
47 | 0 | f20 = |
48 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, |
49 | 0 | (uint32_t)52U), |
50 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(hi, |
51 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
52 | 0 | (uint32_t)12U)); |
53 | 0 | Lib_IntVector_Intrinsics_vec128 |
54 | 0 | f30 = |
55 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(hi, |
56 | 0 | (uint32_t)14U), |
57 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
58 | 0 | Lib_IntVector_Intrinsics_vec128 |
59 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(hi, (uint32_t)40U); |
60 | 0 | Lib_IntVector_Intrinsics_vec128 f02 = f00; |
61 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = f10; |
62 | 0 | Lib_IntVector_Intrinsics_vec128 f22 = f20; |
63 | 0 | Lib_IntVector_Intrinsics_vec128 f32 = f30; |
64 | 0 | Lib_IntVector_Intrinsics_vec128 f42 = f40; |
65 | 0 | e[0U] = f02; |
66 | 0 | e[1U] = f12; |
67 | 0 | e[2U] = f22; |
68 | 0 | e[3U] = f32; |
69 | 0 | e[4U] = f42; |
70 | 0 | uint64_t b10 = (uint64_t)0x1000000U; |
71 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b10); |
72 | 0 | Lib_IntVector_Intrinsics_vec128 f43 = e[4U]; |
73 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec128_or(f43, mask); |
74 | 0 | Lib_IntVector_Intrinsics_vec128 acc0 = acc[0U]; |
75 | 0 | Lib_IntVector_Intrinsics_vec128 acc1 = acc[1U]; |
76 | 0 | Lib_IntVector_Intrinsics_vec128 acc2 = acc[2U]; |
77 | 0 | Lib_IntVector_Intrinsics_vec128 acc3 = acc[3U]; |
78 | 0 | Lib_IntVector_Intrinsics_vec128 acc4 = acc[4U]; |
79 | 0 | Lib_IntVector_Intrinsics_vec128 e0 = e[0U]; |
80 | 0 | Lib_IntVector_Intrinsics_vec128 e1 = e[1U]; |
81 | 0 | Lib_IntVector_Intrinsics_vec128 e2 = e[2U]; |
82 | 0 | Lib_IntVector_Intrinsics_vec128 e3 = e[3U]; |
83 | 0 | Lib_IntVector_Intrinsics_vec128 e4 = e[4U]; |
84 | 0 | Lib_IntVector_Intrinsics_vec128 |
85 | 0 | f0 = Lib_IntVector_Intrinsics_vec128_insert64(acc0, (uint64_t)0U, (uint32_t)1U); |
86 | 0 | Lib_IntVector_Intrinsics_vec128 |
87 | 0 | f1 = Lib_IntVector_Intrinsics_vec128_insert64(acc1, (uint64_t)0U, (uint32_t)1U); |
88 | 0 | Lib_IntVector_Intrinsics_vec128 |
89 | 0 | f2 = Lib_IntVector_Intrinsics_vec128_insert64(acc2, (uint64_t)0U, (uint32_t)1U); |
90 | 0 | Lib_IntVector_Intrinsics_vec128 |
91 | 0 | f3 = Lib_IntVector_Intrinsics_vec128_insert64(acc3, (uint64_t)0U, (uint32_t)1U); |
92 | 0 | Lib_IntVector_Intrinsics_vec128 |
93 | 0 | f4 = Lib_IntVector_Intrinsics_vec128_insert64(acc4, (uint64_t)0U, (uint32_t)1U); |
94 | 0 | Lib_IntVector_Intrinsics_vec128 f01 = Lib_IntVector_Intrinsics_vec128_add64(f0, e0); |
95 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = Lib_IntVector_Intrinsics_vec128_add64(f1, e1); |
96 | 0 | Lib_IntVector_Intrinsics_vec128 f21 = Lib_IntVector_Intrinsics_vec128_add64(f2, e2); |
97 | 0 | Lib_IntVector_Intrinsics_vec128 f31 = Lib_IntVector_Intrinsics_vec128_add64(f3, e3); |
98 | 0 | Lib_IntVector_Intrinsics_vec128 f41 = Lib_IntVector_Intrinsics_vec128_add64(f4, e4); |
99 | 0 | Lib_IntVector_Intrinsics_vec128 acc01 = f01; |
100 | 0 | Lib_IntVector_Intrinsics_vec128 acc11 = f11; |
101 | 0 | Lib_IntVector_Intrinsics_vec128 acc21 = f21; |
102 | 0 | Lib_IntVector_Intrinsics_vec128 acc31 = f31; |
103 | 0 | Lib_IntVector_Intrinsics_vec128 acc41 = f41; |
104 | 0 | acc[0U] = acc01; |
105 | 0 | acc[1U] = acc11; |
106 | 0 | acc[2U] = acc21; |
107 | 0 | acc[3U] = acc31; |
108 | 0 | acc[4U] = acc41; |
109 | 0 | } |
110 | | |
111 | | void |
112 | | Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize( |
113 | | Lib_IntVector_Intrinsics_vec128 *out, |
114 | | Lib_IntVector_Intrinsics_vec128 *p) |
115 | 0 | { |
116 | 0 | Lib_IntVector_Intrinsics_vec128 *r = p; |
117 | 0 | Lib_IntVector_Intrinsics_vec128 *r2 = p + (uint32_t)10U; |
118 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = out[0U]; |
119 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = out[1U]; |
120 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = out[2U]; |
121 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = out[3U]; |
122 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = out[4U]; |
123 | 0 | Lib_IntVector_Intrinsics_vec128 r10 = r[0U]; |
124 | 0 | Lib_IntVector_Intrinsics_vec128 r11 = r[1U]; |
125 | 0 | Lib_IntVector_Intrinsics_vec128 r12 = r[2U]; |
126 | 0 | Lib_IntVector_Intrinsics_vec128 r13 = r[3U]; |
127 | 0 | Lib_IntVector_Intrinsics_vec128 r14 = r[4U]; |
128 | 0 | Lib_IntVector_Intrinsics_vec128 r20 = r2[0U]; |
129 | 0 | Lib_IntVector_Intrinsics_vec128 r21 = r2[1U]; |
130 | 0 | Lib_IntVector_Intrinsics_vec128 r22 = r2[2U]; |
131 | 0 | Lib_IntVector_Intrinsics_vec128 r23 = r2[3U]; |
132 | 0 | Lib_IntVector_Intrinsics_vec128 r24 = r2[4U]; |
133 | 0 | Lib_IntVector_Intrinsics_vec128 |
134 | 0 | r201 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r20, r10); |
135 | 0 | Lib_IntVector_Intrinsics_vec128 |
136 | 0 | r211 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r21, r11); |
137 | 0 | Lib_IntVector_Intrinsics_vec128 |
138 | 0 | r221 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r22, r12); |
139 | 0 | Lib_IntVector_Intrinsics_vec128 |
140 | 0 | r231 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r23, r13); |
141 | 0 | Lib_IntVector_Intrinsics_vec128 |
142 | 0 | r241 = Lib_IntVector_Intrinsics_vec128_interleave_low64(r24, r14); |
143 | 0 | Lib_IntVector_Intrinsics_vec128 |
144 | 0 | r251 = Lib_IntVector_Intrinsics_vec128_smul64(r211, (uint64_t)5U); |
145 | 0 | Lib_IntVector_Intrinsics_vec128 |
146 | 0 | r252 = Lib_IntVector_Intrinsics_vec128_smul64(r221, (uint64_t)5U); |
147 | 0 | Lib_IntVector_Intrinsics_vec128 |
148 | 0 | r253 = Lib_IntVector_Intrinsics_vec128_smul64(r231, (uint64_t)5U); |
149 | 0 | Lib_IntVector_Intrinsics_vec128 |
150 | 0 | r254 = Lib_IntVector_Intrinsics_vec128_smul64(r241, (uint64_t)5U); |
151 | 0 | Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_mul64(r201, a0); |
152 | 0 | Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_mul64(r211, a0); |
153 | 0 | Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_mul64(r221, a0); |
154 | 0 | Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_mul64(r231, a0); |
155 | 0 | Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_mul64(r241, a0); |
156 | 0 | Lib_IntVector_Intrinsics_vec128 |
157 | 0 | a02 = |
158 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a01, |
159 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r254, a1)); |
160 | 0 | Lib_IntVector_Intrinsics_vec128 |
161 | 0 | a12 = |
162 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a11, |
163 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r201, a1)); |
164 | 0 | Lib_IntVector_Intrinsics_vec128 |
165 | 0 | a22 = |
166 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a21, |
167 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r211, a1)); |
168 | 0 | Lib_IntVector_Intrinsics_vec128 |
169 | 0 | a32 = |
170 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a31, |
171 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r221, a1)); |
172 | 0 | Lib_IntVector_Intrinsics_vec128 |
173 | 0 | a42 = |
174 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a41, |
175 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r231, a1)); |
176 | 0 | Lib_IntVector_Intrinsics_vec128 |
177 | 0 | a03 = |
178 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
179 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r253, a2)); |
180 | 0 | Lib_IntVector_Intrinsics_vec128 |
181 | 0 | a13 = |
182 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
183 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r254, a2)); |
184 | 0 | Lib_IntVector_Intrinsics_vec128 |
185 | 0 | a23 = |
186 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
187 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r201, a2)); |
188 | 0 | Lib_IntVector_Intrinsics_vec128 |
189 | 0 | a33 = |
190 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
191 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r211, a2)); |
192 | 0 | Lib_IntVector_Intrinsics_vec128 |
193 | 0 | a43 = |
194 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
195 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r221, a2)); |
196 | 0 | Lib_IntVector_Intrinsics_vec128 |
197 | 0 | a04 = |
198 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
199 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r252, a3)); |
200 | 0 | Lib_IntVector_Intrinsics_vec128 |
201 | 0 | a14 = |
202 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
203 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r253, a3)); |
204 | 0 | Lib_IntVector_Intrinsics_vec128 |
205 | 0 | a24 = |
206 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
207 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r254, a3)); |
208 | 0 | Lib_IntVector_Intrinsics_vec128 |
209 | 0 | a34 = |
210 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
211 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r201, a3)); |
212 | 0 | Lib_IntVector_Intrinsics_vec128 |
213 | 0 | a44 = |
214 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
215 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r211, a3)); |
216 | 0 | Lib_IntVector_Intrinsics_vec128 |
217 | 0 | a05 = |
218 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a04, |
219 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r251, a4)); |
220 | 0 | Lib_IntVector_Intrinsics_vec128 |
221 | 0 | a15 = |
222 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a14, |
223 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r252, a4)); |
224 | 0 | Lib_IntVector_Intrinsics_vec128 |
225 | 0 | a25 = |
226 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a24, |
227 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r253, a4)); |
228 | 0 | Lib_IntVector_Intrinsics_vec128 |
229 | 0 | a35 = |
230 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a34, |
231 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r254, a4)); |
232 | 0 | Lib_IntVector_Intrinsics_vec128 |
233 | 0 | a45 = |
234 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a44, |
235 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r201, a4)); |
236 | 0 | Lib_IntVector_Intrinsics_vec128 t0 = a05; |
237 | 0 | Lib_IntVector_Intrinsics_vec128 t1 = a15; |
238 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a25; |
239 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a35; |
240 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a45; |
241 | 0 | Lib_IntVector_Intrinsics_vec128 |
242 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
243 | 0 | Lib_IntVector_Intrinsics_vec128 |
244 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); |
245 | 0 | Lib_IntVector_Intrinsics_vec128 |
246 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
247 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); |
248 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
249 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); |
250 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
251 | 0 | Lib_IntVector_Intrinsics_vec128 |
252 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
253 | 0 | Lib_IntVector_Intrinsics_vec128 |
254 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
255 | 0 | Lib_IntVector_Intrinsics_vec128 |
256 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
257 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
258 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
259 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
260 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
261 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
262 | 0 | Lib_IntVector_Intrinsics_vec128 |
263 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
264 | 0 | Lib_IntVector_Intrinsics_vec128 |
265 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
266 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
267 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
268 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
269 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
270 | 0 | Lib_IntVector_Intrinsics_vec128 |
271 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
272 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
273 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
274 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = x02; |
275 | 0 | Lib_IntVector_Intrinsics_vec128 o10 = x12; |
276 | 0 | Lib_IntVector_Intrinsics_vec128 o20 = x21; |
277 | 0 | Lib_IntVector_Intrinsics_vec128 o30 = x32; |
278 | 0 | Lib_IntVector_Intrinsics_vec128 o40 = x42; |
279 | 0 | Lib_IntVector_Intrinsics_vec128 |
280 | 0 | o01 = |
281 | 0 | Lib_IntVector_Intrinsics_vec128_add64(o0, |
282 | 0 | Lib_IntVector_Intrinsics_vec128_interleave_high64(o0, o0)); |
283 | 0 | Lib_IntVector_Intrinsics_vec128 |
284 | 0 | o11 = |
285 | 0 | Lib_IntVector_Intrinsics_vec128_add64(o10, |
286 | 0 | Lib_IntVector_Intrinsics_vec128_interleave_high64(o10, o10)); |
287 | 0 | Lib_IntVector_Intrinsics_vec128 |
288 | 0 | o21 = |
289 | 0 | Lib_IntVector_Intrinsics_vec128_add64(o20, |
290 | 0 | Lib_IntVector_Intrinsics_vec128_interleave_high64(o20, o20)); |
291 | 0 | Lib_IntVector_Intrinsics_vec128 |
292 | 0 | o31 = |
293 | 0 | Lib_IntVector_Intrinsics_vec128_add64(o30, |
294 | 0 | Lib_IntVector_Intrinsics_vec128_interleave_high64(o30, o30)); |
295 | 0 | Lib_IntVector_Intrinsics_vec128 |
296 | 0 | o41 = |
297 | 0 | Lib_IntVector_Intrinsics_vec128_add64(o40, |
298 | 0 | Lib_IntVector_Intrinsics_vec128_interleave_high64(o40, o40)); |
299 | 0 | Lib_IntVector_Intrinsics_vec128 |
300 | 0 | l = Lib_IntVector_Intrinsics_vec128_add64(o01, Lib_IntVector_Intrinsics_vec128_zero); |
301 | 0 | Lib_IntVector_Intrinsics_vec128 |
302 | 0 | tmp0 = |
303 | 0 | Lib_IntVector_Intrinsics_vec128_and(l, |
304 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
305 | 0 | Lib_IntVector_Intrinsics_vec128 |
306 | 0 | c0 = Lib_IntVector_Intrinsics_vec128_shift_right64(l, (uint32_t)26U); |
307 | 0 | Lib_IntVector_Intrinsics_vec128 l0 = Lib_IntVector_Intrinsics_vec128_add64(o11, c0); |
308 | 0 | Lib_IntVector_Intrinsics_vec128 |
309 | 0 | tmp1 = |
310 | 0 | Lib_IntVector_Intrinsics_vec128_and(l0, |
311 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
312 | 0 | Lib_IntVector_Intrinsics_vec128 |
313 | 0 | c1 = Lib_IntVector_Intrinsics_vec128_shift_right64(l0, (uint32_t)26U); |
314 | 0 | Lib_IntVector_Intrinsics_vec128 l1 = Lib_IntVector_Intrinsics_vec128_add64(o21, c1); |
315 | 0 | Lib_IntVector_Intrinsics_vec128 |
316 | 0 | tmp2 = |
317 | 0 | Lib_IntVector_Intrinsics_vec128_and(l1, |
318 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
319 | 0 | Lib_IntVector_Intrinsics_vec128 |
320 | 0 | c2 = Lib_IntVector_Intrinsics_vec128_shift_right64(l1, (uint32_t)26U); |
321 | 0 | Lib_IntVector_Intrinsics_vec128 l2 = Lib_IntVector_Intrinsics_vec128_add64(o31, c2); |
322 | 0 | Lib_IntVector_Intrinsics_vec128 |
323 | 0 | tmp3 = |
324 | 0 | Lib_IntVector_Intrinsics_vec128_and(l2, |
325 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
326 | 0 | Lib_IntVector_Intrinsics_vec128 |
327 | 0 | c3 = Lib_IntVector_Intrinsics_vec128_shift_right64(l2, (uint32_t)26U); |
328 | 0 | Lib_IntVector_Intrinsics_vec128 l3 = Lib_IntVector_Intrinsics_vec128_add64(o41, c3); |
329 | 0 | Lib_IntVector_Intrinsics_vec128 |
330 | 0 | tmp4 = |
331 | 0 | Lib_IntVector_Intrinsics_vec128_and(l3, |
332 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
333 | 0 | Lib_IntVector_Intrinsics_vec128 |
334 | 0 | c4 = Lib_IntVector_Intrinsics_vec128_shift_right64(l3, (uint32_t)26U); |
335 | 0 | Lib_IntVector_Intrinsics_vec128 |
336 | 0 | o00 = |
337 | 0 | Lib_IntVector_Intrinsics_vec128_add64(tmp0, |
338 | 0 | Lib_IntVector_Intrinsics_vec128_smul64(c4, (uint64_t)5U)); |
339 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = tmp1; |
340 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = tmp2; |
341 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = tmp3; |
342 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = tmp4; |
343 | 0 | out[0U] = o00; |
344 | 0 | out[1U] = o1; |
345 | 0 | out[2U] = o2; |
346 | 0 | out[3U] = o3; |
347 | 0 | out[4U] = o4; |
348 | 0 | } |
349 | | |
350 | | void |
351 | | Hacl_Poly1305_128_poly1305_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key) |
352 | 0 | { |
353 | 0 | Lib_IntVector_Intrinsics_vec128 *acc = ctx; |
354 | 0 | Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; |
355 | 0 | uint8_t *kr = key; |
356 | 0 | acc[0U] = Lib_IntVector_Intrinsics_vec128_zero; |
357 | 0 | acc[1U] = Lib_IntVector_Intrinsics_vec128_zero; |
358 | 0 | acc[2U] = Lib_IntVector_Intrinsics_vec128_zero; |
359 | 0 | acc[3U] = Lib_IntVector_Intrinsics_vec128_zero; |
360 | 0 | acc[4U] = Lib_IntVector_Intrinsics_vec128_zero; |
361 | 0 | uint64_t u0 = load64_le(kr); |
362 | 0 | uint64_t lo = u0; |
363 | 0 | uint64_t u = load64_le(kr + (uint32_t)8U); |
364 | 0 | uint64_t hi = u; |
365 | 0 | uint64_t mask0 = (uint64_t)0x0ffffffc0fffffffU; |
366 | 0 | uint64_t mask1 = (uint64_t)0x0ffffffc0ffffffcU; |
367 | 0 | uint64_t lo1 = lo & mask0; |
368 | 0 | uint64_t hi1 = hi & mask1; |
369 | 0 | Lib_IntVector_Intrinsics_vec128 *r = pre; |
370 | 0 | Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; |
371 | 0 | Lib_IntVector_Intrinsics_vec128 *rn = pre + (uint32_t)10U; |
372 | 0 | Lib_IntVector_Intrinsics_vec128 *rn_5 = pre + (uint32_t)15U; |
373 | 0 | Lib_IntVector_Intrinsics_vec128 r_vec0 = Lib_IntVector_Intrinsics_vec128_load64(lo1); |
374 | 0 | Lib_IntVector_Intrinsics_vec128 r_vec1 = Lib_IntVector_Intrinsics_vec128_load64(hi1); |
375 | 0 | Lib_IntVector_Intrinsics_vec128 |
376 | 0 | f00 = |
377 | 0 | Lib_IntVector_Intrinsics_vec128_and(r_vec0, |
378 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
379 | 0 | Lib_IntVector_Intrinsics_vec128 |
380 | 0 | f15 = |
381 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec0, |
382 | 0 | (uint32_t)26U), |
383 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
384 | 0 | Lib_IntVector_Intrinsics_vec128 |
385 | 0 | f20 = |
386 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec0, |
387 | 0 | (uint32_t)52U), |
388 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(r_vec1, |
389 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
390 | 0 | (uint32_t)12U)); |
391 | 0 | Lib_IntVector_Intrinsics_vec128 |
392 | 0 | f30 = |
393 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec1, |
394 | 0 | (uint32_t)14U), |
395 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
396 | 0 | Lib_IntVector_Intrinsics_vec128 |
397 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(r_vec1, (uint32_t)40U); |
398 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = f00; |
399 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = f15; |
400 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = f20; |
401 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = f30; |
402 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = f40; |
403 | 0 | r[0U] = f0; |
404 | 0 | r[1U] = f1; |
405 | 0 | r[2U] = f2; |
406 | 0 | r[3U] = f3; |
407 | 0 | r[4U] = f4; |
408 | 0 | Lib_IntVector_Intrinsics_vec128 f200 = r[0U]; |
409 | 0 | Lib_IntVector_Intrinsics_vec128 f210 = r[1U]; |
410 | 0 | Lib_IntVector_Intrinsics_vec128 f220 = r[2U]; |
411 | 0 | Lib_IntVector_Intrinsics_vec128 f230 = r[3U]; |
412 | 0 | Lib_IntVector_Intrinsics_vec128 f240 = r[4U]; |
413 | 0 | r5[0U] = Lib_IntVector_Intrinsics_vec128_smul64(f200, (uint64_t)5U); |
414 | 0 | r5[1U] = Lib_IntVector_Intrinsics_vec128_smul64(f210, (uint64_t)5U); |
415 | 0 | r5[2U] = Lib_IntVector_Intrinsics_vec128_smul64(f220, (uint64_t)5U); |
416 | 0 | r5[3U] = Lib_IntVector_Intrinsics_vec128_smul64(f230, (uint64_t)5U); |
417 | 0 | r5[4U] = Lib_IntVector_Intrinsics_vec128_smul64(f240, (uint64_t)5U); |
418 | 0 | Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; |
419 | 0 | Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; |
420 | 0 | Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; |
421 | 0 | Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; |
422 | 0 | Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; |
423 | 0 | Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; |
424 | 0 | Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; |
425 | 0 | Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; |
426 | 0 | Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; |
427 | 0 | Lib_IntVector_Intrinsics_vec128 f10 = r[0U]; |
428 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = r[1U]; |
429 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = r[2U]; |
430 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = r[3U]; |
431 | 0 | Lib_IntVector_Intrinsics_vec128 f14 = r[4U]; |
432 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = Lib_IntVector_Intrinsics_vec128_mul64(r0, f10); |
433 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = Lib_IntVector_Intrinsics_vec128_mul64(r1, f10); |
434 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = Lib_IntVector_Intrinsics_vec128_mul64(r2, f10); |
435 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = Lib_IntVector_Intrinsics_vec128_mul64(r3, f10); |
436 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = Lib_IntVector_Intrinsics_vec128_mul64(r4, f10); |
437 | 0 | Lib_IntVector_Intrinsics_vec128 |
438 | 0 | a01 = |
439 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a0, |
440 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f11)); |
441 | 0 | Lib_IntVector_Intrinsics_vec128 |
442 | 0 | a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, Lib_IntVector_Intrinsics_vec128_mul64(r0, f11)); |
443 | 0 | Lib_IntVector_Intrinsics_vec128 |
444 | 0 | a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, Lib_IntVector_Intrinsics_vec128_mul64(r1, f11)); |
445 | 0 | Lib_IntVector_Intrinsics_vec128 |
446 | 0 | a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, Lib_IntVector_Intrinsics_vec128_mul64(r2, f11)); |
447 | 0 | Lib_IntVector_Intrinsics_vec128 |
448 | 0 | a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, Lib_IntVector_Intrinsics_vec128_mul64(r3, f11)); |
449 | 0 | Lib_IntVector_Intrinsics_vec128 |
450 | 0 | a02 = |
451 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a01, |
452 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f12)); |
453 | 0 | Lib_IntVector_Intrinsics_vec128 |
454 | 0 | a12 = |
455 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a11, |
456 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f12)); |
457 | 0 | Lib_IntVector_Intrinsics_vec128 |
458 | 0 | a22 = |
459 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a21, |
460 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f12)); |
461 | 0 | Lib_IntVector_Intrinsics_vec128 |
462 | 0 | a32 = |
463 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a31, |
464 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, f12)); |
465 | 0 | Lib_IntVector_Intrinsics_vec128 |
466 | 0 | a42 = |
467 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a41, |
468 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, f12)); |
469 | 0 | Lib_IntVector_Intrinsics_vec128 |
470 | 0 | a03 = |
471 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
472 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, f13)); |
473 | 0 | Lib_IntVector_Intrinsics_vec128 |
474 | 0 | a13 = |
475 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
476 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f13)); |
477 | 0 | Lib_IntVector_Intrinsics_vec128 |
478 | 0 | a23 = |
479 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
480 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f13)); |
481 | 0 | Lib_IntVector_Intrinsics_vec128 |
482 | 0 | a33 = |
483 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
484 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f13)); |
485 | 0 | Lib_IntVector_Intrinsics_vec128 |
486 | 0 | a43 = |
487 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
488 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, f13)); |
489 | 0 | Lib_IntVector_Intrinsics_vec128 |
490 | 0 | a04 = |
491 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
492 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r51, f14)); |
493 | 0 | Lib_IntVector_Intrinsics_vec128 |
494 | 0 | a14 = |
495 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
496 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, f14)); |
497 | 0 | Lib_IntVector_Intrinsics_vec128 |
498 | 0 | a24 = |
499 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
500 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f14)); |
501 | 0 | Lib_IntVector_Intrinsics_vec128 |
502 | 0 | a34 = |
503 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
504 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f14)); |
505 | 0 | Lib_IntVector_Intrinsics_vec128 |
506 | 0 | a44 = |
507 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
508 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f14)); |
509 | 0 | Lib_IntVector_Intrinsics_vec128 t0 = a04; |
510 | 0 | Lib_IntVector_Intrinsics_vec128 t1 = a14; |
511 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a24; |
512 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a34; |
513 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a44; |
514 | 0 | Lib_IntVector_Intrinsics_vec128 |
515 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
516 | 0 | Lib_IntVector_Intrinsics_vec128 |
517 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); |
518 | 0 | Lib_IntVector_Intrinsics_vec128 |
519 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
520 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); |
521 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
522 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); |
523 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
524 | 0 | Lib_IntVector_Intrinsics_vec128 |
525 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
526 | 0 | Lib_IntVector_Intrinsics_vec128 |
527 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
528 | 0 | Lib_IntVector_Intrinsics_vec128 |
529 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
530 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
531 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
532 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
533 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
534 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
535 | 0 | Lib_IntVector_Intrinsics_vec128 |
536 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
537 | 0 | Lib_IntVector_Intrinsics_vec128 |
538 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
539 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
540 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
541 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
542 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
543 | 0 | Lib_IntVector_Intrinsics_vec128 |
544 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
545 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
546 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
547 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = x02; |
548 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = x12; |
549 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = x21; |
550 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = x32; |
551 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = x42; |
552 | 0 | rn[0U] = o0; |
553 | 0 | rn[1U] = o1; |
554 | 0 | rn[2U] = o2; |
555 | 0 | rn[3U] = o3; |
556 | 0 | rn[4U] = o4; |
557 | 0 | Lib_IntVector_Intrinsics_vec128 f201 = rn[0U]; |
558 | 0 | Lib_IntVector_Intrinsics_vec128 f21 = rn[1U]; |
559 | 0 | Lib_IntVector_Intrinsics_vec128 f22 = rn[2U]; |
560 | 0 | Lib_IntVector_Intrinsics_vec128 f23 = rn[3U]; |
561 | 0 | Lib_IntVector_Intrinsics_vec128 f24 = rn[4U]; |
562 | 0 | rn_5[0U] = Lib_IntVector_Intrinsics_vec128_smul64(f201, (uint64_t)5U); |
563 | 0 | rn_5[1U] = Lib_IntVector_Intrinsics_vec128_smul64(f21, (uint64_t)5U); |
564 | 0 | rn_5[2U] = Lib_IntVector_Intrinsics_vec128_smul64(f22, (uint64_t)5U); |
565 | 0 | rn_5[3U] = Lib_IntVector_Intrinsics_vec128_smul64(f23, (uint64_t)5U); |
566 | 0 | rn_5[4U] = Lib_IntVector_Intrinsics_vec128_smul64(f24, (uint64_t)5U); |
567 | 0 | } |
568 | | |
569 | | void |
570 | | Hacl_Poly1305_128_poly1305_update1(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *text) |
571 | 0 | { |
572 | 0 | Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; |
573 | 0 | Lib_IntVector_Intrinsics_vec128 *acc = ctx; |
574 | 0 | KRML_PRE_ALIGN(16) |
575 | 0 | Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; |
576 | 0 | uint64_t u0 = load64_le(text); |
577 | 0 | uint64_t lo = u0; |
578 | 0 | uint64_t u = load64_le(text + (uint32_t)8U); |
579 | 0 | uint64_t hi = u; |
580 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); |
581 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); |
582 | 0 | Lib_IntVector_Intrinsics_vec128 |
583 | 0 | f010 = |
584 | 0 | Lib_IntVector_Intrinsics_vec128_and(f0, |
585 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
586 | 0 | Lib_IntVector_Intrinsics_vec128 |
587 | 0 | f110 = |
588 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
589 | 0 | (uint32_t)26U), |
590 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
591 | 0 | Lib_IntVector_Intrinsics_vec128 |
592 | 0 | f20 = |
593 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
594 | 0 | (uint32_t)52U), |
595 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, |
596 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
597 | 0 | (uint32_t)12U)); |
598 | 0 | Lib_IntVector_Intrinsics_vec128 |
599 | 0 | f30 = |
600 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, |
601 | 0 | (uint32_t)14U), |
602 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
603 | 0 | Lib_IntVector_Intrinsics_vec128 |
604 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); |
605 | 0 | Lib_IntVector_Intrinsics_vec128 f01 = f010; |
606 | 0 | Lib_IntVector_Intrinsics_vec128 f111 = f110; |
607 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = f20; |
608 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = f30; |
609 | 0 | Lib_IntVector_Intrinsics_vec128 f41 = f40; |
610 | 0 | e[0U] = f01; |
611 | 0 | e[1U] = f111; |
612 | 0 | e[2U] = f2; |
613 | 0 | e[3U] = f3; |
614 | 0 | e[4U] = f41; |
615 | 0 | uint64_t b = (uint64_t)0x1000000U; |
616 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); |
617 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; |
618 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); |
619 | 0 | Lib_IntVector_Intrinsics_vec128 *r = pre; |
620 | 0 | Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; |
621 | 0 | Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; |
622 | 0 | Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; |
623 | 0 | Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; |
624 | 0 | Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; |
625 | 0 | Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; |
626 | 0 | Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; |
627 | 0 | Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; |
628 | 0 | Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; |
629 | 0 | Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; |
630 | 0 | Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; |
631 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; |
632 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; |
633 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; |
634 | 0 | Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; |
635 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; |
636 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; |
637 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; |
638 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; |
639 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; |
640 | 0 | Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); |
641 | 0 | Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); |
642 | 0 | Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); |
643 | 0 | Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); |
644 | 0 | Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); |
645 | 0 | Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); |
646 | 0 | Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); |
647 | 0 | Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); |
648 | 0 | Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); |
649 | 0 | Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); |
650 | 0 | Lib_IntVector_Intrinsics_vec128 |
651 | 0 | a03 = |
652 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
653 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); |
654 | 0 | Lib_IntVector_Intrinsics_vec128 |
655 | 0 | a13 = |
656 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
657 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); |
658 | 0 | Lib_IntVector_Intrinsics_vec128 |
659 | 0 | a23 = |
660 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
661 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); |
662 | 0 | Lib_IntVector_Intrinsics_vec128 |
663 | 0 | a33 = |
664 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
665 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); |
666 | 0 | Lib_IntVector_Intrinsics_vec128 |
667 | 0 | a43 = |
668 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
669 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); |
670 | 0 | Lib_IntVector_Intrinsics_vec128 |
671 | 0 | a04 = |
672 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
673 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); |
674 | 0 | Lib_IntVector_Intrinsics_vec128 |
675 | 0 | a14 = |
676 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
677 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); |
678 | 0 | Lib_IntVector_Intrinsics_vec128 |
679 | 0 | a24 = |
680 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
681 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); |
682 | 0 | Lib_IntVector_Intrinsics_vec128 |
683 | 0 | a34 = |
684 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
685 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); |
686 | 0 | Lib_IntVector_Intrinsics_vec128 |
687 | 0 | a44 = |
688 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
689 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); |
690 | 0 | Lib_IntVector_Intrinsics_vec128 |
691 | 0 | a05 = |
692 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a04, |
693 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); |
694 | 0 | Lib_IntVector_Intrinsics_vec128 |
695 | 0 | a15 = |
696 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a14, |
697 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); |
698 | 0 | Lib_IntVector_Intrinsics_vec128 |
699 | 0 | a25 = |
700 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a24, |
701 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); |
702 | 0 | Lib_IntVector_Intrinsics_vec128 |
703 | 0 | a35 = |
704 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a34, |
705 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); |
706 | 0 | Lib_IntVector_Intrinsics_vec128 |
707 | 0 | a45 = |
708 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a44, |
709 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); |
710 | 0 | Lib_IntVector_Intrinsics_vec128 |
711 | 0 | a06 = |
712 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a05, |
713 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); |
714 | 0 | Lib_IntVector_Intrinsics_vec128 |
715 | 0 | a16 = |
716 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a15, |
717 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); |
718 | 0 | Lib_IntVector_Intrinsics_vec128 |
719 | 0 | a26 = |
720 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a25, |
721 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); |
722 | 0 | Lib_IntVector_Intrinsics_vec128 |
723 | 0 | a36 = |
724 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a35, |
725 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); |
726 | 0 | Lib_IntVector_Intrinsics_vec128 |
727 | 0 | a46 = |
728 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a45, |
729 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); |
730 | 0 | Lib_IntVector_Intrinsics_vec128 t0 = a06; |
731 | 0 | Lib_IntVector_Intrinsics_vec128 t1 = a16; |
732 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a26; |
733 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a36; |
734 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a46; |
735 | 0 | Lib_IntVector_Intrinsics_vec128 |
736 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
737 | 0 | Lib_IntVector_Intrinsics_vec128 |
738 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t0, (uint32_t)26U); |
739 | 0 | Lib_IntVector_Intrinsics_vec128 |
740 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
741 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t0, mask26); |
742 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
743 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); |
744 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
745 | 0 | Lib_IntVector_Intrinsics_vec128 |
746 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
747 | 0 | Lib_IntVector_Intrinsics_vec128 |
748 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
749 | 0 | Lib_IntVector_Intrinsics_vec128 |
750 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
751 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
752 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
753 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
754 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
755 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
756 | 0 | Lib_IntVector_Intrinsics_vec128 |
757 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
758 | 0 | Lib_IntVector_Intrinsics_vec128 |
759 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
760 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
761 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
762 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
763 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
764 | 0 | Lib_IntVector_Intrinsics_vec128 |
765 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
766 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
767 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
768 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = x02; |
769 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = x12; |
770 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = x21; |
771 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = x32; |
772 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = x42; |
773 | 0 | acc[0U] = o0; |
774 | 0 | acc[1U] = o1; |
775 | 0 | acc[2U] = o2; |
776 | 0 | acc[3U] = o3; |
777 | 0 | acc[4U] = o4; |
778 | 0 | } |
779 | | |
780 | | void |
781 | | Hacl_Poly1305_128_poly1305_update( |
782 | | Lib_IntVector_Intrinsics_vec128 *ctx, |
783 | | uint32_t len, |
784 | | uint8_t *text) |
785 | 0 | { |
786 | 0 | Lib_IntVector_Intrinsics_vec128 *pre = ctx + (uint32_t)5U; |
787 | 0 | Lib_IntVector_Intrinsics_vec128 *acc = ctx; |
788 | 0 | uint32_t sz_block = (uint32_t)32U; |
789 | 0 | uint32_t len0 = len / sz_block * sz_block; |
790 | 0 | uint8_t *t0 = text; |
791 | 0 | if (len0 > (uint32_t)0U) { |
792 | 0 | uint32_t bs = (uint32_t)32U; |
793 | 0 | uint8_t *text0 = t0; |
794 | 0 | Hacl_Impl_Poly1305_Field32xN_128_load_acc2(acc, text0); |
795 | 0 | uint32_t len1 = len0 - bs; |
796 | 0 | uint8_t *text1 = t0 + bs; |
797 | 0 | uint32_t nb = len1 / bs; |
798 | 0 | for (uint32_t i = (uint32_t)0U; i < nb; i++) { |
799 | 0 | uint8_t *block = text1 + i * bs; |
800 | 0 | KRML_PRE_ALIGN(16) |
801 | 0 | Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; |
802 | 0 | Lib_IntVector_Intrinsics_vec128 b1 = Lib_IntVector_Intrinsics_vec128_load64_le(block); |
803 | 0 | Lib_IntVector_Intrinsics_vec128 |
804 | 0 | b2 = Lib_IntVector_Intrinsics_vec128_load64_le(block + (uint32_t)16U); |
805 | 0 | Lib_IntVector_Intrinsics_vec128 lo = Lib_IntVector_Intrinsics_vec128_interleave_low64(b1, b2); |
806 | 0 | Lib_IntVector_Intrinsics_vec128 |
807 | 0 | hi = Lib_IntVector_Intrinsics_vec128_interleave_high64(b1, b2); |
808 | 0 | Lib_IntVector_Intrinsics_vec128 |
809 | 0 | f00 = |
810 | 0 | Lib_IntVector_Intrinsics_vec128_and(lo, |
811 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
812 | 0 | Lib_IntVector_Intrinsics_vec128 |
813 | 0 | f15 = |
814 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, |
815 | 0 | (uint32_t)26U), |
816 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
817 | 0 | Lib_IntVector_Intrinsics_vec128 |
818 | 0 | f25 = |
819 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(lo, |
820 | 0 | (uint32_t)52U), |
821 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(hi, |
822 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
823 | 0 | (uint32_t)12U)); |
824 | 0 | Lib_IntVector_Intrinsics_vec128 |
825 | 0 | f30 = |
826 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(hi, |
827 | 0 | (uint32_t)14U), |
828 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
829 | 0 | Lib_IntVector_Intrinsics_vec128 |
830 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(hi, (uint32_t)40U); |
831 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = f00; |
832 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = f15; |
833 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = f25; |
834 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = f30; |
835 | 0 | Lib_IntVector_Intrinsics_vec128 f41 = f40; |
836 | 0 | e[0U] = f0; |
837 | 0 | e[1U] = f1; |
838 | 0 | e[2U] = f2; |
839 | 0 | e[3U] = f3; |
840 | 0 | e[4U] = f41; |
841 | 0 | uint64_t b = (uint64_t)0x1000000U; |
842 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); |
843 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; |
844 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); |
845 | 0 | Lib_IntVector_Intrinsics_vec128 *rn = pre + (uint32_t)10U; |
846 | 0 | Lib_IntVector_Intrinsics_vec128 *rn5 = pre + (uint32_t)15U; |
847 | 0 | Lib_IntVector_Intrinsics_vec128 r0 = rn[0U]; |
848 | 0 | Lib_IntVector_Intrinsics_vec128 r1 = rn[1U]; |
849 | 0 | Lib_IntVector_Intrinsics_vec128 r2 = rn[2U]; |
850 | 0 | Lib_IntVector_Intrinsics_vec128 r3 = rn[3U]; |
851 | 0 | Lib_IntVector_Intrinsics_vec128 r4 = rn[4U]; |
852 | 0 | Lib_IntVector_Intrinsics_vec128 r51 = rn5[1U]; |
853 | 0 | Lib_IntVector_Intrinsics_vec128 r52 = rn5[2U]; |
854 | 0 | Lib_IntVector_Intrinsics_vec128 r53 = rn5[3U]; |
855 | 0 | Lib_IntVector_Intrinsics_vec128 r54 = rn5[4U]; |
856 | 0 | Lib_IntVector_Intrinsics_vec128 f10 = acc[0U]; |
857 | 0 | Lib_IntVector_Intrinsics_vec128 f110 = acc[1U]; |
858 | 0 | Lib_IntVector_Intrinsics_vec128 f120 = acc[2U]; |
859 | 0 | Lib_IntVector_Intrinsics_vec128 f130 = acc[3U]; |
860 | 0 | Lib_IntVector_Intrinsics_vec128 f140 = acc[4U]; |
861 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = Lib_IntVector_Intrinsics_vec128_mul64(r0, f10); |
862 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = Lib_IntVector_Intrinsics_vec128_mul64(r1, f10); |
863 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = Lib_IntVector_Intrinsics_vec128_mul64(r2, f10); |
864 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = Lib_IntVector_Intrinsics_vec128_mul64(r3, f10); |
865 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = Lib_IntVector_Intrinsics_vec128_mul64(r4, f10); |
866 | 0 | Lib_IntVector_Intrinsics_vec128 |
867 | 0 | a01 = |
868 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a0, |
869 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f110)); |
870 | 0 | Lib_IntVector_Intrinsics_vec128 |
871 | 0 | a11 = |
872 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a1, |
873 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f110)); |
874 | 0 | Lib_IntVector_Intrinsics_vec128 |
875 | 0 | a21 = |
876 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a2, |
877 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, f110)); |
878 | 0 | Lib_IntVector_Intrinsics_vec128 |
879 | 0 | a31 = |
880 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a3, |
881 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, f110)); |
882 | 0 | Lib_IntVector_Intrinsics_vec128 |
883 | 0 | a41 = |
884 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a4, |
885 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r3, f110)); |
886 | 0 | Lib_IntVector_Intrinsics_vec128 |
887 | 0 | a02 = |
888 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a01, |
889 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f120)); |
890 | 0 | Lib_IntVector_Intrinsics_vec128 |
891 | 0 | a12 = |
892 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a11, |
893 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f120)); |
894 | 0 | Lib_IntVector_Intrinsics_vec128 |
895 | 0 | a22 = |
896 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a21, |
897 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f120)); |
898 | 0 | Lib_IntVector_Intrinsics_vec128 |
899 | 0 | a32 = |
900 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a31, |
901 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, f120)); |
902 | 0 | Lib_IntVector_Intrinsics_vec128 |
903 | 0 | a42 = |
904 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a41, |
905 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, f120)); |
906 | 0 | Lib_IntVector_Intrinsics_vec128 |
907 | 0 | a03 = |
908 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
909 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, f130)); |
910 | 0 | Lib_IntVector_Intrinsics_vec128 |
911 | 0 | a13 = |
912 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
913 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f130)); |
914 | 0 | Lib_IntVector_Intrinsics_vec128 |
915 | 0 | a23 = |
916 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
917 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f130)); |
918 | 0 | Lib_IntVector_Intrinsics_vec128 |
919 | 0 | a33 = |
920 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
921 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f130)); |
922 | 0 | Lib_IntVector_Intrinsics_vec128 |
923 | 0 | a43 = |
924 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
925 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, f130)); |
926 | 0 | Lib_IntVector_Intrinsics_vec128 |
927 | 0 | a04 = |
928 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
929 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r51, f140)); |
930 | 0 | Lib_IntVector_Intrinsics_vec128 |
931 | 0 | a14 = |
932 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
933 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, f140)); |
934 | 0 | Lib_IntVector_Intrinsics_vec128 |
935 | 0 | a24 = |
936 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
937 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, f140)); |
938 | 0 | Lib_IntVector_Intrinsics_vec128 |
939 | 0 | a34 = |
940 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
941 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, f140)); |
942 | 0 | Lib_IntVector_Intrinsics_vec128 |
943 | 0 | a44 = |
944 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
945 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, f140)); |
946 | 0 | Lib_IntVector_Intrinsics_vec128 t01 = a04; |
947 | 0 | Lib_IntVector_Intrinsics_vec128 t1 = a14; |
948 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a24; |
949 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a34; |
950 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a44; |
951 | 0 | Lib_IntVector_Intrinsics_vec128 |
952 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
953 | 0 | Lib_IntVector_Intrinsics_vec128 |
954 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); |
955 | 0 | Lib_IntVector_Intrinsics_vec128 |
956 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
957 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); |
958 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
959 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t1, z0); |
960 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
961 | 0 | Lib_IntVector_Intrinsics_vec128 |
962 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
963 | 0 | Lib_IntVector_Intrinsics_vec128 |
964 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
965 | 0 | Lib_IntVector_Intrinsics_vec128 |
966 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
967 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
968 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
969 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
970 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
971 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
972 | 0 | Lib_IntVector_Intrinsics_vec128 |
973 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
974 | 0 | Lib_IntVector_Intrinsics_vec128 |
975 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
976 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
977 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
978 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
979 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
980 | 0 | Lib_IntVector_Intrinsics_vec128 |
981 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
982 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
983 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
984 | 0 | Lib_IntVector_Intrinsics_vec128 o00 = x02; |
985 | 0 | Lib_IntVector_Intrinsics_vec128 o10 = x12; |
986 | 0 | Lib_IntVector_Intrinsics_vec128 o20 = x21; |
987 | 0 | Lib_IntVector_Intrinsics_vec128 o30 = x32; |
988 | 0 | Lib_IntVector_Intrinsics_vec128 o40 = x42; |
989 | 0 | acc[0U] = o00; |
990 | 0 | acc[1U] = o10; |
991 | 0 | acc[2U] = o20; |
992 | 0 | acc[3U] = o30; |
993 | 0 | acc[4U] = o40; |
994 | 0 | Lib_IntVector_Intrinsics_vec128 f100 = acc[0U]; |
995 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = acc[1U]; |
996 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = acc[2U]; |
997 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = acc[3U]; |
998 | 0 | Lib_IntVector_Intrinsics_vec128 f14 = acc[4U]; |
999 | 0 | Lib_IntVector_Intrinsics_vec128 f20 = e[0U]; |
1000 | 0 | Lib_IntVector_Intrinsics_vec128 f21 = e[1U]; |
1001 | 0 | Lib_IntVector_Intrinsics_vec128 f22 = e[2U]; |
1002 | 0 | Lib_IntVector_Intrinsics_vec128 f23 = e[3U]; |
1003 | 0 | Lib_IntVector_Intrinsics_vec128 f24 = e[4U]; |
1004 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = Lib_IntVector_Intrinsics_vec128_add64(f100, f20); |
1005 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = Lib_IntVector_Intrinsics_vec128_add64(f11, f21); |
1006 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = Lib_IntVector_Intrinsics_vec128_add64(f12, f22); |
1007 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = Lib_IntVector_Intrinsics_vec128_add64(f13, f23); |
1008 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = Lib_IntVector_Intrinsics_vec128_add64(f14, f24); |
1009 | 0 | acc[0U] = o0; |
1010 | 0 | acc[1U] = o1; |
1011 | 0 | acc[2U] = o2; |
1012 | 0 | acc[3U] = o3; |
1013 | 0 | acc[4U] = o4; |
1014 | 0 | } |
1015 | 0 | Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize(acc, pre); |
1016 | 0 | } |
1017 | 0 | uint32_t len1 = len - len0; |
1018 | 0 | uint8_t *t1 = text + len0; |
1019 | 0 | uint32_t nb = len1 / (uint32_t)16U; |
1020 | 0 | uint32_t rem = len1 % (uint32_t)16U; |
1021 | 0 | for (uint32_t i = (uint32_t)0U; i < nb; i++) { |
1022 | 0 | uint8_t *block = t1 + i * (uint32_t)16U; |
1023 | 0 | KRML_PRE_ALIGN(16) |
1024 | 0 | Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; |
1025 | 0 | uint64_t u0 = load64_le(block); |
1026 | 0 | uint64_t lo = u0; |
1027 | 0 | uint64_t u = load64_le(block + (uint32_t)8U); |
1028 | 0 | uint64_t hi = u; |
1029 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); |
1030 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); |
1031 | 0 | Lib_IntVector_Intrinsics_vec128 |
1032 | 0 | f010 = |
1033 | 0 | Lib_IntVector_Intrinsics_vec128_and(f0, |
1034 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1035 | 0 | Lib_IntVector_Intrinsics_vec128 |
1036 | 0 | f110 = |
1037 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
1038 | 0 | (uint32_t)26U), |
1039 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1040 | 0 | Lib_IntVector_Intrinsics_vec128 |
1041 | 0 | f20 = |
1042 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
1043 | 0 | (uint32_t)52U), |
1044 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, |
1045 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
1046 | 0 | (uint32_t)12U)); |
1047 | 0 | Lib_IntVector_Intrinsics_vec128 |
1048 | 0 | f30 = |
1049 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, |
1050 | 0 | (uint32_t)14U), |
1051 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1052 | 0 | Lib_IntVector_Intrinsics_vec128 |
1053 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); |
1054 | 0 | Lib_IntVector_Intrinsics_vec128 f01 = f010; |
1055 | 0 | Lib_IntVector_Intrinsics_vec128 f111 = f110; |
1056 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = f20; |
1057 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = f30; |
1058 | 0 | Lib_IntVector_Intrinsics_vec128 f41 = f40; |
1059 | 0 | e[0U] = f01; |
1060 | 0 | e[1U] = f111; |
1061 | 0 | e[2U] = f2; |
1062 | 0 | e[3U] = f3; |
1063 | 0 | e[4U] = f41; |
1064 | 0 | uint64_t b = (uint64_t)0x1000000U; |
1065 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); |
1066 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = e[4U]; |
1067 | 0 | e[4U] = Lib_IntVector_Intrinsics_vec128_or(f4, mask); |
1068 | 0 | Lib_IntVector_Intrinsics_vec128 *r = pre; |
1069 | 0 | Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; |
1070 | 0 | Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; |
1071 | 0 | Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; |
1072 | 0 | Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; |
1073 | 0 | Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; |
1074 | 0 | Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; |
1075 | 0 | Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; |
1076 | 0 | Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; |
1077 | 0 | Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; |
1078 | 0 | Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; |
1079 | 0 | Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; |
1080 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; |
1081 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; |
1082 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; |
1083 | 0 | Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; |
1084 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; |
1085 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; |
1086 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; |
1087 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; |
1088 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; |
1089 | 0 | Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); |
1090 | 0 | Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); |
1091 | 0 | Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); |
1092 | 0 | Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); |
1093 | 0 | Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); |
1094 | 0 | Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); |
1095 | 0 | Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); |
1096 | 0 | Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); |
1097 | 0 | Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); |
1098 | 0 | Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); |
1099 | 0 | Lib_IntVector_Intrinsics_vec128 |
1100 | 0 | a03 = |
1101 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
1102 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); |
1103 | 0 | Lib_IntVector_Intrinsics_vec128 |
1104 | 0 | a13 = |
1105 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
1106 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); |
1107 | 0 | Lib_IntVector_Intrinsics_vec128 |
1108 | 0 | a23 = |
1109 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
1110 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); |
1111 | 0 | Lib_IntVector_Intrinsics_vec128 |
1112 | 0 | a33 = |
1113 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
1114 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); |
1115 | 0 | Lib_IntVector_Intrinsics_vec128 |
1116 | 0 | a43 = |
1117 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
1118 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); |
1119 | 0 | Lib_IntVector_Intrinsics_vec128 |
1120 | 0 | a04 = |
1121 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
1122 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); |
1123 | 0 | Lib_IntVector_Intrinsics_vec128 |
1124 | 0 | a14 = |
1125 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
1126 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); |
1127 | 0 | Lib_IntVector_Intrinsics_vec128 |
1128 | 0 | a24 = |
1129 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
1130 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); |
1131 | 0 | Lib_IntVector_Intrinsics_vec128 |
1132 | 0 | a34 = |
1133 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
1134 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); |
1135 | 0 | Lib_IntVector_Intrinsics_vec128 |
1136 | 0 | a44 = |
1137 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
1138 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); |
1139 | 0 | Lib_IntVector_Intrinsics_vec128 |
1140 | 0 | a05 = |
1141 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a04, |
1142 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); |
1143 | 0 | Lib_IntVector_Intrinsics_vec128 |
1144 | 0 | a15 = |
1145 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a14, |
1146 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); |
1147 | 0 | Lib_IntVector_Intrinsics_vec128 |
1148 | 0 | a25 = |
1149 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a24, |
1150 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); |
1151 | 0 | Lib_IntVector_Intrinsics_vec128 |
1152 | 0 | a35 = |
1153 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a34, |
1154 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); |
1155 | 0 | Lib_IntVector_Intrinsics_vec128 |
1156 | 0 | a45 = |
1157 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a44, |
1158 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); |
1159 | 0 | Lib_IntVector_Intrinsics_vec128 |
1160 | 0 | a06 = |
1161 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a05, |
1162 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); |
1163 | 0 | Lib_IntVector_Intrinsics_vec128 |
1164 | 0 | a16 = |
1165 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a15, |
1166 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); |
1167 | 0 | Lib_IntVector_Intrinsics_vec128 |
1168 | 0 | a26 = |
1169 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a25, |
1170 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); |
1171 | 0 | Lib_IntVector_Intrinsics_vec128 |
1172 | 0 | a36 = |
1173 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a35, |
1174 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); |
1175 | 0 | Lib_IntVector_Intrinsics_vec128 |
1176 | 0 | a46 = |
1177 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a45, |
1178 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); |
1179 | 0 | Lib_IntVector_Intrinsics_vec128 t01 = a06; |
1180 | 0 | Lib_IntVector_Intrinsics_vec128 t11 = a16; |
1181 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a26; |
1182 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a36; |
1183 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a46; |
1184 | 0 | Lib_IntVector_Intrinsics_vec128 |
1185 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
1186 | 0 | Lib_IntVector_Intrinsics_vec128 |
1187 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); |
1188 | 0 | Lib_IntVector_Intrinsics_vec128 |
1189 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
1190 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); |
1191 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
1192 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); |
1193 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
1194 | 0 | Lib_IntVector_Intrinsics_vec128 |
1195 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
1196 | 0 | Lib_IntVector_Intrinsics_vec128 |
1197 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
1198 | 0 | Lib_IntVector_Intrinsics_vec128 |
1199 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
1200 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
1201 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
1202 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
1203 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
1204 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
1205 | 0 | Lib_IntVector_Intrinsics_vec128 |
1206 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
1207 | 0 | Lib_IntVector_Intrinsics_vec128 |
1208 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
1209 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
1210 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
1211 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
1212 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
1213 | 0 | Lib_IntVector_Intrinsics_vec128 |
1214 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
1215 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
1216 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
1217 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = x02; |
1218 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = x12; |
1219 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = x21; |
1220 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = x32; |
1221 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = x42; |
1222 | 0 | acc[0U] = o0; |
1223 | 0 | acc[1U] = o1; |
1224 | 0 | acc[2U] = o2; |
1225 | 0 | acc[3U] = o3; |
1226 | 0 | acc[4U] = o4; |
1227 | 0 | } |
1228 | 0 | if (rem > (uint32_t)0U) { |
1229 | 0 | uint8_t *last = t1 + nb * (uint32_t)16U; |
1230 | 0 | KRML_PRE_ALIGN(16) |
1231 | 0 | Lib_IntVector_Intrinsics_vec128 e[5U] KRML_POST_ALIGN(16) = { 0U }; |
1232 | 0 | uint8_t tmp[16U] = { 0U }; |
1233 | 0 | memcpy(tmp, last, rem * sizeof(uint8_t)); |
1234 | 0 | uint64_t u0 = load64_le(tmp); |
1235 | 0 | uint64_t lo = u0; |
1236 | 0 | uint64_t u = load64_le(tmp + (uint32_t)8U); |
1237 | 0 | uint64_t hi = u; |
1238 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = Lib_IntVector_Intrinsics_vec128_load64(lo); |
1239 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = Lib_IntVector_Intrinsics_vec128_load64(hi); |
1240 | 0 | Lib_IntVector_Intrinsics_vec128 |
1241 | 0 | f010 = |
1242 | 0 | Lib_IntVector_Intrinsics_vec128_and(f0, |
1243 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1244 | 0 | Lib_IntVector_Intrinsics_vec128 |
1245 | 0 | f110 = |
1246 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
1247 | 0 | (uint32_t)26U), |
1248 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1249 | 0 | Lib_IntVector_Intrinsics_vec128 |
1250 | 0 | f20 = |
1251 | 0 | Lib_IntVector_Intrinsics_vec128_or(Lib_IntVector_Intrinsics_vec128_shift_right64(f0, |
1252 | 0 | (uint32_t)52U), |
1253 | 0 | Lib_IntVector_Intrinsics_vec128_shift_left64(Lib_IntVector_Intrinsics_vec128_and(f1, |
1254 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffU)), |
1255 | 0 | (uint32_t)12U)); |
1256 | 0 | Lib_IntVector_Intrinsics_vec128 |
1257 | 0 | f30 = |
1258 | 0 | Lib_IntVector_Intrinsics_vec128_and(Lib_IntVector_Intrinsics_vec128_shift_right64(f1, |
1259 | 0 | (uint32_t)14U), |
1260 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1261 | 0 | Lib_IntVector_Intrinsics_vec128 |
1262 | 0 | f40 = Lib_IntVector_Intrinsics_vec128_shift_right64(f1, (uint32_t)40U); |
1263 | 0 | Lib_IntVector_Intrinsics_vec128 f01 = f010; |
1264 | 0 | Lib_IntVector_Intrinsics_vec128 f111 = f110; |
1265 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = f20; |
1266 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = f30; |
1267 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = f40; |
1268 | 0 | e[0U] = f01; |
1269 | 0 | e[1U] = f111; |
1270 | 0 | e[2U] = f2; |
1271 | 0 | e[3U] = f3; |
1272 | 0 | e[4U] = f4; |
1273 | 0 | uint64_t b = (uint64_t)1U << rem * (uint32_t)8U % (uint32_t)26U; |
1274 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_load64(b); |
1275 | 0 | Lib_IntVector_Intrinsics_vec128 fi = e[rem * (uint32_t)8U / (uint32_t)26U]; |
1276 | 0 | e[rem * (uint32_t)8U / (uint32_t)26U] = Lib_IntVector_Intrinsics_vec128_or(fi, mask); |
1277 | 0 | Lib_IntVector_Intrinsics_vec128 *r = pre; |
1278 | 0 | Lib_IntVector_Intrinsics_vec128 *r5 = pre + (uint32_t)5U; |
1279 | 0 | Lib_IntVector_Intrinsics_vec128 r0 = r[0U]; |
1280 | 0 | Lib_IntVector_Intrinsics_vec128 r1 = r[1U]; |
1281 | 0 | Lib_IntVector_Intrinsics_vec128 r2 = r[2U]; |
1282 | 0 | Lib_IntVector_Intrinsics_vec128 r3 = r[3U]; |
1283 | 0 | Lib_IntVector_Intrinsics_vec128 r4 = r[4U]; |
1284 | 0 | Lib_IntVector_Intrinsics_vec128 r51 = r5[1U]; |
1285 | 0 | Lib_IntVector_Intrinsics_vec128 r52 = r5[2U]; |
1286 | 0 | Lib_IntVector_Intrinsics_vec128 r53 = r5[3U]; |
1287 | 0 | Lib_IntVector_Intrinsics_vec128 r54 = r5[4U]; |
1288 | 0 | Lib_IntVector_Intrinsics_vec128 f10 = e[0U]; |
1289 | 0 | Lib_IntVector_Intrinsics_vec128 f11 = e[1U]; |
1290 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = e[2U]; |
1291 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = e[3U]; |
1292 | 0 | Lib_IntVector_Intrinsics_vec128 f14 = e[4U]; |
1293 | 0 | Lib_IntVector_Intrinsics_vec128 a0 = acc[0U]; |
1294 | 0 | Lib_IntVector_Intrinsics_vec128 a1 = acc[1U]; |
1295 | 0 | Lib_IntVector_Intrinsics_vec128 a2 = acc[2U]; |
1296 | 0 | Lib_IntVector_Intrinsics_vec128 a3 = acc[3U]; |
1297 | 0 | Lib_IntVector_Intrinsics_vec128 a4 = acc[4U]; |
1298 | 0 | Lib_IntVector_Intrinsics_vec128 a01 = Lib_IntVector_Intrinsics_vec128_add64(a0, f10); |
1299 | 0 | Lib_IntVector_Intrinsics_vec128 a11 = Lib_IntVector_Intrinsics_vec128_add64(a1, f11); |
1300 | 0 | Lib_IntVector_Intrinsics_vec128 a21 = Lib_IntVector_Intrinsics_vec128_add64(a2, f12); |
1301 | 0 | Lib_IntVector_Intrinsics_vec128 a31 = Lib_IntVector_Intrinsics_vec128_add64(a3, f13); |
1302 | 0 | Lib_IntVector_Intrinsics_vec128 a41 = Lib_IntVector_Intrinsics_vec128_add64(a4, f14); |
1303 | 0 | Lib_IntVector_Intrinsics_vec128 a02 = Lib_IntVector_Intrinsics_vec128_mul64(r0, a01); |
1304 | 0 | Lib_IntVector_Intrinsics_vec128 a12 = Lib_IntVector_Intrinsics_vec128_mul64(r1, a01); |
1305 | 0 | Lib_IntVector_Intrinsics_vec128 a22 = Lib_IntVector_Intrinsics_vec128_mul64(r2, a01); |
1306 | 0 | Lib_IntVector_Intrinsics_vec128 a32 = Lib_IntVector_Intrinsics_vec128_mul64(r3, a01); |
1307 | 0 | Lib_IntVector_Intrinsics_vec128 a42 = Lib_IntVector_Intrinsics_vec128_mul64(r4, a01); |
1308 | 0 | Lib_IntVector_Intrinsics_vec128 |
1309 | 0 | a03 = |
1310 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a02, |
1311 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a11)); |
1312 | 0 | Lib_IntVector_Intrinsics_vec128 |
1313 | 0 | a13 = |
1314 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a12, |
1315 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a11)); |
1316 | 0 | Lib_IntVector_Intrinsics_vec128 |
1317 | 0 | a23 = |
1318 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a22, |
1319 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a11)); |
1320 | 0 | Lib_IntVector_Intrinsics_vec128 |
1321 | 0 | a33 = |
1322 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a32, |
1323 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a11)); |
1324 | 0 | Lib_IntVector_Intrinsics_vec128 |
1325 | 0 | a43 = |
1326 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a42, |
1327 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r3, a11)); |
1328 | 0 | Lib_IntVector_Intrinsics_vec128 |
1329 | 0 | a04 = |
1330 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a03, |
1331 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a21)); |
1332 | 0 | Lib_IntVector_Intrinsics_vec128 |
1333 | 0 | a14 = |
1334 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a13, |
1335 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a21)); |
1336 | 0 | Lib_IntVector_Intrinsics_vec128 |
1337 | 0 | a24 = |
1338 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a23, |
1339 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a21)); |
1340 | 0 | Lib_IntVector_Intrinsics_vec128 |
1341 | 0 | a34 = |
1342 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a33, |
1343 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a21)); |
1344 | 0 | Lib_IntVector_Intrinsics_vec128 |
1345 | 0 | a44 = |
1346 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a43, |
1347 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r2, a21)); |
1348 | 0 | Lib_IntVector_Intrinsics_vec128 |
1349 | 0 | a05 = |
1350 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a04, |
1351 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a31)); |
1352 | 0 | Lib_IntVector_Intrinsics_vec128 |
1353 | 0 | a15 = |
1354 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a14, |
1355 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a31)); |
1356 | 0 | Lib_IntVector_Intrinsics_vec128 |
1357 | 0 | a25 = |
1358 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a24, |
1359 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a31)); |
1360 | 0 | Lib_IntVector_Intrinsics_vec128 |
1361 | 0 | a35 = |
1362 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a34, |
1363 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a31)); |
1364 | 0 | Lib_IntVector_Intrinsics_vec128 |
1365 | 0 | a45 = |
1366 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a44, |
1367 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r1, a31)); |
1368 | 0 | Lib_IntVector_Intrinsics_vec128 |
1369 | 0 | a06 = |
1370 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a05, |
1371 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r51, a41)); |
1372 | 0 | Lib_IntVector_Intrinsics_vec128 |
1373 | 0 | a16 = |
1374 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a15, |
1375 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r52, a41)); |
1376 | 0 | Lib_IntVector_Intrinsics_vec128 |
1377 | 0 | a26 = |
1378 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a25, |
1379 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r53, a41)); |
1380 | 0 | Lib_IntVector_Intrinsics_vec128 |
1381 | 0 | a36 = |
1382 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a35, |
1383 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r54, a41)); |
1384 | 0 | Lib_IntVector_Intrinsics_vec128 |
1385 | 0 | a46 = |
1386 | 0 | Lib_IntVector_Intrinsics_vec128_add64(a45, |
1387 | 0 | Lib_IntVector_Intrinsics_vec128_mul64(r0, a41)); |
1388 | 0 | Lib_IntVector_Intrinsics_vec128 t01 = a06; |
1389 | 0 | Lib_IntVector_Intrinsics_vec128 t11 = a16; |
1390 | 0 | Lib_IntVector_Intrinsics_vec128 t2 = a26; |
1391 | 0 | Lib_IntVector_Intrinsics_vec128 t3 = a36; |
1392 | 0 | Lib_IntVector_Intrinsics_vec128 t4 = a46; |
1393 | 0 | Lib_IntVector_Intrinsics_vec128 |
1394 | 0 | mask26 = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
1395 | 0 | Lib_IntVector_Intrinsics_vec128 |
1396 | 0 | z0 = Lib_IntVector_Intrinsics_vec128_shift_right64(t01, (uint32_t)26U); |
1397 | 0 | Lib_IntVector_Intrinsics_vec128 |
1398 | 0 | z1 = Lib_IntVector_Intrinsics_vec128_shift_right64(t3, (uint32_t)26U); |
1399 | 0 | Lib_IntVector_Intrinsics_vec128 x0 = Lib_IntVector_Intrinsics_vec128_and(t01, mask26); |
1400 | 0 | Lib_IntVector_Intrinsics_vec128 x3 = Lib_IntVector_Intrinsics_vec128_and(t3, mask26); |
1401 | 0 | Lib_IntVector_Intrinsics_vec128 x1 = Lib_IntVector_Intrinsics_vec128_add64(t11, z0); |
1402 | 0 | Lib_IntVector_Intrinsics_vec128 x4 = Lib_IntVector_Intrinsics_vec128_add64(t4, z1); |
1403 | 0 | Lib_IntVector_Intrinsics_vec128 |
1404 | 0 | z01 = Lib_IntVector_Intrinsics_vec128_shift_right64(x1, (uint32_t)26U); |
1405 | 0 | Lib_IntVector_Intrinsics_vec128 |
1406 | 0 | z11 = Lib_IntVector_Intrinsics_vec128_shift_right64(x4, (uint32_t)26U); |
1407 | 0 | Lib_IntVector_Intrinsics_vec128 |
1408 | 0 | t = Lib_IntVector_Intrinsics_vec128_shift_left64(z11, (uint32_t)2U); |
1409 | 0 | Lib_IntVector_Intrinsics_vec128 z12 = Lib_IntVector_Intrinsics_vec128_add64(z11, t); |
1410 | 0 | Lib_IntVector_Intrinsics_vec128 x11 = Lib_IntVector_Intrinsics_vec128_and(x1, mask26); |
1411 | 0 | Lib_IntVector_Intrinsics_vec128 x41 = Lib_IntVector_Intrinsics_vec128_and(x4, mask26); |
1412 | 0 | Lib_IntVector_Intrinsics_vec128 x2 = Lib_IntVector_Intrinsics_vec128_add64(t2, z01); |
1413 | 0 | Lib_IntVector_Intrinsics_vec128 x01 = Lib_IntVector_Intrinsics_vec128_add64(x0, z12); |
1414 | 0 | Lib_IntVector_Intrinsics_vec128 |
1415 | 0 | z02 = Lib_IntVector_Intrinsics_vec128_shift_right64(x2, (uint32_t)26U); |
1416 | 0 | Lib_IntVector_Intrinsics_vec128 |
1417 | 0 | z13 = Lib_IntVector_Intrinsics_vec128_shift_right64(x01, (uint32_t)26U); |
1418 | 0 | Lib_IntVector_Intrinsics_vec128 x21 = Lib_IntVector_Intrinsics_vec128_and(x2, mask26); |
1419 | 0 | Lib_IntVector_Intrinsics_vec128 x02 = Lib_IntVector_Intrinsics_vec128_and(x01, mask26); |
1420 | 0 | Lib_IntVector_Intrinsics_vec128 x31 = Lib_IntVector_Intrinsics_vec128_add64(x3, z02); |
1421 | 0 | Lib_IntVector_Intrinsics_vec128 x12 = Lib_IntVector_Intrinsics_vec128_add64(x11, z13); |
1422 | 0 | Lib_IntVector_Intrinsics_vec128 |
1423 | 0 | z03 = Lib_IntVector_Intrinsics_vec128_shift_right64(x31, (uint32_t)26U); |
1424 | 0 | Lib_IntVector_Intrinsics_vec128 x32 = Lib_IntVector_Intrinsics_vec128_and(x31, mask26); |
1425 | 0 | Lib_IntVector_Intrinsics_vec128 x42 = Lib_IntVector_Intrinsics_vec128_add64(x41, z03); |
1426 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = x02; |
1427 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = x12; |
1428 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = x21; |
1429 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = x32; |
1430 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = x42; |
1431 | 0 | acc[0U] = o0; |
1432 | 0 | acc[1U] = o1; |
1433 | 0 | acc[2U] = o2; |
1434 | 0 | acc[3U] = o3; |
1435 | 0 | acc[4U] = o4; |
1436 | 0 | return; |
1437 | 0 | } |
1438 | 0 | } |
1439 | | |
1440 | | void |
1441 | | Hacl_Poly1305_128_poly1305_finish( |
1442 | | uint8_t *tag, |
1443 | | uint8_t *key, |
1444 | | Lib_IntVector_Intrinsics_vec128 *ctx) |
1445 | 0 | { |
1446 | 0 | Lib_IntVector_Intrinsics_vec128 *acc = ctx; |
1447 | 0 | uint8_t *ks = key + (uint32_t)16U; |
1448 | 0 | Lib_IntVector_Intrinsics_vec128 f0 = acc[0U]; |
1449 | 0 | Lib_IntVector_Intrinsics_vec128 f13 = acc[1U]; |
1450 | 0 | Lib_IntVector_Intrinsics_vec128 f23 = acc[2U]; |
1451 | 0 | Lib_IntVector_Intrinsics_vec128 f33 = acc[3U]; |
1452 | 0 | Lib_IntVector_Intrinsics_vec128 f40 = acc[4U]; |
1453 | 0 | Lib_IntVector_Intrinsics_vec128 |
1454 | 0 | l0 = Lib_IntVector_Intrinsics_vec128_add64(f0, Lib_IntVector_Intrinsics_vec128_zero); |
1455 | 0 | Lib_IntVector_Intrinsics_vec128 |
1456 | 0 | tmp00 = |
1457 | 0 | Lib_IntVector_Intrinsics_vec128_and(l0, |
1458 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1459 | 0 | Lib_IntVector_Intrinsics_vec128 |
1460 | 0 | c00 = Lib_IntVector_Intrinsics_vec128_shift_right64(l0, (uint32_t)26U); |
1461 | 0 | Lib_IntVector_Intrinsics_vec128 l1 = Lib_IntVector_Intrinsics_vec128_add64(f13, c00); |
1462 | 0 | Lib_IntVector_Intrinsics_vec128 |
1463 | 0 | tmp10 = |
1464 | 0 | Lib_IntVector_Intrinsics_vec128_and(l1, |
1465 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1466 | 0 | Lib_IntVector_Intrinsics_vec128 |
1467 | 0 | c10 = Lib_IntVector_Intrinsics_vec128_shift_right64(l1, (uint32_t)26U); |
1468 | 0 | Lib_IntVector_Intrinsics_vec128 l2 = Lib_IntVector_Intrinsics_vec128_add64(f23, c10); |
1469 | 0 | Lib_IntVector_Intrinsics_vec128 |
1470 | 0 | tmp20 = |
1471 | 0 | Lib_IntVector_Intrinsics_vec128_and(l2, |
1472 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1473 | 0 | Lib_IntVector_Intrinsics_vec128 |
1474 | 0 | c20 = Lib_IntVector_Intrinsics_vec128_shift_right64(l2, (uint32_t)26U); |
1475 | 0 | Lib_IntVector_Intrinsics_vec128 l3 = Lib_IntVector_Intrinsics_vec128_add64(f33, c20); |
1476 | 0 | Lib_IntVector_Intrinsics_vec128 |
1477 | 0 | tmp30 = |
1478 | 0 | Lib_IntVector_Intrinsics_vec128_and(l3, |
1479 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1480 | 0 | Lib_IntVector_Intrinsics_vec128 |
1481 | 0 | c30 = Lib_IntVector_Intrinsics_vec128_shift_right64(l3, (uint32_t)26U); |
1482 | 0 | Lib_IntVector_Intrinsics_vec128 l4 = Lib_IntVector_Intrinsics_vec128_add64(f40, c30); |
1483 | 0 | Lib_IntVector_Intrinsics_vec128 |
1484 | 0 | tmp40 = |
1485 | 0 | Lib_IntVector_Intrinsics_vec128_and(l4, |
1486 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1487 | 0 | Lib_IntVector_Intrinsics_vec128 |
1488 | 0 | c40 = Lib_IntVector_Intrinsics_vec128_shift_right64(l4, (uint32_t)26U); |
1489 | 0 | Lib_IntVector_Intrinsics_vec128 |
1490 | 0 | f010 = |
1491 | 0 | Lib_IntVector_Intrinsics_vec128_add64(tmp00, |
1492 | 0 | Lib_IntVector_Intrinsics_vec128_smul64(c40, (uint64_t)5U)); |
1493 | 0 | Lib_IntVector_Intrinsics_vec128 f110 = tmp10; |
1494 | 0 | Lib_IntVector_Intrinsics_vec128 f210 = tmp20; |
1495 | 0 | Lib_IntVector_Intrinsics_vec128 f310 = tmp30; |
1496 | 0 | Lib_IntVector_Intrinsics_vec128 f410 = tmp40; |
1497 | 0 | Lib_IntVector_Intrinsics_vec128 |
1498 | 0 | l = Lib_IntVector_Intrinsics_vec128_add64(f010, Lib_IntVector_Intrinsics_vec128_zero); |
1499 | 0 | Lib_IntVector_Intrinsics_vec128 |
1500 | 0 | tmp0 = |
1501 | 0 | Lib_IntVector_Intrinsics_vec128_and(l, |
1502 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1503 | 0 | Lib_IntVector_Intrinsics_vec128 |
1504 | 0 | c0 = Lib_IntVector_Intrinsics_vec128_shift_right64(l, (uint32_t)26U); |
1505 | 0 | Lib_IntVector_Intrinsics_vec128 l5 = Lib_IntVector_Intrinsics_vec128_add64(f110, c0); |
1506 | 0 | Lib_IntVector_Intrinsics_vec128 |
1507 | 0 | tmp1 = |
1508 | 0 | Lib_IntVector_Intrinsics_vec128_and(l5, |
1509 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1510 | 0 | Lib_IntVector_Intrinsics_vec128 |
1511 | 0 | c1 = Lib_IntVector_Intrinsics_vec128_shift_right64(l5, (uint32_t)26U); |
1512 | 0 | Lib_IntVector_Intrinsics_vec128 l6 = Lib_IntVector_Intrinsics_vec128_add64(f210, c1); |
1513 | 0 | Lib_IntVector_Intrinsics_vec128 |
1514 | 0 | tmp2 = |
1515 | 0 | Lib_IntVector_Intrinsics_vec128_and(l6, |
1516 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1517 | 0 | Lib_IntVector_Intrinsics_vec128 |
1518 | 0 | c2 = Lib_IntVector_Intrinsics_vec128_shift_right64(l6, (uint32_t)26U); |
1519 | 0 | Lib_IntVector_Intrinsics_vec128 l7 = Lib_IntVector_Intrinsics_vec128_add64(f310, c2); |
1520 | 0 | Lib_IntVector_Intrinsics_vec128 |
1521 | 0 | tmp3 = |
1522 | 0 | Lib_IntVector_Intrinsics_vec128_and(l7, |
1523 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1524 | 0 | Lib_IntVector_Intrinsics_vec128 |
1525 | 0 | c3 = Lib_IntVector_Intrinsics_vec128_shift_right64(l7, (uint32_t)26U); |
1526 | 0 | Lib_IntVector_Intrinsics_vec128 l8 = Lib_IntVector_Intrinsics_vec128_add64(f410, c3); |
1527 | 0 | Lib_IntVector_Intrinsics_vec128 |
1528 | 0 | tmp4 = |
1529 | 0 | Lib_IntVector_Intrinsics_vec128_and(l8, |
1530 | 0 | Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU)); |
1531 | 0 | Lib_IntVector_Intrinsics_vec128 |
1532 | 0 | c4 = Lib_IntVector_Intrinsics_vec128_shift_right64(l8, (uint32_t)26U); |
1533 | 0 | Lib_IntVector_Intrinsics_vec128 |
1534 | 0 | f02 = |
1535 | 0 | Lib_IntVector_Intrinsics_vec128_add64(tmp0, |
1536 | 0 | Lib_IntVector_Intrinsics_vec128_smul64(c4, (uint64_t)5U)); |
1537 | 0 | Lib_IntVector_Intrinsics_vec128 f12 = tmp1; |
1538 | 0 | Lib_IntVector_Intrinsics_vec128 f22 = tmp2; |
1539 | 0 | Lib_IntVector_Intrinsics_vec128 f32 = tmp3; |
1540 | 0 | Lib_IntVector_Intrinsics_vec128 f42 = tmp4; |
1541 | 0 | Lib_IntVector_Intrinsics_vec128 |
1542 | 0 | mh = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3ffffffU); |
1543 | 0 | Lib_IntVector_Intrinsics_vec128 |
1544 | 0 | ml = Lib_IntVector_Intrinsics_vec128_load64((uint64_t)0x3fffffbU); |
1545 | 0 | Lib_IntVector_Intrinsics_vec128 mask = Lib_IntVector_Intrinsics_vec128_eq64(f42, mh); |
1546 | 0 | Lib_IntVector_Intrinsics_vec128 |
1547 | 0 | mask1 = |
1548 | 0 | Lib_IntVector_Intrinsics_vec128_and(mask, |
1549 | 0 | Lib_IntVector_Intrinsics_vec128_eq64(f32, mh)); |
1550 | 0 | Lib_IntVector_Intrinsics_vec128 |
1551 | 0 | mask2 = |
1552 | 0 | Lib_IntVector_Intrinsics_vec128_and(mask1, |
1553 | 0 | Lib_IntVector_Intrinsics_vec128_eq64(f22, mh)); |
1554 | 0 | Lib_IntVector_Intrinsics_vec128 |
1555 | 0 | mask3 = |
1556 | 0 | Lib_IntVector_Intrinsics_vec128_and(mask2, |
1557 | 0 | Lib_IntVector_Intrinsics_vec128_eq64(f12, mh)); |
1558 | 0 | Lib_IntVector_Intrinsics_vec128 |
1559 | 0 | mask4 = |
1560 | 0 | Lib_IntVector_Intrinsics_vec128_and(mask3, |
1561 | 0 | Lib_IntVector_Intrinsics_vec128_lognot(Lib_IntVector_Intrinsics_vec128_gt64(ml, f02))); |
1562 | 0 | Lib_IntVector_Intrinsics_vec128 ph = Lib_IntVector_Intrinsics_vec128_and(mask4, mh); |
1563 | 0 | Lib_IntVector_Intrinsics_vec128 pl = Lib_IntVector_Intrinsics_vec128_and(mask4, ml); |
1564 | 0 | Lib_IntVector_Intrinsics_vec128 o0 = Lib_IntVector_Intrinsics_vec128_sub64(f02, pl); |
1565 | 0 | Lib_IntVector_Intrinsics_vec128 o1 = Lib_IntVector_Intrinsics_vec128_sub64(f12, ph); |
1566 | 0 | Lib_IntVector_Intrinsics_vec128 o2 = Lib_IntVector_Intrinsics_vec128_sub64(f22, ph); |
1567 | 0 | Lib_IntVector_Intrinsics_vec128 o3 = Lib_IntVector_Intrinsics_vec128_sub64(f32, ph); |
1568 | 0 | Lib_IntVector_Intrinsics_vec128 o4 = Lib_IntVector_Intrinsics_vec128_sub64(f42, ph); |
1569 | 0 | Lib_IntVector_Intrinsics_vec128 f011 = o0; |
1570 | 0 | Lib_IntVector_Intrinsics_vec128 f111 = o1; |
1571 | 0 | Lib_IntVector_Intrinsics_vec128 f211 = o2; |
1572 | 0 | Lib_IntVector_Intrinsics_vec128 f311 = o3; |
1573 | 0 | Lib_IntVector_Intrinsics_vec128 f411 = o4; |
1574 | 0 | acc[0U] = f011; |
1575 | 0 | acc[1U] = f111; |
1576 | 0 | acc[2U] = f211; |
1577 | 0 | acc[3U] = f311; |
1578 | 0 | acc[4U] = f411; |
1579 | 0 | Lib_IntVector_Intrinsics_vec128 f00 = acc[0U]; |
1580 | 0 | Lib_IntVector_Intrinsics_vec128 f1 = acc[1U]; |
1581 | 0 | Lib_IntVector_Intrinsics_vec128 f2 = acc[2U]; |
1582 | 0 | Lib_IntVector_Intrinsics_vec128 f3 = acc[3U]; |
1583 | 0 | Lib_IntVector_Intrinsics_vec128 f4 = acc[4U]; |
1584 | 0 | uint64_t f01 = Lib_IntVector_Intrinsics_vec128_extract64(f00, (uint32_t)0U); |
1585 | 0 | uint64_t f112 = Lib_IntVector_Intrinsics_vec128_extract64(f1, (uint32_t)0U); |
1586 | 0 | uint64_t f212 = Lib_IntVector_Intrinsics_vec128_extract64(f2, (uint32_t)0U); |
1587 | 0 | uint64_t f312 = Lib_IntVector_Intrinsics_vec128_extract64(f3, (uint32_t)0U); |
1588 | 0 | uint64_t f41 = Lib_IntVector_Intrinsics_vec128_extract64(f4, (uint32_t)0U); |
1589 | 0 | uint64_t lo = (f01 | f112 << (uint32_t)26U) | f212 << (uint32_t)52U; |
1590 | 0 | uint64_t hi = (f212 >> (uint32_t)12U | f312 << (uint32_t)14U) | f41 << (uint32_t)40U; |
1591 | 0 | uint64_t f10 = lo; |
1592 | 0 | uint64_t f11 = hi; |
1593 | 0 | uint64_t u0 = load64_le(ks); |
1594 | 0 | uint64_t lo0 = u0; |
1595 | 0 | uint64_t u = load64_le(ks + (uint32_t)8U); |
1596 | 0 | uint64_t hi0 = u; |
1597 | 0 | uint64_t f20 = lo0; |
1598 | 0 | uint64_t f21 = hi0; |
1599 | 0 | uint64_t r0 = f10 + f20; |
1600 | 0 | uint64_t r1 = f11 + f21; |
1601 | 0 | uint64_t c = (r0 ^ ((r0 ^ f20) | ((r0 - f20) ^ f20))) >> (uint32_t)63U; |
1602 | 0 | uint64_t r11 = r1 + c; |
1603 | 0 | uint64_t f30 = r0; |
1604 | 0 | uint64_t f31 = r11; |
1605 | 0 | store64_le(tag, f30); |
1606 | 0 | store64_le(tag + (uint32_t)8U, f31); |
1607 | 0 | } |
1608 | | |
1609 | | void |
1610 | | Hacl_Poly1305_128_poly1305_mac(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key) |
1611 | 0 | { |
1612 | 0 | KRML_PRE_ALIGN(16) |
1613 | 0 | Lib_IntVector_Intrinsics_vec128 ctx[25U] KRML_POST_ALIGN(16) = { 0U }; |
1614 | 0 | Hacl_Poly1305_128_poly1305_init(ctx, key); |
1615 | 0 | Hacl_Poly1305_128_poly1305_update(ctx, len, text); |
1616 | 0 | Hacl_Poly1305_128_poly1305_finish(tag, key, ctx); |
1617 | 0 | } |