Coverage Report

Created: 2024-11-21 07:03

/src/nss-nspr/nss/lib/freebl/verified/Hacl_P521.c
Line
Count
Source (jump to first uncovered line)
1
/* MIT License
2
 *
3
 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
4
 * Copyright (c) 2022-2023 HACL* Contributors
5
 *
6
 * Permission is hereby granted, free of charge, to any person obtaining a copy
7
 * of this software and associated documentation files (the "Software"), to deal
8
 * in the Software without restriction, including without limitation the rights
9
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10
 * copies of the Software, and to permit persons to whom the Software is
11
 * furnished to do so, subject to the following conditions:
12
 *
13
 * The above copyright notice and this permission notice shall be included in all
14
 * copies or substantial portions of the Software.
15
 *
16
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22
 * SOFTWARE.
23
 */
24
25
#include "Hacl_P521.h"
26
27
#include "internal/Hacl_Krmllib.h"
28
#include "internal/Hacl_Bignum_Base.h"
29
30
static inline uint64_t
31
bn_is_eq_mask(uint64_t *x, uint64_t *y)
32
417
{
33
417
    uint64_t mask = 0xFFFFFFFFFFFFFFFFULL;
34
417
    KRML_MAYBE_FOR9(i,
35
417
                    0U,
36
417
                    9U,
37
417
                    1U,
38
417
                    uint64_t uu____0 = FStar_UInt64_eq_mask(x[i], y[i]);
39
417
                    mask = uu____0 & mask;);
40
417
    uint64_t mask1 = mask;
41
417
    return mask1;
42
417
}
43
44
static inline void
45
bn_cmovznz(uint64_t *a, uint64_t b, uint64_t *c, uint64_t *d)
46
136
{
47
136
    uint64_t mask = ~FStar_UInt64_eq_mask(b, 0ULL);
48
136
    KRML_MAYBE_FOR9(i,
49
136
                    0U,
50
136
                    9U,
51
136
                    1U,
52
136
                    uint64_t *os = a;
53
136
                    uint64_t uu____0 = c[i];
54
136
                    uint64_t x = uu____0 ^ (mask & (d[i] ^ uu____0));
55
136
                    os[i] = x;);
56
136
}
57
58
static inline void
59
bn_add_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d)
60
1.79M
{
61
1.79M
    uint64_t c10 = 0ULL;
62
1.79M
    KRML_MAYBE_FOR2(i,
63
1.79M
                    0U,
64
1.79M
                    2U,
65
1.79M
                    1U,
66
1.79M
                    uint64_t t1 = c[4U * i];
67
1.79M
                    uint64_t t20 = d[4U * i];
68
1.79M
                    uint64_t *res_i0 = a + 4U * i;
69
1.79M
                    c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t20, res_i0);
70
1.79M
                    uint64_t t10 = c[4U * i + 1U];
71
1.79M
                    uint64_t t21 = d[4U * i + 1U];
72
1.79M
                    uint64_t *res_i1 = a + 4U * i + 1U;
73
1.79M
                    c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t10, t21, res_i1);
74
1.79M
                    uint64_t t11 = c[4U * i + 2U];
75
1.79M
                    uint64_t t22 = d[4U * i + 2U];
76
1.79M
                    uint64_t *res_i2 = a + 4U * i + 2U;
77
1.79M
                    c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t11, t22, res_i2);
78
1.79M
                    uint64_t t12 = c[4U * i + 3U];
79
1.79M
                    uint64_t t2 = d[4U * i + 3U];
80
1.79M
                    uint64_t *res_i = a + 4U * i + 3U;
81
1.79M
                    c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t12, t2, res_i););
82
1.79M
    {
83
1.79M
        uint64_t t1 = c[8U];
84
1.79M
        uint64_t t2 = d[8U];
85
1.79M
        uint64_t *res_i = a + 8U;
86
1.79M
        c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t2, res_i);
87
1.79M
    }
88
1.79M
    uint64_t c0 = c10;
89
1.79M
    uint64_t tmp[9U] = { 0U };
90
1.79M
    uint64_t c1 = 0ULL;
91
1.79M
    KRML_MAYBE_FOR2(i,
92
1.79M
                    0U,
93
1.79M
                    2U,
94
1.79M
                    1U,
95
1.79M
                    uint64_t t1 = a[4U * i];
96
1.79M
                    uint64_t t20 = b[4U * i];
97
1.79M
                    uint64_t *res_i0 = tmp + 4U * i;
98
1.79M
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0);
99
1.79M
                    uint64_t t10 = a[4U * i + 1U];
100
1.79M
                    uint64_t t21 = b[4U * i + 1U];
101
1.79M
                    uint64_t *res_i1 = tmp + 4U * i + 1U;
102
1.79M
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1);
103
1.79M
                    uint64_t t11 = a[4U * i + 2U];
104
1.79M
                    uint64_t t22 = b[4U * i + 2U];
105
1.79M
                    uint64_t *res_i2 = tmp + 4U * i + 2U;
106
1.79M
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2);
107
1.79M
                    uint64_t t12 = a[4U * i + 3U];
108
1.79M
                    uint64_t t2 = b[4U * i + 3U];
109
1.79M
                    uint64_t *res_i = tmp + 4U * i + 3U;
110
1.79M
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i););
111
1.79M
    {
112
1.79M
        uint64_t t1 = a[8U];
113
1.79M
        uint64_t t2 = b[8U];
114
1.79M
        uint64_t *res_i = tmp + 8U;
115
1.79M
        c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);
116
1.79M
    }
117
1.79M
    uint64_t c11 = c1;
118
1.79M
    uint64_t c2 = c0 - c11;
119
1.79M
    KRML_MAYBE_FOR9(i,
120
1.79M
                    0U,
121
1.79M
                    9U,
122
1.79M
                    1U,
123
1.79M
                    uint64_t *os = a;
124
1.79M
                    uint64_t x = (c2 & a[i]) | (~c2 & tmp[i]);
125
1.79M
                    os[i] = x;);
126
1.79M
}
127
128
static inline uint64_t
129
bn_sub(uint64_t *a, uint64_t *b, uint64_t *c)
130
496
{
131
496
    uint64_t c1 = 0ULL;
132
496
    KRML_MAYBE_FOR2(i,
133
496
                    0U,
134
496
                    2U,
135
496
                    1U,
136
496
                    uint64_t t1 = b[4U * i];
137
496
                    uint64_t t20 = c[4U * i];
138
496
                    uint64_t *res_i0 = a + 4U * i;
139
496
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0);
140
496
                    uint64_t t10 = b[4U * i + 1U];
141
496
                    uint64_t t21 = c[4U * i + 1U];
142
496
                    uint64_t *res_i1 = a + 4U * i + 1U;
143
496
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1);
144
496
                    uint64_t t11 = b[4U * i + 2U];
145
496
                    uint64_t t22 = c[4U * i + 2U];
146
496
                    uint64_t *res_i2 = a + 4U * i + 2U;
147
496
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2);
148
496
                    uint64_t t12 = b[4U * i + 3U];
149
496
                    uint64_t t2 = c[4U * i + 3U];
150
496
                    uint64_t *res_i = a + 4U * i + 3U;
151
496
                    c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i););
152
496
    {
153
496
        uint64_t t1 = b[8U];
154
496
        uint64_t t2 = c[8U];
155
496
        uint64_t *res_i = a + 8U;
156
496
        c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);
157
496
    }
158
496
    uint64_t c10 = c1;
159
496
    return c10;
160
496
}
161
162
static inline void
163
bn_sub_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d)
164
743k
{
165
743k
    uint64_t c10 = 0ULL;
166
743k
    KRML_MAYBE_FOR2(i,
167
743k
                    0U,
168
743k
                    2U,
169
743k
                    1U,
170
743k
                    uint64_t t1 = c[4U * i];
171
743k
                    uint64_t t20 = d[4U * i];
172
743k
                    uint64_t *res_i0 = a + 4U * i;
173
743k
                    c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t20, res_i0);
174
743k
                    uint64_t t10 = c[4U * i + 1U];
175
743k
                    uint64_t t21 = d[4U * i + 1U];
176
743k
                    uint64_t *res_i1 = a + 4U * i + 1U;
177
743k
                    c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t10, t21, res_i1);
178
743k
                    uint64_t t11 = c[4U * i + 2U];
179
743k
                    uint64_t t22 = d[4U * i + 2U];
180
743k
                    uint64_t *res_i2 = a + 4U * i + 2U;
181
743k
                    c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t11, t22, res_i2);
182
743k
                    uint64_t t12 = c[4U * i + 3U];
183
743k
                    uint64_t t2 = d[4U * i + 3U];
184
743k
                    uint64_t *res_i = a + 4U * i + 3U;
185
743k
                    c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t12, t2, res_i););
186
743k
    {
187
743k
        uint64_t t1 = c[8U];
188
743k
        uint64_t t2 = d[8U];
189
743k
        uint64_t *res_i = a + 8U;
190
743k
        c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t2, res_i);
191
743k
    }
192
743k
    uint64_t c0 = c10;
193
743k
    uint64_t tmp[9U] = { 0U };
194
743k
    uint64_t c1 = 0ULL;
195
743k
    KRML_MAYBE_FOR2(i,
196
743k
                    0U,
197
743k
                    2U,
198
743k
                    1U,
199
743k
                    uint64_t t1 = a[4U * i];
200
743k
                    uint64_t t20 = b[4U * i];
201
743k
                    uint64_t *res_i0 = tmp + 4U * i;
202
743k
                    c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t20, res_i0);
203
743k
                    uint64_t t10 = a[4U * i + 1U];
204
743k
                    uint64_t t21 = b[4U * i + 1U];
205
743k
                    uint64_t *res_i1 = tmp + 4U * i + 1U;
206
743k
                    c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t10, t21, res_i1);
207
743k
                    uint64_t t11 = a[4U * i + 2U];
208
743k
                    uint64_t t22 = b[4U * i + 2U];
209
743k
                    uint64_t *res_i2 = tmp + 4U * i + 2U;
210
743k
                    c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t11, t22, res_i2);
211
743k
                    uint64_t t12 = a[4U * i + 3U];
212
743k
                    uint64_t t2 = b[4U * i + 3U];
213
743k
                    uint64_t *res_i = tmp + 4U * i + 3U;
214
743k
                    c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t12, t2, res_i););
215
743k
    {
216
743k
        uint64_t t1 = a[8U];
217
743k
        uint64_t t2 = b[8U];
218
743k
        uint64_t *res_i = tmp + 8U;
219
743k
        c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t2, res_i);
220
743k
    }
221
743k
    uint64_t c11 = c1;
222
743k
    KRML_MAYBE_UNUSED_VAR(c11);
223
743k
    uint64_t c2 = 0ULL - c0;
224
743k
    KRML_MAYBE_FOR9(i,
225
743k
                    0U,
226
743k
                    9U,
227
743k
                    1U,
228
743k
                    uint64_t *os = a;
229
743k
                    uint64_t x = (c2 & tmp[i]) | (~c2 & a[i]);
230
743k
                    os[i] = x;);
231
743k
}
232
233
static inline void
234
bn_mul(uint64_t *a, uint64_t *b, uint64_t *c)
235
1.24M
{
236
1.24M
    memset(a, 0U, 18U * sizeof(uint64_t));
237
1.24M
    KRML_MAYBE_FOR9(
238
1.24M
        i0,
239
1.24M
        0U,
240
1.24M
        9U,
241
1.24M
        1U,
242
1.24M
        uint64_t bj = c[i0];
243
1.24M
        uint64_t *res_j = a + i0;
244
1.24M
        uint64_t c1 = 0ULL;
245
1.24M
        KRML_MAYBE_FOR2(i,
246
1.24M
                        0U,
247
1.24M
                        2U,
248
1.24M
                        1U,
249
1.24M
                        uint64_t a_i = b[4U * i];
250
1.24M
                        uint64_t *res_i0 = res_j + 4U * i;
251
1.24M
                        c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i0);
252
1.24M
                        uint64_t a_i0 = b[4U * i + 1U];
253
1.24M
                        uint64_t *res_i1 = res_j + 4U * i + 1U;
254
1.24M
                        c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c1, res_i1);
255
1.24M
                        uint64_t a_i1 = b[4U * i + 2U];
256
1.24M
                        uint64_t *res_i2 = res_j + 4U * i + 2U;
257
1.24M
                        c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c1, res_i2);
258
1.24M
                        uint64_t a_i2 = b[4U * i + 3U];
259
1.24M
                        uint64_t *res_i = res_j + 4U * i + 3U;
260
1.24M
                        c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c1, res_i););
261
1.24M
        {
262
1.24M
            uint64_t a_i = b[8U];
263
1.24M
            uint64_t *res_i = res_j + 8U;
264
1.24M
            c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i);
265
1.24M
        } uint64_t r = c1;
266
1.24M
        a[9U + i0] = r;);
267
1.24M
}
268
269
static inline void
270
bn_sqr(uint64_t *a, uint64_t *b)
271
375k
{
272
375k
    memset(a, 0U, 18U * sizeof(uint64_t));
273
375k
    KRML_MAYBE_FOR9(
274
375k
        i0,
275
375k
        0U,
276
375k
        9U,
277
375k
        1U,
278
375k
        uint64_t *ab = b;
279
375k
        uint64_t a_j = b[i0];
280
375k
        uint64_t *res_j = a + i0;
281
375k
        uint64_t c = 0ULL;
282
375k
        for (uint32_t i = 0U; i < i0 / 4U; i++) {
283
375k
            uint64_t a_i = ab[4U * i];
284
375k
            uint64_t *res_i0 = res_j + 4U * i;
285
375k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i0);
286
375k
            uint64_t a_i0 = ab[4U * i + 1U];
287
375k
            uint64_t *res_i1 = res_j + 4U * i + 1U;
288
375k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, a_j, c, res_i1);
289
375k
            uint64_t a_i1 = ab[4U * i + 2U];
290
375k
            uint64_t *res_i2 = res_j + 4U * i + 2U;
291
375k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, a_j, c, res_i2);
292
375k
            uint64_t a_i2 = ab[4U * i + 3U];
293
375k
            uint64_t *res_i = res_j + 4U * i + 3U;
294
375k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, a_j, c, res_i);
295
375k
        } for (uint32_t i = i0 / 4U * 4U; i < i0; i++) {
296
375k
            uint64_t a_i = ab[i];
297
375k
            uint64_t *res_i = res_j + i;
298
375k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i);
299
375k
        } uint64_t r = c;
300
375k
        a[i0 + i0] = r;);
301
375k
    uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(18U, a, a, a);
302
375k
    KRML_MAYBE_UNUSED_VAR(c0);
303
375k
    uint64_t tmp[18U] = { 0U };
304
375k
    KRML_MAYBE_FOR9(i,
305
375k
                    0U,
306
375k
                    9U,
307
375k
                    1U,
308
375k
                    FStar_UInt128_uint128 res = FStar_UInt128_mul_wide(b[i], b[i]);
309
375k
                    uint64_t hi = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, 64U));
310
375k
                    uint64_t lo = FStar_UInt128_uint128_to_uint64(res);
311
375k
                    tmp[2U * i] = lo;
312
375k
                    tmp[2U * i + 1U] = hi;);
313
375k
    uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(18U, a, tmp, a);
314
375k
    KRML_MAYBE_UNUSED_VAR(c1);
315
375k
}
316
317
static inline void
318
bn_to_bytes_be(uint8_t *a, uint64_t *b)
319
202
{
320
202
    uint8_t tmp[72U] = { 0U };
321
202
    KRML_MAYBE_FOR9(i, 0U, 9U, 1U, store64_be(tmp + i * 8U, b[9U - i - 1U]););
322
202
    memcpy(a, tmp + 6U, 66U * sizeof(uint8_t));
323
202
}
324
325
static inline void
326
bn_from_bytes_be(uint64_t *a, uint8_t *b)
327
428
{
328
428
    uint8_t tmp[72U] = { 0U };
329
428
    memcpy(tmp + 6U, b, 66U * sizeof(uint8_t));
330
428
    KRML_MAYBE_FOR9(i,
331
428
                    0U,
332
428
                    9U,
333
428
                    1U,
334
428
                    uint64_t *os = a;
335
428
                    uint64_t u = load64_be(tmp + (9U - i - 1U) * 8U);
336
428
                    uint64_t x = u;
337
428
                    os[i] = x;);
338
428
}
339
340
static inline void
341
p521_make_prime(uint64_t *n)
342
4.11M
{
343
4.11M
    n[0U] = 0xffffffffffffffffULL;
344
4.11M
    n[1U] = 0xffffffffffffffffULL;
345
4.11M
    n[2U] = 0xffffffffffffffffULL;
346
4.11M
    n[3U] = 0xffffffffffffffffULL;
347
4.11M
    n[4U] = 0xffffffffffffffffULL;
348
4.11M
    n[5U] = 0xffffffffffffffffULL;
349
4.11M
    n[6U] = 0xffffffffffffffffULL;
350
4.11M
    n[7U] = 0xffffffffffffffffULL;
351
4.11M
    n[8U] = 0x1ffULL;
352
4.11M
}
353
354
static inline void
355
p521_make_order(uint64_t *n)
356
45.0k
{
357
45.0k
    n[0U] = 0xbb6fb71e91386409ULL;
358
45.0k
    n[1U] = 0x3bb5c9b8899c47aeULL;
359
45.0k
    n[2U] = 0x7fcc0148f709a5d0ULL;
360
45.0k
    n[3U] = 0x51868783bf2f966bULL;
361
45.0k
    n[4U] = 0xfffffffffffffffaULL;
362
45.0k
    n[5U] = 0xffffffffffffffffULL;
363
45.0k
    n[6U] = 0xffffffffffffffffULL;
364
45.0k
    n[7U] = 0xffffffffffffffffULL;
365
45.0k
    n[8U] = 0x1ffULL;
366
45.0k
}
367
368
static inline void
369
p521_make_a_coeff(uint64_t *a)
370
77
{
371
77
    a[0U] = 0xfe7fffffffffffffULL;
372
77
    a[1U] = 0xffffffffffffffffULL;
373
77
    a[2U] = 0xffffffffffffffffULL;
374
77
    a[3U] = 0xffffffffffffffffULL;
375
77
    a[4U] = 0xffffffffffffffffULL;
376
77
    a[5U] = 0xffffffffffffffffULL;
377
77
    a[6U] = 0xffffffffffffffffULL;
378
77
    a[7U] = 0xffffffffffffffffULL;
379
77
    a[8U] = 0x01ffULL;
380
77
}
381
382
static inline void
383
p521_make_b_coeff(uint64_t *b)
384
224k
{
385
224k
    b[0U] = 0x8014654fae586387ULL;
386
224k
    b[1U] = 0x78f7a28fea35a81fULL;
387
224k
    b[2U] = 0x839ab9efc41e961aULL;
388
224k
    b[3U] = 0xbd8b29605e9dd8dfULL;
389
224k
    b[4U] = 0xf0ab0c9ca8f63f49ULL;
390
224k
    b[5U] = 0xf9dc5a44c8c77884ULL;
391
224k
    b[6U] = 0x77516d392dccd98aULL;
392
224k
    b[7U] = 0x0fc94d10d05b42a0ULL;
393
224k
    b[8U] = 0x4dULL;
394
224k
}
395
396
static inline void
397
p521_make_g_x(uint64_t *n)
398
135
{
399
135
    n[0U] = 0xb331a16381adc101ULL;
400
135
    n[1U] = 0x4dfcbf3f18e172deULL;
401
135
    n[2U] = 0x6f19a459e0c2b521ULL;
402
135
    n[3U] = 0x947f0ee093d17fd4ULL;
403
135
    n[4U] = 0xdd50a5af3bf7f3acULL;
404
135
    n[5U] = 0x90fc1457b035a69eULL;
405
135
    n[6U] = 0x214e32409c829fdaULL;
406
135
    n[7U] = 0xe6cf1f65b311cadaULL;
407
135
    n[8U] = 0x74ULL;
408
135
}
409
410
static inline void
411
p521_make_g_y(uint64_t *n)
412
135
{
413
135
    n[0U] = 0x28460e4a5a9e268eULL;
414
135
    n[1U] = 0x20445f4a3b4fe8b3ULL;
415
135
    n[2U] = 0xb09a9e3843513961ULL;
416
135
    n[3U] = 0x2062a85c809fd683ULL;
417
135
    n[4U] = 0x164bf7394caf7a13ULL;
418
135
    n[5U] = 0x340bd7de8b939f33ULL;
419
135
    n[6U] = 0xeccc7aa224abcda2ULL;
420
135
    n[7U] = 0x022e452fda163e8dULL;
421
135
    n[8U] = 0x1e0ULL;
422
135
}
423
424
static inline void
425
p521_make_fmont_R2(uint64_t *n)
426
294
{
427
294
    n[0U] = 0x0ULL;
428
294
    n[1U] = 0x400000000000ULL;
429
294
    n[2U] = 0x0ULL;
430
294
    n[3U] = 0x0ULL;
431
294
    n[4U] = 0x0ULL;
432
294
    n[5U] = 0x0ULL;
433
294
    n[6U] = 0x0ULL;
434
294
    n[7U] = 0x0ULL;
435
294
    n[8U] = 0x0ULL;
436
294
}
437
438
static inline void
439
p521_make_fzero(uint64_t *n)
440
338
{
441
338
    memset(n, 0U, 9U * sizeof(uint64_t));
442
338
    n[0U] = 0ULL;
443
338
}
444
445
static inline void
446
p521_make_fone(uint64_t *n)
447
509
{
448
509
    n[0U] = 0x80000000000000ULL;
449
509
    n[1U] = 0x0ULL;
450
509
    n[2U] = 0x0ULL;
451
509
    n[3U] = 0x0ULL;
452
509
    n[4U] = 0x0ULL;
453
509
    n[5U] = 0x0ULL;
454
509
    n[6U] = 0x0ULL;
455
509
    n[7U] = 0x0ULL;
456
509
    n[8U] = 0x0ULL;
457
509
}
458
459
static inline void
460
p521_make_qone(uint64_t *f)
461
68
{
462
68
    f[0U] = 0xfb80000000000000ULL;
463
68
    f[1U] = 0x28a2482470b763cdULL;
464
68
    f[2U] = 0x17e2251b23bb31dcULL;
465
68
    f[3U] = 0xca4019ff5b847b2dULL;
466
68
    f[4U] = 0x2d73cbc3e206834ULL;
467
68
    f[5U] = 0x0ULL;
468
68
    f[6U] = 0x0ULL;
469
68
    f[7U] = 0x0ULL;
470
68
    f[8U] = 0x0ULL;
471
68
}
472
473
static inline void
474
fmont_reduction(uint64_t *res, uint64_t *x)
475
1.57M
{
476
1.57M
    uint64_t n[9U] = { 0U };
477
1.57M
    p521_make_prime(n);
478
1.57M
    uint64_t c0 = 0ULL;
479
1.57M
    KRML_MAYBE_FOR9(
480
1.57M
        i0,
481
1.57M
        0U,
482
1.57M
        9U,
483
1.57M
        1U,
484
1.57M
        uint64_t qj = 1ULL * x[i0];
485
1.57M
        uint64_t *res_j0 = x + i0;
486
1.57M
        uint64_t c = 0ULL;
487
1.57M
        KRML_MAYBE_FOR2(i,
488
1.57M
                        0U,
489
1.57M
                        2U,
490
1.57M
                        1U,
491
1.57M
                        uint64_t a_i = n[4U * i];
492
1.57M
                        uint64_t *res_i0 = res_j0 + 4U * i;
493
1.57M
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0);
494
1.57M
                        uint64_t a_i0 = n[4U * i + 1U];
495
1.57M
                        uint64_t *res_i1 = res_j0 + 4U * i + 1U;
496
1.57M
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1);
497
1.57M
                        uint64_t a_i1 = n[4U * i + 2U];
498
1.57M
                        uint64_t *res_i2 = res_j0 + 4U * i + 2U;
499
1.57M
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2);
500
1.57M
                        uint64_t a_i2 = n[4U * i + 3U];
501
1.57M
                        uint64_t *res_i = res_j0 + 4U * i + 3U;
502
1.57M
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i););
503
1.57M
        {
504
1.57M
            uint64_t a_i = n[8U];
505
1.57M
            uint64_t *res_i = res_j0 + 8U;
506
1.57M
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);
507
1.57M
        } uint64_t r = c;
508
1.57M
        uint64_t c1 = r;
509
1.57M
        uint64_t *resb = x + 9U + i0;
510
1.57M
        uint64_t res_j = x[9U + i0];
511
1.57M
        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb););
512
1.57M
    memcpy(res, x + 9U, 9U * sizeof(uint64_t));
513
1.57M
    uint64_t c00 = c0;
514
1.57M
    uint64_t tmp[9U] = { 0U };
515
1.57M
    uint64_t c = 0ULL;
516
1.57M
    KRML_MAYBE_FOR2(i,
517
1.57M
                    0U,
518
1.57M
                    2U,
519
1.57M
                    1U,
520
1.57M
                    uint64_t t1 = res[4U * i];
521
1.57M
                    uint64_t t20 = n[4U * i];
522
1.57M
                    uint64_t *res_i0 = tmp + 4U * i;
523
1.57M
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
524
1.57M
                    uint64_t t10 = res[4U * i + 1U];
525
1.57M
                    uint64_t t21 = n[4U * i + 1U];
526
1.57M
                    uint64_t *res_i1 = tmp + 4U * i + 1U;
527
1.57M
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
528
1.57M
                    uint64_t t11 = res[4U * i + 2U];
529
1.57M
                    uint64_t t22 = n[4U * i + 2U];
530
1.57M
                    uint64_t *res_i2 = tmp + 4U * i + 2U;
531
1.57M
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
532
1.57M
                    uint64_t t12 = res[4U * i + 3U];
533
1.57M
                    uint64_t t2 = n[4U * i + 3U];
534
1.57M
                    uint64_t *res_i = tmp + 4U * i + 3U;
535
1.57M
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i););
536
1.57M
    {
537
1.57M
        uint64_t t1 = res[8U];
538
1.57M
        uint64_t t2 = n[8U];
539
1.57M
        uint64_t *res_i = tmp + 8U;
540
1.57M
        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);
541
1.57M
    }
542
1.57M
    uint64_t c1 = c;
543
1.57M
    uint64_t c2 = c00 - c1;
544
1.57M
    KRML_MAYBE_FOR9(i,
545
1.57M
                    0U,
546
1.57M
                    9U,
547
1.57M
                    1U,
548
1.57M
                    uint64_t *os = res;
549
1.57M
                    uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]);
550
1.57M
                    os[i] = x1;);
551
1.57M
}
552
553
static inline void
554
qmont_reduction(uint64_t *res, uint64_t *x)
555
44.7k
{
556
44.7k
    uint64_t n[9U] = { 0U };
557
44.7k
    p521_make_order(n);
558
44.7k
    uint64_t c0 = 0ULL;
559
44.7k
    KRML_MAYBE_FOR9(
560
44.7k
        i0,
561
44.7k
        0U,
562
44.7k
        9U,
563
44.7k
        1U,
564
44.7k
        uint64_t qj = 2103001588584519111ULL * x[i0];
565
44.7k
        uint64_t *res_j0 = x + i0;
566
44.7k
        uint64_t c = 0ULL;
567
44.7k
        KRML_MAYBE_FOR2(i,
568
44.7k
                        0U,
569
44.7k
                        2U,
570
44.7k
                        1U,
571
44.7k
                        uint64_t a_i = n[4U * i];
572
44.7k
                        uint64_t *res_i0 = res_j0 + 4U * i;
573
44.7k
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0);
574
44.7k
                        uint64_t a_i0 = n[4U * i + 1U];
575
44.7k
                        uint64_t *res_i1 = res_j0 + 4U * i + 1U;
576
44.7k
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1);
577
44.7k
                        uint64_t a_i1 = n[4U * i + 2U];
578
44.7k
                        uint64_t *res_i2 = res_j0 + 4U * i + 2U;
579
44.7k
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2);
580
44.7k
                        uint64_t a_i2 = n[4U * i + 3U];
581
44.7k
                        uint64_t *res_i = res_j0 + 4U * i + 3U;
582
44.7k
                        c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i););
583
44.7k
        {
584
44.7k
            uint64_t a_i = n[8U];
585
44.7k
            uint64_t *res_i = res_j0 + 8U;
586
44.7k
            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);
587
44.7k
        } uint64_t r = c;
588
44.7k
        uint64_t c1 = r;
589
44.7k
        uint64_t *resb = x + 9U + i0;
590
44.7k
        uint64_t res_j = x[9U + i0];
591
44.7k
        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb););
592
44.7k
    memcpy(res, x + 9U, 9U * sizeof(uint64_t));
593
44.7k
    uint64_t c00 = c0;
594
44.7k
    uint64_t tmp[9U] = { 0U };
595
44.7k
    uint64_t c = 0ULL;
596
44.7k
    KRML_MAYBE_FOR2(i,
597
44.7k
                    0U,
598
44.7k
                    2U,
599
44.7k
                    1U,
600
44.7k
                    uint64_t t1 = res[4U * i];
601
44.7k
                    uint64_t t20 = n[4U * i];
602
44.7k
                    uint64_t *res_i0 = tmp + 4U * i;
603
44.7k
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
604
44.7k
                    uint64_t t10 = res[4U * i + 1U];
605
44.7k
                    uint64_t t21 = n[4U * i + 1U];
606
44.7k
                    uint64_t *res_i1 = tmp + 4U * i + 1U;
607
44.7k
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
608
44.7k
                    uint64_t t11 = res[4U * i + 2U];
609
44.7k
                    uint64_t t22 = n[4U * i + 2U];
610
44.7k
                    uint64_t *res_i2 = tmp + 4U * i + 2U;
611
44.7k
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
612
44.7k
                    uint64_t t12 = res[4U * i + 3U];
613
44.7k
                    uint64_t t2 = n[4U * i + 3U];
614
44.7k
                    uint64_t *res_i = tmp + 4U * i + 3U;
615
44.7k
                    c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i););
616
44.7k
    {
617
44.7k
        uint64_t t1 = res[8U];
618
44.7k
        uint64_t t2 = n[8U];
619
44.7k
        uint64_t *res_i = tmp + 8U;
620
44.7k
        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);
621
44.7k
    }
622
44.7k
    uint64_t c1 = c;
623
44.7k
    uint64_t c2 = c00 - c1;
624
44.7k
    KRML_MAYBE_FOR9(i,
625
44.7k
                    0U,
626
44.7k
                    9U,
627
44.7k
                    1U,
628
44.7k
                    uint64_t *os = res;
629
44.7k
                    uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]);
630
44.7k
                    os[i] = x1;);
631
44.7k
}
632
633
static inline uint64_t
634
bn_is_lt_prime_mask(uint64_t *f)
635
156
{
636
156
    uint64_t tmp[9U] = { 0U };
637
156
    p521_make_prime(tmp);
638
156
    uint64_t c = bn_sub(tmp, f, tmp);
639
156
    uint64_t m = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL);
640
156
    return m;
641
156
}
642
643
static inline void
644
fadd0(uint64_t *a, uint64_t *b, uint64_t *c)
645
1.79M
{
646
1.79M
    uint64_t n[9U] = { 0U };
647
1.79M
    p521_make_prime(n);
648
1.79M
    bn_add_mod(a, n, b, c);
649
1.79M
}
650
651
static inline void
652
fsub0(uint64_t *a, uint64_t *b, uint64_t *c)
653
743k
{
654
743k
    uint64_t n[9U] = { 0U };
655
743k
    p521_make_prime(n);
656
743k
    bn_sub_mod(a, n, b, c);
657
743k
}
658
659
static inline void
660
fmul0(uint64_t *a, uint64_t *b, uint64_t *c)
661
1.23M
{
662
1.23M
    uint64_t tmp[18U] = { 0U };
663
1.23M
    bn_mul(tmp, b, c);
664
1.23M
    fmont_reduction(a, tmp);
665
1.23M
}
666
667
static inline void
668
fsqr0(uint64_t *a, uint64_t *b)
669
339k
{
670
339k
    uint64_t tmp[18U] = { 0U };
671
339k
    bn_sqr(tmp, b);
672
339k
    fmont_reduction(a, tmp);
673
339k
}
674
675
static inline void
676
from_mont(uint64_t *a, uint64_t *b)
677
202
{
678
202
    uint64_t tmp[18U] = { 0U };
679
202
    memcpy(tmp, b, 9U * sizeof(uint64_t));
680
202
    fmont_reduction(a, tmp);
681
202
}
682
683
static inline void
684
to_mont(uint64_t *a, uint64_t *b)
685
294
{
686
294
    uint64_t r2modn[9U] = { 0U };
687
294
    p521_make_fmont_R2(r2modn);
688
294
    uint64_t tmp[18U] = { 0U };
689
294
    bn_mul(tmp, b, r2modn);
690
294
    fmont_reduction(a, tmp);
691
294
}
692
693
static inline void
694
p521_finv(uint64_t *res, uint64_t *a)
695
135
{
696
135
    uint64_t b[9U] = { 0U };
697
135
    b[0U] = 0xfffffffffffffffdULL;
698
135
    b[1U] = 0xffffffffffffffffULL;
699
135
    b[2U] = 0xffffffffffffffffULL;
700
135
    b[3U] = 0xffffffffffffffffULL;
701
135
    b[4U] = 0xffffffffffffffffULL;
702
135
    b[5U] = 0xffffffffffffffffULL;
703
135
    b[6U] = 0xffffffffffffffffULL;
704
135
    b[7U] = 0xffffffffffffffffULL;
705
135
    b[8U] = 0x1ffULL;
706
135
    uint64_t tmp[9U] = { 0U };
707
135
    memcpy(tmp, a, 9U * sizeof(uint64_t));
708
135
    uint64_t table[288U] = { 0U };
709
135
    uint64_t tmp1[9U] = { 0U };
710
135
    uint64_t *t0 = table;
711
135
    uint64_t *t1 = table + 9U;
712
135
    p521_make_fone(t0);
713
135
    memcpy(t1, tmp, 9U * sizeof(uint64_t));
714
135
    KRML_MAYBE_FOR15(i,
715
135
                     0U,
716
135
                     15U,
717
135
                     1U,
718
135
                     uint64_t *t11 = table + (i + 1U) * 9U;
719
135
                     fsqr0(tmp1, t11);
720
135
                     memcpy(table + (2U * i + 2U) * 9U, tmp1, 9U * sizeof(uint64_t));
721
135
                     uint64_t *t2 = table + (2U * i + 2U) * 9U;
722
135
                     fmul0(tmp1, tmp, t2);
723
135
                     memcpy(table + (2U * i + 3U) * 9U, tmp1, 9U * sizeof(uint64_t)););
724
135
    uint32_t i0 = 520U;
725
135
    uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, i0, 5U);
726
135
    memcpy(res, (uint64_t *)table, 9U * sizeof(uint64_t));
727
4.32k
    for (uint32_t i1 = 0U; i1 < 31U; i1++) {
728
4.18k
        uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U));
729
4.18k
        const uint64_t *res_j = table + (i1 + 1U) * 9U;
730
4.18k
        KRML_MAYBE_FOR9(i,
731
4.18k
                        0U,
732
4.18k
                        9U,
733
4.18k
                        1U,
734
4.18k
                        uint64_t *os = res;
735
4.18k
                        uint64_t x = (c & res_j[i]) | (~c & res[i]);
736
4.18k
                        os[i] = x;);
737
4.18k
    }
738
135
    uint64_t tmp10[9U] = { 0U };
739
14.1k
    for (uint32_t i1 = 0U; i1 < 104U; i1++) {
740
14.0k
        KRML_MAYBE_FOR5(i, 0U, 5U, 1U, fsqr0(res, res););
741
14.0k
        uint32_t k = 520U - 5U * i1 - 5U;
742
14.0k
        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, k, 5U);
743
14.0k
        memcpy(tmp10, (uint64_t *)table, 9U * sizeof(uint64_t));
744
449k
        for (uint32_t i2 = 0U; i2 < 31U; i2++) {
745
435k
            uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U));
746
435k
            const uint64_t *res_j = table + (i2 + 1U) * 9U;
747
435k
            KRML_MAYBE_FOR9(i,
748
435k
                            0U,
749
435k
                            9U,
750
435k
                            1U,
751
435k
                            uint64_t *os = tmp10;
752
435k
                            uint64_t x = (c & res_j[i]) | (~c & tmp10[i]);
753
435k
                            os[i] = x;);
754
435k
        }
755
14.0k
        fmul0(res, res, tmp10);
756
14.0k
    }
757
135
}
758
759
static inline void
760
p521_fsqrt(uint64_t *res, uint64_t *a)
761
0
{
762
0
    uint64_t b[9U] = { 0U };
763
0
    b[0U] = 0x0ULL;
764
0
    b[1U] = 0x0ULL;
765
0
    b[2U] = 0x0ULL;
766
0
    b[3U] = 0x0ULL;
767
0
    b[4U] = 0x0ULL;
768
0
    b[5U] = 0x0ULL;
769
0
    b[6U] = 0x0ULL;
770
0
    b[7U] = 0x0ULL;
771
0
    b[8U] = 0x80ULL;
772
0
    uint64_t tmp[9U] = { 0U };
773
0
    memcpy(tmp, a, 9U * sizeof(uint64_t));
774
0
    uint64_t table[288U] = { 0U };
775
0
    uint64_t tmp1[9U] = { 0U };
776
0
    uint64_t *t0 = table;
777
0
    uint64_t *t1 = table + 9U;
778
0
    p521_make_fone(t0);
779
0
    memcpy(t1, tmp, 9U * sizeof(uint64_t));
780
0
    KRML_MAYBE_FOR15(i,
781
0
                     0U,
782
0
                     15U,
783
0
                     1U,
784
0
                     uint64_t *t11 = table + (i + 1U) * 9U;
785
0
                     fsqr0(tmp1, t11);
786
0
                     memcpy(table + (2U * i + 2U) * 9U, tmp1, 9U * sizeof(uint64_t));
787
0
                     uint64_t *t2 = table + (2U * i + 2U) * 9U;
788
0
                     fmul0(tmp1, tmp, t2);
789
0
                     memcpy(table + (2U * i + 3U) * 9U, tmp1, 9U * sizeof(uint64_t)););
790
0
    uint32_t i0 = 520U;
791
0
    uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, i0, 5U);
792
0
    memcpy(res, (uint64_t *)table, 9U * sizeof(uint64_t));
793
0
    for (uint32_t i1 = 0U; i1 < 31U; i1++) {
794
0
        uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U));
795
0
        const uint64_t *res_j = table + (i1 + 1U) * 9U;
796
0
        KRML_MAYBE_FOR9(i,
797
0
                        0U,
798
0
                        9U,
799
0
                        1U,
800
0
                        uint64_t *os = res;
801
0
                        uint64_t x = (c & res_j[i]) | (~c & res[i]);
802
0
                        os[i] = x;);
803
0
    }
804
0
    uint64_t tmp10[9U] = { 0U };
805
0
    for (uint32_t i1 = 0U; i1 < 104U; i1++) {
806
0
        KRML_MAYBE_FOR5(i, 0U, 5U, 1U, fsqr0(res, res););
807
0
        uint32_t k = 520U - 5U * i1 - 5U;
808
0
        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, k, 5U);
809
0
        memcpy(tmp10, (uint64_t *)table, 9U * sizeof(uint64_t));
810
0
        for (uint32_t i2 = 0U; i2 < 31U; i2++) {
811
0
            uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U));
812
0
            const uint64_t *res_j = table + (i2 + 1U) * 9U;
813
0
            KRML_MAYBE_FOR9(i,
814
0
                            0U,
815
0
                            9U,
816
0
                            1U,
817
0
                            uint64_t *os = tmp10;
818
0
                            uint64_t x = (c & res_j[i]) | (~c & tmp10[i]);
819
0
                            os[i] = x;);
820
0
        }
821
0
        fmul0(res, res, tmp10);
822
0
    }
823
0
}
824
825
static inline uint64_t
826
load_qelem_conditional(uint64_t *a, uint8_t *b)
827
135
{
828
135
    bn_from_bytes_be(a, b);
829
135
    uint64_t tmp[9U] = { 0U };
830
135
    p521_make_order(tmp);
831
135
    uint64_t c = bn_sub(tmp, a, tmp);
832
135
    uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL);
833
135
    uint64_t bn_zero[9U] = { 0U };
834
135
    uint64_t res = bn_is_eq_mask(a, bn_zero);
835
135
    uint64_t is_eq_zero = res;
836
135
    uint64_t is_b_valid = is_lt_order & ~is_eq_zero;
837
135
    uint64_t oneq[9U] = { 0U };
838
135
    memset(oneq, 0U, 9U * sizeof(uint64_t));
839
135
    oneq[0U] = 1ULL;
840
135
    KRML_MAYBE_FOR9(i,
841
135
                    0U,
842
135
                    9U,
843
135
                    1U,
844
135
                    uint64_t *os = a;
845
135
                    uint64_t uu____0 = oneq[i];
846
135
                    uint64_t x = uu____0 ^ (is_b_valid & (a[i] ^ uu____0));
847
135
                    os[i] = x;);
848
135
    return is_b_valid;
849
135
}
850
851
static inline void
852
qmod_short(uint64_t *a, uint64_t *b)
853
136
{
854
136
    uint64_t tmp[9U] = { 0U };
855
136
    p521_make_order(tmp);
856
136
    uint64_t c = bn_sub(tmp, b, tmp);
857
136
    bn_cmovznz(a, c, tmp, b);
858
136
}
859
860
static inline void
861
qadd(uint64_t *a, uint64_t *b, uint64_t *c)
862
34
{
863
34
    uint64_t n[9U] = { 0U };
864
34
    p521_make_order(n);
865
34
    bn_add_mod(a, n, b, c);
866
34
}
867
868
static inline void
869
qmul(uint64_t *a, uint64_t *b, uint64_t *c)
870
8.22k
{
871
8.22k
    uint64_t tmp[18U] = { 0U };
872
8.22k
    bn_mul(tmp, b, c);
873
8.22k
    qmont_reduction(a, tmp);
874
8.22k
}
875
876
static inline void
877
qsqr(uint64_t *a, uint64_t *b)
878
36.3k
{
879
36.3k
    uint64_t tmp[18U] = { 0U };
880
36.3k
    bn_sqr(tmp, b);
881
36.3k
    qmont_reduction(a, tmp);
882
36.3k
}
883
884
static inline void
885
from_qmont(uint64_t *a, uint64_t *b)
886
102
{
887
102
    uint64_t tmp[18U] = { 0U };
888
102
    memcpy(tmp, b, 9U * sizeof(uint64_t));
889
102
    qmont_reduction(a, tmp);
890
102
}
891
892
static inline void
893
p521_qinv(uint64_t *res, uint64_t *a)
894
68
{
895
68
    uint64_t b[9U] = { 0U };
896
68
    b[0U] = 0xbb6fb71e91386407ULL;
897
68
    b[1U] = 0x3bb5c9b8899c47aeULL;
898
68
    b[2U] = 0x7fcc0148f709a5d0ULL;
899
68
    b[3U] = 0x51868783bf2f966bULL;
900
68
    b[4U] = 0xfffffffffffffffaULL;
901
68
    b[5U] = 0xffffffffffffffffULL;
902
68
    b[6U] = 0xffffffffffffffffULL;
903
68
    b[7U] = 0xffffffffffffffffULL;
904
68
    b[8U] = 0x1ffULL;
905
68
    uint64_t tmp[9U] = { 0U };
906
68
    memcpy(tmp, a, 9U * sizeof(uint64_t));
907
68
    uint64_t table[288U] = { 0U };
908
68
    uint64_t tmp1[9U] = { 0U };
909
68
    uint64_t *t0 = table;
910
68
    uint64_t *t1 = table + 9U;
911
68
    p521_make_qone(t0);
912
68
    memcpy(t1, tmp, 9U * sizeof(uint64_t));
913
68
    KRML_MAYBE_FOR15(i,
914
68
                     0U,
915
68
                     15U,
916
68
                     1U,
917
68
                     uint64_t *t11 = table + (i + 1U) * 9U;
918
68
                     qsqr(tmp1, t11);
919
68
                     memcpy(table + (2U * i + 2U) * 9U, tmp1, 9U * sizeof(uint64_t));
920
68
                     uint64_t *t2 = table + (2U * i + 2U) * 9U;
921
68
                     qmul(tmp1, tmp, t2);
922
68
                     memcpy(table + (2U * i + 3U) * 9U, tmp1, 9U * sizeof(uint64_t)););
923
68
    uint32_t i0 = 520U;
924
68
    uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, i0, 5U);
925
68
    memcpy(res, (uint64_t *)table, 9U * sizeof(uint64_t));
926
2.17k
    for (uint32_t i1 = 0U; i1 < 31U; i1++) {
927
2.10k
        uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U));
928
2.10k
        const uint64_t *res_j = table + (i1 + 1U) * 9U;
929
2.10k
        KRML_MAYBE_FOR9(i,
930
2.10k
                        0U,
931
2.10k
                        9U,
932
2.10k
                        1U,
933
2.10k
                        uint64_t *os = res;
934
2.10k
                        uint64_t x = (c & res_j[i]) | (~c & res[i]);
935
2.10k
                        os[i] = x;);
936
2.10k
    }
937
68
    uint64_t tmp10[9U] = { 0U };
938
7.14k
    for (uint32_t i1 = 0U; i1 < 104U; i1++) {
939
7.07k
        KRML_MAYBE_FOR5(i, 0U, 5U, 1U, qsqr(res, res););
940
7.07k
        uint32_t k = 520U - 5U * i1 - 5U;
941
7.07k
        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(9U, b, k, 5U);
942
7.07k
        memcpy(tmp10, (uint64_t *)table, 9U * sizeof(uint64_t));
943
226k
        for (uint32_t i2 = 0U; i2 < 31U; i2++) {
944
219k
            uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U));
945
219k
            const uint64_t *res_j = table + (i2 + 1U) * 9U;
946
219k
            KRML_MAYBE_FOR9(i,
947
219k
                            0U,
948
219k
                            9U,
949
219k
                            1U,
950
219k
                            uint64_t *os = tmp10;
951
219k
                            uint64_t x = (c & res_j[i]) | (~c & tmp10[i]);
952
219k
                            os[i] = x;);
953
219k
        }
954
7.07k
        qmul(res, res, tmp10);
955
7.07k
    }
956
68
}
957
958
static inline void
959
point_add(uint64_t *x, uint64_t *y, uint64_t *xy)
960
23.1k
{
961
23.1k
    uint64_t tmp[81U] = { 0U };
962
23.1k
    uint64_t *t0 = tmp;
963
23.1k
    uint64_t *t1 = tmp + 54U;
964
23.1k
    uint64_t *x3 = t1;
965
23.1k
    uint64_t *y3 = t1 + 9U;
966
23.1k
    uint64_t *z3 = t1 + 18U;
967
23.1k
    uint64_t *t01 = t0;
968
23.1k
    uint64_t *t11 = t0 + 9U;
969
23.1k
    uint64_t *t2 = t0 + 18U;
970
23.1k
    uint64_t *t3 = t0 + 27U;
971
23.1k
    uint64_t *t4 = t0 + 36U;
972
23.1k
    uint64_t *t5 = t0 + 45U;
973
23.1k
    uint64_t *x1 = x;
974
23.1k
    uint64_t *y1 = x + 9U;
975
23.1k
    uint64_t *z10 = x + 18U;
976
23.1k
    uint64_t *x20 = y;
977
23.1k
    uint64_t *y20 = y + 9U;
978
23.1k
    uint64_t *z20 = y + 18U;
979
23.1k
    fmul0(t01, x1, x20);
980
23.1k
    fmul0(t11, y1, y20);
981
23.1k
    fmul0(t2, z10, z20);
982
23.1k
    fadd0(t3, x1, y1);
983
23.1k
    fadd0(t4, x20, y20);
984
23.1k
    fmul0(t3, t3, t4);
985
23.1k
    fadd0(t4, t01, t11);
986
23.1k
    uint64_t *y10 = x + 9U;
987
23.1k
    uint64_t *z11 = x + 18U;
988
23.1k
    uint64_t *y2 = y + 9U;
989
23.1k
    uint64_t *z21 = y + 18U;
990
23.1k
    fsub0(t3, t3, t4);
991
23.1k
    fadd0(t4, y10, z11);
992
23.1k
    fadd0(t5, y2, z21);
993
23.1k
    fmul0(t4, t4, t5);
994
23.1k
    fadd0(t5, t11, t2);
995
23.1k
    fsub0(t4, t4, t5);
996
23.1k
    uint64_t *x10 = x;
997
23.1k
    uint64_t *z1 = x + 18U;
998
23.1k
    uint64_t *x2 = y;
999
23.1k
    uint64_t *z2 = y + 18U;
1000
23.1k
    fadd0(x3, x10, z1);
1001
23.1k
    fadd0(y3, x2, z2);
1002
23.1k
    fmul0(x3, x3, y3);
1003
23.1k
    fadd0(y3, t01, t2);
1004
23.1k
    fsub0(y3, x3, y3);
1005
23.1k
    uint64_t b_coeff[9U] = { 0U };
1006
23.1k
    p521_make_b_coeff(b_coeff);
1007
23.1k
    fmul0(z3, b_coeff, t2);
1008
23.1k
    fsub0(x3, y3, z3);
1009
23.1k
    fadd0(z3, x3, x3);
1010
23.1k
    fadd0(x3, x3, z3);
1011
23.1k
    fsub0(z3, t11, x3);
1012
23.1k
    fadd0(x3, t11, x3);
1013
23.1k
    uint64_t b_coeff0[9U] = { 0U };
1014
23.1k
    p521_make_b_coeff(b_coeff0);
1015
23.1k
    fmul0(y3, b_coeff0, y3);
1016
23.1k
    fadd0(t11, t2, t2);
1017
23.1k
    fadd0(t2, t11, t2);
1018
23.1k
    fsub0(y3, y3, t2);
1019
23.1k
    fsub0(y3, y3, t01);
1020
23.1k
    fadd0(t11, y3, y3);
1021
23.1k
    fadd0(y3, t11, y3);
1022
23.1k
    fadd0(t11, t01, t01);
1023
23.1k
    fadd0(t01, t11, t01);
1024
23.1k
    fsub0(t01, t01, t2);
1025
23.1k
    fmul0(t11, t4, y3);
1026
23.1k
    fmul0(t2, t01, y3);
1027
23.1k
    fmul0(y3, x3, z3);
1028
23.1k
    fadd0(y3, y3, t2);
1029
23.1k
    fmul0(x3, t3, x3);
1030
23.1k
    fsub0(x3, x3, t11);
1031
23.1k
    fmul0(z3, t4, z3);
1032
23.1k
    fmul0(t11, t3, t01);
1033
23.1k
    fadd0(z3, z3, t11);
1034
23.1k
    memcpy(xy, t1, 27U * sizeof(uint64_t));
1035
23.1k
}
1036
1037
static inline void
1038
point_double(uint64_t *x, uint64_t *xx)
1039
89.0k
{
1040
89.0k
    uint64_t tmp[45U] = { 0U };
1041
89.0k
    uint64_t *x1 = x;
1042
89.0k
    uint64_t *z = x + 18U;
1043
89.0k
    uint64_t *x3 = xx;
1044
89.0k
    uint64_t *y3 = xx + 9U;
1045
89.0k
    uint64_t *z3 = xx + 18U;
1046
89.0k
    uint64_t *t0 = tmp;
1047
89.0k
    uint64_t *t1 = tmp + 9U;
1048
89.0k
    uint64_t *t2 = tmp + 18U;
1049
89.0k
    uint64_t *t3 = tmp + 27U;
1050
89.0k
    uint64_t *t4 = tmp + 36U;
1051
89.0k
    uint64_t *x2 = x;
1052
89.0k
    uint64_t *y = x + 9U;
1053
89.0k
    uint64_t *z1 = x + 18U;
1054
89.0k
    fsqr0(t0, x2);
1055
89.0k
    fsqr0(t1, y);
1056
89.0k
    fsqr0(t2, z1);
1057
89.0k
    fmul0(t3, x2, y);
1058
89.0k
    fadd0(t3, t3, t3);
1059
89.0k
    fmul0(t4, y, z1);
1060
89.0k
    fmul0(z3, x1, z);
1061
89.0k
    fadd0(z3, z3, z3);
1062
89.0k
    uint64_t b_coeff[9U] = { 0U };
1063
89.0k
    p521_make_b_coeff(b_coeff);
1064
89.0k
    fmul0(y3, b_coeff, t2);
1065
89.0k
    fsub0(y3, y3, z3);
1066
89.0k
    fadd0(x3, y3, y3);
1067
89.0k
    fadd0(y3, x3, y3);
1068
89.0k
    fsub0(x3, t1, y3);
1069
89.0k
    fadd0(y3, t1, y3);
1070
89.0k
    fmul0(y3, x3, y3);
1071
89.0k
    fmul0(x3, x3, t3);
1072
89.0k
    fadd0(t3, t2, t2);
1073
89.0k
    fadd0(t2, t2, t3);
1074
89.0k
    uint64_t b_coeff0[9U] = { 0U };
1075
89.0k
    p521_make_b_coeff(b_coeff0);
1076
89.0k
    fmul0(z3, b_coeff0, z3);
1077
89.0k
    fsub0(z3, z3, t2);
1078
89.0k
    fsub0(z3, z3, t0);
1079
89.0k
    fadd0(t3, z3, z3);
1080
89.0k
    fadd0(z3, z3, t3);
1081
89.0k
    fadd0(t3, t0, t0);
1082
89.0k
    fadd0(t0, t3, t0);
1083
89.0k
    fsub0(t0, t0, t2);
1084
89.0k
    fmul0(t0, t0, z3);
1085
89.0k
    fadd0(y3, y3, t0);
1086
89.0k
    fadd0(t0, t4, t4);
1087
89.0k
    fmul0(z3, t0, z3);
1088
89.0k
    fsub0(x3, x3, z3);
1089
89.0k
    fmul0(z3, t0, t1);
1090
89.0k
    fadd0(z3, z3, z3);
1091
89.0k
    fadd0(z3, z3, z3);
1092
89.0k
}
1093
1094
static inline void
1095
point_zero(uint64_t *one)
1096
169
{
1097
169
    uint64_t *x = one;
1098
169
    uint64_t *y = one + 9U;
1099
169
    uint64_t *z = one + 18U;
1100
169
    p521_make_fzero(x);
1101
169
    p521_make_fone(y);
1102
169
    p521_make_fzero(z);
1103
169
}
1104
1105
static inline void
1106
point_mul(uint64_t *res, uint64_t *scalar, uint64_t *p)
1107
169
{
1108
169
    uint64_t table[432U] = { 0U };
1109
169
    uint64_t tmp[27U] = { 0U };
1110
169
    uint64_t *t0 = table;
1111
169
    uint64_t *t1 = table + 27U;
1112
169
    point_zero(t0);
1113
169
    memcpy(t1, p, 27U * sizeof(uint64_t));
1114
169
    KRML_MAYBE_FOR7(i,
1115
169
                    0U,
1116
169
                    7U,
1117
169
                    1U,
1118
169
                    uint64_t *t11 = table + (i + 1U) * 27U;
1119
169
                    point_double(t11, tmp);
1120
169
                    memcpy(table + (2U * i + 2U) * 27U, tmp, 27U * sizeof(uint64_t));
1121
169
                    uint64_t *t2 = table + (2U * i + 2U) * 27U;
1122
169
                    point_add(p, t2, tmp);
1123
169
                    memcpy(table + (2U * i + 3U) * 27U, tmp, 27U * sizeof(uint64_t)););
1124
169
    uint32_t i0 = 520U;
1125
169
    uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(9U, scalar, i0, 4U);
1126
169
    memcpy(res, (uint64_t *)table, 27U * sizeof(uint64_t));
1127
169
    KRML_MAYBE_FOR15(
1128
169
        i1,
1129
169
        0U,
1130
169
        15U,
1131
169
        1U,
1132
169
        uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U));
1133
169
        const uint64_t *res_j = table + (i1 + 1U) * 27U;
1134
169
        for (uint32_t i = 0U; i < 27U; i++) {
1135
169
            uint64_t *os = res;
1136
169
            uint64_t x = (c & res_j[i]) | (~c & res[i]);
1137
169
            os[i] = x;
1138
169
        });
1139
169
    uint64_t tmp0[27U] = { 0U };
1140
22.1k
    for (uint32_t i1 = 0U; i1 < 130U; i1++) {
1141
21.9k
        KRML_MAYBE_FOR4(i, 0U, 4U, 1U, point_double(res, res););
1142
21.9k
        uint32_t k = 520U - 4U * i1 - 4U;
1143
21.9k
        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(9U, scalar, k, 4U);
1144
21.9k
        memcpy(tmp0, (uint64_t *)table, 27U * sizeof(uint64_t));
1145
21.9k
        KRML_MAYBE_FOR15(
1146
21.9k
            i2,
1147
21.9k
            0U,
1148
21.9k
            15U,
1149
21.9k
            1U,
1150
21.9k
            uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U));
1151
21.9k
            const uint64_t *res_j = table + (i2 + 1U) * 27U;
1152
21.9k
            for (uint32_t i = 0U; i < 27U; i++) {
1153
21.9k
                uint64_t *os = tmp0;
1154
21.9k
                uint64_t x = (c & res_j[i]) | (~c & tmp0[i]);
1155
21.9k
                os[i] = x;
1156
21.9k
            });
1157
21.9k
        point_add(res, tmp0, res);
1158
21.9k
    }
1159
169
}
1160
1161
static inline void
1162
point_mul_g(uint64_t *res, uint64_t *scalar)
1163
135
{
1164
135
    uint64_t g[27U] = { 0U };
1165
135
    uint64_t *x = g;
1166
135
    uint64_t *y = g + 9U;
1167
135
    uint64_t *z = g + 18U;
1168
135
    p521_make_g_x(x);
1169
135
    p521_make_g_y(y);
1170
135
    p521_make_fone(z);
1171
135
    point_mul(res, scalar, g);
1172
135
}
1173
1174
static inline void
1175
point_mul_double_g(uint64_t *res, uint64_t *scalar1, uint64_t *scalar2, uint64_t *p)
1176
34
{
1177
34
    uint64_t tmp[27U] = { 0U };
1178
34
    point_mul_g(tmp, scalar1);
1179
34
    point_mul(res, scalar2, p);
1180
34
    point_add(res, tmp, res);
1181
34
}
1182
1183
static inline bool
1184
ecdsa_sign_msg_as_qelem(
1185
    uint8_t *signature,
1186
    uint64_t *m_q,
1187
    uint8_t *private_key,
1188
    uint8_t *nonce)
1189
34
{
1190
34
    uint64_t rsdk_q[36U] = { 0U };
1191
34
    uint64_t *r_q = rsdk_q;
1192
34
    uint64_t *s_q = rsdk_q + 9U;
1193
34
    uint64_t *d_a = rsdk_q + 18U;
1194
34
    uint64_t *k_q = rsdk_q + 27U;
1195
34
    uint64_t is_sk_valid = load_qelem_conditional(d_a, private_key);
1196
34
    uint64_t is_nonce_valid = load_qelem_conditional(k_q, nonce);
1197
34
    uint64_t are_sk_nonce_valid = is_sk_valid & is_nonce_valid;
1198
34
    uint64_t p[27U] = { 0U };
1199
34
    point_mul_g(p, k_q);
1200
34
    uint64_t zinv[9U] = { 0U };
1201
34
    uint64_t *px = p;
1202
34
    uint64_t *pz = p + 18U;
1203
34
    p521_finv(zinv, pz);
1204
34
    fmul0(r_q, px, zinv);
1205
34
    from_mont(r_q, r_q);
1206
34
    qmod_short(r_q, r_q);
1207
34
    uint64_t kinv[9U] = { 0U };
1208
34
    p521_qinv(kinv, k_q);
1209
34
    qmul(s_q, r_q, d_a);
1210
34
    from_qmont(m_q, m_q);
1211
34
    qadd(s_q, m_q, s_q);
1212
34
    qmul(s_q, kinv, s_q);
1213
34
    bn_to_bytes_be(signature, r_q);
1214
34
    bn_to_bytes_be(signature + 66U, s_q);
1215
34
    uint64_t bn_zero0[9U] = { 0U };
1216
34
    uint64_t res = bn_is_eq_mask(r_q, bn_zero0);
1217
34
    uint64_t is_r_zero = res;
1218
34
    uint64_t bn_zero[9U] = { 0U };
1219
34
    uint64_t res0 = bn_is_eq_mask(s_q, bn_zero);
1220
34
    uint64_t is_s_zero = res0;
1221
34
    uint64_t m = are_sk_nonce_valid & (~is_r_zero & ~is_s_zero);
1222
34
    bool res1 = m == 0xFFFFFFFFFFFFFFFFULL;
1223
34
    return res1;
1224
34
}
1225
1226
static inline bool
1227
ecdsa_verify_msg_as_qelem(
1228
    uint64_t *m_q,
1229
    uint8_t *public_key,
1230
    uint8_t *signature_r,
1231
    uint8_t *signature_s)
1232
34
{
1233
34
    uint64_t tmp[63U] = { 0U };
1234
34
    uint64_t *pk = tmp;
1235
34
    uint64_t *r_q = tmp + 27U;
1236
34
    uint64_t *s_q = tmp + 36U;
1237
34
    uint64_t *u1 = tmp + 45U;
1238
34
    uint64_t *u2 = tmp + 54U;
1239
34
    uint64_t p_aff[18U] = { 0U };
1240
34
    uint8_t *p_x = public_key;
1241
34
    uint8_t *p_y = public_key + 66U;
1242
34
    uint64_t *bn_p_x = p_aff;
1243
34
    uint64_t *bn_p_y = p_aff + 9U;
1244
34
    bn_from_bytes_be(bn_p_x, p_x);
1245
34
    bn_from_bytes_be(bn_p_y, p_y);
1246
34
    uint64_t *px0 = p_aff;
1247
34
    uint64_t *py0 = p_aff + 9U;
1248
34
    uint64_t lessX = bn_is_lt_prime_mask(px0);
1249
34
    uint64_t lessY = bn_is_lt_prime_mask(py0);
1250
34
    uint64_t res0 = lessX & lessY;
1251
34
    bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL;
1252
34
    bool res;
1253
34
    if (!is_xy_valid) {
1254
0
        res = false;
1255
34
    } else {
1256
34
        uint64_t rp[9U] = { 0U };
1257
34
        uint64_t tx[9U] = { 0U };
1258
34
        uint64_t ty[9U] = { 0U };
1259
34
        uint64_t *px = p_aff;
1260
34
        uint64_t *py = p_aff + 9U;
1261
34
        to_mont(tx, px);
1262
34
        to_mont(ty, py);
1263
34
        uint64_t tmp1[9U] = { 0U };
1264
34
        fsqr0(rp, tx);
1265
34
        fmul0(rp, rp, tx);
1266
34
        p521_make_a_coeff(tmp1);
1267
34
        fmul0(tmp1, tmp1, tx);
1268
34
        fadd0(rp, tmp1, rp);
1269
34
        p521_make_b_coeff(tmp1);
1270
34
        fadd0(rp, tmp1, rp);
1271
34
        fsqr0(ty, ty);
1272
34
        uint64_t r = bn_is_eq_mask(ty, rp);
1273
34
        uint64_t r0 = r;
1274
34
        bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL;
1275
34
        res = r1;
1276
34
    }
1277
34
    if (res) {
1278
34
        uint64_t *px = p_aff;
1279
34
        uint64_t *py = p_aff + 9U;
1280
34
        uint64_t *rx = pk;
1281
34
        uint64_t *ry = pk + 9U;
1282
34
        uint64_t *rz = pk + 18U;
1283
34
        to_mont(rx, px);
1284
34
        to_mont(ry, py);
1285
34
        p521_make_fone(rz);
1286
34
    }
1287
34
    bool is_pk_valid = res;
1288
34
    bn_from_bytes_be(r_q, signature_r);
1289
34
    bn_from_bytes_be(s_q, signature_s);
1290
34
    uint64_t tmp10[9U] = { 0U };
1291
34
    p521_make_order(tmp10);
1292
34
    uint64_t c = bn_sub(tmp10, r_q, tmp10);
1293
34
    uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL);
1294
34
    uint64_t bn_zero0[9U] = { 0U };
1295
34
    uint64_t res1 = bn_is_eq_mask(r_q, bn_zero0);
1296
34
    uint64_t is_eq_zero = res1;
1297
34
    uint64_t is_r_valid = is_lt_order & ~is_eq_zero;
1298
34
    uint64_t tmp11[9U] = { 0U };
1299
34
    p521_make_order(tmp11);
1300
34
    uint64_t c0 = bn_sub(tmp11, s_q, tmp11);
1301
34
    uint64_t is_lt_order0 = FStar_UInt64_gte_mask(c0, 0ULL) & ~FStar_UInt64_eq_mask(c0, 0ULL);
1302
34
    uint64_t bn_zero1[9U] = { 0U };
1303
34
    uint64_t res2 = bn_is_eq_mask(s_q, bn_zero1);
1304
34
    uint64_t is_eq_zero0 = res2;
1305
34
    uint64_t is_s_valid = is_lt_order0 & ~is_eq_zero0;
1306
34
    bool is_rs_valid = is_r_valid == 0xFFFFFFFFFFFFFFFFULL && is_s_valid == 0xFFFFFFFFFFFFFFFFULL;
1307
34
    if (!(is_pk_valid && is_rs_valid)) {
1308
0
        return false;
1309
0
    }
1310
34
    uint64_t sinv[9U] = { 0U };
1311
34
    p521_qinv(sinv, s_q);
1312
34
    uint64_t tmp1[9U] = { 0U };
1313
34
    from_qmont(tmp1, m_q);
1314
34
    qmul(u1, sinv, tmp1);
1315
34
    uint64_t tmp12[9U] = { 0U };
1316
34
    from_qmont(tmp12, r_q);
1317
34
    qmul(u2, sinv, tmp12);
1318
34
    uint64_t res3[27U] = { 0U };
1319
34
    point_mul_double_g(res3, u1, u2, pk);
1320
34
    uint64_t *pz0 = res3 + 18U;
1321
34
    uint64_t bn_zero[9U] = { 0U };
1322
34
    uint64_t res10 = bn_is_eq_mask(pz0, bn_zero);
1323
34
    uint64_t m = res10;
1324
34
    if (m == 0xFFFFFFFFFFFFFFFFULL) {
1325
0
        return false;
1326
0
    }
1327
34
    uint64_t x[9U] = { 0U };
1328
34
    uint64_t zinv[9U] = { 0U };
1329
34
    uint64_t *px = res3;
1330
34
    uint64_t *pz = res3 + 18U;
1331
34
    p521_finv(zinv, pz);
1332
34
    fmul0(x, px, zinv);
1333
34
    from_mont(x, x);
1334
34
    qmod_short(x, x);
1335
34
    uint64_t m0 = bn_is_eq_mask(x, r_q);
1336
34
    bool res11 = m0 == 0xFFFFFFFFFFFFFFFFULL;
1337
34
    return res11;
1338
34
}
1339
1340
/*******************************************************************************
1341
1342
 Verified C library for ECDSA and ECDH functions over the P-521 NIST curve.
1343
1344
 This module implements signing and verification, key validation, conversions
1345
 between various point representations, and ECDH key agreement.
1346
1347
*******************************************************************************/
1348
1349
/*****************/
1350
/* ECDSA signing */
1351
/*****************/
1352
1353
/**
1354
Create an ECDSA signature WITHOUT hashing first.
1355
1356
  This function is intended to receive a hash of the input.
1357
  For convenience, we recommend using one of the hash-and-sign combined functions above.
1358
1359
  The argument `msg` MUST be at least 66 bytes (i.e. `msg_len >= 66`).
1360
1361
  NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs
1362
  smaller than 66 bytes. These libraries left-pad the input with enough zeroes to
1363
  reach the minimum 66 byte size. Clients who need behavior identical to OpenSSL
1364
  need to perform the left-padding themselves.
1365
1366
  The function returns `true` for successful creation of an ECDSA signature and `false` otherwise.
1367
1368
  The outparam `signature` (R || S) points to 132 bytes of valid memory, i.e., uint8_t[132].
1369
  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
1370
  The arguments `private_key` and `nonce` point to 66 bytes of valid memory, i.e., uint8_t[66].
1371
1372
  The function also checks whether `private_key` and `nonce` are valid values:
1373
    • 0 < `private_key` < the order of the curve
1374
    • 0 < `nonce` < the order of the curve
1375
*/
1376
bool
1377
Hacl_P521_ecdsa_sign_p521_without_hash(
1378
    uint8_t *signature,
1379
    uint32_t msg_len,
1380
    uint8_t *msg,
1381
    uint8_t *private_key,
1382
    uint8_t *nonce)
1383
34
{
1384
34
    uint64_t m_q[9U] = { 0U };
1385
34
    uint8_t mHash[66U] = { 0U };
1386
34
    memcpy(mHash, msg, 66U * sizeof(uint8_t));
1387
34
    KRML_MAYBE_UNUSED_VAR(msg_len);
1388
34
    bn_from_bytes_be(m_q, mHash);
1389
34
    qmod_short(m_q, m_q);
1390
34
    bool res = ecdsa_sign_msg_as_qelem(signature, m_q, private_key, nonce);
1391
34
    return res;
1392
34
}
1393
1394
/**********************/
1395
/* ECDSA verification */
1396
/**********************/
1397
1398
/**
1399
Verify an ECDSA signature WITHOUT hashing first.
1400
1401
  This function is intended to receive a hash of the input.
1402
  For convenience, we recommend using one of the hash-and-verify combined functions above.
1403
1404
  The argument `msg` MUST be at least 66 bytes (i.e. `msg_len >= 66`).
1405
1406
  The function returns `true` if the signature is valid and `false` otherwise.
1407
1408
  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
1409
  The argument `public_key` (x || y) points to 132 bytes of valid memory, i.e., uint8_t[132].
1410
  The arguments `signature_r` and `signature_s` point to 66 bytes of valid memory, i.e., uint8_t[66].
1411
1412
  The function also checks whether `public_key` is valid
1413
*/
1414
bool
1415
Hacl_P521_ecdsa_verif_without_hash(
1416
    uint32_t msg_len,
1417
    uint8_t *msg,
1418
    uint8_t *public_key,
1419
    uint8_t *signature_r,
1420
    uint8_t *signature_s)
1421
34
{
1422
34
    uint64_t m_q[9U] = { 0U };
1423
34
    uint8_t mHash[66U] = { 0U };
1424
34
    memcpy(mHash, msg, 66U * sizeof(uint8_t));
1425
34
    KRML_MAYBE_UNUSED_VAR(msg_len);
1426
34
    bn_from_bytes_be(m_q, mHash);
1427
34
    qmod_short(m_q, m_q);
1428
34
    bool res = ecdsa_verify_msg_as_qelem(m_q, public_key, signature_r, signature_s);
1429
34
    return res;
1430
34
}
1431
1432
/******************/
1433
/* Key validation */
1434
/******************/
1435
1436
/**
1437
Public key validation.
1438
1439
  The function returns `true` if a public key is valid and `false` otherwise.
1440
1441
  The argument `public_key` points to 132 bytes of valid memory, i.e., uint8_t[132].
1442
1443
  The public key (x || y) is valid (with respect to SP 800-56A):
1444
    • the public key is not the “point at infinity”, represented as O.
1445
    • the affine x and y coordinates of the point represented by the public key are
1446
      in the range [0, p – 1] where p is the prime defining the finite field.
1447
    • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation.
1448
  The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/
1449
*/
1450
bool
1451
Hacl_P521_validate_public_key(uint8_t *public_key)
1452
44
{
1453
44
    uint64_t point_jac[27U] = { 0U };
1454
44
    uint64_t p_aff[18U] = { 0U };
1455
44
    uint8_t *p_x = public_key;
1456
44
    uint8_t *p_y = public_key + 66U;
1457
44
    uint64_t *bn_p_x = p_aff;
1458
44
    uint64_t *bn_p_y = p_aff + 9U;
1459
44
    bn_from_bytes_be(bn_p_x, p_x);
1460
44
    bn_from_bytes_be(bn_p_y, p_y);
1461
44
    uint64_t *px0 = p_aff;
1462
44
    uint64_t *py0 = p_aff + 9U;
1463
44
    uint64_t lessX = bn_is_lt_prime_mask(px0);
1464
44
    uint64_t lessY = bn_is_lt_prime_mask(py0);
1465
44
    uint64_t res0 = lessX & lessY;
1466
44
    bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL;
1467
44
    bool res;
1468
44
    if (!is_xy_valid) {
1469
1
        res = false;
1470
43
    } else {
1471
43
        uint64_t rp[9U] = { 0U };
1472
43
        uint64_t tx[9U] = { 0U };
1473
43
        uint64_t ty[9U] = { 0U };
1474
43
        uint64_t *px = p_aff;
1475
43
        uint64_t *py = p_aff + 9U;
1476
43
        to_mont(tx, px);
1477
43
        to_mont(ty, py);
1478
43
        uint64_t tmp[9U] = { 0U };
1479
43
        fsqr0(rp, tx);
1480
43
        fmul0(rp, rp, tx);
1481
43
        p521_make_a_coeff(tmp);
1482
43
        fmul0(tmp, tmp, tx);
1483
43
        fadd0(rp, tmp, rp);
1484
43
        p521_make_b_coeff(tmp);
1485
43
        fadd0(rp, tmp, rp);
1486
43
        fsqr0(ty, ty);
1487
43
        uint64_t r = bn_is_eq_mask(ty, rp);
1488
43
        uint64_t r0 = r;
1489
43
        bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL;
1490
43
        res = r1;
1491
43
    }
1492
44
    if (res) {
1493
36
        uint64_t *px = p_aff;
1494
36
        uint64_t *py = p_aff + 9U;
1495
36
        uint64_t *rx = point_jac;
1496
36
        uint64_t *ry = point_jac + 9U;
1497
36
        uint64_t *rz = point_jac + 18U;
1498
36
        to_mont(rx, px);
1499
36
        to_mont(ry, py);
1500
36
        p521_make_fone(rz);
1501
36
    }
1502
44
    bool res1 = res;
1503
44
    return res1;
1504
44
}
1505
1506
/**
1507
Private key validation.
1508
1509
  The function returns `true` if a private key is valid and `false` otherwise.
1510
1511
  The argument `private_key` points to 66 bytes of valid memory, i.e., uint8_t[66].
1512
1513
  The private key is valid:
1514
    • 0 < `private_key` < the order of the curve
1515
*/
1516
bool
1517
Hacl_P521_validate_private_key(uint8_t *private_key)
1518
1
{
1519
1
    uint64_t bn_sk[9U] = { 0U };
1520
1
    bn_from_bytes_be(bn_sk, private_key);
1521
1
    uint64_t tmp[9U] = { 0U };
1522
1
    p521_make_order(tmp);
1523
1
    uint64_t c = bn_sub(tmp, bn_sk, tmp);
1524
1
    uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL);
1525
1
    uint64_t bn_zero[9U] = { 0U };
1526
1
    uint64_t res = bn_is_eq_mask(bn_sk, bn_zero);
1527
1
    uint64_t is_eq_zero = res;
1528
1
    uint64_t res0 = is_lt_order & ~is_eq_zero;
1529
1
    return res0 == 0xFFFFFFFFFFFFFFFFULL;
1530
1
}
1531
1532
/*******************************************************************************
1533
  Parsing and Serializing public keys.
1534
1535
  A public key is a point (x, y) on the P-521 NIST curve.
1536
1537
  The point can be represented in the following three ways.
1538
    • raw          = [ x || y ], 132 bytes
1539
    • uncompressed = [ 0x04 || x || y ], 133 bytes
1540
    • compressed   = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes
1541
1542
*******************************************************************************/
1543
1544
/**
1545
Convert a public key from uncompressed to its raw form.
1546
1547
  The function returns `true` for successful conversion of a public key and `false` otherwise.
1548
1549
  The outparam `pk_raw` points to 132 bytes of valid memory, i.e., uint8_t[132].
1550
  The argument `pk` points to 133 bytes of valid memory, i.e., uint8_t[133].
1551
1552
  The function DOESN'T check whether (x, y) is a valid point.
1553
*/
1554
bool
1555
Hacl_P521_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw)
1556
0
{
1557
0
    uint8_t pk0 = pk[0U];
1558
0
    if (pk0 != 0x04U) {
1559
0
        return false;
1560
0
    }
1561
0
    memcpy(pk_raw, pk + 1U, 132U * sizeof(uint8_t));
1562
0
    return true;
1563
0
}
1564
1565
/**
1566
Convert a public key from compressed to its raw form.
1567
1568
  The function returns `true` for successful conversion of a public key and `false` otherwise.
1569
1570
  The outparam `pk_raw` points to 132 bytes of valid memory, i.e., uint8_t[132].
1571
  The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
1572
1573
  The function also checks whether (x, y) is a valid point.
1574
*/
1575
bool
1576
Hacl_P521_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw)
1577
0
{
1578
0
    uint64_t xa[9U] = { 0U };
1579
0
    uint64_t ya[9U] = { 0U };
1580
0
    uint8_t *pk_xb = pk + 1U;
1581
0
    uint8_t s0 = pk[0U];
1582
0
    uint8_t s01 = s0;
1583
0
    bool b;
1584
0
    if (!(s01 == 0x02U || s01 == 0x03U)) {
1585
0
        b = false;
1586
0
    } else {
1587
0
        uint8_t *xb = pk + 1U;
1588
0
        bn_from_bytes_be(xa, xb);
1589
0
        uint64_t is_x_valid = bn_is_lt_prime_mask(xa);
1590
0
        bool is_x_valid1 = is_x_valid == 0xFFFFFFFFFFFFFFFFULL;
1591
0
        bool is_y_odd = s01 == 0x03U;
1592
0
        if (!is_x_valid1) {
1593
0
            b = false;
1594
0
        } else {
1595
0
            uint64_t y2M[9U] = { 0U };
1596
0
            uint64_t xM[9U] = { 0U };
1597
0
            uint64_t yM[9U] = { 0U };
1598
0
            to_mont(xM, xa);
1599
0
            uint64_t tmp[9U] = { 0U };
1600
0
            fsqr0(y2M, xM);
1601
0
            fmul0(y2M, y2M, xM);
1602
0
            p521_make_a_coeff(tmp);
1603
0
            fmul0(tmp, tmp, xM);
1604
0
            fadd0(y2M, tmp, y2M);
1605
0
            p521_make_b_coeff(tmp);
1606
0
            fadd0(y2M, tmp, y2M);
1607
0
            p521_fsqrt(yM, y2M);
1608
0
            from_mont(ya, yM);
1609
0
            fsqr0(yM, yM);
1610
0
            uint64_t r = bn_is_eq_mask(yM, y2M);
1611
0
            uint64_t r0 = r;
1612
0
            bool is_y_valid = r0 == 0xFFFFFFFFFFFFFFFFULL;
1613
0
            bool is_y_valid0 = is_y_valid;
1614
0
            if (!is_y_valid0) {
1615
0
                b = false;
1616
0
            } else {
1617
0
                uint64_t is_y_odd1 = ya[0U] & 1ULL;
1618
0
                bool is_y_odd2 = is_y_odd1 == 1ULL;
1619
0
                uint64_t zero[9U] = { 0U };
1620
0
                if (is_y_odd2 != is_y_odd) {
1621
0
                    fsub0(ya, zero, ya);
1622
0
                }
1623
0
                b = true;
1624
0
            }
1625
0
        }
1626
0
    }
1627
0
    if (b) {
1628
0
        memcpy(pk_raw, pk_xb, 66U * sizeof(uint8_t));
1629
0
        bn_to_bytes_be(pk_raw + 66U, ya);
1630
0
    }
1631
0
    return b;
1632
0
}
1633
1634
/**
1635
Convert a public key from raw to its uncompressed form.
1636
1637
  The outparam `pk` points to 133 bytes of valid memory, i.e., uint8_t[133].
1638
  The argument `pk_raw` points to 132 bytes of valid memory, i.e., uint8_t[132].
1639
1640
  The function DOESN'T check whether (x, y) is a valid point.
1641
*/
1642
void
1643
Hacl_P521_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk)
1644
0
{
1645
0
    pk[0U] = 0x04U;
1646
0
    memcpy(pk + 1U, pk_raw, 132U * sizeof(uint8_t));
1647
0
}
1648
1649
/**
1650
Convert a public key from raw to its compressed form.
1651
1652
  The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
1653
  The argument `pk_raw` points to 132 bytes of valid memory, i.e., uint8_t[132].
1654
1655
  The function DOESN'T check whether (x, y) is a valid point.
1656
*/
1657
void
1658
Hacl_P521_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk)
1659
0
{
1660
0
    uint8_t *pk_x = pk_raw;
1661
0
    uint8_t *pk_y = pk_raw + 66U;
1662
0
    uint64_t bn_f[9U] = { 0U };
1663
0
    bn_from_bytes_be(bn_f, pk_y);
1664
0
    uint64_t is_odd_f = bn_f[0U] & 1ULL;
1665
0
    pk[0U] = (uint32_t)(uint8_t)is_odd_f + 0x02U;
1666
0
    memcpy(pk + 1U, pk_x, 66U * sizeof(uint8_t));
1667
0
}
1668
1669
/******************/
1670
/* ECDH agreement */
1671
/******************/
1672
1673
/**
1674
Compute the public key from the private key.
1675
1676
  The function returns `true` if a private key is valid and `false` otherwise.
1677
1678
  The outparam `public_key`  points to 132 bytes of valid memory, i.e., uint8_t[132].
1679
  The argument `private_key` points to 66 bytes of valid memory, i.e., uint8_t[66].
1680
1681
  The private key is valid:
1682
    • 0 < `private_key` < the order of the curve.
1683
*/
1684
bool
1685
Hacl_P521_dh_initiator(uint8_t *public_key, uint8_t *private_key)
1686
67
{
1687
67
    uint64_t tmp[36U] = { 0U };
1688
67
    uint64_t *sk = tmp;
1689
67
    uint64_t *pk = tmp + 9U;
1690
67
    uint64_t is_sk_valid = load_qelem_conditional(sk, private_key);
1691
67
    point_mul_g(pk, sk);
1692
67
    uint64_t aff_p[18U] = { 0U };
1693
67
    uint64_t zinv[9U] = { 0U };
1694
67
    uint64_t *px = pk;
1695
67
    uint64_t *py0 = pk + 9U;
1696
67
    uint64_t *pz = pk + 18U;
1697
67
    uint64_t *x = aff_p;
1698
67
    uint64_t *y = aff_p + 9U;
1699
67
    p521_finv(zinv, pz);
1700
67
    fmul0(x, px, zinv);
1701
67
    fmul0(y, py0, zinv);
1702
67
    from_mont(x, x);
1703
67
    from_mont(y, y);
1704
67
    uint64_t *px0 = aff_p;
1705
67
    uint64_t *py = aff_p + 9U;
1706
67
    bn_to_bytes_be(public_key, px0);
1707
67
    bn_to_bytes_be(public_key + 66U, py);
1708
67
    return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL;
1709
67
}
1710
1711
/**
1712
Execute the diffie-hellmann key exchange.
1713
1714
  The function returns `true` for successful creation of an ECDH shared secret and
1715
  `false` otherwise.
1716
1717
  The outparam `shared_secret` points to 132 bytes of valid memory, i.e., uint8_t[132].
1718
  The argument `their_pubkey` points to 132 bytes of valid memory, i.e., uint8_t[132].
1719
  The argument `private_key` points to 66 bytes of valid memory, i.e., uint8_t[66].
1720
1721
  The function also checks whether `private_key` and `their_pubkey` are valid.
1722
*/
1723
bool
1724
Hacl_P521_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key)
1725
0
{
1726
0
    uint64_t tmp[264U] = { 0U };
1727
0
    uint64_t *sk = tmp;
1728
0
    uint64_t *pk = tmp + 9U;
1729
0
    uint64_t p_aff[18U] = { 0U };
1730
0
    uint8_t *p_x = their_pubkey;
1731
0
    uint8_t *p_y = their_pubkey + 66U;
1732
0
    uint64_t *bn_p_x = p_aff;
1733
0
    uint64_t *bn_p_y = p_aff + 9U;
1734
0
    bn_from_bytes_be(bn_p_x, p_x);
1735
0
    bn_from_bytes_be(bn_p_y, p_y);
1736
0
    uint64_t *px0 = p_aff;
1737
0
    uint64_t *py0 = p_aff + 9U;
1738
0
    uint64_t lessX = bn_is_lt_prime_mask(px0);
1739
0
    uint64_t lessY = bn_is_lt_prime_mask(py0);
1740
0
    uint64_t res0 = lessX & lessY;
1741
0
    bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL;
1742
0
    bool res;
1743
0
    if (!is_xy_valid) {
1744
0
        res = false;
1745
0
    } else {
1746
0
        uint64_t rp[9U] = { 0U };
1747
0
        uint64_t tx[9U] = { 0U };
1748
0
        uint64_t ty[9U] = { 0U };
1749
0
        uint64_t *px = p_aff;
1750
0
        uint64_t *py = p_aff + 9U;
1751
0
        to_mont(tx, px);
1752
0
        to_mont(ty, py);
1753
0
        uint64_t tmp1[9U] = { 0U };
1754
0
        fsqr0(rp, tx);
1755
0
        fmul0(rp, rp, tx);
1756
0
        p521_make_a_coeff(tmp1);
1757
0
        fmul0(tmp1, tmp1, tx);
1758
0
        fadd0(rp, tmp1, rp);
1759
0
        p521_make_b_coeff(tmp1);
1760
0
        fadd0(rp, tmp1, rp);
1761
0
        fsqr0(ty, ty);
1762
0
        uint64_t r = bn_is_eq_mask(ty, rp);
1763
0
        uint64_t r0 = r;
1764
0
        bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL;
1765
0
        res = r1;
1766
0
    }
1767
0
    if (res) {
1768
0
        uint64_t *px = p_aff;
1769
0
        uint64_t *py = p_aff + 9U;
1770
0
        uint64_t *rx = pk;
1771
0
        uint64_t *ry = pk + 9U;
1772
0
        uint64_t *rz = pk + 18U;
1773
0
        to_mont(rx, px);
1774
0
        to_mont(ry, py);
1775
0
        p521_make_fone(rz);
1776
0
    }
1777
0
    bool is_pk_valid = res;
1778
0
    uint64_t is_sk_valid = load_qelem_conditional(sk, private_key);
1779
0
    uint64_t ss_proj[27U] = { 0U };
1780
0
    if (is_pk_valid) {
1781
0
        point_mul(ss_proj, sk, pk);
1782
0
        uint64_t aff_p[18U] = { 0U };
1783
0
        uint64_t zinv[9U] = { 0U };
1784
0
        uint64_t *px = ss_proj;
1785
0
        uint64_t *py1 = ss_proj + 9U;
1786
0
        uint64_t *pz = ss_proj + 18U;
1787
0
        uint64_t *x = aff_p;
1788
0
        uint64_t *y = aff_p + 9U;
1789
0
        p521_finv(zinv, pz);
1790
0
        fmul0(x, px, zinv);
1791
0
        fmul0(y, py1, zinv);
1792
0
        from_mont(x, x);
1793
0
        from_mont(y, y);
1794
0
        uint64_t *px1 = aff_p;
1795
0
        uint64_t *py = aff_p + 9U;
1796
0
        bn_to_bytes_be(shared_secret, px1);
1797
0
        bn_to_bytes_be(shared_secret + 66U, py);
1798
0
    }
1799
0
    return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL && is_pk_valid;
1800
0
}