ruvector_verified/
lib.rs

1//! Formal verification layer for RuVector using lean-agentic dependent types.
2//!
3//! This crate provides proof-carrying vector operations, verified pipeline
4//! composition, and formal attestation for RuVector's safety-critical paths.
5//!
6//! # Feature Flags
7//!
8//! - `hnsw-proofs`: Enable verified HNSW insert/query operations
9//! - `rvf-proofs`: Enable RVF witness chain integration
10//! - `coherence-proofs`: Enable coherence verification
11//! - `serde`: Enable serialization of proof attestations
12//! - `fast-arena`: SolverArena-style bump allocator
13//! - `simd-hash`: AVX2/NEON accelerated hash-consing
14//! - `gated-proofs`: Coherence-gated proof depth routing
15//! - `ultra`: All optimizations (fast-arena + simd-hash + gated-proofs)
16//! - `all-proofs`: All proof integrations (hnsw + rvf + coherence)
17
18pub mod error;
19pub mod invariants;
20pub mod vector_types;
21pub mod proof_store;
22pub mod pipeline;
23
24#[cfg(feature = "fast-arena")]
25pub mod fast_arena;
26pub mod pools;
27pub mod cache;
28#[cfg(feature = "gated-proofs")]
29pub mod gated;
30
31// Re-exports
32pub use error::{VerificationError, Result};
33pub use vector_types::{mk_vector_type, mk_nat_literal, prove_dim_eq};
34pub use proof_store::ProofAttestation;
35pub use pipeline::VerifiedStage;
36pub use invariants::BuiltinDecl;
37
38/// The proof environment bundles verification state.
39///
40/// One instance per thread (not `Sync` due to interior state).
41/// Create with `ProofEnvironment::new()` which pre-loads RuVector type
42/// declarations.
43///
44/// # Example
45///
46/// ```rust,ignore
47/// use ruvector_verified::ProofEnvironment;
48///
49/// let mut env = ProofEnvironment::new();
50/// let proof = env.prove_dim_eq(128, 128).unwrap();
51/// ```
52pub struct ProofEnvironment {
53    /// Registered built-in symbol names.
54    pub symbols: Vec<String>,
55    /// Proof term counter (monotonically increasing).
56    term_counter: u32,
57    /// Cache of recently verified proofs: (input_hash, proof_id).
58    proof_cache: std::collections::HashMap<u64, u32>,
59    /// Statistics.
60    pub stats: ProofStats,
61}
62
63/// Verification statistics.
64#[derive(Debug, Clone, Default)]
65pub struct ProofStats {
66    /// Total proofs constructed.
67    pub proofs_constructed: u64,
68    /// Total proofs verified.
69    pub proofs_verified: u64,
70    /// Cache hits (proof reused).
71    pub cache_hits: u64,
72    /// Cache misses (new proof constructed).
73    pub cache_misses: u64,
74    /// Total reduction steps consumed.
75    pub total_reductions: u64,
76}
77
78impl ProofEnvironment {
79    /// Create a new proof environment pre-loaded with RuVector type declarations.
80    pub fn new() -> Self {
81        let mut symbols = Vec::with_capacity(32);
82        invariants::register_builtin_symbols(&mut symbols);
83
84        Self {
85            symbols,
86            term_counter: 0,
87            proof_cache: std::collections::HashMap::with_capacity(256),
88            stats: ProofStats::default(),
89        }
90    }
91
92    /// Allocate a new proof term ID.
93    pub fn alloc_term(&mut self) -> u32 {
94        let id = self.term_counter;
95        self.term_counter = self.term_counter.checked_add(1)
96            .ok_or_else(|| VerificationError::ArenaExhausted { allocated: id })
97            .expect("arena overflow");
98        self.stats.proofs_constructed += 1;
99        id
100    }
101
102    /// Look up a symbol index by name.
103    pub fn symbol_id(&self, name: &str) -> Option<usize> {
104        self.symbols.iter().position(|s| s == name)
105    }
106
107    /// Require a symbol index, or return DeclarationNotFound.
108    pub fn require_symbol(&self, name: &str) -> Result<usize> {
109        self.symbol_id(name).ok_or_else(|| {
110            VerificationError::DeclarationNotFound { name: name.to_string() }
111        })
112    }
113
114    /// Check the proof cache for a previously verified proof.
115    pub fn cache_lookup(&mut self, key: u64) -> Option<u32> {
116        if let Some(&id) = self.proof_cache.get(&key) {
117            self.stats.cache_hits += 1;
118            Some(id)
119        } else {
120            self.stats.cache_misses += 1;
121            None
122        }
123    }
124
125    /// Insert a verified proof into the cache.
126    pub fn cache_insert(&mut self, key: u64, proof_id: u32) {
127        self.proof_cache.insert(key, proof_id);
128    }
129
130    /// Get verification statistics.
131    pub fn stats(&self) -> &ProofStats {
132        &self.stats
133    }
134
135    /// Number of terms allocated.
136    pub fn terms_allocated(&self) -> u32 {
137        self.term_counter
138    }
139
140    /// Reset the environment (clear cache, reset counters).
141    /// Useful between independent proof obligations.
142    pub fn reset(&mut self) {
143        self.term_counter = 0;
144        self.proof_cache.clear();
145        self.stats = ProofStats::default();
146        // Re-register builtins
147        self.symbols.clear();
148        invariants::register_builtin_symbols(&mut self.symbols);
149    }
150}
151
152impl Default for ProofEnvironment {
153    fn default() -> Self {
154        Self::new()
155    }
156}
157
158/// A vector operation with a machine-checked type proof.
159#[derive(Debug, Clone, Copy)]
160pub struct VerifiedOp<T> {
161    /// The operation result.
162    pub value: T,
163    /// Proof term ID in the environment.
164    pub proof_id: u32,
165}
166
167#[cfg(test)]
168mod tests {
169    use super::*;
170
171    #[test]
172    fn proof_env_new_has_builtins() {
173        let env = ProofEnvironment::new();
174        assert!(env.symbol_id("Nat").is_some());
175        assert!(env.symbol_id("RuVec").is_some());
176        assert!(env.symbol_id("Eq").is_some());
177        assert!(env.symbol_id("Eq.refl").is_some());
178        assert!(env.symbol_id("HnswIndex").is_some());
179    }
180
181    #[test]
182    fn proof_env_alloc_term() {
183        let mut env = ProofEnvironment::new();
184        assert_eq!(env.alloc_term(), 0);
185        assert_eq!(env.alloc_term(), 1);
186        assert_eq!(env.alloc_term(), 2);
187        assert_eq!(env.terms_allocated(), 3);
188    }
189
190    #[test]
191    fn proof_env_cache() {
192        let mut env = ProofEnvironment::new();
193        assert!(env.cache_lookup(42).is_none());
194        env.cache_insert(42, 7);
195        assert_eq!(env.cache_lookup(42), Some(7));
196        assert_eq!(env.stats().cache_hits, 1);
197        assert_eq!(env.stats().cache_misses, 1);
198    }
199
200    #[test]
201    fn proof_env_reset() {
202        let mut env = ProofEnvironment::new();
203        env.alloc_term();
204        env.cache_insert(1, 2);
205        env.reset();
206        assert_eq!(env.terms_allocated(), 0);
207        assert!(env.cache_lookup(1).is_none());
208        // Builtins restored after reset
209        assert!(env.symbol_id("Nat").is_some());
210    }
211
212    #[test]
213    fn proof_env_require_symbol() {
214        let env = ProofEnvironment::new();
215        assert!(env.require_symbol("Nat").is_ok());
216        assert!(env.require_symbol("NonExistent").is_err());
217    }
218
219    #[test]
220    fn verified_op_copy() {
221        let op = VerifiedOp { value: 42u32, proof_id: 1 };
222        let op2 = op; // Copy
223        assert_eq!(op.value, op2.value);
224    }
225}
ruvector_verified/lib.rs

ruvector_verified/
lib.rs
