diff --git a/.gitignore b/.gitignore index deca35a..75bbd4c 100644 --- a/.gitignore +++ b/.gitignore @@ -24,4 +24,4 @@ MC*.out *.z3-trace -fuzz/target/ \ No newline at end of file +fuzz/target/ diff --git a/docs/src/getting-started/running-the-checker.md b/docs/src/getting-started/running-the-checker.md index 529ea04..4a18685 100644 --- a/docs/src/getting-started/running-the-checker.md +++ b/docs/src/getting-started/running-the-checker.md @@ -77,4 +77,8 @@ specl fmt spec.specl --lint # fast syntax + type + compile check specl info spec.specl -c N=3 # analyze spec: state space, estimates, tips ``` +The formatter does not yet reattach comments to the syntax tree, so to avoid +deleting them it leaves any file that contains comments unchanged (printing a +note). Comment-free files are formatted normally. + See [Advanced Commands](../model-checker/advanced-commands.md) for the full CLI reference. diff --git a/docs/src/language/functions-and-let.md b/docs/src/language/functions-and-let.md index fa57966..b1c208f 100644 --- a/docs/src/language/functions-and-let.md +++ b/docs/src/language/functions-and-let.md @@ -45,6 +45,14 @@ let b = bar(y) in a + b ``` +If the bound value itself uses the membership operator `in`, parenthesize it so +it is not read as the `let ... in` separator: + +```specl +// parenthesize the membership test in the value position +let present = (k in s) in present or not present +``` + ### In invariants ```specl diff --git a/docs/src/language/not-yet-implemented.md b/docs/src/language/not-yet-implemented.md index 8582eb4..4aea0b1 100644 --- a/docs/src/language/not-yet-implemented.md +++ b/docs/src/language/not-yet-implemented.md @@ -1,6 +1,6 @@ # Not Yet Implemented -The following features parse and type-check but are **not yet supported** by the model checker. Using them will not cause errors, but they will have no effect on verification. +The following features are **not yet supported** by the model checker. Temporal operators and fairness parse and type-check and are reported as ignored (a warning), so they have no effect on verification. `enabled`/`changes` and recursive functions are rejected with an error (see their sections below). ## Temporal operators @@ -28,7 +28,10 @@ enabled(Action) // true if Action is enabled in the current state changes(var) // true if var changes in this transition ``` -Parsed and type-checked, but not evaluated. +Not yet evaluated by the model checker. Because they have no working semantics +yet (`changes` would silently return true, `enabled` would error at runtime), +the type checker rejects them with a clear "not yet supported" error rather than +letting an invariant hold for the wrong reason. ## Module composition @@ -36,7 +39,10 @@ Parsed and type-checked, but not evaluated. ## Recursive functions -Functions cannot currently call themselves. +Functions cannot call themselves, directly or indirectly. Because functions are +inlined at their call sites during compilation, recursion is rejected with a +compile error (`recursive function ...`) rather than being silently accepted or +overflowing the stack. ## Planned future features diff --git a/docs/src/language/operators.md b/docs/src/language/operators.md index 12d15f0..5745fd3 100644 --- a/docs/src/language/operators.md +++ b/docs/src/language/operators.md @@ -57,6 +57,7 @@ | Function | Meaning | Type | |----------|---------|------| | `len(x)` | Length/size | `Seq[T] -> Int` or `Set[T] -> Int` | +| `sum(x)` | Sum of numbers | `Seq[Int] -> Int`, `Set[Int] -> Int`, or `Dict[K,Int] -> Int` (sums values) | | `head(s)` | First element | `Seq[T] -> T` | | `tail(s)` | All but first | `Seq[T] -> Seq[T]` | | `keys(d)` | Dict keys | `Dict[K,V] -> Set[K]` | diff --git a/docs/src/language/sets-and-sequences.md b/docs/src/language/sets-and-sequences.md index 20db984..0ac319f 100644 --- a/docs/src/language/sets-and-sequences.md +++ b/docs/src/language/sets-and-sequences.md @@ -23,6 +23,7 @@ Finite, unordered collections with no duplicates. | Difference | `S1 diff S2` | `Set[T]` | | Subset | `S1 subset_of S2` | `Bool` | | Size | `len(S)` | `Int` | +| Sum | `sum(S)` | sums a `Set`/`Seq` of numbers, or a dict's values, to `Int` | | Powerset | `powerset(S)` | `Set[Set[T]]` | | Flatten | `union_all(S)` | flattens `Set[Set[T]]` to `Set[T]` | diff --git a/docs/src/language/types.md b/docs/src/language/types.md index d199355..50c6412 100644 --- a/docs/src/language/types.md +++ b/docs/src/language/types.md @@ -69,6 +69,17 @@ var role: Dict[Int, Int] init { role = {p: 0 for p in 0..N} } // comprehension ``` +Keys may also be strings, for named entities instead of integer indices: + +```specl +var bal: Dict[String, 0..4] +init { bal = {"alice": 2, "bob": 2} } +``` + +The key set is fixed by `init`; iterate it with `keys(d)`. Action parameters +cannot be `String`-typed (they have no finite domain to enumerate) — quantify +over `keys(d)` instead. + See the dedicated [Dicts](./dicts.md) page for full details. ### `Option[T]` diff --git a/specl/crates/specl-cli/src/main.rs b/specl/crates/specl-cli/src/main.rs index 1ea8974..f12286e 100644 --- a/specl/crates/specl-cli/src/main.rs +++ b/specl/crates/specl-cli/src/main.rs @@ -19,7 +19,7 @@ use specl_mc::{ StateStore, }; use specl_symbolic::{SpacerProfile, SymbolicConfig, SymbolicError, SymbolicMode, SymbolicOutcome}; -use specl_syntax::{parse, pretty_print}; +use specl_syntax::parse; use std::collections::BTreeMap; use std::fs; use std::io::IsTerminal; @@ -1748,7 +1748,7 @@ fn cmd_check_ts( ); } if want_bfs { - return run_bfs_check(spec, consts, bfs_flags, None); + return run_bfs_check(spec, consts, bfs_flags, None, 0); } // Auto-select strategy @@ -1758,7 +1758,7 @@ fn cmd_check_ts( } if !auto_symbolic { - return run_bfs_check(spec, consts, bfs_flags, None); + return run_bfs_check(spec, consts, bfs_flags, None, 0); } let auto_sym_flags = SymbolicFlags { @@ -1801,7 +1801,7 @@ fn cmd_check_ts( eprintln!(); eprintln!("Symbolic checking failed. Falling back to BFS exploration..."); } - run_bfs_check(spec, consts, bfs_flags, None) + run_bfs_check(spec, consts, bfs_flags, None, 0) } /// Symbolic checking path for `.ts.json` files. @@ -1834,12 +1834,14 @@ fn run_symbolic_check_with_spec( fn cmd_check(file: &PathBuf, constants: &[String], flags: &BfsFlags) -> CliResult<()> { let (module, spec, source) = compile_spec(file)?; - if !flags.quiet { - warn_unsupported_features(&module); - } + let ignored_liveness = if !flags.quiet { + warn_unsupported_features(&module) + } else { + count_ignored_liveness(&module) + }; let consts = parse_constants(constants, &spec)?; - run_bfs_check(spec, consts, flags, Some((&source, file))) + run_bfs_check(spec, consts, flags, Some((&source, file)), ignored_liveness) } /// Shared BFS check execution: analysis, auto-enable, config, explore, render. @@ -1849,6 +1851,7 @@ fn run_bfs_check( consts: Vec, flags: &BfsFlags, source: Option<(&Arc, &PathBuf)>, + ignored_liveness: usize, ) -> CliResult<()> { let var_names: Vec = spec.vars.iter().map(|v| v.name.clone()).collect(); let action_names: Vec = spec.actions.iter().map(|a| a.name.clone()).collect(); @@ -2038,6 +2041,7 @@ fn run_bfs_check( bloom: flags.bloom, directed: flags.directed, explorer: &explorer, + ignored_liveness, }); if exit_code != 0 { @@ -2588,9 +2592,24 @@ fn filter_invariants(spec: &mut specl_ir::CompiledSpec, check_only: &[String]) - Ok(()) } +/// Count liveness/fairness declarations the checker ignores, without printing. +fn count_ignored_liveness(module: &specl_syntax::Module) -> usize { + module + .decls + .iter() + .filter(|d| { + matches!( + d, + specl_syntax::Decl::Property(_) | specl_syntax::Decl::Fairness(_) + ) + }) + .count() +} + /// Warn about unsupported liveness features (property, fairness, temporal operators). -/// These are parsed but silently ignored by the compiler/checker. -fn warn_unsupported_features(module: &specl_syntax::Module) { +/// These are parsed but silently ignored by the compiler/checker. Returns the +/// number of ignored declarations so the caller can qualify an OK verdict. +fn warn_unsupported_features(module: &specl_syntax::Module) -> usize { let mut has_properties = false; let mut has_fairness = false; let mut property_names = Vec::new(); @@ -2622,6 +2641,8 @@ fn warn_unsupported_features(module: &specl_syntax::Module) { Fairness declarations will be ignored." ); } + + property_names.len() + usize::from(has_fairness) } fn parse_constants(constants: &[String], spec: &specl_ir::CompiledSpec) -> CliResult> { @@ -3052,6 +3073,10 @@ struct BfsResultContext<'a> { bloom: bool, directed: bool, explorer: &'a Explorer, + /// Number of liveness/fairness declarations the checker ignored. When > 0 + /// and the result is OK, the verdict says it covered safety only, so an + /// ignored property is not mistaken for a passing one. + ignored_liveness: usize, } /// Render a BFS check result in the specified output format. Returns the exit code. @@ -3234,7 +3259,14 @@ fn render_text_output(ctx: BfsResultContext<'_>) -> i32 { max_depth, } => { println!(); - println!("Result: OK"); + if ctx.ignored_liveness > 0 { + println!( + "Result: OK (safety invariants only; {} liveness/fairness declaration(s) not checked)", + ctx.ignored_liveness + ); + } else { + println!("Result: OK"); + } println!( " States explored: {}", format_large_number(states_explored as u128) @@ -4104,7 +4136,15 @@ fn cmd_fmt( let module = parse(&source).map_err(|e| CliError::from_parse_error(e, source.clone(), &filename))?; - let formatted = pretty_print(&module); + // Never silently drop comments: if the file has comments the formatter + // cannot yet reattach, it is left unchanged. + let (formatted, kept_for_comments) = specl_syntax::format_or_keep(&source, &module); + if kept_for_comments && !json { + eprintln!( + "fmt: note: {} has comments, which the formatter does not yet preserve — left unchanged", + file.display() + ); + } if check { // Check mode: exit 1 if file is not already formatted diff --git a/specl/crates/specl-eval/src/bytecode.rs b/specl/crates/specl-eval/src/bytecode.rs index d068f7b..bd09d2e 100644 --- a/specl/crates/specl-eval/src/bytecode.rs +++ b/specl/crates/specl-eval/src/bytecode.rs @@ -69,6 +69,8 @@ pub enum Op { DictUpdate, /// Pop collection → push len as Int. Len, + /// Pop collection → push sum of its elements/values as Int. + Sum, /// Pop set, pop elem → push (elem in set). Contains, /// Pop set, pop elem → push (elem not in set). @@ -440,6 +442,11 @@ impl Compiler { self.compile_len(inner); } + CompiledExpr::Sum(inner) => { + self.compile(inner); + self.emit(Op::Sum); + } + CompiledExpr::If { cond, then_branch, @@ -2327,6 +2334,10 @@ fn vm_eval_inner( }; stack.push(Value::int(len)); } + Op::Sum => { + let val = pop_value(stack)?; + stack.push(Value::int(crate::eval::sum_value(&val)?)); + } Op::Contains => { let right_val = pop_value(stack)?; let elem = pop_value(stack)?; diff --git a/specl/crates/specl-eval/src/eval.rs b/specl/crates/specl-eval/src/eval.rs index d3c570d..700c16f 100644 --- a/specl/crates/specl-eval/src/eval.rs +++ b/specl/crates/specl-eval/src/eval.rs @@ -629,6 +629,8 @@ pub fn eval(expr: &CompiledExpr, ctx: &mut EvalContext) -> EvalResult { } } + CompiledExpr::Sum(inner) => Ok(Value::int(sum_value(&eval(inner, ctx)?)?)), + CompiledExpr::Keys(expr) => { let val = eval(expr, ctx)?; match val.kind() { @@ -1007,6 +1009,8 @@ pub fn eval_int(expr: &CompiledExpr, ctx: &mut EvalContext) -> EvalResult { } } + CompiledExpr::Sum(inner) => sum_value(&eval(inner, ctx)?), + CompiledExpr::If { cond, then_branch, @@ -1038,6 +1042,7 @@ pub(crate) fn is_int_expr(expr: &CompiledExpr) -> bool { expr, CompiledExpr::Int(_) | CompiledExpr::Len(_) + | CompiledExpr::Sum(_) | CompiledExpr::Binary { op: BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Div | BinOp::Mod, .. @@ -1373,6 +1378,39 @@ pub fn expect_set(val: &Value) -> EvalResult<&[Value]> { val.as_set().ok_or_else(|| type_mismatch("Set", val)) } +/// Sum the elements of a Seq/Set, or the values of a dict (Fn/IntMap/IntMap2). +/// Element/value types are checked numeric by the type checker, so every entry +/// is expected to be an Int here. +pub(crate) fn sum_value(val: &Value) -> EvalResult { + let mut total: i64 = 0; + match val.kind() { + VK::Seq(s) | VK::Set(s) => { + for v in s.iter() { + total += expect_int(v)?; + } + } + VK::IntMap(arr) => { + for v in arr.iter() { + total += expect_int(v)?; + } + } + // Flat backing store of a 2-level dict: summing all entries aggregates + // over every (outer, inner) key, which is the intended whole-dict sum. + VK::IntMap2(_inner_size, data) => { + for v in data.iter() { + total += expect_int(v)?; + } + } + VK::Fn(m) => { + for (_, v) in m.iter() { + total += expect_int(v)?; + } + } + _ => return Err(type_mismatch("Seq, Set, or Fn", val)), + } + Ok(total) +} + /// Convert an IntMap or IntMap2 value to an IntMap Arc. /// IntMap2 is dematerialized: each row becomes an IntMap value. fn dematerialize_to_intmap(val: &Value) -> Arc> { diff --git a/specl/crates/specl-ir/src/analyze.rs b/specl/crates/specl-ir/src/analyze.rs index cec7cf9..7b20392 100644 --- a/specl/crates/specl-ir/src/analyze.rs +++ b/specl/crates/specl-ir/src/analyze.rs @@ -162,10 +162,16 @@ pub fn analyze(spec: &CompiledSpec) -> SpecProfile { } None => { state_space_bound = None; - warnings.push(Warning::UnboundedType { - var: var.name.clone(), - ty: format!("{}", var.ty), - }); + // A dict with a non-range key (e.g. String) has unknown static + // size, but its keys are fixed by init, so BFS can still + // enumerate it as long as its values are bounded. Only flag a + // genuinely unbounded value leaf (Nat/Int), which forces symbolic. + if !bfs_enumerable(&var.ty) { + warnings.push(Warning::UnboundedType { + var: var.name.clone(), + ty: format!("{}", var.ty), + }); + } } } } @@ -316,6 +322,20 @@ pub fn analyze(spec: &CompiledSpec) -> SpecProfile { } /// Compute the domain size for a type. Returns None for unbounded types. +/// Whether BFS can enumerate values of this type even when its static domain +/// size is unknown. Dict keys are fixed by init, so a dict is enumerable iff its +/// value type is; unbounded scalar leaves (Nat/Int/String) are not. +fn bfs_enumerable(ty: &Type) -> bool { + match ty { + Type::Bool | Type::Range(..) => true, + Type::Nat | Type::Int | Type::String => false, + Type::Set(elem) | Type::Seq(elem) => bfs_enumerable(elem), + // Keys come from init regardless of key type; only the values vary. + Type::Fn(_key, val) => bfs_enumerable(val), + _ => false, + } +} + fn type_domain_size(ty: &Type) -> Option { match ty { Type::Bool => Some(2), @@ -446,6 +466,24 @@ mod tests { .any(|r| matches!(r, Recommendation::UseSymbolic { .. }))); } + #[test] + fn test_string_keyed_dict_not_flagged_unbounded() { + // A dict with a String key but bounded values is BFS-enumerable (keys + // are fixed by init), so it must NOT raise an unbounded-type warning + // that would force symbolic. + let spec = compile_spec( + "module Test\nvar m: Dict[String, 0..3]\ninit { m == {\"a\": 0} }\naction IncA() { require m[\"a\"] < 3; m = m | {\"a\": m[\"a\"] + 1} }\ninvariant Safe { m[\"a\"] <= 3 }" + ); + let profile = analyze(&spec); + assert!( + !profile + .warnings + .iter() + .any(|w| matches!(w, Warning::UnboundedType { .. })), + "string-keyed dict with bounded values should not be flagged unbounded" + ); + } + #[test] fn test_symmetry_recommendation() { let spec = compile_spec( diff --git a/specl/crates/specl-ir/src/compile.rs b/specl/crates/specl-ir/src/compile.rs index d6ddaca..28f067d 100644 --- a/specl/crates/specl-ir/src/compile.rs +++ b/specl/crates/specl-ir/src/compile.rs @@ -56,6 +56,10 @@ struct Compiler { action_indices: HashMap, /// User-defined function definitions (for inlining). func_defs: HashMap, + /// Names of functions currently being inlined, to detect recursion. + /// Functions are inlined at call sites, so a recursive call would otherwise + /// recurse forever and overflow the stack. + inlining: Vec, /// Current local variable stack (for let bindings, quantifiers). locals: Vec, /// Current action parameters (during action compilation). @@ -70,6 +74,7 @@ impl Compiler { const_indices: HashMap::new(), action_indices: HashMap::new(), func_defs: HashMap::new(), + inlining: Vec::new(), locals: Vec::new(), params: Vec::new(), } @@ -397,16 +402,29 @@ impl Compiler { } // Inline: wrap body in nested let bindings for each arg // func(a, b) { body } called with (x, y) becomes: - // let a = x in let b = y in body + // let a = x in let b = y in body. + // Args are compiled in the caller's context BEFORE marking + // this function as being inlined, so nested non-recursive + // use like `Min(Min(a, b), c)` is not mistaken for recursion. let compiled_args: Vec<_> = args .iter() .map(|a| self.compile_expr(a)) .collect::>()?; + // Reject recursion: reaching a call to a function whose body + // we are already inlining would never terminate. + if self.inlining.iter().any(|n| n == name) { + return Err(CompileError::Unsupported(format!( + "recursive function `{}`: functions cannot call themselves (directly or indirectly), because they are inlined at compile time", + name + ))); + } + self.inlining.push(name.clone()); // Push all params onto locals stack for param in &func_def.params { self.locals.push(param.clone()); } let body = self.compile_expr(&func_def.body)?; + self.inlining.pop(); // Pop all params for _ in &func_def.params { self.locals.pop(); @@ -605,6 +623,8 @@ impl Compiler { ExprKind::Len(expr) => CompiledExpr::Len(Box::new(self.compile_expr(expr)?)), + ExprKind::Sum(expr) => CompiledExpr::Sum(Box::new(self.compile_expr(expr)?)), + ExprKind::Keys(expr) => CompiledExpr::Keys(Box::new(self.compile_expr(expr)?)), ExprKind::Values(expr) => CompiledExpr::Values(Box::new(self.compile_expr(expr)?)), @@ -1034,6 +1054,53 @@ mod tests { use super::*; use specl_syntax::parse; + #[test] + fn test_recursive_function_is_error_not_crash() { + // Functions are inlined, so recursion must be rejected at compile time + // rather than overflowing the stack. + let source = r#" +module Rec +var xs: Seq[0..5] +init { xs == [1, 2, 3] } +func sumSeq(s) { if len(s) == 0 then 0 else head(s) + sumSeq(tail(s)) } +invariant I { sumSeq(xs) == 6 } +"#; + let module = parse(source).unwrap(); + let err = compile(&module).unwrap_err(); + assert!(format!("{err}").contains("recursive")); + } + + #[test] + fn test_nested_nonrecursive_call_is_ok() { + // Min(Min(a, b), c): the same function nested as an argument is NOT + // recursion and must compile (regression for the inlining-stack guard). + let source = r#" +module Nested +var x: 0..9 +init { x == 0 } +func Min(a, b) { if a <= b then a else b } +action Step() { require true; x = Min(Min(x, 3), 5) } +invariant I { x <= 9 } +"#; + let module = parse(source).unwrap(); + assert!(compile(&module).is_ok()); + } + + #[test] + fn test_mutually_recursive_functions_are_error() { + let source = r#" +module Mutual +var x: 0..3 +init { x == 0 } +func isEven(n) { if n == 0 then true else isOdd(n - 1) } +func isOdd(n) { if n == 0 then false else isEven(n - 1) } +invariant I { isEven(x) or isOdd(x) } +"#; + let module = parse(source).unwrap(); + let err = compile(&module).unwrap_err(); + assert!(format!("{err}").contains("recursive")); + } + #[test] fn test_compile_simple() { let source = r#" diff --git a/specl/crates/specl-ir/src/ir.rs b/specl/crates/specl-ir/src/ir.rs index aaa681b..776c648 100644 --- a/specl/crates/specl-ir/src/ir.rs +++ b/specl/crates/specl-ir/src/ir.rs @@ -221,6 +221,8 @@ pub enum CompiledExpr { SeqTail(Box), /// Length of sequence, set, or function. Len(Box), + /// Sum of a sequence/set of numbers, or of a dict's values. + Sum(Box), /// Keys of function (domain as set). Keys(Box), /// Values of function (range as set). @@ -405,6 +407,7 @@ impl CompiledExpr { f(hi); } CompiledExpr::Len(e) + | CompiledExpr::Sum(e) | CompiledExpr::Keys(e) | CompiledExpr::Values(e) | CompiledExpr::BigUnion(e) @@ -503,6 +506,9 @@ impl CompiledExpr { CompiledExpr::Len(inner) => { CompiledExpr::Len(Box::new(inner.shift_locals_inner(amount, depth))) } + CompiledExpr::Sum(inner) => { + CompiledExpr::Sum(Box::new(inner.shift_locals_inner(amount, depth))) + } CompiledExpr::If { cond, then_branch, @@ -773,6 +779,8 @@ pub fn expr_cost(expr: &CompiledExpr) -> u32 { CompiledExpr::Len(inner) | CompiledExpr::Keys(inner) | CompiledExpr::Values(inner) => { 2 + expr_cost(inner) } + // Cost scales with collection size at runtime; charge a bit more than len. + CompiledExpr::Sum(inner) => 4 + expr_cost(inner), CompiledExpr::BigUnion(inner) | CompiledExpr::Powerset(inner) => 10 + expr_cost(inner), CompiledExpr::FnUpdate { base, key, value } => { diff --git a/specl/crates/specl-lsp/src/main.rs b/specl/crates/specl-lsp/src/main.rs index 96e5418..7196148 100644 --- a/specl/crates/specl-lsp/src/main.rs +++ b/specl/crates/specl-lsp/src/main.rs @@ -3,7 +3,7 @@ use dashmap::DashMap; use ropey::Rope; use specl_syntax::{ - parse, pretty_print, ConstValue, Decl, Expr, ExprKind, Lexer, Span, Token, TokenKind, TypeExpr, + parse, ConstValue, Decl, Expr, ExprKind, Lexer, Span, Token, TokenKind, TypeExpr, }; use specl_types::check_module; use std::panic; @@ -29,10 +29,15 @@ fn safe_parse(source: &str) -> Option { } /// Format a module, catching panics from pretty printer bugs. -fn safe_pretty_print(module: &specl_syntax::Module) -> Option { +/// +/// Returns `None` (make no edit) if the source has comments the formatter cannot +/// yet preserve, so a format-on-save never deletes comments. +fn safe_pretty_print(source: &str, module: &specl_syntax::Module) -> Option { let module_ref = panic::AssertUnwindSafe(module); - match panic::catch_unwind(move || pretty_print(*module_ref)) { - Ok(s) => Some(s), + let source_ref = panic::AssertUnwindSafe(source); + match panic::catch_unwind(move || specl_syntax::format_or_keep(*source_ref, *module_ref)) { + Ok((_, kept_for_comments)) if kept_for_comments => None, + Ok((formatted, _)) => Some(formatted), Err(payload) => { let msg = panic_payload_to_string(&payload); error!("pretty printer panicked: msg={msg}"); @@ -2373,7 +2378,7 @@ impl LanguageServer for SpeclLanguageServer { return Ok(None); }; - let Some(formatted) = safe_pretty_print(&module) else { + let Some(formatted) = safe_pretty_print(&content, &module) else { return Ok(None); }; @@ -2411,7 +2416,7 @@ impl LanguageServer for SpeclLanguageServer { return Ok(None); }; - let Some(formatted) = safe_pretty_print(&module) else { + let Some(formatted) = safe_pretty_print(&content, &module) else { return Ok(None); }; @@ -2465,7 +2470,7 @@ impl LanguageServer for SpeclLanguageServer { return Ok(None); }; - let Some(formatted) = safe_pretty_print(&module) else { + let Some(formatted) = safe_pretty_print(&content, &module) else { return Ok(None); }; diff --git a/specl/crates/specl-mc/src/explorer.rs b/specl/crates/specl-mc/src/explorer.rs index 21e0868..763dcf3 100644 --- a/specl/crates/specl-mc/src/explorer.rs +++ b/specl/crates/specl-mc/src/explorer.rs @@ -44,6 +44,13 @@ pub enum CheckError { #[error("constant '{name}' not provided")] MissingConstant { name: String }, + + #[error("dict variable '{var}' is declared over {expected} keys but init produced {found}; the init block must cover the whole key domain")] + DictDomainMismatch { + var: String, + expected: usize, + found: usize, + }, } pub type CheckResult = Result; @@ -3121,6 +3128,41 @@ impl Explorer { } /// Generate all initial states satisfying the init predicate. + /// Reject dict variables whose initial value does not cover their declared + /// key domain. A `Dict[0..N, _]` must hold all keys; a partial init otherwise + /// causes out-of-range access downstream (e.g. under symmetry reduction, + /// which permutes over the full declared domain). + fn validate_dict_domains(&self, states: &[State]) -> CheckResult<()> { + use specl_types::Type; + for (i, var) in self.spec.vars.iter().enumerate() { + let expected = match &var.ty { + Type::Fn(key, _) => match key.as_ref() { + Type::Range(lo, hi) if hi >= lo => (hi - lo + 1) as usize, + _ => continue, + }, + _ => continue, + }; + for state in states { + let found = match state.vars[i].kind() { + VK::IntMap(arr) => arr.len(), + VK::IntMap2(inner_size, data) => { + Value::intmap2_outer_len(inner_size as usize, data.len()) + } + VK::Fn(m) => m.len(), + _ => continue, + }; + if found != expected { + return Err(CheckError::DictDomainMismatch { + var: var.name.clone(), + expected, + found, + }); + } + } + } + Ok(()) + } + fn generate_initial_states(&self) -> CheckResult> { // Try direct evaluation first (fast path) match generate_initial_states_direct(&self.spec, &self.consts) { @@ -3129,6 +3171,7 @@ impl Explorer { count = states.len(), "generated initial states via direct evaluation" ); + self.validate_dict_domains(&states)?; // Re-fingerprint with view mask if active if let Some(ref mask) = self.view_mask { let states = states @@ -3166,6 +3209,7 @@ impl Explorer { }, ); + self.validate_dict_domains(&states)?; Ok(states) } @@ -5395,6 +5439,24 @@ action SetFlag(i: 0..9) { ); } + #[test] + fn test_partial_dict_init_is_error_not_panic() { + // bal is declared over keys 0..3 (4 keys) but init fills only 0..1 (2). + // This must be a clean error, not a panic (e.g. under symmetry). + let source = r#" +module Partial +var bal: Dict[0..3, 0..5] +init { bal == {h: 0 for h in 0..1} } +action Noop() { require true; bal = bal } +invariant I { bal[0] >= 0 } +"#; + let result = check_spec(source, vec![]); + assert!( + matches!(result, Err(CheckError::DictDomainMismatch { .. })), + "expected DictDomainMismatch, got: {result:?}" + ); + } + #[test] fn test_orbit_representatives_same_state_count() { // With orbit representatives, the same canonical states should be found diff --git a/specl/crates/specl-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index a5c757c..c97b1f0 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -195,6 +195,9 @@ impl<'a> EncoderCtx<'a> { // === Len === CompiledExpr::Len(inner) => self.encode_len(inner), + // === Sum === + CompiledExpr::Sum(inner) => self.encode_sum(inner), + // === Frame === CompiledExpr::Unchanged(var_idx) => self.encode_unchanged(*var_idx), @@ -932,6 +935,93 @@ impl<'a> EncoderCtx<'a> { } } + /// Encode `sum(...)` as a chained Z3 Add. Mirrors the finite-domain unrolling + /// used for `len`: a dict variable sums its per-key value vars, a set sums the + /// member values, and a comprehension sums the element value where the filter + /// holds. Unsupported shapes return an error so auto-routing falls back to BFS. + fn encode_sum(&mut self, inner: &CompiledExpr) -> SymbolicResult { + let zero = Int::from_i64(0); + + // sum({ x in D if P }) -> Sum over D of (P ? value(x) : 0) + if let CompiledExpr::SetComprehension { + element, + domain, + filter, + } = inner + { + let values = self.resolve_domain_values(domain)?; + let mut terms: Vec = Vec::with_capacity(values.len()); + for val in values { + 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) + }; + let elem = self.encode_int(element)?; + self.locals.pop(); + terms.push(included.ite(&elem, &zero)); + } + return Ok(Dynamic::from_ast(&if terms.is_empty() { + zero + } else { + Int::add(&terms) + })); + } + + match inner { + CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { + let step = match inner { + CompiledExpr::Var(_) => self.current_step, + _ => self.next_step, + }; + let entry = &self.layout.entries[*idx]; + match &entry.kind { + // A dict's values are one Z3 int var per key; sum them all. + VarKind::ExplodedDict { .. } => { + let z3_vars = &self.step_vars[step][*idx]; + let mut ints: Vec = Vec::with_capacity(z3_vars.len()); + for v in z3_vars { + ints.push(v.as_int().ok_or_else(|| { + SymbolicError::Encoding("sum: dict value is not an integer".into()) + })?); + } + Ok(Dynamic::from_ast(&if ints.is_empty() { + zero + } else { + Int::add(&ints) + })) + } + // A set over lo..hi is membership flags; element i has value lo+i. + VarKind::ExplodedSet { lo, .. } => { + let lo = *lo; + let z3_vars = &self.step_vars[step][*idx]; + let mut terms: Vec = Vec::with_capacity(z3_vars.len()); + for (i, v) in z3_vars.iter().enumerate() { + let b = v.as_bool().ok_or_else(|| { + SymbolicError::Encoding("sum: set flag is not a bool".into()) + })?; + let elem_val = Int::from_i64(lo + i as i64); + terms.push(b.ite(&elem_val, &zero)); + } + Ok(Dynamic::from_ast(&if terms.is_empty() { + zero + } else { + Int::add(&terms) + })) + } + _ => Err(SymbolicError::Unsupported( + "sum() on this variable kind is not supported in symbolic mode".into(), + )), + } + } + _ => Err(SymbolicError::Unsupported( + "sum() on this expression is not supported in symbolic mode".into(), + )), + } + } + fn encode_len(&mut self, inner: &CompiledExpr) -> SymbolicResult { if let CompiledExpr::SetComprehension { element: _, diff --git a/specl/crates/specl-symbolic/tests/integration.rs b/specl/crates/specl-symbolic/tests/integration.rs index ddfb869..07a9138 100644 --- a/specl/crates/specl-symbolic/tests/integration.rs +++ b/specl/crates/specl-symbolic/tests/integration.rs @@ -112,6 +112,18 @@ fn bmc_cas_register_ok() { // Inductive tests // ============================================================================ +#[test] +fn inductive_conservation_sum_ok() { + // Exercises symbolic sum() over a dict: total == sum(balances) is inductive + // and must be proven, not error or fall back. + let outcome = + run_symbolic("conservation.specl", &[("CAP", 12)], SymbolicMode::Inductive).unwrap(); + assert!( + matches!(outcome, SymbolicOutcome::Ok { .. }), + "expected Ok, got: {outcome:?}" + ); +} + #[test] fn inductive_reader_writer_ok() { let outcome = diff --git a/specl/crates/specl-syntax/src/ast.rs b/specl/crates/specl-syntax/src/ast.rs index 75c302f..424239e 100644 --- a/specl/crates/specl-syntax/src/ast.rs +++ b/specl/crates/specl-syntax/src/ast.rs @@ -343,6 +343,8 @@ pub enum ExprKind { SeqTail(Box), /// Length `len(x)` - get length of sequence, set, or function. Len(Box), + /// Sum `sum(x)` - sum of a sequence/set of numbers, or of a dict's values. + Sum(Box), /// Function keys `keys(f)` - get domain of function as set. Keys(Box), /// Function values `values(f)` - get range of function as set. diff --git a/specl/crates/specl-syntax/src/lib.rs b/specl/crates/specl-syntax/src/lib.rs index 9aae7c7..7dbfc98 100644 --- a/specl/crates/specl-syntax/src/lib.rs +++ b/specl/crates/specl-syntax/src/lib.rs @@ -9,5 +9,5 @@ pub mod token; pub use ast::*; pub use lexer::Lexer; pub use parser::{parse, ParseError, Parser}; -pub use pretty::{pretty_print, pretty_print_expr, pretty_print_type}; +pub use pretty::{format_or_keep, pretty_print, pretty_print_expr, pretty_print_type}; pub use token::{Span, Token, TokenKind}; diff --git a/specl/crates/specl-syntax/src/parser.rs b/specl/crates/specl-syntax/src/parser.rs index 9b23dd3..72cf218 100644 --- a/specl/crates/specl-syntax/src/parser.rs +++ b/specl/crates/specl-syntax/src/parser.rs @@ -944,6 +944,14 @@ impl Parser { let span = start.merge(self.prev_span()); Ok(Expr::new(ExprKind::Len(Box::new(expr)), span)) } + TokenKind::Sum => { + self.advance(); + self.expect(TokenKind::LParen)?; + let expr = self.parse_expr()?; + self.expect(TokenKind::RParen)?; + let span = start.merge(self.prev_span()); + Ok(Expr::new(ExprKind::Sum(Box::new(expr)), span)) + } TokenKind::Keys => { self.advance(); self.expect(TokenKind::LParen)?; diff --git a/specl/crates/specl-syntax/src/pretty.rs b/specl/crates/specl-syntax/src/pretty.rs index b2c5401..9439d73 100644 --- a/specl/crates/specl-syntax/src/pretty.rs +++ b/specl/crates/specl-syntax/src/pretty.rs @@ -1,6 +1,8 @@ //! Pretty printer for the Specl AST. use crate::ast::*; +use crate::lexer::Lexer; +use crate::token::TokenKind; use std::fmt::Write; /// Pretty print a module to a string. @@ -10,6 +12,38 @@ pub fn pretty_print(module: &Module) -> String { printer.output } +/// The text of every comment in `source`, in source order. +fn collect_comment_texts(source: &str) -> Vec { + Lexer::new(source) + .tokenize() + .into_iter() + .filter_map(|t| match t.kind { + TokenKind::Comment(s) | TokenKind::DocComment(s) => Some(s), + _ => None, + }) + .collect() +} + +/// Format `module`, but never silently drop a comment. +/// +/// The formatter is AST-based and the parser discards comments as trivia, so +/// pretty-printing a spec that has comments would delete them. Until comments +/// are reattached to the AST, this guard returns the original `source` unchanged +/// whenever formatting would lose a comment. The returned bool is `true` when the +/// original was kept for this reason (i.e. the file was not reformatted). +pub fn format_or_keep(source: &str, module: &Module) -> (String, bool) { + let formatted = pretty_print(module); + let mut before = collect_comment_texts(source); + let mut after = collect_comment_texts(&formatted); + before.sort(); + after.sort(); + if before == after { + (formatted, false) + } else { + (source.to_string(), true) + } +} + /// Pretty print an expression to a string. pub fn pretty_print_expr(expr: &Expr) -> String { let mut printer = PrettyPrinter::new(); @@ -528,6 +562,11 @@ impl PrettyPrinter { self.print_expr(expr); self.write(")"); } + ExprKind::Sum(expr) => { + self.write("sum("); + self.print_expr(expr); + self.write(")"); + } ExprKind::Keys(expr) => { self.write("keys("); self.print_expr(expr); @@ -626,6 +665,26 @@ mod tests { assert_eq!(p1, p2, "roundtrip mismatch:\nfirst:\n{p1}\nsecond:\n{p2}"); } + #[test] + fn test_format_or_keep_preserves_comments() { + // A file with comments is left unchanged (kept) rather than having its + // comments deleted by the formatter. + let source = "module Test // trailing\n// leading\nvar x: Nat\ninit { x == 0 }"; + let module = parse(source).unwrap(); + let (out, kept) = format_or_keep(source, &module); + assert!(kept, "file with comments should be kept"); + assert_eq!(out, source, "kept output must equal the original source"); + } + + #[test] + fn test_format_or_keep_formats_when_no_comments() { + let source = "module Test\nvar x:Nat\ninit{x==0}"; + let module = parse(source).unwrap(); + let (out, kept) = format_or_keep(source, &module); + assert!(!kept, "comment-free file should be formatted, not kept"); + assert_eq!(out, pretty_print(&module)); + } + #[test] fn test_pretty_print_simple() { let source = "module Test\nvar x: Nat\ninit { x == 0 }"; diff --git a/specl/crates/specl-syntax/src/token.rs b/specl/crates/specl-syntax/src/token.rs index 5b6f85d..054b4ee 100644 --- a/specl/crates/specl-syntax/src/token.rs +++ b/specl/crates/specl-syntax/src/token.rs @@ -272,6 +272,8 @@ pub enum TokenKind { Powerset, /// `union_all` - distributed union (union of all sets in set) UnionAll, + /// `sum` - sum of a sequence/set of numbers, or of a dict's values + Sum, // === Other operators === /// `&` @@ -364,6 +366,7 @@ impl TokenKind { | TokenKind::Values | TokenKind::Powerset | TokenKind::UnionAll + | TokenKind::Sum ) } @@ -429,6 +432,7 @@ impl TokenKind { "values" => TokenKind::Values, "powerset" => TokenKind::Powerset, "union_all" => TokenKind::UnionAll, + "sum" => TokenKind::Sum, _ => return None, }) } @@ -528,6 +532,7 @@ impl fmt::Display for TokenKind { TokenKind::Values => write!(f, "values"), TokenKind::Powerset => write!(f, "powerset"), TokenKind::UnionAll => write!(f, "union_all"), + TokenKind::Sum => write!(f, "sum"), TokenKind::Ampersand => write!(f, "&"), TokenKind::Assign => write!(f, "="), TokenKind::Integer(n) => write!(f, "{}", n), diff --git a/specl/crates/specl-types/src/checker.rs b/specl/crates/specl-types/src/checker.rs index 3189f0c..92761c1 100644 --- a/specl/crates/specl-types/src/checker.rs +++ b/specl/crates/specl-types/src/checker.rs @@ -111,6 +111,16 @@ impl TypeChecker { // Bind parameters for param in &d.params { let ty = self.convert_type_expr(¶m.ty)?; + // Action parameters are enumerated over a finite domain. A + // String parameter has no such domain (it would be silently + // mis-enumerated), so reject it. String-keyed dicts are still + // supported; iterate their keys with `keys(d)` instead. + if matches!(self.env.resolve_type(&ty), Type::String) { + return Err(TypeError::Unsupported { + feature: "String-typed action parameter".to_string(), + span: param.name.span, + }); + } self.env.bind_local(param.name.name.clone(), ty); } @@ -640,7 +650,13 @@ impl TypeChecker { if self.env.lookup_var(&var.name).is_none() { return Err(TypeError::InvalidPrime { span: expr.span }); } - Type::Bool + // The model checker does not evaluate changes() yet — at runtime + // it would silently return true. Reject it rather than let an + // invariant quietly hold for the wrong reason. + return Err(TypeError::Unsupported { + feature: "changes()".to_string(), + span: expr.span, + }); } ExprKind::Enabled(action) => { @@ -651,7 +667,12 @@ impl TypeChecker { span: action.span, }); } - Type::Bool + // enabled() is not evaluated yet (it errors at runtime). Reject + // it at type-check time with a clear message instead. + return Err(TypeError::Unsupported { + feature: "enabled()".to_string(), + span: expr.span, + }); } ExprKind::SeqHead(seq_expr) => { @@ -713,6 +734,35 @@ impl TypeChecker { } } + ExprKind::Sum(expr) => { + let ty_raw = self.infer_expr(expr)?; + let ty = self.env.resolve_type(&ty_raw); + // sum aggregates the elements of a Seq/Set, or the values of a + // dict (Fn). The element/value type must be numeric. + let elem = match &ty { + Type::Seq(e) | Type::Set(e) => Some(self.env.resolve_type(e)), + Type::Fn(_, v) => Some(self.env.resolve_type(v)), + // Polymorphic func param: defer; assume numeric. + Type::Var(_) => None, + _ => { + return Err(TypeError::NotIterable { + ty, + span: expr.span, + }); + } + }; + if let Some(elem) = elem { + if !elem.is_numeric() && !matches!(elem, Type::Var(_)) { + return Err(TypeError::TypeMismatch { + expected: Type::Int, + found: elem, + span: expr.span, + }); + } + } + Type::Int + } + ExprKind::Keys(expr) => { let ty_raw = self.infer_expr(expr)?; let ty = self.env.resolve_type(&ty_raw); @@ -1104,7 +1154,14 @@ impl TypeChecker { (Type::Nat, Type::Range(lo, _)) | (Type::Range(lo, _), Type::Nat) if *lo >= 0 => { Ok(Substitution::new()) } - (Type::Range(a_lo, a_hi), Type::Range(b_lo, b_hi)) if a_lo == b_lo && a_hi == b_hi => { + // Ranges unify when one contains the other, so a narrower value + // range widens into a wider declared range (e.g. a `1..4` const used + // where a `0..8` slot is expected). This matches the existing + // looseness of Int<->Range unification, which ignores bounds + // entirely. Disjoint or partially-overlapping ranges stay an error. + (Type::Range(a_lo, a_hi), Type::Range(b_lo, b_hi)) + if (a_lo >= b_lo && a_hi <= b_hi) || (b_lo >= a_lo && b_hi <= a_hi) => + { Ok(Substitution::new()) } @@ -1238,6 +1295,118 @@ init { all x in s: x >= 0 } assert!(check(source).is_ok()); } + #[test] + fn test_string_keyed_dict_ok_but_string_param_rejected() { + // A string-keyed dict type-checks (keys come from init)... + let dict_ok = r#" +module M +var m: Dict[String, 0..3] +init { m == {"a": 0, "b": 0} } +action IncA() { require m["a"] < 3; m = m | {"a": m["a"] + 1} } +invariant I { m["a"] <= 3 } +"#; + assert!(check(dict_ok).is_ok()); + + // ...but a String-typed action parameter has no finite domain and is rejected. + let str_param = r#" +module M +var m: Dict[String, 0..3] +init { m == {"a": 0} } +action Inc(k: String) { require k in keys(m); m = m | {k: m[k] + 1} } +invariant I { m["a"] <= 3 } +"#; + assert!(matches!( + check(str_param), + Err(TypeError::Unsupported { .. }) + )); + } + + #[test] + fn test_enabled_and_changes_are_unsupported() { + // Neither is evaluated by the model checker yet; both must be rejected + // rather than silently producing a wrong value. + let changes_src = r#" +module Test +var x: Nat +init { x == 0 } +action Step() { require true; x = x + 1 } +invariant I { changes(x) } +"#; + assert!(matches!( + check(changes_src), + Err(TypeError::Unsupported { .. }) + )); + + let enabled_src = r#" +module Test +var x: Nat +init { x == 0 } +action Step() { require true; x = x + 1 } +invariant I { enabled(Step) } +"#; + assert!(matches!( + check(enabled_src), + Err(TypeError::Unsupported { .. }) + )); + } + + #[test] + fn test_subrange_widens_into_wider_range() { + // A `1..4` const used where a `0..8` dict value is expected (issue #88). + let source = r#" +module Test +const INIT: 1..4 +var wallet: Dict[0..1, 0..8] +init { wallet = {u: INIT for u in 0..1} } +"#; + assert!(check(source).is_ok()); + } + + #[test] + fn test_disjoint_ranges_still_error() { + let source = r#" +module Test +const A: 100..200 +var x: 0..3 +init { x == A } +"#; + assert!(check(source).is_err()); + } + + #[test] + fn test_sum_numeric_collections() { + // sum over a dict's values, a set, and a sequence are all Int-typed. + let source = r#" +module Test +var d: Dict[0..2, 0..10] +var s: Set[Nat] +var q: Seq[Nat] +init { sum(d) == 0 and sum(s) >= 0 and sum(q) == 0 } +"#; + assert!(check(source).is_ok()); + } + + #[test] + fn test_sum_non_numeric_is_error() { + // sum over a set of sets has a non-numeric element type. + let source = r#" +module Test +var s: Set[Set[Nat]] +init { sum(s) == 0 } +"#; + assert!(check(source).is_err()); + } + + #[test] + fn test_sum_non_collection_is_error() { + let source = r#" +module Test +var x: Nat +init { sum(x) == 0 } +"#; + assert!(check(source).is_err()); + } + #[test] fn test_action_type_check() { let source = r#" diff --git a/specl/crates/specl-types/src/error.rs b/specl/crates/specl-types/src/error.rs index 993fd91..94fe24d 100644 --- a/specl/crates/specl-types/src/error.rs +++ b/specl/crates/specl-types/src/error.rs @@ -53,6 +53,9 @@ pub enum TypeError { #[error("operands must be numeric, found {found}")] ExpectedNumeric { found: Type, span: Span }, + + #[error("`{feature}` is not yet supported by the model checker")] + Unsupported { feature: String, span: Span }, } impl TypeError { @@ -71,7 +74,8 @@ impl TypeError { | TypeError::UnificationFailure { span, .. } | TypeError::OccursCheck { span } | TypeError::ExpectedBool { span, .. } - | TypeError::ExpectedNumeric { span, .. } => *span, + | TypeError::ExpectedNumeric { span, .. } + | TypeError::Unsupported { span, .. } => *span, } } } diff --git a/specl/examples/other/conservation.specl b/specl/examples/other/conservation.specl new file mode 100644 index 0000000..526d916 --- /dev/null +++ b/specl/examples/other/conservation.specl @@ -0,0 +1,29 @@ +// Token conservation using sum() over a dict's values. +// Demonstrates the sum builtin: sum(bal) aggregates the values of the dict. +// The invariant holds because mint increments a balance and total together, +// and transfer moves value between balances without changing the total. +// Use: -c CAP=12 + +module Conservation + +const CAP: 0..30 // max total supply + +var bal: Dict[0..2, 0..30] +var total: 0..30 + +init { bal = {h: 0 for h in 0..2} and total = 0 } + +action Mint(h: 0..2, amt: 1..3) { + require total + amt <= CAP + bal = bal | {h: bal[h] + amt} + and total = total + amt +} + +action Transfer(from: 0..2, to: 0..2, amt: 1..3) { + require from != to + require bal[from] >= amt + bal = bal | {from: bal[from] - amt, to: bal[to] + amt} +} + +// Total supply always equals the sum of individual balances. +invariant Conservation { sum(bal) == total } diff --git a/specl/examples/other/string-keys.specl b/specl/examples/other/string-keys.specl new file mode 100644 index 0000000..e176448 --- /dev/null +++ b/specl/examples/other/string-keys.specl @@ -0,0 +1,28 @@ +// String-keyed dictionary: named entities as keys instead of integer indices. +// The keys are fixed by init; values vary. Accessed via string literals and via +// quantification over keys(m). (Action parameters cannot be String-typed, since +// they have no finite domain to enumerate — iterate keys(m) instead.) +// Use: No constants needed + +module StringKeys + +// Account balances keyed by name. +var bal: Dict[String, 0..4] + +init { bal == {"alice": 2, "bob": 2} } + +action AliceToBob() { + require bal["alice"] >= 1 + bal = bal | {"alice": bal["alice"] - 1, "bob": bal["bob"] + 1} +} + +action BobToAlice() { + require bal["bob"] >= 1 + bal = bal | {"bob": bal["bob"] - 1, "alice": bal["alice"] + 1} +} + +// Total is conserved across transfers (sum over a string-keyed dict). +invariant Conservation { sum(bal) == 4 } + +// Every balance stays within range, checked by quantifying over the keys. +invariant InRange { all k in keys(bal): bal[k] <= 4 }