//! hybrid_zeckendorf_nucleus.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.NucleusBridge
//!
//! Bridge lemmas connecting HybridZeckendorf normalization/carry to
//! closure-style (Nucleus) semantics. Proves normalization is an
//! idempotent closure operator.
//!
//! Provenance: Lean 4 -> LambdaIR -> MiniC -> C -> Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_eval::{eval, HybridNumber, MAX_LEVELS};
use crate::hybrid_zeckendorf_fib::lazy_eval_fib;
use crate::hybrid_zeckendorf_normalize::{normalize, carry_at};
use crate::hybrid_zeckendorf_uniqueness::repr_equal;
use crate::hybrid_zeckendorf_weight::weight;

/// Check carry-at idempotence: `carryAt(i, carryAt(i, X)) = carryAt(i, X)`.
///
/// (Lean: `carryAt_idempotent`)
///
/// Proof: both sides are canonical (carryAt_preserves_canonical applied
/// twice). Their weighted evaluations agree at every level (carryAt is
/// eval-preserving + Euclidean division is idempotent on remainders).
/// `canonical_eval_injective` gives representational equality.
pub fn carry_at_idempotent_check(i: usize, x: &HybridNumber) -> bool {
    let mut once = x.clone();
    carry_at(i, &mut once);

    let mut twice = once.clone();
    carry_at(i, &mut twice);

    repr_equal(&once, &twice)
}

/// Check eval-level monotonicity of carry.
///
/// (Lean: `carryAt_eval_monotone`)
///
/// Given `forall j, levelEval(X_j) <= levelEval(Y_j)`,
/// then `eval(carryAt(i, X)) <= eval(carryAt(i, Y))`.
///
/// This is the strongest monotonicity available. Pointwise representational
/// monotonicity FAILS (see `carryAt_not_pointwise_monotone` in Lean).
pub fn carry_eval_monotone_check(
    i: usize,
    x: &HybridNumber,
    y: &HybridNumber,
) -> bool {
    let mut cx = x.clone();
    let mut cy = y.clone();
    carry_at(i, &mut cx);
    carry_at(i, &mut cy);
    eval(&cx) <= eval(&cy)
}

/// Check normalization closure: `normalize(normalize(X)) = normalize(X)`.
///
/// (Lean: `normalize_is_closure_operator`)
///
/// This is the key property connecting normalization to nucleus semantics.
/// The proof composes:
///   1. `normalizeIntra_of_canonical`: intra-normalization is identity on
///      canonical input.
///   2. `interCarry_idempotent_of_canonical`: the ascending carry pass is
///      idempotent because all levels are already carry-normal after the
///      first pass (`levelEval < weight` at every positive level).
pub fn normalize_closure_check(x: &HybridNumber) -> bool {
    let first = normalize(x);
    let second = normalize(&first);
    repr_equal(&first, &second)
}

/// Check carry-normal form: every positive level satisfies
/// `levelEval < weight` after normalization.
///
/// (Lean: `interCarryLoop_small`)
pub fn is_carry_normal(x: &HybridNumber) -> bool {
    for i in 1..MAX_LEVELS {
        let le = lazy_eval_fib(&x.levels[i].indices);
        let wi = weight(i as u32);
        if le >= wi {
            return false;
        }
    }
    true
}

/// Check below-threshold identity: if `levelEval(X_i) < weight(i)`,
/// then `carryAt(i, X) = X` (no carry needed).
///
/// (Lean: `carryAt_eq_self_of_small`)
pub fn carry_noop_check(i: usize, x: &HybridNumber) -> bool {
    let le = lazy_eval_fib(&x.levels[i].indices);
    let wi = weight(i as u32);
    if le >= wi {
        return false; // not below threshold
    }

    let mut copy = x.clone();
    carry_at(i, &mut copy);
    repr_equal(x, &copy)
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::hybrid_zeckendorf_eval::from_nat;
    use crate::hybrid_zeckendorf_normalize::normalize;

    #[test]
    fn test_normalize_is_closure() {
        for n in [0u64, 1, 42, 999, 12345, 999999] {
            let x = from_nat(n);
            assert!(
                normalize_closure_check(&x),
                "closure failed for n={n}"
            );
        }
    }

    #[test]
    fn test_carry_normal_after_normalize() {
        let x = from_nat(123456);
        let norm = normalize(&x);
        assert!(is_carry_normal(&norm));
    }

    #[test]
    fn test_carry_idempotent() {
        let x = from_nat(54321);
        for i in 1..MAX_LEVELS {
            assert!(
                carry_at_idempotent_check(i, &x),
                "carry idempotence failed at level {i}"
            );
        }
    }
}