vyre-conform 0.1.0

//! Law coverage matrix — defense against T03/T04/T05.
//!
//! Enumerates every (op, law) pair and reports whether the pair is:
//! - Declared + enforced
//! - Not applicable (annotated)
//! - Violated (witnessed)
//! - Missing (no coverage — build failure)

use serde::{Deserialize, Serialize};
use std::collections::HashSet;

use crate::spec::law::{AlgebraicLaw, LAW_CATALOG};
use crate::spec::op_registry;

/// Status of one cell in the coverage matrix.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum CellStatus {
    /// Law is declared and the checker has an enforcement function.
    DeclaredAndEnforced,
    /// Law is declared but the checker cannot enforce it for this arity.
    DeclaredButUnenforced,
    /// Law is not declared and a not-applicable annotation exists.
    NotApplicable,
    /// Law is not declared and a violation witness exists.
    Violated,
    /// No entry for this cell.
    Missing,
}

/// One cell in the coverage matrix.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CoverageCell {
    /// Operation identifier.
    pub op_id: String,
    /// Law name from [`LAW_CATALOG`].
    pub law: String,
    /// Coverage status for this pair.
    pub status: CellStatus,
}

/// The full coverage matrix.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct CoverageMatrix {
    /// All cells in the matrix.
    pub cells: Vec<CoverageCell>,
}

impl CoverageMatrix {
    /// Return every cell whose status is [`CellStatus::Missing`].
    #[must_use]
    #[inline]
    pub fn missing(&self) -> Vec<&CoverageCell> {
        self.cells
            .iter()
            .filter(|c| c.status == CellStatus::Missing)
            .collect()
    }

    /// Return every cell whose status is [`CellStatus::DeclaredButUnenforced`].
    #[must_use]
    #[inline]
    pub fn unenforced(&self) -> Vec<&CoverageCell> {
        self.cells
            .iter()
            .filter(|c| c.status == CellStatus::DeclaredButUnenforced)
            .collect()
    }
}

/// Build the coverage matrix for all registered ops.
///
/// This is the entry point used by the test suite and the
/// `vyre-conform coverage-matrix` CLI.
#[inline]
pub fn compute_coverage_matrix() -> CoverageMatrix {
    let specs = op_registry::all_specs();
    let mut cells = Vec::with_capacity(specs.len().saturating_mul(LAW_CATALOG.len()));

    for spec in specs {
        let arity = spec.signature.inputs.len();
        let has_custom = spec
            .laws
            .iter()
            .any(|l| matches!(l, AlgebraicLaw::Custom { .. }));
        let declared_names: HashSet<String> =
            spec.laws.iter().map(|l| l.name().to_string()).collect();

        for &law_name in LAW_CATALOG {
            let is_declared =
                (law_name == "custom" && has_custom) || declared_names.contains(law_name);

            let status = if is_declared {
                if declared_law_is_supported(&spec.laws, law_name, arity) {
                    CellStatus::DeclaredAndEnforced
                } else {
                    CellStatus::DeclaredButUnenforced
                }
            } else if not_applicable_annotation_exists(spec.id, law_name) {
                CellStatus::NotApplicable
            } else if violation_witness_exists(spec.id, law_name) {
                CellStatus::Violated
            } else {
                CellStatus::Missing
            };

            cells.push(CoverageCell {
                op_id: spec.id.to_string(),
                law: law_name.to_string(),
                status,
            });
        }
    }

    CoverageMatrix { cells }
}

/// Create a `not_applicable` annotation for every missing cell.
///
/// Returns the number of files created.
///
/// # Errors
///
/// Propagates I/O errors from directory creation or file write.
#[inline]
pub fn batch_create_missing_annotations(matrix: &CoverageMatrix) -> std::io::Result<usize> {
    let mut created = 0;
    for cell in &matrix.cells {
        if cell.status == CellStatus::Missing {
            let path = annotation_path(&cell.op_id, &cell.law);
            if let Some(parent) = path.parent() {
                std::fs::create_dir_all(parent)?;
                let content = format!(
                    "# {} / {}\nstatus = \"not_applicable\"\nreason = \"auto-generated first-pass annotation\"\n",
                    cell.op_id, cell.law
                );
                std::fs::write(&path, content)?;
                created += 1;
            }
        }
    }
    Ok(created)
}

fn annotation_path(op_id: &str, law_name: &str) -> std::path::PathBuf {
    std::path::PathBuf::from(format!(
        "conform/annotations/{op_id}/{law_name}.not_applicable"
    ))
}

fn not_applicable_annotation_exists(op_id: &str, law_name: &str) -> bool {
    annotation_path(op_id, law_name).is_file()
}

fn violation_witness_exists(op_id: &str, law_name: &str) -> bool {
    crate::verify::regression::load_failures_versioned(op_id, 1)
        .iter()
        .any(|f| f.input_label == format!("law_violation:{law_name}"))
}

fn declared_law_is_supported(laws: &[AlgebraicLaw], law_name: &str, arity: usize) -> bool {
    laws.iter()
        .filter(|law| {
            law.name() == law_name
                || (law_name == "custom" && matches!(law, AlgebraicLaw::Custom { .. }))
        })
        .any(|law| law_variant_is_supported(law, arity))
}

fn law_variant_is_supported(law: &AlgebraicLaw, arity: usize) -> bool {
    match law {
        AlgebraicLaw::Involution
        | AlgebraicLaw::Monotone
        | AlgebraicLaw::Monotonic { .. }
        | AlgebraicLaw::DeMorgan { .. } => arity == 1,
        AlgebraicLaw::Complement { .. } | AlgebraicLaw::Bounded { .. } => arity == 1 || arity == 2,
        AlgebraicLaw::Commutative
        | AlgebraicLaw::Associative
        | AlgebraicLaw::Identity { .. }
        | AlgebraicLaw::LeftIdentity { .. }
        | AlgebraicLaw::RightIdentity { .. }
        | AlgebraicLaw::SelfInverse { .. }
        | AlgebraicLaw::Idempotent
        | AlgebraicLaw::Absorbing { .. }
        | AlgebraicLaw::LeftAbsorbing { .. }
        | AlgebraicLaw::RightAbsorbing { .. }
        | AlgebraicLaw::ZeroProduct { .. }
        | AlgebraicLaw::DistributiveOver { .. }
        | AlgebraicLaw::LatticeAbsorption { .. }
        | AlgebraicLaw::InverseOf { .. }
        | AlgebraicLaw::Trichotomy { .. } => arity == 2,
        AlgebraicLaw::Custom {
            arity: law_arity, ..
        } => *law_arity == arity,
        _ => false,
    }
}

#[cfg(test)]
mod tests {

    use super::violation_witness_exists;

    #[test]
    fn violation_witness_lookup_reads_versioned_regression_store() {
        let op_id = "coverage_witness_store_test";
        let regression_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
            .join("regressions")
            .join(op_id);
        let _ = std::fs::remove_dir_all(&regression_dir);

        let failure = crate::spec::types::ParityFailure {
            op_id: op_id.to_string(),
            generator: "coverage-test".to_string(),
            input_label: "law_violation:commutative".to_string(),
            input: vec![1, 0, 0, 0, 2, 0, 0, 0],
            gpu_output: Vec::new(),
            cpu_output: vec![3, 0, 0, 0],
            message: "commutative violation fixture".to_string(),
            spec_version: 1,
            workgroup_size: 1,
        };
        crate::verify::regression::save(&failure)
            .expect("Fix: regression store must accept coverage witness fixture");

        assert!(
            violation_witness_exists(op_id, "commutative"),
            "Fix: coverage must read law violation witnesses from conform/regressions/<op>/v1/*.json"
        );

        std::fs::remove_dir_all(&regression_dir)
            .expect("Fix: coverage witness fixture cleanup must remove regression dir");
    }
}