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

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

fn check_associative_exhaustive(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    let mut cases = 0u64;
    for a in 0u32..256 {
        for b in 0u32..256 {
            for c in 0u32..256 {
                let ab = call_binary(f, a, b).map_err(|e| engine_failure_violation(op_id, e))?;
                let ab_c = call_binary(f, ab, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let bc = call_binary(f, b, c).map_err(|e| engine_failure_violation(op_id, e))?;
                let a_bc = call_binary(f, a, bc).map_err(|e| engine_failure_violation(op_id, e))?;
                cases += 1;
                if ab_c != a_bc {
                    return Ok((
                        cases,
                        Some(violation(op_id, "associative", a, b, c, ab_c, a_bc)),
                    ));
                }
            }
        }
    }
    Ok((cases, None))
}