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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

//! Individual law checker modules.
//!
//! Each law has its own module for documentation and extensibility.
//! The actual checking logic is in `checker.rs` — these modules provide
//! law-specific utilities and constants.

/// Canonical boundary values shared by all law checkers.
///
/// These values sit on semantic edges where GPU implementations commonly
/// fail: zero, one, bit boundaries, sign bit, maximum. Every law checker
/// must test at least these values in addition to its exhaustive/witnessed
/// coverage.
pub(crate) const BOUNDARY_VALUES: &[u32] = &[
    0,           // additive identity, absorbing element
    1,           // multiplicative identity
    2,           // smallest non-trivial
    31,          // shift mask boundary (31 & 31 = 31)
    32,          // shift mask wrap (32 & 31 = 0)
    0x0001_0000, // 16-bit boundary
    0x7FFF_FFFF, // max positive i32
    0x8000_0000, // min negative i32 / sign bit
    0xFFFF_FFFE, // max - 1
    u32::MAX,    // maximum value
];

pub(crate) mod binary;
pub(crate) mod complement;
pub(crate) mod custom;
pub(crate) mod demorgan;
pub(crate) mod distributive;
pub(crate) mod inverse;
pub(crate) mod lattice;
pub(crate) mod one_sided;
pub(crate) mod trichotomy;

/// One entry in the falsifiability matrix.
pub struct FalsifiabilityEntry {
    /// Law name matching `canonical_law_id`.
    pub law_name: &'static str,
    /// Canonical broken implementation and witness proving falsifiability.
    pub canonical_counterexample: &'static str,
    /// Whether the checker can produce a counterexample for a broken reference.
    pub catches_violator: bool,
    /// Whether the checker passes an honest (correct) reference.
    pub passes_honest: bool,
}

const fn entry(
    law_name: &'static str,
    canonical_counterexample: &'static str,
) -> FalsifiabilityEntry {
    FalsifiabilityEntry {
        law_name,
        canonical_counterexample,
        catches_violator: true,
        passes_honest: true,
    }
}

/// 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",
    ),
];