1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2    Licensed under the Apache 2.0 License. */
3 
4 /* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
5  * KreMLin invocation: /mnt/e/everest/verify/kremlin/krml -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -fc89 -fparentheses -fno-shadow -header /mnt/e/everest/verify/hdrcLh -minimal -I /mnt/e/everest/verify/hacl-star/code/lib/kremlin -I /mnt/e/everest/verify/kremlin/kremlib/compat -I /mnt/e/everest/verify/hacl-star/specs -I /mnt/e/everest/verify/hacl-star/specs/old -I . -ccopt -march=native -verbose -ldopt -flto -tmpdir x25519-c -I ../bignum -bundle Hacl.Curve25519=* -minimal -add-include "kremlib.h" -skip-compilation x25519-c/out.krml -o x25519-c/Hacl_Curve25519.c
6  * F* version: 059db0c8
7  * KreMLin version: 916c37ac
8  */
9 
10 
11 #include "Hacl_Curve25519.h"
12 
13 extern uint64_t FStar_UInt64_eq_mask(uint64_t x0, uint64_t x1);
14 
15 extern uint64_t FStar_UInt64_gte_mask(uint64_t x0, uint64_t x1);
16 
17 extern FStar_UInt128_uint128
18 FStar_UInt128_add(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
19 
20 extern FStar_UInt128_uint128
21 FStar_UInt128_add_mod(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
22 
23 extern FStar_UInt128_uint128
24 FStar_UInt128_logand(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
25 
26 extern FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 x0, uint32_t x1);
27 
28 extern FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t x0);
29 
30 extern uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 x0);
31 
32 extern FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
33 
Hacl_Bignum_Modulo_carry_top(uint64_t * b)34 static void Hacl_Bignum_Modulo_carry_top(uint64_t *b)
35 {
36   uint64_t b4 = b[4U];
37   uint64_t b0 = b[0U];
38   uint64_t b4_ = b4 & (uint64_t)0x7ffffffffffffU;
39   uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U);
40   b[4U] = b4_;
41   b[0U] = b0_;
42 }
43 
44 inline static void
Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t * output,FStar_UInt128_uint128 * input)45 Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_uint128 *input)
46 {
47   uint32_t i;
48   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)
49   {
50     FStar_UInt128_uint128 xi = input[i];
51     output[i] = FStar_UInt128_uint128_to_uint64(xi);
52   }
53 }
54 
55 inline static void
Hacl_Bignum_Fproduct_sum_scalar_multiplication_(FStar_UInt128_uint128 * output,uint64_t * input,uint64_t s)56 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(
57   FStar_UInt128_uint128 *output,
58   uint64_t *input,
59   uint64_t s
60 )
61 {
62   uint32_t i;
63   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)
64   {
65     FStar_UInt128_uint128 xi = output[i];
66     uint64_t yi = input[i];
67     output[i] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s));
68   }
69 }
70 
Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_uint128 * tmp)71 inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_uint128 *tmp)
72 {
73   uint32_t i;
74   for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U)
75   {
76     uint32_t ctr = i;
77     FStar_UInt128_uint128 tctr = tmp[ctr];
78     FStar_UInt128_uint128 tctrp1 = tmp[ctr + (uint32_t)1U];
79     uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU;
80     FStar_UInt128_uint128 c = FStar_UInt128_shift_right(tctr, (uint32_t)51U);
81     tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0);
82     tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c);
83   }
84 }
85 
Hacl_Bignum_Fmul_shift_reduce(uint64_t * output)86 inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)
87 {
88   uint64_t tmp = output[4U];
89   uint64_t b0;
90   {
91     uint32_t i;
92     for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U)
93     {
94       uint32_t ctr = (uint32_t)5U - i - (uint32_t)1U;
95       uint64_t z = output[ctr - (uint32_t)1U];
96       output[ctr] = z;
97     }
98   }
99   output[0U] = tmp;
100   b0 = output[0U];
101   output[0U] = (uint64_t)19U * b0;
102 }
103 
104 static void
Hacl_Bignum_Fmul_mul_shift_reduce_(FStar_UInt128_uint128 * output,uint64_t * input,uint64_t * input2)105 Hacl_Bignum_Fmul_mul_shift_reduce_(
106   FStar_UInt128_uint128 *output,
107   uint64_t *input,
108   uint64_t *input2
109 )
110 {
111   uint32_t i;
112   uint64_t input2i;
113   {
114     uint32_t i0;
115     for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0 = i0 + (uint32_t)1U)
116     {
117       uint64_t input2i0 = input2[i0];
118       Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i0);
119       Hacl_Bignum_Fmul_shift_reduce(input);
120     }
121   }
122   i = (uint32_t)4U;
123   input2i = input2[i];
124   Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
125 }
126 
Hacl_Bignum_Fmul_fmul(uint64_t * output,uint64_t * input,uint64_t * input2)127 inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)
128 {
129   uint64_t tmp[5U] = { 0U };
130   memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
131   KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U);
132   {
133     FStar_UInt128_uint128 t[5U];
134     {
135       uint32_t _i;
136       for (_i = 0U; _i < (uint32_t)5U; ++_i)
137         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
138     }
139     {
140       FStar_UInt128_uint128 b4;
141       FStar_UInt128_uint128 b0;
142       FStar_UInt128_uint128 b4_;
143       FStar_UInt128_uint128 b0_;
144       uint64_t i0;
145       uint64_t i1;
146       uint64_t i0_;
147       uint64_t i1_;
148       Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2);
149       Hacl_Bignum_Fproduct_carry_wide_(t);
150       b4 = t[4U];
151       b0 = t[0U];
152       b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
153       b0_ =
154         FStar_UInt128_add(b0,
155           FStar_UInt128_mul_wide((uint64_t)19U,
156             FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
157       t[4U] = b4_;
158       t[0U] = b0_;
159       Hacl_Bignum_Fproduct_copy_from_wide_(output, t);
160       i0 = output[0U];
161       i1 = output[1U];
162       i0_ = i0 & (uint64_t)0x7ffffffffffffU;
163       i1_ = i1 + (i0 >> (uint32_t)51U);
164       output[0U] = i0_;
165       output[1U] = i1_;
166     }
167   }
168 }
169 
Hacl_Bignum_Fsquare_fsquare__(FStar_UInt128_uint128 * tmp,uint64_t * output)170 inline static void Hacl_Bignum_Fsquare_fsquare__(FStar_UInt128_uint128 *tmp, uint64_t *output)
171 {
172   uint64_t r0 = output[0U];
173   uint64_t r1 = output[1U];
174   uint64_t r2 = output[2U];
175   uint64_t r3 = output[3U];
176   uint64_t r4 = output[4U];
177   uint64_t d0 = r0 * (uint64_t)2U;
178   uint64_t d1 = r1 * (uint64_t)2U;
179   uint64_t d2 = r2 * (uint64_t)2U * (uint64_t)19U;
180   uint64_t d419 = r4 * (uint64_t)19U;
181   uint64_t d4 = d419 * (uint64_t)2U;
182   FStar_UInt128_uint128
183   s0 =
184     FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(r0, r0),
185         FStar_UInt128_mul_wide(d4, r1)),
186       FStar_UInt128_mul_wide(d2, r3));
187   FStar_UInt128_uint128
188   s1 =
189     FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r1),
190         FStar_UInt128_mul_wide(d4, r2)),
191       FStar_UInt128_mul_wide(r3 * (uint64_t)19U, r3));
192   FStar_UInt128_uint128
193   s2 =
194     FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r2),
195         FStar_UInt128_mul_wide(r1, r1)),
196       FStar_UInt128_mul_wide(d4, r3));
197   FStar_UInt128_uint128
198   s3 =
199     FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r3),
200         FStar_UInt128_mul_wide(d1, r2)),
201       FStar_UInt128_mul_wide(r4, d419));
202   FStar_UInt128_uint128
203   s4 =
204     FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r4),
205         FStar_UInt128_mul_wide(d1, r3)),
206       FStar_UInt128_mul_wide(r2, r2));
207   tmp[0U] = s0;
208   tmp[1U] = s1;
209   tmp[2U] = s2;
210   tmp[3U] = s3;
211   tmp[4U] = s4;
212 }
213 
Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_uint128 * tmp,uint64_t * output)214 inline static void Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_uint128 *tmp, uint64_t *output)
215 {
216   FStar_UInt128_uint128 b4;
217   FStar_UInt128_uint128 b0;
218   FStar_UInt128_uint128 b4_;
219   FStar_UInt128_uint128 b0_;
220   uint64_t i0;
221   uint64_t i1;
222   uint64_t i0_;
223   uint64_t i1_;
224   Hacl_Bignum_Fsquare_fsquare__(tmp, output);
225   Hacl_Bignum_Fproduct_carry_wide_(tmp);
226   b4 = tmp[4U];
227   b0 = tmp[0U];
228   b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
229   b0_ =
230     FStar_UInt128_add(b0,
231       FStar_UInt128_mul_wide((uint64_t)19U,
232         FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
233   tmp[4U] = b4_;
234   tmp[0U] = b0_;
235   Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);
236   i0 = output[0U];
237   i1 = output[1U];
238   i0_ = i0 & (uint64_t)0x7ffffffffffffU;
239   i1_ = i1 + (i0 >> (uint32_t)51U);
240   output[0U] = i0_;
241   output[1U] = i1_;
242 }
243 
244 static void
Hacl_Bignum_Fsquare_fsquare_times_(uint64_t * input,FStar_UInt128_uint128 * tmp,uint32_t count1)245 Hacl_Bignum_Fsquare_fsquare_times_(
246   uint64_t *input,
247   FStar_UInt128_uint128 *tmp,
248   uint32_t count1
249 )
250 {
251   uint32_t i;
252   Hacl_Bignum_Fsquare_fsquare_(tmp, input);
253   for (i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U)
254     Hacl_Bignum_Fsquare_fsquare_(tmp, input);
255 }
256 
257 inline static void
Hacl_Bignum_Fsquare_fsquare_times(uint64_t * output,uint64_t * input,uint32_t count1)258 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1)
259 {
260   KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U);
261   {
262     FStar_UInt128_uint128 t[5U];
263     {
264       uint32_t _i;
265       for (_i = 0U; _i < (uint32_t)5U; ++_i)
266         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
267     }
268     memcpy(output, input, (uint32_t)5U * sizeof input[0U]);
269     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);
270   }
271 }
272 
Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t * output,uint32_t count1)273 inline static void Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1)
274 {
275   KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U);
276   {
277     FStar_UInt128_uint128 t[5U];
278     {
279       uint32_t _i;
280       for (_i = 0U; _i < (uint32_t)5U; ++_i)
281         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
282     }
283     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);
284   }
285 }
286 
Hacl_Bignum_Crecip_crecip(uint64_t * out,uint64_t * z)287 inline static void Hacl_Bignum_Crecip_crecip(uint64_t *out, uint64_t *z)
288 {
289   uint64_t buf[20U] = { 0U };
290   uint64_t *a0 = buf;
291   uint64_t *t00 = buf + (uint32_t)5U;
292   uint64_t *b0 = buf + (uint32_t)10U;
293   uint64_t *t01;
294   uint64_t *b1;
295   uint64_t *c0;
296   uint64_t *a;
297   uint64_t *t0;
298   uint64_t *b;
299   uint64_t *c;
300   Hacl_Bignum_Fsquare_fsquare_times(a0, z, (uint32_t)1U);
301   Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)2U);
302   Hacl_Bignum_Fmul_fmul(b0, t00, z);
303   Hacl_Bignum_Fmul_fmul(a0, b0, a0);
304   Hacl_Bignum_Fsquare_fsquare_times(t00, a0, (uint32_t)1U);
305   Hacl_Bignum_Fmul_fmul(b0, t00, b0);
306   Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U);
307   t01 = buf + (uint32_t)5U;
308   b1 = buf + (uint32_t)10U;
309   c0 = buf + (uint32_t)15U;
310   Hacl_Bignum_Fmul_fmul(b1, t01, b1);
311   Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U);
312   Hacl_Bignum_Fmul_fmul(c0, t01, b1);
313   Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U);
314   Hacl_Bignum_Fmul_fmul(t01, t01, c0);
315   Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U);
316   Hacl_Bignum_Fmul_fmul(b1, t01, b1);
317   Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U);
318   a = buf;
319   t0 = buf + (uint32_t)5U;
320   b = buf + (uint32_t)10U;
321   c = buf + (uint32_t)15U;
322   Hacl_Bignum_Fmul_fmul(c, t0, b);
323   Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U);
324   Hacl_Bignum_Fmul_fmul(t0, t0, c);
325   Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)50U);
326   Hacl_Bignum_Fmul_fmul(t0, t0, b);
327   Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)5U);
328   Hacl_Bignum_Fmul_fmul(out, t0, a);
329 }
330 
Hacl_Bignum_fsum(uint64_t * a,uint64_t * b)331 inline static void Hacl_Bignum_fsum(uint64_t *a, uint64_t *b)
332 {
333   uint32_t i;
334   for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)
335   {
336     uint64_t xi = a[i];
337     uint64_t yi = b[i];
338     a[i] = xi + yi;
339   }
340 }
341 
Hacl_Bignum_fdifference(uint64_t * a,uint64_t * b)342 inline static void Hacl_Bignum_fdifference(uint64_t *a, uint64_t *b)
343 {
344   uint64_t tmp[5U] = { 0U };
345   uint64_t b0;
346   uint64_t b1;
347   uint64_t b2;
348   uint64_t b3;
349   uint64_t b4;
350   memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]);
351   b0 = tmp[0U];
352   b1 = tmp[1U];
353   b2 = tmp[2U];
354   b3 = tmp[3U];
355   b4 = tmp[4U];
356   tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;
357   tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U;
358   tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U;
359   tmp[3U] = b3 + (uint64_t)0x3ffffffffffff8U;
360   tmp[4U] = b4 + (uint64_t)0x3ffffffffffff8U;
361   {
362     uint32_t i;
363     for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)
364     {
365       uint64_t xi = a[i];
366       uint64_t yi = tmp[i];
367       a[i] = yi - xi;
368     }
369   }
370 }
371 
Hacl_Bignum_fscalar(uint64_t * output,uint64_t * b,uint64_t s)372 inline static void Hacl_Bignum_fscalar(uint64_t *output, uint64_t *b, uint64_t s)
373 {
374   KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)5U);
375   {
376     FStar_UInt128_uint128 tmp[5U];
377     {
378       uint32_t _i;
379       for (_i = 0U; _i < (uint32_t)5U; ++_i)
380         tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
381     }
382     {
383       FStar_UInt128_uint128 b4;
384       FStar_UInt128_uint128 b0;
385       FStar_UInt128_uint128 b4_;
386       FStar_UInt128_uint128 b0_;
387       {
388         uint32_t i;
389         for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U)
390         {
391           uint64_t xi = b[i];
392           tmp[i] = FStar_UInt128_mul_wide(xi, s);
393         }
394       }
395       Hacl_Bignum_Fproduct_carry_wide_(tmp);
396       b4 = tmp[4U];
397       b0 = tmp[0U];
398       b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
399       b0_ =
400         FStar_UInt128_add(b0,
401           FStar_UInt128_mul_wide((uint64_t)19U,
402             FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
403       tmp[4U] = b4_;
404       tmp[0U] = b0_;
405       Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);
406     }
407   }
408 }
409 
Hacl_Bignum_fmul(uint64_t * output,uint64_t * a,uint64_t * b)410 inline static void Hacl_Bignum_fmul(uint64_t *output, uint64_t *a, uint64_t *b)
411 {
412   Hacl_Bignum_Fmul_fmul(output, a, b);
413 }
414 
Hacl_Bignum_crecip(uint64_t * output,uint64_t * input)415 inline static void Hacl_Bignum_crecip(uint64_t *output, uint64_t *input)
416 {
417   Hacl_Bignum_Crecip_crecip(output, input);
418 }
419 
420 static void
Hacl_EC_Point_swap_conditional_step(uint64_t * a,uint64_t * b,uint64_t swap1,uint32_t ctr)421 Hacl_EC_Point_swap_conditional_step(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr)
422 {
423   uint32_t i = ctr - (uint32_t)1U;
424   uint64_t ai = a[i];
425   uint64_t bi = b[i];
426   uint64_t x = swap1 & (ai ^ bi);
427   uint64_t ai1 = ai ^ x;
428   uint64_t bi1 = bi ^ x;
429   a[i] = ai1;
430   b[i] = bi1;
431 }
432 
433 static void
Hacl_EC_Point_swap_conditional_(uint64_t * a,uint64_t * b,uint64_t swap1,uint32_t ctr)434 Hacl_EC_Point_swap_conditional_(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr)
435 {
436   if (!(ctr == (uint32_t)0U))
437   {
438     uint32_t i;
439     Hacl_EC_Point_swap_conditional_step(a, b, swap1, ctr);
440     i = ctr - (uint32_t)1U;
441     Hacl_EC_Point_swap_conditional_(a, b, swap1, i);
442   }
443 }
444 
Hacl_EC_Point_swap_conditional(uint64_t * a,uint64_t * b,uint64_t iswap)445 static void Hacl_EC_Point_swap_conditional(uint64_t *a, uint64_t *b, uint64_t iswap)
446 {
447   uint64_t swap1 = (uint64_t)0U - iswap;
448   Hacl_EC_Point_swap_conditional_(a, b, swap1, (uint32_t)5U);
449   Hacl_EC_Point_swap_conditional_(a + (uint32_t)5U, b + (uint32_t)5U, swap1, (uint32_t)5U);
450 }
451 
Hacl_EC_Point_copy(uint64_t * output,uint64_t * input)452 static void Hacl_EC_Point_copy(uint64_t *output, uint64_t *input)
453 {
454   memcpy(output, input, (uint32_t)5U * sizeof input[0U]);
455   memcpy(output + (uint32_t)5U,
456     input + (uint32_t)5U,
457     (uint32_t)5U * sizeof (input + (uint32_t)5U)[0U]);
458 }
459 
Hacl_EC_Format_fexpand(uint64_t * output,uint8_t * input)460 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input)
461 {
462   uint64_t i0 = load64_le(input);
463   uint8_t *x00 = input + (uint32_t)6U;
464   uint64_t i1 = load64_le(x00);
465   uint8_t *x01 = input + (uint32_t)12U;
466   uint64_t i2 = load64_le(x01);
467   uint8_t *x02 = input + (uint32_t)19U;
468   uint64_t i3 = load64_le(x02);
469   uint8_t *x0 = input + (uint32_t)24U;
470   uint64_t i4 = load64_le(x0);
471   uint64_t output0 = i0 & (uint64_t)0x7ffffffffffffU;
472   uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU;
473   uint64_t output2 = i2 >> (uint32_t)6U & (uint64_t)0x7ffffffffffffU;
474   uint64_t output3 = i3 >> (uint32_t)1U & (uint64_t)0x7ffffffffffffU;
475   uint64_t output4 = i4 >> (uint32_t)12U & (uint64_t)0x7ffffffffffffU;
476   output[0U] = output0;
477   output[1U] = output1;
478   output[2U] = output2;
479   output[3U] = output3;
480   output[4U] = output4;
481 }
482 
Hacl_EC_Format_fcontract_first_carry_pass(uint64_t * input)483 static void Hacl_EC_Format_fcontract_first_carry_pass(uint64_t *input)
484 {
485   uint64_t t0 = input[0U];
486   uint64_t t1 = input[1U];
487   uint64_t t2 = input[2U];
488   uint64_t t3 = input[3U];
489   uint64_t t4 = input[4U];
490   uint64_t t1_ = t1 + (t0 >> (uint32_t)51U);
491   uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU;
492   uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U);
493   uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU;
494   uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U);
495   uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU;
496   uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U);
497   uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU;
498   input[0U] = t0_;
499   input[1U] = t1__;
500   input[2U] = t2__;
501   input[3U] = t3__;
502   input[4U] = t4_;
503 }
504 
Hacl_EC_Format_fcontract_first_carry_full(uint64_t * input)505 static void Hacl_EC_Format_fcontract_first_carry_full(uint64_t *input)
506 {
507   Hacl_EC_Format_fcontract_first_carry_pass(input);
508   Hacl_Bignum_Modulo_carry_top(input);
509 }
510 
Hacl_EC_Format_fcontract_second_carry_pass(uint64_t * input)511 static void Hacl_EC_Format_fcontract_second_carry_pass(uint64_t *input)
512 {
513   uint64_t t0 = input[0U];
514   uint64_t t1 = input[1U];
515   uint64_t t2 = input[2U];
516   uint64_t t3 = input[3U];
517   uint64_t t4 = input[4U];
518   uint64_t t1_ = t1 + (t0 >> (uint32_t)51U);
519   uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU;
520   uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U);
521   uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU;
522   uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U);
523   uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU;
524   uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U);
525   uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU;
526   input[0U] = t0_;
527   input[1U] = t1__;
528   input[2U] = t2__;
529   input[3U] = t3__;
530   input[4U] = t4_;
531 }
532 
Hacl_EC_Format_fcontract_second_carry_full(uint64_t * input)533 static void Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input)
534 {
535   uint64_t i0;
536   uint64_t i1;
537   uint64_t i0_;
538   uint64_t i1_;
539   Hacl_EC_Format_fcontract_second_carry_pass(input);
540   Hacl_Bignum_Modulo_carry_top(input);
541   i0 = input[0U];
542   i1 = input[1U];
543   i0_ = i0 & (uint64_t)0x7ffffffffffffU;
544   i1_ = i1 + (i0 >> (uint32_t)51U);
545   input[0U] = i0_;
546   input[1U] = i1_;
547 }
548 
Hacl_EC_Format_fcontract_trim(uint64_t * input)549 static void Hacl_EC_Format_fcontract_trim(uint64_t *input)
550 {
551   uint64_t a0 = input[0U];
552   uint64_t a1 = input[1U];
553   uint64_t a2 = input[2U];
554   uint64_t a3 = input[3U];
555   uint64_t a4 = input[4U];
556   uint64_t mask0 = FStar_UInt64_gte_mask(a0, (uint64_t)0x7ffffffffffedU);
557   uint64_t mask1 = FStar_UInt64_eq_mask(a1, (uint64_t)0x7ffffffffffffU);
558   uint64_t mask2 = FStar_UInt64_eq_mask(a2, (uint64_t)0x7ffffffffffffU);
559   uint64_t mask3 = FStar_UInt64_eq_mask(a3, (uint64_t)0x7ffffffffffffU);
560   uint64_t mask4 = FStar_UInt64_eq_mask(a4, (uint64_t)0x7ffffffffffffU);
561   uint64_t mask = (((mask0 & mask1) & mask2) & mask3) & mask4;
562   uint64_t a0_ = a0 - ((uint64_t)0x7ffffffffffedU & mask);
563   uint64_t a1_ = a1 - ((uint64_t)0x7ffffffffffffU & mask);
564   uint64_t a2_ = a2 - ((uint64_t)0x7ffffffffffffU & mask);
565   uint64_t a3_ = a3 - ((uint64_t)0x7ffffffffffffU & mask);
566   uint64_t a4_ = a4 - ((uint64_t)0x7ffffffffffffU & mask);
567   input[0U] = a0_;
568   input[1U] = a1_;
569   input[2U] = a2_;
570   input[3U] = a3_;
571   input[4U] = a4_;
572 }
573 
Hacl_EC_Format_fcontract_store(uint8_t * output,uint64_t * input)574 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input)
575 {
576   uint64_t t0 = input[0U];
577   uint64_t t1 = input[1U];
578   uint64_t t2 = input[2U];
579   uint64_t t3 = input[3U];
580   uint64_t t4 = input[4U];
581   uint64_t o0 = t1 << (uint32_t)51U | t0;
582   uint64_t o1 = t2 << (uint32_t)38U | t1 >> (uint32_t)13U;
583   uint64_t o2 = t3 << (uint32_t)25U | t2 >> (uint32_t)26U;
584   uint64_t o3 = t4 << (uint32_t)12U | t3 >> (uint32_t)39U;
585   uint8_t *b0 = output;
586   uint8_t *b1 = output + (uint32_t)8U;
587   uint8_t *b2 = output + (uint32_t)16U;
588   uint8_t *b3 = output + (uint32_t)24U;
589   store64_le(b0, o0);
590   store64_le(b1, o1);
591   store64_le(b2, o2);
592   store64_le(b3, o3);
593 }
594 
Hacl_EC_Format_fcontract(uint8_t * output,uint64_t * input)595 static void Hacl_EC_Format_fcontract(uint8_t *output, uint64_t *input)
596 {
597   Hacl_EC_Format_fcontract_first_carry_full(input);
598   Hacl_EC_Format_fcontract_second_carry_full(input);
599   Hacl_EC_Format_fcontract_trim(input);
600   Hacl_EC_Format_fcontract_store(output, input);
601 }
602 
Hacl_EC_Format_scalar_of_point(uint8_t * scalar,uint64_t * point)603 static void Hacl_EC_Format_scalar_of_point(uint8_t *scalar, uint64_t *point)
604 {
605   uint64_t *x = point;
606   uint64_t *z = point + (uint32_t)5U;
607   uint64_t buf[10U] = { 0U };
608   uint64_t *zmone = buf;
609   uint64_t *sc = buf + (uint32_t)5U;
610   Hacl_Bignum_crecip(zmone, z);
611   Hacl_Bignum_fmul(sc, x, zmone);
612   Hacl_EC_Format_fcontract(scalar, sc);
613 }
614 
615 static void
Hacl_EC_AddAndDouble_fmonty(uint64_t * pp,uint64_t * ppq,uint64_t * p,uint64_t * pq,uint64_t * qmqp)616 Hacl_EC_AddAndDouble_fmonty(
617   uint64_t *pp,
618   uint64_t *ppq,
619   uint64_t *p,
620   uint64_t *pq,
621   uint64_t *qmqp
622 )
623 {
624   uint64_t *qx = qmqp;
625   uint64_t *x2 = pp;
626   uint64_t *z2 = pp + (uint32_t)5U;
627   uint64_t *x3 = ppq;
628   uint64_t *z3 = ppq + (uint32_t)5U;
629   uint64_t *x = p;
630   uint64_t *z = p + (uint32_t)5U;
631   uint64_t *xprime = pq;
632   uint64_t *zprime = pq + (uint32_t)5U;
633   uint64_t buf[40U] = { 0U };
634   uint64_t *origx = buf;
635   uint64_t *origxprime0 = buf + (uint32_t)5U;
636   uint64_t *xxprime0 = buf + (uint32_t)25U;
637   uint64_t *zzprime0 = buf + (uint32_t)30U;
638   uint64_t *origxprime;
639   uint64_t *xx0;
640   uint64_t *zz0;
641   uint64_t *xxprime;
642   uint64_t *zzprime;
643   uint64_t *zzzprime;
644   uint64_t *zzz;
645   uint64_t *xx;
646   uint64_t *zz;
647   uint64_t scalar;
648   memcpy(origx, x, (uint32_t)5U * sizeof x[0U]);
649   Hacl_Bignum_fsum(x, z);
650   Hacl_Bignum_fdifference(z, origx);
651   memcpy(origxprime0, xprime, (uint32_t)5U * sizeof xprime[0U]);
652   Hacl_Bignum_fsum(xprime, zprime);
653   Hacl_Bignum_fdifference(zprime, origxprime0);
654   Hacl_Bignum_fmul(xxprime0, xprime, z);
655   Hacl_Bignum_fmul(zzprime0, x, zprime);
656   origxprime = buf + (uint32_t)5U;
657   xx0 = buf + (uint32_t)15U;
658   zz0 = buf + (uint32_t)20U;
659   xxprime = buf + (uint32_t)25U;
660   zzprime = buf + (uint32_t)30U;
661   zzzprime = buf + (uint32_t)35U;
662   memcpy(origxprime, xxprime, (uint32_t)5U * sizeof xxprime[0U]);
663   Hacl_Bignum_fsum(xxprime, zzprime);
664   Hacl_Bignum_fdifference(zzprime, origxprime);
665   Hacl_Bignum_Fsquare_fsquare_times(x3, xxprime, (uint32_t)1U);
666   Hacl_Bignum_Fsquare_fsquare_times(zzzprime, zzprime, (uint32_t)1U);
667   Hacl_Bignum_fmul(z3, zzzprime, qx);
668   Hacl_Bignum_Fsquare_fsquare_times(xx0, x, (uint32_t)1U);
669   Hacl_Bignum_Fsquare_fsquare_times(zz0, z, (uint32_t)1U);
670   zzz = buf + (uint32_t)10U;
671   xx = buf + (uint32_t)15U;
672   zz = buf + (uint32_t)20U;
673   Hacl_Bignum_fmul(x2, xx, zz);
674   Hacl_Bignum_fdifference(zz, xx);
675   scalar = (uint64_t)121665U;
676   Hacl_Bignum_fscalar(zzz, zz, scalar);
677   Hacl_Bignum_fsum(zzz, xx);
678   Hacl_Bignum_fmul(z2, zzz, zz);
679 }
680 
681 static void
Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(uint64_t * nq,uint64_t * nqpq,uint64_t * nq2,uint64_t * nqpq2,uint64_t * q,uint8_t byt)682 Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(
683   uint64_t *nq,
684   uint64_t *nqpq,
685   uint64_t *nq2,
686   uint64_t *nqpq2,
687   uint64_t *q,
688   uint8_t byt
689 )
690 {
691   uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U);
692   uint64_t bit;
693   Hacl_EC_Point_swap_conditional(nq, nqpq, bit0);
694   Hacl_EC_AddAndDouble_fmonty(nq2, nqpq2, nq, nqpq, q);
695   bit = (uint64_t)(byt >> (uint32_t)7U);
696   Hacl_EC_Point_swap_conditional(nq2, nqpq2, bit);
697 }
698 
699 static void
Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step(uint64_t * nq,uint64_t * nqpq,uint64_t * nq2,uint64_t * nqpq2,uint64_t * q,uint8_t byt)700 Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step(
701   uint64_t *nq,
702   uint64_t *nqpq,
703   uint64_t *nq2,
704   uint64_t *nqpq2,
705   uint64_t *q,
706   uint8_t byt
707 )
708 {
709   uint8_t byt1;
710   Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(nq, nqpq, nq2, nqpq2, q, byt);
711   byt1 = byt << (uint32_t)1U;
712   Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(nq2, nqpq2, nq, nqpq, q, byt1);
713 }
714 
715 static void
Hacl_EC_Ladder_SmallLoop_cmult_small_loop(uint64_t * nq,uint64_t * nqpq,uint64_t * nq2,uint64_t * nqpq2,uint64_t * q,uint8_t byt,uint32_t i)716 Hacl_EC_Ladder_SmallLoop_cmult_small_loop(
717   uint64_t *nq,
718   uint64_t *nqpq,
719   uint64_t *nq2,
720   uint64_t *nqpq2,
721   uint64_t *q,
722   uint8_t byt,
723   uint32_t i
724 )
725 {
726   if (!(i == (uint32_t)0U))
727   {
728     uint32_t i_ = i - (uint32_t)1U;
729     uint8_t byt_;
730     Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step(nq, nqpq, nq2, nqpq2, q, byt);
731     byt_ = byt << (uint32_t)2U;
732     Hacl_EC_Ladder_SmallLoop_cmult_small_loop(nq, nqpq, nq2, nqpq2, q, byt_, i_);
733   }
734 }
735 
736 static void
Hacl_EC_Ladder_BigLoop_cmult_big_loop(uint8_t * n1,uint64_t * nq,uint64_t * nqpq,uint64_t * nq2,uint64_t * nqpq2,uint64_t * q,uint32_t i)737 Hacl_EC_Ladder_BigLoop_cmult_big_loop(
738   uint8_t *n1,
739   uint64_t *nq,
740   uint64_t *nqpq,
741   uint64_t *nq2,
742   uint64_t *nqpq2,
743   uint64_t *q,
744   uint32_t i
745 )
746 {
747   if (!(i == (uint32_t)0U))
748   {
749     uint32_t i1 = i - (uint32_t)1U;
750     uint8_t byte = n1[i1];
751     Hacl_EC_Ladder_SmallLoop_cmult_small_loop(nq, nqpq, nq2, nqpq2, q, byte, (uint32_t)4U);
752     Hacl_EC_Ladder_BigLoop_cmult_big_loop(n1, nq, nqpq, nq2, nqpq2, q, i1);
753   }
754 }
755 
Hacl_EC_Ladder_cmult(uint64_t * result,uint8_t * n1,uint64_t * q)756 static void Hacl_EC_Ladder_cmult(uint64_t *result, uint8_t *n1, uint64_t *q)
757 {
758   uint64_t point_buf[40U] = { 0U };
759   uint64_t *nq = point_buf;
760   uint64_t *nqpq = point_buf + (uint32_t)10U;
761   uint64_t *nq2 = point_buf + (uint32_t)20U;
762   uint64_t *nqpq2 = point_buf + (uint32_t)30U;
763   Hacl_EC_Point_copy(nqpq, q);
764   nq[0U] = (uint64_t)1U;
765   Hacl_EC_Ladder_BigLoop_cmult_big_loop(n1, nq, nqpq, nq2, nqpq2, q, (uint32_t)32U);
766   Hacl_EC_Point_copy(result, nq);
767 }
768 
Hacl_Curve25519_crypto_scalarmult(uint8_t * mypublic,uint8_t * secret,uint8_t * basepoint)769 void Hacl_Curve25519_crypto_scalarmult(uint8_t *mypublic, uint8_t *secret, uint8_t *basepoint)
770 {
771   uint64_t buf0[10U] = { 0U };
772   uint64_t *x0 = buf0;
773   uint64_t *z = buf0 + (uint32_t)5U;
774   uint64_t *q;
775   Hacl_EC_Format_fexpand(x0, basepoint);
776   z[0U] = (uint64_t)1U;
777   q = buf0;
778   {
779     uint8_t e[32U] = { 0U };
780     uint8_t e0;
781     uint8_t e31;
782     uint8_t e01;
783     uint8_t e311;
784     uint8_t e312;
785     uint8_t *scalar;
786     memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]);
787     e0 = e[0U];
788     e31 = e[31U];
789     e01 = e0 & (uint8_t)248U;
790     e311 = e31 & (uint8_t)127U;
791     e312 = e311 | (uint8_t)64U;
792     e[0U] = e01;
793     e[31U] = e312;
794     scalar = e;
795     {
796       uint64_t buf[15U] = { 0U };
797       uint64_t *nq = buf;
798       uint64_t *x = nq;
799       x[0U] = (uint64_t)1U;
800       Hacl_EC_Ladder_cmult(nq, scalar, q);
801       Hacl_EC_Format_scalar_of_point(mypublic, nq);
802     }
803   }
804 }
805 
806