//! hybrid_zeckendorf_add.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.Addition
//!
//! Lazy level-wise addition with correctness.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → C → Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_eval::{HybridNumber, Payload, MAX_LEVELS};
use crate::hybrid_zeckendorf_normalize::normalize;

/// Lazy addition: per-level payload merge (concatenation).
///
/// (Lean: `addLazy A B = A + B`, where addition is `List.append` per level)
///
/// Theorem preserved: `addLazy_eval` — `lazyEval(addLazy A B) = lazyEval A + lazyEval B`
pub fn add_lazy(a: &HybridNumber, b: &HybridNumber) -> HybridNumber {
    let mut out = HybridNumber::zero();
    for i in 0..MAX_LEVELS {
        let mut merged = a.levels[i].indices.clone();
        merged.extend_from_slice(&b.levels[i].indices);
        out.levels[i] = Payload::from_indices(merged);
    }
    out
}

/// Canonical addition: lazy merge followed by normalization.
///
/// (Lean: `add A B = normalize (addLazy (toLazy A) (toLazy B))`)
///
/// Theorem preserved: `add_correct` — `eval(add A B) = eval A + eval B`
/// Theorem preserved: `add_comm_eval` — `eval(add A B) = eval(add B A)`
pub fn add(a: &HybridNumber, b: &HybridNumber) -> HybridNumber {
    let lazy_sum = add_lazy(a, b);
    normalize(&lazy_sum)
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::hybrid_zeckendorf_eval::{eval, from_nat};

    #[test]
    fn test_add_correct() {
        let a = from_nat(789);
        let b = from_nat(456);
        let sum = add(&a, &b);
        assert_eq!(eval(&sum), 789 + 456);
    }

    #[test]
    fn test_add_commutative() {
        let a = from_nat(42);
        let b = from_nat(99);
        assert_eq!(eval(&add(&a, &b)), eval(&add(&b, &a)));
    }
}