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

//! Cache and seal inferred mandatory laws.

use std::collections::HashMap;
use std::sync::Mutex;
use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::inference::{binary_candidate_laws, unary_candidate_laws};
use crate::spec::law::AlgebraicLaw;
/// Re-export of cross-op law inference.
pub use super::cross::infer_cross_op_laws;
use super::{CacheKey, compute_laws, fn_addr_hash, lock_cache};

/// Run exhaustive u8 proof for every applicable law and return only those that hold.
#[inline]
pub fn infer_and_seal(
    op_id: &'static str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    is_binary: bool,
) -> Vec<AlgebraicLaw> {
    let key = CacheKey {
        op_id,
        is_binary,
        fn_hash: fn_addr_hash(cpu_fn),
    };
    {
        let mut guard = lock_cache();
        if let Some(cache) = guard.as_mut() {
            if let Some(laws) = cache.get(&key) {
                return laws.clone();
            }
        }
    }
    let laws = compute_laws(op_id, cpu_fn, is_binary);
    let mut guard = lock_cache();
    guard
        .get_or_insert_with(HashMap::new)
        .insert(key, laws.clone());
    laws
}