From bfe37fde2de1849165a7b903d009796b4774a3d7 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:10:43 +0200 Subject: [PATCH 01/13] claude: feat(lang): add sum() builtin over collections Aggregates a Seq/Set of numbers, or the values of a dict, into an Int. Conservation invariants like `totalSupply == sum(balances)` were previously unwritable in core specl (only union_all existed; sums needed explicit per-index expansion). Wired through lexer, parser, pretty-printer, type checker, IR, tree-walk evaluator, and bytecode VM. The symbolic backend returns a clear error and auto-routing falls back to BFS (full Z3 sum encoding is a follow-up). Adds examples/other/conservation.specl and type-checker unit tests. --- docs/src/language/operators.md | 1 + docs/src/language/sets-and-sequences.md | 1 + specl/crates/specl-eval/src/bytecode.rs | 11 ++++ specl/crates/specl-eval/src/eval.rs | 38 +++++++++++++ specl/crates/specl-ir/src/compile.rs | 2 + specl/crates/specl-ir/src/ir.rs | 8 +++ specl/crates/specl-symbolic/src/encoder.rs | 8 +++ specl/crates/specl-syntax/src/ast.rs | 2 + specl/crates/specl-syntax/src/parser.rs | 8 +++ specl/crates/specl-syntax/src/pretty.rs | 5 ++ specl/crates/specl-syntax/src/token.rs | 5 ++ specl/crates/specl-types/src/checker.rs | 63 ++++++++++++++++++++++ specl/examples/other/conservation.specl | 29 ++++++++++ 13 files changed, 181 insertions(+) create mode 100644 specl/examples/other/conservation.specl 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/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/compile.rs b/specl/crates/specl-ir/src/compile.rs index d6ddaca..d15a798 100644 --- a/specl/crates/specl-ir/src/compile.rs +++ b/specl/crates/specl-ir/src/compile.rs @@ -605,6 +605,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)?)), 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-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index a5c757c..27416fe 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -195,6 +195,14 @@ impl<'a> EncoderCtx<'a> { // === Len === CompiledExpr::Len(inner) => self.encode_len(inner), + // === Sum === + // Summing a collection in the symbolic backend needs the element + // domain unrolled into a chained Add; not yet supported here, so + // surface a clear error and let auto-routing fall back to BFS. + CompiledExpr::Sum(_) => Err(SymbolicError::Encoding( + "sum() is not yet supported by the symbolic backend; run with --bfs (bounded types required)".into(), + )), + // === Frame === CompiledExpr::Unchanged(var_idx) => self.encode_unchanged(*var_idx), 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/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..6ac6b35 100644 --- a/specl/crates/specl-syntax/src/pretty.rs +++ b/specl/crates/specl-syntax/src/pretty.rs @@ -528,6 +528,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); 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..5eb8563 100644 --- a/specl/crates/specl-types/src/checker.rs +++ b/specl/crates/specl-types/src/checker.rs @@ -713,6 +713,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); @@ -1238,6 +1267,40 @@ init { all x in s: x >= 0 } assert!(check(source).is_ok()); } + #[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/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 } From ddd448e67ddd58f7fde8d7d9af4622d380d5ca2c Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:11:53 +0200 Subject: [PATCH 02/13] claude: fix(types): widen subrange into containing range in unify A range-typed const (e.g. `1..4`) failed to unify where a wider range was expected (e.g. a `Dict[_, 0..8]` value), though an integer literal in the same position widened fine. unify now accepts two ranges when one contains the other, matching the existing Int<->Range looseness; disjoint ranges remain an error. Fixes #88. --- specl/crates/specl-types/src/checker.rs | 32 ++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/specl/crates/specl-types/src/checker.rs b/specl/crates/specl-types/src/checker.rs index 5eb8563..3b438fe 100644 --- a/specl/crates/specl-types/src/checker.rs +++ b/specl/crates/specl-types/src/checker.rs @@ -1133,7 +1133,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()) } @@ -1267,6 +1274,29 @@ init { all x in s: x >= 0 } assert!(check(source).is_ok()); } + #[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. From 7aa30fe44e4df838c7f52c6e8feb58d1cb99d875 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:16:05 +0200 Subject: [PATCH 03/13] claude: fix(ir): reject recursive functions instead of overflowing the stack Functions are inlined at call sites, so a self- or mutually-recursive function inlined forever and aborted the process with a stack overflow. The compiler now tracks the inlining stack and returns a clear compile error on re-entry. Adds direct- and mutual-recursion regression tests. --- docs/src/language/not-yet-implemented.md | 5 ++- specl/crates/specl-ir/src/compile.rs | 46 ++++++++++++++++++++++++ specl/crates/specl-types/src/error.rs | 6 +++- 3 files changed, 55 insertions(+), 2 deletions(-) diff --git a/docs/src/language/not-yet-implemented.md b/docs/src/language/not-yet-implemented.md index 8582eb4..149af82 100644 --- a/docs/src/language/not-yet-implemented.md +++ b/docs/src/language/not-yet-implemented.md @@ -36,7 +36,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/specl/crates/specl-ir/src/compile.rs b/specl/crates/specl-ir/src/compile.rs index d15a798..bdf9e0a 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(), } @@ -395,6 +400,15 @@ impl Compiler { args.len() ))); } + // Reject recursion: inlining a function already on the + // stack would never terminate (it inlines at call sites). + 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()); // 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 @@ -407,6 +421,7 @@ impl Compiler { 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(); @@ -1036,6 +1051,37 @@ 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_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-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, } } } From d6d35102c3f8fc3e7a5a31f35dfae2f1ab26ecb7 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:18:07 +0200 Subject: [PATCH 04/13] claude: fix(types): reject enabled()/changes() instead of silent wrong value Neither is evaluated by the model checker yet: changes() silently returned true at runtime and enabled() raised an internal error. Both are now rejected at type-check time with a clear "not yet supported" message, so an invariant can't quietly hold for the wrong reason. --- docs/src/language/not-yet-implemented.md | 7 ++-- specl/crates/specl-types/src/checker.rs | 44 ++++++++++++++++++++++-- 2 files changed, 47 insertions(+), 4 deletions(-) diff --git a/docs/src/language/not-yet-implemented.md b/docs/src/language/not-yet-implemented.md index 149af82..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 diff --git a/specl/crates/specl-types/src/checker.rs b/specl/crates/specl-types/src/checker.rs index 3b438fe..819220b 100644 --- a/specl/crates/specl-types/src/checker.rs +++ b/specl/crates/specl-types/src/checker.rs @@ -640,7 +640,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 +657,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) => { @@ -1274,6 +1285,35 @@ init { all x in s: x >= 0 } assert!(check(source).is_ok()); } + #[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). From daae5943b9200aa343ada0eeedadd4e0a0a15655 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:24:41 +0200 Subject: [PATCH 05/13] claude: fix(ir): don't flag nested non-recursive calls as recursion The recursion guard pushed the function name before compiling its arguments, so a nested non-recursive call like Min(Min(a, b), c) was wrongly rejected (caught by raft.specl in the example corpus). Compile the arguments in the caller's context first, then mark the function as being inlined only around its body. --- specl/crates/specl-ir/src/compile.rs | 37 +++++++++++++++++++++------- 1 file changed, 28 insertions(+), 9 deletions(-) diff --git a/specl/crates/specl-ir/src/compile.rs b/specl/crates/specl-ir/src/compile.rs index bdf9e0a..28f067d 100644 --- a/specl/crates/specl-ir/src/compile.rs +++ b/specl/crates/specl-ir/src/compile.rs @@ -400,8 +400,18 @@ impl Compiler { args.len() ))); } - // Reject recursion: inlining a function already on the - // stack would never terminate (it inlines at call sites). + // 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. + // 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", @@ -409,13 +419,6 @@ impl Compiler { ))); } self.inlining.push(name.clone()); - // 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 compiled_args: Vec<_> = args - .iter() - .map(|a| self.compile_expr(a)) - .collect::>()?; // Push all params onto locals stack for param in &func_def.params { self.locals.push(param.clone()); @@ -1067,6 +1070,22 @@ invariant I { sumSeq(xs) == 6 } 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#" From e5871850993d8045960c53fe1f1f042d4ba8d7db Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:24:41 +0200 Subject: [PATCH 06/13] claude: feat(cli): qualify OK verdict when liveness properties are ignored The checker warned that liveness/fairness declarations are ignored but still printed a bare "Result: OK", so a skimmer could read an ignored property as a passing one. The OK line now reads "OK (safety invariants only; N liveness/fairness declaration(s) not checked)" when any were ignored. --- specl/crates/specl-cli/src/main.rs | 52 ++++++++++++++++++++++++------ 1 file changed, 42 insertions(+), 10 deletions(-) diff --git a/specl/crates/specl-cli/src/main.rs b/specl/crates/specl-cli/src/main.rs index 1ea8974..07982c0 100644 --- a/specl/crates/specl-cli/src/main.rs +++ b/specl/crates/specl-cli/src/main.rs @@ -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) From 415715ee04f515329e5a4f28c29a4f2f00707d40 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:33:47 +0200 Subject: [PATCH 07/13] claude: fix(fmt): never delete comments; leave commented files unchanged The AST-based formatter dropped every comment because the parser discards them as trivia, so `fmt --write` and the LSP format-on-save silently deleted all comments. Until comments are reattached to the syntax tree, format_or_keep() compares the comment set before and after formatting and returns the original source unchanged if any comment would be lost. The CLI prints a note; the LSP makes no edit. Comment-free files format as before. Addresses the data-loss half of #87 (full comment formatting remains open). --- .../getting-started/running-the-checker.md | 4 ++ specl/crates/specl-cli/src/main.rs | 12 ++++- specl/crates/specl-lsp/src/main.rs | 19 ++++--- specl/crates/specl-syntax/src/lib.rs | 2 +- specl/crates/specl-syntax/src/pretty.rs | 54 +++++++++++++++++++ 5 files changed, 81 insertions(+), 10 deletions(-) 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/specl/crates/specl-cli/src/main.rs b/specl/crates/specl-cli/src/main.rs index 07982c0..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; @@ -4136,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-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-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/pretty.rs b/specl/crates/specl-syntax/src/pretty.rs index 6ac6b35..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(); @@ -631,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 }"; From c03c5f5a613005a3ef30267b6c64a1716aef439f Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:33:47 +0200 Subject: [PATCH 08/13] claude: docs(lang): note parenthesizing membership `in` in let value position Document the workaround for the genuine `let x = EXPR in BODY` ambiguity (#71): parenthesize a membership test used as the bound value. --- docs/src/language/functions-and-let.md | 8 ++++++++ 1 file changed, 8 insertions(+) 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 From a11f4ef1947b66ea4c8534c001e660331d207233 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:51:58 +0200 Subject: [PATCH 09/13] claude: feat(symbolic): encode sum() over dicts, sets, and comprehensions The symbolic backend previously errored on sum() and fell back to BFS. It now unrolls sum into a chained Z3 Add: a dict sums its per-key value vars, a set sums member values, and a comprehension sums the element value where the filter holds. Conservation invariants (total == sum(balances)) over unbounded Nat are now proven inductively. Closes #92. --- specl/crates/specl-symbolic/src/encoder.rs | 94 +++++++++++++++++-- .../specl-symbolic/tests/integration.rs | 12 +++ 2 files changed, 100 insertions(+), 6 deletions(-) diff --git a/specl/crates/specl-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index 27416fe..c97b1f0 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -196,12 +196,7 @@ impl<'a> EncoderCtx<'a> { CompiledExpr::Len(inner) => self.encode_len(inner), // === Sum === - // Summing a collection in the symbolic backend needs the element - // domain unrolled into a chained Add; not yet supported here, so - // surface a clear error and let auto-routing fall back to BFS. - CompiledExpr::Sum(_) => Err(SymbolicError::Encoding( - "sum() is not yet supported by the symbolic backend; run with --bfs (bounded types required)".into(), - )), + CompiledExpr::Sum(inner) => self.encode_sum(inner), // === Frame === CompiledExpr::Unchanged(var_idx) => self.encode_unchanged(*var_idx), @@ -940,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 = From 1d0032e702cfd886b9d1136151520b611d1b65a0 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 17:56:20 +0200 Subject: [PATCH 10/13] claude: fix(mc): reject partial dict init instead of panicking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A dict whose init did not cover its declared key domain (e.g. Dict[0..5, _] filled only over 0..3) caused an out-of-bounds panic downstream — notably under symmetry reduction, which permutes over the full declared domain. The explorer now validates each dict variable's initial size against its declared key range and returns a clear DictDomainMismatch error. Closes #95. --- specl/crates/specl-mc/src/explorer.rs | 62 +++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) 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 From 4e504b8577cca1da1ecd7aa579a35a6c1352b811 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 18:02:46 +0200 Subject: [PATCH 11/13] claude: feat(lang): support string-keyed dicts under BFS MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit String-keyed dicts (Dict[String, V]) were forced to the symbolic backend, which rejects non-range keys, so they could not be checked by default. Their keys are fixed by init and only the values vary, so BFS can enumerate them: analyze() no longer flags a non-range-key dict with bounded values as unbounded, and such specs auto-route to BFS. String-typed action parameters are rejected (no finite domain — previously mis-enumerated as integers); iterate keys(d) instead. Adds examples/other/string-keys.specl and unit tests. Closes #50. --- docs/src/language/types.md | 11 ++++++ specl/crates/specl-ir/src/analyze.rs | 46 ++++++++++++++++++++++--- specl/crates/specl-types/src/checker.rs | 36 +++++++++++++++++++ specl/examples/other/string-keys.specl | 28 +++++++++++++++ 4 files changed, 117 insertions(+), 4 deletions(-) create mode 100644 specl/examples/other/string-keys.specl 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-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-types/src/checker.rs b/specl/crates/specl-types/src/checker.rs index 819220b..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); } @@ -1285,6 +1295,32 @@ 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 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 } From 1793a92dbf7b4897a1ce24ce39c69d9f4285272a Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 18:10:46 +0200 Subject: [PATCH 12/13] claude: test(soundness): add cross-tool oracle vs TLC Adds specl/tools/soundness/oracle.sh: runs the same TLA+ spec through both TLC and specl (auto-translating the .tla) and asserts the verdicts agree, catching unsound results that internal-consistency tests cannot. Ships a known-OK Counter pair and reuses DieHard from the comparison benchmarks. The oracle immediately found a false-proof bug: specl's default symbolic path (IC3) reports OK on DieHard while BFS, BMC, and TLC all find the violation (filed as #96, allowlisted so the oracle stays green while guarding regressions). Closes #94. --- .gitignore | 4 +- specl/tools/soundness/README.md | 35 +++++++++ specl/tools/soundness/oracle.sh | 98 +++++++++++++++++++++++++ specl/tools/soundness/specs/Counter.cfg | 4 + specl/tools/soundness/specs/Counter.tla | 11 +++ 5 files changed, 151 insertions(+), 1 deletion(-) create mode 100644 specl/tools/soundness/README.md create mode 100755 specl/tools/soundness/oracle.sh create mode 100644 specl/tools/soundness/specs/Counter.cfg create mode 100644 specl/tools/soundness/specs/Counter.tla diff --git a/.gitignore b/.gitignore index deca35a..cfd4ada 100644 --- a/.gitignore +++ b/.gitignore @@ -24,4 +24,6 @@ MC*.out *.z3-trace -fuzz/target/ \ No newline at end of file +fuzz/target/ +# Soundness oracle: downloaded TLC jar +specl/tools/soundness/tla2tools.jar diff --git a/specl/tools/soundness/README.md b/specl/tools/soundness/README.md new file mode 100644 index 0000000..3a495c3 --- /dev/null +++ b/specl/tools/soundness/README.md @@ -0,0 +1,35 @@ +# Soundness oracle + +Specl's built-in soundness tests check *internal* consistency (storage backends +agree, parallel == sequential, parse roundtrip). They cannot catch a bug where +the whole checker reaches a wrong verdict. This oracle adds an *external* one: it +runs the same TLA+ spec through both TLC and specl and asserts they agree on +OK-vs-violation. + +## Run + +```bash +# from the repo root; java required, tla2tools.jar auto-downloaded if absent +specl/tools/soundness/oracle.sh +# or pin the tools: +SPECL=specl/target/release/specl TLA_TOOLS_JAR=/path/to/tla2tools.jar specl/tools/soundness/oracle.sh +``` + +Exit 0 if every spec agrees (or is an allowlisted known issue), 1 on a new +disagreement, 2 if a required tool is missing. + +## Specs + +Curated `.tla` + `.cfg` pairs are listed in `oracle.sh` (`SPECS`). Each must use +only scalar constants (specl's `-c` does not take set-valued constants yet) and +translate cleanly. `specs/` holds oracle-only specs; others are reused from +`specl/benchmarks/comparison/`. + +## Known issues + +`KNOWN_ISSUES` in `oracle.sh` lists specs whose disagreement is a filed bug, so +the oracle stays green while still guarding against new disagreements. Remove an +entry when its bug is fixed. + +- `DieHard` — #96: the default symbolic path (IC3) returns a false OK; BFS, BMC, + and TLC all find the violation. diff --git a/specl/tools/soundness/oracle.sh b/specl/tools/soundness/oracle.sh new file mode 100755 index 0000000..75d13da --- /dev/null +++ b/specl/tools/soundness/oracle.sh @@ -0,0 +1,98 @@ +#!/usr/bin/env bash +# Cross-tool soundness oracle: run the same TLA+ spec through both TLC and specl +# (auto-translating the .tla) and assert the two tools agree on the verdict +# (OK vs invariant-violation). A disagreement means one of the tools is unsound +# on that spec — exactly the class of bug internal-consistency tests cannot catch. +# +# This is the external oracle called for in issue #94. +# +# Usage: +# SPECL=path/to/specl TLA_TOOLS_JAR=path/to/tla2tools.jar ./oracle.sh +# +# Defaults: SPECL=specl on PATH (or target/release/specl), tla2tools.jar fetched +# to this directory if absent. Java is required for TLC. +# +# Exit code: 0 if every spec AGREEs (ignoring the documented known-issue +# allowlist), 1 on any new disagreement, 2 if a required tool is missing. +set -uo pipefail + +HERE="$(cd "$(dirname "$0")" && pwd)" +REPO="$(cd "$HERE/../../.." && pwd)" # repo root (contains specl/) + +SPECL="${SPECL:-}" +if [[ -z "$SPECL" ]]; then + if command -v specl >/dev/null 2>&1; then SPECL="specl" + elif [[ -x "$REPO/specl/target/release/specl" ]]; then SPECL="$REPO/specl/target/release/specl" + else echo "INCONCLUSIVE: specl binary not found (set SPECL=...)"; exit 2; fi +fi + +if ! command -v java >/dev/null 2>&1; then + echo "INCONCLUSIVE: java not found (required for TLC)"; exit 2 +fi + +JAR="${TLA_TOOLS_JAR:-$HERE/tla2tools.jar}" +if [[ ! -f "$JAR" ]]; then + echo "Fetching tla2tools.jar ..." + curl -sL -o "$JAR" https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \ + || { echo "INCONCLUSIVE: could not download tla2tools.jar"; exit 2; } +fi + +# Specs whose disagreement is a known, filed bug. Format: "name=issue". +# Remove an entry once its bug is fixed so the oracle guards against regression. +KNOWN_ISSUES=("DieHard=#96") + +# Curated specs: "name|tla|cfg|specl-args". Paths are relative to the repo root. +SPECS=( + "Counter|specl/tools/soundness/specs/Counter.tla|specl/tools/soundness/specs/Counter.cfg|--no-deadlock" + "DieHard|specl/benchmarks/comparison/DieHard.tla|specl/benchmarks/comparison/DieHard.cfg|" +) + +# Map a tool's raw output to OK | VIOLATION | ERROR. +tlc_verdict() { + local out="$1" + if grep -qiE "is violated|Error: Invariant" <<<"$out"; then echo VIOLATION + elif grep -qiE "No error has been found" <<<"$out"; then echo OK + else echo ERROR; fi +} +specl_verdict() { + local out="$1" + if grep -qiE "INVARIANT VIOLATION" <<<"$out"; then echo VIOLATION + elif grep -qiE "Result: OK" <<<"$out"; then echo OK + else echo ERROR; fi +} + +is_known() { + local name="$1" + for k in "${KNOWN_ISSUES[@]}"; do [[ "${k%%=*}" == "$name" ]] && { echo "${k#*=}"; return 0; }; done + return 1 +} + +printf "%-12s %-10s %-10s %-s\n" "SPEC" "TLC" "SPECL" "RESULT" +printf "%-12s %-10s %-10s %-s\n" "----" "---" "-----" "------" + +fail=0 +for entry in "${SPECS[@]}"; do + IFS='|' read -r name tla cfg args <<<"$entry" + tla="$REPO/$tla"; cfg="$REPO/$cfg" + tlc_out="$(java -cp "$JAR" tlc2.TLC -config "$cfg" "$tla" 2>&1)" + specl_out="$("$SPECL" check "$tla" $args 2>&1)" + tv="$(tlc_verdict "$tlc_out")"; sv="$(specl_verdict "$specl_out")" + + if [[ "$tv" == "ERROR" || "$sv" == "ERROR" ]]; then + result="SKIP (tool could not check)" + elif [[ "$tv" == "$sv" ]]; then + result="AGREE" + elif issue="$(is_known "$name")"; then + result="DISAGREE (known $issue)" + else + result="DISAGREE — SOUNDNESS BUG"; fail=1 + fi + printf "%-12s %-10s %-10s %-s\n" "$name" "$tv" "$sv" "$result" +done + +echo +if [[ "$fail" -ne 0 ]]; then + echo "FAIL: a tool disagreed on a spec not in the known-issues allowlist." + exit 1 +fi +echo "OK: all specs agree (or are documented known issues)." diff --git a/specl/tools/soundness/specs/Counter.cfg b/specl/tools/soundness/specs/Counter.cfg new file mode 100644 index 0000000..d84a921 --- /dev/null +++ b/specl/tools/soundness/specs/Counter.cfg @@ -0,0 +1,4 @@ +INIT Init +NEXT Next +INVARIANT Bounded +CHECK_DEADLOCK FALSE diff --git a/specl/tools/soundness/specs/Counter.tla b/specl/tools/soundness/specs/Counter.tla new file mode 100644 index 0000000..cdaad12 --- /dev/null +++ b/specl/tools/soundness/specs/Counter.tla @@ -0,0 +1,11 @@ +---- MODULE Counter ---- +EXTENDS Integers +VARIABLE count + +Init == count = 0 +Inc == count < 5 /\ count' = count + 1 +Dec == count > 0 /\ count' = count - 1 +Next == Inc \/ Dec + +Bounded == count >= 0 /\ count <= 5 +==== From 2731a745d63a13dcae749f2b1e7d5ea293e26589 Mon Sep 17 00:00:00 2001 From: danwt Date: Fri, 26 Jun 2026 18:21:19 +0200 Subject: [PATCH 13/13] claude: chore: remove TLC soundness oracle from public repo The cross-tool oracle lives in the private repo's soundness harness (which has a more comprehensive parser/minispec/e2e differential vs TLC). Keep the public repo free of the TLC/Java dependency. --- .gitignore | 2 - specl/tools/soundness/README.md | 35 --------- specl/tools/soundness/oracle.sh | 98 ------------------------- specl/tools/soundness/specs/Counter.cfg | 4 - specl/tools/soundness/specs/Counter.tla | 11 --- 5 files changed, 150 deletions(-) delete mode 100644 specl/tools/soundness/README.md delete mode 100755 specl/tools/soundness/oracle.sh delete mode 100644 specl/tools/soundness/specs/Counter.cfg delete mode 100644 specl/tools/soundness/specs/Counter.tla diff --git a/.gitignore b/.gitignore index cfd4ada..75bbd4c 100644 --- a/.gitignore +++ b/.gitignore @@ -25,5 +25,3 @@ MC*.out *.z3-trace fuzz/target/ -# Soundness oracle: downloaded TLC jar -specl/tools/soundness/tla2tools.jar diff --git a/specl/tools/soundness/README.md b/specl/tools/soundness/README.md deleted file mode 100644 index 3a495c3..0000000 --- a/specl/tools/soundness/README.md +++ /dev/null @@ -1,35 +0,0 @@ -# Soundness oracle - -Specl's built-in soundness tests check *internal* consistency (storage backends -agree, parallel == sequential, parse roundtrip). They cannot catch a bug where -the whole checker reaches a wrong verdict. This oracle adds an *external* one: it -runs the same TLA+ spec through both TLC and specl and asserts they agree on -OK-vs-violation. - -## Run - -```bash -# from the repo root; java required, tla2tools.jar auto-downloaded if absent -specl/tools/soundness/oracle.sh -# or pin the tools: -SPECL=specl/target/release/specl TLA_TOOLS_JAR=/path/to/tla2tools.jar specl/tools/soundness/oracle.sh -``` - -Exit 0 if every spec agrees (or is an allowlisted known issue), 1 on a new -disagreement, 2 if a required tool is missing. - -## Specs - -Curated `.tla` + `.cfg` pairs are listed in `oracle.sh` (`SPECS`). Each must use -only scalar constants (specl's `-c` does not take set-valued constants yet) and -translate cleanly. `specs/` holds oracle-only specs; others are reused from -`specl/benchmarks/comparison/`. - -## Known issues - -`KNOWN_ISSUES` in `oracle.sh` lists specs whose disagreement is a filed bug, so -the oracle stays green while still guarding against new disagreements. Remove an -entry when its bug is fixed. - -- `DieHard` — #96: the default symbolic path (IC3) returns a false OK; BFS, BMC, - and TLC all find the violation. diff --git a/specl/tools/soundness/oracle.sh b/specl/tools/soundness/oracle.sh deleted file mode 100755 index 75d13da..0000000 --- a/specl/tools/soundness/oracle.sh +++ /dev/null @@ -1,98 +0,0 @@ -#!/usr/bin/env bash -# Cross-tool soundness oracle: run the same TLA+ spec through both TLC and specl -# (auto-translating the .tla) and assert the two tools agree on the verdict -# (OK vs invariant-violation). A disagreement means one of the tools is unsound -# on that spec — exactly the class of bug internal-consistency tests cannot catch. -# -# This is the external oracle called for in issue #94. -# -# Usage: -# SPECL=path/to/specl TLA_TOOLS_JAR=path/to/tla2tools.jar ./oracle.sh -# -# Defaults: SPECL=specl on PATH (or target/release/specl), tla2tools.jar fetched -# to this directory if absent. Java is required for TLC. -# -# Exit code: 0 if every spec AGREEs (ignoring the documented known-issue -# allowlist), 1 on any new disagreement, 2 if a required tool is missing. -set -uo pipefail - -HERE="$(cd "$(dirname "$0")" && pwd)" -REPO="$(cd "$HERE/../../.." && pwd)" # repo root (contains specl/) - -SPECL="${SPECL:-}" -if [[ -z "$SPECL" ]]; then - if command -v specl >/dev/null 2>&1; then SPECL="specl" - elif [[ -x "$REPO/specl/target/release/specl" ]]; then SPECL="$REPO/specl/target/release/specl" - else echo "INCONCLUSIVE: specl binary not found (set SPECL=...)"; exit 2; fi -fi - -if ! command -v java >/dev/null 2>&1; then - echo "INCONCLUSIVE: java not found (required for TLC)"; exit 2 -fi - -JAR="${TLA_TOOLS_JAR:-$HERE/tla2tools.jar}" -if [[ ! -f "$JAR" ]]; then - echo "Fetching tla2tools.jar ..." - curl -sL -o "$JAR" https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \ - || { echo "INCONCLUSIVE: could not download tla2tools.jar"; exit 2; } -fi - -# Specs whose disagreement is a known, filed bug. Format: "name=issue". -# Remove an entry once its bug is fixed so the oracle guards against regression. -KNOWN_ISSUES=("DieHard=#96") - -# Curated specs: "name|tla|cfg|specl-args". Paths are relative to the repo root. -SPECS=( - "Counter|specl/tools/soundness/specs/Counter.tla|specl/tools/soundness/specs/Counter.cfg|--no-deadlock" - "DieHard|specl/benchmarks/comparison/DieHard.tla|specl/benchmarks/comparison/DieHard.cfg|" -) - -# Map a tool's raw output to OK | VIOLATION | ERROR. -tlc_verdict() { - local out="$1" - if grep -qiE "is violated|Error: Invariant" <<<"$out"; then echo VIOLATION - elif grep -qiE "No error has been found" <<<"$out"; then echo OK - else echo ERROR; fi -} -specl_verdict() { - local out="$1" - if grep -qiE "INVARIANT VIOLATION" <<<"$out"; then echo VIOLATION - elif grep -qiE "Result: OK" <<<"$out"; then echo OK - else echo ERROR; fi -} - -is_known() { - local name="$1" - for k in "${KNOWN_ISSUES[@]}"; do [[ "${k%%=*}" == "$name" ]] && { echo "${k#*=}"; return 0; }; done - return 1 -} - -printf "%-12s %-10s %-10s %-s\n" "SPEC" "TLC" "SPECL" "RESULT" -printf "%-12s %-10s %-10s %-s\n" "----" "---" "-----" "------" - -fail=0 -for entry in "${SPECS[@]}"; do - IFS='|' read -r name tla cfg args <<<"$entry" - tla="$REPO/$tla"; cfg="$REPO/$cfg" - tlc_out="$(java -cp "$JAR" tlc2.TLC -config "$cfg" "$tla" 2>&1)" - specl_out="$("$SPECL" check "$tla" $args 2>&1)" - tv="$(tlc_verdict "$tlc_out")"; sv="$(specl_verdict "$specl_out")" - - if [[ "$tv" == "ERROR" || "$sv" == "ERROR" ]]; then - result="SKIP (tool could not check)" - elif [[ "$tv" == "$sv" ]]; then - result="AGREE" - elif issue="$(is_known "$name")"; then - result="DISAGREE (known $issue)" - else - result="DISAGREE — SOUNDNESS BUG"; fail=1 - fi - printf "%-12s %-10s %-10s %-s\n" "$name" "$tv" "$sv" "$result" -done - -echo -if [[ "$fail" -ne 0 ]]; then - echo "FAIL: a tool disagreed on a spec not in the known-issues allowlist." - exit 1 -fi -echo "OK: all specs agree (or are documented known issues)." diff --git a/specl/tools/soundness/specs/Counter.cfg b/specl/tools/soundness/specs/Counter.cfg deleted file mode 100644 index d84a921..0000000 --- a/specl/tools/soundness/specs/Counter.cfg +++ /dev/null @@ -1,4 +0,0 @@ -INIT Init -NEXT Next -INVARIANT Bounded -CHECK_DEADLOCK FALSE diff --git a/specl/tools/soundness/specs/Counter.tla b/specl/tools/soundness/specs/Counter.tla deleted file mode 100644 index cdaad12..0000000 --- a/specl/tools/soundness/specs/Counter.tla +++ /dev/null @@ -1,11 +0,0 @@ ----- MODULE Counter ---- -EXTENDS Integers -VARIABLE count - -Init == count = 0 -Inc == count < 5 /\ count' = count + 1 -Dec == count > 0 /\ count' = count - 1 -Next == Inc \/ Dec - -Bounded == count >= 0 /\ count <= 5 -====