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

//! Violation witness minimizer.
//!
//! Given a violation witness (a, b), try to shrink the inputs while
//! preserving the violation. This makes reported violations easier to
//! read and debug.

use crate::proof::algebra::checker::support::{call_binary, call_unary, SupportError};
use crate::spec::law::AlgebraicLaw;

/// Minimize a binary violation witness.
#[inline]
pub fn minimize_binary(f: fn(&[u8]) -> Vec<u8>, law: &AlgebraicLaw, a: u32, b: u32) -> (u32, u32) {
    let mut cur_a = a;
    let mut cur_b = b;
    if !binary_pair_violates(f, law, cur_a, cur_b).unwrap_or(false) {
        return (cur_a, cur_b);
    }

    loop {
        let old_a = cur_a;
        let old_b = cur_b;
        let next_a = minimize_value(cur_a, |next| {
            binary_pair_violates(f, law, next, cur_b).unwrap_or(false)
        });
        cur_a = next_a;

        let next_b = minimize_value(cur_b, |next| {
            binary_pair_violates(f, law, cur_a, next).unwrap_or(false)
        });
        if next_a == old_a && next_b == old_b {
            return (cur_a, cur_b);
        }
        cur_b = next_b;

        let still_violates = binary_pair_violates(f, law, cur_a, cur_b).unwrap_or(false);
        if !still_violates {
            return (cur_a, cur_b);
        }
    }
}

/// Minimize a unary violation witness.
#[inline]
pub fn minimize_unary(f: fn(&[u8]) -> Vec<u8>, law: &AlgebraicLaw, a: u32) -> u32 {
    if !unary_input_violates(f, law, a).unwrap_or(false) {
        return a;
    }
    minimize_value(a, |next| {
        unary_input_violates(f, law, next).unwrap_or(false)
    })
}

fn minimize_value(mut current: u32, mut violates: impl FnMut(u32) -> bool) -> u32 {
    let exhaustive_limit = current.min(1024);
    for candidate in 0..=exhaustive_limit {
        if violates(candidate) {
            return candidate;
        }
    }
    if current <= exhaustive_limit {
        return current;
    }

    let mut low = exhaustive_limit.saturating_add(1);
    let mut high = current;
    while low < high {
        let mid = low + ((high - low) / 2);
        if violates(mid) {
            high = mid;
        } else {
            low = mid.saturating_add(1);
        }
    }
    if low < current && violates(low) {
        current = low;
    }
    current
}

fn binary_pair_violates(
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    a: u32,
    b: u32,
) -> Result<bool, SupportError> {
    match law {
        AlgebraicLaw::Commutative => Ok(call_binary(f, a, b)? != call_binary(f, b, a)?),
        AlgebraicLaw::Associative => Ok(false), // needs a third operand
        AlgebraicLaw::Identity { element } => {
            let e = *element;
            Ok(call_binary(f, a, e)? != a || call_binary(f, e, a)? != a)
        }
        AlgebraicLaw::SelfInverse { result } => {
            let r = *result;
            Ok(call_binary(f, a, a)? != r || call_binary(f, b, b)? != r)
        }
        AlgebraicLaw::Idempotent => Ok(call_binary(f, a, a)? != a || call_binary(f, b, b)? != b),
        AlgebraicLaw::Absorbing { element } => {
            let z = *element;
            Ok(call_binary(f, a, z)? != z
                || call_binary(f, z, a)? != z
                || call_binary(f, b, z)? != z
                || call_binary(f, z, b)? != z)
        }
        AlgebraicLaw::Bounded { lo, hi } => {
            let ab = call_binary(f, a, b)?;
            Ok(ab < *lo || ab > *hi)
        }
        AlgebraicLaw::ZeroProduct { holds: true } => {
            Ok(call_binary(f, a, b)? == 0 && a != 0 && b != 0)
        }
        AlgebraicLaw::ZeroProduct { holds: false } => {
            Ok(call_binary(f, a, b)? == 0 && a != 0 && b != 0)
        }
        AlgebraicLaw::Custom { check, .. } => Ok(!check(f, &[a, b])),
        _ => Ok(false),
    }
}

fn unary_input_violates(
    f: fn(&[u8]) -> Vec<u8>,
    law: &AlgebraicLaw,
    a: u32,
) -> Result<bool, SupportError> {
    match law {
        AlgebraicLaw::Involution => {
            let fa = call_unary(f, a)?;
            Ok(call_unary(f, fa)? != a)
        }
        AlgebraicLaw::Bounded { lo, hi } => {
            let fa = call_unary(f, a)?;
            Ok(fa < *lo || fa > *hi)
        }
        AlgebraicLaw::Custom { check, .. } => Ok(!check(f, &[a])),
        _ => Ok(false),
    }
}