//! hybrid_zeckendorf_weight.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.WeightSystem
//!
//! Weight hierarchy: w_0 = 1, w_1 = 1000, w_{i+2} = w_{i+1}^2
//! Closed form (i >= 1): w_i = 1000^{2^{i-1}}
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

/// Compute weight(i) for the hybrid hierarchy.
///
/// `w_0 = 1`, `w_1 = 1000`, `w_{i+2} = w_{i+1}^2`
///
/// # Overflow
/// Grows super-exponentially. For `i >= 3` the result overflows `u64`.
/// Use `checked_weight` for safe arithmetic, or big-integer types
/// for production use with large levels.
pub fn weight(i: u32) -> u64 {
    match i {
        0 => 1,
        1 => 1000,
        _ => {
            let mut prev: u64 = 1000;
            for _ in 2..=i {
                prev = prev.wrapping_mul(prev);
            }
            prev
        }
    }
}

/// Checked weight computation that returns `None` on overflow.
pub fn checked_weight(i: u32) -> Option<u64> {
    match i {
        0 => Some(1),
        1 => Some(1000),
        _ => {
            let mut prev: u64 = 1000;
            for _ in 2..=i {
                prev = prev.checked_mul(prev)?;
            }
            Some(prev)
        }
    }
}

/// Positivity: `weight(i) > 0` for all `i`.
///
/// (Lean theorem: `weight_pos`)
pub fn weight_pos(i: u32) -> bool {
    weight(i) > 0
}

/// Strict monotonicity: `weight(i) < weight(i+1)` for all `i`.
///
/// (Lean theorem: `weight_strict_mono`)
pub fn weight_lt_succ(i: u32) -> bool {
    weight(i) < weight(i + 1)
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_base_cases() {
        assert_eq!(weight(0), 1);
        assert_eq!(weight(1), 1000);
        assert_eq!(weight(2), 1_000_000);
    }

    #[test]
    fn test_positivity() {
        for i in 0..3 {
            assert!(weight_pos(i));
        }
    }

    #[test]
    fn test_monotonicity() {
        for i in 0..2 {
            assert!(weight_lt_succ(i));
        }
    }
}