Function Hacl_GenericField32_field_modulus_check 

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

A verified field arithmetic library.

This is a 32-bit optimized version, where bignums are represented as an array of len unsigned 32-bit integers, i.e. uint32_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