ruvector_verified/
pools.rs

1//! Thread-local resource pools for proof-checking.
2//!
3//! Modeled after `ruvector-mincut`'s BfsPool pattern (90%+ hit rate).
4
5use std::cell::RefCell;
6use std::collections::HashMap;
7
8thread_local! {
9    static PROOF_POOL: RefCell<ProofResourcePool> = RefCell::new(ProofResourcePool::new());
10}
11
12struct ProofResourcePool {
13    envs: Vec<crate::ProofEnvironment>,
14    hashmaps: Vec<HashMap<u64, u32>>,
15    acquires: u64,
16    hits: u64,
17}
18
19impl ProofResourcePool {
20    fn new() -> Self {
21        Self {
22            envs: Vec::new(),
23            hashmaps: Vec::new(),
24            acquires: 0,
25            hits: 0,
26        }
27    }
28}
29
30/// Pooled proof resources with auto-return on drop.
31pub struct PooledResources {
32    pub env: crate::ProofEnvironment,
33    pub scratch: HashMap<u64, u32>,
34}
35
36impl Drop for PooledResources {
37    fn drop(&mut self) {
38        let mut env = std::mem::take(&mut self.env);
39        env.reset();
40        let mut map = std::mem::take(&mut self.scratch);
41        map.clear();
42
43        PROOF_POOL.with(|pool| {
44            let mut p = pool.borrow_mut();
45            p.envs.push(env);
46            p.hashmaps.push(map);
47        });
48    }
49}
50
51/// Acquire pooled resources. Auto-returns to pool when dropped.
52pub fn acquire() -> PooledResources {
53    PROOF_POOL.with(|pool| {
54        let mut p = pool.borrow_mut();
55        p.acquires += 1;
56
57        let had_env = !p.envs.is_empty();
58        let had_map = !p.hashmaps.is_empty();
59
60        let env = p.envs.pop().unwrap_or_else(crate::ProofEnvironment::new);
61        let scratch = p.hashmaps.pop().unwrap_or_default();
62
63        if had_env || had_map {
64            p.hits += 1;
65        }
66
67        PooledResources { env, scratch }
68    })
69}
70
71/// Get pool statistics: (acquires, hits, hit_rate).
72pub fn pool_stats() -> (u64, u64, f64) {
73    PROOF_POOL.with(|pool| {
74        let p = pool.borrow();
75        let rate = if p.acquires == 0 {
76            0.0
77        } else {
78            p.hits as f64 / p.acquires as f64
79        };
80        (p.acquires, p.hits, rate)
81    })
82}
83
84#[cfg(test)]
85mod tests {
86    use super::*;
87
88    #[test]
89    fn test_acquire_returns() {
90        {
91            let res = acquire();
92            assert!(res.env.symbol_id("Nat").is_some());
93        }
94        // After drop, pool should have 1 entry
95        let (acquires, _, _) = pool_stats();
96        assert!(acquires >= 1);
97    }
98
99    #[test]
100    fn test_pool_reuse() {
101        {
102            let _r1 = acquire();
103        }
104        {
105            let _r2 = acquire();
106        }
107        let (acquires, hits, _) = pool_stats();
108        assert!(acquires >= 2);
109        assert!(hits >= 1, "second acquire should hit pool");
110    }
111
112    #[test]
113    fn test_pooled_env_is_reset() {
114        {
115            let mut res = acquire();
116            res.env.alloc_term();
117            res.env.alloc_term();
118        }
119        {
120            let res = acquire();
121            assert_eq!(res.env.terms_allocated(), 0, "pooled env should be reset");
122        }
123    }
124}
ruvector_verified/pools.rs

ruvector_verified/
pools.rs
