pub unsafe extern "C" fn Hacl_Bignum256_mont_ctx_init( n: *mut u64, ) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64