//! # coprime
//!
//! Zero-dependency, `no_std`, `u64` number theory and modular arithmetic on
//! **public, secret-free** values, with **no constant-time guarantees** (that is
//! later-stage work). This is **Stage One** — the foundation later layers build
//! on.
//!
//! Correctness is held to a five-tier test harness — doctest, exhaustive/KAT,
//! differential vs. an independent oracle, and coverage-guided fuzz — plus **two
//! formal tools**: Kani bounded model checking on the real compiled code, and
//! Aeneas → Lean/Mathlib unbounded proofs. The two legs are mostly not yet
//! congruent (`isqrt` is the exception: both verify the same clauses),
//! and not every function carries a proof; see `VERIFICATION.md` for the
//! per-function matrix and the exact scope of each claim (notably `is_prime`,
//! whose Lean proof is soundness-only).
//!
//! Stage One begins at the Euclidean root: [`number::gcd`] and
//! [`number::extended_gcd`], then modular exponentiation [`number::modpow`], the
//! modular inverse [`number::modinv`], deterministic primality
//! [`number::is_prime`], the Chinese remainder theorem [`number::crt`], and
//! prime generation [`number::next_prime`] / [`number::random_prime`].
#![cfg_attr(not(test), no_std)]
// The empirical no-panic floor: the product path carries no
// `unwrap`/`expect`/`panic!`/`unreachable!`/`todo!` — a panic on any input is a
// bug, so the lint denies them rather than trusting review to catch a
// regression. The clippy denies are enforced by `cargo clippy`, where `cfg(kani)`
// is unset so `not(test)` is exactly the product path; they are gated `not(test)`
// so test/oracle code (which uses `expect`/asserts freely) is unaffected. Under
// `cargo kani` the clippy lints are inert (no clippy driver runs); there the
// proof bodies hold the line themselves with `kani::assert`, and the ungated
// `missing_docs` keeps every public item documented.
// `arithmetic_side_effects` is deliberately *not* in the floor: in
// this crate the arithmetic is the proven subject (overflow-safety established
// by `u128`/`i128` widening + the per-function bound proofs), so a blanket deny
// plus ubiquitous `#[allow]` would obscure rather than document.
#![cfg_attr(
    not(test),
    deny(
        clippy::unwrap_used,
        clippy::expect_used,
        clippy::panic,
        clippy::unreachable,
        clippy::todo
    )
)]
#![deny(missing_docs)]

pub mod number;

// Kani proofs live in `proofs/`, gated on `cfg(kani)` and `#[path]`-included here
// so they reach crate-internal items via `crate::`. They are invisible to normal
// builds, tests, and clippy. Run with `cargo kani -p coprime`.
#[cfg(kani)]
#[path = "../proofs/extended_gcd_bezout.rs"]
mod extended_gcd_bezout_proofs;

#[cfg(kani)]
#[path = "../proofs/lcm_identity.rs"]
mod lcm_identity_proofs;

#[cfg(kani)]
#[path = "../proofs/modpow_naive.rs"]
mod modpow_naive_proofs;

#[cfg(kani)]
#[path = "../proofs/modinv_invariant.rs"]
mod modinv_invariant_proofs;

#[cfg(kani)]
#[path = "../proofs/jacobi_multiplicative.rs"]
mod jacobi_multiplicative_proofs;

#[cfg(kani)]
#[path = "../proofs/isqrt_floor.rs"]
mod isqrt_floor_proofs;

#[cfg(kani)]
#[path = "../proofs/kronecker_jacobi.rs"]
mod kronecker_jacobi_proofs;

#[cfg(kani)]
#[path = "../proofs/iroot_floor.rs"]
mod iroot_floor_proofs;

#[cfg(kani)]
#[path = "../proofs/cfrac_convergents.rs"]
mod cfrac_convergents_proofs;

#[cfg(kani)]
#[path = "../proofs/factor_sort.rs"]
mod factor_sort_proofs;

#[cfg(kani)]
#[path = "../proofs/factorize_correct.rs"]
mod factorize_correct_proofs;

#[cfg(kani)]
#[path = "../proofs/gcd_correct.rs"]
mod gcd_correct_proofs;

#[cfg(kani)]
#[path = "../proofs/mulmod_widening.rs"]
mod mulmod_widening_proofs;

#[cfg(kani)]
#[path = "../proofs/sprp_soundness.rs"]
mod sprp_soundness_proofs;

#[cfg(kani)]
#[path = "../proofs/next_prime_smallest.rs"]
mod next_prime_smallest_proofs;

#[cfg(kani)]
#[path = "../proofs/crt2_congruences.rs"]
mod crt2_congruences_proofs;
