vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation
//! Checkers for one-sided identity and zero-absorbing laws.

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

/// Side of the binary operation constrained by the law.
#[derive(Clone, Copy)]
pub(crate) enum Side {
    /// Fixed element is the left argument.
    Left,
    /// Fixed element is the right argument.
    Right,
}

/// Verify a one-sided identity over exhaustive u8 inputs.
#[inline]
pub(crate) fn check_identity_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0;
    for a in 0u32..256 {
        cases += 1;
        if let Some(v) = identity_case(op_id, f, side, element, a)? {
            return Ok((cases, Some(v)));
        }
    }
    Ok((cases, None))
}

/// Verify a one-sided identity over deterministic u32 witnesses.
#[inline]
pub(crate) fn check_identity_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
    count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut rng = simple_rng(op_id, identity_law_name(side));
    for i in 0..count {
        if let Some(v) = identity_case(op_id, f, side, element, rng.next_u32())? {
            return Ok((i + 1, Some(v)));
        }
    }
    Ok((count, None))
}

/// Verify a one-sided absorbing law over exhaustive u8 inputs.
#[inline]
pub(crate) fn check_absorbing_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0;
    for a in 0u32..256 {
        cases += 1;
        if let Some(v) = absorbing_case(op_id, f, side, element, a)? {
            return Ok((cases, Some(v)));
        }
    }
    Ok((cases, None))
}

/// Verify a one-sided absorbing law over deterministic u32 witnesses.
#[inline]
pub(crate) fn check_absorbing_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
    count: u64,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut rng = simple_rng(op_id, absorbing_law_name(side));
    for i in 0..count {
        if let Some(v) = absorbing_case(op_id, f, side, element, rng.next_u32())? {
            return Ok((i + 1, Some(v)));
        }
    }
    Ok((count, None))
}

fn identity_case(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
    a: u32,
) -> Result<Option<LawViolation>, LawViolation> {
    let actual = match side {
        Side::Left => call_binary(f, element, a).map_err(|e| engine_failure_violation(op_id, e))?,
        Side::Right => {
            call_binary(f, a, element).map_err(|e| engine_failure_violation(op_id, e))?
        }
    };
    if actual == a {
        Ok(None)
    } else {
        let (left, right) = match side {
            Side::Left => (element, a),
            Side::Right => (a, element),
        };
        Ok(Some(violation(
            op_id,
            identity_law_name(side),
            left,
            right,
            0,
            actual,
            a,
        )))
    }
}

fn absorbing_case(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    side: Side,
    element: u32,
    a: u32,
) -> Result<Option<LawViolation>, LawViolation> {
    let actual = match side {
        Side::Left => call_binary(f, element, a).map_err(|e| engine_failure_violation(op_id, e))?,
        Side::Right => {
            call_binary(f, a, element).map_err(|e| engine_failure_violation(op_id, e))?
        }
    };
    if actual == element {
        Ok(None)
    } else {
        let (left, right) = match side {
            Side::Left => (element, a),
            Side::Right => (a, element),
        };
        Ok(Some(violation(
            op_id,
            absorbing_law_name(side),
            left,
            right,
            0,
            actual,
            element,
        )))
    }
}

fn identity_law_name(side: Side) -> &'static str {
    match side {
        Side::Left => "left-identity",
        Side::Right => "right-identity",
    }
}

fn absorbing_law_name(side: Side) -> &'static str {
    match side {
        Side::Left => "left-absorbing",
        Side::Right => "right-absorbing",
    }
}