vyre-conform 0.1.0

//! Internal support helpers for algebra law checking.

mod boundary;
mod rng;

pub(crate) use boundary::boundary_grid_u32;
pub(crate) use rng::simple_rng;

use crate::spec::law::{AlgebraicLaw, LawViolation, MonotonicDirection};

pub(crate) const ZERO_PRODUCT_COUNTEREXAMPLES: [(u32, u32); 4] = [
    (2, 0x8000_0000),
    (0x8000_0000, 2),
    (0x0001_0000, 0x0001_0000),
    (0xFFFF_0000, 0x0001_0000),
];

/// Pathological u32 witnesses that the checker ALWAYS runs in addition
/// to the u8 exhaustive sweep.
///
/// These values close the blind spot where a sabotage only manifests at
/// u32 values outside the u8 domain — for example `popcount + 1`, which
/// is within Bounded(0, 32) for every u8 input (max popcount = 8,
/// sabotaged = 9) but violates the bound at u32::MAX (popcount = 32,
/// sabotaged = 33). Uniform random u32 sampling has negligible
/// probability of hitting the structural boundary; this fixed set
/// guarantees every bug at a structural value is seen.
///
/// The set covers:
/// - Extremes: 0, 1, u32::MAX, u32::MAX - 1, u32::MAX >> 1
/// - Powers of two: 2^k for k in {8, 15, 16, 23, 24, 31}
/// - Powers of two minus one (all-low-bits masks): 2^k - 1
/// - Sign-bit boundary: 0x7FFF_FFFF, 0x8000_0000
/// - Alternating bit patterns: 0xAAAAAAAA, 0x55555555
/// - 32-set-bits (to catch popcount blind spots): u32::MAX is already
///   in the list and carries popcount = 32
/// - Words where every byte is the same sentinel: 0xDEADBEEF, 0xCAFEBABE
///
/// Every new defendant that trips a new structural class should prompt
/// a new entry here rather than a weakening of the checker.
pub(crate) const PATHOLOGICAL_U32_WITNESSES: &[u32] = &[
    0,
    1,
    2,
    0xFF,
    0x100,
    0x7FFF,
    0x8000,
    0xFFFF,
    0x0001_0000,
    0x00FF_FFFF,
    0x0100_0000,
    0x3FFF_FFFF,
    0x4000_0000,
    0x5555_5555,
    0x7FFF_FFFF,
    0x8000_0000,
    0xAAAA_AAAA,
    0xBFFF_FFFF,
    0xC000_0000,
    0xDEAD_BEEF,
    0xCAFE_BABE,
    0xFFFF_FFFE,
    u32::MAX,
];

pub(crate) type SupportError = String;

#[inline]
pub(crate) fn call_binary(f: fn(&[u8]) -> Vec<u8>, a: u32, b: u32) -> Result<u32, SupportError> {
    let mut input = [0u8; 8];
    input[..4].copy_from_slice(&a.to_le_bytes());
    input[4..].copy_from_slice(&b.to_le_bytes());
    let out = f(&input);
    if out.len() < 4 {
        return Err("binary op output too short (expected 4 bytes)".to_string());
    }
    Ok(u32::from_le_bytes([out[0], out[1], out[2], out[3]]))
}

#[inline]
pub(crate) fn call_unary(f: fn(&[u8]) -> Vec<u8>, a: u32) -> Result<u32, SupportError> {
    let out = f(&a.to_le_bytes());
    if out.len() < 4 {
        return Err("unary op output too short (expected 4 bytes)".to_string());
    }
    Ok(u32::from_le_bytes([out[0], out[1], out[2], out[3]]))
}

#[inline]
pub(crate) fn check_unary_law_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
) -> (u64, Option<LawViolation>) {
    match law {
        AlgebraicLaw::Involution => {
            let mut cases = 0u64;
            for a in 0u32..256 {
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                let ffa = match call_unary(f, fa) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                cases += 1;
                if ffa != a {
                    return (cases, Some(violation(op_id, "involution", a, 0, 0, ffa, a)));
                }
            }
            // Pathological u32 witnesses guard against involution
            // sabotages that fix themselves on u8 inputs but drift on
            // u32-scale bit patterns (e.g. a NOT that also clears bit 31).
            for &a in PATHOLOGICAL_U32_WITNESSES {
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                let ffa = match call_unary(f, fa) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                cases += 1;
                if ffa != a {
                    return (cases, Some(violation(op_id, "involution", a, 0, 0, ffa, a)));
                }
            }
            (cases, None)
        }
        AlgebraicLaw::Bounded { lo, hi } => {
            let mut cases = 0u64;
            // Sweep u8 exhaustively first — the historical guarantee.
            for a in 0u32..256 {
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                cases += 1;
                if fa < *lo || fa > *hi {
                    return (cases, Some(violation(op_id, "bounded", a, 0, 0, fa, *lo)));
                }
            }
            // Then run the pathological u32 witnesses so sabotages that
            // only manifest at structural u32 boundaries (u32::MAX,
            // alternating bit patterns, powers of two) are caught even
            // on the "exhaustive u8" verification level. Without this,
            // e.g. popcount+1 sails past because the u8 domain never
            // reaches popcount 32.
            for &a in PATHOLOGICAL_U32_WITNESSES {
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                };
                cases += 1;
                if fa < *lo || fa > *hi {
                    return (cases, Some(violation(op_id, "bounded", a, 0, 0, fa, *lo)));
                }
            }
            (cases, None)
        }
        AlgebraicLaw::SelfInverse { .. } => {
            // SelfInverse is a binary law used in the unary context — report as finding.
            (
                0,
                Some(violation(
                    op_id,
                    "SelfInverse (misplaced on unary op)",
                    0,
                    0,
                    0,
                    0,
                    0,
                )),
            )
        }
        AlgebraicLaw::Monotonic { direction } => {
            let mut cases = 0u64;
            for a in 0u32..256 {
                for b in a..256 {
                    let fa = match call_unary(f, a) {
                        Ok(v) => v,
                        Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                    };
                    let fb = match call_unary(f, b) {
                        Ok(v) => v,
                        Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                    };
                    cases += 1;
                    let ok = match direction {
                        MonotonicDirection::NonDecreasing => fa <= fb,
                        MonotonicDirection::NonIncreasing => fa >= fb,
                        _ => false,
                    };
                    if !ok {
                        return (cases, Some(violation(op_id, "monotonic", a, b, 0, fa, fb)));
                    }
                }
            }
            for &a in PATHOLOGICAL_U32_WITNESSES {
                for &b in PATHOLOGICAL_U32_WITNESSES {
                    if a <= b {
                        let fa = match call_unary(f, a) {
                            Ok(v) => v,
                            Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                        };
                        let fb = match call_unary(f, b) {
                            Ok(v) => v,
                            Err(e) => return (cases, Some(engine_failure_violation(op_id, e))),
                        };
                        cases += 1;
                        let ok = match direction {
                            MonotonicDirection::NonDecreasing => fa <= fb,
                            MonotonicDirection::NonIncreasing => fa >= fb,
                            _ => false,
                        };
                        if !ok {
                            return (cases, Some(violation(op_id, "monotonic", a, b, 0, fa, fb)));
                        }
                    }
                }
            }
            (cases, None)
        }
        AlgebraicLaw::DeMorgan { inner_op, dual_op } => {
            match crate::proof::algebra::laws::demorgan::check_exhaustive_u8(
                op_id, f, inner_op, dual_op, 0,
            ) {
                Ok(r) => r,
                Err(v) => (0, Some(v)),
            }
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => match crate::proof::algebra::laws::complement::check_exhaustive_u8(
            op_id,
            f,
            complement_op,
            *universe,
            0,
        ) {
            Ok(r) => r,
            Err(v) => (0, Some(v)),
        },
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => {
            crate::proof::algebra::laws::custom::check_exhaustive_u8(op_id, f, name, *arity, *check)
        }
        other => {
            // Unknown law variant — return a structured failure instead of panicking.
            (
                0,
                Some(violation(
                    op_id,
                    &format!("unimplemented: {}", other.name()),
                    0,
                    0,
                    0,
                    0,
                    0,
                )),
            )
        }
    }
}

#[inline]
pub(crate) fn check_unary_law_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    count: u64,
) -> (u64, Option<LawViolation>) {
    let mut rng = simple_rng(op_id, law.name());
    let grid = boundary_grid_u32();

    match law {
        AlgebraicLaw::Involution => {
            // F5: Boundary grid sweep
            for &a in &grid {
                let ffa = match call_unary(f, a) {
                    Ok(v) => match call_unary(f, v) {
                        Ok(v2) => v2,
                        Err(e) => return (0, Some(engine_failure_violation(op_id, e))),
                    },
                    Err(e) => return (0, Some(engine_failure_violation(op_id, e))),
                };
                if ffa != a {
                    return (1, Some(violation(op_id, "involution", a, 0, 0, ffa, a)));
                }
            }
            for i in 0..count {
                let a = rng.next_u32();
                let ffa = match call_unary(f, a) {
                    Ok(v) => match call_unary(f, v) {
                        Ok(v2) => v2,
                        Err(e) => return (i, Some(engine_failure_violation(op_id, e))),
                    },
                    Err(e) => return (i, Some(engine_failure_violation(op_id, e))),
                };
                if ffa != a {
                    return (i + 1, Some(violation(op_id, "involution", a, 0, 0, ffa, a)));
                }
            }
            (count, None)
        }
        AlgebraicLaw::Bounded { lo, hi } => {
            // F5: Boundary grid sweep
            for &a in &grid {
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (0, Some(engine_failure_violation(op_id, e))),
                };
                if fa < *lo || fa > *hi {
                    return (1, Some(violation(op_id, "bounded", a, 0, 0, fa, *lo)));
                }
            }
            for i in 0..count {
                let a = rng.next_u32();
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (i, Some(engine_failure_violation(op_id, e))),
                };
                if fa < *lo || fa > *hi {
                    return (i + 1, Some(violation(op_id, "bounded", a, 0, 0, fa, *lo)));
                }
            }
            (count, None)
        }
        AlgebraicLaw::Monotonic { direction } => {
            for i in 0..count {
                let a = rng.next_u32();
                let b = rng.next_u32();
                let (a, b) = if a <= b { (a, b) } else { (b, a) };
                let fa = match call_unary(f, a) {
                    Ok(v) => v,
                    Err(e) => return (i, Some(engine_failure_violation(op_id, e))),
                };
                let fb = match call_unary(f, b) {
                    Ok(v) => v,
                    Err(e) => return (i, Some(engine_failure_violation(op_id, e))),
                };
                let ok = match direction {
                    MonotonicDirection::NonDecreasing => fa <= fb,
                    MonotonicDirection::NonIncreasing => fa >= fb,
                    _ => false,
                };
                if !ok {
                    return (i + 1, Some(violation(op_id, "monotonic", a, b, 0, fa, fb)));
                }
            }
            (count, None)
        }
        AlgebraicLaw::DeMorgan { inner_op, dual_op } => {
            match crate::proof::algebra::laws::demorgan::check_witnessed_u32(
                op_id, f, inner_op, dual_op, count,
            ) {
                Ok(r) => r,
                Err(v) => (0, Some(v)),
            }
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => match crate::proof::algebra::laws::complement::check_witnessed_u32(
            op_id,
            f,
            complement_op,
            *universe,
            count,
        ) {
            Ok(r) => r,
            Err(v) => (0, Some(v)),
        },
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => crate::proof::algebra::laws::custom::check_witnessed_u32(
            op_id, f, name, *arity, *check, count,
        ),
        other => (
            0,
            Some(violation(
                op_id,
                &format!("unimplemented witnessed: {}", other.name()),
                0,
                0,
                0,
                0,
                0,
            )),
        ),
    }
}

#[inline]
pub(crate) fn violation(
    op_id: &str,
    law: &str,
    a: u32,
    b: u32,
    c: u32,
    lhs: u32,
    rhs: u32,
) -> LawViolation {
    LawViolation {
        law: law.to_string(),
        op_id: op_id.to_string(),
        a,
        b,
        c,
        lhs,
        rhs,
        message: format!(
            "{law} violated: f({a}, {b}{}) = {lhs}, expected {rhs}",
            if c != 0 {
                format!(", {c}")
            } else {
                String::new()
            }
        ),
    }
}

/// Build a structured `LawViolation` when an engine evaluation fails.
#[inline]
pub(crate) fn engine_failure_violation(op_id: &str, err: SupportError) -> LawViolation {
    LawViolation {
        law: "engine-failure".to_string(),
        op_id: op_id.to_string(),
        a: 0,
        b: 0,
        c: 0,
        lhs: 0,
        rhs: 0,
        message: format!(
            "engine evaluation failed: {err}. Fix: ensure the reference engine produces valid 4-byte u32 outputs."
        ),
    }
}

/// Build a structured `LawViolation` when a law declares a companion op id
/// but the registry has no matching OpSpec. Replaces the old `panic!()` pattern
/// so registry gaps become recoverable findings instead of process aborts.
#[inline]
pub(crate) fn missing_companion_violation(
    op_id: &str,
    law: &str,
    companion_op: &str,
    role: &str,
    expected_signature: &str,
) -> LawViolation {
    LawViolation {
        law: law.to_string(),
        op_id: op_id.to_string(),
        a: 0,
        b: 0,
        c: 0,
        lhs: 0,
        rhs: 0,
        message: format!(
            "missing {role} companion op `{companion_op}` for {law} on `{op_id}`. \
             Fix: register a {expected_signature} OpSpec with id `{companion_op}` \
             or remove the declared {law} law from `{op_id}`."
        ),
    }
}