xldenis / cdsat

cdsat

🌱 The Sprout SMT solver

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.

Running Sprout

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.

Running the proofs

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.