Lines Matching refs:uint64_t
13 extern uint64_t FStar_UInt64_eq_mask(uint64_t x0, uint64_t x1);
15 extern uint64_t FStar_UInt64_gte_mask(uint64_t x0, uint64_t x1);
25 extern uint128_t FStar_UInt128_uint64_to_uint128(uint64_t x0);
27 extern uint64_t FStar_UInt128_uint128_to_uint64(uint128_t x0);
29 extern uint128_t FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
31 static void Hacl_Bignum_Modulo_carry_top(uint64_t *b)
33 uint64_t b4 = b[4U];
34 uint64_t b0 = b[0U];
35 uint64_t b4_ = b4 & (uint64_t)0x7ffffffffffffU;
36 uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U);
41 inline static void Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, uint128_t *input)
47 output[i] = (uint64_t)xi;
52 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint128_t *output, uint64_t *input, uint64_t s)
58 uint64_t yi = input[i];
71 uint64_t r0 = (uint64_t)tctr & (uint64_t)0x7ffffffffffffU;
78 inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)
80 uint64_t tmp = output[4U];
81 uint64_t b0;
87 uint64_t z = output[ctr - (uint32_t)1U];
93 output[0U] = (uint64_t)19U * b0;
97 Hacl_Bignum_Fmul_mul_shift_reduce_(uint128_t *output, uint64_t *input, uint64_t *input2)
100 uint64_t input2i;
105 uint64_t input2i0 = input2[i0];
115 inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)
117 uint64_t tmp[5U] = { 0U };
125 t[_i] = (uint128_t)(uint64_t)0U;
132 uint64_t i0;
133 uint64_t i1;
134 uint64_t i0_;
135 uint64_t i1_;
140 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
141 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);
147 i0_ = i0 & (uint64_t)0x7ffffffffffffU;
155 inline static void Hacl_Bignum_Fsquare_fsquare__(uint128_t *tmp, uint64_t *output)
157 uint64_t r0 = output[0U];
158 uint64_t r1 = output[1U];
159 uint64_t r2 = output[2U];
160 uint64_t r3 = output[3U];
161 uint64_t r4 = output[4U];
162 uint64_t d0 = r0 * (uint64_t)2U;
163 uint64_t d1 = r1 * (uint64_t)2U;
164 uint64_t d2 = r2 * (uint64_t)2U * (uint64_t)19U;
165 uint64_t d419 = r4 * (uint64_t)19U;
166 uint64_t d4 = d419 * (uint64_t)2U;
168 uint128_t s1 = (uint128_t)d0 * r1 + (uint128_t)d4 * r2 + (uint128_t)(r3 * (uint64_t)19U) * r3;
179 inline static void Hacl_Bignum_Fsquare_fsquare_(uint128_t *tmp, uint64_t *output)
185 uint64_t i0;
186 uint64_t i1;
187 uint64_t i0_;
188 uint64_t i1_;
193 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
194 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);
200 i0_ = i0 & (uint64_t)0x7ffffffffffffU;
207 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, uint128_t *tmp, uint32_t count1)
216 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1)
224 t[_i] = (uint128_t)(uint64_t)0U;
231 inline static void Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1)
239 t[_i] = (uint128_t)(uint64_t)0U;
245 inline static void Hacl_Bignum_Crecip_crecip(uint64_t *out, uint64_t *z)
247 uint64_t buf[20U] = { 0U };
248 uint64_t *a0 = buf;
249 uint64_t *t00 = buf + (uint32_t)5U;
250 uint64_t *b0 = buf + (uint32_t)10U;
251 uint64_t *t01;
252 uint64_t *b1;
253 uint64_t *c0;
254 uint64_t *a;
255 uint64_t *t0;
256 uint64_t *b;
257 uint64_t *c;
289 inline static void Hacl_Bignum_fsum(uint64_t *a, uint64_t *b)
294 uint64_t xi = a[i];
295 uint64_t yi = b[i];
300 inline static void Hacl_Bignum_fdifference(uint64_t *a, uint64_t *b)
302 uint64_t tmp[5U] = { 0U };
303 uint64_t b0;
304 uint64_t b1;
305 uint64_t b2;
306 uint64_t b3;
307 uint64_t b4;
314 tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;
315 tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U;
316 tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U;
317 tmp[3U] = b3 + (uint64_t)0x3ffffffffffff8U;
318 tmp[4U] = b4 + (uint64_t)0x3ffffffffffff8U;
323 uint64_t xi = a[i];
324 uint64_t yi = tmp[i];
330 inline static void Hacl_Bignum_fscalar(uint64_t *output, uint64_t *b, uint64_t s)
338 tmp[_i] = (uint128_t)(uint64_t)0U;
349 uint64_t xi = b[i];
356 b4_ = b4 & (uint128_t)(uint64_t)0x7ffffffffffffU;
357 b0_ = b0 + (uint128_t)(uint64_t)19U * (uint64_t)(b4 >> (uint32_t)51U);
365 inline static void Hacl_Bignum_fmul(uint64_t *output, uint64_t *a, uint64_t *b)
370 inline static void Hacl_Bignum_crecip(uint64_t *output, uint64_t *input)
376 Hacl_EC_Point_swap_conditional_step(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr)
379 uint64_t ai = a[i];
380 uint64_t bi = b[i];
381 uint64_t x = swap1 & (ai ^ bi);
382 uint64_t ai1 = ai ^ x;
383 uint64_t bi1 = bi ^ x;
389 Hacl_EC_Point_swap_conditional_(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr)
400 static void Hacl_EC_Point_swap_conditional(uint64_t *a, uint64_t *b, uint64_t iswap)
402 uint64_t swap1 = (uint64_t)0U - iswap;
407 static void Hacl_EC_Point_copy(uint64_t *output, uint64_t *input)
415 static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input)
417 uint64_t i0 = load64_le(input);
419 uint64_t i1 = load64_le(x00);
421 uint64_t i2 = load64_le(x01);
423 uint64_t i3 = load64_le(x02);
425 uint64_t i4 = load64_le(x0);
426 uint64_t output0 = i0 & (uint64_t)0x7ffffffffffffU;
427 uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU;
428 uint64_t output2 = i2 >> (uint32_t)6U & (uint64_t)0x7ffffffffffffU;
429 uint64_t output3 = i3 >> (uint32_t)1U & (uint64_t)0x7ffffffffffffU;
430 uint64_t output4 = i4 >> (uint32_t)12U & (uint64_t)0x7ffffffffffffU;
438 static void Hacl_EC_Format_fcontract_first_carry_pass(uint64_t *input)
440 uint64_t t0 = input[0U];
441 uint64_t t1 = input[1U];
442 uint64_t t2 = input[2U];
443 uint64_t t3 = input[3U];
444 uint64_t t4 = input[4U];
445 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U);
446 uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU;
447 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U);
448 uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU;
449 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U);
450 uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU;
451 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U);
452 uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU;
460 static void Hacl_EC_Format_fcontract_first_carry_full(uint64_t *input)
466 static void Hacl_EC_Format_fcontract_second_carry_pass(uint64_t *input)
468 uint64_t t0 = input[0U];
469 uint64_t t1 = input[1U];
470 uint64_t t2 = input[2U];
471 uint64_t t3 = input[3U];
472 uint64_t t4 = input[4U];
473 uint64_t t1_ = t1 + (t0 >> (uint32_t)51U);
474 uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU;
475 uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U);
476 uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU;
477 uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U);
478 uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU;
479 uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U);
480 uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU;
488 static void Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input)
490 uint64_t i0;
491 uint64_t i1;
492 uint64_t i0_;
493 uint64_t i1_;
498 i0_ = i0 & (uint64_t)0x7ffffffffffffU;
504 static void Hacl_EC_Format_fcontract_trim(uint64_t *input)
506 uint64_t a0 = input[0U];
507 uint64_t a1 = input[1U];
508 uint64_t a2 = input[2U];
509 uint64_t a3 = input[3U];
510 uint64_t a4 = input[4U];
511 uint64_t mask0 = FStar_UInt64_gte_mask(a0, (uint64_t)0x7ffffffffffedU);
512 uint64_t mask1 = FStar_UInt64_eq_mask(a1, (uint64_t)0x7ffffffffffffU);
513 uint64_t mask2 = FStar_UInt64_eq_mask(a2, (uint64_t)0x7ffffffffffffU);
514 uint64_t mask3 = FStar_UInt64_eq_mask(a3, (uint64_t)0x7ffffffffffffU);
515 uint64_t mask4 = FStar_UInt64_eq_mask(a4, (uint64_t)0x7ffffffffffffU);
516 uint64_t mask = (((mask0 & mask1) & mask2) & mask3) & mask4;
517 uint64_t a0_ = a0 - ((uint64_t)0x7ffffffffffedU & mask);
518 uint64_t a1_ = a1 - ((uint64_t)0x7ffffffffffffU & mask);
519 uint64_t a2_ = a2 - ((uint64_t)0x7ffffffffffffU & mask);
520 uint64_t a3_ = a3 - ((uint64_t)0x7ffffffffffffU & mask);
521 uint64_t a4_ = a4 - ((uint64_t)0x7ffffffffffffU & mask);
529 static void Hacl_EC_Format_fcontract_store(uint8_t *output, uint64_t *input)
531 uint64_t t0 = input[0U];
532 uint64_t t1 = input[1U];
533 uint64_t t2 = input[2U];
534 uint64_t t3 = input[3U];
535 uint64_t t4 = input[4U];
536 uint64_t o0 = t1 << (uint32_t)51U | t0;
537 uint64_t o1 = t2 << (uint32_t)38U | t1 >> (uint32_t)13U;
538 uint64_t o2 = t3 << (uint32_t)25U | t2 >> (uint32_t)26U;
539 uint64_t o3 = t4 << (uint32_t)12U | t3 >> (uint32_t)39U;
550 static void Hacl_EC_Format_fcontract(uint8_t *output, uint64_t *input)
558 static void Hacl_EC_Format_scalar_of_point(uint8_t *scalar, uint64_t *point)
560 uint64_t *x = point;
561 uint64_t *z = point + (uint32_t)5U;
562 uint64_t buf[10U] = { 0U };
563 uint64_t *zmone = buf;
564 uint64_t *sc = buf + (uint32_t)5U;
572 uint64_t *pp,
573 uint64_t *ppq,
574 uint64_t *p,
575 uint64_t *pq,
576 uint64_t *qmqp
579 uint64_t *qx = qmqp;
580 uint64_t *x2 = pp;
581 uint64_t *z2 = pp + (uint32_t)5U;
582 uint64_t *x3 = ppq;
583 uint64_t *z3 = ppq + (uint32_t)5U;
584 uint64_t *x = p;
585 uint64_t *z = p + (uint32_t)5U;
586 uint64_t *xprime = pq;
587 uint64_t *zprime = pq + (uint32_t)5U;
588 uint64_t buf[40U] = { 0U };
589 uint64_t *origx = buf;
590 uint64_t *origxprime0 = buf + (uint32_t)5U;
591 uint64_t *xxprime0 = buf + (uint32_t)25U;
592 uint64_t *zzprime0 = buf + (uint32_t)30U;
593 uint64_t *origxprime;
594 uint64_t *xx0;
595 uint64_t *zz0;
596 uint64_t *xxprime;
597 uint64_t *zzprime;
598 uint64_t *zzzprime;
599 uint64_t *zzz;
600 uint64_t *xx;
601 uint64_t *zz;
602 uint64_t scalar;
630 scalar = (uint64_t)121665U;
638 uint64_t *nq,
639 uint64_t *nqpq,
640 uint64_t *nq2,
641 uint64_t *nqpq2,
642 uint64_t *q,
646 uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U);
647 uint64_t bit;
650 bit = (uint64_t)(byt >> (uint32_t)7U);
656 uint64_t *nq,
657 uint64_t *nqpq,
658 uint64_t *nq2,
659 uint64_t *nqpq2,
660 uint64_t *q,
672 uint64_t *nq,
673 uint64_t *nqpq,
674 uint64_t *nq2,
675 uint64_t *nqpq2,
676 uint64_t *q,
694 uint64_t *nq,
695 uint64_t *nqpq,
696 uint64_t *nq2,
697 uint64_t *nqpq2,
698 uint64_t *q,
711 static void Hacl_EC_Ladder_cmult(uint64_t *result, uint8_t *n1, uint64_t *q)
713 uint64_t point_buf[40U] = { 0U };
714 uint64_t *nq = point_buf;
715 uint64_t *nqpq = point_buf + (uint32_t)10U;
716 uint64_t *nq2 = point_buf + (uint32_t)20U;
717 uint64_t *nqpq2 = point_buf + (uint32_t)30U;
719 nq[0U] = (uint64_t)1U;
726 uint64_t buf0[10U] = { 0U };
727 uint64_t *x0 = buf0;
728 uint64_t *z = buf0 + (uint32_t)5U;
729 uint64_t *q;
731 z[0U] = (uint64_t)1U;
751 uint64_t buf[15U] = { 0U };
752 uint64_t *nq = buf;
753 uint64_t *x = nq;
754 x[0U] = (uint64_t)1U;