Coverage Report

Created: 2026-02-18 06:59

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