vyre-conform 0.1.0

//! Witnessed u32 binary law checkers.

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

pub(super) fn check_identity_witnessed(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    e: u32,
    count: u64,
    grid: &[u32],
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for &a in grid {
        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)),
            ));
        }
    }

    let mut rng = simple_rng(op_id, "identity");
    for i in 0..count {
        let a = rng.next_u32();
        let ae = call_binary(f, a, e).map_err(|e| engine_failure_violation(op_id, e))?;
        if ae != a {
            return Ok((
                cases + i + 1,
                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 + i + 1,
                Some(violation(op_id, "identity(left)", e, a, 0, ea, a)),
            ));
        }
    }
    Ok((cases + count, None))
}

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

    let mut rng = simple_rng(op_id, "self-inverse");
    for i in 0..count {
        let a = rng.next_u32();
        let aa = call_binary(f, a, a).map_err(|e| engine_failure_violation(op_id, e))?;
        if aa != r {
            return Ok((
                cases + i + 1,
                Some(violation(op_id, "self-inverse", a, a, 0, aa, r)),
            ));
        }
    }
    Ok((cases + count, None))
}

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

    let mut rng = simple_rng(op_id, "idempotent");
    for i in 0..count {
        let a = rng.next_u32();
        let aa = call_binary(f, a, a).map_err(|e| engine_failure_violation(op_id, e))?;
        if aa != a {
            return Ok((
                cases + i + 1,
                Some(violation(op_id, "idempotent", a, a, 0, aa, a)),
            ));
        }
    }
    Ok((cases + count, None))
}

pub(super) fn check_absorbing_witnessed(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    z: u32,
    count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let grid = boundary_grid_u32();
    let mut cases = 0u64;
    for &a in &grid {
        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)),
            ));
        }
    }

    let mut rng = simple_rng(op_id, "absorbing");
    for i in 0..count {
        let a = rng.next_u32();
        let az = call_binary(f, a, z).map_err(|e| engine_failure_violation(op_id, e))?;
        if az != z {
            return Ok((
                cases + i + 1,
                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 + i + 1,
                Some(violation(op_id, "absorbing(left)", z, a, 0, za, z)),
            ));
        }
    }
    Ok((cases + count, None))
}

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

    let mut rng = simple_rng(op_id, "bounded");
    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))?;
        if ab < lo || ab > hi {
            return Ok((
                cases + i + 1,
                Some(violation(op_id, "bounded", a, b, 0, ab, lo)),
            ));
        }
    }
    Ok((cases + count, None))
}

pub(super) fn check_zero_product_witnessed(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    holds: bool,
    count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let grid = boundary_grid_u32();
    let mut cases = 0u64;
    if !holds {
        for &a in &grid {
            for &b in &grid {
                cases += 1;
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                if a != 0 && b != 0 && ab == 0 {
                    return Ok((cases, None));
                }
            }
        }
        for (i, &(a, b)) in ZERO_PRODUCT_COUNTEREXAMPLES.iter().enumerate() {
            let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
            if ab == 0 {
                return Ok((cases + i as u64 + 1, None));
            }
        }
        let mut rng = simple_rng(op_id, "zero-product");
        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))?;
            if a != 0 && b != 0 && ab == 0 {
                return Ok((
                    cases + ZERO_PRODUCT_COUNTEREXAMPLES.len() as u64 + i + 1,
                    None,
                ));
            }
        }
        let zp = call_binary(f, 2, 0x8000_0000).map_err(|e| engine_failure_violation(op_id, e))?;
        return Ok((
            cases + ZERO_PRODUCT_COUNTEREXAMPLES.len() as u64 + count,
            Some(violation(
                op_id,
                "zero-product(false)",
                2,
                0x8000_0000,
                0,
                zp,
                0,
            )),
        ));
    }

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

    let mut rng = simple_rng(op_id, "zero-product");
    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))?;
        if ab == 0 && a != 0 && b != 0 {
            return Ok((
                cases + i + 1,
                Some(violation(op_id, "zero-product(true)", a, b, 0, ab, 1)),
            ));
        }
    }
    Ok((cases + count, None))
}