// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Nucleus.FixedPoints
// Theorem preserved: fixedPoints_finite, fixedPoints_monotone

use crate::padic_rounding::{depth_restrict, DepthState};

/// Check if S is a fixed point at depth k: depthRestrict(k, S) = S
/// Semantically: S and depthRestrict(k, S) agree on all indices,
/// treating out-of-bounds positions as false.
pub fn is_fixed_point(p: u64, k: u32, s: &DepthState) -> bool {
    let restricted = depth_restrict(p, k, s);
    let len = restricted.capacity().max(s.capacity());
    for i in 0..len {
        let a = restricted.members.get(i).copied().unwrap_or(false);
        let b = s.members.get(i).copied().unwrap_or(false);
        if a != b {
            return false;
        }
    }
    true
}

/// Theorem preserved: fixedPoints_finite
/// |fixedPointsAtDepth(k)| < ∞
/// The number of fixed-point subsets at depth k is at most 2^(p^k).
pub fn fixed_points_upper_bound(p: u64, k: u32) -> u64 {
    let skel_sz = p.pow(k);
    if skel_sz >= 64 {
        u64::MAX
    } else {
        1u64 << skel_sz
    }
}

/// Theorem preserved: fixedPoints_monotone
/// k₁ ≤ k₂ ⟹ fix(k₁) ⊆ fix(k₂)
pub fn check_monotone(p: u64, k1: u32, k2: u32, s: &DepthState) -> bool {
    if k1 > k2 {
        return true; // precondition not met
    }
    if !is_fixed_point(p, k1, s) {
        return true; // not in fix(k1), vacuously true
    }
    is_fixed_point(p, k2, s)
}

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

    #[test]
    fn upper_bound() {
        assert_eq!(fixed_points_upper_bound(2, 3), 256); // 2^(2^3) = 2^8
    }

    #[test]
    fn fixed_within_skeleton() {
        // State with support {0,1} within skeleton {0..7} is fixed at depth 3
        let mut s = DepthState::new(8);
        s.members[0] = true;
        s.members[1] = true;
        assert!(is_fixed_point(2, 3, &s));
    }

    #[test]
    fn monotone() {
        // State must have capacity matching the smaller skeleton (p^k1 = 4)
        // and be a fixed point at depth k1=2 to test monotonicity
        let mut s = DepthState::new(4);
        s.members[0] = true;
        s.members[1] = true;
        // Fixed at k1=2 (capacity == skeleton size), must be fixed at k2=3
        assert!(is_fixed_point(2, 2, &s));
        assert!(check_monotone(2, 2, 3, &s));
    }
}