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

//! Falsifiability matrix for all cataloged laws.

use super::{entry, FalsifiabilityEntry};

/// Falsifiability matrix: every law must have a checker that can distinguish
/// a correct reference from a deliberately broken one.
pub static FALSIFIABILITY_MATRIX: &[FalsifiabilityEntry] = &[
    entry("commutative", "sub: f(0,1)=4294967295 != f(1,0)=1"),
    entry(
        "associative",
        "sub: f(f(1,1),2)=4294967294 != f(1,f(1,2))=2",
    ),
    entry("identity(0)", "add with declared element 1: f(0,1)=1 != 0"),
    entry(
        "left-identity(0)",
        "add with declared element 1: f(1,0)=1 != 0",
    ),
    entry(
        "right-identity(0)",
        "add with declared element 1: f(0,1)=1 != 0",
    ),
    entry("self-inverse(0)", "or with result 0: f(1,1)=1 != 0"),
    entry("idempotent", "add: f(1,1)=2 != 1"),
    entry("absorbing(0)", "or with element 0: f(1,0)=1 != 0"),
    entry("left-absorbing(0)", "broken z=1 absorber: f(1,0)=0 != 1"),
    entry("right-absorbing(0)", "broken z=1 absorber: f(0,1)=0 != 1"),
    entry("involution", "clear-low-bit: f(f(1))=0 != 1"),
    entry("monotone", "bitwise-not: 0 <= 1 but f(0) > f(1)"),
    entry(
        "bounded(0,4294967295)",
        "popcount+1: f(4294967295)=33 outside [0,32]",
    ),
    entry(
        "zero-product(true)",
        "wrapping-mul: f(2,2147483648)=0 with nonzero operands",
    ),
    entry(
        "de-morgan(and,or)",
        "identity-not: f(and(0,1))=0 != or(f(0),f(1))=1",
    ),
    entry(
        "monotonic(NonDecreasing)",
        "bitwise-not: 0 <= 1 but f(0) > f(1)",
    ),
    entry(
        "complement(not,4294967295)",
        "popcount/not: f(0)+f(not(0))=33 != 32",
    ),
    entry(
        "distributive(add)",
        "bad-mul: f(3,add(0,0))=1 != add(f(3,0),f(3,0))=2",
    ),
    entry(
        "lattice-absorption(min)",
        "fake-max-add: f(1,min(1,1))=2 != 1",
    ),
    entry("inverse-of(add)", "sub+1: f(add(1,1),1)=2 != 1"),
    entry(
        "trichotomy(lt,eq,gt)",
        "lt-always-zero at (0,1): lt+eq+gt=0 != 1",
    ),
    entry(
        "custom(parity-even,1)",
        "parity-even custom check rejects input 1",
    ),
];