vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

//! Exhaustive u8 law verification entry point.

use crate::spec::law::{AlgebraicLaw, LawViolation};
#[cfg(not(loom))]
use rayon::prelude::*;
use super::support::{check_unary_law_exhaustive_u8, check_unary_law_witnessed_u32};
use super::rebuild::{minimize_binary_violation, minimize_unary_violation};
use super::{LawResult, verify_one_law_exhaustive};

/// Verify all declared laws for an operation using exhaustive u8 verification.
///
/// This is the proof path. Every input in the u8 domain is tested. If all
/// pass, the law is proven within u8.
///
/// `cpu_fn` takes raw bytes and returns raw bytes (the standard conform
/// reference function signature). For binary ops, input is 8 bytes (two u32
/// LE). For unary ops, input is 4 bytes.
#[inline]
pub fn verify_laws(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    laws: &[AlgebraicLaw],
    is_binary: bool,
) -> Vec<LawResult> {
    laws.iter()
        .map(|law| verify_one_law_exhaustive(op_id, cpu_fn, law, is_binary))
        .collect()
}