//! Tight bounds on assembly index: log₂(size) ≤ AI ≤ size - 1.
//!
//! Corresponds to AssemblyBounds.lean.

use crate::assembly_space::Obj;
use crate::assembly_index::assembly_index;

/// Floor of log₂(n) for n ≥ 1.
fn nat_log2(n: u32) -> u32 {
    if n <= 1 { return 0; }
    31 - n.leading_zeros()
}

/// Verify upper bound: AI ≤ size - 1.
///
/// Lean: `assemblyIndex_le_size_sub_one`
pub fn upper_bound_holds(o: &Obj) -> bool {
    assembly_index(o) <= o.size() - 1
}

/// Verify lower bound: log₂(size) ≤ AI (when size > 1).
///
/// Lean: `assemblyIndex_ge_log2`
pub fn lower_bound_holds(o: &Obj) -> bool {
    let sz = o.size();
    if sz <= 1 { return true; }
    nat_log2(sz) <= assembly_index(o)
}

/// Both bounds hold simultaneously.
///
/// Lean: `dagJoinCount_bounds`
pub fn both_bounds_hold(o: &Obj) -> bool {
    lower_bound_holds(o) && upper_bound_holds(o)
}

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

    fn base(a: u32) -> Obj { Obj::Base(a) }
    fn join(l: Obj, r: Obj) -> Obj { Obj::Join(Box::new(l), Box::new(r)) }

    #[test]
    fn bounds_primitive() {
        assert!(both_bounds_hold(&base(0)));
    }

    #[test]
    fn bounds_single_join() {
        assert!(both_bounds_hold(&join(base(0), base(1))));
    }

    #[test]
    fn bounds_chain() {
        let o = join(join(join(base(0), base(1)), base(2)), base(3));
        assert!(both_bounds_hold(&o));
    }

    #[test]
    fn bounds_with_reuse() {
        let ab = join(base(0), base(1));
        let o = join(ab.clone(), ab);
        assert!(both_bounds_hold(&o));
    }

    #[test]
    fn bounds_deep_tree() {
        // 8-leaf balanced tree: AI should be between log₂(8)=3 and 7
        let l1 = join(base(0), base(1));
        let l2 = join(base(2), base(3));
        let l3 = join(base(4), base(5));
        let l4 = join(base(6), base(7));
        let o = join(join(l1, l2), join(l3, l4));
        assert!(both_bounds_hold(&o));
    }

    #[test]
    fn nat_log2_values() {
        assert_eq!(super::nat_log2(1), 0);
        assert_eq!(super::nat_log2(2), 1);
        assert_eq!(super::nat_log2(4), 2);
        assert_eq!(super::nat_log2(8), 3);
        assert_eq!(super::nat_log2(7), 2); // floor
    }
}