Struct ProofEnvironment 

pub struct ProofEnvironment {
    pub symbols: Vec<String>,
    pub stats: ProofStats,
    /* private fields */
}

The proof environment bundles verification state.

One instance per thread (not Sync due to interior state). Create with ProofEnvironment::new() which pre-loads RuVector type declarations.

Example

use ruvector_verified::ProofEnvironment;

let mut env = ProofEnvironment::new();
let proof = env.prove_dim_eq(128, 128).unwrap();

Fields

symbols: Vec<String>

Registered built-in symbol names.

stats: ProofStats

Statistics.

Implementations

impl ProofEnvironment

pub fn new() -> Self

Create a new proof environment pre-loaded with RuVector type declarations.

pub fn alloc_term(&mut self) -> u32

Allocate a new proof term ID.

pub fn symbol_id(&self, name: &str) -> Option<usize>

Look up a symbol index by name.

pub fn require_symbol(&self, name: &str) -> Result<usize>

Require a symbol index, or return DeclarationNotFound.

pub fn cache_lookup(&mut self, key: u64) -> Option<u32>

Check the proof cache for a previously verified proof.

pub fn cache_insert(&mut self, key: u64, proof_id: u32)

Insert a verified proof into the cache.

pub fn stats(&self) -> &ProofStats

Get verification statistics.

pub fn terms_allocated(&self) -> u32

Number of terms allocated.

pub fn reset(&mut self)

Reset the environment (clear cache, reset counters). Useful between independent proof obligations.

Trait Implementations

impl Default for ProofEnvironment

fn default() -> Self

Returns the “default value” for a type.