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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

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::{
    check_absorbing_exhaustive, check_associative_exhaustive, check_bounded_exhaustive,
    check_commutative_exhaustive, check_identity_exhaustive, check_idempotent_exhaustive,
    check_self_inverse_exhaustive, check_zero_product_exhaustive,
};

/// Verify one binary law over exhaustive u8 inputs.
#[inline]
pub(crate) fn check_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
) -> Result<(u64, Option<LawViolation>), LawViolation> {
    match law {
        AlgebraicLaw::Commutative => check_commutative_exhaustive(op_id, f),
        AlgebraicLaw::Associative => check_associative_exhaustive(op_id, f),
        AlgebraicLaw::Identity { element } => check_identity_exhaustive(op_id, f, *element),
        AlgebraicLaw::LeftIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
            )
        }
        AlgebraicLaw::RightIdentity { element } => {
            crate::proof::algebra::laws::one_sided::check_identity_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
            )
        }
        AlgebraicLaw::SelfInverse { result } => check_self_inverse_exhaustive(op_id, f, *result),
        AlgebraicLaw::Idempotent => check_idempotent_exhaustive(op_id, f),
        AlgebraicLaw::Absorbing { element } => check_absorbing_exhaustive(op_id, f, *element),
        AlgebraicLaw::LeftAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Left,
                *element,
            )
        }
        AlgebraicLaw::RightAbsorbing { element } => {
            crate::proof::algebra::laws::one_sided::check_absorbing_exhaustive_u8(
                op_id,
                f,
                crate::proof::algebra::laws::one_sided::Side::Right,
                *element,
            )
        }
        AlgebraicLaw::Bounded { lo, hi } => check_bounded_exhaustive(op_id, f, *lo, *hi),
        AlgebraicLaw::ZeroProduct { holds } => check_zero_product_exhaustive(op_id, f, *holds),
        AlgebraicLaw::DistributiveOver { over_op } => {
            crate::proof::algebra::laws::distributive::check_exhaustive_u8(op_id, f, over_op, 0)
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => crate::proof::algebra::laws::complement::check_binary_exhaustive_u8(
            op_id,
            f,
            complement_op,
            *universe,
            0,
        ),
        AlgebraicLaw::LatticeAbsorption { dual_op } => {
            Ok(crate::proof::algebra::laws::lattice::check_exhaustive_u8(op_id, f, dual_op, 0))
        }
        AlgebraicLaw::InverseOf { op } => {
            crate::proof::algebra::laws::inverse::check_exhaustive_u8(op_id, f, op, 0)
        }
        AlgebraicLaw::Trichotomy {
            less_op,
            equal_op,
            greater_op,
        } => crate::proof::algebra::laws::trichotomy::check_exhaustive_u8(
            op_id, f, less_op, equal_op, greater_op, 0,
        ),
        AlgebraicLaw::Custom {
            name, arity, check, ..
        } => Ok(crate::proof::algebra::laws::custom::check_exhaustive_u8(
            op_id, f, name, *arity, *check,
        )),
        other => Ok((0, Some(LawViolation {
            law: format!("{:?}", other),
            op_id: op_id.to_string(),
            message: format!("unimplemented binary law checker for {:?}. Fix: add a real checker or remove the declared law.", other),
            a: 0, b: 0, c: 0, lhs: 0, rhs: 0,
        }))),
    }
}