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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

//! Checker for lattice absorption.

use crate::proof::algebra::checker::support::{
    call_binary, engine_failure_violation, missing_companion_violation, simple_rng, violation,
};
use crate::spec::law::LawViolation;
use crate::{spec::op_registry, DataType};

use super::BOUNDARY_VALUES;

/// Verify `f(a, g(a,b)) = a` over u8 plus u32 witnesses.
#[inline]
pub(crate) fn check_exhaustive_u8(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    dual_op: &str,
    witness_count: u64,
) -> (u64, Option<LawViolation>) {
    let Some(dual) = lookup_binary(dual_op) else {
        return (
            0,
            Some(missing_companion_violation(
                op_id,
                "LatticeAbsorption",
                dual_op,
                "dual",
                "u32,u32 -> u32",
            )),
        );
    };
    let mut cases = 0;
    for a in 0u32..256 {
        for b in 0u32..256 {
            cases += 1;
            if let Some(v) = check_case(op_id, f, dual, a, b) {
                return (cases, Some(v));
            }
        }
    }
    check_witnesses(op_id, f, dual, cases, witness_count)
}

/// Verify `f(a, g(a,b)) = a` over deterministic u32 witnesses.
#[inline]
pub(crate) fn check_witnessed_u32(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    dual_op: &str,
    count: u64,
) -> (u64, Option<LawViolation>) {
    let Some(dual) = lookup_binary(dual_op) else {
        return (
            0,
            Some(missing_companion_violation(
                op_id,
                "LatticeAbsorption",
                dual_op,
                "dual",
                "u32,u32 -> u32",
            )),
        );
    };
    check_witnesses(op_id, f, dual, 0, count)
}

fn check_witnesses(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    dual: fn(&[u8]) -> Vec<u8>,
    mut cases: u64,
    count: u64,
) -> (u64, Option<LawViolation>) {
    for &a in BOUNDARY_VALUES {
        for &b in BOUNDARY_VALUES {
            cases += 1;
            if let Some(v) = check_case(op_id, f, dual, a, b) {
                return (cases, Some(v));
            }
        }
    }
    let mut rng = simple_rng(op_id, "lattice-absorption");
    for _ in 0..count {
        let a = rng.next_u32();
        let b = rng.next_u32();
        cases += 1;
        if let Some(v) = check_case(op_id, f, dual, a, b) {
            return (cases, Some(v));
        }
    }
    (cases, None)
}

fn check_case(
    op_id: &str,
    f: fn(&[u8]) -> Vec<u8>,
    dual: fn(&[u8]) -> Vec<u8>,
    a: u32,
    b: u32,
) -> Option<LawViolation> {
    let dual_ab = match call_binary(dual, a, b) {
        Ok(v) => v,
        Err(e) => return Some(engine_failure_violation(op_id, e)),
    };
    let actual = match call_binary(f, a, dual_ab) {
        Ok(v) => v,
        Err(e) => return Some(engine_failure_violation(op_id, e)),
    };
    if actual != a {
        return Some(violation(op_id, "lattice-absorption", a, b, 0, actual, a));
    }

    // Dual absorption: g(a, f(a,b)) = a
    let f_ab = match call_binary(f, a, b) {
        Ok(v) => v,
        Err(e) => return Some(engine_failure_violation(op_id, e)),
    };
    let dual_actual = match call_binary(dual, a, f_ab) {
        Ok(v) => v,
        Err(e) => return Some(engine_failure_violation(op_id, e)),
    };
    if dual_actual != a {
        Some(violation(
            op_id,
            "lattice-absorption",
            a,
            b,
            0,
            dual_actual,
            a,
        ))
    } else {
        None
    }
}

fn lookup_binary(op_id: &str) -> Option<fn(&[u8]) -> Vec<u8>> {
    op_registry::all_specs()
        .into_iter()
        .find(|spec| {
            spec.id == op_id
                && spec.signature.inputs == [DataType::U32, DataType::U32]
                && spec.signature.output == DataType::U32
        })
        .map(|spec| spec.cpu_fn)
}