logicaffeine_verify/
strategy.rs

1//! Strategy Selection Engine
2//!
3//! Automatically selects the best verification algorithm based on property structure.
4
5use crate::ir::VerifyExpr;
6use crate::equivalence::Trace;
7use crate::kinduction::{self, KInductionResult, SignalDecl};
8
9/// Verification strategy.
10#[derive(Debug, Clone, PartialEq)]
11pub enum Strategy {
12    Bmc(u32),
13    KInduction(u32),
14    Ic3,
15    Interpolation(u32),
16    LivenessToSafety,
17    Portfolio { strategies: Vec<Strategy>, timeout_each_ms: u64 },
18}
19
20/// Unified verification result from auto-selection.
21#[derive(Debug)]
22pub enum VerificationResult {
23    Safe { strategy_used: Strategy },
24    Unsafe { trace: Trace, strategy_used: Strategy },
25    Unknown,
26}
27
28/// Select the best strategy based on property structure.
29pub fn select_strategy(property: &VerifyExpr, _signals: &[SignalDecl]) -> Strategy {
30    // Heuristic: analyze property structure
31    if contains_liveness_pattern(property) {
32        return Strategy::LivenessToSafety;
33    }
34
35    // For most safety properties, try IC3 first (most capable)
36    if is_small_property(property) {
37        Strategy::KInduction(10)
38    } else {
39        Strategy::Ic3
40    }
41}
42
43/// Verify a property using automatic strategy selection.
44pub fn verify_auto(
45    init: &VerifyExpr,
46    transition: &VerifyExpr,
47    property: &VerifyExpr,
48    signals: &[SignalDecl],
49) -> VerificationResult {
50    let strategy = select_strategy(property, signals);
51
52    match &strategy {
53        Strategy::KInduction(max_k) => {
54            let result = kinduction::k_induction(init, transition, property, signals, *max_k);
55            match result {
56                KInductionResult::Proven { .. } => VerificationResult::Safe {
57                    strategy_used: strategy,
58                },
59                KInductionResult::Counterexample { trace, .. } => VerificationResult::Unsafe {
60                    trace,
61                    strategy_used: strategy,
62                },
63                _ => {
64                    // Fall through to IC3
65                    try_ic3(init, transition, property)
66                }
67            }
68        }
69        Strategy::Ic3 => try_ic3(init, transition, property),
70        Strategy::LivenessToSafety => {
71            let result = crate::liveness::check_liveness(init, transition, &[], property, 10);
72            match result {
73                crate::liveness::LivenessResult::Live => VerificationResult::Safe {
74                    strategy_used: strategy,
75                },
76                crate::liveness::LivenessResult::NotLive { trace, .. } => VerificationResult::Unsafe {
77                    trace,
78                    strategy_used: strategy,
79                },
80                _ => VerificationResult::Unknown,
81            }
82        }
83        Strategy::Interpolation(bound) => {
84            let result = crate::interpolation::itp_model_check(init, transition, property, *bound);
85            match result {
86                crate::interpolation::InterpolationResult::Safe
87                | crate::interpolation::InterpolationResult::Fixpoint { .. } => {
88                    VerificationResult::Safe { strategy_used: strategy }
89                }
90                crate::interpolation::InterpolationResult::Unsafe { trace } => {
91                    VerificationResult::Unsafe { trace, strategy_used: strategy }
92                }
93                _ => VerificationResult::Unknown,
94            }
95        }
96        Strategy::Bmc(bound) => {
97            let result = kinduction::k_induction(init, transition, property, signals, *bound);
98            match result {
99                KInductionResult::Counterexample { trace, .. } => VerificationResult::Unsafe {
100                    trace,
101                    strategy_used: strategy,
102                },
103                KInductionResult::Proven { .. } => VerificationResult::Safe {
104                    strategy_used: strategy,
105                },
106                _ => VerificationResult::Unknown,
107            }
108        }
109        Strategy::Portfolio { strategies, .. } => {
110            // Try strategies in order, return first definitive result
111            for s in strategies {
112                let result = verify_with_strategy(init, transition, property, signals, s);
113                match &result {
114                    VerificationResult::Safe { .. } | VerificationResult::Unsafe { .. } => return result,
115                    VerificationResult::Unknown => continue,
116                }
117            }
118            VerificationResult::Unknown
119        }
120    }
121}
122
123fn try_ic3(init: &VerifyExpr, transition: &VerifyExpr, property: &VerifyExpr) -> VerificationResult {
124    let result = crate::ic3::ic3(init, transition, property, 20);
125    match result {
126        crate::ic3::Ic3Result::Safe { .. } => VerificationResult::Safe {
127            strategy_used: Strategy::Ic3,
128        },
129        crate::ic3::Ic3Result::Unsafe { trace } => VerificationResult::Unsafe {
130            trace,
131            strategy_used: Strategy::Ic3,
132        },
133        _ => VerificationResult::Unknown,
134    }
135}
136
137fn verify_with_strategy(
138    init: &VerifyExpr,
139    transition: &VerifyExpr,
140    property: &VerifyExpr,
141    signals: &[SignalDecl],
142    strategy: &Strategy,
143) -> VerificationResult {
144    match strategy {
145        Strategy::KInduction(k) => {
146            let result = kinduction::k_induction(init, transition, property, signals, *k);
147            match result {
148                KInductionResult::Proven { .. } => VerificationResult::Safe {
149                    strategy_used: strategy.clone(),
150                },
151                KInductionResult::Counterexample { trace, .. } => VerificationResult::Unsafe {
152                    trace,
153                    strategy_used: strategy.clone(),
154                },
155                _ => VerificationResult::Unknown,
156            }
157        }
158        Strategy::Ic3 => try_ic3(init, transition, property),
159        _ => VerificationResult::Unknown,
160    }
161}
162
163fn contains_liveness_pattern(_expr: &VerifyExpr) -> bool {
164    // Simple heuristic: check for patterns that suggest liveness
165    // G(F(p)) patterns would typically have nested temporal operators
166    // For now, we don't have explicit temporal operators in VerifyExpr,
167    // so this is a placeholder
168    false
169}
170
171fn is_small_property(expr: &VerifyExpr) -> bool {
172    expr_size(expr) < 20
173}
174
175fn expr_size(expr: &VerifyExpr) -> usize {
176    match expr {
177        VerifyExpr::Bool(_) | VerifyExpr::Int(_) | VerifyExpr::Var(_) => 1,
178        VerifyExpr::BitVecConst { .. } => 1,
179        VerifyExpr::Binary { left, right, .. } => 1 + expr_size(left) + expr_size(right),
180        VerifyExpr::Not(inner) => 1 + expr_size(inner),
181        VerifyExpr::Iff(l, r) => 1 + expr_size(l) + expr_size(r),
182        VerifyExpr::ForAll { body, .. } | VerifyExpr::Exists { body, .. } => 1 + expr_size(body),
183        VerifyExpr::Apply { args, .. } | VerifyExpr::ApplyInt { args, .. } => 1 + args.iter().map(expr_size).sum::<usize>(),
184        VerifyExpr::BitVecBinary { left, right, .. } => 1 + expr_size(left) + expr_size(right),
185        VerifyExpr::BitVecExtract { operand, .. } => 1 + expr_size(operand),
186        VerifyExpr::BitVecConcat(l, r) => 1 + expr_size(l) + expr_size(r),
187        VerifyExpr::Select { array, index } => 1 + expr_size(array) + expr_size(index),
188        VerifyExpr::Store { array, index, value } => 1 + expr_size(array) + expr_size(index) + expr_size(value),
189        VerifyExpr::AtState { state, expr } => 1 + expr_size(state) + expr_size(expr),
190        VerifyExpr::Transition { from, to } => 1 + expr_size(from) + expr_size(to),
191    }
192}
logicaffeine_verify/strategy.rs

logicaffeine_verify/
strategy.rs
