Lines Matching refs:low

395 -            .low = a.low + b.low,
396 -            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
398 +    ret.low = a.low + b.low;
399 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
408 -            .low = a.low + b.low,
409 -            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
411 +    ret.low = a.low + b.low;
412 +    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
421 -            .low = a.low - b.low,
422 -            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
424 +    ret.low = a.low - b.low;
425 +    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
434 -            .low = a.low - b.low,
435 -            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
437 +    ret.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 });
449 +    ret.low = a.low & b.low;
457 -    return ((FStar_UInt128_uint128){.low = a.low ^ b.low, .high = a.high ^ b.high });
459 +    ret.low = a.low ^ b.low;
467 -    return ((FStar_UInt128_uint128){.low = a.low | b.low, .high = a.high | b.high });
469 +    ret.low = a.low | b.low;
477 -    return ((FStar_UInt128_uint128){.low = ~a.low, .high = ~a.high });
479 +    ret.low = ~a.low;
495 -                .low = a.low << s,
496 -                .high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) });
498 +        ret.low = 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…
509 +    ret.low = (uint64_t)0U;
510 +    ret.high = a.low << (s - FStar_UInt128_u32_64);
525 -                .low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s),
528 +        ret.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, 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);
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 …low = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UIn…
565 …a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)) });
567 …low = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UIn…
568 …sk(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low));
575 -    return ((FStar_UInt128_uint128){.low = a, .high = (uint64_t)0U });
577 +    ret.low = a;
609 -            .low = FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64…
614 +    ret.low = FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_…