oxilean_kernel/def_eq_cache/
functions.rs

1//! Functions for the Definitional Equality Cache.
2//!
3//! Provides the core cache operations: construction, lookup, insertion,
4//! eviction, statistics, and a higher-order memoizing wrapper.
5
6use crate::proof_cert::hash_expr;
7use crate::Expr;
8
9use super::types::{CacheEviction, DefEqCache, DefEqCacheStats, DefEqEntry, DefEqKey};
10
11// ---------------------------------------------------------------------------
12// DefEqKey construction
13// ---------------------------------------------------------------------------
14
15impl DefEqKey {
16    /// Construct a canonical `DefEqKey` for the given expression pair.
17    ///
18    /// The two hashes are sorted so that `new(a, b) == new(b, a)`, enabling
19    /// symmetric reuse of cache entries regardless of argument order.
20    pub fn new(lhs: &Expr, rhs: &Expr) -> Self {
21        let h_lhs = hash_expr(lhs);
22        let h_rhs = hash_expr(rhs);
23        if h_lhs <= h_rhs {
24            DefEqKey {
25                lhs_hash: h_lhs,
26                rhs_hash: h_rhs,
27            }
28        } else {
29            DefEqKey {
30                lhs_hash: h_rhs,
31                rhs_hash: h_lhs,
32            }
33        }
34    }
35
36    /// Construct a `DefEqKey` directly from two hashes (already in canonical order).
37    pub fn from_hashes(a: u64, b: u64) -> Self {
38        if a <= b {
39            DefEqKey {
40                lhs_hash: a,
41                rhs_hash: b,
42            }
43        } else {
44            DefEqKey {
45                lhs_hash: b,
46                rhs_hash: a,
47            }
48        }
49    }
50}
51
52// ---------------------------------------------------------------------------
53// DefEqCache construction and core operations
54// ---------------------------------------------------------------------------
55
56impl DefEqCache {
57    /// Create a new empty cache with the given capacity and LRU eviction.
58    pub fn new(max_size: usize) -> Self {
59        DefEqCache {
60            hits: 0,
61            misses: 0,
62            entries: std::collections::HashMap::new(),
63            max_size,
64            eviction: CacheEviction::LRU,
65            clock: 0,
66            insertion_order: std::collections::HashMap::new(),
67            insert_clock: 0,
68        }
69    }
70
71    /// Create a new cache with an explicit eviction policy.
72    pub fn with_eviction(max_size: usize, eviction: CacheEviction) -> Self {
73        DefEqCache {
74            eviction,
75            ..DefEqCache::new(max_size)
76        }
77    }
78
79    /// Look up whether `(lhs, rhs)` is in the cache.
80    ///
81    /// Updates `hits`/`misses` and refreshes the LRU timestamp on a hit.
82    pub fn lookup(&mut self, lhs: &Expr, rhs: &Expr) -> Option<bool> {
83        let key = DefEqKey::new(lhs, rhs);
84        self.clock = self.clock.wrapping_add(1);
85        let now = self.clock;
86        if let Some(entry) = self.entries.get_mut(&key) {
87            entry.checked_count = entry.checked_count.saturating_add(1);
88            entry.last_access = now;
89            self.hits += 1;
90            Some(entry.result)
91        } else {
92            self.misses += 1;
93            None
94        }
95    }
96
97    /// Insert the result of a definitional equality check into the cache.
98    ///
99    /// If the cache is full, one entry is evicted according to the policy
100    /// before insertion.
101    pub fn insert(&mut self, lhs: &Expr, rhs: &Expr, result: bool) {
102        let key = DefEqKey::new(lhs, rhs);
103        // If entry already exists, update it in-place.
104        if let Some(entry) = self.entries.get_mut(&key) {
105            entry.result = result;
106            return;
107        }
108        // Evict if at capacity.
109        if self.entries.len() >= self.max_size && self.max_size > 0 {
110            self.evict_by_policy();
111        }
112        self.clock = self.clock.wrapping_add(1);
113        self.insert_clock = self.insert_clock.wrapping_add(1);
114        let now = self.clock;
115        let ins = self.insert_clock;
116        self.insertion_order.insert(key, ins);
117        self.entries.insert(
118            key,
119            DefEqEntry {
120                key,
121                result,
122                checked_count: 0,
123                last_access: now,
124            },
125        );
126    }
127
128    /// Evict one entry according to the configured eviction policy.
129    fn evict_by_policy(&mut self) {
130        match self.eviction {
131            CacheEviction::LRU => self.evict_lru(),
132            CacheEviction::LFU => self.evict_lfu(),
133            CacheEviction::FIFO => self.evict_fifo(),
134        }
135    }
136
137    /// Remove the least-recently-used entry.
138    pub fn evict_lru(&mut self) {
139        let victim = self
140            .entries
141            .iter()
142            .min_by_key(|(_, e)| e.last_access)
143            .map(|(k, _)| *k);
144        if let Some(k) = victim {
145            self.entries.remove(&k);
146            self.insertion_order.remove(&k);
147        }
148    }
149
150    /// Remove the least-frequently-used entry.
151    pub fn evict_lfu(&mut self) {
152        let victim = self
153            .entries
154            .iter()
155            .min_by_key(|(_, e)| e.checked_count)
156            .map(|(k, _)| *k);
157        if let Some(k) = victim {
158            self.entries.remove(&k);
159            self.insertion_order.remove(&k);
160        }
161    }
162
163    /// Remove the oldest-inserted entry (FIFO).
164    pub fn evict_fifo(&mut self) {
165        let victim = self
166            .insertion_order
167            .iter()
168            .min_by_key(|(_, &ord)| ord)
169            .map(|(k, _)| *k);
170        if let Some(k) = victim {
171            self.entries.remove(&k);
172            self.insertion_order.remove(&k);
173        }
174    }
175
176    /// Return a snapshot of current cache statistics.
177    pub fn stats(&self) -> DefEqCacheStats {
178        let total = self.hits + self.misses;
179        let hit_rate = if total == 0 {
180            0.0
181        } else {
182            self.hits as f64 / total as f64
183        };
184        DefEqCacheStats {
185            hits: self.hits,
186            misses: self.misses,
187            hit_rate,
188            size: self.entries.len(),
189        }
190    }
191
192    /// Clear all entries and reset statistics.
193    pub fn clear(&mut self) {
194        self.entries.clear();
195        self.insertion_order.clear();
196        self.hits = 0;
197        self.misses = 0;
198        self.clock = 0;
199        self.insert_clock = 0;
200    }
201
202    /// Return the number of currently cached entries.
203    pub fn size(&self) -> usize {
204        self.entries.len()
205    }
206
207    /// Return true if the cache has no entries.
208    pub fn is_empty(&self) -> bool {
209        self.entries.is_empty()
210    }
211}
212
213// ---------------------------------------------------------------------------
214// Memoizing wrapper
215// ---------------------------------------------------------------------------
216
217/// Memoizing wrapper that checks the cache before invoking the checker.
218///
219/// If `(lhs, rhs)` is already in `cache`, returns the cached result immediately.
220/// Otherwise, calls `check()`, stores the result in the cache, and returns it.
221///
222/// This is the primary way to integrate `DefEqCache` into a definitional
223/// equality checker without modifying the checker itself.
224///
225/// # Example
226///
227/// ```ignore
228/// let result = with_cache(&mut cache, &expr_a, &expr_b, || {
229///     expensive_def_eq_check(&expr_a, &expr_b)
230/// });
231/// ```
232pub fn with_cache<F>(cache: &mut DefEqCache, lhs: &Expr, rhs: &Expr, check: F) -> bool
233where
234    F: FnOnce() -> bool,
235{
236    if let Some(cached) = cache.lookup(lhs, rhs) {
237        return cached;
238    }
239    let result = check();
240    cache.insert(lhs, rhs, result);
241    result
242}
243
244// ---------------------------------------------------------------------------
245// Tests
246// ---------------------------------------------------------------------------
247
248#[cfg(test)]
249mod tests {
250    use super::*;
251    use crate::{Expr, Level, Name};
252
253    fn prop() -> Expr {
254        Expr::Sort(Level::Zero)
255    }
256
257    fn type0() -> Expr {
258        Expr::Sort(Level::succ(Level::Zero))
259    }
260
261    fn const_expr(name: &str) -> Expr {
262        Expr::Const(Name::from_str(name), vec![])
263    }
264
265    fn bvar(n: u32) -> Expr {
266        Expr::BVar(n)
267    }
268
269    // --- DefEqKey ---
270
271    #[test]
272    fn test_key_symmetric() {
273        let a = prop();
274        let b = type0();
275        let k1 = DefEqKey::new(&a, &b);
276        let k2 = DefEqKey::new(&b, &a);
277        assert_eq!(k1, k2, "DefEqKey must be symmetric");
278    }
279
280    #[test]
281    fn test_key_same_expr() {
282        let a = prop();
283        let k = DefEqKey::new(&a, &a);
284        assert_eq!(k.lhs_hash, k.rhs_hash);
285    }
286
287    #[test]
288    fn test_key_from_hashes_canonical() {
289        let k1 = DefEqKey::from_hashes(10, 20);
290        let k2 = DefEqKey::from_hashes(20, 10);
291        assert_eq!(k1, k2);
292        assert_eq!(k1.lhs_hash, 10);
293        assert_eq!(k1.rhs_hash, 20);
294    }
295
296    #[test]
297    fn test_key_distinct_exprs() {
298        let a = prop();
299        let b = type0();
300        let ka = DefEqKey::new(&a, &a);
301        let kb = DefEqKey::new(&b, &b);
302        let kab = DefEqKey::new(&a, &b);
303        // All three should be distinct (modulo hash collision, which is unlikely).
304        assert_ne!(ka, kb);
305        assert_ne!(ka, kab);
306    }
307
308    // --- DefEqCache construction ---
309
310    #[test]
311    fn test_new_cache_empty() {
312        let cache = DefEqCache::new(128);
313        assert!(cache.is_empty());
314        assert_eq!(cache.hits, 0);
315        assert_eq!(cache.misses, 0);
316    }
317
318    #[test]
319    fn test_new_cache_zero_capacity() {
320        // A zero-capacity cache should not panic.
321        let cache = DefEqCache::new(0);
322        assert_eq!(cache.max_size, 0);
323    }
324
325    // --- lookup / insert ---
326
327    #[test]
328    fn test_miss_on_empty() {
329        let mut cache = DefEqCache::new(64);
330        let result = cache.lookup(&prop(), &type0());
331        assert!(result.is_none());
332        assert_eq!(cache.misses, 1);
333        assert_eq!(cache.hits, 0);
334    }
335
336    #[test]
337    fn test_hit_after_insert() {
338        let mut cache = DefEqCache::new(64);
339        let a = prop();
340        let b = type0();
341        cache.insert(&a, &b, true);
342        let result = cache.lookup(&a, &b);
343        assert_eq!(result, Some(true));
344        assert_eq!(cache.hits, 1);
345    }
346
347    #[test]
348    fn test_symmetric_hit() {
349        let mut cache = DefEqCache::new(64);
350        let a = prop();
351        let b = type0();
352        cache.insert(&a, &b, false);
353        // Lookup with reversed arguments should also hit.
354        let result = cache.lookup(&b, &a);
355        assert_eq!(result, Some(false));
356    }
357
358    #[test]
359    fn test_insert_same_entry_twice() {
360        let mut cache = DefEqCache::new(64);
361        let a = prop();
362        let b = type0();
363        cache.insert(&a, &b, true);
364        cache.insert(&a, &b, false); // overwrite
365        let result = cache.lookup(&a, &b);
366        assert_eq!(result, Some(false));
367    }
368
369    #[test]
370    fn test_size_tracking() {
371        let mut cache = DefEqCache::new(64);
372        assert_eq!(cache.size(), 0);
373        cache.insert(&prop(), &type0(), true);
374        assert_eq!(cache.size(), 1);
375        cache.insert(&bvar(0), &bvar(1), false);
376        assert_eq!(cache.size(), 2);
377    }
378
379    // --- clear ---
380
381    #[test]
382    fn test_clear_resets_everything() {
383        let mut cache = DefEqCache::new(64);
384        cache.insert(&prop(), &type0(), true);
385        let _ = cache.lookup(&prop(), &type0());
386        cache.clear();
387        assert!(cache.is_empty());
388        assert_eq!(cache.hits, 0);
389        assert_eq!(cache.misses, 0);
390    }
391
392    // --- stats ---
393
394    #[test]
395    fn test_stats_zero_queries() {
396        let cache = DefEqCache::new(64);
397        let s = cache.stats();
398        assert_eq!(s.hits, 0);
399        assert_eq!(s.misses, 0);
400        assert_eq!(s.hit_rate, 0.0);
401        assert_eq!(s.size, 0);
402    }
403
404    #[test]
405    fn test_stats_hit_rate() {
406        let mut cache = DefEqCache::new(64);
407        let a = prop();
408        let b = type0();
409        cache.insert(&a, &b, true);
410        let _ = cache.lookup(&a, &b); // hit
411        let _ = cache.lookup(&bvar(0), &bvar(1)); // miss
412        let s = cache.stats();
413        assert_eq!(s.hits, 1);
414        assert_eq!(s.misses, 1);
415        assert!((s.hit_rate - 0.5).abs() < 1e-9);
416    }
417
418    // --- eviction ---
419
420    #[test]
421    fn test_lru_eviction_capacity_respected() {
422        let mut cache = DefEqCache::new(2);
423        cache.insert(&prop(), &type0(), true);
424        cache.insert(&bvar(0), &bvar(1), false);
425        // Access first entry to make it recently used.
426        let _ = cache.lookup(&prop(), &type0());
427        // Insert a third entry — should evict the LRU (bvar(0)/bvar(1)).
428        cache.insert(&const_expr("Nat"), &const_expr("Int"), true);
429        assert_eq!(cache.size(), 2, "cache should not exceed max_size");
430    }
431
432    #[test]
433    fn test_lfu_eviction() {
434        let mut cache = DefEqCache::with_eviction(2, CacheEviction::LFU);
435        cache.insert(&prop(), &type0(), true);
436        cache.insert(&bvar(0), &bvar(1), false);
437        // Access first entry many times.
438        for _ in 0..5 {
439            let _ = cache.lookup(&prop(), &type0());
440        }
441        // Insert third entry — should evict the less-frequently-used bvar pair.
442        cache.insert(&const_expr("Nat"), &const_expr("Int"), true);
443        assert_eq!(cache.size(), 2);
444    }
445
446    #[test]
447    fn test_fifo_eviction() {
448        let mut cache = DefEqCache::with_eviction(2, CacheEviction::FIFO);
449        cache.insert(&prop(), &type0(), true); // inserted first
450        cache.insert(&bvar(0), &bvar(1), false); // inserted second
451                                                 // Access first entry to make it recently used (should NOT affect FIFO).
452        let _ = cache.lookup(&prop(), &type0());
453        // Third insertion should evict the first-inserted (prop/type0).
454        cache.insert(&const_expr("Nat"), &const_expr("Int"), true);
455        assert_eq!(cache.size(), 2);
456        // After FIFO eviction of the first entry, its lookup should miss.
457        let result = cache.lookup(&prop(), &type0());
458        assert!(result.is_none(), "FIFO should have evicted the first entry");
459    }
460
461    #[test]
462    fn test_evict_lru_explicit() {
463        let mut cache = DefEqCache::new(4);
464        cache.insert(&prop(), &type0(), true);
465        cache.insert(&bvar(0), &bvar(1), false);
466        // Access second entry to make it recently used.
467        let _ = cache.lookup(&bvar(0), &bvar(1));
468        cache.evict_lru();
469        assert_eq!(cache.size(), 1);
470        // The LRU (prop/type0, never accessed after insert) should be gone.
471        assert!(cache.lookup(&prop(), &type0()).is_none());
472    }
473
474    // --- with_cache ---
475
476    #[test]
477    fn test_with_cache_miss_calls_check() {
478        let mut cache = DefEqCache::new(64);
479        let a = prop();
480        let b = type0();
481        let mut called = false;
482        let result = with_cache(&mut cache, &a, &b, || {
483            called = true;
484            true
485        });
486        assert!(called, "checker should have been invoked on a miss");
487        assert!(result);
488    }
489
490    #[test]
491    fn test_with_cache_hit_skips_check() {
492        let mut cache = DefEqCache::new(64);
493        let a = prop();
494        let b = type0();
495        cache.insert(&a, &b, false);
496        let mut called = false;
497        let result = with_cache(&mut cache, &a, &b, || {
498            called = true;
499            true // would return a different value if called
500        });
501        assert!(!called, "checker must not be invoked on a cache hit");
502        assert!(!result, "cached value (false) must be returned");
503    }
504
505    #[test]
506    fn test_with_cache_stores_result() {
507        let mut cache = DefEqCache::new(64);
508        let a = prop();
509        let b = type0();
510        let _ = with_cache(&mut cache, &a, &b, || true);
511        // Second call should be a cache hit.
512        let result = with_cache(&mut cache, &a, &b, || false);
513        assert!(result, "second call should return the cached true");
514        assert_eq!(cache.hits, 1);
515    }
516
517    #[test]
518    fn test_with_cache_symmetric_hit() {
519        let mut cache = DefEqCache::new(64);
520        let a = prop();
521        let b = type0();
522        let _ = with_cache(&mut cache, &a, &b, || true);
523        // Reverse argument order.
524        let mut called = false;
525        let result = with_cache(&mut cache, &b, &a, || {
526            called = true;
527            false
528        });
529        assert!(!called);
530        assert!(result);
531    }
532
533    // --- CacheEviction display ---
534
535    #[test]
536    fn test_eviction_display() {
537        assert_eq!(format!("{}", CacheEviction::LRU), "LRU");
538        assert_eq!(format!("{}", CacheEviction::LFU), "LFU");
539        assert_eq!(format!("{}", CacheEviction::FIFO), "FIFO");
540    }
541
542    // --- DefEqCacheStats display ---
543
544    #[test]
545    fn test_stats_display() {
546        let cache = DefEqCache::new(64);
547        let s = cache.stats();
548        let text = format!("{}", s);
549        assert!(text.contains("DefEqCacheStats"));
550    }
551}
oxilean_kernel/def_eq_cache/functions.rs

oxilean_kernel/def_eq_cache/
functions.rs
