// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Nucleus.PadicRounding
// Theorem preserved: depthRestrict_idempotent, roundedSkeleton_finite, padicDepthNucleus

/// DepthState: a set of p-adic integers represented as a bitset over residues mod p^k.
#[derive(Clone, Debug)]
pub struct DepthState {
    pub members: Vec<bool>,
}

impl DepthState {
    pub fn new(capacity: usize) -> Self {
        Self { members: vec![false; capacity] }
    }

    pub fn capacity(&self) -> usize {
        self.members.len()
    }
}

/// roundedSkeleton(p, k) = {0, 1, ..., p^k - 1}
pub fn rounded_skeleton_size(p: u64, k: u32) -> u64 {
    p.pow(k)
}

/// depthRestrict(k, S) = S ∩ roundedSkeleton(p, k)
pub fn depth_restrict(p: u64, k: u32, input: &DepthState) -> DepthState {
    let skel_sz = rounded_skeleton_size(p, k) as usize;
    let mut out = DepthState::new(skel_sz);
    for i in 0..skel_sz.min(input.capacity()) {
        out.members[i] = input.members[i];
    }
    out
}

/// Theorem preserved: depthRestrict_idempotent
/// depthRestrict(k, depthRestrict(k, S)) = depthRestrict(k, S)
pub fn check_idempotent(p: u64, k: u32, s: &DepthState) -> bool {
    let r1 = depth_restrict(p, k, s);
    let r2 = depth_restrict(p, k, &r1);
    r1.members == r2.members
}

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

    #[test]
    fn skeleton_size() {
        assert_eq!(rounded_skeleton_size(2, 3), 8);
        assert_eq!(rounded_skeleton_size(3, 2), 9);
    }

    #[test]
    fn idempotent() {
        let mut s = DepthState::new(16);
        s.members[0] = true;
        s.members[3] = true;
        s.members[10] = true;
        assert!(check_idempotent(2, 3, &s)); // skeleton = {0..7}
    }
}