#![allow(non_snake_case)]
#![allow(non_upper_case_globals)]
#![allow(non_camel_case_types)]
#![allow(unused_assignments)]
#![allow(unreachable_patterns)]

use libcrux_macros as krml;

use crate::fstar;
use crate::lowstar;

#[inline]
pub fn fadd(out: &mut [u64], f1: &[u64], f2: &[u64]) {
    let f10: u64 = f1[0usize];
    let f20: u64 = f2[0usize];
    let f11: u64 = f1[1usize];
    let f21: u64 = f2[1usize];
    let f12: u64 = f1[2usize];
    let f22: u64 = f2[2usize];
    let f13: u64 = f1[3usize];
    let f23: u64 = f2[3usize];
    let f14: u64 = f1[4usize];
    let f24: u64 = f2[4usize];
    out[0usize] = f10.wrapping_add(f20);
    out[1usize] = f11.wrapping_add(f21);
    out[2usize] = f12.wrapping_add(f22);
    out[3usize] = f13.wrapping_add(f23);
    out[4usize] = f14.wrapping_add(f24)
}

#[inline]
pub fn fsub(out: &mut [u64], f1: &[u64], f2: &[u64]) {
    let f10: u64 = f1[0usize];
    let f20: u64 = f2[0usize];
    let f11: u64 = f1[1usize];
    let f21: u64 = f2[1usize];
    let f12: u64 = f1[2usize];
    let f22: u64 = f2[2usize];
    let f13: u64 = f1[3usize];
    let f23: u64 = f2[3usize];
    let f14: u64 = f1[4usize];
    let f24: u64 = f2[4usize];
    out[0usize] = f10.wrapping_add(0x3fffffffffff68u64).wrapping_sub(f20);
    out[1usize] = f11.wrapping_add(0x3ffffffffffff8u64).wrapping_sub(f21);
    out[2usize] = f12.wrapping_add(0x3ffffffffffff8u64).wrapping_sub(f22);
    out[3usize] = f13.wrapping_add(0x3ffffffffffff8u64).wrapping_sub(f23);
    out[4usize] = f14.wrapping_add(0x3ffffffffffff8u64).wrapping_sub(f24)
}

#[inline]
pub fn fmul(out: &mut [u64], f1: &[u64], f2: &[u64], uu___: &[fstar::uint128::uint128]) {
    lowstar::ignore::ignore::<&[fstar::uint128::uint128]>(uu___);
    let f10: u64 = f1[0usize];
    let f11: u64 = f1[1usize];
    let f12: u64 = f1[2usize];
    let f13: u64 = f1[3usize];
    let f14: u64 = f1[4usize];
    let f20: u64 = f2[0usize];
    let f21: u64 = f2[1usize];
    let f22: u64 = f2[2usize];
    let f23: u64 = f2[3usize];
    let f24: u64 = f2[4usize];
    let tmp1: u64 = f21.wrapping_mul(19u64);
    let tmp2: u64 = f22.wrapping_mul(19u64);
    let tmp3: u64 = f23.wrapping_mul(19u64);
    let tmp4: u64 = f24.wrapping_mul(19u64);
    let o0: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f20);
    let o1: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f21);
    let o2: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f22);
    let o3: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f23);
    let o4: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f24);
    let o01: fstar::uint128::uint128 = fstar::uint128::add(o0, fstar::uint128::mul_wide(f11, tmp4));
    let o11: fstar::uint128::uint128 = fstar::uint128::add(o1, fstar::uint128::mul_wide(f11, f20));
    let o21: fstar::uint128::uint128 = fstar::uint128::add(o2, fstar::uint128::mul_wide(f11, f21));
    let o31: fstar::uint128::uint128 = fstar::uint128::add(o3, fstar::uint128::mul_wide(f11, f22));
    let o41: fstar::uint128::uint128 = fstar::uint128::add(o4, fstar::uint128::mul_wide(f11, f23));
    let o02: fstar::uint128::uint128 =
        fstar::uint128::add(o01, fstar::uint128::mul_wide(f12, tmp3));
    let o12: fstar::uint128::uint128 =
        fstar::uint128::add(o11, fstar::uint128::mul_wide(f12, tmp4));
    let o22: fstar::uint128::uint128 = fstar::uint128::add(o21, fstar::uint128::mul_wide(f12, f20));
    let o32: fstar::uint128::uint128 = fstar::uint128::add(o31, fstar::uint128::mul_wide(f12, f21));
    let o42: fstar::uint128::uint128 = fstar::uint128::add(o41, fstar::uint128::mul_wide(f12, f22));
    let o03: fstar::uint128::uint128 =
        fstar::uint128::add(o02, fstar::uint128::mul_wide(f13, tmp2));
    let o13: fstar::uint128::uint128 =
        fstar::uint128::add(o12, fstar::uint128::mul_wide(f13, tmp3));
    let o23: fstar::uint128::uint128 =
        fstar::uint128::add(o22, fstar::uint128::mul_wide(f13, tmp4));
    let o33: fstar::uint128::uint128 = fstar::uint128::add(o32, fstar::uint128::mul_wide(f13, f20));
    let o43: fstar::uint128::uint128 = fstar::uint128::add(o42, fstar::uint128::mul_wide(f13, f21));
    let o04: fstar::uint128::uint128 =
        fstar::uint128::add(o03, fstar::uint128::mul_wide(f14, tmp1));
    let o14: fstar::uint128::uint128 =
        fstar::uint128::add(o13, fstar::uint128::mul_wide(f14, tmp2));
    let o24: fstar::uint128::uint128 =
        fstar::uint128::add(o23, fstar::uint128::mul_wide(f14, tmp3));
    let o34: fstar::uint128::uint128 =
        fstar::uint128::add(o33, fstar::uint128::mul_wide(f14, tmp4));
    let o44: fstar::uint128::uint128 = fstar::uint128::add(o43, fstar::uint128::mul_wide(f14, f20));
    let tmp_w0: fstar::uint128::uint128 = o04;
    let tmp_w1: fstar::uint128::uint128 = o14;
    let tmp_w2: fstar::uint128::uint128 = o24;
    let tmp_w3: fstar::uint128::uint128 = o34;
    let tmp_w4: fstar::uint128::uint128 = o44;
    let l·: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w0, fstar::uint128::uint64_to_uint128(0u64));
    let tmp01: u64 = fstar::uint128::uint128_to_uint64(l·) & 0x7ffffffffffffu64;
    let c0: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·, 51u32));
    let l·0: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w1, fstar::uint128::uint64_to_uint128(c0));
    let tmp11: u64 = fstar::uint128::uint128_to_uint64(l·0) & 0x7ffffffffffffu64;
    let c1: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·0, 51u32));
    let l·1: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w2, fstar::uint128::uint64_to_uint128(c1));
    let tmp21: u64 = fstar::uint128::uint128_to_uint64(l·1) & 0x7ffffffffffffu64;
    let c2: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·1, 51u32));
    let l·2: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w3, fstar::uint128::uint64_to_uint128(c2));
    let tmp31: u64 = fstar::uint128::uint128_to_uint64(l·2) & 0x7ffffffffffffu64;
    let c3: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·2, 51u32));
    let l·3: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w4, fstar::uint128::uint64_to_uint128(c3));
    let tmp41: u64 = fstar::uint128::uint128_to_uint64(l·3) & 0x7ffffffffffffu64;
    let c4: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·3, 51u32));
    let l·4: u64 = tmp01.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let o00: u64 = tmp0·;
    let o10: u64 = tmp11.wrapping_add(c5);
    let o20: u64 = tmp21;
    let o30: u64 = tmp31;
    let o40: u64 = tmp41;
    out[0usize] = o00;
    out[1usize] = o10;
    out[2usize] = o20;
    out[3usize] = o30;
    out[4usize] = o40
}

#[inline]
pub fn fmul2(out: &mut [u64], f1: &[u64], f2: &[u64], uu___: &[fstar::uint128::uint128]) {
    lowstar::ignore::ignore::<&[fstar::uint128::uint128]>(uu___);
    let f10: u64 = f1[0usize];
    let f11: u64 = f1[1usize];
    let f12: u64 = f1[2usize];
    let f13: u64 = f1[3usize];
    let f14: u64 = f1[4usize];
    let f20: u64 = f2[0usize];
    let f21: u64 = f2[1usize];
    let f22: u64 = f2[2usize];
    let f23: u64 = f2[3usize];
    let f24: u64 = f2[4usize];
    let f30: u64 = f1[5usize];
    let f31: u64 = f1[6usize];
    let f32: u64 = f1[7usize];
    let f33: u64 = f1[8usize];
    let f34: u64 = f1[9usize];
    let f40: u64 = f2[5usize];
    let f41: u64 = f2[6usize];
    let f42: u64 = f2[7usize];
    let f43: u64 = f2[8usize];
    let f44: u64 = f2[9usize];
    let tmp11: u64 = f21.wrapping_mul(19u64);
    let tmp12: u64 = f22.wrapping_mul(19u64);
    let tmp13: u64 = f23.wrapping_mul(19u64);
    let tmp14: u64 = f24.wrapping_mul(19u64);
    let tmp21: u64 = f41.wrapping_mul(19u64);
    let tmp22: u64 = f42.wrapping_mul(19u64);
    let tmp23: u64 = f43.wrapping_mul(19u64);
    let tmp24: u64 = f44.wrapping_mul(19u64);
    let o0: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f20);
    let o1: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f21);
    let o2: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f22);
    let o3: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f23);
    let o4: fstar::uint128::uint128 = fstar::uint128::mul_wide(f10, f24);
    let o01: fstar::uint128::uint128 =
        fstar::uint128::add(o0, fstar::uint128::mul_wide(f11, tmp14));
    let o11: fstar::uint128::uint128 = fstar::uint128::add(o1, fstar::uint128::mul_wide(f11, f20));
    let o21: fstar::uint128::uint128 = fstar::uint128::add(o2, fstar::uint128::mul_wide(f11, f21));
    let o31: fstar::uint128::uint128 = fstar::uint128::add(o3, fstar::uint128::mul_wide(f11, f22));
    let o41: fstar::uint128::uint128 = fstar::uint128::add(o4, fstar::uint128::mul_wide(f11, f23));
    let o02: fstar::uint128::uint128 =
        fstar::uint128::add(o01, fstar::uint128::mul_wide(f12, tmp13));
    let o12: fstar::uint128::uint128 =
        fstar::uint128::add(o11, fstar::uint128::mul_wide(f12, tmp14));
    let o22: fstar::uint128::uint128 = fstar::uint128::add(o21, fstar::uint128::mul_wide(f12, f20));
    let o32: fstar::uint128::uint128 = fstar::uint128::add(o31, fstar::uint128::mul_wide(f12, f21));
    let o42: fstar::uint128::uint128 = fstar::uint128::add(o41, fstar::uint128::mul_wide(f12, f22));
    let o03: fstar::uint128::uint128 =
        fstar::uint128::add(o02, fstar::uint128::mul_wide(f13, tmp12));
    let o13: fstar::uint128::uint128 =
        fstar::uint128::add(o12, fstar::uint128::mul_wide(f13, tmp13));
    let o23: fstar::uint128::uint128 =
        fstar::uint128::add(o22, fstar::uint128::mul_wide(f13, tmp14));
    let o33: fstar::uint128::uint128 = fstar::uint128::add(o32, fstar::uint128::mul_wide(f13, f20));
    let o43: fstar::uint128::uint128 = fstar::uint128::add(o42, fstar::uint128::mul_wide(f13, f21));
    let o04: fstar::uint128::uint128 =
        fstar::uint128::add(o03, fstar::uint128::mul_wide(f14, tmp11));
    let o14: fstar::uint128::uint128 =
        fstar::uint128::add(o13, fstar::uint128::mul_wide(f14, tmp12));
    let o24: fstar::uint128::uint128 =
        fstar::uint128::add(o23, fstar::uint128::mul_wide(f14, tmp13));
    let o34: fstar::uint128::uint128 =
        fstar::uint128::add(o33, fstar::uint128::mul_wide(f14, tmp14));
    let o44: fstar::uint128::uint128 = fstar::uint128::add(o43, fstar::uint128::mul_wide(f14, f20));
    let tmp_w10: fstar::uint128::uint128 = o04;
    let tmp_w11: fstar::uint128::uint128 = o14;
    let tmp_w12: fstar::uint128::uint128 = o24;
    let tmp_w13: fstar::uint128::uint128 = o34;
    let tmp_w14: fstar::uint128::uint128 = o44;
    let o00: fstar::uint128::uint128 = fstar::uint128::mul_wide(f30, f40);
    let o10: fstar::uint128::uint128 = fstar::uint128::mul_wide(f30, f41);
    let o20: fstar::uint128::uint128 = fstar::uint128::mul_wide(f30, f42);
    let o30: fstar::uint128::uint128 = fstar::uint128::mul_wide(f30, f43);
    let o40: fstar::uint128::uint128 = fstar::uint128::mul_wide(f30, f44);
    let o010: fstar::uint128::uint128 =
        fstar::uint128::add(o00, fstar::uint128::mul_wide(f31, tmp24));
    let o110: fstar::uint128::uint128 =
        fstar::uint128::add(o10, fstar::uint128::mul_wide(f31, f40));
    let o210: fstar::uint128::uint128 =
        fstar::uint128::add(o20, fstar::uint128::mul_wide(f31, f41));
    let o310: fstar::uint128::uint128 =
        fstar::uint128::add(o30, fstar::uint128::mul_wide(f31, f42));
    let o410: fstar::uint128::uint128 =
        fstar::uint128::add(o40, fstar::uint128::mul_wide(f31, f43));
    let o020: fstar::uint128::uint128 =
        fstar::uint128::add(o010, fstar::uint128::mul_wide(f32, tmp23));
    let o120: fstar::uint128::uint128 =
        fstar::uint128::add(o110, fstar::uint128::mul_wide(f32, tmp24));
    let o220: fstar::uint128::uint128 =
        fstar::uint128::add(o210, fstar::uint128::mul_wide(f32, f40));
    let o320: fstar::uint128::uint128 =
        fstar::uint128::add(o310, fstar::uint128::mul_wide(f32, f41));
    let o420: fstar::uint128::uint128 =
        fstar::uint128::add(o410, fstar::uint128::mul_wide(f32, f42));
    let o030: fstar::uint128::uint128 =
        fstar::uint128::add(o020, fstar::uint128::mul_wide(f33, tmp22));
    let o130: fstar::uint128::uint128 =
        fstar::uint128::add(o120, fstar::uint128::mul_wide(f33, tmp23));
    let o230: fstar::uint128::uint128 =
        fstar::uint128::add(o220, fstar::uint128::mul_wide(f33, tmp24));
    let o330: fstar::uint128::uint128 =
        fstar::uint128::add(o320, fstar::uint128::mul_wide(f33, f40));
    let o430: fstar::uint128::uint128 =
        fstar::uint128::add(o420, fstar::uint128::mul_wide(f33, f41));
    let o040: fstar::uint128::uint128 =
        fstar::uint128::add(o030, fstar::uint128::mul_wide(f34, tmp21));
    let o140: fstar::uint128::uint128 =
        fstar::uint128::add(o130, fstar::uint128::mul_wide(f34, tmp22));
    let o240: fstar::uint128::uint128 =
        fstar::uint128::add(o230, fstar::uint128::mul_wide(f34, tmp23));
    let o340: fstar::uint128::uint128 =
        fstar::uint128::add(o330, fstar::uint128::mul_wide(f34, tmp24));
    let o440: fstar::uint128::uint128 =
        fstar::uint128::add(o430, fstar::uint128::mul_wide(f34, f40));
    let tmp_w20: fstar::uint128::uint128 = o040;
    let tmp_w21: fstar::uint128::uint128 = o140;
    let tmp_w22: fstar::uint128::uint128 = o240;
    let tmp_w23: fstar::uint128::uint128 = o340;
    let tmp_w24: fstar::uint128::uint128 = o440;
    let l·: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w10, fstar::uint128::uint64_to_uint128(0u64));
    let tmp0: u64 = fstar::uint128::uint128_to_uint64(l·) & 0x7ffffffffffffu64;
    let c0: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·, 51u32));
    let l·0: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w11, fstar::uint128::uint64_to_uint128(c0));
    let tmp1: u64 = fstar::uint128::uint128_to_uint64(l·0) & 0x7ffffffffffffu64;
    let c1: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·0, 51u32));
    let l·1: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w12, fstar::uint128::uint64_to_uint128(c1));
    let tmp2: u64 = fstar::uint128::uint128_to_uint64(l·1) & 0x7ffffffffffffu64;
    let c2: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·1, 51u32));
    let l·2: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w13, fstar::uint128::uint64_to_uint128(c2));
    let tmp3: u64 = fstar::uint128::uint128_to_uint64(l·2) & 0x7ffffffffffffu64;
    let c3: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·2, 51u32));
    let l·3: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w14, fstar::uint128::uint64_to_uint128(c3));
    let tmp4: u64 = fstar::uint128::uint128_to_uint64(l·3) & 0x7ffffffffffffu64;
    let c4: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·3, 51u32));
    let l·4: u64 = tmp0.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let o100: u64 = tmp0·;
    let o111: u64 = tmp1.wrapping_add(c5);
    let o121: u64 = tmp2;
    let o131: u64 = tmp3;
    let o141: u64 = tmp4;
    let l·5: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w20, fstar::uint128::uint64_to_uint128(0u64));
    let tmp00: u64 = fstar::uint128::uint128_to_uint64(l·5) & 0x7ffffffffffffu64;
    let c00: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·5, 51u32));
    let l·6: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w21, fstar::uint128::uint64_to_uint128(c00));
    let tmp10: u64 = fstar::uint128::uint128_to_uint64(l·6) & 0x7ffffffffffffu64;
    let c10: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·6, 51u32));
    let l·7: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w22, fstar::uint128::uint64_to_uint128(c10));
    let tmp20: u64 = fstar::uint128::uint128_to_uint64(l·7) & 0x7ffffffffffffu64;
    let c20: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·7, 51u32));
    let l·8: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w23, fstar::uint128::uint64_to_uint128(c20));
    let tmp30: u64 = fstar::uint128::uint128_to_uint64(l·8) & 0x7ffffffffffffu64;
    let c30: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·8, 51u32));
    let l·9: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w24, fstar::uint128::uint64_to_uint128(c30));
    let tmp40: u64 = fstar::uint128::uint128_to_uint64(l·9) & 0x7ffffffffffffu64;
    let c40: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·9, 51u32));
    let l·10: u64 = tmp00.wrapping_add(c40.wrapping_mul(19u64));
    let tmp0·0: u64 = l·10 & 0x7ffffffffffffu64;
    let c50: u64 = l·10.wrapping_shr(51u32);
    let o200: u64 = tmp0·0;
    let o211: u64 = tmp10.wrapping_add(c50);
    let o221: u64 = tmp20;
    let o231: u64 = tmp30;
    let o241: u64 = tmp40;
    let o101: u64 = o100;
    let o112: u64 = o111;
    let o122: u64 = o121;
    let o132: u64 = o131;
    let o142: u64 = o141;
    let o201: u64 = o200;
    let o212: u64 = o211;
    let o222: u64 = o221;
    let o232: u64 = o231;
    let o242: u64 = o241;
    out[0usize] = o101;
    out[1usize] = o112;
    out[2usize] = o122;
    out[3usize] = o132;
    out[4usize] = o142;
    out[5usize] = o201;
    out[6usize] = o212;
    out[7usize] = o222;
    out[8usize] = o232;
    out[9usize] = o242
}

#[inline]
pub fn fmul1(out: &mut [u64], f1: &[u64], f2: u64) {
    let f10: u64 = f1[0usize];
    let f11: u64 = f1[1usize];
    let f12: u64 = f1[2usize];
    let f13: u64 = f1[3usize];
    let f14: u64 = f1[4usize];
    let tmp_w0: fstar::uint128::uint128 = fstar::uint128::mul_wide(f2, f10);
    let tmp_w1: fstar::uint128::uint128 = fstar::uint128::mul_wide(f2, f11);
    let tmp_w2: fstar::uint128::uint128 = fstar::uint128::mul_wide(f2, f12);
    let tmp_w3: fstar::uint128::uint128 = fstar::uint128::mul_wide(f2, f13);
    let tmp_w4: fstar::uint128::uint128 = fstar::uint128::mul_wide(f2, f14);
    let l·: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w0, fstar::uint128::uint64_to_uint128(0u64));
    let tmp0: u64 = fstar::uint128::uint128_to_uint64(l·) & 0x7ffffffffffffu64;
    let c0: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·, 51u32));
    let l·0: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w1, fstar::uint128::uint64_to_uint128(c0));
    let tmp1: u64 = fstar::uint128::uint128_to_uint64(l·0) & 0x7ffffffffffffu64;
    let c1: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·0, 51u32));
    let l·1: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w2, fstar::uint128::uint64_to_uint128(c1));
    let tmp2: u64 = fstar::uint128::uint128_to_uint64(l·1) & 0x7ffffffffffffu64;
    let c2: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·1, 51u32));
    let l·2: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w3, fstar::uint128::uint64_to_uint128(c2));
    let tmp3: u64 = fstar::uint128::uint128_to_uint64(l·2) & 0x7ffffffffffffu64;
    let c3: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·2, 51u32));
    let l·3: fstar::uint128::uint128 =
        fstar::uint128::add(tmp_w4, fstar::uint128::uint64_to_uint128(c3));
    let tmp4: u64 = fstar::uint128::uint128_to_uint64(l·3) & 0x7ffffffffffffu64;
    let c4: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·3, 51u32));
    let l·4: u64 = tmp0.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let o0: u64 = tmp0·;
    let o1: u64 = tmp1.wrapping_add(c5);
    let o2: u64 = tmp2;
    let o3: u64 = tmp3;
    let o4: u64 = tmp4;
    out[0usize] = o0;
    out[1usize] = o1;
    out[2usize] = o2;
    out[3usize] = o3;
    out[4usize] = o4
}

#[inline]
pub fn fsqr(out: &mut [u64], f: &[u64], uu___: &[fstar::uint128::uint128]) {
    lowstar::ignore::ignore::<&[fstar::uint128::uint128]>(uu___);
    let f0: u64 = f[0usize];
    let f1: u64 = f[1usize];
    let f2: u64 = f[2usize];
    let f3: u64 = f[3usize];
    let f4: u64 = f[4usize];
    let d0: u64 = 2u64.wrapping_mul(f0);
    let d1: u64 = 2u64.wrapping_mul(f1);
    let d2: u64 = 38u64.wrapping_mul(f2);
    let d3: u64 = 19u64.wrapping_mul(f3);
    let d419: u64 = 19u64.wrapping_mul(f4);
    let d4: u64 = 2u64.wrapping_mul(d419);
    let s0: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(f0, f0),
            fstar::uint128::mul_wide(d4, f1),
        ),
        fstar::uint128::mul_wide(d2, f3),
    );
    let s1: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f1),
            fstar::uint128::mul_wide(d4, f2),
        ),
        fstar::uint128::mul_wide(d3, f3),
    );
    let s2: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f2),
            fstar::uint128::mul_wide(f1, f1),
        ),
        fstar::uint128::mul_wide(d4, f3),
    );
    let s3: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f3),
            fstar::uint128::mul_wide(d1, f2),
        ),
        fstar::uint128::mul_wide(f4, d419),
    );
    let s4: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f4),
            fstar::uint128::mul_wide(d1, f3),
        ),
        fstar::uint128::mul_wide(f2, f2),
    );
    let o0: fstar::uint128::uint128 = s0;
    let o1: fstar::uint128::uint128 = s1;
    let o2: fstar::uint128::uint128 = s2;
    let o3: fstar::uint128::uint128 = s3;
    let o4: fstar::uint128::uint128 = s4;
    let l·: fstar::uint128::uint128 =
        fstar::uint128::add(o0, fstar::uint128::uint64_to_uint128(0u64));
    let tmp0: u64 = fstar::uint128::uint128_to_uint64(l·) & 0x7ffffffffffffu64;
    let c0: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·, 51u32));
    let l·0: fstar::uint128::uint128 =
        fstar::uint128::add(o1, fstar::uint128::uint64_to_uint128(c0));
    let tmp1: u64 = fstar::uint128::uint128_to_uint64(l·0) & 0x7ffffffffffffu64;
    let c1: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·0, 51u32));
    let l·1: fstar::uint128::uint128 =
        fstar::uint128::add(o2, fstar::uint128::uint64_to_uint128(c1));
    let tmp2: u64 = fstar::uint128::uint128_to_uint64(l·1) & 0x7ffffffffffffu64;
    let c2: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·1, 51u32));
    let l·2: fstar::uint128::uint128 =
        fstar::uint128::add(o3, fstar::uint128::uint64_to_uint128(c2));
    let tmp3: u64 = fstar::uint128::uint128_to_uint64(l·2) & 0x7ffffffffffffu64;
    let c3: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·2, 51u32));
    let l·3: fstar::uint128::uint128 =
        fstar::uint128::add(o4, fstar::uint128::uint64_to_uint128(c3));
    let tmp4: u64 = fstar::uint128::uint128_to_uint64(l·3) & 0x7ffffffffffffu64;
    let c4: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·3, 51u32));
    let l·4: u64 = tmp0.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let o00: u64 = tmp0·;
    let o10: u64 = tmp1.wrapping_add(c5);
    let o20: u64 = tmp2;
    let o30: u64 = tmp3;
    let o40: u64 = tmp4;
    out[0usize] = o00;
    out[1usize] = o10;
    out[2usize] = o20;
    out[3usize] = o30;
    out[4usize] = o40
}

#[inline]
pub fn fsqr2(out: &mut [u64], f: &[u64], uu___: &[fstar::uint128::uint128]) {
    lowstar::ignore::ignore::<&[fstar::uint128::uint128]>(uu___);
    let f10: u64 = f[0usize];
    let f11: u64 = f[1usize];
    let f12: u64 = f[2usize];
    let f13: u64 = f[3usize];
    let f14: u64 = f[4usize];
    let f20: u64 = f[5usize];
    let f21: u64 = f[6usize];
    let f22: u64 = f[7usize];
    let f23: u64 = f[8usize];
    let f24: u64 = f[9usize];
    let d0: u64 = 2u64.wrapping_mul(f10);
    let d1: u64 = 2u64.wrapping_mul(f11);
    let d2: u64 = 38u64.wrapping_mul(f12);
    let d3: u64 = 19u64.wrapping_mul(f13);
    let d419: u64 = 19u64.wrapping_mul(f14);
    let d4: u64 = 2u64.wrapping_mul(d419);
    let s0: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(f10, f10),
            fstar::uint128::mul_wide(d4, f11),
        ),
        fstar::uint128::mul_wide(d2, f13),
    );
    let s1: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f11),
            fstar::uint128::mul_wide(d4, f12),
        ),
        fstar::uint128::mul_wide(d3, f13),
    );
    let s2: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f12),
            fstar::uint128::mul_wide(f11, f11),
        ),
        fstar::uint128::mul_wide(d4, f13),
    );
    let s3: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f13),
            fstar::uint128::mul_wide(d1, f12),
        ),
        fstar::uint128::mul_wide(f14, d419),
    );
    let s4: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d0, f14),
            fstar::uint128::mul_wide(d1, f13),
        ),
        fstar::uint128::mul_wide(f12, f12),
    );
    let o10: fstar::uint128::uint128 = s0;
    let o11: fstar::uint128::uint128 = s1;
    let o12: fstar::uint128::uint128 = s2;
    let o13: fstar::uint128::uint128 = s3;
    let o14: fstar::uint128::uint128 = s4;
    let d00: u64 = 2u64.wrapping_mul(f20);
    let d10: u64 = 2u64.wrapping_mul(f21);
    let d20: u64 = 38u64.wrapping_mul(f22);
    let d30: u64 = 19u64.wrapping_mul(f23);
    let d4190: u64 = 19u64.wrapping_mul(f24);
    let d40: u64 = 2u64.wrapping_mul(d4190);
    let s00: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(f20, f20),
            fstar::uint128::mul_wide(d40, f21),
        ),
        fstar::uint128::mul_wide(d20, f23),
    );
    let s10: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d00, f21),
            fstar::uint128::mul_wide(d40, f22),
        ),
        fstar::uint128::mul_wide(d30, f23),
    );
    let s20: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d00, f22),
            fstar::uint128::mul_wide(f21, f21),
        ),
        fstar::uint128::mul_wide(d40, f23),
    );
    let s30: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d00, f23),
            fstar::uint128::mul_wide(d10, f22),
        ),
        fstar::uint128::mul_wide(f24, d4190),
    );
    let s40: fstar::uint128::uint128 = fstar::uint128::add(
        fstar::uint128::add(
            fstar::uint128::mul_wide(d00, f24),
            fstar::uint128::mul_wide(d10, f23),
        ),
        fstar::uint128::mul_wide(f22, f22),
    );
    let o20: fstar::uint128::uint128 = s00;
    let o21: fstar::uint128::uint128 = s10;
    let o22: fstar::uint128::uint128 = s20;
    let o23: fstar::uint128::uint128 = s30;
    let o24: fstar::uint128::uint128 = s40;
    let l·: fstar::uint128::uint128 =
        fstar::uint128::add(o10, fstar::uint128::uint64_to_uint128(0u64));
    let tmp0: u64 = fstar::uint128::uint128_to_uint64(l·) & 0x7ffffffffffffu64;
    let c0: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·, 51u32));
    let l·0: fstar::uint128::uint128 =
        fstar::uint128::add(o11, fstar::uint128::uint64_to_uint128(c0));
    let tmp1: u64 = fstar::uint128::uint128_to_uint64(l·0) & 0x7ffffffffffffu64;
    let c1: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·0, 51u32));
    let l·1: fstar::uint128::uint128 =
        fstar::uint128::add(o12, fstar::uint128::uint64_to_uint128(c1));
    let tmp2: u64 = fstar::uint128::uint128_to_uint64(l·1) & 0x7ffffffffffffu64;
    let c2: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·1, 51u32));
    let l·2: fstar::uint128::uint128 =
        fstar::uint128::add(o13, fstar::uint128::uint64_to_uint128(c2));
    let tmp3: u64 = fstar::uint128::uint128_to_uint64(l·2) & 0x7ffffffffffffu64;
    let c3: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·2, 51u32));
    let l·3: fstar::uint128::uint128 =
        fstar::uint128::add(o14, fstar::uint128::uint64_to_uint128(c3));
    let tmp4: u64 = fstar::uint128::uint128_to_uint64(l·3) & 0x7ffffffffffffu64;
    let c4: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·3, 51u32));
    let l·4: u64 = tmp0.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let o101: u64 = tmp0·;
    let o111: u64 = tmp1.wrapping_add(c5);
    let o121: u64 = tmp2;
    let o131: u64 = tmp3;
    let o141: u64 = tmp4;
    let l·5: fstar::uint128::uint128 =
        fstar::uint128::add(o20, fstar::uint128::uint64_to_uint128(0u64));
    let tmp00: u64 = fstar::uint128::uint128_to_uint64(l·5) & 0x7ffffffffffffu64;
    let c00: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·5, 51u32));
    let l·6: fstar::uint128::uint128 =
        fstar::uint128::add(o21, fstar::uint128::uint64_to_uint128(c00));
    let tmp10: u64 = fstar::uint128::uint128_to_uint64(l·6) & 0x7ffffffffffffu64;
    let c10: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·6, 51u32));
    let l·7: fstar::uint128::uint128 =
        fstar::uint128::add(o22, fstar::uint128::uint64_to_uint128(c10));
    let tmp20: u64 = fstar::uint128::uint128_to_uint64(l·7) & 0x7ffffffffffffu64;
    let c20: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·7, 51u32));
    let l·8: fstar::uint128::uint128 =
        fstar::uint128::add(o23, fstar::uint128::uint64_to_uint128(c20));
    let tmp30: u64 = fstar::uint128::uint128_to_uint64(l·8) & 0x7ffffffffffffu64;
    let c30: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·8, 51u32));
    let l·9: fstar::uint128::uint128 =
        fstar::uint128::add(o24, fstar::uint128::uint64_to_uint128(c30));
    let tmp40: u64 = fstar::uint128::uint128_to_uint64(l·9) & 0x7ffffffffffffu64;
    let c40: u64 = fstar::uint128::uint128_to_uint64(fstar::uint128::shift_right(l·9, 51u32));
    let l·10: u64 = tmp00.wrapping_add(c40.wrapping_mul(19u64));
    let tmp0·0: u64 = l·10 & 0x7ffffffffffffu64;
    let c50: u64 = l·10.wrapping_shr(51u32);
    let o201: u64 = tmp0·0;
    let o211: u64 = tmp10.wrapping_add(c50);
    let o221: u64 = tmp20;
    let o231: u64 = tmp30;
    let o241: u64 = tmp40;
    let o100: u64 = o101;
    let o110: u64 = o111;
    let o120: u64 = o121;
    let o130: u64 = o131;
    let o140: u64 = o141;
    let o200: u64 = o201;
    let o210: u64 = o211;
    let o220: u64 = o221;
    let o230: u64 = o231;
    let o240: u64 = o241;
    out[0usize] = o100;
    out[1usize] = o110;
    out[2usize] = o120;
    out[3usize] = o130;
    out[4usize] = o140;
    out[5usize] = o200;
    out[6usize] = o210;
    out[7usize] = o220;
    out[8usize] = o230;
    out[9usize] = o240
}

pub fn store_felem(u64s: &mut [u64], f: &[u64]) {
    let f0: u64 = f[0usize];
    let f1: u64 = f[1usize];
    let f2: u64 = f[2usize];
    let f3: u64 = f[3usize];
    let f4: u64 = f[4usize];
    let l·: u64 = f0.wrapping_add(0u64);
    let tmp0: u64 = l· & 0x7ffffffffffffu64;
    let c0: u64 = l·.wrapping_shr(51u32);
    let l·0: u64 = f1.wrapping_add(c0);
    let tmp1: u64 = l·0 & 0x7ffffffffffffu64;
    let c1: u64 = l·0.wrapping_shr(51u32);
    let l·1: u64 = f2.wrapping_add(c1);
    let tmp2: u64 = l·1 & 0x7ffffffffffffu64;
    let c2: u64 = l·1.wrapping_shr(51u32);
    let l·2: u64 = f3.wrapping_add(c2);
    let tmp3: u64 = l·2 & 0x7ffffffffffffu64;
    let c3: u64 = l·2.wrapping_shr(51u32);
    let l·3: u64 = f4.wrapping_add(c3);
    let tmp4: u64 = l·3 & 0x7ffffffffffffu64;
    let c4: u64 = l·3.wrapping_shr(51u32);
    let l·4: u64 = tmp0.wrapping_add(c4.wrapping_mul(19u64));
    let tmp0·: u64 = l·4 & 0x7ffffffffffffu64;
    let c5: u64 = l·4.wrapping_shr(51u32);
    let f01: u64 = tmp0·;
    let f11: u64 = tmp1.wrapping_add(c5);
    let f21: u64 = tmp2;
    let f31: u64 = tmp3;
    let f41: u64 = tmp4;
    let m0: u64 = fstar::uint64::gte_mask(f01, 0x7ffffffffffedu64);
    let m1: u64 = fstar::uint64::eq_mask(f11, 0x7ffffffffffffu64);
    let m2: u64 = fstar::uint64::eq_mask(f21, 0x7ffffffffffffu64);
    let m3: u64 = fstar::uint64::eq_mask(f31, 0x7ffffffffffffu64);
    let m4: u64 = fstar::uint64::eq_mask(f41, 0x7ffffffffffffu64);
    let mask: u64 = m0 & m1 & m2 & m3 & m4;
    let f0·: u64 = f01.wrapping_sub(mask & 0x7ffffffffffedu64);
    let f1·: u64 = f11.wrapping_sub(mask & 0x7ffffffffffffu64);
    let f2·: u64 = f21.wrapping_sub(mask & 0x7ffffffffffffu64);
    let f3·: u64 = f31.wrapping_sub(mask & 0x7ffffffffffffu64);
    let f4·: u64 = f41.wrapping_sub(mask & 0x7ffffffffffffu64);
    let f02: u64 = f0·;
    let f12: u64 = f1·;
    let f22: u64 = f2·;
    let f32: u64 = f3·;
    let f42: u64 = f4·;
    let o0: u64 = f02 | f12.wrapping_shl(51u32);
    let o1: u64 = f12.wrapping_shr(13u32) | f22.wrapping_shl(38u32);
    let o2: u64 = f22.wrapping_shr(26u32) | f32.wrapping_shl(25u32);
    let o3: u64 = f32.wrapping_shr(39u32) | f42.wrapping_shl(12u32);
    let o00: u64 = o0;
    let o10: u64 = o1;
    let o20: u64 = o2;
    let o30: u64 = o3;
    u64s[0usize] = o00;
    u64s[1usize] = o10;
    u64s[2usize] = o20;
    u64s[3usize] = o30
}

#[inline]
pub fn cswap2(bit: u64, p1: &mut [u64], p2: &mut [u64]) {
    let mask: u64 = 0u64.wrapping_sub(bit);
    krml::unroll_for!(10, "i", 0u32, 1u32, {
        let dummy: u64 = mask & (p1[i as usize] ^ p2[i as usize]);
        p1[i as usize] ^= dummy;
        p2[i as usize] ^= dummy
    })
}