diff --git a/specl/crates/specl-cli/src/main.rs b/specl/crates/specl-cli/src/main.rs index ace9fdb..7b5ee72 100644 --- a/specl/crates/specl-cli/src/main.rs +++ b/specl/crates/specl-cli/src/main.rs @@ -176,6 +176,10 @@ enum Commands { #[arg(long)] smart: bool, + /// Maximum sequence length for symbolic Seq[T] variables (default: 5) + #[arg(long, default_value = "5")] + seq_bound: usize, + /// Show verbose output #[arg(short, long)] verbose: bool, @@ -279,10 +283,20 @@ fn main() { k_induction, ic3, smart, + seq_bound, verbose, } => { if symbolic || inductive || k_induction.is_some() || ic3 || smart { - cmd_check_symbolic(&file, &constant, depth, inductive, k_induction, ic3, smart) + cmd_check_symbolic( + &file, + &constant, + depth, + inductive, + k_induction, + ic3, + smart, + seq_bound, + ) } else { cmd_check( &file, @@ -505,6 +519,7 @@ fn cmd_check_symbolic( k_induction: Option, ic3: bool, smart: bool, + seq_bound: usize, ) -> CliResult<()> { let filename = file.display().to_string(); let source = Arc::new(fs::read_to_string(file).map_err(|e| CliError::IoError { @@ -539,6 +554,7 @@ fn cmd_check_symbolic( SymbolicMode::Bmc }, depth, + seq_bound, }; let mode_str = if smart { diff --git a/specl/crates/specl-symbolic/src/bmc.rs b/specl/crates/specl-symbolic/src/bmc.rs index 0533599..15b66eb 100644 --- a/specl/crates/specl-symbolic/src/bmc.rs +++ b/specl/crates/specl-symbolic/src/bmc.rs @@ -15,10 +15,11 @@ pub fn check_bmc( spec: &CompiledSpec, consts: &[Value], max_depth: usize, + seq_bound: usize, ) -> SymbolicResult { info!(depth = max_depth, "starting symbolic BMC"); - let layout = VarLayout::from_spec(spec, consts)?; + let layout = VarLayout::from_spec(spec, consts, seq_bound)?; let solver = Solver::new(); // Create Z3 variables for steps 0..=max_depth @@ -54,6 +55,8 @@ pub fn check_bmc( next_step: k, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_encoded = enc.encode_bool(&inv.body)?; diff --git a/specl/crates/specl-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index c8636ca..cdf245e 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -21,6 +21,12 @@ pub struct EncoderCtx<'a> { pub params: &'a [Dynamic], /// Local variable stack (for Let/Forall/Exists bindings). pub locals: Vec, + /// Compound locals: tracks locals bound to compound dict values (e.g., d[k] where d is Dict[Range, Seq]). + /// Each entry: (abs_depth, var_idx, step, key_z3) where abs_depth is the locals stack position. + pub compound_locals: Vec<(usize, usize, usize, Int)>, + /// Set locals: maps absolute locals stack position → concrete set members. + /// Used for powerset quantifier bindings where the local represents a concrete subset. + pub set_locals: Vec<(usize, Vec)>, } impl<'a> EncoderCtx<'a> { @@ -107,11 +113,35 @@ impl<'a> EncoderCtx<'a> { // === Let binding === CompiledExpr::Let { value, body } => { - let val = self.encode(value)?; - self.locals.push(val); - let result = self.encode(body); - self.locals.pop(); - result + // Try to encode the value as a scalar + match self.encode(value) { + Ok(val) => { + self.locals.push(val); + let result = self.encode(body); + self.locals.pop(); + result + } + Err(_) => { + // Value might be a compound expression (e.g., d[k] where d is Dict[Range, Seq]). + // Track as a compound local. + if let Some((var_idx, step, key_z3)) = + self.try_resolve_compound_local(value) + { + // Push a dummy value to maintain local index alignment + let abs_depth = self.locals.len(); + self.locals.push(Dynamic::from_ast(&Int::from_i64(0))); + self.compound_locals + .push((abs_depth, var_idx, step, key_z3)); + let result = self.encode(body); + self.compound_locals.pop(); + self.locals.pop(); + result + } else { + // Re-raise the original error + self.encode(value).and_then(|_| unreachable!()) + } + } + } } // === Quantifiers === @@ -149,27 +179,61 @@ impl<'a> EncoderCtx<'a> { "Range expression used outside quantifier context".into(), )), + // === Seq operations === + CompiledExpr::SeqHead(inner) => self.encode_seq_head(inner), + CompiledExpr::SeqTail(_) => Err(SymbolicError::Encoding( + "SeqTail should be handled at the effect level".into(), + )), + CompiledExpr::SeqLit(_) => Err(SymbolicError::Encoding( + "SeqLit should be handled at the init/effect level".into(), + )), + CompiledExpr::Slice { .. } => Err(SymbolicError::Encoding( + "Slice should be handled at the effect level".into(), + )), + + // === Choose === + CompiledExpr::Choose { domain, predicate } => self.encode_choose(domain, predicate), + + // === Keys/Values (set-returning — error in scalar context) === + CompiledExpr::Keys(_) => Err(SymbolicError::Encoding( + "keys() returns a set; use in set context (in, len, quantifier)".into(), + )), + CompiledExpr::Values(_) => Err(SymbolicError::Encoding( + "values() returns a set; use in set context (in, len, quantifier)".into(), + )), + // === Unsupported === - CompiledExpr::SeqLit(_) - | CompiledExpr::SeqHead(_) - | CompiledExpr::SeqTail(_) - | CompiledExpr::Slice { .. } - | CompiledExpr::Powerset(_) - | CompiledExpr::BigUnion(_) - | CompiledExpr::Fix { .. } - | CompiledExpr::Keys(_) - | CompiledExpr::Values(_) - | CompiledExpr::Changes(_) - | CompiledExpr::Enabled(_) - | CompiledExpr::ActionCall { .. } - | CompiledExpr::Field { .. } - | CompiledExpr::RecordUpdate { .. } - | CompiledExpr::TupleLit(_) - | CompiledExpr::Call { .. } - | CompiledExpr::Choose { .. } => Err(SymbolicError::Unsupported(format!( - "{:?}", - std::mem::discriminant(expr) - ))), + CompiledExpr::Powerset(_) => Err(SymbolicError::Unsupported( + "powerset() as a value; use in quantifier context (any Q in powerset(S): ...)" + .into(), + )), + CompiledExpr::BigUnion(_) => Err(SymbolicError::Unsupported( + "union_all requires set-of-sets encoding".into(), + )), + CompiledExpr::Fix { .. } => Err(SymbolicError::Unsupported( + "fix expression requires unbounded domain".into(), + )), + CompiledExpr::Changes(_) => Err(SymbolicError::Unsupported( + "changes() is a temporal operator".into(), + )), + CompiledExpr::Enabled(_) => Err(SymbolicError::Unsupported( + "enabled() is a temporal operator".into(), + )), + CompiledExpr::ActionCall { .. } => Err(SymbolicError::Unsupported( + "action calls in expressions not supported".into(), + )), + CompiledExpr::Call { .. } => Err(SymbolicError::Unsupported( + "function calls should be inlined by the compiler; this is a bug".into(), + )), + CompiledExpr::Field { .. } => Err(SymbolicError::Unsupported( + "record field access not yet supported in symbolic mode".into(), + )), + CompiledExpr::RecordUpdate { .. } => Err(SymbolicError::Unsupported( + "record update not yet supported in symbolic mode".into(), + )), + CompiledExpr::TupleLit(_) => Err(SymbolicError::Unsupported( + "tuple literal not yet supported in symbolic mode".into(), + )), } } @@ -179,12 +243,12 @@ impl<'a> EncoderCtx<'a> { VarKind::Bool | VarKind::Int { .. } => { Ok(self.step_vars[step][specl_var_idx][0].clone()) } - VarKind::ExplodedDict { .. } | VarKind::ExplodedSet { .. } => { - Err(SymbolicError::Encoding(format!( - "dict/set variable '{}' accessed directly (use index operator)", - entry.name - ))) - } + VarKind::ExplodedDict { .. } + | VarKind::ExplodedSet { .. } + | VarKind::ExplodedSeq { .. } => Err(SymbolicError::Encoding(format!( + "compound variable '{}' accessed directly (use index/len/head operator)", + entry.name + ))), } } @@ -193,6 +257,12 @@ impl<'a> EncoderCtx<'a> { match val { Value::Bool(b) => Ok(Dynamic::from_ast(&Bool::from_bool(*b))), Value::Int(n) => Ok(Dynamic::from_ast(&Int::from_i64(*n))), + Value::String(s) => { + let id = self.layout.string_id(s).ok_or_else(|| { + SymbolicError::Encoding(format!("string constant not in table: {:?}", s)) + })?; + Ok(Dynamic::from_ast(&Int::from_i64(id))) + } _ => Err(SymbolicError::Unsupported(format!( "constant type: {:?}", val @@ -309,7 +379,9 @@ impl<'a> EncoderCtx<'a> { Ok(Dynamic::from_ast(&Bool::and(&conjuncts))) } - BinOp::Concat => Err(SymbolicError::Unsupported("sequence concat".into())), + BinOp::Concat => Err(SymbolicError::Encoding( + "sequence concat (++) should be handled at the effect level".into(), + )), } } @@ -326,6 +398,11 @@ impl<'a> EncoderCtx<'a> { return Ok(Dynamic::from_ast(&Bool::and(&conjuncts))); } + // Check if either side is a seq expression — compare len + elements + if self.is_seq_expr(left) || self.is_seq_expr(right) { + return self.encode_seq_eq(left, right); + } + let l = self.encode(left)?; let r = self.encode(right)?; if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) { @@ -358,6 +435,19 @@ impl<'a> EncoderCtx<'a> { body: &CompiledExpr, is_forall: bool, ) -> SymbolicResult { + // Powerset domain: enumerate all subsets + if let CompiledExpr::Powerset(inner) = domain { + return self.encode_powerset_quantifier(inner, body, is_forall); + } + + // Set local domain (e.g., `all a in Q` where Q is a powerset-bound local) + if let CompiledExpr::Local(idx) = domain { + if let Some(members) = self.resolve_set_local(*idx) { + let members = members.clone(); + return self.encode_set_local_quantifier(&members, body, is_forall); + } + } + let (lo, hi) = self.extract_range(domain)?; let mut conjuncts = Vec::new(); @@ -376,41 +466,162 @@ impl<'a> EncoderCtx<'a> { } } + fn encode_powerset_quantifier( + &mut self, + inner: &CompiledExpr, + body: &CompiledExpr, + is_forall: bool, + ) -> SymbolicResult { + let (lo, hi) = self.extract_range(inner)?; + let n = (hi - lo + 1) as u32; + if n > 20 { + return Err(SymbolicError::Encoding(format!( + "powerset too large: 2^{} subsets", + n + ))); + } + let num_subsets = 1u32 << n; + let mut results = Vec::new(); + + for mask in 0..num_subsets { + let members: Vec = (0..n) + .filter(|bit| mask & (1 << bit) != 0) + .map(|bit| lo + bit as i64) + .collect(); + + // Push a dummy local for the set variable + let abs_depth = self.locals.len(); + self.locals.push(Dynamic::from_ast(&Int::from_i64(0))); + self.set_locals.push((abs_depth, members)); + let result = self.encode_bool(body)?; + self.set_locals.pop(); + self.locals.pop(); + results.push(result); + } + + if is_forall { + Ok(Dynamic::from_ast(&Bool::and(&results))) + } else { + Ok(Dynamic::from_ast(&Bool::or(&results))) + } + } + + fn encode_set_local_quantifier( + &mut self, + members: &[i64], + body: &CompiledExpr, + is_forall: bool, + ) -> SymbolicResult { + if members.is_empty() { + return Ok(Dynamic::from_ast(&Bool::from_bool(is_forall))); + } + let mut results = Vec::new(); + for &val in members { + let z3_val = Dynamic::from_ast(&Int::from_i64(val)); + self.locals.push(z3_val); + let result = self.encode_bool(body)?; + self.locals.pop(); + results.push(result); + } + if is_forall { + Ok(Dynamic::from_ast(&Bool::and(&results))) + } else { + Ok(Dynamic::from_ast(&Bool::or(&results))) + } + } + + /// Resolve a Local(idx) as a set local, returning its concrete members. + fn resolve_set_local(&self, local_idx: usize) -> Option<&Vec> { + let depth = self.locals.len(); + let abs_idx = depth - 1 - local_idx; + for (abs_depth, members) in self.set_locals.iter().rev() { + if *abs_depth == abs_idx { + return Some(members); + } + } + None + } + + fn encode_choose( + &mut self, + domain: &CompiledExpr, + predicate: &CompiledExpr, + ) -> SymbolicResult { + let (lo, hi) = self.extract_range(domain)?; + // Build ITE chain: if P(lo) then lo else if P(lo+1) then lo+1 else ... else lo + let mut result = Dynamic::from_ast(&Int::from_i64(lo)); // default fallback + for val in (lo..=hi).rev() { + let z3_val = Dynamic::from_ast(&Int::from_i64(val)); + self.locals.push(z3_val); + let pred = self.encode_bool(predicate)?; + self.locals.pop(); + let val_int = Int::from_i64(val); + if let Some(ri) = result.as_int() { + result = Dynamic::from_ast(&pred.ite(&val_int, &ri)); + } + } + Ok(result) + } + fn encode_index( &mut self, base: &CompiledExpr, index: &CompiledExpr, ) -> SymbolicResult { - let (specl_var_idx, step) = match base { - CompiledExpr::Var(idx) => (*idx, self.current_step), - CompiledExpr::PrimedVar(idx) => (*idx, self.next_step), - _ => { - return Err(SymbolicError::Encoding( - "index base must be a state variable".into(), - )) + // Handle nested index: d[k][i] where d is Dict[Range, Seq[T]] + if let CompiledExpr::Index { + base: outer_base, + index: outer_key, + } = base + { + return self.encode_nested_index(outer_base, outer_key, index); + } + + // Handle Local(n)[i] for compound locals (seq within dict) + if let CompiledExpr::Local(local_idx) = base { + if let Some((var_idx, step, key_z3)) = self + .resolve_compound_local(*local_idx) + .map(|(v, s, k)| (*v, *s, k.clone())) + { + return self.encode_compound_local_index(var_idx, step, &key_z3, index); } - }; + } + let (specl_var_idx, step) = self.extract_var_step(base)?; let entry = &self.layout.entries[specl_var_idx]; match &entry.kind { - VarKind::ExplodedDict { key_lo, key_hi, .. } => { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { let key_lo = *key_lo; let key_hi = *key_hi; let z3_vars = &self.step_vars[step][specl_var_idx]; + let stride = value_kind.z3_var_count(); - if let Some(concrete_key) = self.try_concrete_int(index) { - let offset = (concrete_key - key_lo) as usize; - if offset < z3_vars.len() { - Ok(z3_vars[offset].clone()) + if stride == 1 { + // Simple value kind (Bool/Int): one var per key + if let Some(concrete_key) = self.try_concrete_int(index) { + let offset = (concrete_key - key_lo) as usize; + if offset < z3_vars.len() { + Ok(z3_vars[offset].clone()) + } else { + Err(SymbolicError::Encoding(format!( + "dict key {} out of range [{}, {}]", + concrete_key, key_lo, key_hi + ))) + } } else { - Err(SymbolicError::Encoding(format!( - "dict key {} out of range [{}, {}]", - concrete_key, key_lo, key_hi - ))) + let key_z3 = self.encode_int(index)?; + self.build_ite_chain(&key_z3, z3_vars, key_lo) } } else { - let key_z3 = self.encode_int(index)?; - self.build_ite_chain(&key_z3, z3_vars, key_lo) + // Compound value kind: d[k] is not a scalar + Err(SymbolicError::Encoding(format!( + "dict variable '{}' has compound values; use nested index (d[k][i]) or len(d[k])", + entry.name + ))) } } VarKind::ExplodedSet { lo, .. } => { @@ -428,13 +639,152 @@ impl<'a> EncoderCtx<'a> { self.build_ite_chain(&key_z3, z3_vars, lo) } } + VarKind::ExplodedSeq { max_len, .. } => { + let max_len = *max_len; + let z3_vars = &self.step_vars[step][specl_var_idx]; + let elem_vars = &z3_vars[1..1 + max_len]; + if let Some(concrete_idx) = self.try_concrete_int(index) { + let idx = concrete_idx as usize; + if idx < max_len { + Ok(elem_vars[idx].clone()) + } else { + Err(SymbolicError::Encoding(format!( + "seq index {} out of bounds (max_len {})", + concrete_idx, max_len + ))) + } + } else { + let idx_z3 = self.encode_int(index)?; + self.build_ite_chain(&idx_z3, elem_vars, 0) + } + } _ => Err(SymbolicError::Encoding(format!( - "index on non-dict/set variable '{}'", + "index on non-dict/set/seq variable '{}'", entry.name ))), } } + /// Nested index: d[k][i] where d is Dict[Range, Seq[T]]. + fn encode_nested_index( + &mut self, + dict_base: &CompiledExpr, + dict_key: &CompiledExpr, + seq_index: &CompiledExpr, + ) -> SymbolicResult { + let (var_idx, step) = self.extract_var_step(dict_base)?; + let entry = &self.layout.entries[var_idx]; + let (key_lo, key_hi, value_kind) = match &entry.kind { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => (*key_lo, *key_hi, value_kind.as_ref()), + _ => { + return Err(SymbolicError::Encoding( + "nested index requires dict base".into(), + )) + } + }; + + let stride = value_kind.z3_var_count(); + let max_len = match value_kind { + VarKind::ExplodedSeq { max_len, .. } => *max_len, + _ => { + return Err(SymbolicError::Encoding( + "nested index: dict value must be Seq".into(), + )) + } + }; + + let z3_vars = &self.step_vars[step][var_idx]; + + if let Some(concrete_key) = self.try_concrete_int(dict_key) { + // Concrete dict key: directly access the seq elements for this key + let key_offset = (concrete_key - key_lo) as usize * stride; + let elem_vars = &z3_vars[key_offset + 1..key_offset + 1 + max_len]; + if let Some(concrete_idx) = self.try_concrete_int(seq_index) { + let idx = concrete_idx as usize; + if idx < max_len { + Ok(elem_vars[idx].clone()) + } else { + Err(SymbolicError::Encoding(format!( + "seq index {} out of bounds (max_len {})", + concrete_idx, max_len + ))) + } + } else { + let idx_z3 = self.encode_int(seq_index)?; + self.build_ite_chain(&idx_z3, elem_vars, 0) + } + } else { + // Symbolic dict key: ITE chain over all keys, each resolving the seq element + let key_z3 = self.encode_int(dict_key)?; + let idx_z3 = self.encode_int(seq_index)?; + let num_keys = (key_hi - key_lo + 1) as usize; + // Build the ITE: for each possible key, get the element at seq_index + let mut result: Option = None; + for k in (0..num_keys).rev() { + let key_offset = k * stride; + let elem_vars = &z3_vars[key_offset + 1..key_offset + 1 + max_len]; + // ITE chain for seq_index within this key's elements + let elem_val = self.build_ite_chain(&idx_z3, elem_vars, 0)?; + let k_z3 = Int::from_i64(key_lo + k as i64); + let cond = key_z3.eq(&k_z3); + result = Some(match result { + None => elem_val, + Some(prev) => { + if let (Some(ei), Some(pi)) = (elem_val.as_int(), prev.as_int()) { + Dynamic::from_ast(&cond.ite(&ei, &pi)) + } else if let (Some(eb), Some(pb)) = (elem_val.as_bool(), prev.as_bool()) { + Dynamic::from_ast(&cond.ite(&eb, &pb)) + } else { + prev + } + } + }); + } + result.ok_or_else(|| SymbolicError::Encoding("empty dict for nested index".into())) + } + } + + /// len(d[k]) for Dict[Range, Seq[T]]: return the len var for the seq at key k. + fn encode_nested_len( + &mut self, + dict_base: &CompiledExpr, + dict_key: &CompiledExpr, + ) -> SymbolicResult { + let (var_idx, step) = self.extract_var_step(dict_base)?; + let entry = &self.layout.entries[var_idx]; + let (key_lo, key_hi, value_kind) = match &entry.kind { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => (*key_lo, *key_hi, value_kind.as_ref()), + _ => { + return Err(SymbolicError::Encoding( + "nested len requires dict base".into(), + )) + } + }; + + let stride = value_kind.z3_var_count(); + let z3_vars = &self.step_vars[step][var_idx]; + + if let Some(concrete_key) = self.try_concrete_int(dict_key) { + let key_offset = (concrete_key - key_lo) as usize * stride; + Ok(z3_vars[key_offset].clone()) // len var is at offset 0 within each key's stride + } else { + // Symbolic key: ITE chain over all len vars + let key_z3 = self.encode_int(dict_key)?; + let num_keys = (key_hi - key_lo + 1) as usize; + let len_vars: Vec = + (0..num_keys).map(|k| z3_vars[k * stride].clone()).collect(); + self.build_ite_chain(&key_z3, &len_vars, key_lo) + } + } + fn encode_len(&mut self, inner: &CompiledExpr) -> SymbolicResult { if let CompiledExpr::SetComprehension { element: _, @@ -468,21 +818,55 @@ impl<'a> EncoderCtx<'a> { _ => self.next_step, }; let entry = &self.layout.entries[*idx]; - if let VarKind::ExplodedSet { .. } = &entry.kind { - let z3_vars = &self.step_vars[step][*idx]; - let one = Int::from_i64(1); - let zero = Int::from_i64(0); - let terms: Vec = z3_vars - .iter() - .map(|v| v.as_bool().unwrap().ite(&one, &zero)) - .collect(); - Ok(Dynamic::from_ast(&Int::add(&terms))) + match &entry.kind { + VarKind::ExplodedSet { .. } => { + let z3_vars = &self.step_vars[step][*idx]; + let one = Int::from_i64(1); + let zero = Int::from_i64(0); + let terms: Vec = z3_vars + .iter() + .map(|v| v.as_bool().unwrap().ite(&one, &zero)) + .collect(); + Ok(Dynamic::from_ast(&Int::add(&terms))) + } + VarKind::ExplodedSeq { .. } => { + // len is the first var (offset 0) + Ok(self.step_vars[step][*idx][0].clone()) + } + _ => Err(SymbolicError::Unsupported( + "len() on non-set/seq variable".into(), + )), + } + } + // len(d[k]) for Dict[Range, Seq[T]] + CompiledExpr::Index { base, index } => self.encode_nested_len(base, index), + // len(Local(n)) for compound locals or set locals + CompiledExpr::Local(idx) => { + if let Some((var_idx, step, key_z3)) = self + .resolve_compound_local(*idx) + .map(|(v, s, k)| (*v, *s, k.clone())) + { + self.encode_compound_local_len(var_idx, step, &key_z3) + } else if let Some(members) = self.resolve_set_local(*idx) { + Ok(Dynamic::from_ast(&Int::from_i64(members.len() as i64))) } else { Err(SymbolicError::Unsupported( - "len() on non-set variable".into(), + "len() on non-compound/non-set local".into(), )) } } + // len(keys(d)) = number of keys in dict + CompiledExpr::Keys(inner) => { + if let CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) = inner.as_ref() { + let entry = &self.layout.entries[*idx]; + if let VarKind::ExplodedDict { key_lo, key_hi, .. } = &entry.kind { + return Ok(Dynamic::from_ast(&Int::from_i64(key_hi - key_lo + 1))); + } + } + Err(SymbolicError::Encoding( + "len(keys()) requires a dict variable".into(), + )) + } _ => { // Try encoding as a set expression if self.is_set_expr(inner) { @@ -607,6 +991,138 @@ impl<'a> EncoderCtx<'a> { let final_val = if negate { result.not() } else { result }; Ok(Dynamic::from_ast(&final_val)) } + // Set local membership (e.g., `a in Q` where Q is powerset-bound) + CompiledExpr::Local(idx) => { + if let Some(members) = self.resolve_set_local(*idx) { + let members = members.clone(); + let elem_z3 = self.encode_int(elem)?; + let mut disjuncts = Vec::new(); + for m in &members { + disjuncts.push(elem_z3.eq(&Int::from_i64(*m))); + } + 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)) + } else { + Err(SymbolicError::Encoding(format!( + "'in' with Local({}) is not a set local", + idx + ))) + } + } + // Powerset membership (e.g., `s in powerset({1,2,3})`) + CompiledExpr::Powerset(inner) => { + // A set is always in the powerset of its superset — encode as subset check + let (lo, hi) = self.extract_range(inner)?; + if let CompiledExpr::Var(var_idx) | CompiledExpr::PrimedVar(var_idx) = elem { + let step = match elem { + CompiledExpr::Var(_) => self.current_step, + _ => self.next_step, + }; + let entry = &self.layout.entries[*var_idx]; + if let VarKind::ExplodedSet { + lo: set_lo, + hi: set_hi, + } = &entry.kind + { + let z3_vars = &self.step_vars[step][*var_idx]; + // s in powerset(lo..hi) iff all members of s are in lo..hi + // Since s is ExplodedSet over set_lo..set_hi, check that flags + // outside lo..hi are false + let mut constraints = Vec::new(); + for (i, k) in (*set_lo..=*set_hi).enumerate() { + if k < lo || k > hi { + // This element is outside powerset range — must not be member + if let Some(b) = z3_vars[i].as_bool() { + constraints.push(b.not()); + } + } + } + let result = if constraints.is_empty() { + Bool::from_bool(true) + } else { + Bool::and(&constraints) + }; + let final_val = if negate { result.not() } else { result }; + return Ok(Dynamic::from_ast(&final_val)); + } + } + // For set locals bound by outer powerset quantifier + // `s in powerset(R)` where s is a set local is always true by construction + if let CompiledExpr::Local(idx) = elem { + if self.resolve_set_local(*idx).is_some() { + let result = Bool::from_bool(!negate); + return Ok(Dynamic::from_ast(&result)); + } + } + Err(SymbolicError::Encoding( + "'in' powerset: unsupported element expression".into(), + )) + } + // keys(d): for ExplodedDict, keys is always the full range + CompiledExpr::Keys(inner) => { + if let CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) = inner.as_ref() { + let entry = &self.layout.entries[*idx]; + if let VarKind::ExplodedDict { key_lo, key_hi, .. } = &entry.kind { + let elem_z3 = self.encode_int(elem)?; + let lo_z3 = Int::from_i64(*key_lo); + let hi_z3 = Int::from_i64(*key_hi); + let in_range = Bool::and(&[elem_z3.ge(&lo_z3), elem_z3.le(&hi_z3)]); + let final_val = if negate { in_range.not() } else { in_range }; + return Ok(Dynamic::from_ast(&final_val)); + } + } + Err(SymbolicError::Encoding( + "keys() requires a dict variable".into(), + )) + } + // values(d): v in values(d) iff exists k in key_range: d[k] == v + CompiledExpr::Values(inner) => { + if let CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) = inner.as_ref() { + let step = match inner.as_ref() { + CompiledExpr::Var(_) => self.current_step, + _ => self.next_step, + }; + let entry = &self.layout.entries[*idx]; + if let VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } = &entry.kind + { + if value_kind.z3_var_count() == 1 { + let elem_z3 = self.encode(elem)?; + let z3_vars = &self.step_vars[step][*idx]; + let mut disjuncts = Vec::new(); + for (i, _k) in (*key_lo..=*key_hi).enumerate() { + if let (Some(ei), Some(vi)) = + (elem_z3.as_int(), z3_vars[i].as_int()) + { + disjuncts.push(ei.eq(&vi)); + } else if let (Some(eb), Some(vb)) = + (elem_z3.as_bool(), z3_vars[i].as_bool()) + { + disjuncts.push(eb.eq(&vb)); + } + } + let result = if disjuncts.is_empty() { + Bool::from_bool(false) + } else { + Bool::or(&disjuncts) + }; + let final_val = if negate { result.not() } else { result }; + return Ok(Dynamic::from_ast(&final_val)); + } + } + } + Err(SymbolicError::Encoding( + "values() requires a simple-valued dict variable".into(), + )) + } _ => { // Try as a set expression with known bounds (union, intersect, etc.) if self.is_set_expr(set) { @@ -662,6 +1178,184 @@ impl<'a> EncoderCtx<'a> { Ok(Dynamic::from_ast(&Bool::and(&eqs))) } + // === Compound local helpers === + + /// Try to resolve an expression as a compound local (d[k] where d is Dict[Range, Seq]). + /// Returns Some((var_idx, step, key_z3)) on success. + fn try_resolve_compound_local(&mut self, expr: &CompiledExpr) -> Option<(usize, usize, Int)> { + if let CompiledExpr::Index { base, index } = expr { + let (var_idx, step) = match base.as_ref() { + CompiledExpr::Var(idx) => (*idx, self.current_step), + CompiledExpr::PrimedVar(idx) => (*idx, self.next_step), + _ => return None, + }; + let entry = &self.layout.entries[var_idx]; + if let VarKind::ExplodedDict { value_kind, .. } = &entry.kind { + let stride = value_kind.z3_var_count(); + if stride > 1 { + let key_z3 = self.encode_int(index).ok()?; + return Some((var_idx, step, key_z3)); + } + } + } + None + } + + /// Check if a Local(idx) resolves to a compound local. + /// Returns (var_idx, step, key_z3) if so. + fn resolve_compound_local(&self, local_idx: usize) -> Option<(&usize, &usize, &Int)> { + let depth = self.locals.len(); + let abs_idx = depth - 1 - local_idx; + for (abs_depth, var_idx, step, key_z3) in self.compound_locals.iter().rev() { + if *abs_depth == abs_idx { + return Some((var_idx, step, key_z3)); + } + } + None + } + + /// Access element `elem_idx` of a compound local (seq within dict). + fn encode_compound_local_index( + &mut self, + var_idx: usize, + step: usize, + key_z3: &Int, + elem_index: &CompiledExpr, + ) -> SymbolicResult { + let entry = &self.layout.entries[var_idx]; + if let VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } = &entry.kind + { + let stride = value_kind.z3_var_count(); + if let VarKind::ExplodedSeq { max_len, .. } = value_kind.as_ref() { + let max_len = *max_len; + let idx_z3 = self.encode_int(elem_index)?; + let z3_vars = &self.step_vars[step][var_idx]; + // Build ITE chain: for each key k, for each element index i + // if key == k && idx == i then z3_vars[k*stride + 1 + i] + let key_lo = *key_lo; + let key_hi = *key_hi; + let mut result: Option = None; + for k in (key_lo..=key_hi).rev() { + let k_offset = (k - key_lo) as usize * stride; + for i in (0..max_len).rev() { + let elem_var = z3_vars[k_offset + 1 + i].clone(); + let cond = Bool::and(&[ + &key_z3.eq(&Int::from_i64(k)), + &idx_z3.eq(&Int::from_i64(i as i64)), + ]); + result = Some(match result { + None => elem_var, + Some(prev) => { + if let (Some(ev), Some(pv)) = (elem_var.as_int(), prev.as_int()) { + Dynamic::from_ast(&cond.ite(&ev, &pv)) + } else if let (Some(ev), Some(pv)) = + (elem_var.as_bool(), prev.as_bool()) + { + Dynamic::from_ast(&cond.ite(&ev, &pv)) + } else { + return Err(SymbolicError::Encoding( + "compound local index: type mismatch".into(), + )); + } + } + }); + } + } + return result + .ok_or_else(|| SymbolicError::Encoding("empty compound local".into())); + } + } + Err(SymbolicError::Encoding( + "compound local index on non-dict-of-seq".into(), + )) + } + + /// Get the len of a compound local (seq within dict). + fn encode_compound_local_len( + &self, + var_idx: usize, + step: usize, + key_z3: &Int, + ) -> SymbolicResult { + let entry = &self.layout.entries[var_idx]; + if let VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } = &entry.kind + { + let stride = value_kind.z3_var_count(); + let z3_vars = &self.step_vars[step][var_idx]; + let num_keys = (*key_hi - *key_lo + 1) as usize; + let len_vars: Vec = + (0..num_keys).map(|k| z3_vars[k * stride].clone()).collect(); + return self.build_ite_chain(key_z3, &len_vars, *key_lo); + } + Err(SymbolicError::Encoding( + "compound local len on non-dict".into(), + )) + } + + /// Get head (first element) of a compound local (seq within dict). + fn encode_compound_local_head( + &self, + var_idx: usize, + step: usize, + key_z3: &Int, + ) -> SymbolicResult { + let entry = &self.layout.entries[var_idx]; + if let VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } = &entry.kind + { + let stride = value_kind.z3_var_count(); + let z3_vars = &self.step_vars[step][var_idx]; + let num_keys = (*key_hi - *key_lo + 1) as usize; + // elem 0 is at offset 1 within each key's stride + let head_vars: Vec = (0..num_keys) + .map(|k| z3_vars[k * stride + 1].clone()) + .collect(); + return self.build_ite_chain(key_z3, &head_vars, *key_lo); + } + Err(SymbolicError::Encoding( + "compound local head on non-dict".into(), + )) + } + + // === Seq helpers === + + fn encode_seq_head(&mut self, inner: &CompiledExpr) -> SymbolicResult { + // Handle head(d[k]) for Dict[Range, Seq[T]] + if let CompiledExpr::Index { base, index } = inner { + return self.encode_nested_index(base, index, &CompiledExpr::Int(0)); + } + // Handle head(Local(n)) for compound local + if let CompiledExpr::Local(idx) = inner { + if let Some((var_idx, step, key_z3)) = self + .resolve_compound_local(*idx) + .map(|(v, s, k)| (*v, *s, k.clone())) + { + return self.encode_compound_local_head(var_idx, step, &key_z3); + } + } + let (var_idx, step) = self.extract_var_step(inner)?; + let entry = &self.layout.entries[var_idx]; + if !matches!(entry.kind, VarKind::ExplodedSeq { .. }) { + return Err(SymbolicError::Encoding(format!( + "head() on non-seq variable '{}'", + entry.name + ))); + } + // Element 0 is at offset 1 (after len var) + Ok(self.step_vars[step][var_idx][1].clone()) + } + // === Set helpers === /// Check if an expression represents a set (for equality routing). @@ -678,6 +1372,86 @@ impl<'a> EncoderCtx<'a> { } } + // === Seq helpers === + + fn is_seq_expr(&self, expr: &CompiledExpr) -> bool { + match expr { + CompiledExpr::SeqLit(_) => true, + CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { + matches!(self.layout.entries[*idx].kind, VarKind::ExplodedSeq { .. }) + } + _ => false, + } + } + + /// Encode seq equality: `seq == []` → `len == 0`; general: `len1 == len2 ∧ elem-wise eq`. + fn encode_seq_eq( + &mut self, + left: &CompiledExpr, + right: &CompiledExpr, + ) -> SymbolicResult { + // Detect seq == [] or [] == seq + if let CompiledExpr::SeqLit(elems) = right { + if elems.is_empty() { + let len = self.encode_len(left)?; + return Ok(Dynamic::from_ast(&len.eq(&Int::from_i64(0)))); + } + } + if let CompiledExpr::SeqLit(elems) = left { + if elems.is_empty() { + let len = self.encode_len(right)?; + return Ok(Dynamic::from_ast(&len.eq(&Int::from_i64(0)))); + } + } + + // General case: get both seq vars and compare len + elements + let (l_idx, l_step) = self.extract_var_step(left)?; + let (r_idx, r_step) = self.extract_var_step(right)?; + let l_kind = &self.layout.entries[l_idx].kind; + let r_kind = &self.layout.entries[r_idx].kind; + let max_len = match (l_kind, r_kind) { + ( + VarKind::ExplodedSeq { max_len: ml, .. }, + VarKind::ExplodedSeq { max_len: mr, .. }, + ) => (*ml).min(*mr), + _ => { + return Err(SymbolicError::Encoding( + "seq equality requires two sequence variables".into(), + )); + } + }; + + let l_vars = &self.step_vars[l_step][l_idx]; + let r_vars = &self.step_vars[r_step][r_idx]; + + let mut conjuncts = Vec::new(); + // len equality + let l_len = l_vars[0].as_int().unwrap(); + let r_len = r_vars[0].as_int().unwrap(); + conjuncts.push(l_len.eq(&r_len)); + // element equality (for all positions up to max_len) + for i in 0..max_len { + let l_elem = &l_vars[1 + i]; + let r_elem = &r_vars[1 + i]; + if let (Some(li), Some(ri)) = (l_elem.as_int(), r_elem.as_int()) { + conjuncts.push(li.eq(&ri)); + } else if let (Some(lb), Some(rb)) = (l_elem.as_bool(), r_elem.as_bool()) { + conjuncts.push(lb.eq(&rb)); + } + } + Ok(Dynamic::from_ast(&Bool::and(&conjuncts))) + } + + fn extract_var_step(&self, expr: &CompiledExpr) -> SymbolicResult<(usize, usize)> { + match expr { + CompiledExpr::Var(idx) => Ok((*idx, self.current_step)), + CompiledExpr::PrimedVar(idx) => Ok((*idx, self.next_step)), + _ => Err(SymbolicError::Encoding( + "expected state variable in seq equality".into(), + )), + } + } + /// Infer set bounds from two operands (at least one must reveal bounds). fn infer_set_bounds( &mut self, @@ -928,20 +1702,12 @@ fn create_var_z3(entry: &VarEntry, step: usize) -> Vec { } => { let mut vars = Vec::new(); for k in *key_lo..=*key_hi { - match value_kind.as_ref() { - VarKind::Bool => { - vars.push(Dynamic::from_ast(&Bool::new_const(format!( - "{}_{}_s{}", - entry.name, k, step - )))); - } - _ => { - vars.push(Dynamic::from_ast(&Int::new_const(format!( - "{}_{}_s{}", - entry.name, k, step - )))); - } - } + create_vars_for_kind( + value_kind, + &format!("{}_{}", entry.name, k), + step, + &mut vars, + ); } vars } @@ -955,6 +1721,63 @@ fn create_var_z3(entry: &VarEntry, step: usize) -> Vec { } vars } + VarKind::ExplodedSeq { max_len, elem_kind } => { + let mut vars = Vec::new(); + // First var: length + vars.push(Dynamic::from_ast(&Int::new_const(format!( + "{}_len_s{}", + entry.name, step + )))); + // Element vars + for i in 0..*max_len { + create_vars_for_kind(elem_kind, &format!("{}_{}", entry.name, i), step, &mut vars); + } + vars + } + } +} + +/// Recursively create Z3 variables for a VarKind (used for compound value kinds). +fn create_vars_for_kind(kind: &VarKind, prefix: &str, step: usize, out: &mut Vec) { + match kind { + VarKind::Bool => { + out.push(Dynamic::from_ast(&Bool::new_const(format!( + "{}_s{}", + prefix, step + )))); + } + VarKind::Int { .. } => { + out.push(Dynamic::from_ast(&Int::new_const(format!( + "{}_s{}", + prefix, step + )))); + } + VarKind::ExplodedSeq { max_len, elem_kind } => { + out.push(Dynamic::from_ast(&Int::new_const(format!( + "{}_len_s{}", + prefix, step + )))); + for i in 0..*max_len { + create_vars_for_kind(elem_kind, &format!("{}_{}", prefix, i), step, out); + } + } + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { + for k in *key_lo..=*key_hi { + create_vars_for_kind(value_kind, &format!("{}_{}", prefix, k), step, out); + } + } + VarKind::ExplodedSet { lo, hi } => { + for k in *lo..=*hi { + out.push(Dynamic::from_ast(&Bool::new_const(format!( + "{}_{}_s{}", + prefix, k, step + )))); + } + } } } @@ -982,9 +1805,28 @@ fn assert_var_range(solver: &Solver, kind: &VarKind, z3_vars: &[Dynamic]) { solver.assert(&z3_vars[0].as_int().unwrap().le(&z3_hi)); } } - VarKind::ExplodedDict { value_kind, .. } => { - for var in z3_vars { - assert_var_range(solver, value_kind, &[var.clone()]); + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { + let stride = value_kind.z3_var_count(); + let num_keys = (*key_hi - *key_lo + 1) as usize; + for k in 0..num_keys { + let start = k * stride; + assert_var_range(solver, value_kind, &z3_vars[start..start + stride]); + } + } + VarKind::ExplodedSeq { max_len, elem_kind } => { + // len bounded: 0 <= len <= max_len + let len_var = z3_vars[0].as_int().unwrap(); + solver.assert(&len_var.ge(&Int::from_i64(0))); + solver.assert(&len_var.le(&Int::from_i64(*max_len as i64))); + // Element range constraints + let elem_stride = elem_kind.z3_var_count(); + for i in 0..*max_len { + let start = 1 + i * elem_stride; + assert_var_range(solver, elem_kind, &z3_vars[start..start + elem_stride]); } } VarKind::Bool | VarKind::ExplodedSet { .. } => {} diff --git a/specl/crates/specl-symbolic/src/ic3.rs b/specl/crates/specl-symbolic/src/ic3.rs index 6080713..3cabb8f 100644 --- a/specl/crates/specl-symbolic/src/ic3.rs +++ b/specl/crates/specl-symbolic/src/ic3.rs @@ -15,10 +15,14 @@ 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 { +pub fn check_ic3( + spec: &CompiledSpec, + consts: &[Value], + seq_bound: usize, +) -> SymbolicResult { info!("starting IC3/CHC verification"); - let layout = VarLayout::from_spec(spec, consts)?; + let layout = VarLayout::from_spec(spec, consts, seq_bound)?; let ctx = Context::thread_local().get_z3_context(); let fp = Fixedpoint::new(); @@ -92,6 +96,8 @@ pub fn check_ic3(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { + out.push(int_sort); // len + for _ in 0..*max_len { + collect_sorts_for_kind(elem_kind, bool_sort, int_sort, out); + } + } } } diff --git a/specl/crates/specl-symbolic/src/inductive.rs b/specl/crates/specl-symbolic/src/inductive.rs index 51f318c..b42bdf4 100644 --- a/specl/crates/specl-symbolic/src/inductive.rs +++ b/specl/crates/specl-symbolic/src/inductive.rs @@ -17,10 +17,14 @@ use z3::{SatResult, Solver}; /// /// If UNSAT, I is inductive and holds for all reachable states. /// If SAT, I is not inductive — the model gives a counterexample to induction (CTI). -pub fn check_inductive(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { +pub fn check_inductive( + spec: &CompiledSpec, + consts: &[Value], + seq_bound: usize, +) -> SymbolicResult { info!("starting inductive invariant checking"); - let layout = VarLayout::from_spec(spec, consts)?; + let layout = VarLayout::from_spec(spec, consts, seq_bound)?; let solver = Solver::new(); let step0_vars = create_step_vars(&layout, 0); @@ -44,6 +48,8 @@ pub fn check_inductive(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult< next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_at_0 = enc0.encode_bool(&inv.body)?; solver.assert(&inv_at_0); @@ -56,6 +62,8 @@ pub fn check_inductive(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult< next_step: 1, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_at_1 = enc1.encode_bool(&inv.body)?; solver.assert(&inv_at_1.not()); diff --git a/specl/crates/specl-symbolic/src/k_induction.rs b/specl/crates/specl-symbolic/src/k_induction.rs index db95b78..e0fff51 100644 --- a/specl/crates/specl-symbolic/src/k_induction.rs +++ b/specl/crates/specl-symbolic/src/k_induction.rs @@ -22,10 +22,11 @@ pub fn check_k_induction( spec: &CompiledSpec, consts: &[Value], k: usize, + seq_bound: usize, ) -> SymbolicResult { info!(k, "starting k-induction"); - let layout = VarLayout::from_spec(spec, consts)?; + let layout = VarLayout::from_spec(spec, consts, seq_bound)?; // === Base case: BMC to depth K === info!(k, "k-induction base case"); @@ -75,6 +76,8 @@ fn check_base_case( next_step: depth, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_encoded = enc.encode_bool(&inv.body)?; solver.assert(&inv_encoded.not()); @@ -146,6 +149,8 @@ fn check_inductive_step( next_step: step, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_at_step = enc.encode_bool(&inv.body)?; solver.assert(&inv_at_step); @@ -160,6 +165,8 @@ fn check_inductive_step( next_step: k, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let inv_at_k = enc_k.encode_bool(&inv.body)?; solver.assert(&inv_at_k.not()); diff --git a/specl/crates/specl-symbolic/src/lib.rs b/specl/crates/specl-symbolic/src/lib.rs index 533aa44..fae6f0d 100644 --- a/specl/crates/specl-symbolic/src/lib.rs +++ b/specl/crates/specl-symbolic/src/lib.rs @@ -64,6 +64,8 @@ pub struct TraceStep { pub struct SymbolicConfig { pub mode: SymbolicMode, pub depth: usize, + /// Maximum sequence length for Seq[T] variables (default: 5). + pub seq_bound: usize, } /// Symbolic checking mode. @@ -87,11 +89,12 @@ pub fn check( consts: &[Value], config: &SymbolicConfig, ) -> SymbolicResult { + let sb = config.seq_bound; 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), + SymbolicMode::Bmc => bmc::check_bmc(spec, consts, config.depth, sb), + SymbolicMode::Inductive => inductive::check_inductive(spec, consts, sb), + SymbolicMode::KInduction(k) => k_induction::check_k_induction(spec, consts, k, sb), + SymbolicMode::Ic3 => ic3::check_ic3(spec, consts, sb), + SymbolicMode::Smart => smart::check_smart(spec, consts, config.depth, sb), } } diff --git a/specl/crates/specl-symbolic/src/smart.rs b/specl/crates/specl-symbolic/src/smart.rs index 9b7fbcc..66b5995 100644 --- a/specl/crates/specl-symbolic/src/smart.rs +++ b/specl/crates/specl-symbolic/src/smart.rs @@ -16,10 +16,11 @@ pub fn check_smart( spec: &CompiledSpec, consts: &[Value], bmc_depth: usize, + seq_bound: usize, ) -> SymbolicResult { // 1. Try simple induction info!("smart: trying inductive checking"); - match crate::inductive::check_inductive(spec, consts)? { + match crate::inductive::check_inductive(spec, consts, seq_bound)? { SymbolicOutcome::Ok { .. } => { return Ok(SymbolicOutcome::Ok { method: "smart(inductive)", @@ -37,7 +38,7 @@ pub fn check_smart( // 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)? { + match crate::k_induction::check_k_induction(spec, consts, k, seq_bound)? { SymbolicOutcome::Ok { .. } => { return Ok(SymbolicOutcome::Ok { method: "smart(k-induction)", @@ -55,7 +56,7 @@ pub fn check_smart( // 3. Try IC3/CHC info!("smart: trying IC3/CHC"); - match crate::ic3::check_ic3(spec, consts)? { + match crate::ic3::check_ic3(spec, consts, seq_bound)? { SymbolicOutcome::Ok { .. } => { return Ok(SymbolicOutcome::Ok { method: "smart(IC3)", @@ -71,7 +72,7 @@ pub fn check_smart( // 4. Fall back to BMC info!(depth = bmc_depth, "smart: falling back to BMC"); - match crate::bmc::check_bmc(spec, consts, bmc_depth)? { + match crate::bmc::check_bmc(spec, consts, bmc_depth, seq_bound)? { SymbolicOutcome::Ok { .. } => Ok(SymbolicOutcome::Ok { method: "smart(BMC)", }), diff --git a/specl/crates/specl-symbolic/src/state_vars.rs b/specl/crates/specl-symbolic/src/state_vars.rs index fa5a510..990f76e 100644 --- a/specl/crates/specl-symbolic/src/state_vars.rs +++ b/specl/crates/specl-symbolic/src/state_vars.rs @@ -14,6 +14,8 @@ pub struct VarLayout { pub entries: Vec, /// String interning table: maps string literals to integer IDs. pub string_table: Vec, + /// Maximum sequence length for ExplodedSeq variables. + pub seq_bound: usize, } /// How a single specl variable maps to Z3 variables. @@ -42,15 +44,25 @@ pub enum VarKind { }, /// Set over bounded domain: one Z3 Bool per element. ExplodedSet { lo: i64, hi: i64 }, + /// Bounded sequence: len_var (Int) + max_len element variables. + /// Z3 layout: [len, elem_0, elem_1, ..., elem_{max_len-1}] + ExplodedSeq { + max_len: usize, + elem_kind: Box, + }, } impl VarLayout { /// Analyze a compiled spec and compute the Z3 variable layout. - pub fn from_spec(spec: &CompiledSpec, consts: &[Value]) -> SymbolicResult { + pub fn from_spec( + spec: &CompiledSpec, + consts: &[Value], + seq_bound: usize, + ) -> SymbolicResult { let string_table = build_string_table(spec); let mut entries = Vec::new(); for var in &spec.vars { - let kind = type_to_kind(&var.ty, var.index, spec, consts, &string_table)?; + let kind = type_to_kind(&var.ty, var.index, spec, consts, &string_table, seq_bound)?; entries.push(VarEntry { specl_var_idx: var.index, name: var.name.clone(), @@ -60,6 +72,7 @@ impl VarLayout { Ok(VarLayout { entries, string_table, + seq_bound, }) } @@ -78,6 +91,7 @@ fn type_to_kind( spec: &CompiledSpec, consts: &[Value], string_table: &[String], + seq_bound: usize, ) -> SymbolicResult { match ty { Type::Bool => Ok(VarKind::Bool), @@ -102,16 +116,15 @@ fn type_to_kind( }), 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)?; + let value_kind = type_to_kind_simple(val_ty, seq_bound)?; 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)?; + let value_kind = type_to_kind_simple(val_ty, seq_bound)?; Ok(VarKind::ExplodedDict { key_lo: lo, key_hi: hi, @@ -134,7 +147,6 @@ fn type_to_kind( 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 { @@ -150,6 +162,24 @@ fn type_to_kind( ))) } } + Type::Seq(elem_ty) => { + let elem_kind = type_to_kind_simple(elem_ty, seq_bound)?; + let max_len = infer_seq_max_len(var_idx, spec, consts).unwrap_or(seq_bound); + Ok(VarKind::ExplodedSeq { + max_len, + elem_kind: Box::new(elem_kind), + }) + } + Type::Tuple(elems) => Err(crate::SymbolicError::Unsupported(format!( + "Tuple type ({} elements) not yet supported in symbolic mode", + elems.len() + ))), + Type::Record(_) => Err(crate::SymbolicError::Unsupported( + "Record type not yet supported in symbolic mode".into(), + )), + Type::Option(_) => Err(crate::SymbolicError::Unsupported( + "Option[T] type not yet supported in symbolic mode".into(), + )), _ => Err(crate::SymbolicError::Unsupported(format!( "variable type: {:?}", ty @@ -158,7 +188,7 @@ fn type_to_kind( } /// Simple type_to_kind without spec/const context (for value types within containers). -fn type_to_kind_simple(ty: &Type) -> SymbolicResult { +fn type_to_kind_simple(ty: &Type, seq_bound: usize) -> SymbolicResult { match ty { Type::Bool => Ok(VarKind::Bool), Type::Int | Type::String => Ok(VarKind::Int { lo: None, hi: None }), @@ -170,6 +200,23 @@ fn type_to_kind_simple(ty: &Type) -> SymbolicResult { lo: Some(*lo), hi: Some(*hi), }), + Type::Seq(elem_ty) => { + let elem_kind = type_to_kind_simple(elem_ty, seq_bound)?; + Ok(VarKind::ExplodedSeq { + max_len: seq_bound, + elem_kind: Box::new(elem_kind), + }) + } + Type::Tuple(elems) => Err(crate::SymbolicError::Unsupported(format!( + "Tuple type ({} elements) not yet supported in symbolic mode", + elems.len() + ))), + Type::Record(_) => Err(crate::SymbolicError::Unsupported( + "Record type not yet supported in symbolic mode".into(), + )), + Type::Option(_) => Err(crate::SymbolicError::Unsupported( + "Option[T] type not yet supported in symbolic mode".into(), + )), _ => Err(crate::SymbolicError::Unsupported(format!( "value type in container: {:?}", ty @@ -428,6 +475,59 @@ impl VarKind { num_keys * value_kind.z3_var_count() } VarKind::ExplodedSet { lo, hi } => (*hi - *lo + 1) as usize, + VarKind::ExplodedSeq { max_len, elem_kind } => 1 + max_len * elem_kind.z3_var_count(), // len + elements + } + } +} + +/// Infer max sequence length from action guards (look for len(var) < K patterns). +fn infer_seq_max_len(var_idx: usize, spec: &CompiledSpec, consts: &[Value]) -> Option { + for action in &spec.actions { + if let Some(bound) = find_len_bound(&action.guard, var_idx, consts) { + return Some(bound); + } + } + None +} + +/// Walk an expression looking for `Len(Var(var_idx)) < K` or `Len(Var(var_idx)) <= K`. +fn find_len_bound(expr: &CompiledExpr, var_idx: usize, consts: &[Value]) -> Option { + match expr { + CompiledExpr::Binary { + op: specl_ir::BinOp::And, + left, + right, + } => { + find_len_bound(left, var_idx, consts).or_else(|| find_len_bound(right, var_idx, consts)) + } + // len(var) < K → max_len = K + CompiledExpr::Binary { + op: specl_ir::BinOp::Lt, + left, + right, + } => { + if is_len_of_var(left, var_idx) { + eval_const_int(right, consts).map(|k| k as usize) + } else { + None + } + } + // len(var) <= K → max_len = K + 1 + CompiledExpr::Binary { + op: specl_ir::BinOp::Le, + left, + right, + } => { + if is_len_of_var(left, var_idx) { + eval_const_int(right, consts).map(|k| (k + 1) as usize) + } else { + None + } } + _ => None, } } + +fn is_len_of_var(expr: &CompiledExpr, var_idx: usize) -> bool { + matches!(expr, CompiledExpr::Len(inner) if matches!(inner.as_ref(), CompiledExpr::Var(idx) if *idx == var_idx)) +} diff --git a/specl/crates/specl-symbolic/src/trace.rs b/specl/crates/specl-symbolic/src/trace.rs index 0bce393..bd34819 100644 --- a/specl/crates/specl-symbolic/src/trace.rs +++ b/specl/crates/specl-symbolic/src/trace.rs @@ -54,6 +54,14 @@ fn identify_action( .param_type_exprs .get(i) .and_then(|te| crate::state_vars::eval_type_expr_range(te, spec, consts)), + Type::String => { + let n = layout.string_table.len() as i64; + if n > 0 { + Some((0, n - 1)) + } else { + None + } + } _ => None, } }) @@ -112,6 +120,8 @@ fn guard_satisfied( next_step: step + 1, params: &z3_params, locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let Ok(guard) = enc.encode_bool(&action.guard) else { @@ -170,20 +180,34 @@ fn extract_state( key_hi, value_kind, } => { + let stride = value_kind.z3_var_count(); let mut pairs = Vec::new(); for (i, k) in (*key_lo..=*key_hi).enumerate() { - let val = model - .eval(&z3_vars[i], true) - .and_then(|v| { - v.as_int() - .and_then(|i| i.as_i64()) - .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()) - }) - }) - .unwrap_or_else(|| "?".to_string()); - pairs.push(format!("{}: {}", k, val)); + if stride == 1 { + let val = model + .eval(&z3_vars[i], true) + .and_then(|v| { + v.as_int() + .and_then(|i| i.as_i64()) + .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()) + }) + }) + .unwrap_or_else(|| "?".to_string()); + pairs.push(format!("{}: {}", k, val)); + } else { + // Compound value (e.g., Seq) + let key_offset = i * stride; + let key_vars = &z3_vars[key_offset..key_offset + stride]; + let val_str = format_compound_value( + model, + value_kind, + key_vars, + &layout.string_table, + ); + pairs.push(format!("{}: {}", k, val_str)); + } } format!("{{{}}}", pairs.join(", ")) } @@ -201,6 +225,30 @@ fn extract_state( } format!("{{{}}}", members.join(", ")) } + VarKind::ExplodedSeq { max_len, elem_kind } => { + let len = model + .eval(&z3_vars[0], true) + .and_then(|v| v.as_int()) + .and_then(|i| i.as_i64()) + .unwrap_or(0) as usize; + let len = len.min(*max_len); + let mut elems = Vec::new(); + for i in 0..len { + let val = model + .eval(&z3_vars[1 + i], true) + .and_then(|v| { + v.as_int() + .and_then(|i| i.as_i64()) + .map(|n| format_int_value(n, elem_kind, &layout.string_table)) + .or_else(|| { + v.as_bool().and_then(|b| b.as_bool()).map(|b| b.to_string()) + }) + }) + .unwrap_or_else(|| "?".to_string()); + elems.push(val); + } + format!("[{}]", elems.join(", ")) + } }; state.push((entry.name.clone(), value_str)); @@ -209,6 +257,42 @@ fn extract_state( state } +/// Format a compound value (e.g., Seq within a Dict). +fn format_compound_value( + model: &Model, + kind: &VarKind, + vars: &[Dynamic], + string_table: &[String], +) -> String { + match kind { + VarKind::ExplodedSeq { max_len, elem_kind } => { + let len = model + .eval(&vars[0], true) + .and_then(|v| v.as_int()) + .and_then(|i| i.as_i64()) + .unwrap_or(0) as usize; + let len = len.min(*max_len); + let mut elems = Vec::new(); + for i in 0..len { + let val = model + .eval(&vars[1 + i], true) + .and_then(|v| { + v.as_int() + .and_then(|i| i.as_i64()) + .map(|n| format_int_value(n, elem_kind, string_table)) + .or_else(|| { + v.as_bool().and_then(|b| b.as_bool()).map(|b| b.to_string()) + }) + }) + .unwrap_or_else(|| "?".to_string()); + elems.push(val); + } + format!("[{}]", elems.join(", ")) + } + _ => "?".to_string(), + } +} + /// 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 { diff --git a/specl/crates/specl-symbolic/src/transition.rs b/specl/crates/specl-symbolic/src/transition.rs index 5d12e9a..713d557 100644 --- a/specl/crates/specl-symbolic/src/transition.rs +++ b/specl/crates/specl-symbolic/src/transition.rs @@ -66,6 +66,8 @@ fn encode_init_expr( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let constraint = enc.encode_bool(expr)?; solver.assert(&constraint); @@ -86,6 +88,8 @@ fn encode_init_expr( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let constraint = enc.encode_bool(expr)?; solver.assert(&constraint); @@ -115,6 +119,8 @@ fn encode_init_assignment( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let rhs_z3 = enc.encode(rhs)?; if let (Some(vi), Some(ri)) = (z3_vars[0].as_int(), rhs_z3.as_int()) { @@ -124,9 +130,14 @@ fn encode_init_assignment( } Ok(()) } - VarKind::ExplodedDict { key_lo, key_hi, .. } => { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { let key_lo = *key_lo; let key_hi = *key_hi; + let stride = value_kind.z3_var_count(); match rhs { CompiledExpr::FnLit { domain: _, body } => { for (i, k) in (key_lo..=key_hi).enumerate() { @@ -138,21 +149,56 @@ fn encode_init_assignment( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let k_val = Dynamic::from_ast(&Int::from_i64(k)); enc.locals.push(k_val); - let body_z3 = enc.encode(body)?; - if let (Some(vi), Some(ri)) = (z3_vars[i].as_int(), body_z3.as_int()) { - solver.assert(&vi.eq(&ri)); - } else if let (Some(vb), Some(rb)) = - (z3_vars[i].as_bool(), body_z3.as_bool()) - { - solver.assert(&vb.eq(&rb)); + + if stride == 1 { + let body_z3 = enc.encode(body)?; + if let (Some(vi), Some(ri)) = (z3_vars[i].as_int(), body_z3.as_int()) { + solver.assert(&vi.eq(&ri)); + } else if let (Some(vb), Some(rb)) = + (z3_vars[i].as_bool(), body_z3.as_bool()) + { + solver.assert(&vb.eq(&rb)); + } + } else { + // Compound value: handle SeqLit + let key_offset = i * stride; + let key_vars = &z3_vars[key_offset..key_offset + stride]; + if let CompiledExpr::SeqLit(elems) = body.as_ref() { + let len_var = key_vars[0].as_int().unwrap(); + solver.assert(&len_var.eq(&Int::from_i64(elems.len() as i64))); + if let VarKind::ExplodedSeq { max_len, .. } = value_kind.as_ref() { + for (ei, elem_expr) in elems.iter().enumerate() { + if ei >= *max_len { + break; + } + let val = enc.encode(elem_expr)?; + let offset = 1 + ei; + if let (Some(vi), Some(ri)) = + (key_vars[offset].as_int(), val.as_int()) + { + solver.assert(&vi.eq(&ri)); + } else if let (Some(vb), Some(rb)) = + (key_vars[offset].as_bool(), val.as_bool()) + { + solver.assert(&vb.eq(&rb)); + } + } + } + } else { + return Err(SymbolicError::Encoding( + "Dict[Range, Seq] init body must be SeqLit".into(), + )); + } } } Ok(()) } - CompiledExpr::DictLit(pairs) => { + CompiledExpr::DictLit(pairs) if stride == 1 => { for (key_expr, val_expr) in pairs { let mut enc = EncoderCtx { layout, @@ -162,6 +208,8 @@ fn encode_init_assignment( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let key_val = enc.extract_concrete_int_helper(key_expr)?; let offset = (key_val - key_lo) as usize; @@ -191,6 +239,8 @@ fn encode_init_assignment( next_step: 0, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let flags = enc.encode_as_set(rhs, *lo, *hi)?; for (i, flag) in flags.iter().enumerate() { @@ -199,6 +249,47 @@ fn encode_init_assignment( } Ok(()) } + VarKind::ExplodedSeq { max_len, elem_kind } => { + let mut enc = EncoderCtx { + layout, + consts, + step_vars, + current_step: 0, + next_step: 0, + params: &[], + locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), + }; + match rhs { + CompiledExpr::SeqLit(elems) => { + // len = elems.len() + let len_var = z3_vars[0].as_int().unwrap(); + solver.assert(&len_var.eq(&Int::from_i64(elems.len() as i64))); + // assign each element + let elem_stride = elem_kind.z3_var_count(); + for (i, elem_expr) in elems.iter().enumerate() { + if i >= *max_len { + break; + } + let val = enc.encode(elem_expr)?; + let offset = 1 + i * elem_stride; + if let (Some(vi), Some(ri)) = (z3_vars[offset].as_int(), val.as_int()) { + solver.assert(&vi.eq(&ri)); + } else if let (Some(vb), Some(rb)) = + (z3_vars[offset].as_bool(), val.as_bool()) + { + solver.assert(&vb.eq(&rb)); + } + } + Ok(()) + } + _ => Err(SymbolicError::Encoding(format!( + "unsupported seq init rhs: {:?}", + std::mem::discriminant(rhs) + ))), + } + } } } @@ -245,6 +336,16 @@ fn encode_action( Err(SymbolicError::Unsupported("unbounded Int parameter".into())) } } + Type::String => { + let n = layout.string_table.len() as i64; + if n == 0 { + Err(SymbolicError::Encoding( + "String parameter but no strings in spec".into(), + )) + } else { + Ok((0, n - 1)) + } + } _ => Err(SymbolicError::Unsupported(format!( "parameter type: {:?}", ty @@ -261,6 +362,8 @@ fn encode_action( next_step: step + 1, params: &[], locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let guard = enc.encode_bool(&action.guard)?; @@ -287,6 +390,8 @@ fn encode_action( next_step: step + 1, params: &z3_params, locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; let guard = enc.encode_bool(&action.guard)?; @@ -334,6 +439,8 @@ fn encode_effect( next_step: step + 1, params, locals: Vec::new(), + compound_locals: Vec::new(), + set_locals: Vec::new(), }; encode_effect_expr(&action.effect, &mut enc, layout, step_vars, step) @@ -406,9 +513,14 @@ fn encode_primed_assignment( )) } } - VarKind::ExplodedDict { key_lo, key_hi, .. } => { + VarKind::ExplodedDict { + key_lo, + key_hi, + value_kind, + } => { let key_lo = *key_lo; let key_hi = *key_hi; + let stride = value_kind.z3_var_count(); let curr_vars = &step_vars[step][var_idx]; match rhs { @@ -416,7 +528,7 @@ fn encode_primed_assignment( base: _, key, value, - } => { + } if stride == 1 => { let mut conjuncts = Vec::new(); let key_z3 = enc.encode_int(key)?; let val_z3 = enc.encode(value)?; @@ -442,7 +554,7 @@ fn encode_primed_assignment( Ok(Bool::and(&conjuncts)) } - CompiledExpr::FnLit { domain: _, body } => { + CompiledExpr::FnLit { domain: _, body } if stride == 1 => { let mut conjuncts = Vec::new(); for (i, k) in (key_lo..=key_hi).enumerate() { let k_val = Dynamic::from_ast(&Int::from_i64(k)); @@ -461,12 +573,62 @@ fn encode_primed_assignment( Ok(Bool::and(&conjuncts)) } // Dict merge: state | { k1: v1, k2: v2, ... } - // For each key in range: next[k] = if k matches any pair key then pair value else curr[k] CompiledExpr::Binary { op: BinOp::Union, left: _, right, - } => encode_dict_merge(right, enc, next_vars, curr_vars, key_lo, key_hi), + } => { + if stride == 1 { + encode_dict_merge(right, enc, next_vars, curr_vars, key_lo, key_hi) + } else { + encode_dict_merge_compound( + right, enc, next_vars, curr_vars, key_lo, key_hi, stride, value_kind, + step_vars, step, var_idx, + ) + } + } + // FnLit with compound values (Dict[Range, Seq[T]] init) + CompiledExpr::FnLit { domain: _, body } => { + // body is evaluated per key, expecting a SeqLit + let mut conjuncts = Vec::new(); + for (i, k) in (key_lo..=key_hi).enumerate() { + let k_val = Dynamic::from_ast(&Int::from_i64(k)); + enc.locals.push(k_val); + let key_offset = i * stride; + let key_next = &next_vars[key_offset..key_offset + stride]; + if let CompiledExpr::SeqLit(elems) = body.as_ref() { + let next_len = key_next[0].as_int().unwrap(); + conjuncts.push(next_len.eq(&Int::from_i64(elems.len() as i64))); + if let VarKind::ExplodedSeq { max_len, elem_kind } = value_kind.as_ref() + { + let es = elem_kind.z3_var_count(); + for (ei, elem_expr) in elems.iter().enumerate() { + if ei >= *max_len { + break; + } + let val = enc.encode(elem_expr)?; + let offset = 1 + ei * es; + if let (Some(ni), Some(ri)) = + (key_next[offset].as_int(), val.as_int()) + { + conjuncts.push(ni.eq(&ri)); + } else if let (Some(nb), Some(rb)) = + (key_next[offset].as_bool(), val.as_bool()) + { + conjuncts.push(nb.eq(&rb)); + } + } + } + } else { + enc.locals.pop(); + return Err(SymbolicError::Encoding( + "Dict[Range, Seq] init body must be a SeqLit".into(), + )); + } + enc.locals.pop(); + } + Ok(Bool::and(&conjuncts)) + } _ => Err(SymbolicError::Encoding(format!( "unsupported dict rhs: {:?}", std::mem::discriminant(rhs) @@ -484,6 +646,161 @@ fn encode_primed_assignment( } Ok(Bool::and(&conjuncts)) } + VarKind::ExplodedSeq { max_len, elem_kind } => { + let curr_vars = &step_vars[step][var_idx]; + let elem_stride = elem_kind.z3_var_count(); + + match rhs { + CompiledExpr::SeqLit(elems) => { + let mut conjuncts = Vec::new(); + let next_len = next_vars[0].as_int().unwrap(); + conjuncts.push(next_len.eq(&Int::from_i64(elems.len() as i64))); + for (i, elem_expr) in elems.iter().enumerate() { + if i >= *max_len { + break; + } + let val = enc.encode(elem_expr)?; + let offset = 1 + i * elem_stride; + if let (Some(ni), Some(ri)) = (next_vars[offset].as_int(), val.as_int()) { + conjuncts.push(ni.eq(&ri)); + } else if let (Some(nb), Some(rb)) = + (next_vars[offset].as_bool(), val.as_bool()) + { + conjuncts.push(nb.eq(&rb)); + } + } + // Frame remaining slots + for i in elems.len()..*max_len { + let offset = 1 + i * elem_stride; + for j in 0..elem_stride { + if let (Some(ni), Some(ci)) = ( + next_vars[offset + j].as_int(), + curr_vars[offset + j].as_int(), + ) { + conjuncts.push(ni.eq(&ci)); + } else if let (Some(nb), Some(cb)) = ( + next_vars[offset + j].as_bool(), + curr_vars[offset + j].as_bool(), + ) { + conjuncts.push(nb.eq(&cb)); + } + } + } + Ok(Bool::and(&conjuncts)) + } + // SeqTail: shift left, len - 1 + CompiledExpr::SeqTail(_) => { + let mut conjuncts = Vec::new(); + let curr_len = curr_vars[0].as_int().unwrap(); + let next_len = next_vars[0].as_int().unwrap(); + conjuncts.push(next_len.eq(&Int::sub(&[&curr_len, &Int::from_i64(1)]))); + for i in 0..max_len.saturating_sub(1) { + let next_offset = 1 + i * elem_stride; + let curr_offset = 1 + (i + 1) * elem_stride; + for j in 0..elem_stride { + if let (Some(ni), Some(ci)) = ( + next_vars[next_offset + j].as_int(), + curr_vars[curr_offset + j].as_int(), + ) { + conjuncts.push(ni.eq(&ci)); + } else if let (Some(nb), Some(cb)) = ( + next_vars[next_offset + j].as_bool(), + curr_vars[curr_offset + j].as_bool(), + ) { + conjuncts.push(nb.eq(&cb)); + } + } + } + Ok(Bool::and(&conjuncts)) + } + // Concat: base ++ [val] (append single element) + CompiledExpr::Binary { + op: BinOp::Concat, + left: _, + right, + } => match right.as_ref() { + CompiledExpr::SeqLit(elems) if elems.len() == 1 => { + let mut conjuncts = Vec::new(); + let curr_len = curr_vars[0].as_int().unwrap(); + let next_len = next_vars[0].as_int().unwrap(); + conjuncts.push(next_len.eq(&Int::add(&[&curr_len, &Int::from_i64(1)]))); + let appended = enc.encode(&elems[0])?; + for j in 0..*max_len { + let offset = 1 + j * elem_stride; + let j_z3 = Int::from_i64(j as i64); + let is_append_slot = curr_len.eq(&j_z3); + for s in 0..elem_stride { + if let (Some(ni), Some(ci)) = ( + next_vars[offset + s].as_int(), + curr_vars[offset + s].as_int(), + ) { + let new_val = if s == 0 { + appended.as_int().unwrap() + } else { + ci.clone() + }; + conjuncts.push(ni.eq(&is_append_slot.ite(&new_val, &ci))); + } else if let (Some(nb), Some(cb)) = ( + next_vars[offset + s].as_bool(), + curr_vars[offset + s].as_bool(), + ) { + let new_val = if s == 0 { + appended.as_bool().unwrap() + } else { + cb.clone() + }; + conjuncts.push(nb.eq(&is_append_slot.ite(&new_val, &cb))); + } + } + } + Ok(Bool::and(&conjuncts)) + } + _ => Err(SymbolicError::Encoding( + "concat in seq effect: only `base ++ [single_elem]` is supported".into(), + )), + }, + // Slice: base[lo..hi] + CompiledExpr::Slice { base: _, lo, hi } => { + let mut conjuncts = Vec::new(); + let lo_z3 = enc.encode_int(lo)?; + let hi_z3 = enc.encode_int(hi)?; + let next_len = next_vars[0].as_int().unwrap(); + conjuncts.push(next_len.eq(&Int::sub(&[&hi_z3, &lo_z3]))); + for i in 0..*max_len { + let next_offset = 1 + i * elem_stride; + let i_z3 = Int::from_i64(i as i64); + let src_idx = Int::add(&[&lo_z3, &i_z3]); + // ITE chain over source elements + for s in 0..elem_stride { + if let Some(ni) = next_vars[next_offset + s].as_int() { + let mut val = curr_vars[1 + s].as_int().unwrap().clone(); // default: elem 0 + for j in (0..*max_len).rev() { + let src_offset = 1 + j * elem_stride; + let cond = src_idx.eq(&Int::from_i64(j as i64)); + let cv = curr_vars[src_offset + s].as_int().unwrap(); + val = cond.ite(&cv, &val); + } + conjuncts.push(ni.eq(&val)); + } else if let Some(nb) = next_vars[next_offset + s].as_bool() { + let mut val = curr_vars[1 + s].as_bool().unwrap().clone(); + for j in (0..*max_len).rev() { + let src_offset = 1 + j * elem_stride; + let cond = src_idx.eq(&Int::from_i64(j as i64)); + let cv = curr_vars[src_offset + s].as_bool().unwrap(); + val = cond.ite(&cv, &val); + } + conjuncts.push(nb.eq(&val)); + } + } + } + Ok(Bool::and(&conjuncts)) + } + _ => Err(SymbolicError::Encoding(format!( + "unsupported seq effect rhs: {:?}", + std::mem::discriminant(rhs) + ))), + } + } } } @@ -551,6 +868,204 @@ fn encode_dict_merge( Ok(Bool::and(&conjuncts)) } +/// Dict merge for compound value kinds (e.g., Dict[Range, Seq[T]]). +/// For each key k: if k is updated, encode the seq operation; otherwise frame. +#[allow(clippy::too_many_arguments)] +fn encode_dict_merge_compound( + merge_expr: &CompiledExpr, + enc: &mut EncoderCtx, + next_vars: &[Dynamic], + curr_vars: &[Dynamic], + key_lo: i64, + key_hi: i64, + stride: usize, + value_kind: &VarKind, + _step_vars: &[Vec>], + _step: usize, + _var_idx: usize, +) -> SymbolicResult { + let pairs: Vec<(&CompiledExpr, &CompiledExpr)> = match merge_expr { + CompiledExpr::DictLit(ps) => ps.iter().map(|(k, v)| (k, v)).collect(), + _ => { + return Err(SymbolicError::Encoding(format!( + "unsupported compound dict merge rhs: {:?}", + std::mem::discriminant(merge_expr) + ))); + } + }; + + let max_len = match value_kind { + VarKind::ExplodedSeq { max_len, .. } => *max_len, + _ => { + return Err(SymbolicError::Encoding( + "compound dict merge only supports Seq values".into(), + )); + } + }; + + // Encode Z3 key expressions for each update pair + let mut encoded_keys: Vec<(Int, &CompiledExpr)> = Vec::new(); + for (key_expr, val_expr) in &pairs { + let key_z3 = enc.encode_int(key_expr)?; + encoded_keys.push((key_z3, val_expr)); + } + + let mut conjuncts = Vec::new(); + + for k in key_lo..=key_hi { + let k_idx = (k - key_lo) as usize; + let key_offset = k_idx * stride; + let key_next = &next_vars[key_offset..key_offset + stride]; + let key_curr = &curr_vars[key_offset..key_offset + stride]; + let k_z3 = Int::from_i64(k); + + // Check if any update key matches this slot + // Build ITE: for each update pair, if key matches → apply operation, else frame + // With multiple update pairs, later pairs shadow earlier ones (last match wins) + // We process pairs in reverse to build nested ITEs correctly. + + // First, compute the "framed" values (copy current to next) + let frame_len = key_curr[0].as_int().unwrap(); + let mut frame_elems: Vec = Vec::new(); + for j in 0..stride { + frame_elems.push(key_curr[j].clone()); + } + + // For each update pair, compute what the updated values would be + // and build ITE selection + let mut result_vars: Vec = frame_elems; + for (pair_key, val_expr) in encoded_keys.iter().rev() { + let is_match = pair_key.eq(&k_z3); + let updated = + encode_seq_update_for_slot(enc, *val_expr, key_curr, max_len, &frame_len)?; + // ITE per var: if this key matches, use updated; else use previous result + let mut new_result = Vec::with_capacity(stride); + for j in 0..stride { + let selected = ite_dynamic(&is_match, &updated[j], &result_vars[j])?; + new_result.push(selected); + } + result_vars = new_result; + } + + // Assert next == result + for j in 0..stride { + let c = eq_dynamic(&key_next[j], &result_vars[j])?; + conjuncts.push(c); + } + } + + Ok(Bool::and(&conjuncts)) +} + +/// Encode a seq operation (append, tail, literal) for a single dict key slot. +/// Returns the updated Z3 var values (len + elements). +fn encode_seq_update_for_slot( + enc: &mut EncoderCtx, + val_expr: &CompiledExpr, + key_curr: &[Dynamic], + max_len: usize, + curr_len: &Int, +) -> SymbolicResult> { + let stride = key_curr.len(); + match val_expr { + CompiledExpr::Binary { + op: BinOp::Concat, + left: _, + right: concat_right, + } => { + // Append: base ++ [elem] + if let CompiledExpr::SeqLit(elems) = concat_right.as_ref() { + if elems.len() == 1 { + let new_len = Dynamic::from_ast(&Int::add(&[curr_len, &Int::from_i64(1)])); + let appended = enc.encode(&elems[0])?; + let mut result = vec![new_len]; + for j in 0..max_len { + let j_z3 = Int::from_i64(j as i64); + let is_append = curr_len.eq(&j_z3); + let updated = ite_dynamic(&is_append, &appended, &key_curr[1 + j])?; + result.push(updated); + } + return Ok(result); + } + } + Err(SymbolicError::Encoding( + "dict-of-seq merge: only single-element append supported".into(), + )) + } + CompiledExpr::SeqTail(_) => { + let new_len = Dynamic::from_ast(&Int::sub(&[curr_len, &Int::from_i64(1)])); + let mut result = vec![new_len]; + for i in 0..max_len.saturating_sub(1) { + result.push(key_curr[1 + (i + 1)].clone()); // shift left + } + // Last element slot: keep current (doesn't matter, beyond new len) + if max_len > 0 { + result.push(key_curr[stride - 1].clone()); + } + Ok(result) + } + CompiledExpr::SeqLit(elems) => { + let mut result = vec![Dynamic::from_ast(&Int::from_i64(elems.len() as i64))]; + for (i, elem_expr) in elems.iter().enumerate() { + if i >= max_len { + break; + } + result.push(enc.encode(elem_expr)?); + } + // Pad remaining slots with current values + while result.len() < stride { + result.push(key_curr[result.len()].clone()); + } + Ok(result) + } + CompiledExpr::If { + cond, + then_branch, + else_branch, + } => { + let cond_z3 = enc.encode_bool(cond)?; + let then_vars = + encode_seq_update_for_slot(enc, then_branch, key_curr, max_len, curr_len)?; + let else_vars = + encode_seq_update_for_slot(enc, else_branch, key_curr, max_len, curr_len)?; + let mut result = Vec::with_capacity(stride); + for i in 0..stride { + result.push(ite_dynamic(&cond_z3, &then_vars[i], &else_vars[i])?); + } + Ok(result) + } + // Index into same variable (identity/frame): just return current slot values. + // This handles patterns like `d = d | {i: d[i]}` where the value is unchanged. + CompiledExpr::Index { .. } | CompiledExpr::Local(_) => Ok(key_curr.to_vec()), + _ => Err(SymbolicError::Encoding(format!( + "unsupported seq operation in dict merge: {:?}", + std::mem::discriminant(val_expr) + ))), + } +} + +/// ITE on Dynamic values (works for both Int and Bool). +fn ite_dynamic(cond: &Bool, then_val: &Dynamic, else_val: &Dynamic) -> SymbolicResult { + if let (Some(t), Some(e)) = (then_val.as_int(), else_val.as_int()) { + Ok(Dynamic::from_ast(&cond.ite(&t, &e))) + } else if let (Some(t), Some(e)) = (then_val.as_bool(), else_val.as_bool()) { + Ok(Dynamic::from_ast(&cond.ite(&t, &e))) + } else { + Err(SymbolicError::Encoding("ite_dynamic: type mismatch".into())) + } +} + +/// Equality on Dynamic values (works for both Int and Bool). +fn eq_dynamic(a: &Dynamic, b: &Dynamic) -> SymbolicResult { + if let (Some(ai), Some(bi)) = (a.as_int(), b.as_int()) { + Ok(ai.eq(&bi)) + } else if let (Some(ab), Some(bb)) = (a.as_bool(), b.as_bool()) { + Ok(ab.eq(&bb)) + } else { + Err(SymbolicError::Encoding("eq_dynamic: type mismatch".into())) + } +} + fn encode_frame( action: &CompiledAction, layout: &VarLayout,