rexact-check 0.2.0

//! Independent checker for certificates and witnesses (NFR-M01, FR-G01).
//!
//! Contract: consumes only the documented serialisations (the term "spec"
//! format and the certificate JSON); it has its own term type, normaliser,
//! derivative function, matcher and JSON reader, written in a deliberately
//! simple, unoptimised style. INVARIANT: this crate depends on no other
//! project crate (enforced by `scripts/check_independence.py`), so a defect in
//! the engine cannot also be present here.
//!
//! Failure modes: every problem is a [`CheckError`] carrying the catalogue code
//! `RX-E001` (evidence rejected) or `RX-E004` (malformed or unknown version).
//! Deep terms are handled by running on a thread with a large stack.

mod cert;
mod json;
mod term;

pub use cert::{check_certificate, check_counterexample, check_witness, CertInfo};

/// A rejected or malformed piece of evidence.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CheckError {
    /// `RX-E001` (rejected) or `RX-E004` (malformed or unknown version).
    pub code: &'static str,
    /// What was wrong, including the failing pair where there is one.
    pub message: String,
}

impl std::fmt::Display for CheckError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}: {}", self.code, self.message)
    }
}

impl std::error::Error for CheckError {}

pub(crate) fn rejected(msg: impl Into<String>) -> CheckError {
    CheckError {
        code: "RX-E001",
        message: msg.into(),
    }
}
pub(crate) fn malformed(msg: impl Into<String>) -> CheckError {
    CheckError {
        code: "RX-E004",
        message: msg.into(),
    }
}

/// Run `f` on a thread with a large stack: terms from counted repetition are
/// thousands of levels deep and the checker is plainly recursive. A panic in
/// the checker aborts the process: it must never be mistaken for "valid".
#[cfg(target_arch = "wasm32")]
pub(crate) fn on_big_stack<R: Send + 'static>(f: impl FnOnce() -> R + Send + 'static) -> R {
    // No threads on WebAssembly: the module is linked with a large stack instead.
    f()
}

#[cfg(not(target_arch = "wasm32"))]
pub(crate) fn on_big_stack<R: Send + 'static>(f: impl FnOnce() -> R + Send + 'static) -> R {
    match std::thread::Builder::new()
        .stack_size(256 * 1024 * 1024)
        .spawn(f)
    {
        Ok(h) => match h.join() {
            Ok(r) => r,
            Err(_) => std::process::abort(),
        },
        Err(_) => std::process::abort(),
    }
}