vyre-conform 0.1.0

//! Dispatch for binary algebra law checkers.
//!
//! Investigation report for the April 2026 dead-code finding:
//! - `check_exhaustive_u8` and `check_witnessed_u32` were crate-visible but
//!   had no callers under `conform/src`.
//! - Every standalone checker below was only reachable through those orphaned
//!   helpers, so rustc correctly warned that the module was bypassed.
//! - The active dispatch had been duplicated inline in `algebra/checker.rs`.
//!   That path did execute the same exhaustive checks and a stronger witnessed
//!   path with boundary-grid sweeps.
//! - The fix wires `algebra/checker.rs` back to this module and keeps the
//!   stronger witnessed boundary coverage here, making this file the single
//!   binary-law dispatch engine again.

use crate::proof::algebra::checker::support::{
    boundary_grid_u32, call_binary, engine_failure_violation, simple_rng, violation,
};
use crate::spec::law::{AlgebraicLaw, LawViolation};

/// Verify one binary law over exhaustive u8 inputs.
#[inline]
pub(crate) fn check_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    match law {
        AlgebraicLaw::Commutative => check_commutative_exhaustive(op_id, f),
        AlgebraicLaw::Associative => check_associative_exhaustive(op_id, f),
        AlgebraicLaw::Identity { element } => check_identity_exhaustive(op_id, f, *element),
        AlgebraicLaw::LeftIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
            )
        }
        AlgebraicLaw::RightIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
            )
        }
        AlgebraicLaw::SelfInverse { result } => check_self_inverse_exhaustive(op_id, f, *result),
        AlgebraicLaw::Idempotent => check_idempotent_exhaustive(op_id, f),
        AlgebraicLaw::Absorbing { element } => check_absorbing_exhaustive(op_id, f, *element),
        AlgebraicLaw::LeftAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
            )
        }
        AlgebraicLaw::RightAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
            )
        }
        AlgebraicLaw::Bounded { lo, hi } => check_bounded_exhaustive(op_id, f, *lo, *hi),
        AlgebraicLaw::ZeroProduct { holds } => check_zero_product_exhaustive(op_id, f, *holds),
        AlgebraicLaw::DistributiveOver { over_op } => {
            crate::proof::algebra::laws::distributive::check_exhaustive_u8(op_id, f, over_op, 0)
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => crate::proof::algebra::laws::complement::check_binary_exhaustive_u8(
            op_id,
            f,
            complement_op,
            *universe,
            0,
        ),
        AlgebraicLaw::LatticeAbsorption { dual_op } => {
            Ok(crate::proof::algebra::laws::lattice::check_exhaustive_u8(op_id, f, dual_op, 0))
        }
        AlgebraicLaw::InverseOf { op } => {
            crate::proof::algebra::laws::inverse::check_exhaustive_u8(op_id, f, op, 0)
        }
        AlgebraicLaw::Trichotomy {
            less_op,
            equal_op,
            greater_op,
        } => crate::proof::algebra::laws::trichotomy::check_exhaustive_u8(
            op_id, f, less_op, equal_op, greater_op, 0,
        ),
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => Ok(crate::proof::algebra::laws::custom::check_exhaustive_u8(
            op_id, f, name, *arity, *check,
        )),
        other => Ok((0, Some(LawViolation {
            law: format!("{:?}", other),
            op_id: op_id.to_string(),
            message: format!("unimplemented binary law checker for {:?}. Fix: add a real checker or remove the declared law.", other),
            a: 0, b: 0, c: 0, lhs: 0, rhs: 0,
        }))),
    }
}

/// Verify one binary law over deterministic u32 witnesses.
#[inline]
pub(crate) fn check_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut rng = simple_rng(op_id, law.name());
    let grid = boundary_grid_u32();
    match law {
        AlgebraicLaw::Commutative => {
            for &a in &grid {
                for &b in &grid {
                    let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                    let ba = call_binary(f, b, a).map_err(|e| engine_failure_violation(op_id, e))?;
                    if ab != ba {
                        return Ok((1, Some(violation(op_id, "commutative", a, b, 0, ab, ba))));
                    }
                }
            }
            for i in 0..count {
                let a = rng.next_u32();
                let b = rng.next_u32();
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                let ba = call_binary(f, b, a).map_err(|e| engine_failure_violation(op_id, e))?;
                if ab != ba {
                    return Ok((i + 1, Some(violation(op_id, "commutative", a, b, 0, ab, ba))));
                }
            }
            Ok((count, None))
        }
        AlgebraicLaw::Associative => {
            for &a in &grid {
                for &b in &grid {
                    for &c in &grid {
                        let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                        let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
                        let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
                        let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
                        if ab_c != a_bc {
                            return Ok((
                                1,
                                Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
                            ));
                        }
                    }
                }
            }
            for i in 0..count {
                let a = rng.next_u32();
                let b = rng.next_u32();
                let c = rng.next_u32();
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
                if ab_c != a_bc {
                    return Ok((
                        i + 1,
                        Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
                    ));
                }
            }
            Ok((count, None))
        }
        AlgebraicLaw::Identity { element } => {
            check_identity_witnessed(op_id, f, *element, count, &grid)
        }
        AlgebraicLaw::LeftIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_witnessed_u32(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
                count,
            )
        }
        AlgebraicLaw::RightIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_witnessed_u32(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
                count,
            )
        }
        AlgebraicLaw::SelfInverse { result } => {
            check_self_inverse_witnessed(op_id, f, *result, count)
        }
        AlgebraicLaw::Idempotent => check_idempotent_witnessed(op_id, f, count),
        AlgebraicLaw::Absorbing { element } => check_absorbing_witnessed(op_id, f, *element, count),
        AlgebraicLaw::LeftAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_witnessed_u32(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
                count,
            )
        }
        AlgebraicLaw::RightAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_witnessed_u32(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
                count,
            )
        }
        AlgebraicLaw::Bounded { lo, hi } => check_bounded_witnessed(op_id, f, *lo, *hi, count),
        AlgebraicLaw::ZeroProduct { holds } => check_zero_product_witnessed(op_id, f, *holds, count),
        AlgebraicLaw::DistributiveOver { over_op } => {
            crate::proof::algebra::laws::distributive::check_witnessed_u32(op_id, f, over_op, count)
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => crate::proof::algebra::laws::complement::check_binary_witnessed_u32(
            op_id,
            f,
            complement_op,
            *universe,
            count,
        ),
        AlgebraicLaw::LatticeAbsorption { dual_op } => {
            Ok(crate::proof::algebra::laws::lattice::check_witnessed_u32(op_id, f, dual_op, count))
        }
        AlgebraicLaw::InverseOf { op } => {
            crate::proof::algebra::laws::inverse::check_witnessed_u32(op_id, f, op, count)
        }
        AlgebraicLaw::Trichotomy {
            less_op,
            equal_op,
            greater_op,
        } => crate::proof::algebra::laws::trichotomy::check_witnessed_u32(
            op_id, f, less_op, equal_op, greater_op, count,
        ),
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => Ok(crate::proof::algebra::laws::custom::check_witnessed_u32(
            op_id, f, name, *arity, *check, count,
        )),
        other => Ok((0, Some(LawViolation {
            law: format!("{:?}", other),
            op_id: op_id.to_string(),
            message: format!("unimplemented binary witnessed law checker for {:?}. Fix: add a real checker or remove the declared law.", other),
            a: 0, b: 0, c: 0, lhs: 0, rhs: 0,
        }))),
    }
}

fn check_commutative_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        for b in 0u32..256 {
            let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
            let ba = call_binary(f, b, a).map_err(|e| engine_failure_violation(op_id, e))?;
            cases += 1;
            if ab != ba {
                return Ok((
                    cases,
                    Some(violation(op_id, "commutative", a, b, 0, ab, ba)),
                ));
            }
        }
    }
    Ok((cases, None))
}

fn check_associative_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        for b in 0u32..256 {
            for c in 0u32..256 {
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
                cases += 1;
                if ab_c != a_bc {
                    return Ok((
                        cases,
                        Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
                    ));
                }
            }
        }
    }
    Ok((cases, None))
}

fn check_identity_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    e: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        cases += 2;
        let ae = call_binary(f, a, e).map_err(|e| engine_failure_violation(op_id, e))?;
        if ae != a {
            return Ok((
                cases,
                Some(violation(op_id, "identity(right)", a, e, 0, ae, a)),
            ));
        }
        let ea = call_binary(f, e, a).map_err(|e| engine_failure_violation(op_id, e))?;
        if ea != a {
            return Ok((
                cases,
                Some(violation(op_id, "identity(left)", e, a, 0, ea, a)),
            ));
        }
    }
    Ok((cases, None))
}

fn check_self_inverse_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    r: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        let aa = call_binary(f, a, a).map_err(|e| engine_failure_violation(op_id, e))?;
        cases += 1;
        if aa != r {
            return Ok((
                cases,
                Some(violation(op_id, "self-inverse", a, a, 0, aa, r)),
            ));
        }
    }
    Ok((cases, None))
}

fn check_idempotent_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        let aa = call_binary(f, a, a).map_err(|e| engine_failure_violation(op_id, e))?;
        cases += 1;
        if aa != a {
            return Ok((cases, Some(violation(op_id, "idempotent", a, a, 0, aa, a))));
        }
    }
    Ok((cases, None))
}

fn check_absorbing_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    z: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        cases += 2;
        let az = call_binary(f, a, z).map_err(|e| engine_failure_violation(op_id, e))?;
        if az != z {
            return Ok((
                cases,
                Some(violation(op_id, "absorbing(right)", a, z, 0, az, z)),
            ));
        }
        let za = call_binary(f, z, a).map_err(|e| engine_failure_violation(op_id, e))?;
        if za != z {
            return Ok((
                cases,
                Some(violation(op_id, "absorbing(left)", z, a, 0, za, z)),
            ));
        }
    }
    Ok((cases, None))
}

fn check_bounded_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    lo: u32,
    hi: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        for b in 0u32..256 {
            let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
            cases += 1;
            if ab < lo || ab > hi {
                return Ok((cases, Some(violation(op_id, "bounded", a, b, 0, ab, lo))));
            }
        }
    }
    Ok((cases, None))
}

fn check_zero_product_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    holds: bool,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    if !holds {
        let mut cases = 0u64;
        for a in 0u32..256 {
            for b in 0u32..256 {
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                cases += 1;
                if ab == 0 && a != 0 && b != 0 {
                    return Ok((cases, None));
                }
            }
        }
        let zp = call_binary(f, 2, 0x8000_0000).map_err(|e| engine_failure_violation(op_id, e))?;
        return Ok((
            cases,
            Some(violation(
                op_id,
                "zero-product(false)",
                2,
                0x8000_0000,
                0,
                zp,
                0,
            )),
        ));
    }

    let mut cases = 0u64;
    for a in 0u32..256 {
        for b in 0u32..256 {
            let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
            cases += 1;
            if ab == 0 && a != 0 && b != 0 {
                return Ok((
                    cases,
                    Some(violation(op_id, "zero-product(true)", a, b, 0, ab, 1)),
                ));
            }
        }
    }
    Ok((cases, None))
}

mod witnessed;
use witnessed::*;