logicaffeine_verify/
incremental.rs

1//! Incremental Verification
2//!
3//! Cache verification results, track dependencies, invalidate only what changed.
4
5use crate::ir::VerifyExpr;
6use std::collections::HashMap;
7use std::hash::{Hash, Hasher};
8
9/// A hash of a property for caching.
10pub type PropertyHash = u64;
11
12/// Cached verification result.
13#[derive(Debug, Clone)]
14pub struct CachedResult {
15    pub is_safe: bool,
16    pub dependencies: Vec<String>,
17    pub timestamp: u64,
18}
19
20/// Verification cache.
21#[derive(Debug, Clone, Default)]
22pub struct VerificationCache {
23    pub entries: HashMap<PropertyHash, CachedResult>,
24}
25
26/// A change event.
27#[derive(Debug, Clone)]
28pub struct ChangeEvent {
29    pub changed_item: String,
30}
31
32impl VerificationCache {
33    pub fn new() -> Self {
34        Self { entries: HashMap::new() }
35    }
36
37    /// Store a result in the cache.
38    pub fn store(&mut self, hash: PropertyHash, result: CachedResult) {
39        self.entries.insert(hash, result);
40    }
41
42    /// Look up a cached result.
43    pub fn lookup(&self, hash: PropertyHash) -> Option<&CachedResult> {
44        self.entries.get(&hash)
45    }
46
47    /// Invalidate entries affected by changes.
48    pub fn invalidate(&mut self, changes: &[ChangeEvent]) {
49        let changed_items: Vec<&str> = changes.iter().map(|c| c.changed_item.as_str()).collect();
50        self.entries.retain(|_, result| {
51            !result.dependencies.iter().any(|dep| changed_items.contains(&dep.as_str()))
52        });
53    }
54
55    /// Number of cached entries.
56    pub fn len(&self) -> usize {
57        self.entries.len()
58    }
59
60    pub fn is_empty(&self) -> bool {
61        self.entries.is_empty()
62    }
63}
64
65/// Compute a hash for a property expression.
66pub fn hash_property(expr: &VerifyExpr) -> PropertyHash {
67    let mut hasher = std::collections::hash_map::DefaultHasher::new();
68    format!("{:?}", expr).hash(&mut hasher);
69    hasher.finish()
70}
71
72/// Verify properties incrementally.
73pub fn verify_incremental(
74    properties: &[(VerifyExpr, Vec<String>)],
75    changes: &[ChangeEvent],
76    cache: &mut VerificationCache,
77) -> Vec<(PropertyHash, bool)> {
78    // Invalidate cache for changed items
79    cache.invalidate(changes);
80
81    let mut results = Vec::new();
82
83    for (prop, deps) in properties {
84        let hash = hash_property(prop);
85
86        if let Some(cached) = cache.lookup(hash) {
87            // Cache hit
88            results.push((hash, cached.is_safe));
89        } else {
90            // Cache miss — need to verify
91            // Use k-induction as a simple verifier
92            // For now, just mark as safe if the property is a tautology
93            let is_safe = matches!(prop, VerifyExpr::Bool(true));
94
95            cache.store(hash, CachedResult {
96                is_safe,
97                dependencies: deps.clone(),
98                timestamp: 0,
99            });
100
101            results.push((hash, is_safe));
102        }
103    }
104
105    results
106}
logicaffeine_verify/incremental.rs

logicaffeine_verify/
incremental.rs
