vyre-conform 0.1.0

//! Mandatory law inference for certified algebra declarations.

use std::collections::HashMap;
use std::sync::Mutex;

mod cross;

use crate::proof::algebra::checker::verify_laws;
use crate::proof::algebra::inference::{binary_candidate_laws, unary_candidate_laws};
use crate::spec::law::AlgebraicLaw;

/// Cross-operation law inference re-export.
pub use cross::infer_cross_op_laws;

static CACHE: Mutex<Option<HashMap<CacheKey, Vec<AlgebraicLaw>>>> = Mutex::new(None);

#[derive(Clone, Copy, PartialEq, Eq, Hash)]
struct CacheKey {
    op_id: &'static str,
    is_binary: bool,
    fn_hash: u64,
}

fn fn_addr_hash(f: fn(&[u8]) -> Vec<u8>) -> u64 {
    f as usize as u64
}

/// 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
}

fn lock_cache() -> std::sync::MutexGuard<'static, Option<HashMap<CacheKey, Vec<AlgebraicLaw>>>> {
    CACHE
        .lock()
        .unwrap_or_else(|poisoned| poisoned.into_inner())
}

fn compute_laws(op_id: &str, cpu_fn: fn(&[u8]) -> Vec<u8>, is_binary: bool) -> Vec<AlgebraicLaw> {
    let mut proven = Vec::new();
    let candidates = if is_binary {
        binary_candidate_laws()
    } else {
        unary_candidate_laws()
    };
    for law in candidates {
        try_law(op_id, cpu_fn, law, is_binary, &mut proven);
    }
    proven
}

fn try_law(
    op_id: &str,
    cpu_fn: fn(&[u8]) -> Vec<u8>,
    law: AlgebraicLaw,
    is_binary: bool,
    proven: &mut Vec<AlgebraicLaw>,
) {
    let results = verify_laws(op_id, cpu_fn, std::slice::from_ref(&law), is_binary);
    for result in results {
        if result.cases_tested == 0 {
            continue;
        }
        if result.violation.is_none() {
            proven.push(law);
            return;
        }
    }
}