vyre-conform 0.1.0

//! Checker for custom law predicates.

use crate::proof::algebra::checker::support::{simple_rng, violation, PATHOLOGICAL_U32_WITNESSES};
use crate::spec::law::{LawCheckFn, LawViolation};

/// Verify a custom law over exhaustive u8 inputs plus structural witnesses.
#[inline]
pub(crate) fn check_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    name: &str,
    arity: usize,
    check: LawCheckFn,
) -> (u64, Option<LawViolation>) {
    let mut cases = 0;
    if let Some(v) = exhaustive_u8_cases(op_id, f, name, arity, check, &mut cases) {
        return (cases, Some(v));
    }
    if let Some(v) = boundary_cases(op_id, f, name, arity, check, &mut cases) {
        return (cases, Some(v));
    }
    (cases, None)
}

/// Verify a custom law over deterministic u32 witnesses.
#[inline]
pub(crate) fn check_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    name: &str,
    arity: usize,
    check: LawCheckFn,
    count: u64,
) -> (u64, Option<LawViolation>) {
    let mut cases = 0;
    if let Some(v) = boundary_cases(op_id, f, name, arity, check, &mut cases) {
        return (cases, Some(v));
    }
    let mut rng = simple_rng(op_id, name);
    for _ in 0..count {
        let mut args = vec![0; arity];
        for arg in &mut args {
            *arg = rng.next_u32();
        }
        cases += 1;
        if !check(f, &args) {
            return (cases, Some(custom_violation(op_id, name, &args)));
        }
    }
    (cases, None)
}

fn exhaustive_u8_cases(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    name: &str,
    arity: usize,
    check: LawCheckFn,
    cases: &mut u64,
) -> Option<LawViolation> {
    match arity {
        1 => {
            for a in 0u32..256 {
                *cases += 1;
                let args = [a];
                if !check(f, &args) {
                    return Some(custom_violation(op_id, name, &args));
                }
            }
            None
        }
        2 => {
            for a in 0u32..256 {
                for b in 0u32..256 {
                    *cases += 1;
                    let args = [a, b];
                    if !check(f, &args) {
                        return Some(custom_violation(op_id, name, &args));
                    }
                }
            }
            None
        }
        3 => {
            for a in 0u32..256 {
                for b in 0u32..256 {
                    for c in 0u32..256 {
                        *cases += 1;
                        let args = [a, b, c];
                        if !check(f, &args) {
                            return Some(custom_violation(op_id, name, &args));
                        }
                    }
                }
            }
            None
        }
        _ => Some(LawViolation {
            law: format!("Custom({name})"),
            op_id: op_id.to_string(),
            message: format!(
                "unsupported Custom law arity `{arity}` for `{name}`. Fix: use arity 1, 2, or 3."
            ),
            a: 0,
            b: 0,
            c: 0,
            lhs: 0,
            rhs: 0,
        }),
    }
}

fn boundary_cases(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    name: &str,
    arity: usize,
    check: LawCheckFn,
    cases: &mut u64,
) -> Option<LawViolation> {
    match arity {
        1 => {
            for &a in PATHOLOGICAL_U32_WITNESSES {
                *cases += 1;
                let args = [a];
                if !check(f, &args) {
                    return Some(custom_violation(op_id, name, &args));
                }
            }
            None
        }
        2 => {
            for &a in PATHOLOGICAL_U32_WITNESSES {
                for &b in PATHOLOGICAL_U32_WITNESSES {
                    *cases += 1;
                    let args = [a, b];
                    if !check(f, &args) {
                        return Some(custom_violation(op_id, name, &args));
                    }
                }
            }
            None
        }
        3 => {
            for &a in PATHOLOGICAL_U32_WITNESSES {
                for &b in PATHOLOGICAL_U32_WITNESSES {
                    for &c in PATHOLOGICAL_U32_WITNESSES {
                        *cases += 1;
                        let args = [a, b, c];
                        if !check(f, &args) {
                            return Some(custom_violation(op_id, name, &args));
                        }
                    }
                }
            }
            None
        }
        _ => Some(LawViolation {
            law: format!("Custom({name})"),
            op_id: op_id.to_string(),
            message: format!("unsupported Custom law witnessed arity `{arity}` for `{name}`. Fix: use arity 1, 2, or 3."),
            a: 0, b: 0, c: 0, lhs: 0, rhs: 0,
        }),
    }
}

fn custom_violation(op_id: &str, name: &str, args: &[u32]) -> LawViolation {
    let a = args.first().copied().unwrap_or(0);
    let b = args.get(1).copied().unwrap_or(0);
    let c = args.get(2).copied().unwrap_or(0);
    violation(op_id, name, a, b, c, 0, 1)
}