Coverage Report

Created: 2024-11-21 07:03

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