Function fiat_crypto::secp256k1_montgomery_scalar_32::fiat_secp256k1_montgomery_scalar_divstep_precomp

pub fn fiat_secp256k1_montgomery_scalar_divstep_precomp(out1: &mut [u32; 8])

The function fiat_secp256k1_montgomery_scalar_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 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]