Conversation
…, strings, traces Complete symbolic model checking phase 2: - Set operations: union/intersect/diff/subset for ExplodedSet encoding. Enables TwoPhaseCommit verification. - String variable encoding: intern string literals as bounded integers via a string table. Enables TCommit_Simple verification. - Const-dependent type inference: resolve 0..MAX ranges from AST type expressions when the type checker compiles them to bare Int. - k-induction: base case (BMC to depth K) + inductive step with K consecutive states. CLI: --k-induction K - IC3/CHC: unbounded verification via Z3's Spacer engine using raw z3-sys fixedpoint API with explicit forall quantification. CLI: --ic3 - Smart mode: automatic strategy cascade (induction -> k-induction K=2..5 -> IC3 -> BMC fallback). CLI: --smart - Trace action identification: counterexample traces now show which action (with parameters) fired at each step. - Fix: k-induction inductive step failure (CTI) returns Unknown, not InvariantViolation. New files: k_induction.rs, fixedpoint.rs, ic3.rs, smart.rs Dependencies: z3-sys 0.10.4, specl-syntax (for AST type expressions) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Complete symbolic model checking phase 2, adding all remaining verification modes and encoding capabilities:
0..MAXwhen MAX is a const)--k-induction K): base case BMC + K-step inductive strengthening--ic3): unbounded verification via Z3's Spacer engine, using raw z3-sys fixedpoint API with explicit forall quantification--smart): automatic strategy cascade (induction → k-induction K=2..5 → IC3 → BMC)Verification
cargo fmt --checkclean, zero warnings on specl-symbolicTest plan
cargo test --workspace --exclude specl-tla— 119 tests passcargo fmt --check— clean--k-induction 3,--ic3,--smartall OK--ic3,--smartall OK--symbolic --depth 5,--ic3,--smartall OK🤖 Generated with Claude Code