diff --git a/specl/Cargo.lock b/specl/Cargo.lock index a0e6c8a..82627cb 100644 --- a/specl/Cargo.lock +++ b/specl/Cargo.lock @@ -2301,10 +2301,12 @@ version = "0.1.0" dependencies = [ "specl-eval", "specl-ir", + "specl-syntax", "specl-types", "thiserror 1.0.69", "tracing", "z3", + "z3-sys", ] [[package]] diff --git a/specl/crates/specl-cli/src/main.rs b/specl/crates/specl-cli/src/main.rs index 0d4a8ce..ace9fdb 100644 --- a/specl/crates/specl-cli/src/main.rs +++ b/specl/crates/specl-cli/src/main.rs @@ -164,6 +164,18 @@ enum Commands { #[arg(long)] inductive: bool, + /// Use k-induction with given strengthening depth (Z3-backed) + #[arg(long, value_name = "K")] + k_induction: Option, + + /// Use IC3/CHC verification via Z3's Spacer engine (unbounded, Z3-backed) + #[arg(long)] + ic3: bool, + + /// Smart mode: automatically try induction, k-induction, IC3, then BMC (Z3-backed) + #[arg(long)] + smart: bool, + /// Show verbose output #[arg(short, long)] verbose: bool, @@ -264,10 +276,13 @@ fn main() { symbolic, depth, inductive, + k_induction, + ic3, + smart, verbose, } => { - if symbolic || inductive { - cmd_check_symbolic(&file, &constant, depth, inductive) + if symbolic || inductive || k_induction.is_some() || ic3 || smart { + cmd_check_symbolic(&file, &constant, depth, inductive, k_induction, ic3, smart) } else { cmd_check( &file, @@ -487,6 +502,9 @@ fn cmd_check_symbolic( constants: &[String], depth: usize, inductive: bool, + k_induction: Option, + ic3: bool, + smart: bool, ) -> CliResult<()> { let filename = file.display().to_string(); let source = Arc::new(fs::read_to_string(file).map_err(|e| CliError::IoError { @@ -509,7 +527,13 @@ fn cmd_check_symbolic( let consts = parse_constants(constants, &spec)?; let config = SymbolicConfig { - mode: if inductive { + mode: if smart { + SymbolicMode::Smart + } else if ic3 { + SymbolicMode::Ic3 + } else if let Some(k) = k_induction { + SymbolicMode::KInduction(k) + } else if inductive { SymbolicMode::Inductive } else { SymbolicMode::Bmc @@ -517,7 +541,13 @@ fn cmd_check_symbolic( depth, }; - let mode_str = if inductive { + let mode_str = if smart { + "smart" + } else if ic3 { + "IC3" + } else if k_induction.is_some() { + "k-induction" + } else if inductive { "inductive" } else { "symbolic BMC" @@ -537,7 +567,9 @@ fn cmd_check_symbolic( println!(); println!("Result: OK"); println!(" Method: {}", method); - if !inductive { + if let Some(k) = k_induction { + println!(" K: {}", k); + } else if !inductive && !ic3 { println!(" Depth: {}", depth); } println!(" Time: {:.2}s", elapsed.as_secs_f64()); diff --git a/specl/crates/specl-symbolic/Cargo.toml b/specl/crates/specl-symbolic/Cargo.toml index 5d30b4f..3f4c735 100644 --- a/specl/crates/specl-symbolic/Cargo.toml +++ b/specl/crates/specl-symbolic/Cargo.toml @@ -11,6 +11,8 @@ description = "Symbolic model checking backend for Specl using Z3" specl-ir.workspace = true specl-types.workspace = true specl-eval.workspace = true +specl-syntax.workspace = true z3 = { version = "0.19", features = ["bundled"] } +z3-sys = "0.10.4" thiserror.workspace = true tracing.workspace = true diff --git a/specl/crates/specl-symbolic/src/bmc.rs b/specl/crates/specl-symbolic/src/bmc.rs index 78717f1..0533599 100644 --- a/specl/crates/specl-symbolic/src/bmc.rs +++ b/specl/crates/specl-symbolic/src/bmc.rs @@ -18,7 +18,7 @@ pub fn check_bmc( ) -> SymbolicResult { info!(depth = max_depth, "starting symbolic BMC"); - let layout = VarLayout::from_spec(spec)?; + let layout = VarLayout::from_spec(spec, consts)?; let solver = Solver::new(); // Create Z3 variables for steps 0..=max_depth diff --git a/specl/crates/specl-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index 3f2c2c9..c8636ca 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -47,10 +47,10 @@ impl<'a> EncoderCtx<'a> { CompiledExpr::Bool(b) => Ok(Dynamic::from_ast(&Bool::from_bool(*b))), CompiledExpr::Int(n) => Ok(Dynamic::from_ast(&Int::from_i64(*n))), CompiledExpr::String(s) => { - let hash = s - .bytes() - .fold(0i64, |acc, b| acc.wrapping_mul(31).wrapping_add(b as i64)); - Ok(Dynamic::from_ast(&Int::from_i64(hash))) + let id = self.layout.string_id(s).ok_or_else(|| { + SymbolicError::Encoding(format!("string literal not in table: {:?}", s)) + })?; + Ok(Dynamic::from_ast(&Int::from_i64(id))) } // === Variables === @@ -130,13 +130,13 @@ impl<'a> EncoderCtx<'a> { "DictLit should be handled at the init/effect level".into(), )), - // === Set operations === - CompiledExpr::SetLit(_) => Err(SymbolicError::Unsupported( - "set literal as expression (only supported in membership checks)".into(), - )), - CompiledExpr::SetComprehension { .. } => Err(SymbolicError::Unsupported( - "set comprehension as expression (only supported in len() and membership)".into(), - )), + // === Set operations (handled as expressions for equality/assignment) === + CompiledExpr::SetLit(_) | CompiledExpr::SetComprehension { .. } => { + Err(SymbolicError::Encoding( + "set expression used in non-set context (use in equality, membership, or len)" + .into(), + )) + } // === Len === CompiledExpr::Len(inner) => self.encode_len(inner), @@ -288,16 +288,44 @@ impl<'a> EncoderCtx<'a> { BinOp::In => self.encode_set_membership(left, right, false), BinOp::NotIn => self.encode_set_membership(left, right, true), - // Set operations (not yet implemented) - BinOp::Union | BinOp::Intersect | BinOp::Diff | BinOp::SubsetOf => Err( - SymbolicError::Unsupported(format!("set operation {:?}", op)), - ), + // Set operations on ExplodedSet + BinOp::Union | BinOp::Intersect | BinOp::Diff => { + // These produce a set — cannot be used as a scalar expression. + // They are handled at the effect/equality level via encode_as_set. + Err(SymbolicError::Encoding(format!( + "set operation {:?} used in scalar context (handled in effects/equality)", + op + ))) + } + BinOp::SubsetOf => { + // subset_of returns a Bool: for all elements, left[i] implies right[i] + let (lo, hi) = self.infer_set_bounds(left, right)?; + let l_set = self.encode_as_set(left, lo, hi)?; + let r_set = self.encode_as_set(right, lo, hi)?; + let mut conjuncts = Vec::new(); + for (lb, rb) in l_set.iter().zip(r_set.iter()) { + conjuncts.push(lb.implies(rb)); + } + Ok(Dynamic::from_ast(&Bool::and(&conjuncts))) + } BinOp::Concat => Err(SymbolicError::Unsupported("sequence concat".into())), } } fn encode_eq(&mut self, left: &CompiledExpr, right: &CompiledExpr) -> SymbolicResult { + // Check if either side is a set expression — use per-element equality + if self.is_set_expr(left) || self.is_set_expr(right) { + let (lo, hi) = self.infer_set_bounds(left, right)?; + let l_set = self.encode_as_set(left, lo, hi)?; + let r_set = self.encode_as_set(right, lo, hi)?; + let mut conjuncts = Vec::new(); + for (lb, rb) in l_set.iter().zip(r_set.iter()) { + conjuncts.push(lb.eq(rb)); + } + return Ok(Dynamic::from_ast(&Bool::and(&conjuncts))); + } + let l = self.encode(left)?; let r = self.encode(right)?; if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) { @@ -455,9 +483,22 @@ impl<'a> EncoderCtx<'a> { )) } } - _ => Err(SymbolicError::Unsupported( - "len() on complex expression".into(), - )), + _ => { + // Try encoding as a set expression + if self.is_set_expr(inner) { + if let Some((lo, hi)) = self.try_set_bounds(inner) { + let flags = self.encode_as_set(inner, lo, hi)?; + let one = Int::from_i64(1); + let zero = Int::from_i64(0); + let terms: Vec = + flags.iter().map(|b| b.ite(&one, &zero)).collect(); + return Ok(Dynamic::from_ast(&Int::add(&terms))); + } + } + Err(SymbolicError::Unsupported( + "len() on complex expression".into(), + )) + } } } } @@ -546,10 +587,60 @@ impl<'a> EncoderCtx<'a> { let final_val = if negate { result.not() } else { result }; Ok(Dynamic::from_ast(&final_val)) } - _ => Err(SymbolicError::Unsupported(format!( - "'in' operator with set expression: {:?}", - std::mem::discriminant(set) - ))), + CompiledExpr::SetLit(elements) => { + let elem_z3 = self.encode(elem)?; + let mut disjuncts = Vec::new(); + for set_elem in elements { + let set_elem_z3 = self.encode(set_elem)?; + if let (Some(ei), Some(si)) = (elem_z3.as_int(), set_elem_z3.as_int()) { + disjuncts.push(ei.eq(&si)); + } else if let (Some(eb), Some(sb)) = (elem_z3.as_bool(), set_elem_z3.as_bool()) + { + disjuncts.push(eb.eq(&sb)); + } + } + let result = if disjuncts.is_empty() { + Bool::from_bool(false) + } else { + Bool::or(&disjuncts) + }; + let final_val = if negate { result.not() } else { result }; + Ok(Dynamic::from_ast(&final_val)) + } + _ => { + // Try as a set expression with known bounds (union, intersect, etc.) + if self.is_set_expr(set) { + if let Some((lo, hi)) = self.try_set_bounds(set) { + let flags = self.encode_as_set(set, lo, hi)?; + if let Some(concrete_elem) = self.try_concrete_int(elem) { + let offset = (concrete_elem - lo) as usize; + let result = if offset < flags.len() { + flags[offset].clone() + } else { + Bool::from_bool(false) + }; + let final_val = if negate { result.not() } else { result }; + return Ok(Dynamic::from_ast(&final_val)); + } else { + let elem_z3 = self.encode_int(elem)?; + let z3_vars: Vec = + flags.iter().map(|b| Dynamic::from_ast(b)).collect(); + let result = self.build_ite_chain(&elem_z3, &z3_vars, lo)?; + let result_bool = result.as_bool().unwrap(); + let final_val = if negate { + result_bool.not() + } else { + result_bool + }; + return Ok(Dynamic::from_ast(&final_val)); + } + } + } + Err(SymbolicError::Unsupported(format!( + "'in' operator with set expression: {:?}", + std::mem::discriminant(set) + ))) + } } } @@ -571,6 +662,162 @@ impl<'a> EncoderCtx<'a> { Ok(Dynamic::from_ast(&Bool::and(&eqs))) } + // === Set helpers === + + /// Check if an expression represents a set (for equality routing). + fn is_set_expr(&self, expr: &CompiledExpr) -> bool { + match expr { + CompiledExpr::SetLit(_) | CompiledExpr::SetComprehension { .. } => true, + CompiledExpr::Binary { op, .. } => { + matches!(op, BinOp::Union | BinOp::Intersect | BinOp::Diff) + } + CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { + matches!(self.layout.entries[*idx].kind, VarKind::ExplodedSet { .. }) + } + _ => false, + } + } + + /// Infer set bounds from two operands (at least one must reveal bounds). + fn infer_set_bounds( + &mut self, + left: &CompiledExpr, + right: &CompiledExpr, + ) -> SymbolicResult<(i64, i64)> { + self.try_set_bounds(left) + .or_else(|| self.try_set_bounds(right)) + .ok_or_else(|| SymbolicError::Encoding("cannot infer set bounds from operands".into())) + } + + fn try_set_bounds(&self, expr: &CompiledExpr) -> Option<(i64, i64)> { + match expr { + CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { + if let VarKind::ExplodedSet { lo, hi } = &self.layout.entries[*idx].kind { + Some((*lo, *hi)) + } else { + None + } + } + CompiledExpr::SetComprehension { domain, .. } => { + if let CompiledExpr::Range { lo, hi } = domain.as_ref() { + let lo_val = self.extract_concrete_int(lo).ok()?; + let hi_val = self.extract_concrete_int(hi).ok()?; + Some((lo_val, hi_val)) + } else { + None + } + } + CompiledExpr::Binary { left, right, .. } => self + .try_set_bounds(left) + .or_else(|| self.try_set_bounds(right)), + _ => None, + } + } + + /// Encode a set expression as a Vec of per-element membership flags. + pub fn encode_as_set( + &mut self, + expr: &CompiledExpr, + lo: i64, + hi: i64, + ) -> SymbolicResult> { + let count = (hi - lo + 1) as usize; + match expr { + CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { + let step = match expr { + CompiledExpr::Var(_) => self.current_step, + _ => self.next_step, + }; + let z3_vars = &self.step_vars[step][*idx]; + Ok(z3_vars.iter().map(|v| v.as_bool().unwrap()).collect()) + } + CompiledExpr::SetLit(elements) => { + let mut flags = vec![Bool::from_bool(false); count]; + for elem in elements { + if let Some(val) = self.try_concrete_int(elem) { + let offset = (val - lo) as usize; + if offset < count { + flags[offset] = Bool::from_bool(true); + } + } else { + // Symbolic element: set the flag at the symbolic index + let elem_z3 = self.encode_int(elem)?; + for (i, k) in (lo..=hi).enumerate() { + let k_z3 = Int::from_i64(k); + let is_match = elem_z3.eq(&k_z3); + flags[i] = Bool::or(&[flags[i].clone(), is_match]); + } + } + } + Ok(flags) + } + CompiledExpr::SetComprehension { + element: _, + domain, + filter, + } => { + let (dom_lo, dom_hi) = self.extract_range(domain)?; + let mut flags = vec![Bool::from_bool(false); count]; + for val in dom_lo..=dom_hi { + let offset = (val - lo) as usize; + if offset >= count { + continue; + } + let z3_val = Dynamic::from_ast(&Int::from_i64(val)); + self.locals.push(z3_val); + let included = if let Some(f) = filter { + self.encode_bool(f)? + } else { + Bool::from_bool(true) + }; + self.locals.pop(); + flags[offset] = included; + } + Ok(flags) + } + CompiledExpr::Binary { + op: BinOp::Union, + left, + right, + } => { + let l = self.encode_as_set(left, lo, hi)?; + let r = self.encode_as_set(right, lo, hi)?; + Ok(l.iter() + .zip(r.iter()) + .map(|(a, b)| Bool::or(&[a.clone(), b.clone()])) + .collect()) + } + CompiledExpr::Binary { + op: BinOp::Intersect, + left, + right, + } => { + let l = self.encode_as_set(left, lo, hi)?; + let r = self.encode_as_set(right, lo, hi)?; + Ok(l.iter() + .zip(r.iter()) + .map(|(a, b)| Bool::and(&[a.clone(), b.clone()])) + .collect()) + } + CompiledExpr::Binary { + op: BinOp::Diff, + left, + right, + } => { + let l = self.encode_as_set(left, lo, hi)?; + let r = self.encode_as_set(right, lo, hi)?; + Ok(l.iter() + .zip(r.iter()) + .map(|(a, b)| Bool::and(&[a.clone(), b.not()])) + .collect()) + } + _ => Err(SymbolicError::Encoding(format!( + "cannot encode as set: {:?}", + std::mem::discriminant(expr) + ))), + } + } + // === Helpers === fn try_concrete_int(&self, expr: &CompiledExpr) -> Option { diff --git a/specl/crates/specl-symbolic/src/fixedpoint.rs b/specl/crates/specl-symbolic/src/fixedpoint.rs new file mode 100644 index 0000000..ebd0eb8 --- /dev/null +++ b/specl/crates/specl-symbolic/src/fixedpoint.rs @@ -0,0 +1,66 @@ +//! Minimal safe wrapper around z3-sys fixedpoint (Spacer/IC3) API. + +use z3::Context; + +/// Wrapper around Z3 fixedpoint engine (Spacer). +pub struct Fixedpoint { + ctx: z3_sys::Z3_context, + fp: z3_sys::Z3_fixedpoint, +} + +impl Fixedpoint { + /// Create a new fixedpoint engine using the thread-local Z3 context. + pub fn new() -> Self { + let ctx = Context::thread_local().get_z3_context(); + let fp = unsafe { z3_sys::Z3_mk_fixedpoint(ctx) }.unwrap(); + unsafe { z3_sys::Z3_fixedpoint_inc_ref(ctx, fp) }; + + // Set engine to spacer (IC3) + let params = unsafe { z3_sys::Z3_mk_params(ctx) }.unwrap(); + unsafe { z3_sys::Z3_params_inc_ref(ctx, params) }; + let key = + unsafe { z3_sys::Z3_mk_string_symbol(ctx, b"engine\0".as_ptr() as *const _) }.unwrap(); + let val = + unsafe { z3_sys::Z3_mk_string_symbol(ctx, b"spacer\0".as_ptr() as *const _) }.unwrap(); + unsafe { z3_sys::Z3_params_set_symbol(ctx, params, key, val) }; + unsafe { z3_sys::Z3_fixedpoint_set_params(ctx, fp, params) }; + unsafe { z3_sys::Z3_params_dec_ref(ctx, params) }; + + Fixedpoint { ctx, fp } + } + + /// Register a relation (func_decl) with the fixedpoint engine. + pub fn register_relation(&self, func_decl: z3_sys::Z3_func_decl) { + unsafe { z3_sys::Z3_fixedpoint_register_relation(self.ctx, self.fp, func_decl) }; + } + + /// Add a rule (universally quantified Horn clause). + pub fn add_rule(&self, rule: z3_sys::Z3_ast) { + let name = unsafe { z3_sys::Z3_mk_string_symbol(self.ctx, b"rule\0".as_ptr() as *const _) } + .unwrap(); + unsafe { z3_sys::Z3_fixedpoint_add_rule(self.ctx, self.fp, rule, name) }; + } + + /// Query whether the given relation is reachable. Returns Z3_lbool. + pub fn query(&self, query: z3_sys::Z3_ast) -> z3_sys::Z3_lbool { + unsafe { z3_sys::Z3_fixedpoint_query(self.ctx, self.fp, query) } + } + + /// Get the reason for an unknown result. + pub fn get_reason_unknown(&self) -> String { + let s = unsafe { z3_sys::Z3_fixedpoint_get_reason_unknown(self.ctx, self.fp) }; + if s.is_null() { + return "(null)".to_string(); + } + unsafe { std::ffi::CStr::from_ptr(s) } + .to_str() + .unwrap_or("(invalid utf8)") + .to_string() + } +} + +impl Drop for Fixedpoint { + fn drop(&mut self) { + unsafe { z3_sys::Z3_fixedpoint_dec_ref(self.ctx, self.fp) }; + } +} diff --git a/specl/crates/specl-symbolic/src/ic3.rs b/specl/crates/specl-symbolic/src/ic3.rs new file mode 100644 index 0000000..6080713 --- /dev/null +++ b/specl/crates/specl-symbolic/src/ic3.rs @@ -0,0 +1,281 @@ +//! IC3/CHC verification via Z3's Spacer engine. +//! +//! Encodes the spec as Constrained Horn Clauses and uses Z3's fixedpoint +//! engine (Spacer) to perform unbounded verification. + +use crate::encoder::{assert_range_constraints, create_step_vars, EncoderCtx}; +use crate::fixedpoint::Fixedpoint; +use crate::state_vars::{VarKind, VarLayout}; +use crate::transition::{encode_init, encode_transition}; +use crate::{SymbolicOutcome, SymbolicResult}; +use specl_eval::Value; +use specl_ir::CompiledSpec; +use tracing::info; +use z3::ast::{Ast, Dynamic}; +use z3::{Context, Solver}; + +/// Run IC3/CHC verification using Z3's Spacer engine. +pub fn check_ic3(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { + info!("starting IC3/CHC verification"); + + let layout = VarLayout::from_spec(spec, consts)?; + let ctx = Context::thread_local().get_z3_context(); + let fp = Fixedpoint::new(); + + // Collect sorts for all flattened state variables + let sorts = collect_sorts(&layout, ctx); + let num_vars = sorts.len(); + + // Declare Reach relation + let reach_name = + unsafe { z3_sys::Z3_mk_string_symbol(ctx, b"Reach\0".as_ptr() as *const _) }.unwrap(); + let bool_sort = unsafe { z3_sys::Z3_mk_bool_sort(ctx) }.unwrap(); + let reach_decl = unsafe { + z3_sys::Z3_mk_func_decl(ctx, reach_name, num_vars as u32, sorts.as_ptr(), bool_sort) + } + .unwrap(); + fp.register_relation(reach_decl); + + // Create step vars for step 0 and step 1 + let step0_vars = create_step_vars(&layout, 0); + let step1_vars = create_step_vars(&layout, 1); + let all_step_vars = vec![step0_vars, step1_vars]; + + // Collect all Z3 constants (as Z3_app) for quantification + let flat0 = flatten_step_vars(&all_step_vars[0]); + let flat1 = flatten_step_vars(&all_step_vars[1]); + let apps0 = to_apps(ctx, &flat0); + let apps1 = to_apps(ctx, &flat1); + let all_apps: Vec = apps0.iter().chain(apps1.iter()).copied().collect(); + + let reach_0 = mk_app(ctx, reach_decl, &flat0); + let reach_1 = mk_app(ctx, reach_decl, &flat1); + + // === Init rule: forall vars0. init(vars0) => Reach(vars0) === + let init_solver = Solver::new(); + assert_range_constraints(&init_solver, &layout, &all_step_vars, 0); + encode_init(&init_solver, spec, consts, &layout, &all_step_vars)?; + let init_formula = solver_conjunction_raw(ctx, &init_solver); + let init_body = mk_implies(ctx, init_formula, reach_0); + let init_rule = mk_forall(ctx, &apps0, init_body); + fp.add_rule(init_rule); + + // === Transition rule: forall vars0,vars1. Reach(vars0) ∧ range(vars1) ∧ trans => Reach(vars1) === + let trans = encode_transition(spec, consts, &layout, &all_step_vars, 0)?; + let trans_raw = trans.get_z3_ast(); + inc_ref(ctx, trans_raw); + + let range_solver = Solver::new(); + assert_range_constraints(&range_solver, &layout, &all_step_vars, 1); + let range_formula = solver_conjunction_raw(ctx, &range_solver); + + let trans_body = mk_and3(ctx, reach_0, range_formula, trans_raw); + let trans_impl = mk_implies(ctx, trans_body, reach_1); + let trans_rule = mk_forall(ctx, &all_apps, trans_impl); + fp.add_rule(trans_rule); + + // === Query each invariant === + // Use Error relation pattern: Reach(vars) ∧ ¬inv(vars) => Error + let err_name = + unsafe { z3_sys::Z3_mk_string_symbol(ctx, b"Error\0".as_ptr() as *const _) }.unwrap(); + let err_decl = + unsafe { z3_sys::Z3_mk_func_decl(ctx, err_name, 0, std::ptr::null(), bool_sort) }.unwrap(); + fp.register_relation(err_decl); + let err_app = mk_app(ctx, err_decl, &[]); + + for inv in &spec.invariants { + let mut enc = EncoderCtx { + layout: &layout, + consts, + step_vars: &all_step_vars, + current_step: 0, + next_step: 0, + params: &[], + locals: Vec::new(), + }; + let inv_encoded = enc.encode_bool(&inv.body)?; + let inv_raw = inv_encoded.get_z3_ast(); + inc_ref(ctx, inv_raw); + let neg_inv_raw = mk_not(ctx, inv_raw); + + // Rule: forall vars0. Reach(vars0) ∧ ¬I(vars0) => Error + let err_body = mk_and2(ctx, reach_0, neg_inv_raw); + let err_impl = mk_implies(ctx, err_body, err_app); + let err_rule = mk_forall(ctx, &apps0, err_impl); + fp.add_rule(err_rule); + + match fp.query(err_app) { + z3_sys::Z3_L_FALSE => { + info!(invariant = inv.name, "invariant verified by IC3"); + } + z3_sys::Z3_L_TRUE => { + info!(invariant = inv.name, "IC3 found invariant violation"); + return Ok(SymbolicOutcome::InvariantViolation { + invariant: inv.name.clone(), + trace: Vec::new(), + }); + } + _ => { + let reason = fp.get_reason_unknown(); + info!( + invariant = inv.name, + reason = reason, + "IC3 returned unknown" + ); + return Ok(SymbolicOutcome::Unknown { + reason: format!( + "IC3 returned unknown for invariant '{}': {}", + inv.name, reason + ), + }); + } + } + } + + info!("all invariants verified by IC3"); + Ok(SymbolicOutcome::Ok { method: "IC3" }) +} + +// === Raw z3-sys helper functions === +// All helpers inc_ref their return values to prevent Z3 GC. + +fn inc_ref(ctx: z3_sys::Z3_context, ast: z3_sys::Z3_ast) { + unsafe { z3_sys::Z3_inc_ref(ctx, ast) }; +} + +fn mk_implies(ctx: z3_sys::Z3_context, a: z3_sys::Z3_ast, b: z3_sys::Z3_ast) -> z3_sys::Z3_ast { + let r = unsafe { z3_sys::Z3_mk_implies(ctx, a, b) }.unwrap(); + inc_ref(ctx, r); + r +} + +fn mk_not(ctx: z3_sys::Z3_context, a: z3_sys::Z3_ast) -> z3_sys::Z3_ast { + let r = unsafe { z3_sys::Z3_mk_not(ctx, a) }.unwrap(); + inc_ref(ctx, r); + r +} + +fn mk_and2(ctx: z3_sys::Z3_context, a: z3_sys::Z3_ast, b: z3_sys::Z3_ast) -> z3_sys::Z3_ast { + let args = [a, b]; + let r = unsafe { z3_sys::Z3_mk_and(ctx, 2, args.as_ptr()) }.unwrap(); + inc_ref(ctx, r); + r +} + +fn mk_and3( + ctx: z3_sys::Z3_context, + a: z3_sys::Z3_ast, + b: z3_sys::Z3_ast, + c: z3_sys::Z3_ast, +) -> z3_sys::Z3_ast { + let args = [a, b, c]; + let r = unsafe { z3_sys::Z3_mk_and(ctx, 3, args.as_ptr()) }.unwrap(); + inc_ref(ctx, r); + r +} + +fn mk_app( + ctx: z3_sys::Z3_context, + decl: z3_sys::Z3_func_decl, + args: &[z3_sys::Z3_ast], +) -> z3_sys::Z3_ast { + let r = unsafe { z3_sys::Z3_mk_app(ctx, decl, args.len() as u32, args.as_ptr()) }.unwrap(); + inc_ref(ctx, r); + r +} + +fn mk_forall( + ctx: z3_sys::Z3_context, + apps: &[z3_sys::Z3_app], + body: z3_sys::Z3_ast, +) -> z3_sys::Z3_ast { + if apps.is_empty() { + return body; + } + let r = unsafe { + z3_sys::Z3_mk_forall_const( + ctx, + 0, // weight + apps.len() as u32, + apps.as_ptr(), + 0, // num_patterns + std::ptr::null(), + body, + ) + } + .unwrap(); + inc_ref(ctx, r); + r +} + +/// Convert Z3_ast constants to Z3_app for quantifier binding. +fn to_apps(ctx: z3_sys::Z3_context, asts: &[z3_sys::Z3_ast]) -> Vec { + asts.iter() + .map(|a| unsafe { z3_sys::Z3_to_app(ctx, *a) }.unwrap()) + .collect() +} + +/// Extract all solver assertions as a raw Z3_ast conjunction. +/// The returned AST is ref-counted (inc_ref called). +fn solver_conjunction_raw(ctx: z3_sys::Z3_context, solver: &Solver) -> z3_sys::Z3_ast { + let assertions = solver.get_assertions(); + if assertions.is_empty() { + let t = unsafe { z3_sys::Z3_mk_true(ctx) }.unwrap(); + inc_ref(ctx, t); + return t; + } + let raw: Vec = assertions.iter().map(|a| a.get_z3_ast()).collect(); + let result = if raw.len() == 1 { + raw[0] + } else { + unsafe { z3_sys::Z3_mk_and(ctx, raw.len() as u32, raw.as_ptr()) }.unwrap() + }; + inc_ref(ctx, result); + result +} + +/// Collect Z3 sorts for all flattened state variables. +fn collect_sorts(layout: &VarLayout, ctx: z3_sys::Z3_context) -> Vec { + let bool_sort = unsafe { z3_sys::Z3_mk_bool_sort(ctx) }.unwrap(); + let int_sort = unsafe { z3_sys::Z3_mk_int_sort(ctx) }.unwrap(); + + let mut sorts = Vec::new(); + for entry in &layout.entries { + collect_sorts_for_kind(&entry.kind, bool_sort, int_sort, &mut sorts); + } + sorts +} + +fn collect_sorts_for_kind( + kind: &VarKind, + bool_sort: z3_sys::Z3_sort, + int_sort: z3_sys::Z3_sort, + out: &mut Vec, +) { + match kind { + VarKind::Bool => out.push(bool_sort), + VarKind::Int { .. } => out.push(int_sort), + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { + for _ in 0..(*key_hi - *key_lo + 1) { + collect_sorts_for_kind(value_kind, bool_sort, int_sort, out); + } + } + VarKind::ExplodedSet { lo, hi } => { + for _ in 0..(*hi - *lo + 1) { + out.push(bool_sort); + } + } + } +} + +/// Flatten step vars into a single vec of raw Z3 ASTs. +fn flatten_step_vars(step_vars: &[Vec]) -> Vec { + step_vars + .iter() + .flat_map(|vs| vs.iter().map(|v| v.get_z3_ast())) + .collect() +} diff --git a/specl/crates/specl-symbolic/src/inductive.rs b/specl/crates/specl-symbolic/src/inductive.rs index dd8b8c1..51f318c 100644 --- a/specl/crates/specl-symbolic/src/inductive.rs +++ b/specl/crates/specl-symbolic/src/inductive.rs @@ -20,7 +20,7 @@ use z3::{SatResult, Solver}; pub fn check_inductive(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { info!("starting inductive invariant checking"); - let layout = VarLayout::from_spec(spec)?; + let layout = VarLayout::from_spec(spec, consts)?; let solver = Solver::new(); let step0_vars = create_step_vars(&layout, 0); diff --git a/specl/crates/specl-symbolic/src/k_induction.rs b/specl/crates/specl-symbolic/src/k_induction.rs new file mode 100644 index 0000000..db95b78 --- /dev/null +++ b/specl/crates/specl-symbolic/src/k_induction.rs @@ -0,0 +1,197 @@ +//! k-induction: strictly more powerful than simple induction. +//! +//! For each invariant I, checks two conditions: +//! Base case: BMC to depth K finds no violation (init + transitions + ¬I is UNSAT for all steps) +//! Inductive step: K+1 consecutive states where I holds for the first K, +//! transitions hold between all, and ¬I at step K — must be UNSAT. +//! +//! Both UNSAT → proven for all reachable states. + +use crate::encoder::{assert_range_constraints, create_step_vars, EncoderCtx}; +use crate::state_vars::VarLayout; +use crate::trace::extract_trace; +use crate::transition::{encode_init, encode_transition}; +use crate::{SymbolicOutcome, SymbolicResult}; +use specl_eval::Value; +use specl_ir::CompiledSpec; +use tracing::info; +use z3::{SatResult, Solver}; + +/// Run k-induction checking with the given strengthening depth. +pub fn check_k_induction( + spec: &CompiledSpec, + consts: &[Value], + k: usize, +) -> SymbolicResult { + info!(k, "starting k-induction"); + + let layout = VarLayout::from_spec(spec, consts)?; + + // === Base case: BMC to depth K === + info!(k, "k-induction base case"); + if let Some(outcome) = check_base_case(spec, consts, &layout, k)? { + return Ok(outcome); + } + + // === Inductive step === + info!(k, "k-induction inductive step"); + check_inductive_step(spec, consts, &layout, k) +} + +/// Base case: init + transitions for K steps, check ¬I at each step. +fn check_base_case( + spec: &CompiledSpec, + consts: &[Value], + layout: &VarLayout, + k: usize, +) -> SymbolicResult> { + let solver = Solver::new(); + + let mut all_step_vars = Vec::new(); + for step in 0..=k { + all_step_vars.push(create_step_vars(layout, step)); + } + + for step in 0..=k { + assert_range_constraints(&solver, layout, &all_step_vars, step); + } + + encode_init(&solver, spec, consts, layout, &all_step_vars)?; + + for depth in 0..=k { + if depth > 0 { + let trans = encode_transition(spec, consts, layout, &all_step_vars, depth - 1)?; + solver.assert(&trans); + } + + for inv in &spec.invariants { + solver.push(); + + let mut enc = EncoderCtx { + layout, + consts, + step_vars: &all_step_vars, + current_step: depth, + next_step: depth, + params: &[], + locals: Vec::new(), + }; + let inv_encoded = enc.encode_bool(&inv.body)?; + solver.assert(&inv_encoded.not()); + + match solver.check() { + SatResult::Sat => { + info!(invariant = inv.name, depth, "base case violation found"); + let model = solver.get_model().unwrap(); + let trace = extract_trace(&model, layout, &all_step_vars, spec, consts, depth); + return Ok(Some(SymbolicOutcome::InvariantViolation { + invariant: inv.name.clone(), + trace, + })); + } + SatResult::Unsat => {} + SatResult::Unknown => { + solver.pop(1); + return Ok(Some(SymbolicOutcome::Unknown { + reason: format!( + "Z3 returned unknown at base depth {} for invariant '{}'", + depth, inv.name + ), + })); + } + } + + solver.pop(1); + } + } + + Ok(None) +} + +/// Inductive step: K+1 states (0..=K), assert I at 0..K-1, transitions, ¬I at K. +fn check_inductive_step( + spec: &CompiledSpec, + consts: &[Value], + layout: &VarLayout, + k: usize, +) -> SymbolicResult { + let solver = Solver::new(); + + // K+1 states: 0..=K + let mut all_step_vars = Vec::new(); + for step in 0..=k { + all_step_vars.push(create_step_vars(layout, step)); + } + + for step in 0..=k { + assert_range_constraints(&solver, layout, &all_step_vars, step); + } + + // Assert transitions between all consecutive pairs + for step in 0..k { + let trans = encode_transition(spec, consts, layout, &all_step_vars, step)?; + solver.assert(&trans); + } + + for inv in &spec.invariants { + solver.push(); + + // Assert I(s_0), ..., I(s_{K-1}) + for step in 0..k { + let mut enc = EncoderCtx { + layout, + consts, + step_vars: &all_step_vars, + current_step: step, + next_step: step, + params: &[], + locals: Vec::new(), + }; + let inv_at_step = enc.encode_bool(&inv.body)?; + solver.assert(&inv_at_step); + } + + // Assert ¬I(s_K) + let mut enc_k = EncoderCtx { + layout, + consts, + step_vars: &all_step_vars, + current_step: k, + next_step: k, + params: &[], + locals: Vec::new(), + }; + let inv_at_k = enc_k.encode_bool(&inv.body)?; + solver.assert(&inv_at_k.not()); + + match solver.check() { + SatResult::Sat => { + // CTI (counterexample to induction) — not a real bug, just not provable at K + info!(invariant = inv.name, k, "inductive step failed (CTI)"); + solver.pop(1); + return Ok(SymbolicOutcome::Unknown { + reason: format!("invariant '{}' not k-inductive at k={}", inv.name, k), + }); + } + SatResult::Unsat => { + info!(invariant = inv.name, k, "invariant is k-inductive"); + } + SatResult::Unknown => { + solver.pop(1); + return Ok(SymbolicOutcome::Unknown { + reason: format!( + "Z3 returned unknown for k-induction step for invariant '{}'", + inv.name + ), + }); + } + } + + solver.pop(1); + } + + info!(k, "all invariants are k-inductive"); + Ok(SymbolicOutcome::Ok { + method: "k-induction", + }) +} diff --git a/specl/crates/specl-symbolic/src/lib.rs b/specl/crates/specl-symbolic/src/lib.rs index 9799e9f..533aa44 100644 --- a/specl/crates/specl-symbolic/src/lib.rs +++ b/specl/crates/specl-symbolic/src/lib.rs @@ -5,7 +5,11 @@ pub mod bmc; pub mod encoder; +pub mod fixedpoint; +pub mod ic3; pub mod inductive; +pub mod k_induction; +pub mod smart; pub mod state_vars; pub mod trace; pub mod transition; @@ -69,6 +73,12 @@ pub enum SymbolicMode { Bmc, /// Inductive invariant checking: single-step proof. Inductive, + /// k-induction with given strengthening depth. + KInduction(usize), + /// IC3/CHC via Z3's Spacer engine (unbounded verification). + Ic3, + /// Smart mode: automatic strategy cascade. + Smart, } /// Run symbolic model checking on a compiled spec. @@ -80,5 +90,8 @@ pub fn check( match config.mode { SymbolicMode::Bmc => bmc::check_bmc(spec, consts, config.depth), SymbolicMode::Inductive => inductive::check_inductive(spec, consts), + SymbolicMode::KInduction(k) => k_induction::check_k_induction(spec, consts, k), + SymbolicMode::Ic3 => ic3::check_ic3(spec, consts), + SymbolicMode::Smart => smart::check_smart(spec, consts, config.depth), } } diff --git a/specl/crates/specl-symbolic/src/smart.rs b/specl/crates/specl-symbolic/src/smart.rs new file mode 100644 index 0000000..9b7fbcc --- /dev/null +++ b/specl/crates/specl-symbolic/src/smart.rs @@ -0,0 +1,80 @@ +//! Smart mode: automatic strategy cascade for symbolic verification. +//! +//! Tries progressively stronger techniques: +//! 1. Inductive checking (fastest, but may fail for non-inductive invariants) +//! 2. k-induction with increasing K (2..5) +//! 3. IC3/CHC via Spacer (unbounded, most powerful) +//! 4. BMC fallback (bounded, catches real bugs) + +use crate::{SymbolicOutcome, SymbolicResult}; +use specl_eval::Value; +use specl_ir::CompiledSpec; +use tracing::info; + +/// Run smart mode: try increasingly powerful strategies. +pub fn check_smart( + spec: &CompiledSpec, + consts: &[Value], + bmc_depth: usize, +) -> SymbolicResult { + // 1. Try simple induction + info!("smart: trying inductive checking"); + match crate::inductive::check_inductive(spec, consts)? { + SymbolicOutcome::Ok { .. } => { + return Ok(SymbolicOutcome::Ok { + method: "smart(inductive)", + }); + } + SymbolicOutcome::InvariantViolation { .. } => { + // Inductive failure = CTI (counterexample to induction), not a real bug + info!("smart: inductive check found CTI, trying k-induction"); + } + SymbolicOutcome::Unknown { .. } => { + info!("smart: inductive check returned unknown, trying k-induction"); + } + } + + // 2. Try k-induction with increasing K + for k in [2, 3, 4, 5] { + info!(k, "smart: trying k-induction"); + match crate::k_induction::check_k_induction(spec, consts, k)? { + SymbolicOutcome::Ok { .. } => { + return Ok(SymbolicOutcome::Ok { + method: "smart(k-induction)", + }); + } + SymbolicOutcome::InvariantViolation { invariant, trace } => { + // k-induction base case failure = real bug + return Ok(SymbolicOutcome::InvariantViolation { invariant, trace }); + } + SymbolicOutcome::Unknown { .. } => { + // Inductive step failed at this K, try higher + } + } + } + + // 3. Try IC3/CHC + info!("smart: trying IC3/CHC"); + match crate::ic3::check_ic3(spec, consts)? { + SymbolicOutcome::Ok { .. } => { + return Ok(SymbolicOutcome::Ok { + method: "smart(IC3)", + }); + } + SymbolicOutcome::InvariantViolation { invariant, trace } => { + return Ok(SymbolicOutcome::InvariantViolation { invariant, trace }); + } + SymbolicOutcome::Unknown { .. } => { + info!("smart: IC3 returned unknown, falling back to BMC"); + } + } + + // 4. Fall back to BMC + info!(depth = bmc_depth, "smart: falling back to BMC"); + match crate::bmc::check_bmc(spec, consts, bmc_depth)? { + SymbolicOutcome::Ok { .. } => Ok(SymbolicOutcome::Ok { + method: "smart(BMC)", + }), + other => Ok(other), + } +} diff --git a/specl/crates/specl-symbolic/src/state_vars.rs b/specl/crates/specl-symbolic/src/state_vars.rs index a70131a..fa5a510 100644 --- a/specl/crates/specl-symbolic/src/state_vars.rs +++ b/specl/crates/specl-symbolic/src/state_vars.rs @@ -1,6 +1,8 @@ //! Variable layout analysis: maps specl state variables to Z3 variables. -use specl_ir::CompiledSpec; +use specl_eval::Value; +use specl_ir::{CompiledExpr, CompiledSpec}; +use specl_syntax::{ExprKind, TypeExpr}; use specl_types::Type; use crate::SymbolicResult; @@ -10,6 +12,8 @@ use crate::SymbolicResult; pub struct VarLayout { /// One entry per specl state variable. pub entries: Vec, + /// String interning table: maps string literals to integer IDs. + pub string_table: Vec, } /// How a single specl variable maps to Z3 variables. @@ -42,61 +46,371 @@ pub enum VarKind { impl VarLayout { /// Analyze a compiled spec and compute the Z3 variable layout. - pub fn from_spec(spec: &CompiledSpec) -> SymbolicResult { + pub fn from_spec(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { + let string_table = build_string_table(spec); let mut entries = Vec::new(); for var in &spec.vars { - let kind = Self::type_to_kind(&var.ty)?; + let kind = type_to_kind(&var.ty, var.index, spec, consts, &string_table)?; entries.push(VarEntry { specl_var_idx: var.index, name: var.name.clone(), kind, }); } - Ok(VarLayout { entries }) - } - - fn type_to_kind(ty: &Type) -> SymbolicResult { - match ty { - Type::Bool => Ok(VarKind::Bool), - Type::Int => Ok(VarKind::Int { lo: None, hi: None }), - Type::Nat => Ok(VarKind::Int { - lo: Some(0), - hi: None, - }), - Type::Range(lo, hi) => Ok(VarKind::Int { - lo: Some(*lo), - hi: Some(*hi), - }), - Type::Fn(key_ty, val_ty) => { - if let Type::Range(lo, hi) = key_ty.as_ref() { - let value_kind = Self::type_to_kind(val_ty)?; + Ok(VarLayout { + entries, + string_table, + }) + } + + /// Look up a string literal's integer ID. + pub fn string_id(&self, s: &str) -> Option { + self.string_table + .iter() + .position(|t| t == s) + .map(|i| i as i64) + } +} + +fn type_to_kind( + ty: &Type, + var_idx: usize, + spec: &CompiledSpec, + consts: &[Value], + string_table: &[String], +) -> SymbolicResult { + match ty { + Type::Bool => Ok(VarKind::Bool), + Type::Int => Ok(VarKind::Int { lo: None, hi: None }), + Type::Nat => Ok(VarKind::Int { + lo: Some(0), + hi: None, + }), + Type::String => { + if string_table.is_empty() { + Ok(VarKind::Int { lo: None, hi: None }) + } else { + Ok(VarKind::Int { + lo: Some(0), + hi: Some(string_table.len() as i64 - 1), + }) + } + } + Type::Range(lo, hi) => Ok(VarKind::Int { + lo: Some(*lo), + hi: Some(*hi), + }), + Type::Fn(key_ty, val_ty) => { + if let Type::Range(lo, hi) = key_ty.as_ref() { + let value_kind = type_to_kind_simple(val_ty)?; + Ok(VarKind::ExplodedDict { + key_lo: *lo, + key_hi: *hi, + value_kind: Box::new(value_kind), + }) + } else if matches!(key_ty.as_ref(), Type::Int | Type::Nat) { + // Key type is Int/Nat — try to infer range from init expression + if let Some((lo, hi)) = infer_dict_range(var_idx, spec, consts) { + let value_kind = type_to_kind_simple(val_ty)?; Ok(VarKind::ExplodedDict { - key_lo: *lo, - key_hi: *hi, + key_lo: lo, + key_hi: hi, value_kind: Box::new(value_kind), }) } else { Err(crate::SymbolicError::Unsupported(format!( - "Dict with non-range key type: {:?}", + "Dict with unbounded key type {:?} (cannot infer range from init)", key_ty ))) } + } else { + Err(crate::SymbolicError::Unsupported(format!( + "Dict with non-range key type: {:?}", + key_ty + ))) } - Type::Set(elem_ty) => { - if let Type::Range(lo, hi) = elem_ty.as_ref() { - Ok(VarKind::ExplodedSet { lo: *lo, hi: *hi }) + } + Type::Set(elem_ty) => { + if let Type::Range(lo, hi) = elem_ty.as_ref() { + Ok(VarKind::ExplodedSet { lo: *lo, hi: *hi }) + } else if matches!(elem_ty.as_ref(), Type::Int | Type::Nat) { + // Try to infer range from action parameters or init + if let Some((lo, hi)) = infer_set_range_from_actions(var_idx, spec, consts) { + Ok(VarKind::ExplodedSet { lo, hi }) } else { Err(crate::SymbolicError::Unsupported(format!( - "Set with non-range element type: {:?}", + "Set with unbounded element type {:?} (cannot infer range)", elem_ty ))) } + } else { + Err(crate::SymbolicError::Unsupported(format!( + "Set with non-range element type: {:?}", + elem_ty + ))) } - _ => Err(crate::SymbolicError::Unsupported(format!( - "variable type: {:?}", - ty - ))), } + _ => Err(crate::SymbolicError::Unsupported(format!( + "variable type: {:?}", + ty + ))), + } +} + +/// Simple type_to_kind without spec/const context (for value types within containers). +fn type_to_kind_simple(ty: &Type) -> SymbolicResult { + match ty { + Type::Bool => Ok(VarKind::Bool), + Type::Int | Type::String => Ok(VarKind::Int { lo: None, hi: None }), + Type::Nat => Ok(VarKind::Int { + lo: Some(0), + hi: None, + }), + Type::Range(lo, hi) => Ok(VarKind::Int { + lo: Some(*lo), + hi: Some(*hi), + }), + _ => Err(crate::SymbolicError::Unsupported(format!( + "value type in container: {:?}", + ty + ))), + } +} + +/// Infer dict key range from init expression or action parameters. +fn infer_dict_range(var_idx: usize, spec: &CompiledSpec, consts: &[Value]) -> Option<(i64, i64)> { + if let Some(range) = find_var_init_range(var_idx, &spec.init, consts) { + return Some(range); + } + // Fall through to AST type expressions on actions that modify this variable + for action in &spec.actions { + if !action.changes.contains(&var_idx) { + continue; + } + for type_expr in &action.param_type_exprs { + if let Some(range) = eval_type_expr_range(type_expr, spec, consts) { + return Some(range); + } + } + } + None +} + +/// Infer set element range from action parameters that add to this set. +fn infer_set_range_from_actions( + var_idx: usize, + spec: &CompiledSpec, + consts: &[Value], +) -> Option<(i64, i64)> { + // First try init expression + if let Some(range) = find_var_init_range(var_idx, &spec.init, consts) { + return Some(range); + } + // Try to find from action parameter types that reference this set + for action in &spec.actions { + if !action.changes.contains(&var_idx) { + continue; + } + // Try compiled param types first (works when type checker resolved the range) + for (_, param_ty) in &action.params { + if let Type::Range(lo, hi) = param_ty { + return Some((*lo, *hi)); + } + } + // Fall through to AST type expressions (works when consts aren't resolved by type checker) + for type_expr in &action.param_type_exprs { + if let Some(range) = eval_type_expr_range(type_expr, spec, consts) { + return Some(range); + } + } + } + None +} + +/// Walk the init expression to find a FnLit/SetComprehension domain for a variable. +fn find_var_init_range( + var_idx: usize, + expr: &CompiledExpr, + consts: &[Value], +) -> Option<(i64, i64)> { + match expr { + CompiledExpr::Binary { + op: specl_ir::BinOp::And, + left, + right, + } => find_var_init_range(var_idx, left, consts) + .or_else(|| find_var_init_range(var_idx, right, consts)), + CompiledExpr::Binary { + op: specl_ir::BinOp::Eq, + left, + right, + } => { + let target_idx = match left.as_ref() { + CompiledExpr::PrimedVar(idx) | CompiledExpr::Var(idx) => Some(*idx), + _ => None, + }; + if target_idx == Some(var_idx) { + extract_domain_range(right, consts) + } else { + None + } + } + _ => None, + } +} + +/// Extract domain range from a FnLit or SetComprehension RHS. +fn extract_domain_range(expr: &CompiledExpr, consts: &[Value]) -> Option<(i64, i64)> { + match expr { + CompiledExpr::FnLit { domain, .. } | CompiledExpr::SetComprehension { domain, .. } => { + extract_range_bounds(domain, consts) + } + _ => None, + } +} + +fn extract_range_bounds(expr: &CompiledExpr, consts: &[Value]) -> Option<(i64, i64)> { + if let CompiledExpr::Range { lo, hi } = expr { + let lo_val = eval_const_int(lo, consts)?; + let hi_val = eval_const_int(hi, consts)?; + Some((lo_val, hi_val)) + } else { + None + } +} + +fn eval_const_int(expr: &CompiledExpr, consts: &[Value]) -> Option { + match expr { + CompiledExpr::Int(n) => Some(*n), + CompiledExpr::Const(idx) => { + if let Value::Int(n) = &consts[*idx] { + Some(*n) + } else { + None + } + } + _ => None, + } +} + +/// Evaluate an AST TypeExpr::Range to a concrete (lo, hi) using const values. +pub fn eval_type_expr_range( + type_expr: &TypeExpr, + spec: &CompiledSpec, + consts: &[Value], +) -> Option<(i64, i64)> { + if let TypeExpr::Range(lo_expr, hi_expr, _) = type_expr { + let lo = eval_ast_expr_int(lo_expr, spec, consts)?; + let hi = eval_ast_expr_int(hi_expr, spec, consts)?; + Some((lo, hi)) + } else { + None + } +} + +/// Evaluate a simple AST Expr to an i64 (handles int literals and const identifiers). +fn eval_ast_expr_int( + expr: &specl_syntax::Expr, + spec: &CompiledSpec, + consts: &[Value], +) -> Option { + match &expr.kind { + ExprKind::Int(n) => Some(*n), + ExprKind::Ident(name) => { + let const_decl = spec.consts.iter().find(|c| c.name == *name)?; + if let Value::Int(n) = &consts[const_decl.index] { + Some(*n) + } else { + None + } + } + _ => None, + } +} + +/// Scan all expressions in the spec for string literals and build a deduped table. +fn build_string_table(spec: &CompiledSpec) -> Vec { + let mut strings = Vec::new(); + collect_strings_from_expr(&spec.init, &mut strings); + for action in &spec.actions { + collect_strings_from_expr(&action.guard, &mut strings); + collect_strings_from_expr(&action.effect, &mut strings); + } + for inv in &spec.invariants { + collect_strings_from_expr(&inv.body, &mut strings); + } + strings.sort(); + strings.dedup(); + strings +} + +fn collect_strings_from_expr(expr: &CompiledExpr, out: &mut Vec) { + match expr { + CompiledExpr::String(s) => out.push(s.clone()), + CompiledExpr::Binary { left, right, .. } => { + collect_strings_from_expr(left, out); + collect_strings_from_expr(right, out); + } + CompiledExpr::Unary { operand, .. } => collect_strings_from_expr(operand, out), + CompiledExpr::If { + cond, + then_branch, + else_branch, + } => { + collect_strings_from_expr(cond, out); + collect_strings_from_expr(then_branch, out); + collect_strings_from_expr(else_branch, out); + } + CompiledExpr::Let { value, body, .. } => { + collect_strings_from_expr(value, out); + collect_strings_from_expr(body, out); + } + CompiledExpr::Forall { body, domain, .. } | CompiledExpr::Exists { body, domain, .. } => { + collect_strings_from_expr(domain, out); + collect_strings_from_expr(body, out); + } + CompiledExpr::FnLit { domain, body, .. } => { + collect_strings_from_expr(domain, out); + collect_strings_from_expr(body, out); + } + CompiledExpr::Index { base, index } => { + collect_strings_from_expr(base, out); + collect_strings_from_expr(index, out); + } + CompiledExpr::SetComprehension { + element, + domain, + filter, + .. + } => { + collect_strings_from_expr(element, out); + collect_strings_from_expr(domain, out); + if let Some(f) = filter { + collect_strings_from_expr(f, out); + } + } + CompiledExpr::SetLit(elems) | CompiledExpr::SeqLit(elems) => { + for e in elems { + collect_strings_from_expr(e, out); + } + } + CompiledExpr::Range { lo, hi } => { + collect_strings_from_expr(lo, out); + collect_strings_from_expr(hi, out); + } + CompiledExpr::DictLit(pairs) => { + for (k, v) in pairs { + collect_strings_from_expr(k, out); + collect_strings_from_expr(v, out); + } + } + CompiledExpr::Choose { + domain, predicate, .. + } => { + collect_strings_from_expr(domain, out); + collect_strings_from_expr(predicate, out); + } + _ => {} } } diff --git a/specl/crates/specl-symbolic/src/trace.rs b/specl/crates/specl-symbolic/src/trace.rs index cd028f3..0bce393 100644 --- a/specl/crates/specl-symbolic/src/trace.rs +++ b/specl/crates/specl-symbolic/src/trace.rs @@ -1,10 +1,11 @@ //! Counterexample trace extraction from Z3 models. +use crate::encoder::EncoderCtx; use crate::state_vars::{VarKind, VarLayout}; use crate::TraceStep; use specl_eval::Value; use specl_ir::CompiledSpec; -use z3::ast::Dynamic; +use z3::ast::{Dynamic, Int}; use z3::Model; /// Extract a counterexample trace from a Z3 model. @@ -12,21 +13,136 @@ pub fn extract_trace( model: &Model, layout: &VarLayout, step_vars: &[Vec>], - _spec: &CompiledSpec, - _consts: &[Value], + spec: &CompiledSpec, + consts: &[Value], depth: usize, ) -> Vec { let mut trace = Vec::new(); for step in 0..=depth { let state = extract_state(model, layout, &step_vars[step]); - let action = None; // Action identification is a future improvement + let action = if step > 0 { + identify_action(model, layout, step_vars, spec, consts, step - 1) + } else { + Some("init".to_string()) + }; trace.push(TraceStep { state, action }); } trace } +/// Identify which action fired at the given step by evaluating guards against the model. +fn identify_action( + model: &Model, + layout: &VarLayout, + step_vars: &[Vec>], + spec: &CompiledSpec, + consts: &[Value], + step: usize, +) -> Option { + for action in &spec.actions { + let param_ranges: Vec<(i64, i64)> = action + .params + .iter() + .enumerate() + .filter_map(|(i, (_, ty))| { + use specl_types::Type; + match ty { + Type::Range(lo, hi) => Some((*lo, *hi)), + Type::Int => action + .param_type_exprs + .get(i) + .and_then(|te| crate::state_vars::eval_type_expr_range(te, spec, consts)), + _ => None, + } + }) + .collect(); + + if param_ranges.len() != action.params.len() { + continue; + } + + if param_ranges.is_empty() { + // No parameters — just evaluate the guard + if guard_satisfied(model, layout, step_vars, spec, consts, action, step, &[]) { + return Some(action.name.clone()); + } + } else { + // Try each parameter combination + let mut combos = Vec::new(); + enumerate_param_combos(¶m_ranges, 0, &mut Vec::new(), &mut combos); + for combo in &combos { + if guard_satisfied(model, layout, step_vars, spec, consts, action, step, combo) { + let params_str = combo + .iter() + .map(|v| v.to_string()) + .collect::>() + .join(", "); + return Some(format!("{}({})", action.name, params_str)); + } + } + } + } + + None +} + +/// Check if an action's guard is satisfied in the model at the given step. +fn guard_satisfied( + model: &Model, + layout: &VarLayout, + step_vars: &[Vec>], + _spec: &CompiledSpec, + consts: &[Value], + action: &specl_ir::CompiledAction, + step: usize, + params: &[i64], +) -> bool { + let z3_params: Vec = params + .iter() + .map(|v| Dynamic::from_ast(&Int::from_i64(*v))) + .collect(); + + let mut enc = EncoderCtx { + layout, + consts, + step_vars, + current_step: step, + next_step: step + 1, + params: &z3_params, + locals: Vec::new(), + }; + + let Ok(guard) = enc.encode_bool(&action.guard) else { + return false; + }; + + model + .eval(&Dynamic::from_ast(&guard), true) + .and_then(|v| v.as_bool()) + .and_then(|b| b.as_bool()) + .unwrap_or(false) +} + +fn enumerate_param_combos( + ranges: &[(i64, i64)], + depth: usize, + current: &mut Vec, + result: &mut Vec>, +) { + if depth == ranges.len() { + result.push(current.clone()); + return; + } + let (lo, hi) = ranges[depth]; + for v in lo..=hi { + current.push(v); + enumerate_param_combos(ranges, depth + 1, current, result); + current.pop(); + } +} + fn extract_state( model: &Model, layout: &VarLayout, @@ -47,9 +163,13 @@ fn extract_state( .eval(&z3_vars[0], true) .and_then(|v| v.as_int()) .and_then(|i| i.as_i64()) - .map(|n| n.to_string()) + .map(|n| format_int_value(n, &entry.kind, &layout.string_table)) .unwrap_or_else(|| "?".to_string()), - VarKind::ExplodedDict { key_lo, key_hi, .. } => { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { let mut pairs = Vec::new(); for (i, k) in (*key_lo..=*key_hi).enumerate() { let val = model @@ -57,7 +177,7 @@ fn extract_state( .and_then(|v| { v.as_int() .and_then(|i| i.as_i64()) - .map(|n| n.to_string()) + .map(|n| format_int_value(n, value_kind, &layout.string_table)) .or_else(|| { v.as_bool().and_then(|b| b.as_bool()).map(|b| b.to_string()) }) @@ -88,3 +208,19 @@ fn extract_state( state } + +/// Format an integer value, using string table reverse-lookup if applicable. +fn format_int_value(n: i64, kind: &VarKind, string_table: &[String]) -> String { + if let VarKind::Int { + lo: Some(0), + hi: Some(hi), + } = kind + { + if !string_table.is_empty() && *hi == string_table.len() as i64 - 1 { + if let Some(s) = string_table.get(n as usize) { + return format!("\"{}\"", s); + } + } + } + n.to_string() +} diff --git a/specl/crates/specl-symbolic/src/transition.rs b/specl/crates/specl-symbolic/src/transition.rs index 822e7b4..5d12e9a 100644 --- a/specl/crates/specl-symbolic/src/transition.rs +++ b/specl/crates/specl-symbolic/src/transition.rs @@ -182,10 +182,20 @@ fn encode_init_assignment( ))), } } - VarKind::ExplodedSet { .. } => { - // Default: empty set - for var in z3_vars { - solver.assert(&var.as_bool().unwrap().not()); + VarKind::ExplodedSet { lo, hi } => { + let mut enc = EncoderCtx { + layout, + consts, + step_vars, + current_step: 0, + next_step: 0, + params: &[], + locals: Vec::new(), + }; + let flags = enc.encode_as_set(rhs, *lo, *hi)?; + for (i, flag) in flags.iter().enumerate() { + let vb = z3_vars[i].as_bool().unwrap(); + solver.assert(&vb.eq(flag)); } Ok(()) } @@ -204,7 +214,7 @@ pub fn encode_transition( let mut action_encodings = Vec::new(); for action in &spec.actions { - let action_enc = encode_action(action, consts, layout, step_vars, step)?; + let action_enc = encode_action(action, spec, consts, layout, step_vars, step)?; action_encodings.push(action_enc); } @@ -213,6 +223,7 @@ pub fn encode_transition( fn encode_action( action: &CompiledAction, + spec: &CompiledSpec, consts: &[Value], layout: &VarLayout, step_vars: &[Vec>], @@ -221,10 +232,19 @@ fn encode_action( let param_ranges: Vec<(i64, i64)> = action .params .iter() - .map(|(_, ty)| match ty { + .enumerate() + .map(|(i, (_, ty))| match ty { Type::Range(lo, hi) => Ok((*lo, *hi)), Type::Nat => Ok((0, 100)), - Type::Int => Err(SymbolicError::Unsupported("unbounded Int parameter".into())), + Type::Int => { + // Try resolving from AST type expressions (handles const-dependent ranges) + if let Some(type_expr) = action.param_type_exprs.get(i) { + crate::state_vars::eval_type_expr_range(type_expr, spec, consts) + .ok_or_else(|| SymbolicError::Unsupported("unbounded Int parameter".into())) + } else { + Err(SymbolicError::Unsupported("unbounded Int parameter".into())) + } + } _ => Err(SymbolicError::Unsupported(format!( "parameter type: {:?}", ty @@ -453,9 +473,17 @@ fn encode_primed_assignment( ))), } } - VarKind::ExplodedSet { .. } => Err(SymbolicError::Unsupported( - "set variable assignment in effect".into(), - )), + VarKind::ExplodedSet { lo, hi } => { + let lo = *lo; + let hi = *hi; + let flags = enc.encode_as_set(rhs, lo, hi)?; + let mut conjuncts = Vec::new(); + for (i, flag) in flags.iter().enumerate() { + let nb = next_vars[i].as_bool().unwrap(); + conjuncts.push(nb.eq(flag)); + } + Ok(Bool::and(&conjuncts)) + } } }