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
29
30
31
32
33
34
35
36
37
38
39

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::{check_binary_law_exhaustive_u8, LawResult, VerificationLevel};

fn verify_one_law_exhaustive(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    is_binary: bool,
) -> LawResult {
    let (cases, violation) = if is_binary {
        check_binary_law_exhaustive_u8(op_id, cpu_fn, law)
    } else {
        check_unary_law_exhaustive_u8(op_id, cpu_fn, law)
    };
    let violation = violation.map(|v| {
        if is_binary {
            match minimize_binary_violation(op_id, cpu_fn, law, v.a, v.b, v.c) {
                Ok(minimized) => minimized.unwrap_or(v),
                Err(rebuild_err) => rebuild_err,
            }
        } else {
            match minimize_unary_violation(op_id, cpu_fn, law, v.a) {
                Ok(minimized) => minimized.unwrap_or(v),
                Err(rebuild_err) => rebuild_err,
            }
        }
    });
    LawResult {
        op_id: op_id.to_string(),
        law_name: law.name().to_string(),
        level: VerificationLevel::ExhaustiveU8,
        cases_tested: cases,
        violation,
    }
}