//! hybrid_zeckendorf_fib.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.FibIdentities
//!
//! Fibonacci recurrence and lazy per-level evaluation helpers.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

/// Standard Fibonacci: `fib(0) = 0`, `fib(1) = 1`,
/// `fib(n+2) = fib(n) + fib(n+1)`.
///
/// Matches Mathlib's `Nat.fib` definition.
pub fn fib(n: u32) -> u64 {
    match n {
        0 => 0,
        1 => 1,
        _ => {
            let (mut a, mut b) = (0u64, 1u64);
            for _ in 2..=n {
                let c = a + b;
                a = b;
                b = c;
            }
            b
        }
    }
}

/// Evaluate a lazy Zeckendorf payload by summing Fibonacci values of indices.
///
/// (Lean: `lazyEvalFib`)
///
/// # Arguments
/// * `indices` — Fibonacci indices (duplicates/consecutives allowed)
///
/// # Returns
/// `Σ fib(indices[i])`
pub fn lazy_eval_fib(indices: &[u32]) -> u64 {
    indices.iter().map(|&idx| fib(idx)).sum()
}

/// Append two lazy payloads (concatenation).
///
/// (Lean theorem: `lazyEvalFib_append` — eval of append = sum of evals)
pub fn lazy_append(a: &[u32], b: &[u32]) -> Vec<u32> {
    let mut out = Vec::with_capacity(a.len() + b.len());
    out.extend_from_slice(a);
    out.extend_from_slice(b);
    out
}

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

    #[test]
    fn test_fib_values() {
        assert_eq!(fib(0), 0);
        assert_eq!(fib(1), 1);
        assert_eq!(fib(2), 1);
        assert_eq!(fib(3), 2);
        assert_eq!(fib(10), 55);
    }

    #[test]
    fn test_lazy_eval() {
        assert_eq!(lazy_eval_fib(&[]), 0);
        assert_eq!(lazy_eval_fib(&[3]), 2);
        assert_eq!(lazy_eval_fib(&[5, 3]), fib(5) + fib(3));
    }

    #[test]
    fn test_append_preserves_eval() {
        let a = vec![3u32, 5];
        let b = vec![7u32];
        let ab = lazy_append(&a, &b);
        assert_eq!(lazy_eval_fib(&ab), lazy_eval_fib(&a) + lazy_eval_fib(&b));
    }
}