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

//! Verification level taxonomy for law checking.

use crate::spec::law::{AlgebraicLaw, LawViolation};
#[cfg(not(loom))]
use rayon::prelude::*;
use super::support::{check_unary_law_exhaustive_u8, check_unary_law_witnessed_u32};
use super::rebuild::{minimize_binary_violation, minimize_unary_violation};

/// Verification level.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum VerificationLevel {
    /// Exhaustive on u8 domain. Proof within domain.
    ExhaustiveU8,
    /// Random witnesses on u32 domain.
    WitnessedU32 {
        /// Number of witnesses.
        count: u64,
    },
    /// Random witnesses on u32 domain through a GPU backend.
    GpuWitnessedU32 {
        /// Number of witnesses.
        count: u64,
    },
    /// Both exhaustive u8 and witnessed u32.
    Combined {
        /// Number of u32 witnesses.
        witness_count: u64,
    },
}