Cosette is an automated prover for checking equivalences of SQL queries. It formalizes a substantial fragment of SQL in the Coq Proof Assistant and the Rosette symbolic virtual machine. It returns either a formal proof of equivalance or a counterexample for a pair of given queries.
Our medium article
Checking SQL Equivalences in Cosette
How does Cosette work?
Cosette compiles input queries to constraints over symbolic relations and calls Rosette to find counterexamples, which are input tables that the two input queries return different answer. Cosette also compiles input queries into expressions of K-relations, UniNomials we call, which are mathematical functions that returns multiplicity of tuples, using Coq with Homotopy Type Theory. Cosette then tries to search a Coq proof of equivalence of the two input queries given any valid input data. The architecture of Cosette is shown as below:
Cosette System Architecture
- Demonstration of the Cosette Automated SQL Prover. [ paper ] SIGMOD 2017 (best demo award)
- Cosette: An Automated Prover For SQL. [ paper ] CIDR 2017.
- HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics. [ paper ] [ full version ] [ artifact ] [ video ] PLDI 2017.
- Blog Post on the Homotopy Type Theory Blog.
If you have any questions, want to contribute to the project, or just want to say hi, email us at email@example.com.
Cosette is developed by the Database Group and the Programming Languages and Software Engineering Group at the University of Washington, the main contributors are: