Function Hacl_GenericField64_field_modulus_check 

pub unsafe extern "C" fn Hacl_GenericField64_field_modulus_check(
    len: u32,
    n: *mut u64,
) -> bool

A verified field arithmetic library.

This is a 64-bit optimized version, where bignums are represented as an array of len unsigned 64-bit integers, i.e. uint64_t[len].

All the arithmetic operations are performed in the Montgomery domain.

All the functions below preserve the following invariant for a bignum aM in Montgomery form. • aM < n