//! Constructive primality proofs — Pratt certificates.
//!
//! Unlike [`is_prime`](crate::number::is_prime) (the cited twelve-base witness
//! set) and [`bpsw`](crate::number::bpsw) (an empirical no-counterexample
//! result), a Pratt certificate is a *constructive proof* that a specific `n` is
//! prime. It is a deduplicated tree: each node names a prime `value`, a witness
//! base, and the distinct primes of `value − 1` (its children, themselves
//! certified), bottoming out at the atom `2`. For each child prime `q`, the
//! witness satisfies the Pocklington conditions, which force every prime divisor
//! of `value` to `≡ 1 (mod value − 1)` — pinning the only divisor at `value`
//! (Pratt 1975; Pocklington 1914; Brillhart, Lehmer & Selfridge, Math. Comp. 1975).
//!
//! [`verify_certificate`] re-checks a certificate with **modular exponentiation
//! alone** — it never calls [`factorize`] or any other primality test, and never
//! trusts that a factor is prime: it re-derives factor-completeness by division
//! and certifies each factor recursively from the tree. So its soundness is
//! self-contained, depending on neither `DET12` nor the Feitsma enumeration.
//!
//! The verifier is **machine-checked end to end**: `verify-lean/Coprime/`
//! extracts [`verify_certificate`] and its loops (Aeneas→Lean) and proves
//! (`CertificateVerifySpec.lean`, `verify_certificate_spec`, axiom-clean) that
//! an accepting run implies primality — for *any* certificate value, with no
//! well-formedness hypotheses — by induction over the nodes, each discharged
//! through the proved Pocklington criterion (`Pocklington.lean`,
//! `pocklington_prime`) via the extracted witness check (`CertificateSpec.lean`,
//! `is_witness_spec`). (The recursive tree structure mirrors Wimmer &
//! Noschinski's formalization of Pratt's system, *J. Automated Reasoning*
//! 2020.)

use crate::number::{bpsw, factorize, gcd, modpow};

/// Cap on the per-prime witness search. For a prime `n`, a base passing
/// [`is_witness`] for *every* distinct prime of `n − 1` is exactly a **primitive
/// root** of `n`, so the search's reach is the least-primitive-root question.
/// Primitive roots are dense (`φ(n−1)/(n−1) ≫ 1/log log n` of all bases), and the
/// least one sits orders of magnitude below this cap in every published
/// tabulation — but **no theorem puts it below the cap for every `u64` prime**:
/// the unconditional Burgess bound is `O(p^{1/4+ε})`, GRH-conditional bounds are
/// polylog-but-asymptotic, and enumerating ~4·10¹⁷ primes is not a computation
/// anyone has done (see PAPERS.md). So the completeness claim is *empirical*,
/// pinned in-repo by `certificate_completeness_sweep`. The cap is **fail-safe**:
/// it never weakens an acceptance (a found witness is a proof regardless); a
/// prime whose least primitive root exceeded it would get `None` — a
/// completeness miss, never an unsound accept.
const WITNESS_CAP: u64 = 4096;

/// Capacity of a certificate tree. With deduplication, the distinct primes in the
/// recursive factor chains of `n − 1` for a `u64` prime stay far under this in
/// every observed case (the sweep's trees run dozens of nodes at most), but like
/// [`WITNESS_CAP`] the headroom is empirical, not a theorem — and fail-safe:
/// overflow returns `None`, never an unsound accept.
const MAX_NODES: usize = 128;

/// `gcd(aᵉ − 1, n)`, formed from `aᵉ mod n` (so `aᵉ − 1 ≡ (aᵉ mod n) − 1`, with
/// `aᵉ ≡ 0` giving `n − 1`). A value strictly between `1` and `n` is a proper
/// factor of `n` — i.e. a compositeness proof — but the caller only needs the
/// `= 1` case, so the gcd is returned as is.
fn gcd_pow_minus_one(a: u64, e: u64, n: u64) -> u64 {
    let ae = modpow(a, e, n);
    let d = if ae == 0 { n - 1 } else { ae - 1 };
    gcd(d, n)
}

/// Does base `a` witness `n`'s primality for the prime factor `q` of `n − 1`? —
/// the Pocklington conditions `a^(n−1) ≡ 1 (mod n)` and
/// `gcd(a^((n−1)/q) − 1, n) = 1`.
fn is_witness(n: u64, q: u64, a: u64) -> bool {
    let nm1 = n - 1;
    modpow(a, nm1, n) == 1 && gcd_pow_minus_one(a, nm1 / q, n) == 1
}

/// One node of a Pratt certificate tree. `value` is prime because, for each
/// distinct prime `q` of `value − 1` — the `children` (indices of earlier nodes
/// that certify those `q`) — the single `witness` satisfies `is_witness`. The
/// atom is `value == 2` (`n_children == 0`).
#[derive(Clone, Copy, Debug)]
struct PrattNode {
    value: u64,
    witness: u64,
    children: [u8; 15],
    n_children: u8,
}

const ATOM: PrattNode = PrattNode {
    value: 0,
    witness: 0,
    children: [0; 15],
    n_children: 0,
};

/// A **Pratt certificate** for `n`: a deduplicated, post-order tree of nodes whose
/// root (the last node) is `n`, bottoming out at the atom `2`. Construct with
/// [`prime_certificate`], re-check with [`verify_certificate`]. Verification is
/// self-contained — it trusts nothing but modular arithmetic.
#[derive(Clone, Copy, Debug)]
pub struct PrimalityCertificate {
    nodes: [PrattNode; MAX_NODES],
    len: usize,
}

impl PrimalityCertificate {
    /// The certified prime values, in verification (post-order) order; the last is
    /// the certificate.s root `n`.
    pub fn primes(&self) -> impl Iterator<Item = u64> + '_ {
        self.nodes[..self.len].iter().map(|node| node.value)
    }

    /// Index of an already-built node for `value`, for deduplication.
    fn find(&self, value: u64) -> Option<usize> {
        self.nodes[..self.len]
            .iter()
            .position(|node| node.value == value)
    }

    fn push(&mut self, node: PrattNode) -> Option<usize> {
        if self.len >= MAX_NODES {
            return None;
        }
        self.nodes[self.len] = node;
        let i = self.len;
        self.len += 1;
        Some(i)
    }

    /// Decode arbitrary fuzzer bytes into a possibly-malformed certificate, for the
    /// `verify_certificate` hostile-input fuzz target (`coprime/fuzz`): it must
    /// never panic on, nor falsely accept, any byte string. Compiled **only** under
    /// `cargo fuzz` (`--cfg fuzzing`); absent from every normal and published build,
    /// so it widens no real API. The first byte sets the node count; each node then
    /// consumes its `value`, `witness`, child count (bounded to the array), and that
    /// many child indices — leaving forward/out-of-range indices, composite values,
    /// and wrong witnesses for the verifier to reject safely.
    #[cfg(fuzzing)]
    #[must_use]
    pub fn from_fuzz_bytes(data: &[u8]) -> Self {
        let g = |i: usize| data.get(i).copied().unwrap_or(0);
        let rd_u64 = |off: usize| (0..8).fold(0u64, |v, k| v | (u64::from(g(off + k)) << (8 * k)));
        let mut nodes = [ATOM; MAX_NODES];
        let count = (g(0) as usize) % (MAX_NODES + 1);
        let mut off = 1usize;
        for node in nodes.iter_mut().take(count) {
            let value = rd_u64(off);
            let witness = rd_u64(off + 8);
            let n_children = g(off + 16) % 16;
            off += 17;
            let mut children = [0u8; 15];
            for child in children.iter_mut().take(n_children as usize) {
                *child = g(off);
                off += 1;
            }
            *node = PrattNode {
                value,
                witness,
                children,
                n_children,
            };
        }
        PrimalityCertificate { nodes, len: count }
    }
}

/// A single base witnessing `n`'s primality for *every* distinct prime of `n − 1`
/// (a primitive root); `None` if none below the search cap.
fn find_witness(n: u64, primes: &[(u64, u32)]) -> Option<u64> {
    let cap = WITNESS_CAP.min(n);
    let mut a = 2u64;
    while a < cap {
        if primes.iter().all(|&(q, _)| is_witness(n, q, a)) {
            return Some(a);
        }
        a += 1;
    }
    None
}

/// Build the Pratt tree for `value` into `cert`, appending nodes post-order
/// (children before parents) with deduplication; returns the node index, or `None`
/// if `value` is composite or the tree would exceed `MAX_NODES`. Recursion is on
/// the prime factors of `value − 1`, each `< value`, so it terminates.
fn build(value: u64, cert: &mut PrimalityCertificate) -> Option<usize> {
    if let Some(i) = cert.find(value) {
        return Some(i);
    }
    if value == 2 {
        return cert.push(PrattNode { value: 2, ..ATOM });
    }
    if value < 2 || value.is_multiple_of(2) {
        return None;
    }
    let f = factorize(value - 1);
    let primes = f.as_slice();
    let mut children = [0u8; 15];
    let mut nc = 0usize;
    for &(q, _) in primes {
        let ci = build(q, cert)?;
        #[allow(clippy::cast_possible_truncation)] // ci < MAX_NODES = 128 fits u8
        let ci8 = ci as u8;
        children[nc] = ci8;
        nc += 1;
    }
    let witness = find_witness(value, primes)?;
    #[allow(clippy::cast_possible_truncation)] // nc <= 15 fits u8
    let nc8 = nc as u8;
    cert.push(PrattNode {
        value,
        witness,
        children,
        n_children: nc8,
    })
}

/// **Constructive primality test** — `true` iff `n` is prime, proved from the
/// ground up by constructing a Pratt certificate and re-verifying it. The `bpsw`
/// prefilter only rejects composites fast (every prime passes it — a theorem); the
/// certificate is what proves an acceptance, leaning on neither the twelve-base
/// witness set nor the Feitsma sweep. It is the *certifying* backstop, not the
/// hot-path test.
///
/// # Examples
///
/// ```
/// use coprime::number::is_prime_certified;
///
/// assert!(is_prime_certified(2_305_843_009_213_693_951)); // the Mersenne prime 2^61 − 1
/// assert!(!is_prime_certified(561)); // a Carmichael number
/// assert!(!is_prime_certified(2047)); // 23 · 89, a base-2 strong pseudoprime
/// ```
#[must_use]
pub fn is_prime_certified(n: u64) -> bool {
    if n == 2 {
        return true;
    }
    if n < 2 || n.is_multiple_of(2) {
        return false;
    }
    // Sound prefilter: every prime passes bpsw, so !bpsw ⇒ composite.
    if !bpsw(n) {
        return false;
    }
    match prime_certificate(n) {
        Some(cert) => verify_certificate(n, &cert),
        None => false,
    }
}

/// Construct a Pratt certificate proving `n` prime, or `None` if `n` is composite
/// (a returned certificate is a proof — see [`verify_certificate`]; `None` for a
/// true prime would require a witness past the internal search cap or a tree past
/// `MAX_NODES` — never observed, but an empirical claim, not a theorem; such a
/// miss would be fail-safe, never an unsound accept — see `WITNESS_CAP`).
#[must_use]
pub fn prime_certificate(n: u64) -> Option<PrimalityCertificate> {
    let mut cert = PrimalityCertificate {
        nodes: [ATOM; MAX_NODES],
        len: 0,
    };
    build(n, &mut cert)?;
    Some(cert)
}

/// Re-verify a Pratt certificate for `n` using modular exponentiation alone:
/// `true` iff it proves `n` prime. Processes nodes in order; each node is either
/// the atom `2`, or has its `value` certified prime by (1) re-dividing `value − 1`
/// by its children's values down to `1` (completeness — those children *are* every
/// prime factor of `value − 1`), each child being an **earlier**, already-verified
/// node, and (2) a holding Pocklington `is_witness` for each. The root (last
/// node) must equal `n`. **Trusts nothing but arithmetic** — no [`factorize`], no
/// recursion into another primality test. Soundness is **machine-checked end to
/// end**: the Lean theorem `verify_certificate_spec` (this function extracted
/// Aeneas→Lean, axiom-clean) proves a `true` from this function implies `n` is
/// prime, for any certificate value.
///
/// # Examples
///
/// ```
/// use coprime::number::{prime_certificate, verify_certificate};
///
/// let n = 1_000_003; // prime
/// let cert = prime_certificate(n).expect("1_000_003 is prime");
/// assert!(verify_certificate(n, &cert));
/// ```
#[must_use]
pub fn verify_certificate(n: u64, cert: &PrimalityCertificate) -> bool {
    if cert.len == 0 {
        return false;
    }
    // `ok` accumulates "every node so far is valid" by AND — a flag rather than an
    // early `return` from inside the loop, the form the Aeneas→Lean extraction
    // models (a return that exits a loop *and* the function is not translatable);
    // do not "simplify" back to early returns. Behaviorally identical: a single
    // bad node forces `ok = false`, and the final result is `false`.
    let mut i = 0usize;
    let mut ok = true;
    while i < cert.len {
        if !verify_node(cert.nodes[i], cert, i) {
            ok = false;
        }
        i += 1;
    }
    ok && cert.nodes[cert.len - 1].value == n
}

/// Remove every factor of `f` from `m` (for `f >= 2`, so it terminates: `m`
/// strictly decreases while `f` divides it). Returns the `f`-free part of `m`.
fn divide_out(m: u64, f: u64) -> u64 {
    let mut m = m;
    while m.is_multiple_of(f) {
        m /= f;
    }
    m
}

/// Is node `i` (the `i`-th, given the earlier nodes) valid? — the atom `2`, or an
/// odd `value > 2` whose children are exactly the prime factors of `value − 1`
/// (dividing them out reaches `1`), each an **earlier** node (`< i`, already
/// verified) with `value >= 2`, and each carrying a holding [`is_witness`]. Uses
/// the same flag-not-`return` shape so the loop is Aeneas-extractable.
#[allow(clippy::many_single_char_names)] // m, j, f — loop scalars
fn verify_node(node: PrattNode, cert: &PrimalityCertificate, i: usize) -> bool {
    if node.value == 2 {
        return true;
    }
    if node.value < 2 || node.value.is_multiple_of(2) {
        return false;
    }
    let mut m = node.value - 1;
    let mut j = 0usize;
    let mut ok = true;
    while j < node.n_children as usize {
        let ci = node.children[j] as usize;
        if ci >= i {
            ok = false;
        } else {
            let f = cert.nodes[ci].value;
            if f < 2 {
                ok = false;
            } else {
                m = divide_out(m, f);
                if !is_witness(node.value, f, node.witness) {
                    ok = false;
                }
            }
        }
        j += 1;
    }
    ok && m == 1
}

#[cfg(test)]
mod tests {
    use super::{ATOM, MAX_NODES, PrattNode, PrimalityCertificate, verify_certificate};

    /// `verify_certificate` must reject a forged certificate — one not produced by
    /// [`super::build`] — that claims a composite is prime. Here a single node
    /// `value = 9` with no children: nothing divides `9 − 1 = 8` down to `1`, so
    /// the node fails its completeness check and verification returns `false`.
    /// (These fields are private, so this lives in-module; the public round-trip
    /// test in `number/tests.rs` cannot construct a malformed tree.)
    #[test]
    fn rejects_forged_certificate_for_composite() {
        let mut nodes = [ATOM; MAX_NODES];
        nodes[0] = PrattNode {
            value: 9,
            witness: 2,
            children: [0; 15],
            n_children: 0,
        };
        let forged = PrimalityCertificate { nodes, len: 1 };
        assert!(
            !verify_certificate(9, &forged),
            "verified a forged certificate for the composite 9"
        );
    }
}
