Function fiat_crypto::p384_64::fiat_p384_divstep_precomp

pub fn fiat_p384_divstep_precomp(out1: &mut [u64; 6])

The function fiat_p384_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).

Postconditions: eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋) 0 ≤ eval out1 < m

Output Bounds: out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]