Coverage Report

Created: 2026-10-06 06:17

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