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

pub use verify_law::verify_law;

use crate::properties::tests::{pair, primitive, result_u32, unary};
use crate::spec::law::AlgebraicLaw;

#[test]
fn all_declared_laws_hold_on_cpu_reference() {
    for spec in primitive::specs() {
        for law in &spec.laws {
            super::verify_law::verify_law(&spec, law);
        }
    }
}

use crate::properties::tests::declared_laws::{
    commutative, associative, identity, bounded, distributive, demorgan,
};
use super::super::{complement, custom, monotone, zero_product};
use super::super::infra::{lookup_primitive_cpu, is_unary_spec};

#[inline]
pub fn verify_law(spec: &crate::spec::types::OpSpec, law: &AlgebraicLaw) {
    match law {
        AlgebraicLaw::Commutative => commutative::verify_commutative(spec),
        AlgebraicLaw::Associative => associative::verify_associative(spec),
        AlgebraicLaw::Identity { element } => identity::verify_identity(spec, *element),
        AlgebraicLaw::SelfInverse { result } => identity::verify_self_inverse(spec, *result),
        AlgebraicLaw::Idempotent => identity::verify_idempotent(spec),
        AlgebraicLaw::Absorbing { element } => identity::verify_absorbing(spec, *element),
        AlgebraicLaw::Involution => identity::verify_involution(spec),
        AlgebraicLaw::Bounded { lo, hi } => bounded::verify_bounded(spec, *lo, *hi),
        AlgebraicLaw::ZeroProduct { holds } => zero_product::verify_zero_product(spec, *holds),
        AlgebraicLaw::DeMorgan { inner_op, dual_op } => {
            let inner = lookup_primitive_cpu(*inner_op);
            let dual = lookup_primitive_cpu(*dual_op);
            demorgan::check_demorgan(spec.id, spec.cpu_fn, *inner_op, inner, *dual_op, dual);
        }
        AlgebraicLaw::Monotone => {
            monotone::check_monotone(spec.id, spec.cpu_fn);
        }
        AlgebraicLaw::Complement {
            complement_op,
            universe,
        } => {
            let comp = lookup_primitive_cpu(*complement_op);
            if is_unary_spec(spec) {
                complement::check_complement_unary(spec.id, spec.cpu_fn, *complement_op, comp, *universe);
            } else {
                complement::check_complement_binary(spec.id, spec.cpu_fn, *complement_op, comp, *universe);
            }
        }
        AlgebraicLaw::DistributiveOver { over_op } => {
            let over = lookup_primitive_cpu(*over_op);
            distributive::check_distributive(spec.id, spec.cpu_fn, *over_op, over);
        }
        AlgebraicLaw::Custom {
            name,
            arity,
            check,
            ..
        } => {
            custom::check_custom(spec.id, spec.cpu_fn, *name, *arity, *check);
        }
        // Non-exhaustive enum — every other variant is either handled above
        // or deliberately delegated to the algebra checker, so no fallthrough
        // is required here.
        _ => {
            // Laws not self-tested here: InverseOf, LeftIdentity, RightIdentity,
            // LeftAbsorbing, RightAbsorbing, LatticeAbsorption, Trichotomy, etc.
            // Those are verified by the conformance harness via the algebra
            // checker, not by this CPU-only self-test.
        }
    }
}