vyre-conform 0.1.0

//! Law inference — determine which laws an operation satisfies.
//!
//! Instead of requiring contributors to manually pick laws from a menu,
//! this module tries every applicable law against a CPU reference function
//! and reports which ones hold. The contributor confirms the suggestions
//! rather than inventing them.
//!
//! This turns contribution from "decide which laws apply" (requires domain
//! expertise) into "confirm these laws that your function satisfies"
//! (mechanical).

use crate::proof::algebra::checker::verify_laws;
use crate::spec::law::{AlgebraicLaw, MonotonicDirection, ALL_ALGEBRAIC_LAWS};

/// A law that the inference engine determined holds for an operation.
#[derive(Debug, Clone)]
pub struct InferredLaw {
    /// The law that holds.
    pub law: AlgebraicLaw,
    /// Human-readable name for reports.
    pub name: &'static str,
    /// Suggested action for the contributor.
    pub recommendation: String,
}

/// Result of running law inference on an operation.
#[derive(Debug, Clone)]
pub struct InferenceReport {
    /// Operation ID.
    pub op_id: String,
    /// Laws that hold under exhaustive u8 verification.
    pub proven: Vec<InferredLaw>,
    /// Laws that were tested but didn't apply (e.g., unary laws on binary ops).
    pub skipped: Vec<&'static str>,
    /// Engine-level findings (e.g., truncated outputs) that caused witnesses to be skipped.
    pub findings: Vec<crate::spec::law::LawViolation>,
    /// Human-readable summary.
    pub summary: String,
}

/// Try every binary law against a binary operation's CPU reference.
///
/// Returns all laws that hold, with recommended parameters where applicable.
/// Identity and Absorbing are tried with common values (0, 1, u32::MAX).
#[inline]
pub fn infer_binary_laws(op_id: &str, cpu_fn: fn(&[u8]) -> Vec<u8>) -> InferenceReport {
    let mut proven = Vec::new();
    let mut skipped = Vec::new();

    for law in binary_candidate_laws() {
        try_law(op_id, cpu_fn, law, true, &mut proven);
    }

    skipped.push("involution (unary only)");
    skipped.push("monotone (unary only)");
    skipped.push("monotonic (unary only)");
    skipped.push("de-morgan (unary transform over binary companions)");

    let summary = build_summary(op_id, &proven, &skipped);

    InferenceReport {
        op_id: op_id.to_string(),
        proven,
        skipped,
        findings: Vec::new(),
        summary,
    }
}

/// Try every unary law against a unary operation's CPU reference.
#[inline]
pub fn infer_unary_laws(op_id: &str, cpu_fn: fn(&[u8]) -> Vec<u8>) -> InferenceReport {
    let mut proven = Vec::new();
    let mut skipped = Vec::new();

    for law in unary_candidate_laws() {
        try_law(op_id, cpu_fn, law, false, &mut proven);
    }

    skipped.push("commutative (binary only)");
    skipped.push("associative (binary only)");
    skipped.push("identity (binary only)");
    skipped.push("left-identity (binary only)");
    skipped.push("right-identity (binary only)");
    skipped.push("self-inverse (binary only)");
    skipped.push("idempotent (binary only)");
    skipped.push("absorbing (binary only)");
    skipped.push("left-absorbing (binary only)");
    skipped.push("right-absorbing (binary only)");
    skipped.push("zero-product (binary only)");
    skipped.push("distributive (binary only)");
    skipped.push("lattice-absorption (binary only)");
    skipped.push("inverse-of (binary only)");
    skipped.push("trichotomy (binary only)");

    let summary = build_summary(op_id, &proven, &skipped);

    InferenceReport {
        op_id: op_id.to_string(),
        proven,
        skipped,
        findings: Vec::new(),
        summary,
    }
}

#[inline]
pub(crate) fn binary_candidate_laws() -> Vec<AlgebraicLaw> {
    let mut laws = Vec::new();
    for law in ALL_ALGEBRAIC_LAWS {
        match law {
            AlgebraicLaw::Commutative
            | AlgebraicLaw::Associative
            | AlgebraicLaw::Idempotent
            | AlgebraicLaw::ZeroProduct { .. }
            | AlgebraicLaw::DistributiveOver { .. }
            | AlgebraicLaw::Complement { .. }
            | AlgebraicLaw::LatticeAbsorption { .. }
            | AlgebraicLaw::InverseOf { .. }
            | AlgebraicLaw::Trichotomy { .. }
            | AlgebraicLaw::Custom { .. } => laws.push(law.clone()),
            AlgebraicLaw::Identity { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::Identity { element });
                }
            }
            AlgebraicLaw::LeftIdentity { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::LeftIdentity { element });
                }
            }
            AlgebraicLaw::RightIdentity { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::RightIdentity { element });
                }
            }
            AlgebraicLaw::SelfInverse { .. } => {
                for result in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::SelfInverse { result });
                }
            }
            AlgebraicLaw::Absorbing { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::Absorbing { element });
                }
            }
            AlgebraicLaw::LeftAbsorbing { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::LeftAbsorbing { element });
                }
            }
            AlgebraicLaw::RightAbsorbing { .. } => {
                for element in [0u32, 1, u32::MAX] {
                    laws.push(AlgebraicLaw::RightAbsorbing { element });
                }
            }
            AlgebraicLaw::Bounded { .. } => {
                for (lo, hi) in [(0u32, 1), (0, 32), (0, 255), (0, u32::MAX)] {
                    laws.push(AlgebraicLaw::Bounded { lo, hi });
                }
            }
            AlgebraicLaw::Involution | AlgebraicLaw::Monotone | AlgebraicLaw::Monotonic { .. } => {}
            AlgebraicLaw::DeMorgan { .. } => {}
            _ => {}
        }
    }
    laws
}

#[inline]
pub(crate) fn unary_candidate_laws() -> Vec<AlgebraicLaw> {
    let mut laws = Vec::new();
    for law in ALL_ALGEBRAIC_LAWS {
        match law {
            AlgebraicLaw::Involution
            | AlgebraicLaw::Monotone
            | AlgebraicLaw::DeMorgan { .. }
            | AlgebraicLaw::Complement { .. }
            | AlgebraicLaw::Custom { .. } => laws.push(law.clone()),
            AlgebraicLaw::Monotonic { .. } => {
                laws.push(AlgebraicLaw::Monotonic {
                    direction: MonotonicDirection::NonDecreasing,
                });
                laws.push(AlgebraicLaw::Monotonic {
                    direction: MonotonicDirection::NonIncreasing,
                });
            }
            AlgebraicLaw::Bounded { .. } => {
                for (lo, hi) in [(0u32, 1), (0, 32), (0, 255), (0, u32::MAX)] {
                    laws.push(AlgebraicLaw::Bounded { lo, hi });
                }
            }
            _ => {}
        }
    }
    laws
}

fn try_law(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: AlgebraicLaw,
    is_binary: bool,
    proven: &mut Vec<InferredLaw>,
) {
    let results = verify_laws(op_id, cpu_fn, std::slice::from_ref(&law), is_binary);
    for result in results {
        if result.cases_tested == 0 {
            continue; // Law doesn't apply to this arity
        }
        if result.violation.is_none() {
            let name = law.name();
            let recommendation = recommend(&law);
            proven.push(InferredLaw {
                law: law.clone(),
                name: static_name(name),
                recommendation,
            });
            return; // Don't duplicate — first match wins for parameterized laws
        }
    }
}

#[inline]
pub(crate) fn static_name(name: &str) -> &'static str {
    // Map dynamic names back to static ones
    match name {
        "commutative" => "commutative",
        "associative" => "associative",
        "identity" => "identity",
        "self-inverse" => "self-inverse",
        "idempotent" => "idempotent",
        "absorbing" => "absorbing",
        "left-absorbing" => "left-absorbing",
        "right-absorbing" => "right-absorbing",
        "left-identity" => "left-identity",
        "right-identity" => "right-identity",
        "involution" => "involution",
        "bounded" => "bounded",
        "zero-product" => "zero-product",
        "distributive" => "distributive",
        "de-morgan" => "de-morgan",
        "monotone" => "monotone",
        "monotonic" => "monotonic",
        "complement" => "complement",
        "lattice-absorption" => "lattice-absorption",
        "inverse-of" => "inverse-of",
        "trichotomy" => "trichotomy",
        _ => "custom",
    }
}

#[inline]
pub(crate) fn recommend(law: &AlgebraicLaw) -> String {
    match law {
        AlgebraicLaw::Commutative => "Add: AlgebraicLaw::Commutative".to_string(),
        AlgebraicLaw::Associative => "Add: AlgebraicLaw::Associative".to_string(),
        AlgebraicLaw::Identity { element } => {
            format!("Add: AlgebraicLaw::Identity {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::LeftIdentity { element } => {
            format!("Add: AlgebraicLaw::LeftIdentity {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::RightIdentity { element } => {
            format!("Add: AlgebraicLaw::RightIdentity {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::SelfInverse { result } => {
            format!("Add: AlgebraicLaw::SelfInverse {{ result: {result} }}")
        }
        AlgebraicLaw::Idempotent => "Add: AlgebraicLaw::Idempotent".to_string(),
        AlgebraicLaw::Absorbing { element } => {
            format!("Add: AlgebraicLaw::Absorbing {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::LeftAbsorbing { element } => {
            format!("Add: AlgebraicLaw::LeftAbsorbing {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::RightAbsorbing { element } => {
            format!("Add: AlgebraicLaw::RightAbsorbing {{ element: 0x{element:08X} }}")
        }
        AlgebraicLaw::Involution => "Add: AlgebraicLaw::Involution".to_string(),
        AlgebraicLaw::Monotone => "Add: AlgebraicLaw::Monotone".to_string(),
        AlgebraicLaw::Monotonic { direction } => {
            format!("Add: AlgebraicLaw::Monotonic {{ direction: {direction:?} }}")
        }
        AlgebraicLaw::Bounded { lo, hi } => {
            format!("Add: AlgebraicLaw::Bounded {{ lo: {lo}, hi: {hi} }}")
        }
        AlgebraicLaw::ZeroProduct { holds } => {
            format!("Add: AlgebraicLaw::ZeroProduct {{ holds: {holds} }}")
        }
        AlgebraicLaw::DistributiveOver { over_op } => {
            format!("Add: AlgebraicLaw::DistributiveOver {{ over_op: \"{over_op}\" }}")
        }
        AlgebraicLaw::DeMorgan { inner_op, dual_op } => {
            format!("Add: AlgebraicLaw::DeMorgan {{ inner_op: \"{inner_op}\", dual_op: \"{dual_op}\" }}")
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => {
            format!("Add: AlgebraicLaw::Complement {{ complement_op: \"{complement_op}\", universe: 0x{universe:08X} }}")
        }
        AlgebraicLaw::LatticeAbsorption { dual_op } => {
            format!("Add: AlgebraicLaw::LatticeAbsorption {{ dual_op: \"{dual_op}\" }}")
        }
        AlgebraicLaw::InverseOf { op } => {
            format!("Add: AlgebraicLaw::InverseOf {{ op: \"{op}\" }}")
        }
        AlgebraicLaw::Trichotomy {
            less_op,
            equal_op,
            greater_op,
        } => {
            format!("Add: AlgebraicLaw::Trichotomy {{ less_op: \"{less_op}\", equal_op: \"{equal_op}\", greater_op: \"{greater_op}\" }}")
        }
        _ => "Review this law's parameters and add if applicable.".to_string(),
    }
}

fn build_summary(op_id: &str, proven: &[InferredLaw], _skipped: &[&'static str]) -> String {
    if proven.is_empty() {
        return format!(
            "{op_id}: no standard laws hold. This operation may need custom law declarations.\n\
             If the op has structural properties, consider adding a Custom law."
        );
    }
    let law_list: Vec<String> = proven.iter().map(|l| l.name.to_string()).collect();
    let recommendations: Vec<String> = proven
        .iter()
        .map(|l| format!("  {}", l.recommendation))
        .collect();
    format!(
        "{op_id}: inferred {} laws hold: [{}]\n\
         Recommended declarations:\n{}",
        proven.len(),
        law_list.join(", "),
        recommendations.join("\n")
    )
}

/// Compare declared laws to inferred laws and report gaps.
///
/// Returns a list of laws that hold but were not declared. If non-empty,
/// the contributor should add them to the spec.
#[inline]
pub fn find_missing_laws(
    declared: &[AlgebraicLaw],
    inferred: &InferenceReport,
) -> Vec<InferredLaw> {
    let declared_names: std::collections::HashSet<&str> =
        declared.iter().map(|l| l.name()).collect();
    inferred
        .proven
        .iter()
        .filter(|l| !declared_names.contains(l.name))
        .cloned()
        .collect()
}