vyre-conform 0.1.0

//! Law verification engine.
//!
//! Given an operation's CPU reference function and declared laws, verify
//! that the function satisfies every law. This is the "type checker" of
//! vyre-conform: if it accepts, the operation is correct (within the
//! verification domain).

mod rebuild;
/// Helper functions for law checking (boundary grids, RNG, violations).
#[cfg(loom)]
pub mod support;
#[cfg(not(loom))]
pub(crate) mod support;

use crate::spec::law::{AlgebraicLaw, LawViolation};
#[cfg(not(loom))]
use rayon::prelude::*;
use std::sync::{Mutex, OnceLock};
use support::{check_unary_law_exhaustive_u8, check_unary_law_witnessed_u32};

/// Result of verifying one law against one operation.
#[derive(Debug, Clone)]
pub struct LawResult {
    /// Operation ID.
    pub op_id: String,
    /// Law that was verified.
    pub law_name: String,
    /// Verification level used.
    pub level: VerificationLevel,
    /// Number of input cases tested.
    pub cases_tested: u64,
    /// Violation, if any. None = law holds.
    pub violation: Option<LawViolation>,
}

impl LawResult {
    /// Whether the law was verified successfully.
    ///
    /// A law passes iff the checker actually ran at least one case
    /// AND no violation was found. Returning `passed` on zero cases
    /// would silently accept:
    ///
    /// - A mismatched-arity law (e.g., Involution declared on a
    ///   binary op — the binary dispatch falls through to `_ =>
    ///   (0, None)`).
    /// - An unverified cross-op law (DistributiveOver, DeMorgan,
    ///   Complement — same fall-through path as of the current
    ///   checker).
    /// - A witnessed check with `witness_count = 0` — the loop runs
    ///   zero times and returns `(0, None)`.
    ///
    /// All three are critical findings from Kimi audit #3 and this
    /// accessor is the single place they are rejected. A caller that
    /// wants the old "violation only" semantic can read `violation`
    /// directly; the `passed` accessor is the safe default.
    #[must_use]
    #[inline]
    pub fn passed(&self) -> bool {
        self.violation.is_none() && self.cases_tested > 0
    }

    /// Whether the checker declined to verify this law because it
    /// could not run a single case. Callers should surface this as a
    /// finding, not a pass.
    #[must_use]
    #[inline]
    pub fn is_inapplicable(&self) -> bool {
        self.cases_tested == 0 && self.violation.is_none()
    }
}

/// Verification level.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum VerificationLevel {
    /// Exhaustive on u8 domain. Proof within domain.
    ExhaustiveU8,
    /// Random witnesses on u32 domain.
    WitnessedU32 {
        /// Number of witnesses.
        count: u64,
    },
    /// Random witnesses on u32 domain through a GPU backend.
    GpuWitnessedU32 {
        /// Number of witnesses.
        count: u64,
    },
    /// Both exhaustive u8 and witnessed u32.
    Combined {
        /// Number of u32 witnesses.
        witness_count: u64,
    },
}

/// Verify all declared laws for an operation using exhaustive u8 verification.
///
/// This is the proof path. Every input in the u8 domain is tested. If all
/// pass, the law is proven within u8.
///
/// `cpu_fn` takes raw bytes and returns raw bytes (the standard conform
/// reference function signature). For binary ops, input is 8 bytes (two u32
/// LE). For unary ops, input is 4 bytes.
#[inline]
pub fn verify_laws(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    laws: &[AlgebraicLaw],
    is_binary: bool,
) -> Vec<LawResult> {
    laws.iter()
        .map(|law| verify_one_law_exhaustive(op_id, cpu_fn, law, is_binary))
        .collect()
}

/// Verify all declared laws using witnessed u32 verification.
#[cfg(loom)]
#[inline]
pub fn verify_laws_witnessed(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    laws: &[AlgebraicLaw],
    is_binary: bool,
    witness_count: u64,
) -> Vec<LawResult> {
    use loom::sync::{mpsc, Arc, Mutex};
    use loom::thread;

    if laws.is_empty() {
        return Vec::new();
    }

    let (tx, rx) = mpsc::channel();
    let rx = Arc::new(Mutex::new(rx));

    let worker_count = 2;
    let mut handles = Vec::with_capacity(worker_count);
    for _ in 0..worker_count {
        let rx = Arc::clone(&rx);
        let handle = thread::spawn(move || {
            let mut results = Vec::new();
            loop {
                let msg = {
                    let lock = rx.lock().unwrap();
                    lock.recv()
                };
                match msg {
                    Ok((idx, law)) => {
                        let result =
                            verify_one_law_witnessed(op_id, cpu_fn, &law, is_binary, witness_count);
                        results.push((idx, result));
                    }
                    Err(_) => break,
                }
            }
            results
        });
        handles.push(handle);
    }

    for (idx, law) in laws.iter().enumerate() {
        tx.send((idx, law.clone())).unwrap();
    }
    drop(tx);

    let mut all_results = vec![None; laws.len()];
    for handle in handles {
        for (idx, result) in handle.join().unwrap() {
            all_results[idx] = Some(result);
        }
    }
    all_results.into_iter().flatten().collect()
}

/// Verify all declared laws using witnessed u32 verification.
#[cfg(not(loom))]
#[inline]
pub fn verify_laws_witnessed(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    laws: &[AlgebraicLaw],
    is_binary: bool,
    witness_count: u64,
) -> Vec<LawResult> {
    laws.par_iter()
        .map(|law| verify_one_law_witnessed(op_id, cpu_fn, law, is_binary, witness_count))
        .collect()
}

fn verify_one_law_exhaustive(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    is_binary: bool,
) -> LawResult {
    let (cases, violation) = if is_binary {
        check_binary_law_exhaustive_u8(op_id, cpu_fn, law)
    } else {
        check_unary_law_exhaustive_u8(op_id, cpu_fn, law)
    };
    let violation = violation.map(|v| {
        if is_binary {
            match minimize_binary_violation(op_id, cpu_fn, law, v.a, v.b, v.c) {
                Ok(minimized) => minimized.unwrap_or(v),
                Err(rebuild_err) => rebuild_err,
            }
        } else {
            match minimize_unary_violation(op_id, cpu_fn, law, v.a) {
                Ok(minimized) => minimized.unwrap_or(v),
                Err(rebuild_err) => rebuild_err,
            }
        }
    });
    LawResult {
        op_id: op_id.to_string(),
        law_name: law.name().to_string(),
        level: VerificationLevel::ExhaustiveU8,
        cases_tested: cases,
        violation,
    }
}

fn verify_one_law_witnessed(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    is_binary: bool,
    witness_count: u64,
) -> LawResult {
    let (cases, violation) = if is_binary {
        check_binary_law_witnessed_u32(op_id, cpu_fn, law, witness_count)
    } else {
        check_unary_law_witnessed_u32(op_id, cpu_fn, law, witness_count)
    };
    let violation = violation.map(|v| {
        let mut minimized = match if is_binary {
            minimize_binary_violation(op_id, cpu_fn, law, v.a, v.b, v.c)
        } else {
            minimize_unary_violation(op_id, cpu_fn, law, v.a)
        } {
            Ok(minimized) => minimized.unwrap_or(v),
            Err(rebuild_err) => rebuild_err,
        };
        // F5: Persist failing witnesses to regression/ so future runs
        // catch them even if the random seed changes.
        if let Err(err) = persist_violation(op_id, &minimized) {
            minimized.message = format!(
                "{} Regression persistence failed: {err}. Fix: ensure conform/regressions is writable before trusting witnessed law replay.",
                minimized.message
            );
        }
        minimized
    });
    LawResult {
        op_id: op_id.to_string(),
        law_name: law.name().to_string(),
        level: VerificationLevel::WitnessedU32 {
            count: witness_count,
        },
        cases_tested: cases,
        violation,
    }
}

fn persist_violation(op_id: &str, v: &LawViolation) -> std::io::Result<()> {
    static PERSIST_LOCK: OnceLock<Mutex<()>> = OnceLock::new();
    let _guard = PERSIST_LOCK
        .get_or_init(|| Mutex::new(()))
        .lock()
        .map_err(|_| std::io::Error::other("Fix: regression persistence lock was poisoned."))?;
    let mut input = Vec::with_capacity(12);
    input.extend_from_slice(&v.a.to_le_bytes());
    input.extend_from_slice(&v.b.to_le_bytes());
    input.extend_from_slice(&v.c.to_le_bytes());

    let failure = crate::spec::types::ParityFailure {
        op_id: op_id.to_string(),
        generator: "algebra_checker".to_string(),
        input_label: format!("law_violation:{}", v.law),
        input,
        gpu_output: vec![],
        cpu_output: v.lhs.to_le_bytes().to_vec(),
        message: v.message.clone(),
        spec_version: 1,
        workgroup_size: 1,
    };
    crate::verify::regression::save(&failure).map(|_| ())
}

// ---------------------------------------------------------------------------
// Binary law checkers — exhaustive u8
// ---------------------------------------------------------------------------

fn check_binary_law_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
) -> (u64, Option<LawViolation>) {
    match crate::proof::algebra::laws::binary::check_exhaustive_u8(op_id, f, law) {
        Ok(r) => r,
        Err(v) => (0, Some(v)),
    }
}

// ---------------------------------------------------------------------------
// Witnessed u32 checkers
// ---------------------------------------------------------------------------

fn check_binary_law_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    count: u64,
) -> (u64, Option<LawViolation>) {
    match crate::proof::algebra::laws::binary::check_witnessed_u32(op_id, f, law, count) {
        Ok(r) => r,
        Err(v) => (0, Some(v)),
    }
}

// ---------------------------------------------------------------------------
// Minimization helpers
// ---------------------------------------------------------------------------

use rebuild::{minimize_binary_violation, minimize_unary_violation};