pub unsafe extern "C" fn Hacl_Bignum32_mod_precomp( k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, a: *mut u32, res: *mut u32, )