Function fiat_crypto::p448_solinas_64::fiat_p448_carry

pub fn fiat_p448_carry(out1: &mut [u64; 8], arg1: &[u64; 8])

The function fiat_p448_carry reduces a field element. Postconditions: eval out1 mod m = eval arg1 mod m

Input Bounds: arg1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]] Output Bounds: out1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]