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

//! Single-law trial for mandatory inference.

use std::collections::HashMap;
use std::sync::Mutex;
use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::inference::{binary_candidate_laws, unary_candidate_laws};
use crate::spec::law::AlgebraicLaw;
/// Re-export of cross-op law inference.
pub use super::cross::infer_cross_op_laws;

fn try_law(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: AlgebraicLaw,
    is_binary: bool,
    proven: &mut Vec<AlgebraicLaw>,
) {
    let results = verify_laws(op_id, cpu_fn, &[law.clone()], is_binary);
    for result in results {
        if result.cases_tested == 0 {
            continue;
        }
        if result.violation.is_none() {
            proven.push(law);
            return;
        }
    }
}