# VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with
Integrity Constraints

Yang He  0009-0007-7755-3112 Simon Fraser UniversityBurnabyCanada
<EMAIL_ADDRESS>,  Pinhan Zhao  0009-0002-1149-0706 University of MichiganAnn
ArborUSA<EMAIL_ADDRESS>,  Xinyu Wang  0000-0002-1836-0202 University of
MichiganAnn ArborUSA<EMAIL_ADDRESS>and  Yuepeng Wang  0000-0003-3370-2431
Simon Fraser UniversityBurnabyCanada<EMAIL_ADDRESS>
(2024; 2023-10-21; 2024-02-24)

###### Abstract.

The task of SQL query equivalence checking is important in various real-world
applications (including query rewriting and automated grading) that involve
_complex queries with integrity constraints_ ; yet, state-of-the-art
techniques are very limited in their capability of reasoning about complex
features (e.g., those that involve sorting, case statement, rich integrity
constraints, etc.) in real-life queries. To the best of our knowledge, we
propose the first SMT-based approach and its implementation, VeriEQL, capable
of proving and disproving bounded equivalence of _complex_ SQL queries.
VeriEQL is based on a new logical encoding that models query semantics over
symbolic tuples using the theory of integers with uninterpreted functions. It
is _simple yet highly practical_ — our comprehensive evaluation on over 20,000
benchmarks shows that VeriEQL outperforms _all_ state-of-the-art techniques by
_more than one order of magnitude_ in terms of the number of benchmarks that
can be proved or disproved. VeriEQL can also generate counterexamples that
facilitate many downstream tasks (such as finding serious bugs in systems like
MySQL and Apache Calcite).

Program Verification, Equivalence Checking, Relational Databases.

††copyright: rightsretained††doi: 10.1145/3649849††journalyear:
2024††submissionid: oopslaa24main-p142-p††journal: PACMPL††journalvolume:
8††journalnumber: OOPSLA1††article: 132††publicationmonth: 4††ccs: Theory of
computation Program verification††ccs: Software and its engineering Software
verification††ccs: Software and its engineering Formal software verification

##  1\. Introduction

Equivalence checking of SQL queries is an important problem with various real-
world applications, including validating source-level query rewriting (Graefe,
1995; Chu et al., 2017b) and automated grading of SQL queries (Chandra et al.,
2019). A useful SQL equivalence checker should be able to (i) provide formal
guarantee on query equivalence (either fully or in a bounded manner), (ii)
generate counterexamples to witness query non-equivalence, and (iii) support
an expressive query language. For example, in the context of query rewriting
where a slow query $Q_{1}$ is rewritten to a faster query $Q_{2}$ using
rewrite rules, one may want to ensure the rewrite is correct by showing
$Q_{1}$ and $Q_{2}$ are semantically equivalent with a certain level of formal
guarantee, and in case of non-equivalence, obtain a counterexample input
database to help fix the incorrect rule. Equivalence checking is also useful
for automated query grading. In particular, it can provide feedback to users
by checking their submitted queries against a ground-truth query, where the
feedback could be a counterexample (i.e., a concrete database) that
illustrates why the user query is wrong. Moreover, these counterexamples can
also serve as additional test cases to augment an existing test suite (such as
the one maintained by LeetCode (LeetCode, 2023), the world’s most popular
online programming platform).

While prior work (Chu et al., 2017b, a, c, 2018; Wang et al., 2018a; Veanes et
al., 2010) has made some advances in both proving and disproving query
equivalence, there remain a number of challenges that significantly limit the
practical usage of existing techniques in real-world applications. The gap, as
we will also show in our evaluation section later, is in fact _extremely
large_ : for example, existing work supports less than 2% of the SQL queries
from LeetCode. The reasons are threefold.

  * •

First, real-world queries are complex. In addition to the simplest select-
project-join queries using common aggregate functions such as
$\texttt{SUM},\texttt{COUNT},\texttt{MAX}$ — that existing techniques support
fairly well — queries in the wild frequently use advanced SQL features with
much more complex logic (such as sorting, case statement, common table
expressions, IN and NOT IN operators, etc.) which, to our best knowledge,
existing SQL equivalence checkers rarely support. For example, among more than
20,000 real-life queries we studied, more than 20% of them involve ORDER BY,
over 30% have CASE WHEN, over 15% require IN or NOT IN, and 15% use WITH,
among others. This brings up new challenges in how to precisely model the
semantics of these advanced SQL operators.

  * •

Furthermore, the interleaving between these advanced operators and other SQL
features (such as three-valued logic, aggregate functions, grouping, etc.)
makes the problem even more challenging. For example, the three-valued logic
uses a special value NULL that many existing techniques (such as HoTTSQL (Chu
et al., 2017c)) do not consider. We must take into account all these
additional SQL features to properly model the semantics of SQL operators in
order to fully support complex real-world queries and reason about query
equivalence.

  * •

Finally, most real-world queries involve integrity constraints, but prior work
barely supports them. For instance, over 95% of our benchmarks require
integrity constraints, yet all existing techniques _cumulatively_ support
under 2%, to our best knowledge. These constraints are rich: in addition to
the primary key and foreign key constraints that stipulate uniqueness and
value references, there are many others including NOT NULL (used by _all_
queries in our Calcite benchmark suite) and various constraints that restrict
attribute values (¿70% across all our benchmarks) such as requiring an
attribute to be only positive integers. This richness poses significant
challenges: for example, to witness the non-equivalence of two queries, a
valid counterexample must not only yield different outputs _but also_ meet the
integrity constraints.

In this paper, we propose a _simple yet practical_ approach to SQL query
equivalence checking — we can prove equivalence (in a bounded fashion) and
non-equivalence (by generating counterexamples) for _a complex query language
with rich integrity constraints._ Our key contribution is a _new SMT encoding_
tailored towards bounded equivalence verification, based on a _new semantics
formalization_ for a practical fragment of SQL (which is _significantly
larger_ than those considered in prior work). First, we formalize our SQL
semantics using list and higher-order functions, different from the
K-relations in HoTTSQL (Chu et al., 2017c) or U-semiring in UDP (Chu et al.,
2018). Our formalization is inspired by Mediator (Wang et al., 2018b).
However, Mediator considers unbounded equivalence verification for a small set
of SQL queries, while our formalization considers a much larger language.
Second, building upon the standard approach of using SMT formulas to relate
the program inputs and outputs, we develop a _new SMT encoding_ , for our
formalized query semantics, in the theory of integers and uninterpreted
functions that is based on symbolic tuples. This new SMT encoding allows us to
handle complex SQL features (e.g., ORDER BY, NULL, etc) and rich integrity
constraints without unnecessarily heavy theories such as theory of lists in
Qex (Veanes et al., 2010). It also does not require an indirect encoding by
translating the SQL queries to an intermediate representation in solver-aided
programming language (e.g., Rosette (Torlak and Bodík, 2014)), unlike the
previous Cosette line of work (Chu et al., 2017b, a; Wang et al., 2018a). Last
but not least, we provide detailed correctness proofs of our SMT encoding with
respect to our formal semantics.

_VeriEQL._ We have implemented our approach in VeriEQL, which is described
schematically in Figure 1. At a high-level, VeriEQL takes as input a pair of
queries $(Q_{1},Q_{2})$, the database schema $\mathcal{S}$ and its integrity
constraint $\mathcal{C}$, and a bound $N$ defining the input space. It
constructs an SMT formula $\Phi$ such that: (i) if $\Phi$ is unsatisfiable,
then $Q_{1}$ and $Q_{2}$ are guaranteed to be equivalent for all database
relations with at most $N$ tuples, and (ii) if $\Phi$ is satisfiable, then
$Q_{1}$ and $Q_{2}$ are provably non-equivalent, and we generate a
counterexample (i.e., a database that meets $\mathcal{C}$ but leads to
different query outputs) from $\Phi$’s satisfying assignments. Internally, 1
VeriEQL first creates a symbolic representation $\Gamma$ of all input
databases with up to $N$ tuples in their relations, and encodes the integrity
constraint $\mathcal{C}$ over $\Gamma$ into an SMT formula
$\Phi_{\mathcal{C}}$. Then, we process both queries and encode their
equivalence into an SMT formula $\Phi_{R}$: 2 we traverse $Q_{i}$ in a forward
fashion, encode how each operator in $Q_{i}$ transforms its input to output,
obtain the final output $R_{i}$ of $Q_{i}$ for all input databases under
consideration, and 3 generate an SMT formula $\Phi_{R}$ that asserts
$R_{1}\neq R_{2}$ (we support bag and list semantics). While this overall
approach is standard, our encoding scheme of each operator’s semantics is new
and has some important advantages. First, our encoding is based on the theory
of integers with uninterpreted functions: it is simple yet sufficient to
precisely encode all SQL features in our language (such as complex aggregate
functions with grouping and previously unsupported operators like ORDER BY).
Crucially, our approach can support these advanced SQL features without
needing additional axioms, which prior work like Qex would otherwise require.
Second, our encoding follows the three-valued logic and supports NULL for all
of our operators, whereas prior work supports NULL for significantly fewer
cases. In the final step 4, we construct
$\Phi=\Phi_{\mathcal{C}}\land\Phi_{R}$ and use an off-the-shelf SMT solver to
solve $\Phi$. Notably, $\Phi$ takes into account both query semantics and
integrity constraints in a much simpler and more unified manner than some
prior work that has separate schemes to handle queries and integrity
constraints. For example, SPES (Zhou et al., 2022) performs symbolic encoding
for queries but uses rewrite rules to deal with integrity constraints — it is
fundamentally hard for such approaches to support complex integrity
constraints such as those that restrict the value range.

Figure 1. Schematic workflow of VeriEQL.

We have evaluated VeriEQL on an extremely large number of benchmarks,
consisting of 24,455 query pairs collected from three different workloads
(including all benchmarks from the literature, standard benchmarks from
Calcite, and over 20,000 new benchmarks from LeetCode). Our evaluation results
show that VeriEQL can prove the bounded equivalence for significantly more
benchmarks than all state-of-the-art techniques, disprove and find
counterexamples for two orders of magnitude more benchmarks, and uncover
serious bugs in real-world codebases (including MySQL and Calcite).

_Contributions._ This paper makes the following contributions.

  * •

We formulate the problem of bounded SQL equivalence verification _modulo
integrity constraints_.

  * •

We formalize the semantics of a practical fragment of SQL queries through list
and higher-order functions. Our SQL fragment is significantly larger than
those in prior work.

  * •

We propose a novel SMT encoding tailored towards bounded equivalence
verification of SQL queries, including previously unsupported SQL operators
(e.g., ORDER BY, CASE WHEN) and rich integrity constraints. To our best
knowledge, this is the first approach that supports complex SQL queries with
rich integrity constraints.

  * •

We prove our SMT encoding of SQL queries is correct with respect to the formal
semantics.

  * •

We implement our approach in VeriEQL. Our comprehensive evaluation on a total
of 24,455 benchmarks — including a new benchmark suite with over 20,000 real-
life queries — shows that, VeriEQL can solve (i.e., prove or disprove
equivalence) 77% of these benchmarks, while state-of-the-art bounded verifier
can solve ¡2% and testing tools can disprove ¡1%.

##  2\. Overview

(a) Schema, integrity constraint, and queries.

(b) Generating symbolic database.

(c) Encoding integrity constraint.

(d) Encoding query semantics.

(e) Checking equality.

(f) Constraint solving.

Figure 2. Illustration of how VeriEQL works on a simple LeetCode task.

In this section, we further illustrate VeriEQL’s workflow using a simple
example from LeetCode111https://leetcode.com/problems/page-recommendations.
Note that for illustration purposes, we significantly simplify the database
schema and queries in this task, but VeriEQL can handle the original
queries222The original queries are available in Appendix A. that are much more
complex.

Specifically, this task involves a database with two relations, Friendship (or
$F$) and Likes (or $L$), where $F$ records users’ friends and $L$ stores
users’ preferred pages. The task is to write a query that, given a user,
returns the recommended pages which their friends prefer but are not preferred
by the given user. In what follows, we explain this task in more detail.

_Schema and integrity constraint._ Figure 2(a) shows the database schema
$\mathcal{S}$ with the two relations: (i) Friendship relation $F$ has two
attributes $uid$ and $fid$, denoting the ID of each user and their friends,
and (ii) Likes relation $L$ with two attributes $id$ and $pid$ which denote
the user ID and the preferred page ID. The integrity constraint $\mathcal{C}$
for this task specifies that the pair $(uid,fid)$ is the primary key of $F$,
and $id$ is the primary key of $L$.

_Queries._ Consider the user with $id=1$. Figure 2(a) shows a query $Q_{1}$
that can solve the task for this given user. In particular, $Q_{1}$ uses an 1
INNER JOIN to find the given user’s friends, and uses a 2 nested query
followed by a 3 NOT IN filter to rule out the given user’s preferred pages.
Figure 2(a) also shows another query $Q_{2}$ which is similar to $Q_{1}$ but
uses a 5 LEFT JOIN instead. Note that $Q_{2}$ is _not_ equivalent to $Q_{1}$ —
consider the case where the given user does not have any friends (i.e., $F$
does not have a tuple with $uid=1$). In this case, the INNER JOIN in $Q_{1}$
returns an empty result as the join condition $F.uid=1$ never holds, whereas
the LEFT JOIN from $Q_{2}$ gives a product tuple $t^{\prime}$ for each tuple
$t$ in $L$ and $t^{\prime}.pid=\texttt{NULL}$. The NULL values on $pid$ will
eventually be projected out by $Q_{2}$, leading to (incorrect) NULL tuples in
the result.

In what follows, let us explain how VeriEQL proves the non-equivalence of
$(Q_{1},Q_{2})$. Specifically, we will explain the key concepts in Figure 1:
(1) what does a symbolic database look like, (2) how to encode the integrity
constraint, (3) how to encode the query semantics, (4) how to check two
queries always produce identical outputs, and (5) how to obtain verification
results.

_Generating symbolic database._ Figure 2(b) shows the symbolic DB generated by
VeriEQL that has _up to_ 2 rows in each relation (i.e., the input bound is 2).
Each row is called a _symbolic tuple_. For instance, we denote the tuples in
$F$ by $t_{1},t_{2}$ and denote the attribute values by $x_{1}=t_{1}.uid$ and
$x_{2}=t_{1}.fid$ and etc. Similarly, the tuples in $L$ are $t_{3},t_{4}$ and
the values for $id$ and $pid$ are $y_{1},y_{2}$ and $y_{3},y_{4}$,
respectively. In general, we use an _uninterpreted_ predicate Del over tuples
to indicate whether a tuple is deleted after an operation. Since the value of
$\text{Del}(t_{i})$ is unspecified, whether $t_{i}$ is deleted or not is non-
deterministic. Thus, the initial symbolic database encodes all databases where
each relation has _at most_ two tuples.

_Encoding integrity constraint._ Figure 2(c) shows VeriEQL’s SMT encoding
$\Phi_{\mathcal{C}}$ of the integrity constraint $\mathcal{C}$. It has two
parts. The first part

$x_{1}\neq\text{Null}\land x_{2}\neq\text{Null}\land x_{3}\neq\text{Null}\land
x_{4}\neq\text{Null}\land\neg(x_{1}=x_{3}\land x_{2}=x_{4})$

specifies that tuples $t_{1},t_{2}$ are unique and all attributes are not
null, since $(uid,fid)$ is a primary key. The second part
$y_{1}\neq\text{Null}\land y_{3}\neq\text{Null}\land y_{1}\neq y_{3}$ encodes
that $id$ is a primary key of relation $L$.

_Encoding query semantics._ To encode the semantics of a query, VeriEQL
encodes the semantics of each operator which are then composed to form the
encoding of the entire query. For example, the formula $\Phi_{1}$ to encode
$Q_{1}$ is the conjunction of $\Phi_{R_{1}}$, $\Phi_{R_{2}}$, $\Phi_{R_{3}}$
and $\Phi_{R_{4}}$. Specifically, to encode the inner join $T_{1}\bowtie
T_{2}$ in 1, VeriEQL considers the Cartesian product of tuples in $T_{1}$ and
$T_{2}$, followed by a filter to set all resulted tuples that do not satisfy
$T_{1}.fid=T_{2}.id$ and $T_{1}.id=1$ as deleted. For the NOT IN in $Q_{1}$,
it analyzes the nested query and generates the formula $\Phi_{R_{2}}$ (as
shown in 2), and checks the membership of $T_{1}.pid$ with the obtained $pid$,
which is encoded as $\Phi_{R_{3}}$ in 3. Finally, the $pid$ is projected out
by 4, resulting in the output $R_{4}$ and a formula $\Phi_{R_{4}}$. The
obtained formula
$\Phi_{1}=\Phi_{R_{1}}\land\Phi_{R_{2}}\land\Phi_{R_{3}}\land\Phi_{R_{4}}$
precisely encodes the query semantics of $Q_{1}$. Similarly, $Q_{2}$’s output
is $R_{8}$ and the corresponding formula $\Phi_{2}$ consists of
$\Phi_{R_{5}}$, $\Phi_{R_{6}}$, $\Phi_{R_{7}}$ and $\Phi_{R_{8}}$ from 5 6 7
8, respectively.

_Checking equality._ After encoding the semantics of queries $Q_{1}$ and
$Q_{2}$, VeriEQL needs to compare their outputs $R_{4}$ and $R_{8}$. Although
$R_{4}$ and $R_{8}$ do not have the same number of symbolic tuples, they can
still be equal because some tuples may have been deleted. To check the
equality, VeriEQL generates a formula $\Phi_{\Leftrightarrow}$ (in Figure
2(e)) asserting $R_{4}$ is equal to $R_{8}$. VeriEQL supports both list and
bag semantics. In this example, it uses bag semantics because neither of the
queries involves sorting operations. $\Phi_{\Leftrightarrow}$ encodes two
properties: (1) $R_{4}$ and $R_{8}$ have the same number of non-deleted tuples
and (2) for each non-deleted tuple in $R_{4}$, its multiplicity in $R_{4}$ is
the same as that in $R_{8}$. Since properties (1) and (2) imply that (3) for
each non-deleted tuple in $R_{8}$, its multiplicity in $R_{8}$ is the same as
that in $R_{4}$, we do not need to include a formula for property (3) in
$\Phi_{\Leftrightarrow}$.

_Verification result._ Finally, VeriEQL builds a formula
$\Phi=\Phi_{\mathcal{C}}\land\Phi_{1}\land\Phi_{2}\land\neg\Phi_{\Leftrightarrow}$
encoding the existence of a database $\mathcal{D}$ such that (1) $\mathcal{D}$
satisfies the integrity constraint $\mathcal{C}$ and (2) $Q_{1}$ and $Q_{2}$
have different outputs on $\mathcal{D}$. VeriEQL invokes Z3 and finds $\Phi$
is satisfiable, so it concludes that $Q_{1}$ and $Q_{2}$ are not equivalent
and generates a counterexample database (shown in Figure 2(f)) where $Q_{1}$
and $Q_{2}$ indeed yield different results.

##  3\. Problem Formulation

We first describe the preliminaries of relational schema and database, and
then present our query language and integrity constraints, followed by a
formal problem statement.

###  3.1. Relational Schema and Database

$\begin{array}[]{rcl}\text{Schema}&::&\text{RelName}\to\text{RelSchema}\\\
\text{RelSchema}&::&[(\text{AttrName},\text{Type})]\\\
\text{Type}&\in&\\{\text{Int},\text{Bool}\\}\\\ \end{array}$ (a) Schema

$\begin{array}[]{rcl}\text{Database}&::&\text{RelName}\to\text{Relation}\\\
\text{Relation}&::&[\text{Tuple}]\\\
\text{Tuple}&::&[(\text{AttrName},\text{Value})]\\\
\text{Value}&\in&\textbf{Int}\cup\textbf{Bool}\cup\\{\text{Null}\\}\\\
\end{array}$ (b) Database

Figure 3. Relational schema and database.

_Schema._ As shown in Figure 3(a), a relational database schema is a mapping
from relation names to their relation schemas, where each relation schema is a
list of attributes. Each attribute is represented by a pair of attribute name
and type. All attribute names are assumed to be globally unique, which can be
easily enforced by using fully qualified attribute names that include relation
names, e.g., EMP.age. We only consider two primitive types, namely Int and
Bool, in this paper. Other types (e.g., strings and dates) can be treated as
Int and functions involving those types can be treated as uninterpreted
functions over Int.

_Database._ Similarly, as shown in Figure 3(b), a relational database is a
mapping from relation names to their corresponding relations, where each
relation consists of a list of tuples.333 If a relation is created by a non-
ORDER BY query, then we interpret this list as a bag.  Each tuple contains a
list of values with corresponding attribute names, and a value can be an
integer, bool, or NULL.

###  3.2. Syntax of SQL Queries

$\begin{array}[]{rcl}\text{Query}~{}Q_{r}&::=&Q~{}|~{}\text{OrderBy}(Q,\vec{E},b)\\\
\text{Subquery}~{}Q&::=&R~{}|~{}\Pi_{L}(Q)~{}|~{}\sigma_{\phi}(Q)~{}|~{}\rho_{R}(Q)~{}|~{}Q\oplus
Q~{}|~{}\text{Distinct}(Q)~{}|~{}Q\otimes
Q~{}|~{}\text{GroupBy}(Q,\vec{E},L,\phi)\\\
&|&\text{With}(\vec{Q},\vec{R},Q)\\\ \text{Attr
List}~{}L&::=&id(A)~{}|~{}\rho_{a}(A)~{}|~{}L,L\\\
\text{Attr}~{}A&::=&{\text{Cast}(\phi)}~{}|~{}E~{}|~{}\mathcal{G}(E)~{}|~{}{A\diamond
A}\\\ \text{Pred}~{}\phi&::=&b~{}|~{}\text{Null}~{}|~{}{A\odot
A}~{}|~{}\text{IsNull}(E)~{}|~{}\vec{E}\in\vec{v}~{}|~{}\vec{E}\in
Q~{}|~{}\phi\land\phi~{}|~{}\phi\lor\phi~{}|~{}\neg\phi\\\
\text{Expr}~{}E&::=&a~{}|~{}v~{}|~{}E\diamond
E~{}|~{}\text{ITE}(\phi,E,E)~{}|~{}\text{Case}(\vec{\phi},\vec{E},E)\\\
\text{Join
Op}~{}\otimes&::=&\times~{}|~{}\bowtie_{\phi}~{}|~{}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}~{}|~{}\mathbin{\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}~{}|~{}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}\\\ \text{Collection
Op}~{}\oplus&::=&\cup~{}|~{}\cap~{}|~{}\setminus~{}|~{}\uplus~{}|~{}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}~{}|~{}-\\\
\text{Arith Op}~{}\diamond&::=&+~{}|~{}-~{}|~{}\times~{}|~{}/~{}|~{}\%\\\
\text{Logic
Op}~{}\odot&::=&\leq~{}|~{}<~{}|~{}=~{}|~{}\neq~{}|~{}>~{}|~{}\geq\\\
\end{array}$

$\begin{array}[]{c}R\in\textbf{Relation Names}\quad a\in\textbf{Attribute
Names}\quad v\in\textbf{Values}\quad
b\in\textbf{Bools}\quad\mathcal{G}\in\\{\text{Count},\text{Min},\text{Max},\text{Sum},\text{Avg}\\}\end{array}$

Figure 4. Syntax of SQL Queries. Values include integers, bools, and Null.
$id(A)$ is a construct denoting attribute $A$ itself occurs in the attribute
list. If the context is clear, we may also omit the $id$ constructor for
brevity. The Cast function takes as input a predicate $\phi$ and returns Null
if $\phi$ is Null, 1 if $\phi$ is $\top$, and 0 otherwise.

The syntax of our query language is shown in Figure 4, which covers various
practical SQL operators, including projection $\Pi$, selection $\sigma$,
renaming $\rho$, set union $\cup$, intersection $\cap$, minus $\setminus$, bag
union $\uplus$, intersection
$\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}$, minus $-$,
Distinct, Cartesian product $\times$, inner join $\bowtie_{\phi}$, left outer
join $\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}$, right
outer join $\mathbin{\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}$, full outer join
$\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}$, GroupBy with Having
clauses, With clauses, and OrderBy. In addition, the query language also
supports various attribute expressions such as arithmetic expressions
$E_{1}\diamond E_{2}$, aggregate functions $\mathcal{G}(E)$, if-then-else
expressions $\text{ITE}(\phi,E_{1},E_{2})$, and case expressions
$\text{Case}(\vec{\phi},\vec{E},E^{\prime})$, as well as predicates such as
logical comparison $A_{1}\odot A_{2}$, null checks $\text{IsNull}(E)$, and
membership check $\vec{E}\in Q$. Many of these constructs are not supported by
prior work, such as OrderBy, With, Case, and so on. In what follows, we
discuss the syntax of aggregate functions, GroupBy, and OrderBy in more
detail.

_Aggregate functions and GroupBy._ Our language includes five common aggregate
functions $\mathcal{G}$, and as is standard, it does not permit nested
aggregate functions such as SUM(SUM(a)). The language also has a construct
$\text{GroupBy}(Q,\vec{E},L,\phi)$ for grouping tuples. Intuitively,
$\text{GroupBy}(Q,\vec{E},L,\phi)$ groups the tuples of subquery $Q$ based on
attribute expressions $\vec{E}$ and for each group satisfying condition
$\phi$, it computes an aggregate tuple according to the attribute list $L$.

###### Example 3.1.

The GroupBy operation is closely related to the GROUP BY and HAVING clauses in
standard SQL. For instance, consider a relation EMP(id, gender, age, sal) and
a SQL query:

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{SELECT}}}}}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{AVG}}}}}(\texttt{age}),\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{AVG}}}}}(\texttt{sal})\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{FROM}}}}}\;\texttt{EMP}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{WHERE}}}}}\;\texttt{age}>20\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{GROUP}}\;\textbf{{BY}}}}}\;\texttt{gender}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{HAVING}}}}}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{AVG}}}}}(\texttt{sal})>30000$

It can be represented by the following query in our language

$\text{GroupBy}(\sigma_{\texttt{age}>20}(\texttt{EMP}),[\texttt{gender}],[\text{Avg}(\texttt{age}),\text{Avg}(\texttt{sal})],\text{Avg}(\texttt{sal})>30000)$

It is worthwhile to point out that the grammar in Figure 4 does not precisely
capture all syntactic requirements on valid queries. In particular, a query
with certain syntax errors may also be accepted by the language, because those
syntactic requirements are difficult to describe at the grammar level. We
instead perform static analysis to check if a query is well-formed and throw
errors if the query contains invalid expressions. For example, consider the
following SQL query

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{SELECT}}}}}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{SUM}}}}}(\texttt{sal})\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{FROM}}}}}\;\texttt{EMP}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{GROUP}}\;\textbf{{BY}}}}}\;\texttt{age}\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{{\textbf{{HAVING}}}}}\;\texttt{sal}>10000$

where the HAVING clause uses a non-aggregated attribute sal that is not in the
GROUP BY list. Such a query is not permitted in standard SQL, because it may
contain ambiguity where a group of tuples with the same age may have different
sal values. Our query language also disallows such GroupBy queries. Although a
simple syntactic check can reveal this error, describing the check in grammar
is non-trivial, so we perform static analysis to reject such queries.

_Sorting and OrderBy._ Our language supports sorting the query result.
Specifically, $\text{OrderBy}(Q,\vec{E},b)$ can sort the result of subquery
$Q$ according to a list of attribute expressions $\vec{E}$. The result is in
ascending order if $b=\top$ and in descending order otherwise. Note that as
shown in Figure 4, OrderBy is only allowed to be used at the topmost level of
a query.

###  3.3. Semantics of SQL Queries

$\llbracket Q\rrbracket::\text{Database }\mathcal{D}\to\text{Relation}$

$\begin{array}[]{lcl}\llbracket R\rrbracket_{\mathcal{D}}&=&\mathcal{D}(R)\\\
\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{ite}(\textsf{hasAgg}(L),[\llbracket
L\rrbracket_{\mathcal{D},\llbracket
Q\rrbracket_{\mathcal{D}}}],\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda x.\llbracket
L\rrbracket_{\mathcal{D},x}))\\\
\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda
x.\llbracket\phi\rrbracket_{\mathcal{D},[x]}=\top)\\\
\llbracket\rho_{R}{(Q)}\rrbracket_{\mathcal{D}}&=&\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda
x.\textsf{map}(x,\lambda(n,v).(\textsf{rename}(R,n),v)))\\\ \llbracket
Q_{1}\cap
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket\text{Distinct}(Q_{1})\rrbracket_{\mathcal{D}},\lambda
x.x\in\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\ \llbracket Q_{1}\cup
Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket\text{Distinct}(Q_{1}\uplus
Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket Q_{1}\setminus
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket\text{Distinct}(Q_{1})\rrbracket_{\mathcal{D}},\lambda
x.x\not\in\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\ \llbracket
Q_{1}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket
Q_{1}-(Q_{1}-Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket Q_{1}\uplus
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{append}(\llbracket
Q_{1}\rrbracket_{\mathcal{D}},\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\
\llbracket Q_{1}-Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda x.\textsf{ite}(x\in xs,xs-x,xs),\llbracket
Q_{1}\rrbracket_{\mathcal{D}},\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\
\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{foldr}(\lambda
x.\lambda xs.\textsf{cons}(x,\textsf{filter}(xs,\lambda y.x\neq
y)),[],\llbracket Q\rrbracket_{\mathcal{D}})\\\ \llbracket Q_{1}\times
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{map}(\llbracket
Q_{2}\rrbracket_{\mathcal{D}},\lambda y.\textsf{merge}(x,y))),[],\llbracket
Q_{1}\rrbracket_{\mathcal{D}})\\\ \llbracket
Q_{1}\bowtie_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket\sigma_{\phi}(Q_{1}\times
Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\llbracket
Q_{1}\rrbracket_{\mathcal{D}})\\\
&&\quad\text{where}~{}v_{1}(x)=\llbracket[x]\bowtie_{\phi}Q_{2}\rrbracket_{\mathcal{D}}~{}\text{and}~{}v_{2}(x)=[\textsf{merge}(x,T_{\text{Null}})]\\\
\llbracket
Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\llbracket
Q_{2}\rrbracket_{\mathcal{D}})\\\ &&\quad\text{where}~{}v_{1}(x)=\llbracket
Q_{1}\bowtie_{\phi}[x]\rrbracket_{\mathcal{D}}~{}\text{and}~{}v_{2}(x)=[\textsf{merge}(T_{\text{Null}},x)]\\\
\llbracket Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{append}(\llbracket
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\rrbracket_{\mathcal{D}},\textsf{map}(xs,\lambda
x.\textsf{merge}(T_{\text{Null}},x)))\\\
&&\quad\text{where}~{}xs=\textsf{filter}(\llbracket
Q_{2}\rrbracket_{\mathcal{D}},\lambda y.|\llbracket
Q_{1}\bowtie_{\phi}[y]\rrbracket_{\mathcal{D}}|=0)\\\
\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{D}}\\!\\!\\!\\!&=&\textsf{map}(\textsf{filter}(Gs,\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})~{}\text{where}\\\ &&\quad
Gs=\textsf{map}(\text{Dedup}(Q,\vec{E}),\lambda y.\textsf{filter}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda z.\text{Eval}(\vec{E},[z])=y)),\\\
&&\quad\text{Dedup}(Q,\vec{E})=\textsf{foldr}(\lambda x.\lambda
xs.\textsf{cons}(x,\textsf{filter}(xs,\lambda y.x\neq
y)),[],\textsf{map}(\llbracket Q\rrbracket_{\mathcal{D}},\lambda
z.\text{Eval}(\vec{E},[z]))),\\\
&&\quad\text{Eval}(\vec{E},xs)=\textsf{map}(\vec{E},\lambda e.\llbracket
e\rrbracket_{\mathcal{D},xs})\\\
\llbracket\text{With}(\vec{Q},\vec{R},Q)\rrbracket_{\mathcal{D}}&=&\llbracket
Q\rrbracket_{\mathcal{D}^{\prime}}~{}\text{where}~{}\mathcal{D}^{\prime}=\mathcal{D}[R_{i}\mapsto\llbracket
Q_{i}\rrbracket_{\mathcal{D}}~{}|~{}R_{i}\in\vec{R}]\\\
\llbracket\text{OrderBy}(Q,\vec{E},b)\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,[\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{D}}-xs)])),[],\llbracket
Q\rrbracket_{\mathcal{D}})~{}\text{where}\\\
&&\quad\text{MinTuple}(\vec{E},b,xs)=\textsf{foldl}(\lambda x.\lambda
y.\textsf{ite}(\text{Cmp}(\vec{E},b,x,y),y,x),\textsf{head}(xs),xs),\\\
&&\quad\text{Cmp}(\vec{E},b,x_{1},x_{2})=b\neq\textsf{foldr}(\lambda
E_{i}.\lambda y.\textsf{ite}(v(x_{1},E_{i})<v(x_{2},E_{i}),\top,\\\
&&\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\textsf{ite}(v(x_{1},E_{i})>v(x_{2},E_{i}),\bot,y)),\top,\vec{E}),\\\
&&\quad v(x,E)=\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[x]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{D},[x]})\\\ \end{array}$

Figure 5. Formal semantics of SQL queries. ite is the standard if-then-else
function. $\textsf{hasAgg}(L)$ checks if the attribute list $L$ has an
attribute computing an aggregation. $\textsf{merge}(x,y)$ merges two tuples
$x$ and $y$ into one tuple. $\textsf{rename}(R,n)$ replaces all occurrences of
the original table name $R$ with the new globally unique name $n$.
$T_{\text{Null}}$ represents a tuple of Null’s, whose length is determined as
appropriate by the context for brevity. Note that $xs-x$ on the right-hand
side of $\llbracket Q_{1}-Q_{2}\rrbracket_{\mathcal{D}}$ denotes deleting one
tuple $x$ in $xs$ iff $xs\in x$. Full formal semantics of all constructs in
our query language, including predicates
$\llbracket\phi\rrbracket_{\mathcal{D},xs}$, attribute lists $\llbracket
L\rrbracket_{\mathcal{D},xs}$, and expressions $\llbracket
e\rrbracket_{\mathcal{D},xs}$ is available in Appendix A .

The denotational semantics of our SQL queries is presented in Figure 5, where
$\llbracket Q\rrbracket$ takes as an input a database $\mathcal{D}$ and
produces as output a relation.

_Bag and list semantics._ As is standard in SQL, we conceptually view a
relation as a bag (multiset) of tuples and use the bag semantics for queries.
However, our denotational semantics in Figure 5 uses lists to implement bags
and define query operators through higher-order combinators such as map,
filter, and foldl. In this way, we can easily define complex query operators
and switch to list semantics when the query needs to sort the result using
ORDER BY.

_Three-valued semantics._ Similar to standard SQL, our semantics also uses
three-valued logic. More specifically, a relation may use NULL values to
represent unknown information, and all query operators should behave correctly
with respect to the NULL value. For example, our semantics considers a
predicate can be evaluated to three possible values, namely $\top$ (true),
$\bot$ (false), and Null. A notation like
$\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top$ means the predicate $\phi$
evaluates to true (not false nor Null) given database $\mathcal{D}$ and tuples
$xs$. 444Detailed definition of predicate semantics is available in Appendix
A.

_Basics._ At a high level, our denotational semantics can be viewed as a
function or a functional program $\llbracket Q\rrbracket_{\mathcal{D}}$ that
pattern matches different constructors of query $Q$ and evaluates them to
relations given a concrete database $\mathcal{D}$. If the query is a relation
name $R$, then $\llbracket R\rrbracket_{\mathcal{D}}$ simply looks up the name
$R$ in $\mathcal{D}$. If the query is a projection,
$\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}$ first checks if the attribute
list $L$ includes aggregation functions. If so, it evaluates query $Q$ and
invokes $\llbracket L\rrbracket_{\mathcal{D},\llbracket
Q\rrbracket_{\mathcal{D}}}$ to compute the aggregate values. Otherwise, it
projects each tuple in the result of $\llbracket Q\rrbracket_{\mathcal{D}}$
according to $L$ through a standard map combinator. If the query is renaming,
$\llbracket\rho_{R}(Q)\rrbracket_{\mathcal{D}}$ first evaluates $\llbracket
Q\rrbracket_{\mathcal{D}}$. Then for each tuple in the result, it updates the
attribute name $n$ to be a new name $\textsf{rename}(R,n)$ that is related to
relation name $R$. Following similar ideas of functional programming, we can
define semantics for filtering $\sigma$, set operations $\cap,\cup,\setminus$,
bag operations
$\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}},\uplus,-$, and
Distinct for removing duplicated tuples.

_Cartesian product and joins._ Apart from the standard Cartesian product
$Q_{1}\times Q_{2}$, there are four different joins in our language. An _inner
join_ $Q_{1}\bowtie_{\phi}Q_{2}$ can be viewed as a syntactic sugar of
$\sigma_{\phi}(Q_{1}\times Q_{2})$. A _left outer join_
$Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}$ is
more involved. $\llbracket Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}Q_{2}\rrbracket_{\mathcal{D}}$
iterates tuples in the result of $\llbracket Q_{1}\rrbracket_{\mathcal{D}}$
and for each tuple $x$, it computes the inner join of $[x]$ and $Q_{2}$ and
denotes the result by $v_{1}(x)$. If $v_{1}(x)$ is not empty, it is appended
to the final result of the left outer join. Otherwise, $\llbracket
Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}Q_{2}\rrbracket_{\mathcal{D}}$
computes a _null extension_ $v_{2}(x)$ of $x$ by taking the Cartesian product
between $x$ and $T_{\textsf{Null}}$ (a tuple of Null values) and appends
$v_{2}(x)$ to the result. Similarly, a _right outer join_
$Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q_{2}$ can be defined in the
same way. For _full outer join_ , $\llbracket
Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}$
starts with the left outer join
$Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}$.
Then for each tuple $y$ in $\llbracket Q_{2}\rrbracket_{\mathcal{D}}$, if the
inner join between $Q_{1}$ and $[y]$ returns empty, $\llbracket
Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}$
adds a null extension $\textsf{merge}(T_{\text{Null}},y)$ to the result.

###### Example 3.2.

Consider the following two relations EMP and DEPT. What follows illustrates
the difference in the results of various joins and their Cartesian product.

eid | ename | did
---|---|---
1 | A | 11
2 | B | 12
EMP

id | dname
---|---
10 | C
11 | D
DEPT

eid | ename | did | id | dname
---|---|---|---|---
1 | A | 11 | 11 | D
$\texttt{EMP}\bowtie_{\texttt{did=id}}\texttt{DEPT}$

eid | ename | did | id | dname
---|---|---|---|---
1 | A | 11 | 11 | D
2 | B | 12 | NULL | NULL
$\texttt{EMP}\mathbin{\rule[0.36597pt]{1.25pt}{0.6pt}\hbox
to0.0pt{\hss\rule[1.89444pt]{1.25pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\texttt{did=id}}\texttt{DEPT}$

eid | ename | did | id | dname
---|---|---|---|---
NULL | NULL | NULL | 10 | C
1 | A | 11 | 11 | D
$\texttt{EMP}\mathbin{\bowtie\mkern-5.8mu\rule[0.36597pt]{1.25pt}{0.6pt}\hbox
to0.0pt{\hss\rule[1.89444pt]{1.25pt}{0.6pt}}}_{\texttt{did=id}}\texttt{DEPT}$

eid | ename | did | id | dname
---|---|---|---|---
1 | A | 11 | 11 | D
2 | B | 12 | NULL | NULL
NULL | NULL | NULL | 10 | C
$\texttt{EMP}\mathbin{\rule[0.36597pt]{1.25pt}{0.6pt}\hbox
to0.0pt{\hss\rule[1.89444pt]{1.25pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.36597pt]{1.25pt}{0.6pt}\hbox
to0.0pt{\hss\rule[1.89444pt]{1.25pt}{0.6pt}}}_{\texttt{did=id}}\texttt{DEPT}$

eid | ename | did | id | dname
---|---|---|---|---
1 | A | 11 | 10 | C
1 | A | 11 | 11 | D
2 | B | 12 | 10 | C
2 | B | 12 | 11 | D
$\texttt{EMP}\times\texttt{DEPT}$

_GroupBy._ To define the semantics of $\text{GroupBy}(Q,\vec{E},L,\phi)$, we
use several auxiliary functions. Specifically, $\text{Eval}(\vec{E},xs)$
computes the values of expressions $\vec{E}$ to be grouped over tuple list
$xs$, and $\text{Dedup}(Q,\vec{E})$ invokes Eval to retain only unique values
of $\vec{E}$. Then GroupBy maps each unique $\vec{E}$ value to a group of
tuples sharing the same value over $\vec{E}$ and obtains all groups $Gs$. It
evaluates the HAVING condition $\phi$ and only retains those groups satisfying
$\phi$ by the filter combinator. Finally, for each retained group $xs$,
GroupBy computes an aggregate value $\llbracket L\rrbracket_{\mathcal{D},xs}$
and adds it to the result.

_With clause._ To evaluate $\text{With}(\vec{Q},\vec{R},Q)$, our semantics
first evaluates all subqueries $Q_{i}\in\vec{Q}$, then creates a new database
$\mathcal{D}^{\prime}$ by adding mappings $R_{i}\mapsto\llbracket
Q_{i}\rrbracket_{\mathcal{D}}$, and finally evaluates $Q$ under
$\mathcal{D}^{\prime}$. Intuitively, the With clause creates local bindings
for subqueries $Q_{i}$ which can be used in query $Q$.

_OrderBy._ We define a deterministic semantics for the OrderBy construct in
our language, i.e., two runs of OrderBy with the same arguments always return
the same result. Specifically, $\text{OrderBy}(Q,\vec{E},\\\ $$b)$ performs a
selection sort on the results of $\llbracket Q\rrbracket_{\mathcal{D}}$ by
expressions $\vec{E}$. The sorted results are in ascending order if $b=\top$
and in descending order if $b=\bot$. At a high level, OrderBy maintains a list
of sorted tuples in ascending (resp. descending) order and repeatedly selects
the minimum (resp. maximum) tuple from the unsorted tuples using the MinTuple
function. In particular, MinTuple invokes the Cmp function for pair-wise
comparison of two tuples $x_{1}$ and $x_{2}$ over expression list $\vec{E}$.
Null is viewed as a special value $-\infty$ that is smaller than any other
values, so Null’s can also be ordered correctly by our semantics.

_Our language vs. prior work’s._ Our formal semantics is inspired by prior
work such as Mediator (Wang et al., 2018b). While Mediator defines semantics
for simple update and query operators, our semantics defines more complex
query operators, including outer joins, GROUP BY, WITH, and ORDER BY.
Furthermore, to our best knowledge, our semantics considers many operators
that are important in practice but not considered in any prior work such as
ORDER BY, WITH, IF, INTERSECT, EXCEPT, etc. In addition, our work supports
complex attribute expressions and predicates, such as Avg(age + 10), whereas
prior work has very limited support for such features.

###  3.4. Integrity Constraints

Integrity constraints are fundamental to data integrity and therefore must be
followed by a database. In this paper, we support the constraints shown in
Figure 7. In particular, an integrity constraint consists of a set of
primitive constraints, detailed as follows.

_Primary keys._ $\text{PK}(R,\vec{a})$ says that a list of attributes
$\vec{a}$ is the primary key of relation $R$. In particular, it requires that
all values of any attribute in $\vec{a}$ are not NULL. Furthermore, given two
different tuples $t_{1},t_{2}\in R$, $t_{1}$ and $t_{2}$ must have different
values on at least one attribute in $\vec{a}$.

_Foreign keys._ $\text{FK}(R_{1},a_{1},R_{2},a_{2})$ means that the attribute
$a_{1}$ of relation $R_{1}$ is a foreign key referencing the attribute $a_{2}$
of relation $R_{2}$. Specifically, it requires that, for each tuple $t_{1}\in
R_{1}$, there exists a tuple $t_{2}\in R_{2}$ such that
$t_{1}.a_{1}=t_{2}.a_{2}$.

$\begin{array}[]{rcl}\text{Constraint}~{}\mathcal{C}&::=&\text{PK}(R,\vec{a})~{}|~{}\text{FK}(R,a,R,a)~{}|~{}\text{NotNull}(R,a)~{}|~{}\text{Check}(R,\psi)~{}|~{}\text{Inc}(R,a,v)~{}|~{}\mathcal{C}\land\mathcal{C}\\\
\text{Pred}~{}\psi&::=&a\odot v~{}|~{}a\odot
a~{}|~{}a\in\vec{v}~{}|~{}\psi\land\psi~{}|~{}\psi\lor\psi~{}|~{}\neg\psi\\\
\text{Logic
Op}~{}\odot&::=&\leq~{}|~{}<~{}|~{}=~{}|~{}\neq~{}|~{}>~{}|~{}\geq\end{array}$

$R\in\textbf{Relations}\qquad a\in\textbf{Attributes}\qquad
v\in\textbf{Values}$

Figure 7. Syntax of Integrity Constraints.

_Not-null constraints._ NotNull(R, a) imposes a NOT NULL constraint on the
attribute $a$ of relation $R$. It stipulates that for each tuple $t\in R$,
$t.a$ is not NULL.

_Check constraints._ $\text{Check}(R,\psi)$ requires that every tuple $t\in R$
must satisfy the predicate $\psi$, where $\psi$ can be a boolean combination
of atomic predicates. Each atomic predicate can be logical comparisons between
two attributes of $R$, between an attribute and a constant value. or of the
form $a\in\vec{v}$ meaning the value of attribute $a$ is in a list of provided
constants $\vec{v}$.

_Auto increment._ $\text{Inc}(R,a,v)$ means that the value of attribute $a$ in
relation $R$ starts with $v$ and strictly increases by one for each new tuple
added to $R$. We require the value to strictly increase by one to obtain a
deterministic semantics of the auto increment constraint. However, this is not
a fundamental limitation. We can easily generalize to the scenarios where
values are not continuous.

###  3.5. Problem Statement

To describe our problem statement, we start with a notion of conformance
between a relational database and its schema. Specifically, an attribute value
$(a,v)$ conforms to an attribute schema $(b,\tau)$, denoted
$(a,v)::_{A}(b,\tau)$, if $a=b$ and $v$ is of type $\tau$. 555Null is viewed
as a polymorphic value of both type Int and Bool. A tuple $t$ conforms to a
relation schema $RS$, denoted $t::_{T}RS$, if (1) they have the same size,
i.e. $|t|=|RS|$ and (2) each attribute value $(a_{i},v_{i})$ in $T$ is
conforming to the corresponding attribute schema $(b_{i},\tau_{i})$ in $RS$.

###### Definition 3.3 (Conformance between Database and Schema).

A database $\mathcal{D}$ conforms to a schema $\mathcal{S}$, denoted
$\mathcal{D}::\mathcal{S}$, if (1) $\mathcal{D}$ and $\mathcal{S}$ have the
same domain and (2) for each relation name $R\in\textsf{Dom}(\mathcal{D})$,
all tuples in $\mathcal{D}(R)$ conform to their corresponding relation schema
$\mathcal{S}(R)$, i.e.,

$\mathcal{D}::\mathcal{S}\overset{\mathrm{def}}{=\joinrel=}\textsf{Dom}(\mathcal{D})=\textsf{Dom}(\mathcal{S})\land(\forall
R\in\textsf{Dom}(\mathcal{D}).\forall t\in R.~{}t::_{T}\mathcal{S}(R))$

Recall from Figure 3 that we only consider Int and Bool types in this paper.
Other types of values (e.g., strings and dates) can be treated as integers and
functions involving those types can be treated as uninterpreted functions over
integers.

###### Example 3.4.

Let schema
$\mathcal{S}=[\texttt{EMP}\mapsto[(\texttt{eid},Int),(\texttt{cid},Int)],\texttt{CAR}\mapsto[(\texttt{id},Int),(\texttt{used},Bool)]]$
and database

$\begin{array}[]{rl}\mathcal{D}=[&\texttt{EMP}\mapsto[[(\texttt{eid},1),(\texttt{cid},10)],[(\texttt{eid},2),(\texttt{cid},\texttt{NULL})]],\\\
&\texttt{CAR}\mapsto[(\texttt{id},10),(\texttt{used},\top)]\quad]\\\
\end{array}$

Here, $\mathcal{D}::\mathcal{S}$ because
$[(\texttt{eid},1),(\texttt{cid},10)]::_{T}[(\texttt{eid},Int),(\texttt{cid},Int)]$
and
$[(\texttt{eid},2),(\texttt{cid},\texttt{NULL})]::_{T}[(\texttt{eid},Int),(\texttt{cid},Int)]$
hold for relation name EMP and
$[(\texttt{id},10),(\texttt{used},\top)]::_{T}[(\texttt{id},Int),(\texttt{used},\\\
$$Bool)]$ holds for relation name CAR.

###### Definition 3.5 (Bounded Equivalence modulo Integrity Constraint).

Given two queries $(Q_{1},Q_{2})$ under schema $\mathcal{S}$ and a positive
integer bound $N$, $Q_{1}$ and $Q_{2}$ are said to be _bounded equivalent
modulo integrity constraint_ $\mathcal{C}$, denoted by
$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$, if for any database
$\mathcal{D}$ that conforms to schema $\mathcal{S}$ satisfies $\mathcal{C}$
and each relation has at most $N$ tuples, the execution result of $Q_{1}$ is
the same as the execution result of $Q_{2}$ on $\mathcal{D}$, i.e.,

$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}\overset{\mathrm{def}}{=\joinrel=}\forall\mathcal{D}.~{}\mathcal{D}::\mathcal{S}\land(\forall
R\in\mathcal{D}.~{}|R|\leq
N)\land\mathcal{C}(\mathcal{D})\Rightarrow\llbracket
Q_{1}\rrbracket_{\mathcal{D}}=\llbracket Q_{2}\rrbracket_{\mathcal{D}}$

##  4\. Bounded Equivalence Verification Modulo Integrity Constraints

This section presents our algorithm for bounded equivalence verification of
two queries modulo integrity constraints.

###  4.1. Algorithm Overview

The top-level algorithm of our verification technique is shown in Algorithm 1.
The Verify procedure takes as input two queries $Q_{1}$ and $Q_{2}$ over
schema $\mathcal{S}$, an integrity constraint $\mathcal{C}$, and a bound $N$
on the size of all relations in the database. It returns $\top$ indicating
$Q_{1}$ and $Q_{2}$ are bounded equivalent modulo integrity constraint
$\mathcal{C}$, i.e., $Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$.
Otherwise, it returns a counterexample database satisfying $\mathcal{C}$ where
$Q_{1}$ and $Q_{2}$ yield different results.

Algorithm 1 Equivalence Verification

1:procedure Verify($Q_{1},Q_{2},\mathcal{S},\mathcal{C},N$)

2:Input: Queries $Q_{1},Q_{2}$, schema $\mathcal{S}$, integrity constraint
$\mathcal{C}$, and bound size $N$

3:Output: $\top$ for equivalence, otherwise a counterexample

4: $\Gamma\leftarrow\textsf{BuildSymbolicDB}(\mathcal{S},N)$;

5:
$\Phi_{\mathcal{C}}\leftarrow\textsc{EncodeConstraint}(\Gamma,\mathcal{C})$;

6:
$\Phi_{R_{1}},R_{1}\leftarrow\textsc{EncodeQuery}(\mathcal{S},\Gamma,Q_{1})$;

7:
$\Phi_{R_{2}},R_{2}\leftarrow\textsc{EncodeQuery}(\mathcal{S},\Gamma,Q_{2})$;

8:
$\Phi\leftarrow\Phi_{\mathcal{C}}\land\Phi_{R_{1}}\land\Phi_{R_{2}}\land\neg\textsc{Equal}(R_{1},R_{2})$;

9: if UNSAT($\Phi$) then return $\top$;

10: else return BuildExample($\mathcal{S}$, Model($\Phi$));

At a high-level, our technique reduces the verification problem into a
constraint-solving problem and generates an SMT formula through the encoding
of integrity constraints and SQL operations. Specifically, we first create a
symbolic representation of the database $\Gamma$, where each relation has at
most $N$ tuples (Line 2). Then we encode the integrity constraint
$\mathcal{C}$ over $\Gamma$ and obtain an SMT formula $\Phi_{\mathcal{C}}$
(Line 3). Next, we analyze queries $Q_{1},Q_{2}$ to obtain their outputs
$R_{1},R_{2}$ given input $\Gamma$ and two SMT formulas
$\Phi_{R_{1}},\Phi_{R_{2}}$ encoding how $R_{1},R_{2}$ are computed from
$\Gamma$ (Lines 4 – 5). Finally, we build a formula $\Phi$ asserting the
existence of a database satisfying the integrity constraint $\mathcal{C}$ such
that $R_{1}$ is different from $R_{2}$ (Line 6). If no such database exists
(i.e., formula $\Phi$ is unsatisfiable), then $Q_{1}$ and $Q_{2}$ are bounded
equivalent modulo integrity constraint $\mathcal{C}$, i.e.,
$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$ (Line 7). Otherwise, if such a
database exists, $Q_{1}$ and $Q_{2}$ are not equivalent, so we build a
counterexample database from a model of $\Phi$ to disprove the equivalence
(Line 8).

###  4.2. Schema and Symbolic Database

Since our verification technique is centered around a symbolic representation
of the database, we first describe how to build the symbolic database.

_Symbolic database._ Given a schema $\mathcal{S}$ and a bound $N$ for the size
of relations, we build a symbolic database containing all relations in
$\textsf{Dom}(\mathcal{S})$ and each relation has $N$ symbolic tuples. We
denote the symbolic database by $\Gamma$ where
$\Gamma:\text{RelName}\to[\text{SymTuple}]$ maps relation names to their
corresponding lists of symbolic tuples. In general, we introduce an
uninterpreted predicate $\text{Del}(t)$ for each tuple $t$ to indicate whether
or not $t$ is deleted by subquery. 666 Alternatively, we can introduce a
predicate $\textsf{Present}(t)$ to indicate a tuple is indeed present, i.e.,
$\textsf{Present}(t)\Leftrightarrow\neg\text{Del}(t)$.  Since the Del
predicates hold non-deterministic values in the symbolic database, we can use
$\Gamma$ to encode all possible databases where each relation has _at most_
$N$ tuples.

###### Example 4.1.

Consider again the schema $\mathcal{S}$ in Example 3.4. Given a bound $N=2$,
we can build a symbolic database
$\Gamma=\\{\texttt{EMP}\mapsto[t_{1},t_{2}],\texttt{CAR}\mapsto[t_{3},t_{4}]\\}$,
where $t_{1},t_{2},t_{3},t_{4}$ are symbolic tuples.

_Encoding attributes._ As is standard, we use uninterpreted functions to
encode attributes. Specifically, for each attribute $attr$ in the database
schema, we introduce an uninterpreted function called $attr$ that takes as
input a symbolic tuple and produces as output a symbolic value. For example,
$t.name$ for getting the $name$ attribute of tuple $t$ should be encoded as
$name(t)$ where $name$ is an uninterpreted function.

_Encoding NULL._ To support NULL and three-valued semantics, we encode each
symbolic value as a pair $(b,v)$ in the SMT formula, where $b$ is a boolean
variable indicating whether the value is NULL, and $v$ is a non-NULL value. In
particular, if $b$ is $\top$ (i.e., true), then the value $(b,v)$ is NULL.
Otherwise, if $b$ is $\bot$ (i.e., false), the value is $v$. For example,
constant 1 is represented by $(\bot,1)$. In this way, NULL is not equal to any
legitimate non-NULL values. Furthermore, we consider all the null values are
equal. Although we allow different representations of null values like
$(\top,1)$ and $(\top,2)$, they are considered equal because both of them are
considered to be NULL.

###  4.3. Encoding Integrity Constraints

$\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma(R)=[t_{1},\ldots,t_{n}]\quad\Phi_{1}=\land_{i=1}^{n}\land_{k=1}^{m}t_{i}.a_{k}\neq\text{Null}\\\ m=|\vec{a}|\quad\Phi_{2}=\land_{i=1}^{n}\land_{j=i+1}^{n}\neg(\land_{k=1}^{m}t_{i}.a_{k}=t_{j}.a_{k})\\\ \end{array}}{\vphantom{,}\Gamma\vdash\text{PK}(R,\vec{a})\rightsquigarrow\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(IC-PK)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma(R_{1})=[t_{1},\ldots,t_{n}]\\\ \Gamma(R_{2})=[t^{\prime}_{1},\ldots,t^{\prime}_{m}]\\\ \Phi=\land_{i=1}^{n}\lor_{j=1}^{m}t_{i}.a_{1}=t^{\prime}_{j}.a_{2}\\\ \end{array}}{\vphantom{,}\Gamma\vdash\text{FK}(R_{1},a_{1},R_{2},a_{2})\rightsquigarrow\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(IC-FK)}\end{array}\par\mkern-2.0mu\\\ \\\ \mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma(R)=[t_{1},\ldots,t_{n}]\quad\Phi=\land_{i=1}^{n}t_{i}.a\neq\text{Null}\\\ \end{array}}{\vphantom{,}\Gamma\vdash\text{NotNull}(R,a)\rightsquigarrow\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(IC-NN)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma(R)=[t_{1},\ldots,t_{n}]\quad\Phi=\land_{i=1}^{n}\llbracket\psi\rrbracket_{t_{i}}\\\ \end{array}}{\vphantom{,}\Gamma\vdash\text{Check}(R,\psi)\rightsquigarrow\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(IC-Check)}\end{array}\par\mkern-2.0mu\\\ \\\ \mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma(R)=[t_{1},\ldots,t_{n}]\\\ \Phi_{1}=\land_{i=1}^{n}t_{i}.a=v+i-1\quad\Phi_{2}=\land_{i=1}^{n}t_{i}.a\neq\text{Null}\\\ \end{array}}{\vphantom{,}\Gamma\vdash\text{Inc}(R,a,v)\rightsquigarrow\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(IC-Inc)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash\mathcal{C}_{1}\rightsquigarrow\Phi_{1}\\\ \Gamma\vdash\mathcal{C}_{2}\rightsquigarrow\Phi_{2}\\\ \end{array}}{\vphantom{,}\Gamma\vdash\mathcal{C}_{1}\land\mathcal{C}_{2}\rightsquigarrow\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(IC-Comp)}\end{array}\par\mkern-2.0mu\end{array}$ Figure 8. Symbolic encoding of integrity constraints. $\llbracket a\odot v\rrbracket_{t}$ | = | $t.a\neq\text{Null}\land t.a\odot v$ |  | $\llbracket\psi_{1}\land\psi_{2}\rrbracket_{t}$ | = | $\llbracket\psi_{1}\rrbracket_{t}\land\llbracket\psi_{2}\rrbracket_{t}$
---|---|---|---|---|---|---
$\llbracket a_{1}\in\vec{v}\rrbracket_{t}$ | = | $t.a\neq\text{Null}\land\bigvee_{i=1}^{|\vec{v}|}t.a=v_{i}$ |  | $\llbracket\psi_{1}\lor\psi_{2}\rrbracket_{t}$ | = | $\llbracket\psi_{1}\rrbracket_{t}\lor\llbracket\psi_{2}\rrbracket_{t}$
$\llbracket a_{1}\odot a_{2}\rrbracket_{t}$ | = | $t.a_{1}\odot t.a_{2}~{}\text{where}~{}\odot\in\\{=,\neq\\}$ |  | $\llbracket\neg\psi\rrbracket_{t}$ | = | $\neg\llbracket\psi\rrbracket_{t}$
$\llbracket a_{1}\odot a_{2}\rrbracket_{t}$ | = | $t.a_{1}\neq\text{Null}\land t.a_{2}\neq\text{Null}\land t.a_{1}\odot t.a_{2}~{}\text{where}~{}\odot\in\\{\leq,<,>,\geq\\}$
Figure 9. Symbolic encoding of predicates in integrity constraints.

Given a symbolic database $\Gamma$ and an integrity constraint $\mathcal{C}$,
we follow the semantics of $\mathcal{C}$ to encode $\mathcal{C}$ as an SMT
formula over $\Gamma$. The encoding procedure is summarized as inference rules
in Figure 8, where judgments of the form
$\Gamma\vdash\mathcal{C}\rightsquigarrow\Phi$ represent that the encoding of
integrity constraint $\mathcal{C}$ is $\Phi$ given a symbolic database
$\Gamma$.

In a nutshell, we encode each atomic integrity constraint in $\mathcal{C}$ and
conjoin the formulas together according to the IC-Comp rule. Specifically, the
IC-PK rule specifies that the encoding of a primary key constraint
$\text{PK}(R,a)$ consists of two parts: $\Phi_{1}$ asserting all attributes in
the primary key have no NULL values, and $\Phi_{2}$ stating for any pair of
tuples $t_{1}$ and $t_{2}$ where $t_{1}\neq t_{2}$, they do not agree on all
attributes in $\vec{a}$. For $\text{FK}(R_{1},a_{1},R_{2},a_{2})$ where
$R_{1}.a_{1}$ is a foreign key referencing $R_{2}.a_{2}$, the IC-FK rule looks
up the symbolic database $\Gamma$ and finds the tuples for $R_{1}$ are
$t_{1},\ldots,t_{n}$ and the tuples for $R_{2}$ are
$t^{\prime}_{1},\ldots,t^{\prime}_{m}$. The formula asserts that for each
tuple $t_{i}$ in $R_{1}$, there exists a tuple $t^{\prime}_{j}$ in $R_{2}$
such that the value $t_{i}.a_{1}$ is equal to $t^{\prime}_{j}.a_{2}$. The IC-
NN rule simply encodes that $\text{NotNull}(R,a)$ requires that all tuples in
R must have a non-NULL value on attribute a. For the constraint
$\text{Check}(R,\psi)$ that specifies ranges of values, the IC-Check rule uses
an auxiliary function $\llbracket\psi\rrbracket_{t}$ (shown in Figure 9) to
compute the formula of predicate $\psi$ on each tuple $t_{i}$ in $R$ and
obtain the formula by conjoining the $\llbracket\psi\rrbracket_{t}$ formulas
together. For the auto-increment constraint $\text{Inc}(R,a,v)$, the IC-Inc
rule also looks up the symbolic database $\Gamma$ and finds all tuples
$t_{1},\ldots,t_{n}$ of $R$. It then enforces the value of $t_{i}.a$ is not
NULL and that $t_{i}.a=v+i-1$.

###### Lemma 4.2.

777The proof of all lemmas and theorems can be found in Appendix D.

Given a symbolic database $\Gamma$ and an integrity constraint $\mathcal{C}$,
consider a formula $\Phi$ such that
$\Gamma\vdash\mathcal{C}\rightsquigarrow\Phi$. If $\Phi$ is satisfiable, then
the model of $\Phi$ corresponds to a database consistent with $\Gamma$ that
satisfies $\mathcal{C}$. If $\Phi$ is unsatisfiable, then no database
consistent with $\Gamma$ satisfies $\mathcal{C}$.

###  4.4. Encoding SQL Queries

To encode the semantics of a query, we traverse the query and encode how each
operator transforms its input to output. Since this process requires the
attributes and symbolic tuples of each subquery, we first describe how to
compute attributes and tuples of arbitrary intermediate subqueries, followed
by the encoding of all query operators.

####  4.4.1. Attributes of Intermediate Subqueries

$\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{R\in
dom(\mathcal{S})}{\vphantom{,}\mathcal{S}\vdash
R:\mathcal{S}(R)}&\\!\\!\\!\\!\\!\\!\textrm{(A-Rel)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\\\ \forall e\in L.\forall
a\in\text{Attrs}(e).~{}a\in\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\Pi_{L}(Q):L}&\\!\\!\\!\\!\\!\\!\textrm{(A-Proj)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q_{1}:\mathcal{A}_{1}\quad\mathcal{S}\vdash Q_{2}:\mathcal{A}_{2}\\\
\otimes\in\\{\times,\bowtie_{\phi},\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi},\mathbin{\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi},\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}\\}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash Q_{1}\otimes
Q_{2}:\mathcal{A}_{1}+\\!+~{}\mathcal{A}_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Join)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\quad\mathcal{A}^{\prime}=[\text{rename}(R,a)~{}|~{}a\in\mathcal{A}]\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\rho_{R}(Q):\mathcal{A}^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Rename)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\sigma_{\phi}(Q):\mathcal{A}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Filter)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\text{GroupBy}(Q,\vec{E},L,\phi):\mathcal{A}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Group)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\text{OrderBy}(Q,\vec{E},b):\mathcal{A}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Order)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q:\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash\text{Distinct}(Q):\mathcal{A}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Dist)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\oplus\in\\{\cup,\cap,\setminus,\uplus,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}},-\\}\\\
\mathcal{S}\vdash Q_{1}:\mathcal{A}\quad\mathcal{S}\vdash Q_{2}:\mathcal{A}\\\
\end{array}}{\vphantom{,}\mathcal{S}\vdash Q_{1}\oplus
Q_{2}:\mathcal{A}}&\\!\\!\\!\\!\\!\\!\textrm{(A-Coll)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q_{i}:\mathcal{A}_{i}\quad 1\leq i\leq n\quad n=|\vec{Q}|=|\vec{R}|\\\
\mathcal{S}[R_{1}\mapsto\mathcal{A}_{1},\ldots,R_{n}\mapsto\mathcal{A}_{n}]\vdash
Q^{\prime}:\mathcal{A}^{\prime}\end{array}}{\vphantom{,}\mathcal{S}\vdash\text{With}(\vec{Q},\vec{R},Q^{\prime}):\mathcal{A}^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(A-With)}\end{array}\par\par\par\mkern-2.0mu\end{array}$
Figure 10. Rules for inferring the attributes of a query result. As is
standard in SQL, the name of an attribute expression is assumed to be a
function over all attributes involved in the expression. For example, the name
of attribute expression $\text{Avg}(a)$ is a string Avg_a.

While the database schema describes the attributes of each relation in the
_initial_ database, it does not directly give the attributes of those
intermediate query results. To infer the attributes of each intermediate
subquery, we develop an algorithm for all query operations in our SQL
language. The algorithm is summarized as a set of inference rules, shown in
Figure 10. Intuitively, our rules for inferring attributes are similar to the
traditional typing rules. The judgments of the form $\mathcal{S}\vdash
Q:\mathcal{A}$ mean the attributes of query $Q$ is $\mathcal{A}$ under schema
$\mathcal{S}$.

Specifically, the attributes of a relation in the initial database can be
obtained by looking up the schema $\mathcal{S}$ directly (A-Rel). To find all
attributes of a projection $\Pi_{L}(Q)$, the A-Proj rule first computes the
attribute list $\mathcal{A}$ of query $Q$ and then checks if all attributes
occurring in the attribute expression list $L$ belong to $\mathcal{A}$. If so,
the attributes of $\Pi_{L}(Q)$ are $L$ with all attribute expressions
converted to the corresponding attribute names, e.g., Avg(a) to Avg_a.
Otherwise, there is a type error in the query. For Cartesian product or any
join operator $\otimes$, the attributes of $Q_{1}\otimes Q_{2}$ are obtained
by concatenating the attributes of $Q_{1}$ and those of $Q_{2}$ (A-Join). The
renaming operation $\rho_{R}(Q)$ first computes the attributes of $Q$ and then
renames each of them according to the new relation name $R$ in the result
(A-Rename). Based on the A-Filter, A-Group, A-Order, and A-Dist rules, the
filtering, GroupBy, OrderBy, and Distinct operations do not change the
attribute list. The A-Coll rule specifies that for any collection operator
$\oplus$, the attributes of its two operands $Q_{1}$ and $Q_{2}$ must be the
same, which are also identical to the attributes of $Q_{1}\oplus Q_{2}$. The
inference rule for a WITH clause $\text{With}(\vec{Q},\vec{R},Q^{\prime})$ is
slightly more involved. Since the query $Q^{\prime}$ can use $R_{i}$ to refer
to the results of a subquery $Q_{i}$, the A-With rule first infers the
attributes $\mathcal{A}_{i}$ of each subquery $Q_{i}$ and then augments the
schema $\mathcal{S}$ to a temporary new schema $\mathcal{S}^{\prime}$ by
adding entries $R_{i}\mapsto\mathcal{A}_{i}$. Finally, the attributes of query
$Q^{\prime}$ (and the whole WITH clause) are inferred based on the schema
$\mathcal{S}^{\prime}$.

####  4.4.2. Symbolic Tuples of Intermediate Subqueries.

$\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}R\in
dom(\Gamma)\\\ \end{array}}{\vphantom{,}\Gamma\vdash
R\hookrightarrow\Gamma(R)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Rel)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\text{hasAgg}(L)\end{array}}{\vphantom{,}\Gamma\vdash\Pi_{L}(Q)\hookrightarrow\sigma(1)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Agg)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\neg\text{hasAgg}(L)\quad\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\Pi_{L}(Q)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Proj)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\sigma_{\phi}(Q)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Filter)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\rho_{R}(Q)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Rename)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{1}\hookrightarrow\mathcal{T}_{1}\quad\Gamma\vdash
Q_{2}\hookrightarrow\mathcal{T}_{2}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\times
Q_{2}\hookrightarrow\sigma(|\mathcal{T}_{1}|\cdot|\mathcal{T}_{2}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Prod)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash\sigma_{\phi}(Q_{1}\times
Q_{2})\hookrightarrow\mathcal{T}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\hookrightarrow\mathcal{T}}&\\!\\!\\!\\!\\!\\!\textrm{(T-IJoin)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\hookrightarrow\mathcal{T}_{1}\\\ \Gamma\vdash
Q_{1}\hookrightarrow\mathcal{T}_{2}\\\
\mathcal{T}^{\prime}=\mathcal{T}_{1}+\\!+~{}\sigma(|\mathcal{T}_{2}|)\\\
\end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\hookrightarrow\mathcal{T}^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(T-LJoin)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\hookrightarrow\mathcal{T}_{1}\\\ \Gamma\vdash
Q_{2}\hookrightarrow\mathcal{T}_{2}\\\
\mathcal{T}^{\prime}=\mathcal{T}_{1}+\\!+~{}\sigma(|\mathcal{T}_{2}|)\\\
\end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}Q_{2}\hookrightarrow\mathcal{T}^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(T-RJoin)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\hookrightarrow\mathcal{T}_{1}\quad\Gamma\vdash
Q_{1}\hookrightarrow\mathcal{T}_{2}\quad\Gamma\vdash
Q_{2}\hookrightarrow\mathcal{T}_{3}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}Q_{2}\hookrightarrow\mathcal{T}_{1}+\\!+~{}\sigma(|\mathcal{T}_{2}|+|\mathcal{T}_{3}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-FJoin)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\text{Distinct}(Q)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Dist)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\text{GroupBy}(Q,\vec{E},L,\phi)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-GroupBy)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow\mathcal{T}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\text{OrderBy}(Q,\vec{E},b)\hookrightarrow\sigma(|\mathcal{T}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-OrderBy)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\oplus\in\\{\cap,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}\\}\quad\Gamma\vdash
Q_{1}\hookrightarrow\mathcal{T}_{1}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\oplus
Q_{2}\hookrightarrow\sigma(|\mathcal{T}_{1}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Intx)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\oplus\in\\{\setminus,-\\}\quad\Gamma\vdash
Q_{1}\hookrightarrow\mathcal{T}_{1}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\oplus
Q_{2}\hookrightarrow\sigma(|\mathcal{T}_{1}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Ex)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\oplus\in\\{\cup,\uplus\\}\\\
\Gamma\vdash Q_{1}\hookrightarrow\mathcal{T}_{1}\quad\Gamma\vdash
Q_{2}\hookrightarrow\mathcal{T}_{2}\\\ \end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\oplus
Q_{2}\hookrightarrow\sigma(|\mathcal{T}_{1}|+|\mathcal{T}_{2}|)}&\\!\\!\\!\\!\\!\\!\textrm{(T-Union)}\end{array}\mkern-2.0mu\par\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{i}\hookrightarrow\mathcal{T}_{i}\quad 1\leq i\leq n\quad
n=|\vec{Q}|=|\vec{R}|\\\
\Gamma[R_{1}\mapsto\mathcal{T}_{1},\ldots,R_{n}\mapsto\mathcal{T}_{n}]\vdash
Q^{\prime}\hookrightarrow\mathcal{T}^{\prime}\\\
\end{array}}{\vphantom{,}\Gamma\vdash\text{With}(\vec{Q},\vec{R},Q^{\prime})\hookrightarrow\mathcal{T}^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(T-With)}\end{array}\par\mkern-2.0mu\\\
\\\ \end{array}$ Figure 11. Rules for inferring the tuples of a query.
$\sigma(n)$ generates a list of $n$ fresh tuples.

Similar to the database schema, a symbolic database $\Gamma$ only describes
those tuples in each relation of the _initial_ database, but it does not
present what tuples are in the result of intermediate subqueries. To obtain
the tuples in each intermediate subquery, we develop a set of inference rules
as shown in Figure 11, where judgments of the form $\Gamma\vdash
Q\hookrightarrow\mathcal{T}$ mean the result of query $Q$ has a list of
symbolic tuples $\mathcal{T}$ given the initial database $\Gamma$.

The goal of these rules is to compute the number (at most) of symbolic tuples
in the result of each intermediate subquery and what are their names, so we
just need to look up the tuples for relations in $\Gamma$ (T-Rel) and generate
fresh tuples for other queries. Specifically, if a projection $\Pi_{L}(Q)$ has
aggregate functions in the attribute expression list $L$, there is only one
tuple in the result (T-Agg). But if the projection $\Pi_{L}(Q)$ does not have
aggregate functions, the number of tuples in the result is the same as that in
$Q$. For filtering $\sigma_{\phi}(Q)$, the T-Filter rule generates the same
number of tuples as $Q$, because the predicate $\phi$ may not filter out any
tuple from $Q$. The T-Rename rule specifies that the renaming operation
$\rho_{R}(Q)$ produces the same number of tuples as $Q$. Given the tuples of
$Q_{1}$ are $\mathcal{T}_{1}$ and the tuples of $Q_{2}$ are $\mathcal{T}_{2}$,
the numbers of fresh tuples for the Cartesian product, inner join, left outer
join, right outer join, and full outer join are
$|\mathcal{T}_{1}|\cdot|\mathcal{T}_{2}|$,
$|\mathcal{T}_{1}|\cdot|\mathcal{T}_{2}|$,
$|\mathcal{T}_{1}|\cdot(|\mathcal{T}_{2}|+1)$,
$(|\mathcal{T}_{1}|+1)\cdot|\mathcal{T}_{2}|$, and
$|\mathcal{T}_{1}|\cdot|\mathcal{T}_{2}|+|\mathcal{T}_{1}|+|\mathcal{T}_{2}|$,
respectively. In addition, the numbers of fresh tuples for union, intersect,
and except operations of $Q_{1}$ and $Q_{2}$ are
$|\mathcal{T}_{1}|+|\mathcal{T}_{2}|$, $|\mathcal{T}_{1}|$, and
$|\mathcal{T}_{1}|$, respectively. According to the T-Dist, T-GroupBy, and
T-OrderBy rules, the Distinct, GroupBy, and OrderBy operation preserves the
number of tuples in their subqueries. Finally, to infer the tuples for
$\text{With}(\vec{Q},\vec{R},Q^{\prime})$, we first need to obtain the tuples
$\mathcal{T}_{i}$ for its subquery $Q_{i}$. Then we create a new symbolic
database $\Gamma^{\prime}$ by adding mappings from tuples $\mathcal{T}_{i}$ to
relation $R_{i}$ to $\Gamma$. Finally, we infer the tuples
$\mathcal{T}^{\prime}$ for $Q^{\prime}$ given the new symbolic database
$\Gamma^{\prime}$ and get the result of
$\text{With}(\vec{Q},\vec{R},Q^{\prime})$ based on the T-With rule.

####  4.4.3. Symbolic Encoding of Query Operators

$\scriptsize\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}R\in\textsf{Dom}(\Gamma)\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
R\leadsto\top}&\\!\\!\\!\\!\\!\\!\textrm{(E-Rel)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\neg\text{hasAgg}(L)\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\\\ \Gamma\vdash Q\hookrightarrow[t_{1},\ldots,t_{n}]\\\
\mathcal{S}\vdash\Pi_{L}(Q):[a_{1}^{\prime},\ldots,a_{l}^{\prime}]\quad\Gamma\vdash\Pi_{L}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\\\
\Phi_{2}=\land_{i=1}^{n}(\land_{j=1}^{l}\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\land\text{Del}(t_{i}^{\prime})\leftrightarrow\text{Del}(t_{i}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Proj)}\end{array}\par\par\par\par\par\par\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\Gamma\vdash\sigma_{\phi}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\\\
\Phi_{2}=\land_{i=1}^{n}((\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\top)\to
t_{i}^{\prime}=t_{i}\land(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\neq\top)\to\text{Del}(t_{i}^{\prime}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\sigma_{\phi}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Filter)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S}\vdash
Q_{1}:[a_{1},\ldots,a_{p}]\quad\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q_{1}\leadsto\Phi_{1}\\\ \mathcal{S}\vdash
Q_{2}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{2}\leadsto\Phi_{2}\quad\par\Gamma\vdash Q_{1}\times
Q_{2}\hookrightarrow[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime}]\\\
\Phi_{3}=\land_{i=1}^{n}\land_{j=1}^{m}(\neg\text{Del}(t_{i})\land\neg\text{Del}(t_{j}^{\prime}))\to\land_{k=1}^{p}\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i,j}^{\prime\prime}]}=\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\land\land_{k=1}^{q}\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i,j}^{\prime\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{j}^{\prime}]}\land\\\
\qquad(\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime}))\to\text{Del}(t_{i,j}^{\prime\prime})\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash Q_{1}\times
Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Prod)}\end{array}\mkern-2.0mu\\\
\\\ \end{array}$ Figure 12.  Sample inference rules for encoding SQL queries.
$\text{Del}(t)$ indicates that a tuple $t$ is deleted.

Since our query language supports various complex attribute expressions and
predicates, we introduce two auxiliary functions $\llbracket
e\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ and
$\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ to encode
attribute expressions and predicates in a query, respectively888We precisely
define these auxiliary functions in Appendix A.. Intuitively,
$\llbracket\cdot\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ evaluates an
attribute expression or a predicate in a recursive fashion given the schema
$\mathcal{S}$, database $\Gamma$, and a list of tuples $\mathcal{T}$. For
example, suppose $a$ is an attribute of an relation and $t$ is a tuple of that
relation, $\llbracket a+1\rrbracket_{\mathcal{S},\Gamma,[t]}=\llbracket
a\rrbracket_{\mathcal{S},\Gamma,[t]}+\llbracket
1\rrbracket_{\mathcal{S},\Gamma,[t]}=t.a+1$. Furthermore, it is worthwhile to
point out that the tuple list $\mathcal{T}$ has more than one tuple in several
cases when evaluating GROUP BY and aggregate queries. For instance,
$\llbracket\text{AVG}(\text{EMP.age})\rrbracket_{\mathcal{S},\Gamma,[t_{1},t_{2},...,t_{n}]}$
is used to compute the average age of EMP where the EMP table has $n$ symbolic
tuples.

Our encoding algorithm for query operators is represented as a set of
inference rules. Judgments are of the form $\mathcal{S},\Gamma\vdash
Q\leadsto\Phi$, meaning the encoding of query $Q$ is formula $\Phi$ given
schema $\mathcal{S}$ and database $\Gamma$. Figure 12 presents a sample set of
such inference rules.

_Relation._ The encoding for a simple relation query is trivially $\top$,
because the result can be obtained from the database $\Gamma$ directly, i.e.,
the output is the same as input.

_Filtering._ The E-Filter rule specifies how to encode filtering operations.
In particular, given a query $\sigma_{\phi}(Q)$, we can first determine the
input (result of $Q$) is $[t_{1},\ldots,t_{n}]$ and the output should be
$[t^{\prime}_{1},\ldots,t^{\prime}_{n}]$ based on the rules in Figure 11. Then
we can generate a formula $\Phi_{2}$ to describe the relationship between
$[t^{\prime}_{1},\ldots,t^{\prime}_{n}]$ and $[t_{1},\ldots,t_{n}]$.
Specifically, if a tuple $t_{i}$ is not deleted and the predicate $\phi$
evaluates to be $\top$ on $t_{i}$, then it is retained in the result, i.e.,
$t^{\prime}_{i}=t_{i}$. Otherwise, the corresponding output tuple
$t^{\prime}_{i}$ is deleted. The final formula encoding $\sigma_{\phi}(Q)$ is
the conjunction of $\Phi_{2}$ and the formula $\Phi_{1}$ that encodes $Q$.

_Projection._ According to the E-Proj rule, to encode $\Pi_{L}(Q)$ where $L$
does not contain aggregate functions, we can first infer that its input is
$[t_{1},\ldots,t_{n}]$ with attributes $[a_{1},\ldots,a_{m}]$ and output is
$[t^{\prime}_{1},\ldots,t^{\prime}_{n}]$ with attributes
$[a^{\prime}_{1},\ldots,a^{\prime}_{l}]$ based on the rules in Figure 11 and
Figure 10. Then for each $a^{\prime}_{k}$, we find its corresponding index
$c_{k}$ in the attributes of $Q$ and generate a formula $\Phi_{2}$ that
asserts for each tuple and its output $(t_{i},t^{\prime}_{i})$, they have the
same Del status and they agree on attribute $a^{\prime}_{k}$. The E-Agg rule
for encoding projection with aggregate functions is similar to E-Proj. The
main difference is that it only generates one tuple $t^{\prime}_{1}$ in the
output and sets the aggregated value based on all input tuples, i.e.,
$\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{1}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,\vec{t}}$.

_Cartesian product._ Based on the E-Prod rule to encode $Q_{1}\times Q_{2}$,
we just need to generate a formula $\Phi_{3}$ that encodes an output tuple
$t^{\prime\prime}_{i,j}$ is obtained by concatenating a tuple $t_{i}$ from
$Q_{1}$ and a tuple $t^{\prime}_{j}$ from $Q_{2}$. Specifically, $\Phi_{3}$
describes the attributes of $t^{\prime\prime}_{i,j}$ agree with those of
$t_{i}$ and $t^{\prime}_{j}$, and $t^{\prime\prime}_{i,j}$ is deleted if
either $t_{i}$ or $t^{\prime}_{j}$ is deleted.

_Left outer join._ The E-LJoin rule specifies the encoding of a left outer
join $Q_{1}\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}$ is
based on the formula $\Phi_{1}$ of inner join $Q_{1}\bowtie_{\phi}Q_{2}$
(which is a syntactic sugar of $\sigma_{\phi}(Q_{1}\times Q_{2})$). In
addition to $\Phi_{1}$, the encoding also includes $\Phi_{2}$, which describes
the output tuples from $Q_{1}$’s null extension.

_Other operations._ The rules for encoding other query operations are in
similar flavor of the above rules. Specifically, the high-level idea is to
first obtain the schema and tuples for its input and output based on the rules
in Figure 10 and Figure 11. Then we can encode the relationship between the
input and output tuples and generate a formula that encodes the query
semantics. Due to page limit, the complete set of our inference rules are
presented in Appendix B. These rules closely follow the standard three-valued
logic when evaluating expressions and predicates that involve NULL’s. For
example, the predicate NULL = NULL evaluates to NULL, which is consistent with
the three-valued logic.

###### Definition 4.3 (Interpretation).

An interpretation of a formula is a mapping from variables, function symbols,
and predicate symbols in the formula to values, functions, and predicates,
respectively.

###### Definition 4.4 (Interpretation Extension).

Interpretation $\mathcal{I}_{1}$ is an _extension_ of interpretation
$\mathcal{I}_{2}$, denoted $\mathcal{I}_{1}\sqsupseteq\mathcal{I}_{2}$, if (1)
$\textsf{Dom}(\mathcal{I}_{1})\supseteq\textsf{Dom}(\mathcal{I}_{2})$, (2)
$\forall
v\in\textsf{Vars}(\mathcal{I}_{2}).~{}\mathcal{I}_{1}(v)=\mathcal{I}_{2}(v)$,
and (3) for the Del predicate, $\forall
v\in\textsf{Vars}(\mathcal{I}_{1}).~{}\mathcal{I}_{2}(\text{Del})(v)\leftrightarrow\mathcal{I}_{1}(\text{Del})(v)$.

Intuitively, interpretation $\mathcal{I}_{1}$ is an extension of
$\mathcal{I}_{2}$ if (1) all variables, functions, and predicates defined by
$\mathcal{I}_{2}$ are also defined by $\mathcal{I}_{1}$, (2) $\mathcal{I}_{1}$
preserves the values of variables occurring in $\mathcal{I}_{2}$ while it
assigns values to new variables, and (3) $\mathcal{I}_{1}$ preserves the
definition of Del predicate on variables occurring in $\mathcal{I}_{2}$.

###### Theorem 4.5.

Let $\mathcal{D}$ be a database over schema $\mathcal{S}$ and $o_{R}$ be the
output relation of running query $Q$ over $\mathcal{D}$. Consider a symbolic
database $\Gamma$ over $\mathcal{S}$, a symbolic relation $R$ and a formula
$\Phi$ such that $\Gamma\vdash Q\hookrightarrow R$ and
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi$. For any interpretation $\mathcal{I}$
such that $\mathcal{I}(\Gamma)=\mathcal{D}$, there exists an extension
$\mathcal{I}^{\prime}$ of $\mathcal{I}$ such that (1) the result of query $Q$
over $\mathcal{D}$ is $\mathcal{I}^{\prime}(R)$, and (2) the database
$\mathcal{D}$ and $\mathcal{I}^{\prime}$ jointly satisfy $\Phi$, i.e., 999 We
slightly abuse the notation $\mathcal{I}(x)$ over lists to apply $\mathcal{I}$
to each element in list $x$. We also abuse the notation $\mathcal{I}(x)$ over
maps to apply $\mathcal{I}$ to each value in the range of map $x$.

$\begin{array}[]{l}(\Gamma\vdash Q\hookrightarrow
R)\land(\mathcal{S},\Gamma\vdash
Q\leadsto\Phi)\land(\mathcal{I}(\Gamma)=\mathcal{D})\Rightarrow\\\
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\exists\mathcal{I}^{\prime}\sqsupseteq\mathcal{I}.~{}\mathcal{I}^{\prime}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}\land(\mathcal{I}^{\prime},\mathcal{D}[o_{R}\mapsto\mathcal{I}^{\prime}(R)]\models\Phi)\end{array}$

###### Theorem 4.6.

Let $\Gamma$ be a symbolic database over schema $\mathcal{S}$ and $Q$ be a
query. Consider a symbolic relation $R$ and a formula $\Phi$ such that
$\Gamma\vdash Q\hookrightarrow R$ and $\mathcal{S},\Gamma\vdash
Q\leadsto\Phi$. If $\Phi$ is satisfiable, then for any satisfying
interpretation $\mathcal{I}$ of $\Phi$, running $Q$ over the concrete database
$\mathcal{I}(\Gamma)$ yields the relation $\mathcal{I}(R)$, i.e.,

$(\Gamma\vdash Q\hookrightarrow R)\land(\mathcal{S},\Gamma\vdash
Q\leadsto\Phi)\land(\mathcal{I}\models\Phi)\Rightarrow\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$

###  4.5. Equivalence under Bag and List Semantics

We first discuss how to check the equality of symbolic tuples and then present
how to check the equality of query outputs under _both_ bag and list
semantics. We use bag semantics by default, but for queries that involve
sorting, we switch to list semantics to preserve the order of sorted tuples.

_Equality of symbolic tuples._ Recall from Figure 3(b) that a tuple is
represented by a list of pairs, where each pair consists of an attribute name
and its corresponding value. Two symbolic tuples $t$ and $t^{\prime}$ are
considered equal iff (1) they have the same number of pairs and (2) their
corresponding symbolic values at the same index are equal. Specifically,
suppose $t=[(a_{1},v_{1}),(a_{2},v_{2}),\ldots,(a_{n},v_{n})]$ and
$t^{\prime}=[(a^{\prime}_{1},v^{\prime}_{1}),(a^{\prime}_{2},v^{\prime}_{2}),\ldots,(a^{\prime}_{n},v^{\prime}_{n})]$
where $a_{i},a^{\prime}_{i}$ are the attribute names and
$v_{i},v^{\prime}_{i}$ are their corresponding values. We say $t=t^{\prime}$
if $v_{i}=v^{\prime}_{i}$ holds for all $1\leq i\leq n$. Note that the
attribute names are ignored for equality comparison to support the renaming
operations in SQL.

_Equivalence under bag semantics._ Given two query results with symbolic
tuples $R_{1}=[t_{1},\ldots,t_{n}]$ and $R_{2}=[r_{1},\ldots,r_{m}]$, we
encode the following two properties to ensure $R_{1}$ and $R_{2}$ are
equivalent under bag semantics:

  * •

$R_{1}$ and $R_{2}$ have the same number of non-deleted tuples.

(1)
$\vspace{-2pt}\sum\limits_{i=1}^{n}\mathbb{I}[\neg\text{Del}(t_{i})]=\sum\limits_{j=1}^{m}\mathbb{I}[\neg\text{Del}(r_{j})]\vspace{-2pt}$

where $\mathbb{I}[b]$ is an indicator function that evaluates to 1 when $b$ is
true or 0 when $b$ is false.

  * •

For each non-deleted symbolic tuple in $R_{1}$, its multiplicity in $R_{1}$ is
equal to its multiplicity in $R_{2}$.

(2)
$\vspace{-2pt}\bigwedge\limits_{i=1}^{n}\Big{(}\sum\limits_{j=1}^{n}\mathbb{I}[\neg\text{Del}(t_{i})\land\neg\text{Del}(t_{j})\land
t_{i}=t_{j}]=\sum\limits_{k=1}^{m}\mathbb{I}[\neg\text{Del}(t_{i})\land\neg\text{Del}(r_{k})\land
t_{i}=r_{k}]\Big{)}\vspace{-2pt}$

Here, we include the predicates $\neg\text{Del}(t_{i})$,
$\neg\text{Del}(t_{j})$, and $\neg\text{Del}(r_{k})$ to only count those non-
deleted symbolic tuples in $R_{1}$ and $R_{2}$.

_Equivalence under list semantics._ Since the equivalence of two queries is
only checked when they involve sorting operations, the corresponding query
results $R_{1}=[t_{1},\ldots,t_{n}]$ and $R_{2}=[r_{1},\ldots,r_{m}]$ are
sorted using the OrderBy operator. Recall from Figure 4 that OrderBy must be
the last operation of a query. Furthermore, our encoding of OrderBy ensures
that all deleted tuples are placed at the end of the list and non-deleted
tuples are sorted in ascending or descending order, so we just need to encode
the following two properties to assert $R_{1}$ and $R_{2}$ are equivalent
under list semantics.

  * •

$R_{1}$ and $R_{2}$ have the same number of non-deleted tuples.

(3)
$\vspace{-2pt}\sum\limits_{i=1}^{n}\mathbb{I}[\neg\text{Del}(t_{i})]=\sum\limits_{j=1}^{m}\mathbb{I}[\neg\text{Del}(r_{j})]\vspace{-2pt}$

  * •

The tuples with the same index in $R_{1}$ and $R_{2}$ are equal.

(4)
$\vspace{-2pt}\bigwedge\limits_{i=1}^{\text{min}\\{m,n\\}}t_{i}=r_{i}\vspace{-2pt}$

Intuitively, we just need to check the pair-wise equality of tuples until the
end of $R_{1}$ or $R_{2}$, because the OrderBy operator has moved the deleted
tuples to the end of the list. This OrderBy encoding greatly simplifies the
equality check. Alternatively, one can encode the check without the assumption
of OrderBy moving deleted tuples to the end. The key idea is to maintain two
pointers, one on each list, moving from the beginning to the end of the lists.
Every time a pointer moves to a new location, it checks whether or not the
corresponding tuple is deleted. If the tuple is not deleted, then it checks if
the tuple is equal to the tuple pointed by the other pointer. Otherwise, if
the tuple is deleted, it moves to the next location.

###### Lemma 4.7.

Given two relations $R_{1}=[t_{1},\ldots,t_{n}]$ and
$R_{2}=[r_{1},\ldots,r_{m}]$, if the formula
$(\ref{eq:bag1})\land(\ref{eq:bag2})$ is valid, then $R_{1}$ is equal to
$R_{2}$ under bag semantics. If the formula
$(\ref{eq:list1})\land(\ref{eq:list2})$ is valid, then $R_{1}$ is equal to
$R_{2}$ under list semantics.

###### Theorem 4.8.

Given two queries $Q_{1},Q_{2}$ under schema $\mathcal{S}$, an integrity
constraint $\mathcal{C}$, a bound $N$, if
$\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},\mathcal{C},N)$ returns $\top$, then
$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$. Otherwise, if
$\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},\mathcal{C},N)$ returns a database
$\mathcal{D}$, then $\mathcal{D}::\mathcal{S}$ and $\llbracket
Q_{1}\rrbracket_{\mathcal{D}}\neq\llbracket Q_{2}\rrbracket_{\mathcal{D}}$.

##  5\. Implementation

Based on the techniques in Section 4, we have implemented a tool called
VeriEQL for verifying the bounded equivalence of SQL queries modulo integrity
constraints. VeriEQL uses the Z3 SMT solver (de Moura and Bjørner, 2008) for
constraint solving and model generation. In this section, we discuss several
details that are important to the implementation of VeriEQL.

_Attribute renaming._ We pre-process the queries to resolve attribute renaming
issues before starting the verification. Specifically, we design a unique
identifier generator and a name cache for pre-processing. The unique
identifier generator allows VeriEQL to efficiently track attributes while the
name cache pool stores temporary aliases of an attribute under different
scopes and automatically updates them for scope change.

_Sorting symbolic tuples._ To sort symbolic tuples based on an ORDER BY
operation, we implement an encoding for the standard bubble sort algorithm.
More specifically, we first move those deleted tuples to the end of the list,
and then sort non-deleted tuples based on the sorting criteria specified by
ORDER BY. As part of the bubble sort algorithm, two adjacent tuples
$t_{1},t_{2}$ in the list are swapped under two conditions: (1)
$t_{1}\neq\text{Null}$ whereas $t_{2}=\text{Null}$, or (2) $t_{1},t_{2}$ are
not Null but $t_{1}<t_{2}$ for ascending order ($t_{1}>t_{2}$ for descending
order).

##  6\. Evaluation

This section presents a series of experiments that are designed to answer the
following questions.

  * •

RQ1: How does VeriEQL compare with state-of-the-art SQL equivalence checking
techniques in terms of _coverage_? That is, does VeriEQL support more complex
queries? (Section 6.2)

  * •

RQ2: How effective is VeriEQL at _disproving_ query equivalence? Does VeriEQL
generate useful counterexamples to facilitate downstream tasks? (Section 6.3)

  * •

RQ3: How large input bounds can VeriEQL reach during verification? (Section
6.4)

###  6.1. Experimental Setup

_Benchmarks._ We collected benchmarks — each of which is a pair of queries —
from three different workloads. To the best of our knowledge, we have
incorporated _all_ benchmarks publicly available from recent work on query
equivalence checking (Chu et al., 2017b, a, c, 2018; Zhou et al., 2019, 2022;
Wang et al., 2018a). Additionally, we also curated a very large collection of
new queries that, to the best of our knowledge, has not been used in any prior
work.

  * •

LeetCode. This is a new dataset curated by us containing a total of 23,994
query pairs $(Q_{1},Q_{2})$. To curate this dataset, we first crawled _all_
publicly available queries accepted by LeetCode (LeetCode, 2023) that are
syntactically distinct. Then, we grouped them based on the LeetCode problem —
queries in the same group are written and submitted by actual users that solve
the same problem. For each problem, we have also manually written a “ground-
truth” query that is _guaranteed_ to be correct. Finally, each _user query_
$Q_{1}$ is paired with its corresponding _ground-truth query_ $Q_{2}$,
yielding a total of 23,994 query _pairs_. In each pair, $Q_{1}$ is supposed to
be equivalent to $Q_{2}$, which, however, is not always the case due to
missing test cases on LeetCode. Indeed, as we will see shortly, VeriEQL has
identified many wrong queries confirmed by LeetCode. As a final note: queries
in our dataset naturally exhibit diverse patterns since they were written by
different people with diverse backgrounds around the world, which makes this
particular dataset especially valuable for evaluating query equivalence
checkers. We also manually formalize the schema and integrity constraint for
each LeetCode problem.

  * •

Calcite. Our second benchmark set is constructed from the Calcite’s
optimization rules test suite (Calcite, 2023). This is a standard workload
used extensively in prior work (Zhou et al., 2022, 2019; Wang et al., 2018a;
Chu et al., 2017b, a, c, 2018). In particular, each Calcite test case has a
pair of queries $(Q_{1},Q_{2})$, where $Q_{1}$ can be rewritten to $Q_{2}$
using the optimization rule under test. In other words, $Q_{1}$ and $Q_{2}$
should be equivalent to each other, since all optimization rules are supposed
to preserve the semantics. We included query pairs from _all_ test cases and
ended up with a total of 397 query pairs. This number is noticeably higher
than 232 pairs reported in prior work (Zhou et al., 2022), because the Calcite
project is under active development and prior work used test cases from the
version in year 2018. The Calcite project also includes necessary schema and
integrity constraints, which were all incorporated into our benchmark suite.

  * •

Literature. Finally, we used _all_ other benchmarks from recent work that are
publicly available. In particular, the Cosette series (Cosette, 2018; Chu et
al., 2017b, a, c, 2018) of work has 38 benchmarks — all of them are included
in our suite (8 involve integrity constraints). We also used all 26 benchmarks
from (Wang et al., 2018a). In total, our Literature dataset has 64 benchmarks.

Across all our workloads, the average query size is 84.54 (measured by the
number of AST nodes), where the max, min, and median are 679, 5, and 73,
respectively. In addition to the large query size, our benchmarks are complex
in terms of query nesting. In particular, 57.7% have sub-queries (e.g., SELECT
* FROM T1 WHERE T1.id IN (SELECT uid FROM T2)), and a number of them have four
levels of query-nesting. In addition, 95.7% of the queries involve joining
multiple tables, and 33.2% use the outer-join operation, which is generally
quite challenging to verify. Finally, our queries also use other SQL features,
such as group-by (58.7%), aggregate functions (65.3%), and order-by (21.6%).

_Baselines._ We compare VeriEQL against _all_ state-of-the-art _bounded_
equivalence checking techniques that have corresponding tools publicly
available. These tools all accept a smaller subset of SQL than VeriEQL.

  * •

An extended version of Cosette (Chu et al., 2017b, a) which uses the
provenance-base pruning technique from (Wang et al., 2018a) to speed up the
original Cosette technique. This baseline represents the state-of-the-art
along the Cosette line of work. It does not support any integrity
constraints.101010Cosette assumes all columns are NOT NULL — which can be
viewed as a “built-in integrity constraint” — even if a column can in fact be
NULL. In other words, Cosette may not consider all valid inputs and,
therefore, may be incomplete. For brevity, we call this baseline Cosette.

  * •

An extension of Qex (Veanes et al., 2010) that incorporates the provenance-
base pruning technique from (Wang et al., 2018a) and significantly outperforms
the original Qex. For brevity, we call this baseline Qex. This baseline does
not consider integrity constraints.

In addition, we compare VeriEQL against two SQL testing tools that cannot
verify equivalence of two queries (neither in a bounded nor unbounded way) but
can potentially generate counterexamples to disprove their equivalence.

  * •

DataFiller (Guagliardo and Libkin, 2017; Coelho, 2013) is a random database
generator that produces databases based on the schema and integrity
constraints. We use DataFiller to generate random databases and run two
queries over the databases to check if the outputs are different.

  * •

XData (Chandra et al., 2015) is a constraint-based mutation testing tool that
can generate databases to disprove equivalence of two queries.

While not apples-to-apples, we also compare VeriEQL with state-of-the-art
_full_ (i.e., unbounded) verification techniques that can prove query
equivalence. None of these tools are able to generate counterexamples and all
of them support a smaller subset of SQL than VeriEQL.

  * •

SPES (Zhou et al., 2022) is a state-of-the-art verifier from the databases
community. It does not support query operations beyond select-project-join
(e.g., ORDER BY and set operations such as INTERSECT), and has very limited
support for integrity constraints111111While the SPES paper claims to accept
simple primary key constraints, the artifact (https://github.com/georgia-tech-
db/spes) is not parameterized with any constraints. Instead, it is specialized
to Calcite’s tables, schema, and integrity constraints..

  * •

HoTTSQL (Chu et al., 2017c) and UDP (Chu et al., 2018) use a proof assistant
(in particular, Coq and Lean respectively) to prove query equivalence. They
are quite different from the aforementioned techniques that utilize an
automated theorem prover (e.g., Z3) and require more manual effort. Since UDP
does not have a publicly available artifact that is usable, we include HoTTSQL
as a baseline to facilitate a complete and thorough evaluation.

###  6.2. RQ1: Coverage and Comparison against State-of-the-Art Techniques

In this section, we report the number of (1) query pairs whose _bounded_
equivalence (against a space of bounded-size inputs) can be successfully
verified by VeriEQL and (2) those that can be proved non-equivalent (i.e.,
counterexamples are generated). We also compare VeriEQL with baselines.

_Setup._ Given a benchmark consisting of queries $(Q_{1},Q_{2})$ with their
schema and integrity constraint, we run VeriEQL using a 10-minute timeout.
There are three possible outcomes for each benchmark: (1) unsupported, (2)
checked, or (3) refuted. “unsupported” means VeriEQL is not applicable to the
benchmark (e.g., due to unsupported integrity constraints or SQL features).
Otherwise, VeriEQL would report either “checked” (meaning bounded equivalence)
or “refuted” (with a counterexample witnessing the non-equivalence of $Q_{1}$
and $Q_{2}$). The bound is incrementally increased from 1 until the timeout is
reached or a counterexample is identified. If no counterexample is found
before timeout and the bounded equivalence is verified for at least bound 1,
we report “checked”.

The same setup is used for bounded verification baselines, namely Cosette and
Qex. For testing baselines (i.e., DataFiller and XData), there are three
possible outcomes: (1) unsupported, (2) not-refuted, and (3) refuted. Since
DataFiller is a random database generator, we use it to generate $1,000$
random databases where each relation has $100$ tuples for each supported
benchmark. If any of these databases leads to different execution results on
the two queries, we report it as “refuted”; otherwise, we report “not-
refuted”. By contrast, XData performs mutation testing, so we only run the
tool once on each supported benchmark. We report “refuted” if it finds a
counterexample of equivalence and report “not-refuted” otherwise. For
unbounded verification baselines (i.e., SPES and HoTTSQL), there are three
possible outcomes: (1) unsupported, (2) verified, and (3) not-verified.
“Verified” means the full equivalence of two queries is verified, and “not-
verified” means the result is unknown (as none of them can generate
counterexamples). This leads to an apples-to-oranges comparison; nevertheless,
we include the results as well for a complete evaluation. All baseline tools
use a 10-minute timeout, which is the same as VeriEQL.

(a) _LeetCode._

(b) _Calcite._

(c) _Literature._

Figure 13. RQ1: Each workload has a sub-figure that shows, for each tool, the
percentage of benchmarks (i.e., query pairs) in each category:
unsupported/checked/refuted for bounded verification, unsupported/not-
refuted/refuted for testing, unsupported/verified/not-verified for unbounded
verification.

RQ1 take-away: VeriEQL supports over 75% of the benchmarks, which is more than
all baselines. VeriEQL also significantly outperforms all baselines across all
workloads in terms of both disproving equivalence and proving (bounded)
equivalence of query pairs.

_Results._ Our main result for each workload is shown in Figures 13(a), 13(b),
and 13(c). For the LeetCode dataset, VeriEQL supports 77.1% of benchmarks,
which is higher than all baselines. This very large gap is due to baselines’
poor support for integrity constraints and complex SQL features such as ORDER
BY. Furthermore, VeriEQL is able to disprove equivalence for 14.9% of the
LeetCode benchmarks, whereas none of the _bounded_ verification baselines can
disprove any. Unbounded verification tools cannot disprove equivalence by
nature, and only the testing tool DataFiller can disprove 0.5%. For Calcite
(see Figure 13(b)), the result is similar. The only difference is that
DataFiller can support all benchmarks, but it can only refute 0.8% of
benchmarks, smaller than the 1.0% of VeriEQL. For Literature (see Figure
13(c)), VeriEQL supports 98.4% of benchmarks, which outperforms most of
baselines other than DataFiller. It is comparable with bounded verification
baselines, hypothetically because baselines were better-engineered for
Literature queries, but it still outperforms testing baseline on disproving
equivalence.

_Qualitative Analysis on Failure to Disprove Equivalence._ To understand
whether two queries are indeed equivalent if VeriEQL reports “checked”, we
perform manual inspections during the evaluation. Given that we have over
$24,000$ benchmarks in total and exhaustive inspection is not practically
feasible, we perform a non-exhaustive manual inspection. Specifically, we
sampled 50 benchmarks from LeetCode where VeriEQL reported “checked” and
confirmed all of them are indeed equivalent. In addition, for the benchmarks
that can be proved equivalent by other tools (i.e., SPES), VeriEQL also agrees
on the result. This serves as some evidence on which we believe the
equivalences checked by VeriEQL are valid. For Calcite dataset, we found that
one benchmark where VeriEQL reported “checked” but one baseline tool (namely
Cosette) reported “refuted”. After further inspection, we believe this
benchmark should be equivalent but Cosette gave a spurious counterexample
input on which both queries produce the same output table. We suspect Cosette
may have an implementation bug that led to spurious counterexamples. For
Literature dataset, we manually inspected all of the 34 “checked” benchmarks
and found that 27 are indeed equivalent but 7 are not equivalent. Among these
7 non-equivalent benchmarks, baselines generate spurious counterexamples for 5
of them; in other words, baselines also cannot disprove these 5. The remaining
two non-equivalent benchmarks need large input databases (e.g., with $>$1000
tuples) in order to be differentiated; within our 10-minute timeout, VeriEQL
cannot disprove them but Cosette can. The reason is that Cosette has some
internal heuristics that consider specific inputs with more tuples before
exhausting the space of smaller inputs, whereas VeriEQL simply increments the
size of the input database from one.121212Even with this simple size-
increasing strategy, VeriEQL can disprove 5 Literature benchmarks for which
Cosette reports “checked.”

_Small-Scope Hypothesis._ Our evaluation echos the small-scope hypothesis
discussed in prior work (Miao et al., 2019): “mistakes in most of the queries
may be explained by only a small number of tuples.” There are only a small
number of sources in SQL queries that could potentially break the small scope
hypothesis, such as LIMIT clause 131313Recall from Figure 4 that we do not
support LIMIT clauses. or aggregation function COUNT with a large constant.
Empirically, we observe that the small scope hypothesis holds for most of all
our benchmarks. We only find two benchmarks that require an input relation
with more than 1000 tuples to disprove equivalence; both of them have a clause
like COUNT(a) > 1000.

_Limitations of Bounded Equivalence Verification._ While in principle the
bounded equivalence verification approach taken by VeriEQL can disprove or
prove equivalence of two SQL queries for all input relations up to a finite
size, it may not be able to disprove equivalence within a practical amount of
time if the counterexample can only be large input relations. For example,
during our evaluation, VeriEQL failed to disprove equivalence for the
following two queries from the Literature dataset:  SELECTC.name FROMCarriers
ASC JOINFlights ASF ONC.cid = F.carrier_id GROUP BY C.name, F.year,
F.month_id, F.day_of_month HAVINGCOUNT(F.fid) ¿ 1000

SELECTC.name FROMCarriers ASC JOINFlights ASF ONC.cid = F.carrier_id
---
GROUP BY C.name, F.day_of_month HAVINGCOUNT(F.fid) ¿ 1000

In fact, a counterexample refuting their equivalence has more than $1000$
tuples, which VeriEQL cannot find within the 10-minute time limit.

_Discussion._ Interested readers might wonder why baselines perform poorly on
Calcite given it was used extensively as a benchmark suite in prior work (Wang
et al., 2018a; Chu et al., 2017b). The reason is that Cosette, Qex, and
HoTTSQL do not support the NOT NULL constraint (among others) required in all
Calcite benchmarks. As a result, we directly report “unsupported” in RQ1
setup. Results reported in prior work were obtained by running the tools
_without considering_ constraints (like NOT NULL). One may also wonder why
VeriEQL has 1% (i.e., 4 benchmarks) “not checked” for Calcite, where all
Calcite’s query pairs are supposed to be equivalent. We manually inspected
these benchmarks and believe some of Calcite’s rewrite rules are not
equivalence preserving (i.e., wrong), leading to non-equivalent query pairs —
we will expand on this in RQ2.

###  6.3. RQ2: Effectiveness at Generating Counterexamples to Facilitate
Downstream Tasks

So far, we have seen the overall result of VeriEQL and how that compares
against baselines. In RQ2, we will concentrate on those “refuted” benchmarks
and evaluate VeriEQL’s capability at generating counterexamples. Notably,
VeriEQL’s counterexamples revealed serious bugs in MySQL and Calcite, and
suggested new test inputs to augment LeetCode’s existing test suite.

_Setup._ Since the unbounded verifiers do not generate counterexamples, let us
answer the following question: given each workload, for each _bounded
verification_ and _testing_ approach (including VeriEQL and baselines), how
many benchmarks did the tool identify a counterexample for? How many of these
counterexamples are genuine (i.e., not spurious)? Here, a counterexample is
genuine if (i) it meets the integrity constraint associated with the benchmark
and (ii) the two queries yield different outputs. To study the impact of
integrity constraints, we run two versions of each tool: (1) the original
version as in RQ1, and (2) a version denoted by a suffix “-noIC” that drops
all integrity constraints when running the tool (but we still consider
integrity constraints when checking if the counterexample is genuine).

RQ2 take-away: VeriEQL can disprove equivalence for significantly more
benchmarks than all bounded baselines across all workloads. VeriEQL can also
generate counterexamples to help identify bugs in real-world systems and
augment existing test suites.

(a) _LeetCode._

(b) _Calcite._

(c) _Literature._

Figure 14. RQ2: We have a sub-figure for each workload that shows (1) the
number of _all_ benchmarks for which a tool generates a counterexample and (2)
the number of benchmarks where the counterexamples are _genuine_.

_Results._ Our main results are presented in Figure 14. In a nutshell, VeriEQL
can prove much more non-equivalent benchmarks than all baselines across all
workloads. For example, VeriEQL found counterexamples for 3,586 LeetCode
benchmarks; 3,584 of them are confirmed to be genuine. The counterexample
inputs for the remaining two benchmarks conform to the integrity constraints
but they produce the same output when executed on the input _using MySQL._ It
turns out these two seemingly “spurious” counterexamples are due to a
previously unknown bug in MySQL — they should produce different outputs. When
dropping integrity constraints, VeriEQL-noIC found 11,390 counterexamples —
but only 2,754 are genuine, which is even lower than VeriEQL’s. This suggests
that the false alarm rate will be significantly higher without considering
integrity constraints. For the other two workloads, we observe a very similar
trend.

_Finding bugs in MySQL._ As mentioned earlier, for two LeetCode benchmarks,
VeriEQL generates “spurious” counterexamples — that are actually genuine — due
to a bug in MySQL’s latest release version 8.0.32. The MySQL verification team
had confirmed and classified this bug with _serious_ severity. Details of the
bug are provided in Appendix D under supplementary materials.

_Detecting missing test cases for LeetCode._ Recall that some of the user-
submitted queries from our LeetCode workload may be wrong (i.e., not
equivalent to the ground-truth queries), which suggests that new test cases
are needed. In particular, as of the submission date (October 20, 2023), we
have manually inspected 17 LeetCode problems for which VeriEQL reported non-
equivalent benchmarks, and filed issues to the LeetCode team. Notably, our
issue reports also have meaningful counterexamples generated by VeriEQL. To
date, 13 of them have been confirmed and fixed, while the remaining ones have
all been acknowledged. A common pattern is that existing tests miss the NULL
case — this again highlights the importance of modeling the three-valued logic
in SQL.

_Identifying buggy Calcite rewrite rules._ VeriEQL found 4 “not checked”
(i.e., non-equivalent) Calcite benchmarks with valid counterexamples. The
Calcite team has confirmed that two of them are due to bugs in two rewrite
rules: one is a duplicate of an existing bug report, while the other is a new
bug. In particular, for the new bug, the rule would rewrite a query $Q_{1}$ to
a non-equivalent $Q_{2}$ when $Q_{1}$ has SUM applied to an empty table. The
third is due to a bug in an internal translation step in Calcite, which has
also been confirmed by the Calcite team. The fourth one is still being worked
on by the team currently. This result again demonstrates that VeriEQL is able
to uncover very tricky bugs from well-maintained open-source projects.

###  6.4. RQ3: Distribution of Bounds on Checked Benchmarks

(a) _LeetCode_

(b) _Calcite_

(c) _Literature_

Figure 15. RQ3: distribution of bounds on checked benchmarks.

As an indicator of VeriEQL’s scalability, we study how large input bounds
VeriEQL can reach within the 10-minute time limit when it reports a benchmark
is checked.

_Setup._ We collected all 14,905 (62.1% of 23,994) LeetCode benchmarks that
VeriEQL reports checked in RQ1. Similarly, we also collected all 261 (65.7% of
397) checked benchmarks from Calcite and all 34 (53.1% of 64) checked
benchmarks from Literature. For each benchmark, we run VeriEQL by gradually
increasing the bound from 1 until it gets timeout and keep records of the
bound.

RQ3 take-away: VeriEQL can verify over 70% of the checked benchmarks within 10
minutes given an input bound 5. For 3% of the checked benchmarks, VeriEQL can
verify the query equivalence for an input bound ¿100.

_Results._ The evaluation results are presented in Figure 15, where the bar
shows the number of benchmarks VeriEQL can verify for a given input bound. For
example, as shown in Figure 15(a), VeriEQL can verify equivalence for bound 1
on all 14,905 LeetCode benchmarks. Among them, it can verify equivalence for
bound 2 on 14,894 benchmarks. In a nutshell, on 71% of checked LeetCode
benchmarks, VeriEQL can reach bound 5, 28% for bound 10, 8% for bound 50, and
3% for bound 100. It shows similar patterns on Calcite. For Literature,
VeriEQL only reaches bound 20 within the time limit, hypothetically because
many benchmarks combine several complex SQL operators (e.g., Distinct and
GroupBy) that are challenging for symbolic reasoning.

##  7\. Related Work

_Equivalence checking for SQL queries._ SQL equivalence checking is an
important problem in both programming languages and database communities.
There is a line of work on automated verification of query equivalence,
including full verification (Zhou et al., 2022, 2019; Chu et al., 2017c, 2018;
Green, 2011; Chandra and Merlin, 1977; Aho et al., 1979) and bounded
verification (Chu et al., 2017a, b; Veanes et al., 2010; Wang et al., 2018a).
For example, SPES (Zhou et al., 2022) takes a symbolic approach for proving
the existence of a bijective identity map between tuples returned by two
queries. HoTTSQL (Chu et al., 2017c) and UDP (Chu et al., 2018) encode SQL
queries in an algebraic structure to syntactically canonicalize two queries
and then verify the equivalence of corresponding algebraic expressions using
interactive theorem provers. Unlike prior work that aims for full equivalence
verification, VeriEQL targets to solve the bounded equivalence verification
problem modulo integrity constraints and can generate counterexamples for
disproving equivalence. Compared to prior work for bounded verification such
as Cosette (Chu et al., 2017b; Wang et al., 2018a), VeriEQL supports a larger
fragment of SQL queries and a richer set of integrity constraints and
significantly outperforms all baselines as demonstrated by our comprehensive
evaluation. One limitation of VeriEQL is that it does not support correlated
subqueries in its current status, which can be overcome by incorporating
unnesting techniques proposed by Seshadri et al. (1996).

_Testing SQL queries._ Another line of related work is about testing the
correctness of SQL queries. For instance, XData (Chandra et al., 2015) uses
mutation-based testing to detect common mistake patterns in SQL queries. Shah
et al. (2011) also uses mutation testing with hard-coded rules to kill as many
query mutants as possible. In addition, EvoSQL (Castelein et al., 2018) uses
an evolutionary search algorithm to generate test data in an offline manner,
guided by predicate coverage Tuya et al. (2010). RATest (Miao et al., 2019)
uses a provenance-based algorithm to find a minimal counterexample database
that can explain incorrect queries. DataFiller (Guagliardo and Libkin, 2017;
Coelho, 2013) uses random database generation to produce test databases based
on the schema and integrity constraints. Different from these testing
approaches, VeriEQL provides formal guarantees on query equivalence (in a
bounded fashion).

_Formal methods for databases._ Formal methods have been used to facilitate
the development and maintenance of database systems and applications, such as
optimizing database applications (Cheung et al., 2013; Delaware et al., 2015)
and data storage (Feser et al., 2020), model checking database applications
(Deutsch et al., 2005, 2007; Gligoric and Majumdar, 2013), providing
foundations to queries (Ricciotti and Cheney, 2019; Cheney and Ricciotti,
2021; Ricciotti and Cheney, 2022), verifying correctness of schema refactoring
(Wang et al., 2018b), and synthesizing programs for schema evolution (Wang et
al., 2019, 2020). Among various work, Mediator (Wang et al., 2018b) is the
most related to our work. However, Mediator studies the full equivalence
verification problem of two database applications over different schemas,
whereas VeriEQL performs bounded equivalence verification of two SQL queries
under the same schema, but it generates counterexamples for disproving query
equivalence.

_Semantics of SQL queries._ Different formal semantics of SQL queries have
been proposed in the literature, such as set semantics, bag semantics, list
semantics, and their combinations (Negri et al., 1991; Benzaken and Contejean,
2019; Ricciotti and Cheney, 2019; Chu et al., 2017c, 2018; Wang et al.,
2018b). We base the SQL semantics of VeriEQL on list operations and quotient
by bag equivalence at the end mainly because lists, by their ordered nature,
facilitate the definition of ORDER BY in the semantics. We have not explored
the formal difference between our semantics and state-of-the-art semantics
proposals. In fact, we believe that proving the equivalence between our
semantics and existing semantics or characterizing the differences between
semantics with demonstrating examples is an interesting direction for future
work.

_Bounded verification._ Bounded verification has been used to find various
kinds of bugs in software systems while providing formal guarantees on the
result. Prior work such as CBMC (Clarke et al., 2004), JBMC (Cordeiro et al.,
2018), and Corral (Lal et al., 2012) has been quite successful to this end for
imperative languages like C, C++, or Java. However, VeriEQL performs bounded
verification to check equivalence of declarative SQL queries. Unlike prior
work that unrolls loops, VeriEQL bounds the size of relations in the database
and can guarantee the equivalence of two queries for all databases where
relations are up to a given finite size.

_Equivalence verification._ Equivalence verification has been studied
extensively in the literature. Researchers have developed many approaches for
checking equivalence of various applications, such as translation validation
for compilers (Pnueli et al., 1998; Necula, 2000; Stepp et al., 2011), product
program (Zaks and Pnueli, 2008; Barthe et al., 2011), relational Hoare logic
(Benton, 2004), Cartesian Hoare Logic (Sousa and Dillig, 2016), and so on.
VeriEQL is along the line of equivalence verification, but it is tailored
towards a different application, SQL queries, and presents an SMT-based
approach for verifying bounded equivalence of queries modulo integrity
constraints.

##  8\. Conclusion

In this paper, we presented VeriEQL, a simple yet highly practical approach
that can both prove and disprove the bounded equivalence of _complex SQL
queries with integrity constraints_. For a total of 24,455 benchmarks, VeriEQL
can prove and disprove over 70% of them, significantly outperforming all
state-of-the-art SQL equivalence checking techniques.

## Acknowledgments

We would like to thank the anonymous reviewers of OOPSLA for their detailed
and helpful comments on an earlier version of this paper. This research is
supported by the Natural Sciences and Engineering Research Council of Canada
(NSERC) Discovery Grant and the National Science Foundation (NSF) Grant No.
CCF-2210832.

## Data-Availability Statement

The software that implements the techniques described in Section 4 and
supports the evaluation results reported in Section 6 is available on Zenodo
(He et al., 2024).

## References

  * (1)
  * Aho et al. (1979) Alfred V. Aho, Yehoshua Sagiv, and Jeffrey D. Ullman. 1979\.  Equivalences among Relational Expressions.  _SIAM J. Comput._ 8, 2 (1979), 218–246.  https://doi.org/10.1137/0208017
  * Barthe et al. (2011) Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011\.  Relational Verification Using Product Programs. In _Proceedings of the International Symposium on Formal Methods (FM)_ _(Lecture Notes in Computer Science, Vol. 6664)_. 200–214.  https://doi.org/10.1007/978-3-642-21437-0_17
  * Benton (2004) Nick Benton. 2004\.  Simple relational correctness proofs for static analyses and program transformations. In _Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. ACM, 14–25.  https://doi.org/10.1145/964001.964003
  * Benzaken and Contejean (2019) Véronique Benzaken and Evelyne Contejean. 2019.  A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In _Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs_. 249–261.  https://doi.org/10.1145/3293880.3294107
  * Calcite (2023) Calcite. 2023.  Calcite Optimization Rules Test Suite.  https://github.com/apache/calcite/blob/main/core/src/test/java/org/apache/calcite/test/RelOptRulesTest.java.
  * Castelein et al. (2018) Jeroen Castelein, Maurício Aniche, Mozhan Soltani, Annibale Panichella, and Arie van Deursen. 2018.  Search-based test data generation for SQL queries. In _Proceedings of the 40th international conference on software engineering_. 1220–1230.  https://doi.org/10.1145/3180155.3180202
  * Chandra and Merlin (1977) Ashok K. Chandra and Philip M. Merlin. 1977.  Optimal Implementation of Conjunctive Queries in Relational Data Bases. In _Proceedings of the ACM Symposium on Theory of Computing (STOC)_. ACM, 77–90.  https://doi.org/10.1145/800105.803397
  * Chandra et al. (2019) Bikash Chandra, Ananyo Banerjee, Udbhas Hazra, Mathew Joseph, and S Sudarshan. 2019.  Automated grading of sql queries. In _2019 IEEE 35th International Conference on Data Engineering (ICDE)_. IEEE, 1630–1633.  https://doi.org/10.1109/ICDE.2019.00159
  * Chandra et al. (2015) Bikash Chandra, Bhupesh Chawda, Biplab Kar, KV Maheshwara Reddy, Shetal Shah, and S Sudarshan. 2015\.  Data generation for testing and grading SQL queries.  _The VLDB Journal_ 24, 6 (2015), 731–755.  https://doi.org/10.1007/s00778-015-0395-0
  * Cheney and Ricciotti (2021) James Cheney and Wilmer Ricciotti. 2021.  Comprehending nulls. In _Proceedings of the International Symposium on Database Programming Languages (DBPL)_. ACM, 3–6.  https://doi.org/10.1145/3475726.3475730
  * Cheung et al. (2013) Alvin Cheung, Armando Solar-Lezama, and Samuel Madden. 2013\.  Optimizing database-backed applications with query synthesis. In _ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI)_. ACM, 3–14.  https://doi.org/10.1145/2491956.2462180
  * Chu et al. (2017a) Shumo Chu, Daniel Li, Chenglong Wang, Alvin Cheung, and Dan Suciu. 2017a.  Demonstration of the cosette automated sql prover. In _Proceedings of the 2017 ACM International Conference on Management of Data_. 1591–1594.  https://doi.org/10.1145/3035918.3058728
  * Chu et al. (2018) Shumo Chu, Brendan Murphy, Jared Roesch, Alvin Cheung, and Dan Suciu. 2018.  Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries.  _Proc. VLDB Endow._ 11, 11 (2018), 1482–1495.  https://doi.org/10.14778/3236187.3236200
  * Chu et al. (2017b) Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017b.  Cosette: An Automated Prover for SQL.. In _CIDR_.