main/nss/nss_win.patch

397 +    FStar_UInt128_uint128 ret;
398 +    ret.low = a.low + b.low;
399 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
400 +    return (ret);
410 +    FStar_UInt128_uint128 ret;
411 +    ret.low = a.low + b.low;
412 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
413 +    return (ret);
423 +    FStar_UInt128_uint128 ret;
424 +    ret.low = a.low - b.low;
425 +    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
426 +    return (ret);
436 +    FStar_UInt128_uint128 ret;
437 +    ret.low = a.low - b.low;
438 +    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
439 +    return (ret);
448 +    FStar_UInt128_uint128 ret;
449 +    ret.low = a.low & b.low;
450 +    ret.high = a.high & b.high;
451 +    return (ret);
458 +    FStar_UInt128_uint128 ret;
459 +    ret.low = a.low ^ b.low;
460 +    ret.high = a.high ^ b.high;
461 +    return (ret);
468 +    FStar_UInt128_uint128 ret;
469 +    ret.low = a.low | b.low;
470 +    ret.high = a.high | b.high;
471 +    return (ret);
478 +    FStar_UInt128_uint128 ret;
479 +    ret.low = ~a.low;
480 +    ret.high = ~a.high;
481 +    return (ret);
489 +    FStar_UInt128_uint128 ret;
498 +        ret.low = a.low << s;
499 +        ret.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s);
500 +        return (ret);
508 +    FStar_UInt128_uint128 ret;
509 +    ret.low = (uint64_t)0U;
510 +    ret.high = a.low << (s - FStar_UInt128_u32_64);
511 +    return (ret);
519 +    FStar_UInt128_uint128 ret;
528 +        ret.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s);
529 +        ret.high = a.high >> s;
530 +        return (ret);
538 +    FStar_UInt128_uint128 ret;
539 +    ret.low = a.high >> (s - FStar_UInt128_u32_64);
540 +    ret.high = (uint64_t)0U;
541 +    return (ret);
553 +    FStar_UInt128_uint128 ret;
554 +    ret.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
555 +    ret.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
556 +    return (ret);
566 +    FStar_UInt128_uint128 ret;
567 +    ret.low = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (F…
568 +    ret.high = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (…
569 +    return (ret);
576 +    FStar_UInt128_uint128 ret;
577 +    ret.low = a;
578 +    ret.high = (uint64_t)0U;
579 +    return (ret);
594 +    K___uint64_t_uint64_t_uint64_t_uint64_t ret;
595 +    ret.fst = FStar_UInt128_u64_mod_32(x);
596 +    ret.snd = FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y));
597 +    ret.thd = x >> FStar_UInt128_u32_32;
598 +    ret.f3 = (x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32…
599 +    return (ret);
613 +    FStar_UInt128_uint128 ret;
614 +    ret.low = FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_…
616 +    ret.high = x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +
618 +    return (ret);
1902 +    Hacl_Impl_Poly1305_32_State_poly1305_state ret;
1903 +    ret.r = r;
1904 +    ret.h = h;
1905 +    return (ret);