rexact_check/
lib.rs

1//! Independent checker for certificates and witnesses (NFR-M01, FR-G01).
2//!
3//! Contract: consumes only the documented serialisations (the term "spec"
4//! format and the certificate JSON); it has its own term type, normaliser,
5//! derivative function, matcher and JSON reader, written in a deliberately
6//! simple, unoptimised style. INVARIANT: this crate depends on no other
7//! project crate (enforced by `scripts/check_independence.py`), so a defect in
8//! the engine cannot also be present here.
9//!
10//! Failure modes: every problem is a [`CheckError`] carrying the catalogue code
11//! `RX-E001` (evidence rejected) or `RX-E004` (malformed or unknown version).
12//! Deep terms are handled by running on a thread with a large stack.
13
14mod cert;
15mod json;
16mod term;
17
18pub use cert::{check_certificate, check_counterexample, check_witness, CertInfo};
19
20/// A rejected or malformed piece of evidence.
21#[derive(Debug, Clone, PartialEq, Eq)]
22pub struct CheckError {
23    /// `RX-E001` (rejected) or `RX-E004` (malformed or unknown version).
24    pub code: &'static str,
25    /// What was wrong, including the failing pair where there is one.
26    pub message: String,
27}
28
29impl std::fmt::Display for CheckError {
30    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
31        write!(f, "{}: {}", self.code, self.message)
32    }
33}
34
35impl std::error::Error for CheckError {}
36
37pub(crate) fn rejected(msg: impl Into<String>) -> CheckError {
38    CheckError {
39        code: "RX-E001",
40        message: msg.into(),
41    }
42}
43pub(crate) fn malformed(msg: impl Into<String>) -> CheckError {
44    CheckError {
45        code: "RX-E004",
46        message: msg.into(),
47    }
48}
49
50/// Run `f` on a thread with a large stack: terms from counted repetition are
51/// thousands of levels deep and the checker is plainly recursive. A panic in
52/// the checker aborts the process: it must never be mistaken for "valid".
53#[cfg(target_arch = "wasm32")]
54pub(crate) fn on_big_stack<R: Send + 'static>(f: impl FnOnce() -> R + Send + 'static) -> R {
55    // No threads on WebAssembly: the module is linked with a large stack instead.
56    f()
57}
58
59#[cfg(not(target_arch = "wasm32"))]
60pub(crate) fn on_big_stack<R: Send + 'static>(f: impl FnOnce() -> R + Send + 'static) -> R {
61    match std::thread::Builder::new()
62        .stack_size(256 * 1024 * 1024)
63        .spawn(f)
64    {
65        Ok(h) => match h.join() {
66            Ok(r) => r,
67            Err(_) => std::process::abort(),
68        },
69        Err(_) => std::process::abort(),
70    }
71}
rexact_check/lib.rs

rexact_check/
lib.rs
