Foundation fixes: sum (core+symbolic), string-keyed dicts, recursion/enabled/changes/partial-dict errors, fmt safety, soundness oracle

.gitignore

@@ -24,4 +24,4 @@ MC*.out
 
 *.z3-trace
 
-fuzz/target/
+fuzz/target/

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.

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

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,15 +28,21 @@ 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
 
 `EXTENDS` and `INSTANCE` (TLA+-style module composition) are not yet supported. Each spec is a single module.
 
 ## 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
 

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]` |

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]` |
 

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]`

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<Value>,
     flags: &BfsFlags,
     source: Option<(&Arc<String>, &PathBuf)>,
+    ignored_liveness: usize,
 ) -> CliResult<()> {
     let var_names: Vec<String> = spec.vars.iter().map(|v| v.name.clone()).collect();
     let action_names: Vec<String> = 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<Vec<Value>> {
@@ -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

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)?;

specl/crates/specl-eval/src/eval.rs

@@ -629,6 +629,8 @@ pub fn eval(expr: &CompiledExpr, ctx: &mut EvalContext) -> EvalResult<Value> {
             }
         }
 
+        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<i64> {
             }
         }
 
+        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<i64> {
+    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<Vec<Value>> {