main/nss/nss_win.patch

396 -            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
399 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
409 -            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
412 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
422 -            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
425 +    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
435 -            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
438 +    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
447 -    return ((FStar_UInt128_uint128){.low = a.low & b.low, .high = a.high & b.high });
450 +    ret.high = a.high & b.high;
457 -    return ((FStar_UInt128_uint128){.low = a.low ^ b.low, .high = a.high ^ b.high });
460 +    ret.high = a.high ^ b.high;
467 -    return ((FStar_UInt128_uint128){.low = a.low | b.low, .high = a.high | b.high });
470 +    ret.high = a.high | b.high;
477 -    return ((FStar_UInt128_uint128){.low = ~a.low, .high = ~a.high });
480 +    ret.high = ~a.high;
496 -                .high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) });
499 +        ret.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s);
507 -    return ((FStar_UInt128_uint128){.low = (uint64_t)0U, .high = a.low << (s - FStar_UInt128_u32_6…
510 +    ret.high = a.low << (s - FStar_UInt128_u32_64);
525 -                .low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s),
526 -                .high = a.high >> s });
528 +        ret.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s);
529 +        ret.high = a.high >> s;
537 -    return ((FStar_UInt128_uint128){.low = a.high >> (s - FStar_UInt128_u32_64), .high = (uint64_t…
539 +    ret.low = a.high >> (s - FStar_UInt128_u32_64);
540 +    ret.high = (uint64_t)0U;
551 -            .low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high),
552 -            .high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high) });
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);
564 …ow = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt…
565 -            .high = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)…
567 …ow = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt…
568 +    ret.high = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (…
575 -    return ((FStar_UInt128_uint128){.low = a, .high = (uint64_t)0U });
578 +    ret.high = (uint64_t)0U;
611 -            .high = x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +
616 +    ret.high = x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +