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
You can try the Cosette demo online, using Cosette Web API or download its source code from github. Read the Cosette Guide to learn how to use Cosette, it is very easy to use!
Cosette Web UI (click image above to visit demo website)
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
Publications
- Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries [ paper ] VLDB 2018.
- 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.
Contact
If you have any questions, want to contribute to the project, or just want to say hi, email us at cosette@cs.washington.edu.
People
Cosette is developed by the Database Group and the Programming Languages and Software Engineering Group at the University of Washington, the main contributors are:
