Sprout is a baby, verified implementation of the CDSAT (seedy-SAT) SMT solving algorithm. It is verified using Creusot.
The key feature of Sprout is its verified implementation of the core CDSAT loop, including conflict resolution. Additionally it contains two naive implementations of theories for boolean logic and linear rational arithmetic.
Sprout can be fed SMTLIB inputs simply by passing then as input to the binary:
cargo run --bin=cdsat -- file.smt2
Currently it accepts a subset of SMTLIB relevant to the theories implemented, it may crash with an error if you provide an unsupported syntax.
The various proofs of Sprout's correctness are stored in the mlcfg directory. They were built using a version of Creusot built from commit 5646d67143.
Once you have installed Creusot and & Why3, and configured CVC4, CVC5, Z3, and Alt-Ergo as provers, you will be able to verify the various proofs.
Due to performance limitations of the Why3 GUI, the proofs were split up into several independent sessions in a fairly ad-hoc manner. The following table shows how this partioning was performed, and which command can be used to browse the resulting proofs.
| Rust Module / Function | Proof Session Name | Command | Notes |
|---|---|---|---|
src/theory.rs |
theory |
./dev theory |
|
src/trail.rs |
trail |
./dev trail |
|
concrete::resolve_conflict |
resolve_conflict |
./dev resolve_conflict |
|
concrete::solver |
concrete |
./dev concrete |
In this proof, ignore resolve_conflict which is proved in a standalone session |
src/bool.rs |
bool |
./dev bool |
|
src/term.rs |
term |
./dev term |
|
src/heap.rs |
heap |
./dev heap |
A bug in the type invariants of Creusot causes it to report a trait refinment as unproved |
All proofs were verified on a Apple M1 Pro with 32GB of RAM.