//! Core types for nucleus grafting
//! Source: HeytingLean.NucleusGrafting.Types
//!
//! Theorem preserved: latticeSpacing_pos
//! Theorem preserved: activationFixedSet_mono
//! Theorem preserved: componentUpperBound_eq_total
//! Theorem preserved: componentUpperBound_nonneg

/// Quantization parameters for a single layer.
#[derive(Debug, Clone)]
pub struct LayerQuantParams {
    pub layer_name: String,
    pub scale: f64,
    pub zero_point: i32,
    pub lattice_spacing: f64,
}

impl LayerQuantParams {
    pub fn new(layer_name: impl Into<String>, scale: f64, zero_point: i32) -> Self {
        assert!(scale > 0.0, "scale must be positive");
        Self {
            layer_name: layer_name.into(),
            scale,
            zero_point,
            lattice_spacing: scale,
        }
    }

    /// Theorem: latticeSpacing_pos
    pub fn lattice_spacing_pos(&self) -> bool {
        self.lattice_spacing > 0.0
    }
}

/// Gap decomposition: total = quantization + gate + reconstruction
#[derive(Debug, Clone)]
pub struct GapDecomposition {
    pub quantization: f64,
    pub gate: f64,
    pub reconstruction: f64,
    pub total: f64,
}

impl GapDecomposition {
    pub fn new(quantization: f64, gate: f64, reconstruction: f64) -> Self {
        assert!(quantization >= 0.0 && gate >= 0.0 && reconstruction >= 0.0);
        let total = quantization + gate + reconstruction;
        Self { quantization, gate, reconstruction, total }
    }

    /// Theorem: componentUpperBound_eq_total
    pub fn component_upper_bound(&self) -> f64 {
        self.quantization + self.gate + self.reconstruction
    }

    pub fn is_valid(&self) -> bool {
        self.quantization >= 0.0
            && self.gate >= 0.0
            && self.reconstruction >= 0.0
            && self.total >= 0.0
            && (self.total - self.component_upper_bound()).abs() < 1e-12
    }
}

/// Activation fixed set: { v | forall i, z <= v[i] }
pub fn activation_fixed_set_contains(z: i32, v: &[i32]) -> bool {
    v.iter().all(|&vi| z <= vi)
}

/// Theorem: activationFixedSet_mono
/// z1 <= z2 implies fixedSet(z2) ⊆ fixedSet(z1)
pub fn activation_fixed_set_mono(z1: i32, z2: i32, v: &[i32]) -> bool {
    if z1 <= z2 {
        !activation_fixed_set_contains(z2, v) || activation_fixed_set_contains(z1, v)
    } else {
        true
    }
}

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

    #[test]
    fn test_gap_valid() {
        let g = GapDecomposition::new(0.5, 2.1, 0.0);
        assert!(g.is_valid());
        assert!((g.total - 2.6).abs() < 1e-12);
        assert!((g.component_upper_bound() - g.total).abs() < 1e-12);
    }

    #[test]
    fn test_fixed_set_mono() {
        let v = vec![5, 10, 3];
        assert!(activation_fixed_set_contains(3, &v));
        assert!(!activation_fixed_set_contains(6, &v));
        assert!(activation_fixed_set_mono(3, 6, &v));
    }

    #[test]
    fn test_lattice_spacing() {
        let p = LayerQuantParams::new("layer1", 0.015, -128);
        assert!(p.lattice_spacing_pos());
    }
}