Struct ProofVerifier 

pub struct ProofVerifier {
    pub rules: HashMap<String, RuleSpec>,
    pub memo: HashMap<u64, bool>,
    pub in_progress: HashSet<u64>,
}

Verifies serialized proof trees by re-checking each node’s rule application.

Maintains a memoization cache so that shared sub-proofs (DAG structure) are not re-verified on subsequent traversals. A fresh ProofVerifier starts with an empty rule registry and an empty memo cache.

Fields

rules: HashMap<String, RuleSpec>

Registered inference rules, keyed by rule ID.

memo: HashMap<u64, bool>

Memoized verification results: node_id → verified.

in_progress: HashSet<u64>

Nodes currently on the DFS stack — used for cycle detection.

Implementations

impl ProofVerifier

pub fn new() -> Self

Create a new, empty ProofVerifier.

pub fn register_rule(&mut self, spec: RuleSpec)

Register an inference rule. Replaces any existing rule with the same ID.

pub fn verify(&mut self, nodes: &[ProofNode]) -> VerificationResult

Verify a slice of ProofNodes.

Identifies the root as the node whose ID does not appear as any other node’s premise. If there is no unique root, the first node is used.

DFS from the root re-checks every rule application. Results are memoized so shared sub-proofs are counted as cache hits.

pub fn clear_memo(&mut self)

Reset memo cache and in-progress set.

pub fn stats(&self) -> (usize, usize)

Returns (rules_registered, memo_entries).

Trait Implementations

impl Default for ProofVerifier

fn default() -> Self

Returns the “default value” for a type.