Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance

Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance Jingyu Ke

Jingyang Li

Guoqiang Li

Shanghai Jiao Tong University Shanghai, China Windocotber@sjtu.edu.cn

Shanghai Jiao Tong University Shanghai, China lijjjjj@sjtu.edu.cn

Shanghai Jiao Tong University Shanghai, China li.g@sjtu.edu.cn

arXiv:2608.15709v1 [cs.DB] 16 Aug 2026

ABSTRACT SQL rewrite verification must account for duplicate rows, observable row order, and typed value semantics. Existing verifiers have yet to combine proofs over database instances of arbitrary finite cardinality with an ordered-list semantics for nested, tie-sensitive top-𝑘. Unbounded systems reason primarily over bags or handle ordering through syntax-directed restrictions, whereas bounded systems either support only restricted top-𝑘 forms or impose a deterministic ordering rather than retain all legal tie-induced outcomes. Support for typed expression and aggregate semantics, observable runtime errors, and integrity constraints also remains partial. In Rocq, we mechanize a compositional logical semantics for a typed SQL core with order-sensitive operators, capturing all possible ordered lists and observable SQL failures in the supported fragment. To our knowledge, this is the first mechanized SQL semantics to combine nested, tie-sensitive top-𝑘 with a closure-based lifting from bag equivalence to ordered-list equivalence, enabling sound reuse of bag-theoretic reasoning while preserving compositionality across order-sensitive and correlated contexts. The formalization further provides executable semantics for PostgreSQL-oriented scalar and aggregate evaluation and an explicit account of integrity constraints. Building on this semantics, we present Logos, an LLMguided Rocq verifier for unbounded SQL rewrite equivalence. Its agent uses a verified SQL-specific lemma library to construct queryspecific Rocq proofs. Our evaluation covers 389 query pairs from Apache Calcite optimizer tests, TPC-H and TPC-DS rewrites, and WeTune’s real-application workloads. Logos solves 86.9% of them, compared with 64.0% for SQLSolver, the strongest baseline. PVLDB Reference Format: Jingyu Ke, Jingyang Li, and Guoqiang Li. Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance. PVLDB, 20(1): XXX-XXX, 2027. doi:XX.XX/XXX.XX

1

INTRODUCTION

Query rewriting is a central technique for improving database performance [17]. Reported application cases include a 100× speedup for an individual query and a 3.7× reduction in production workload latency [2, 22]. Recent rewriting systems have also uncovered hundreds of optimization opportunities missed by existing DBMSs in This work is licensed under the Creative Commons BY-NC-ND 4.0 International License. Visit https://creativecommons.org/licenses/by-nc-nd/4.0/ to view a copy of this license. For any use beyond those covered by this license, obtain permission by emailing info@vldb.org. Copyright is held by the owner/author(s). Publication rights licensed to the VLDB Endowment. Proceedings of the VLDB Endowment, Vol. 20, No. 1 ISSN 2150-8097. doi:XX.XX/XXX.XX

widely used open-source applications [27]. Deploying such rewrites requires establishing semantic equivalence between the original and rewritten queries. Specifically, the two queries must have the same observable behavior on every schema-conforming finite database instance, without any preset bound on relation cardinality. Testing can refute this obligation by finding a counterexample, but it cannot establish it. This gap is increasingly consequential as optimizers combine hand-written rules, workload-derived transformations, and LLM-generated rewrites; recent industrial evidence shows that realistic query pairs remain beyond the coverage of current equivalence checkers [16]. The central semantic challenge arises from the interaction between bag semantics and order-sensitive operators. Some relational arguments are permutation-invariant and admit concise multiplicity proofs. In contrast, ORDER BY establishes order, whereas slicing and window operators can consume row positions. Globally quotienting intermediate results by permutation therefore erases behavior observable to nested, tie-sensitive top-𝑘, whereas assigning each operator one fixed output list invents an execution order that SQL leaves unspecified. Retaining all legal ordered lists preserves this behavior, but introduces a substantial proof burden: even routine query-specific equivalence arguments require nontrivial structural induction over lists, often coupled with explicit permutation reasoning [7, 9]. Sound verification also requires concrete semantics for typed scalar and aggregate evaluation, including observable failures, together with a formal account of integrity constraints. Modeling scalar and aggregate operations as uninterpreted functions overapproximates their behavior and can admit spurious counterexamples that cannot arise under concrete SQL semantics. Existing unbounded verifiers obtain much of their power from bag semantics and algebraic normalization [7, 9, 12, 26]. Support for ordered fragments is typically syntax-directed, requiring syntactic alignment of corresponding order-sensitive operators. Conversely, list encodings can cover richer SQL but have so far provided bounded guarantees for restricted order-sensitive fragments [13]. The missing connection is not another global choice between lists and bags. A verifier needs a semantics that retains every possible result order, together with a checked criterion for using bag theory at a particular subquery. We present Logos, a proof-producing verifier that realizes this criterion. Its semantic foundation is FormalSQL, our order-sensitive extension of SQLCoq [5], mechanized in Rocq. The extension provides a compositional logical semantics for a typed SQL core with order-sensitive operators, together with executable, PostgreSQLoriented value and error interpretations for the supported fragment. Rather than selecting one implementation-dependent result, FormalSQL assigns each query a relation containing all possible

----- Source Query ----SELECT * FROM users WHERE active IS TRUE AND users.id IN ( SELECT user_id FROM group_users WHERE group_id = 8861) LIMIT 20;

ordered row lists and observable SQL failures in this fragment. Applying the order-forgetting map to every successful result yields the query’s bag projection, which preserves multiplicities while discarding order. The projection may contain multiple distinct bags, for example when top-𝑘 cuts through a tie. We identify a semantic closure condition under which two sets of legal ordered lists are equivalent exactly when their bag projections are equal. At such a boundary, standard multiplicity arguments can be used locally and then lifted through the surrounding order-sensitive context. Logos then performs LLM-guided counterexample search. If the model predicts non-equivalence, it must propose a concrete, schemaconforming database instance. A pair of differing executions on that instance does not in general establish non-equivalence. When SQL does not determine a unique order, an engine produces only one of several legal ordered lists; the observed choice may depend on optimizer-selected scan and join plans and physical storage order, while the relative order of rows tied on every ordering expression remains implementation-dependent. Row-limiting operators can turn this freedom into different selected subsets [18]. For a proof-producing non-equivalence result, Logos therefore reifies the candidate as a fixed, typed FormalSQL database instance and requires the proof agent to establish a countermodel against the complete outcome relations. The proof exhibits a legal outcome on one side that no legal outcome on the other can match. Likewise, when the model predicts equivalence, Logos requires the proof agent to establish the fixed Rocq equivalence theorem over all schema-conforming database instances. Building on FormalSQL, we provide a library of verified lemmas covering general structural properties and common operator interactions. The library keeps the agent from reproving these reusable facts and concentrates its effort on the semantic interactions and feature combinations specific to each query pair. We evaluate Logos on 389 query pairs spanning Calcite, the TPC decision-support suites, and WeTune. Logos solves 86.9% of the pairs, improving over the strongest baseline, SQLSolver (64.0%), by 22.9 percentage points. On the order-sensitive subset, it solves 73.1%, compared with 41.3% for the strongest baseline on that subset. These results show that explicit treatment of order and lemma-guided proof synthesis extend proof-producing verification to substantially broader SQL feature combinations. This paper makes three contributions:

----- Target Query ----SELECT users.* FROM users INNER JOIN group_users ON group_users.user_id = users.id WHERE active IS TRUE AND group_users.group_id = 8861 LIMIT 20;

Figure 1: A real-world Discourse rewrite from the WeTune benchmark that replaces an IN membership test with a join.

supported PostgreSQL fragment into fixed Rocq verification goals and combines LLM-guided synthesis of equivalence proofs and certified countermodels with a reusable SQL lemma library and domain-specific Rocq automation. Every resulting certificate is checked in isolation by the Rocq kernel. • We evaluate Logos against state-of-the-art SQL equivalence verifiers on a diverse suite of optimizer, decisionsupport, and real-application benchmarks, including Calcite, the TPC decision-support suites, and WeTune. Logos solves 86.9% of the query pairs, exceeding the bestperforming baseline, SQLSolver (64.0%), by 22.9 percentage points. These results show that mechanized SQL semantics combined with LLM-guided proof search substantially broadens the practical coverage of proof-producing equivalence verification.

2

OVERVIEW

Figure 1 shows a real-world Discourse rewrite from the WeTune benchmark [27]. The source selects active users whose identifiers occur among the members of group 8861. The target replaces this membership test with an inner join. The schema declares (group_id, user_id) unique in group_users, so a fixed group contributes at most one matching membership row per user. Both queries then retain at most 20 rows without specifying an order. Consider a database in which the relevant rows are summarized below. The symbols 𝑢 1, . . . , 𝑢 21 stand for distinct complete rows of users.

• We extend FormalSQL with a mechanized, compositional semantics for a typed SQL core with order-sensitive operators. Each query denotes all possible ordered lists and observable SQL failures in the supported fragment. The formalization provides executable Rocq semantics for PostgreSQLoriented scalar and aggregate evaluation. This includes NULL-sensitive evaluation and PostgreSQL numeric and temporal types (e.g., DECIMAL and TIMESTAMPTZ), with all supported failures explicit. To our knowledge, this is the first mechanized SQL semantics to combine nested, tiesensitive top-𝑘 with a closure-based lifting from bag equivalence to ordered-list equivalence while preserving compositionality across order-sensitive and correlated contexts. • We implement Logos as a proof-producing prototype for SQL equivalence verification. It lowers query pairs in its

User rows

active

Membership in group 8861

𝑢 1 , . . . , 𝑢 21 𝑣 𝑤

TRUE FALSE TRUE

one row per user one row none

Before applying limit, the source core retains exactly 𝑢 1, . . . , 𝑢 21 : the inactive row 𝑣 fails the first predicate, and 𝑤 fails the membership test. The target core reaches the same rows through the join. Uniqueness is essential here; it ensures that the join emits each 𝑢𝑖 once rather than multiplying it by several matching membership 2

3.1

rows. Thus, immediately before limit, the two query cores produce the same bag of 21 user rows with the same multiplicities and modeled failures. At this boundary, neither core establishes an order. Every permutation of the 21 rows is therefore a legal result, but all of these ordered lists have the same underlying bag. The collection of possible bags consequently has one member before limit. The limit makes the distinction observable. Because any 𝑢𝑖 may occur last, taking the first 20 rows can omit any one of the 21 users. The complete query therefore has 21 possible result bags, each containing a different 20-user subset. Logos records these alternatives separately instead of selecting one engine-dependent order or combining the alternatives into a single bag. Preserving this set of alternatives is necessary for equivalence reasoning, especially when the query is embedded as a subquery. Replacing the 21 possible bags by one arbitrarily selected bag would make the comparison depend on that choice: two equivalent queries could be assigned different 20-row bags even though they admit the same complete set of alternatives. The resulting loss of correspondence could cause equivalent queries to be reported as nonequivalent, and the discrepancy could propagate through the enclosing query. Logos makes these alternatives explicit. Write 𝐵 21 for the bag that contains each of 𝑢 1, . . . , 𝑢 21 once. On the database above, its compact summary of the possible bags at the two relevant boundaries is before limit: {𝐵 21 },

Thus, V𝜎 is the domain of well-typed row values conforming to 𝜎, and 𝑟 ∈ V𝜎 denotes a particular row value. The 𝑖th component of 𝑟 is a nullable value of type 𝜏𝑖 ; for 𝑎𝑖 : 𝜏𝑖 ∈ 𝜎, write 𝑟 [𝑎𝑖 ] for this component. Rows satisfy 𝑟 1 ≈𝜎 𝑟 2 when their corresponding components are related by the appropriate ≈𝜏 . Definition 1 (Finite bag). For a set 𝑋 , a finite bag over 𝑋 is a function 𝐵 : 𝑋 → N whose support {𝑥 ∈ 𝑋 | 𝐵(𝑥) > 0} is finite; 𝐵(𝑥) is the multiplicity of 𝑥. We write Bag(𝑋 ) for the set of finite bags over 𝑋 . When 𝑋 carries a semantic equivalence ≈𝑋 , let #𝐵 (𝑥) count all occurrences in 𝐵 equivalent to 𝑥, and write 𝐵 1 =B 𝐵 2 when #𝐵1 (𝑥) = #𝐵2 (𝑥) for every 𝑥 ∈ 𝑋 . Definition 2 (Finite list). For a set 𝑋 , the set of all finite lists over 𝑋 is List(𝑋 ) ≜ {[𝑥 1, . . . , 𝑥𝑛 ] | 𝑛 ∈ N ∧ ∀𝑖 ∈ {1, . . . , 𝑛}. 𝑥𝑖 ∈ 𝑋 }. (2)

after limit: {𝐵 21 \ {𝑢𝑖 } | 1 ≤ 𝑖 ≤ 21},

The case 𝑛 = 0 is the empty list [ ]; equivalently, finite lists are generated by ℓ ::= [ ] | 𝑥 :: ℓ for 𝑥 ∈ 𝑋 . Positions and repeated occurrences are retained. A list ℓ = [𝑥 1, . . . , 𝑥𝑛 ] induces bag(ℓ) ∈ Bag(𝑋 ) by counting occurrences. Thus bag forgets order but retains multiplicity; we write {{𝑥 1, . . . , 𝑥𝑛 }} for the resulting bag. For 𝐵 ∈ Bag(𝑋 ), write Rows(𝐵, ℓ) when bag(ℓ) =B 𝐵.

where subtraction removes the single occurrence of 𝑢𝑖 . The first set says that all legal core results share one bag; the second keeps the 21 alternatives created when limit observes their positions. This bag summary is not itself the query semantics. Logos retains ordered row sequences as its successful outcomes and keeps modeled SQL errors as separate outcomes. It forgets order only at a local proof boundary, without merging distinct possible bags. To verify the rewrite, Logos first proves that the two cores produce the same 𝐵 21 . It then establishes that both cores are bag closed: every ordering of 𝐵 21 is legal. These facts allow the local bag proof to recover equality of all ordered core outcomes, as formalized in Section 3.3. Semantic congruence then carries this equality through the common limit and, when present, through any enclosing query. Consequently, the complete queries preserve precisely the same 21 possible bags above, while genuine errors remain visible throughout the query context.

3

Notation and Typed Core Syntax

Let 𝜏 range over the supported SQL types, V𝜏 over their non-NULL values, and V𝜏⊥ = V𝜏 ⊎{NULL𝜏 } over their nullable values. A typed attribute 𝑎 : 𝜏 associates the column identifier 𝑎 with its SQL type 𝜏. Write 𝑣 1 ≈𝜏 𝑣 2 when two nullable values agree in the typed SQL value model; in particular, NULL𝜏 ≈𝜏 NULL𝜏 . An ordered relation signature 𝜎 = (𝑎 1 : 𝜏1, . . . , 𝑎𝑚 : 𝜏𝑚 ) is a finite sequence of typed attributes with distinct identifiers and fixes both column order and types, with V𝜎 = V𝜏⊥1 × · · · × V𝜏⊥𝑚 . (1)

Definition 3 (Schema and schema contract). A schema Σ maps each relation name 𝑅 to an ordered relation signature Σ(𝑅). A schema contract Γ is a finite set of integrity constraints over the relations and attributes declared by Σ. Definition 4 (Finite database). A finite database 𝐷 over Σ maps each declared relation 𝑅 to 𝐷 (𝑅) ∈ Bag(VΣ(𝑅) ). We write 𝐷 |= (Σ, Γ) when 𝐷 satisfies every constraint in Γ. Figure 2 presents the typed core syntax used by Logos. It covers the supported SQL query expressions, scalar expressions, predicates, and the integrity constraints admitted by schema contracts. The metavariables 𝑓 and 𝜃 range over the supported typed scalar and predicate operators, 𝑛 ∈ N, and 𝜑 row is a well-typed, subqueryfree predicate in the scope of its declared relation. The list 𝑊 = [𝑤 1, . . . , 𝑤𝑢 ] contains typed window outputs 𝑤 = (𝑎 : 𝜏,𝜓 ), where 𝜓 is row number, a cumulative aggregate over the current partition prefix, or an aggregate over the complete partition. The corresponding semantics supports common aggregate functions and typed scalar operators over the modeled SQL types. The query-expression category 𝑄 begins with two constant relations. Empty(𝜎) denotes the empty relation of signature 𝜎, whereas Singleton denotes the relation of empty signature () whose sole row is the empty tuple ⟨⟩. The latter supplies a unit input from which extended projection can construct a concrete row. Since Project

FORMAL SEMANTICS AND SEMANTIC DECOMPOSITION

The formal development of Logos is grounded in an ordered-list semantics of query execution, from which bag reasoning is derived as a controlled abstraction. Section 3.1 fixes the notation used throughout the paper and presents the typed core syntax of our supported SQL fragment. Section 3.2 gives this syntax an error-aware execution semantics and defines the resulting verification objective. Section 3.3 then establishes the closure conditions under which bag equivalence can be lifted to ordered outcome equivalence and composed with surrounding operators. Finally, Section 3.4 instantiates the development on the running example from Section 2. 3

Query Expressions

𝑄 ::= Empty(𝜎 ) | Singleton | Table(𝑅) | Set(OP set , 𝑄 1 , 𝑄 2 ) | CrossJoin(𝑄 1 , 𝑄 2 ) | Join(OP join , 𝑃, 𝑄 1 , 𝑄 2 ) | Project(𝐿, 𝑄 ) | Filter(𝑃, 𝑄 ) | Distinct(𝑄 ) | Group(𝐿, 𝐺, 𝑃, 𝑄 ) | GroupingSets( G, 𝑄 ) | Rank(𝐾𝑝 , 𝐾, 𝑎 rank : BIGINT, 𝑄 ) | Window(𝐾𝑝 , 𝐾,𝑊 , 𝑄 ) | OrderBy(𝐾, 𝑄 ) | Offset(𝑛, 𝑄 ) | Fetch(𝑛, 𝑄 )

No rows of signature 𝜎 One empty row of signature () Base relation 𝑅 Order-insensitive bag operation Cartesian product Outer/semi/anti join on 𝑃 Order-preserving projection Three-valued selection Duplicate elimination Grouped aggregation with having Shared-input grouping-set branches rank window Shared window evaluation Constrain output order Drop first 𝑛 rows Keep first 𝑛 rows

𝜎 ::= (𝑎 1 :𝜏1 , . . . , 𝑎𝑚 :𝜏𝑚 ) 𝐿 ::= [ (𝑉1 , 𝑎 1 :𝜏1 ), . . . , (𝑉𝑘 , 𝑎𝑘 :𝜏𝑘 ) ] 𝐺 ::= [𝑉1 , . . . , 𝑉𝑔 ] G ::= [ (𝐿1 , 𝐺 1 ), . . . , (𝐿𝑠 , 𝐺𝑠 ) ] 𝐾𝑝 , 𝐾 ::= [𝜅 1 , . . . , 𝜅𝑟 ] 𝜅 ::= (𝑎 :𝜏, 𝛿, 𝜈 ) 𝛿 ::= Asc | Desc 𝜈 ::= First | Last OP set ::= Union | Intersect | Except OP join ::= Left | Right | Full | Semi | Anti

Ordered relation signature Projection list Grouping expressions Nonempty grouping-set branch list Partition/order specification Typed sort key Sort direction NULL placement ALL-mode bag-operation kind Join kind

Scalar Expressions

𝑉 ::= 𝑐 : 𝜏 | 𝑎 : 𝜏 | 𝛼𝜔 (𝑉 ) : 𝜏 | 𝑓 (𝑉1 , . . . , 𝑉𝑟 ) : 𝜏 | Case(𝑃, 𝑉1 , 𝑉2 ) : 𝜏 | Subquery(𝑄 ) : 𝜏

Typed literal or attribute Aggregate application Scalar application Lazy case Scalar subquery

𝛼 ::= Count | Sum | Avg | Min | Max | · · · Aggregate operator 𝜔 ::= All | Distinct Aggregate duplicate policy 𝑓 ::= + | − | × | ÷ | Cast | Concat | · · · Scalar operator Predicates

𝑃 ::= True | 𝜃 (𝑉1 , . . . , 𝑉𝑟 ) | Not(𝑃 ) | And( [𝑃1 , . . . , 𝑃ℎ ] ) | Or( [𝑃1 , . . . , 𝑃ℎ ] ) | In( (𝑉1 , . . . , 𝑉𝑟 ), 𝑄 ) | Exists(𝑄 )

Truth constant Scalar predicate Three-valued negation SQL conjunction SQL disjunction Tuple membership Query nonemptiness Integrity Constraints

𝐶 ::= NotNull(𝑅, [𝑎 1 , . . . , 𝑎ℎ ] ) | PrimaryKey(𝑅, [𝑎 1 , . . . , 𝑎ℎ ] ) | Unique(𝑅, [𝑎 1 , . . . , 𝑎ℎ ] ) | ForeignKey 𝑅, [𝑎 1 , .
. . , 𝑎ℎ ], 𝑅 ′ , [𝑏 1 , . . . , 𝑏ℎ ] | Check(𝑅, 𝜑 row )
| UniqueIndex 𝑅, [𝑉1 , . . . , 𝑉𝑢 ], 𝜑 row

Nullability constraint Primary key Unique key Foreign key Row-local check Expression/partial unique index

Figure 2: Typed core syntax for queries and integrity constraints. evaluates its list once for each input row, Singleton makes that evaluation occur exactly once. For example,
Project [(1 : INTEGER, 𝑥 : INTEGER)], Singleton

An SQL program state is a pair Ω = (𝐷, 𝜌),

where 𝐷 is the finite database and 𝜌 = 𝛽 0 :: · · · :: 𝛽𝑘 :: 𝜖 is a list of visible row and group bindings, with the head 𝛽 0 denoting the innermost scope. The top-level environment is 𝜖, and an extension prepends its new binding to 𝜌.

has signature (𝑥 : INTEGER) and contains the single row ⟨1⟩; it is the core representation of the single-row table constructor VALUES (1). Bag union of such terms represents a multirow VALUES constructor. The remaining query constructors cover the relational and ordersensitive operators listed in Figure 2. Section 3.2 assigns them ordered-list semantics and specifies how modeled errors propagate from demanded subterms. The core set operators are the all variants with bag multiplicities; surface distinct variants are normalized into these operators and Distinct. Within this syntax, inner joins are represented by filtering a cross join, because the separate Join constructor is reserved for outer, semi, and anti joins.

3.2

(3)

Binding resolution. For a well-scoped typed attribute 𝑎 : 𝜏, define 𝑖 = min{ 𝑗 | 𝑎 : 𝜏 ∈ 𝜎𝛽 𝑗 ∧ ℓ𝛽 𝑗 ≠ [ ]}. If ℓ𝛽𝑖 = 𝑟 :: ℓ ′ , then resolve𝜌 (𝑎) = 𝑟 [𝑎]. Thus, resolution searches from the list head (the stack top) toward the outer bindings and returns the value from the first row of the nearest nonempty binding in which the attribute is visible. Attribute evaluation is given by resolve𝜌 (𝑎) = 𝑣 (𝐷, 𝜌) ⊢ 𝑎 : 𝜏 ⇓ ok(𝑣)

Error-Aware Execution Semantics and Equivalence

(Attribute)

A row binding supplies values to scalar expressions and predicates; a group binding additionally supplies the rows consumed by aggregate expressions. Subqueries inherit the current binding list, so an attribute not resolved by the innermost binding may refer to an enclosing one, as required for correlated subqueries. Let B3 = {T, F, U} and let Err be the domain of modeled SQL failures. Lowercase 𝑞 ranges over well-typed terms generated by 𝑄, while 𝑉 and 𝑃 range over the corresponding scalar and predicate terms. We write Ω ⊢ 𝑞 ⇓ ok(ℓ) when executing query 𝑞 in program state Ω may return the ordered row list ℓ ∈ List(V𝜎 ), and write Ω ⊢ 𝑞 ⇓ err(𝑒) when it may instead fail with 𝑒 ∈ Err. The symbol ⇓ is relational: the same query may derive multiple ordered-list outcomes. Analogously, Ω ⊢ 𝑉 ⇓ ok(𝑣) returns 𝑣 ∈ V𝜏⊥ , and Ω ⊢ 𝑃 ⇓ ok(𝑏) returns 𝑏 ∈ B3 ; either judgment may instead

Query execution depends on more than the database contents. A subquery may refer to row and group bindings supplied by its surrounding context, while unordered inputs and unresolved sort ties may admit multiple ordered lists. We first formalize the SQL program state that makes these dependencies explicit. Definition 5 (SQL program state). An SQL binding is a triple 𝛽 = (𝜎𝛽 , 𝑚 𝛽 , ℓ𝛽 ), where 𝜎𝛽 is its row signature, 𝑚 𝛽 is either Row or Group(𝐺), and ℓ𝛽 ∈ List(V𝜎𝛽 ). A row binding induced by 𝑟 ∈ V𝜎 is row𝜎 (𝑟 ) = (𝜎, Row, [𝑟 ]); a group binding stores in ℓ𝛽 all rows consumed by aggregate expressions. For 𝑔 ∈ List(V𝜎 ), write gbind𝜎,𝐺 (𝑔) = (𝜎, Group(𝐺), 𝑔). 4

Ω ⊢ Empty(𝜎 ) ⇓ ok( [ ] ) Ω ⊢ Singleton ⇓ ok( [ ⟨ ⟩ ] ) Rows(𝐷 (𝑅), ℓ ) Ω ⊢ Table(𝑅) ⇓ ok(ℓ )

( Singleton )

Ω[𝑟 ] ⊢ 𝐿 ⇓ err(𝑒 ) Ω ⊢ project𝐿 (𝑟 :: ℓ ) ⇓ err(𝑒 )

Ω ⊢ 𝑞 1 ⇓ err(𝑒 ) Ω ⊢ 𝐵 (𝑞 1 , 𝑞 2 ) ⇓ err(𝑒 )

Ω ⊢ 𝑞 ⇓ ok(ℓ ) Ω ⊢ filter𝑃 (ℓ ) ⇓ 𝑜 Ω ⊢ Filter(𝑃, 𝑞) ⇓ 𝑜

( Project )

Ω ⊢ filter𝑃 ( [ ] ) ⇓ ok( [ ] ) Ω[𝑟 ] ⊢ 𝑃 ⇓ err(𝑒 ) Ω ⊢ filter𝑃 (𝑟 :: ℓ ) ⇓ err(𝑒 )

( Proj-Err )

( Cross )

( Filter )

( Filter-Nil )

( Filter-Err )

Ω[𝑟 ] ⊢ 𝑃 ⇓ ok(𝑏 ) Ω ⊢ filter𝑃 (ℓ ) ⇓ 𝑜 Ω ⊢ filter𝑃 (𝑟 :: ℓ ) ⇓ keep(𝑏, 𝑟, 𝑜 )

( Proj-Cons )

Ω ⊢ 𝑞 ⇓ ok(ℓ0 ) GroupsΩ,𝐺 (bag(ℓ0 ), Π) Ω ⊢ groups𝐿,𝐺,𝑃 (Π) ⇓ ok(ℓ𝑔 ) Rows(bag(ℓ𝑔 ), ℓ ) Ω ⊢ Group(𝐿, 𝐺, 𝑃, 𝑞) ⇓ ok(ℓ ) Ω ⊢ 𝑞 ⇓ err(𝑒 ) Ω ⊢ 𝑈 (𝑞) ⇓ err(𝑒 )

Ω ⊢ 𝑞 1 ⇓ ok(ℓ1 ) Ω ⊢ 𝑞 2 ⇓ ok(ℓ2 ) Rows(bag(ℓ1 ) ⊗ bag(ℓ2 ), ℓ ) Ω ⊢ CrossJoin(𝑞 1 , 𝑞 2 ) ⇓ ok(ℓ )

( Set )

( Proj-Nil )

Ω[𝑟 ] ⊢ 𝐿 ⇓ ok(𝑟 ′ ) Ω ⊢ project𝐿 (ℓ ) ⇓ 𝑜 Ω ⊢ project𝐿 (𝑟 :: ℓ ) ⇓ cons(𝑟 ′ , 𝑜 )

( Join )

Ω ⊢ Join( 𝑗, 𝑃, 𝑞 1 , 𝑞 2 ) ⇓ 𝑜

Ω ⊢ Set(op, 𝑞 1 , 𝑞 2 ) ⇓ ok(ℓ ) Ω ⊢ 𝑞 ⇓ ok(ℓ ) Ω ⊢ project𝐿 (ℓ ) ⇓ 𝑜 Ω ⊢ Project(𝐿, 𝑞) ⇓ 𝑜

( Distinct )

Ω ⊢ 𝑞 1 ⇓ ok(ℓ1 ) Ω ⊢ 𝑞 2 ⇓ ok(ℓ2 ) Ω ⊢ joinB𝑗,𝑃 (bag(ℓ1 ), bag(ℓ2 ) ) ⇓ 𝑜

( Table )

Ω ⊢ 𝑞 1 ⇓ ok(ℓ1 ) Ω ⊢ 𝑞 2 ⇓ ok(ℓ2 ) Rows(setBop (bag(ℓ1 ), bag(ℓ2 ) ), ℓ )

Ω ⊢ project𝐿 ( [ ] ) ⇓ ok( [ ] )

Ω ⊢ 𝑞 ⇓ ok(ℓ0 ) Rows(distinctB (bag(ℓ0 ) ), ℓ ) Ω ⊢ Distinct(𝑞) ⇓ ok(ℓ )

( Empty )

( Filter-Cons )

Ω ⊢ 𝑞 ⇓ ok(ℓ0 ) Rows(bag(ℓ0 ), ℓ ) sorted𝐾 (ℓ ) Ω ⊢ OrderBy(𝐾, 𝑞) ⇓ ok(ℓ ) ( Group )

( Unary-Err )

Ω ⊢ 𝑞 ⇓ ok(ℓ ) Ω ⊢ Offset(𝑛, 𝑞) ⇓ ok(drop𝑛 (ℓ ) )

( Offset )

Ω ⊢ 𝑞 ⇓ ok(ℓ ) Ω ⊢ Fetch(𝑛, 𝑞) ⇓ ok(take𝑛 (ℓ ) )

( Fetch )

Ω ⊢ 𝑞 1 ⇓ ok(ℓ1 ) Ω ⊢ 𝑞 2 ⇓ err(𝑒 ) Ω ⊢ 𝐵 (𝑞 1 , 𝑞 2 ) ⇓ err(𝑒 )

( Left-Err )

( Order )

( Right-Err )

Figure 3: Big-step ordered-list semantic rules for part of the core query language. Here 𝑈 and 𝐵 range over well-typed unary and left-to-right binary query constructors. All metavariables are implicitly quantified over well-typed objects; in Group, Π ranges over lists of row groups and ℓ𝑔 over lists of rows produced from those groups. The auxiliary judgments are explained in Section 3.2. return err(𝑒). Scalar calls use their concrete typed interpretations, predicates use SQL three-valued logic, and Case executes only its selected branch. A scalar subquery returns its sole value, returns a typed null on an empty result, and raises a cardinality error on multiple rows. The In judgment applies SQL three-valued existential comparison, while Exists observes nonemptiness and evaluates only the subterms needed to determine it; both preserve errors from demanded subterms. Let 𝑄 𝜎 denote the well-typed query terms with output signature 𝜎, and write O𝜎 for the semantic domain of their results:

Auxiliary judgments. Figure 3 defines the big-step semantics for most of the well-typed SQL query expressions introduced in Figure 2.1 We next explain the auxiliary judgments and relations used in these rules. The superscript B marks an auxiliary relation that treats successful query inputs as bags: the enclosing rule replaces each child list ℓ by bag(ℓ), thereby discarding positions while retaining multiplicities. The auxiliary relation operates on these bags and produces a result bag 𝐵, which represents every ordered list ℓ ′ satisfying Rows(𝐵, ℓ ′ ); errors are propagated unchanged. This convention keeps the displayed judgments in the common result domain O𝜎 . For Ω = (𝐷, 𝜌) and 𝑟 ∈ V𝜎 , define

O𝜎 = {ok(ℓ) | ℓ ∈ List(V𝜎 )} ⊎ {err(𝑒) | 𝑒 ∈ Err}.

Ω[𝑟 ] = (𝐷, row𝜎 (𝑟 ) :: 𝜌),

For a fixed database 𝐷 and binding list 𝜌, query semantics is the set-valued map E𝐷,𝜌 : 𝑄 𝜎 → P (O𝜎 ), defined by E𝐷,𝜌 (𝑞) = {𝑜 ∈ O𝜎 | (𝐷, 𝜌) ⊢ 𝑞 ⇓ 𝑜}.

which makes 𝑟 the innermost visible row. This extension is used whenever an auxiliary judgment evaluates an expression against one input row.

(4)

Thus, a query denotes its complete relation of legal ordered lists and observable failures, rather than one execution selected by an engine.

1 The complete typing and semantic definitions, including the rules omitted from

Figure 3, are available in the FormalSQL mechanization at https://github.com/ WindOctober/FormalSQL. 5

Ω[𝑟 ] ⊢ 𝑉𝑗 ⇓ ok(𝑣 𝑗 ) (1 ≤ 𝑗 ≤ 𝑘) (List-Ok) Ω[𝑟 ] ⊢ 𝐿 ⇓ ok(⟨𝑎 1 = 𝑣 1, . . . , 𝑎𝑘 = 𝑣𝑘 ⟩)

Bag-level auxiliary relations. Recall that Rows(𝐵, ℓ) makes ℓ an arbitrary ordered representative of the bag 𝐵. The operation setBop applies the SQL bag operation designated by op; for example, the union all case adds multiplicities: #setB

Union (𝐵 1 ,𝐵 2 )

Ω[𝑟 ]⊢𝑉 𝑗 ⇓ok(𝑣 𝑗 ) 1≤ 𝑗 <𝑖

Ω[𝑟 ] ⊢ 𝑉𝑖 ⇓ err(𝑒) (List-Err) Ω[𝑟 ] ⊢ 𝐿 ⇓ err(𝑒) For 𝑟 ∈ V𝜎 and 𝑜 ∈ O𝜎 , projection and filtering use the following combinators: ( ok(𝑟 :: ℓ), 𝑜 = ok(ℓ), cons(𝑟, 𝑜) = err(𝑒), 𝑜 = err(𝑒), ( cons(𝑟, 𝑜), 𝑏 = T, keep(𝑏, 𝑟, 𝑜) = 𝑜, 𝑏 ∈ {F, U}.

(𝑟 ) = #𝐵1 (𝑟 ) + #𝐵2 (𝑟 ).

The operator distinctB assigns multiplicity one to every semantic row class occurring in its input bag. For rows 𝑟𝑖 ∈ V𝜎𝑖 with disjoint attributes, let 𝑟 1 ∥ 𝑟 2 be their concatenation, of signature 𝜎1 ∥ 𝜎2 . The bag product satisfies #𝐵1 ⊗𝐵2 (𝑟 1 ∥ 𝑟 2 ) = #𝐵1 (𝑟 1 )#𝐵2 (𝑟 2 ). The auxiliary join judgment joinB𝑗,𝑃 (𝐵 1, 𝐵 2 ) first evaluates 𝑃 on each candidate 𝑟 1 ∥ 𝑟 2 under the corresponding row binding. A pair matches exactly when this evaluation returns T; F and U do not match, and an error is propagated. The join kind 𝑗 then determines the result: left, right, and full joins add their respective null-extended unmatched rows, while semi and anti joins retain a left row according to whether a match exists. The auxiliary judgment then admits every ordered representative of the resulting bag. Grouping illustrates how a compound operator is defined at this boundary. Recall from Figure 2 that 𝐺 = [𝑉1, . . . , 𝑉𝑠 ] is a welltyped list of scalar expressions. Let 𝜎𝐺 be its induced ordered result signature. Evaluating 𝐺 under Ω[𝑟 ] assembles a key row 𝑘 ∈ V𝜎𝐺 , written Ω[𝑟 ] ⊢ 𝐺 ⇓ ok(𝑘). The grouping relation has signature

Projection consequently emits one row for each input position, whereas filtering returns a stable subsequence. Both judgments preserve the first error encountered in a demanded row. A sort specification 𝐾 = [𝜅 1, . . . , 𝜅𝑠 ] is a lexicographic list of keys 𝜅 = (𝑎 : 𝜏, 𝛿, 𝜈), where 𝛿 chooses ascending or descending comparison and 𝜈 places nulls first or last. Write 𝑟 ⪯𝐾 𝑟 ′ when the first key on which 𝑟 and 𝑟 ′ differ orders 𝑟 before 𝑟 ′ (or all keys tie). Then sorted𝐾 ([𝑟 1, . . . , 𝑟𝑚 ])

⇐⇒

∀𝑖 < 𝑚. 𝑟𝑖 ⪯𝐾 𝑟𝑖+1 .

Together, Rows(bag(ℓ0 ), ℓ) and sorted𝐾 (ℓ) state that ℓ is a 𝐾-sorted permutation of the input occurrences; no order is imposed between rows that tie on all keys. For ℓ = [𝑟 1, . . . , 𝑟𝑚 ], the positional operators are take𝑛 (ℓ) = [𝑟 1, . . . , 𝑟 min(𝑛,𝑚) ], drop𝑛 (ℓ) = [𝑟 min(𝑛,𝑚)+1, . . . , 𝑟𝑚 ]. Here an empty index interval denotes [ ]. The rules in Figure 3 expose the order boundary directly. Projection and filtering transform one selected child list without reordering it. Table scans, bag operations, and the auxiliary judgments for joins and grouping do not preserve child positions; they directly admit their legal ordered outputs. Sorting admits every bag-preserving list satisfying 𝐾, so ties remain nondeterministic, whereas offset and fetch consume concrete positions. For any outcome relation 𝐸 ⊆ O𝜎 , define

GroupsΩ,𝐺 ⊆ Bag(V𝜎 ) × List(List(V𝜎 )). To derive GroupsΩ,𝐺 (𝐵, Π), choose an ordered representative ℓ = [𝑟 1, . . . , 𝑟𝑛 ] of 𝐵 and evaluate one key row for each occurrence: Û Rows(𝐵, ℓ), Ω[𝑟𝑖 ] ⊢ 𝐺 ⇓ ok(𝑘𝑖 ). 1≤𝑖 ≤𝑛

Rows whose key rows are related by ≈𝜎𝐺 belong to the same group. Taking the first occurrence of each key as its representative gives h i 1≤𝑖 ≤𝑛, Π = [𝑟𝑡 | 𝑘𝑡 ≈𝜎𝐺 𝑘𝑖 ] ¬∃ℎ<𝑖. 𝑘ℎ ≈𝜎𝐺 𝑘𝑖 .

Succ(𝐸) = {ℓ | ok(ℓ) ∈ 𝐸},

Both comprehensions range over input positions in increasing order, so duplicates are retained and first-occurrence order is preserved. The SQL global-group convention is GroupsΩ,[ ] (∅, [[ ]]). For Ω = (𝐷, 𝜌) and 𝑔 ∈ List(V𝜎 ), write

Errs(𝐸) = {𝑒 | err(𝑒) ∈ 𝐸}.

Definition 6 (Observation and outcome equivalence). Using the typed value and row equivalences from Section 3.1, write ℓ1 ≈L ℓ2 when two lists have equal length and their rows are related positionwise by ≈𝜎 . Two sets of legal lists match in both directions when 𝑂 1 ≡L 𝑂 2 ⇔ (∀ℓ1 ∈ 𝑂 1 . ∃ℓ2 ∈ 𝑂 2 . ℓ1 ≈L ℓ2 ) ∧ (5) (∀ℓ2 ∈ 𝑂 2 . ∃ℓ1 ∈ 𝑂 1 . ℓ1 ≈L ℓ2 ).

Ω⟨𝐺, 𝑔⟩ = (𝐷, gbind𝜎,𝐺 (𝑔) :: 𝜌). The judgment Ω ⊢ groups𝐿,𝐺,𝑃 (Π) ⇓ 𝑜 processes each 𝑔 ∈ Π under Ω⟨𝐺, 𝑔⟩. It first finalizes the aggregate applications required by 𝐿 and 𝑃, then evaluates 𝑃 as having. On success it produces   ℓ𝑔 = 𝑟𝑔 | 𝑔 ← Π, Ω⟨𝐺, 𝑔⟩ ⊢ 𝑃 ⇓ ok(T), Ω⟨𝐺, 𝑔⟩ ⊢ 𝐿 ⇓ ok(𝑟𝑔 ) .

For full outcome relations over one signature, define 𝐸 1 ≡out 𝐸 2 ⇔ 𝐸 1 ≠ ∅ ∧ 𝐸 2 ≠ ∅ ∧ Succ(𝐸 1 ) ≡L Succ(𝐸 2 ) ∧ Errs(𝐸 1 ) = Errs(𝐸 2 ).

Thus F and U discard a group, while demanded failures are propagated. Order-aware list operations. The order-sensitive auxiliary operations act on concrete list positions. Recall from Figure 2 that 𝐿 = [(𝑉1, 𝑎 1 : 𝜏1 ), . . . , (𝑉𝑘 , 𝑎𝑘 : 𝜏𝑘 )]. Its left-to-right evaluation is specified by the following rule schemes:

(6)

An outcome relation is safe when it contains at least one successful result and no failure: Safe(𝐸) ⇔ Succ(𝐸) ≠ ∅ ∧ Errs(𝐸) = ∅. Safe outcome equivalence is therefore

Ω[𝑟 ] ⊢ [ ] ⇓ ok(⟨⟩)

(List-Nil)

𝐸 1 ≡safe 𝐸 2 ⇔ 𝐸 1 ≡out 𝐸 2 ∧ Safe(𝐸 1 ) ∧ Safe(𝐸 2 ). 6

(7)

The inhabitedness conditions exclude vacuous equivalence of malformed relations; an equivalence certificate must establish at least one legal outcome on each side. Successful results never match errors, and distinct modeled failures remain distinguishable.

Indeed, the lists have the same length and pair equivalent rows at every position, so each row-equivalence class has the same multiplicity. For the forward direction, assume 𝐸 1 ≡out 𝐸 2 . Equation (6) immediately gives

Schema conformance is part of the semantic premise. Constraints in Γ are interpreted over the same nullable values and three-valued predicates as query execution; row predicates and expression-index terms must also evaluate without error when their constraint requires them. The complete satisfaction relation is mechanized in the FormalSQL development cited above.

Errs(𝐸 1 ) = Errs(𝐸 2 ), Let 𝐵 ∈ Bags(𝑂 1 ). By Equation (11),

∃ℓ1 ∈ 𝑂 1 . bag(ℓ1 ) =B 𝐵. Forward list matching then supplies an ℓ2 ∈ 𝑂 2 such that (∗)

Definition 7 (Query equivalence contracts). For query terms 𝑞 1 and 𝑞 2 with the same output signature, the default verification contract is unconditional, error-preserving equivalence: (Σ, Γ) |= 𝑞 1 ≡ 𝑞 2 ⇔ ∀𝐷 |= (Σ, Γ). E𝐷,𝜖 (𝑞 1 ) ≡out E𝐷,𝜖 (𝑞 2 ).

ℓ1 ≈L ℓ2 =⇒ bag(ℓ1 ) =B bag(ℓ2 ) =⇒ 𝐵 ∈ Bags(𝑂 2 ), where the last implication also uses symmetry and transitivity of =B . Thus Bags(𝑂 1 ) ⊆ Bags(𝑂 2 ). The backward matching clause gives the reverse inclusion, and hence Bags(𝑂 1 ) = Bags(𝑂 2 ). Conversely, assume equality of the two bag projections and of the two error sets. For any ℓ1 ∈ 𝑂 1 , reflexivity of =B and equality of the projections give

(8)

Safe equivalence additionally requires both queries to have at least one successful outcome and no error on any conforming database: (Σ, Γ) |= 𝑞 1 ≡safe 𝑞 2 ⇔ ∀𝐷 |= (Σ, Γ). E𝐷,𝜖 (𝑞 1 ) ≡safe E𝐷,𝜖 (𝑞 2 ).

ℓ1 ∈ 𝑂 1 =⇒ bag(ℓ1 ) ∈ Bags(𝑂 1 ) = Bags(𝑂 2 ).

(9) Conditional extension. A well-typed precondition Φ restricts either contract to databases that satisfy it. For the default errorpreserving contract, this gives ∀𝐷 |= (Σ, Γ). Φ(𝐷) ⇒ E𝐷,𝜖 (𝑞 1 ) ≡out E𝐷,𝜖 (𝑞 2 ).

Since 𝑂 2 is closed, Definition 8 now supplies ∃ℓ2 ∈ 𝑂 2 . ℓ1 ≈L ℓ2 . Thus every observation in 𝑂 1 has a matching observation in 𝑂 2 . Applying the same argument with the sides reversed and using closure of 𝑂 1 gives 𝑂 1 ≡L 𝑂 2 . Finally, the assumed inhabitedness of 𝐸 1 and 𝐸 2 , together with error-set equality, discharges all clauses of Equation (6). □

(10)

The safe conditional variant replaces ≡out with ≡safe . In either case, the certificate must establish that Φ either follows from the input contract or is jointly satisfiable with it. Every database quantifier ranges over arbitrary finite cardinalities. Failed proof search reports unknown; it does not weaken any of these contracts. The outcome relation remains the specification at every query boundary. The next section characterizes when its successful ordered lists may be replaced locally by possible bags.

3.3

This closure property arises throughout the core query language. In fact, let R = {Empty, Singleton, Table, Set, CrossJoin, Join, Distinct, Group, GroupingSets, Rank, Window}.

Lifting Bag Equivalence to Ordered-List Equivalence

We define the syntactic certificate as ( true, the outer constructor of 𝑞 is in R, cert(𝑞) = false, otherwise.

Fix an output signature 𝜎 and let 𝑂 ⊆ List(V𝜎 ) be a relation of successful ordered observations. Its order-forgetting projection is Bags(𝑂) = {𝐵 | ∃ℓ ∈ 𝑂. bag(ℓ) =B 𝐵}.

Theorem 10 (Closure-certificate soundness). For every admitted 𝑞,
cert(𝑞) = true =⇒ ∀𝐷, 𝜌. Closed Succ(E𝐷,𝜌 (𝑞)) . (15)

(12) Proof sketch. Inspect the execution rule for each constructor in R. Its successful result does not fix the order of the returned row list: once one list represents the computed bag, every permutation of that list is also admitted. Hence its successful observations contain every ordering of each possible result bag, which is precisely the closure property in Definition 8. □

The following theorem is the central lifting result: at bag-closed boundaries, equality of possible bags and failures characterizes outcome equivalence over ordered lists. Theorem 9 (Bag-to-list lifting). Let 𝐸 1 and 𝐸 2 be inhabited outcome relations over the same signature, and let 𝑂𝑖 = Succ(𝐸𝑖 ). If Closed(𝑂 1 ) and Closed(𝑂 2 ), then

In contrast, Project and Filter preserve the order selected by their child rather than reset it: applied to [𝑟 1, 𝑟 2 ], they retain the corresponding projected or retained rows in that order, without independently admitting the reverse order. Establishing closure for either operator therefore requires additional premises about its child and row-level expressions. A failed certificate leaves the

𝐸 1 ≡out 𝐸 2 ⇔ Bags(𝑂 1 ) = Bags(𝑂 2 ) ∧ Errs(𝐸 1 ) = Errs(𝐸 2 ). (13) Proof. First observe that position-wise list equivalence preserves row multiplicities: ℓ1 ≈L ℓ2 =⇒ bag(ℓ1 ) =B bag(ℓ2 ).

(14)

(11)

Definition 8 (Bag closure). 𝑂 is bag closed, written Closed(𝑂), when ∀ℓreq . bag(ℓreq ) ∈ Bags(𝑂) =⇒ ∃ℓobs ∈ 𝑂. ℓreq ≈L ℓobs .

𝑂 1 ≡L 𝑂 2 .

(∗) 7

ordered-list semantics unchanged and does not authorize forgetting order. Once Theorem 9 recovers outcome equivalence at a bag-closed boundary, semantic congruence permits an outcome-equivalent child to be replaced inside an enclosing operator. For Fetch, the property used below is

on their well-typed row bindings. Uniformly in 𝐷 and 𝜌, we obtain Bags(Succ(E𝐷,𝜌 (𝐶 src ))) = Bags(Succ(E𝐷,𝜌 (𝐶 tgt ))), Errs(E𝐷,𝜌 (𝐶 src )) = Errs(E𝐷,𝜌 (𝐶 tgt )) = ∅.

The successful observations of both cores are bag closed. For 𝐶 src , the table scan admits every input permutation, the filters act pointwise, and In depends on membership in 𝐼 rather than the order of its rows. For 𝐶 tgt , CrossJoin resets order, after which pointwise filtering and projection commute with permutations. The closure lemmas of Section 3.3 therefore give

Closed Succ(E𝐷,𝜌 (𝐶 src )) , Closed Succ(E𝐷,𝜌 (𝐶 tgt )) . (20)

E𝐷,𝜌 (𝑞 1 ) ≡out E𝐷,𝜌 (𝑞 2 ) =⇒ E𝐷,𝜌 (Fetch(𝑛, 𝑞 1 )) ≡out E𝐷,𝜌 (Fetch(𝑛, 𝑞 2 )). It follows because take𝑛 preserves position-wise list equivalence and Fetch propagates child errors unchanged. FormalSQL mechanizes the analogous congruence lemmas for query, scalar, and predicate contexts.

3.4

(19)

The outcome relations are inhabited, so Theorem 9, together with Equations (19) and (20), yields E𝐷,𝜌 (𝐶 src ) ≡out E𝐷,𝜌 (𝐶 tgt ).

Formalizing the Running Example

We now instantiate the preceding results for the rewrite in Figure 1. Fix a schema Σ containing users and group_users. Let 𝐿𝑈 be the complete typed projection list for users. The following well-typed core predicates are obtained by lowering the corresponding SQL conditions:

(21)

Applying this Fetch property to Equation (21) gives outcome equivalence for 𝑆 and 𝑇 . On the 21-user instance from Section 2, this gives the same 21 possible 20-row bags on both sides. Theorem 11 (Rewrite eqivalence). Under the schema contract (Σ, Γ) above, (Σ, Γ) |= 𝑆 ≡ 𝑇 . (22)

• 𝑃𝐴 := users.active IS TRUE; • 𝑃𝐺 := group_users.group_id = 8861; and • 𝑃 𝐽 := users.id = group_users.user_id. The two query cores and their enclosing limits are

Proof. Fix 𝐷 |= (Σ, Γ). Instantiating Equation (21) at 𝜌 = 𝜖 and applying the Fetch property above gives

𝑈 = Filter(𝑃𝐴 , Table(users)),

E𝐷,𝜖 (𝑆) ≡out E𝐷,𝜖 (𝑇 ).

𝑀 = Filter(𝑃𝐺 , Table(group_users)),

The claim follows from Definition 7, since 𝐷 was arbitrary and 𝑆,𝑇 have the same output signature. □

𝐼 = Project([user_id], 𝑀), (16)

𝐶 src = Filter(In((id), 𝐼 ), 𝑈 ),

4

𝐶 tgt = Project(𝐿𝑈 , Filter(𝑃 𝐽 , CrossJoin(𝑈 , 𝑀))), 𝑆 = Fetch(20, 𝐶 src ),

Logos2 comprises a typed SQL frontend, the FormalSQL Rocq library, and an untrusted proof-search loop. SQLGlot translates the declared input dialect to Calcite-compatible SQL [15]; Calcite resolves types and operators [4]; and the Rust frontend lowers Calcite’s intermediate representation to the Rocq representation of the typed core shown in Figure 2. In Rocq, we refactor and extend SQLCoq [5] into FormalSQL, an order-sensitive semantic library. FormalSQL mechanizes the complete execution and error semantics underlying Figure 3 and provides the bridge between bag and ordered-list equivalence developed in Section 3.3. Its library contains over 2,000 verified lemmas. They primarily support three parts of verification: compositional query rewrites, such as merging adjacent projections; reasoning about scalar and grouped expressions under schema constraints, such as proving two scalar expressions equivalent in their respective typed theories; and semantic lifting, such as transporting local equivalence proofs across query constructors and enclosing contexts while preserving errors and observable order. For each input SQL query pair, Logos generates a Rocq verification task that formalizes its schema constraints, queries, and equivalence statement under FormalSQL semantics. It then invokes a proof agent, which determines whether to prove equivalence or establish non-equivalence. To focus the agent on proof construction rather than repository navigation, Logos provides a compact

𝑇 = Fetch(20, 𝐶 tgt ).

Here LIMIT 20 lowers to Fetch(20, ·) without an OrderBy, and hence consumes an unconstrained child order. Assume that Γ contains the benchmark’s NOT-NULL declarations, the primary key on users.id, and a unique key on the group_users attribute pair (group_id, user_id). Fix 𝐷 |= (Σ, Γ) and a binding list 𝜌, and write Ω = (𝐷, 𝜌). For each of 𝑈 , 𝑀, 𝐶 src , and 𝐶 tgt , all successful observations differ only in order; write 𝐵𝑈 , 𝐵𝑀 , 𝐵 src , and 𝐵 tgt for their respective underlying result bags. For a user row 𝑢, define the number of matching membership occurrences by ∑︁   𝑁 (𝑢) = #𝐵𝑀 (𝑚) · 1 Ω[𝑢 ∥ 𝑚] ⊢ 𝑃 𝐽 ⇓ ok(T) . (17) 𝑚∈supp(𝐵𝑀 )

The indicator is one exactly when 𝑃 𝐽 evaluates to T under the joined row binding for 𝑢 and 𝑚, and zero otherwise. The source retains each occurrence of 𝑢 iff 𝑁 (𝑢) > 0, whereas the target produces one projected occurrence for every match. Their multiplicities are therefore #𝐵src (𝑢) = #𝐵𝑈 (𝑢)1[𝑁 (𝑢) > 0],

IMPLEMENTATION

#𝐵tgt (𝑢) = #𝐵𝑈 (𝑢)𝑁 (𝑢). (18)

Since 𝑀 restricts group_id to 8861, the unique key gives 𝑁 (𝑢) ∈ {0, 1}. Equation (18) thus establishes equal multiplicities for every user row. Moreover, all scalar operations in 𝑃𝐴 , 𝑃𝐺 , and 𝑃 𝐽 are total

2 https://github.com/WindOctober/Logos

8

Table 1: Composition and input-query characteristics of the 389 benchmark pairs. Corpus Benchmark family Literature [13] Calcite [4, 13] R-Bot TPC-H [22, 24] R-Bot DSB [11, 22] TPC-DS variants [25] WeTune [27]

Input-query structure (P50/P90)

Pairs containing feature (%)

Pairs

Schemas (tables)

Query operators

Join occurrences

Agg./ dist.

Subq. (corr.)

Set ops

Outer join

Order/ slice

Top-𝑘

Window

30 236 22 37 14 50

24 (1–4) 1 (6) 1 (8) 1 (25) 1 (25) 7 (22–332)

6/9 6/10 12/18 22/50 34.5/72 9.5/17

1/2 1/2 1/5 6/11 5/15 1/3

50% 42.4% 100% 97.3% 100% 44%

13.3% (0%) 11% (2.5%) 45.5% (27.3%) 35.1% (21.6%) 28.6% (14.3%) 72% (26%)

13.3% 10.2% 0% 18.9% 92.9% 26%

0% 26.7% 4.5% 10.8% 28.6% 28%

0% 7.6% 100% 94.6% 100% 30%

0% 3% 100% 75.7% 100% 20%

0% 0.8% 0% 0% 35.7% 0%

Schemas (tables) reports distinct schemas and the range of table counts. The query operators metric counts projections, scans, joins, filters, aggregation or duplicate elimination, set operations, ordering/slicing, windows, and VALUES. Nested queries are included, with each CTE definition counted once. The join occurrences metric counts explicit joins and comma-separated FROM items. Pair-level P50/P90 use the larger query. Feature percentages count a pair when either query contains the feature; shading shows prevalence, and columns may overlap. Agg./dist. covers aggregation, grouping, and duplicate elimination; parentheses under Subq. report correlated subqueries. Top-𝑘 counts LIMIT/FETCH, but not OFFSET alone.

FormalSQL semantic context together with semantic indexes for the lemma library. Non-equivalence cannot in general be certified merely by generating a database instance and executing it in a deterministic engine such as PostgreSQL [18]. FormalSQL may assign a query a set of possible ordered-list results, whereas one concrete execution observes only a single result. Logos therefore accepts non-equivalence only through a countermodel checked against the complete FormalSQL semantics or an observable mismatch between the queries’ output signatures.

5

and the TPC-DS variants instead supply substantially larger analytical queries, with P90 operator counts of 50 and 72 and join counts of 11 and 15. TPC-DS also provides the broadest feature interactions: every pair combines aggregation, ordering, and top-𝑘, while 92.9% contain set operations and 35.7% contain windows. Thus, the corpus progresses from localized optimizer rewrites to feature-rich analytical workloads and tests order sensitivity in composition with other SQL operators. Environment. We run all experiments on a Linux server with an AMD Ryzen 9 5950X CPU (16 cores and 32 hardware threads) and 128 GB of memory. Every tool receives a 14,400-second wall-clock budget and a 16 GB memory limit per query pair, and we report per-case end-to-end time rather than campaign makespan. Logos uses the gpt-5.6-sol proof agent at medium reasoning effort and permits at most three counterexample rounds. Each proof-agent sandbox is limited to 6 GB of memory and 2 GB of writable storage; proof search and trusted Rocq checking are capped at 14,100 and 420 seconds, respectively.

EVALUATION

We evaluate Logos on 389 query pairs from six benchmark families and compare it with three unbounded SQL verifiers. Our evaluation addresses two questions: • RQ1 (Effectiveness): How does the verification coverage of Logos compare with existing verifiers? • RQ2 (Efficiency): What is the runtime of Logos, and where are its main performance bottlenecks?

5.1

Baselines. We compare Logos with three unbounded SQL equivalence verifiers using their original implementations: • Cosette uses Rosette, a solver-aided language embedded in Racket [23], for bounded counterexample search, and Coq for checked proofs over K-relations and UniNomials [8]. • SQLSolver reduces U-expressions with unbounded summations to an extension of linear integer arithmetic discharged by SMT solvers [12]. • QED normalizes queries into a sum-product normal form and proves equality through stabilization and recursive unification, using SMT solvers for first-order side conditions [26].

Experimental Setup

Benchmarks. Our corpus combines six complementary benchmark families. The Literature family contains 30 standard-SQL query pairs from VeriEQL’s Literature benchmark [13], while Calcite contains 236 pairs derived from Apache Calcite optimizer tests [4, 13]. The R-Bot TPC-H and R-Bot DSB families contain 22 and 37 decision-support query pairs, respectively. For these families, we generate each target reproducibly by applying a single rewrite with a pinned version of R-Bot’s Calcite rewrite engine [22]. They are therefore deterministic rewrite workloads rather than unpublished LLM outputs from the R-Bot study. The TPC-DS variants family pairs 14 official base templates with their corresponding variants. Finally, WeTune contributes 50 before/after rewrites taken from commits in seven open-source applications [27]. Table 1 shows that corpus complexity is multidimensional. Literature and Calcite account for 266 of the 389 pairs, but their individual queries are relatively small: their P90 sizes are 9 and 10 operators, respectively, with two join occurrences in both families. WeTune shifts the stress to application context: its seven schemas contain 22–332 tables, and 72% of its pairs contain subqueries. R-Bot DSB

Cosette requires its dedicated DSL, whereas SQLSolver and QED accept Calcite-compatible SQL subsets. Since the benchmark families span several source dialects, we build tool-specific materialization adapters on SQLGlot to translate each case’s declared dialect into the corresponding schema and query pair. This lets every verifier run through its intended frontend.

5.2

RQ1: Comparison with Existing Verifiers

Table 2 reports coverage by benchmark family. Across the full corpus, Logos solves 338 pairs (86.9%), compared with 249 (64.0%) for 9

Table 2: Comparison of automated SQL equivalence verifiers by benchmark family. Benchmark family

Logos

Pairs

SQLSolver

QED

Cosette

Solved

Timeout

Unsupported

Solved

Timeout

Unsupported

Solved

Timeout

Unsupported

Solved

Timeout

Unsupported

Literature Calcite R-Bot TPC-H R-Bot DSB TPC-DS variants WeTune

30 236 22 37 14 50

28 (93.3%) 227 (96.2%) 16 (72.7%) 24 (64.9%) 9 (64.3%) 34 (68.0%)

2 (6.7%) 9 (3.8%) 6 (27.3%) 12 (32.4%) 5 (35.7%) 13 (26.0%)

0 (0.0%) 0 (0.0%) 0 (0.0%) 1 (2.7%) 0 (0.0%) 3 (6.0%)

23 (76.7%) 183 (77.5%) 16 (72.7%) 9 (24.3%) 3 (21.4%) 15 (30.0%)

0 (0.0%) 1 (0.4%) 0 (0.0%) 14 (37.8%) 4 (28.6%) 3 (6.0%)

7 (23.3%) 52 (22.0%) 6 (27.3%) 14 (37.8%) 7 (50.0%) 32 (64.0%)

16 (53.3%) 156 (66.1%) 5 (22.7%) 19 (51.4%) 2 (14.3%) 15 (30.0%)

0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%)

14 (46.7%) 80 (33.9%) 17 (77.3%) 18 (48.6%) 12 (85.7%) 35 (70.0%)

14 (46.7%) 36 (15.3%) 0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%)

0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%) 0 (0.0%)

16 (53.3%) 200 (84.7%) 22 (100.0%) 37 (100.0%) 14 (100.0%) 50 (100.0%)

Aggregate

389

338 (86.9%)

47 (12.1%)

4 (1.0%)

249 (64.0%)

22 (5.7%)

118 (30.3%)

213 (54.8%)

0 (0.0%)

176 (45.2%)

50 (12.9%)

0 (0.0%)

339 (87.1%)

Cumulative Runtime Across Solved Cases

Cumulative runtime (log scale)

SQLSolver, the strongest baseline—an improvement of 22.9 percentage points. Logos attains the highest solved count on every family, tying SQLSolver only on R-Bot TPC-H. The advantage grows on the 104 order-sensitive pairs identified by Table 1: Logos solves 76 (73.1%), whereas SQLSolver solves 43 (41.3%), QED 35 (33.7%), and Cosette 5 (4.8%). Thus the aggregate improvement is not obtained solely from the predominantly unordered Calcite family. Examining the solved-case intersections, Logos solves 72 cases that no other evaluated verifier solves, compared with 13 for SQLSolver, four for QED, and none for Cosette. The baseline portfolio collectively covers another six cases through the overlap of SQLSolver and QED, so its total contribution beyond Logos is 23 cases. Verification coverage also depends on whether a tool can carry a case through its input and semantic interfaces. Table 2 uses Unsupported for non-definite outcomes other than timeouts, including syntax and lowering failures, model or prover limitations, and solver errors. Only four Logos cases (1.0%) fall into this category, compared with 118 (30.3%) for SQLSolver, 176 (45.2%) for QED, and 339 (87.1%) for Cosette. Thus, Logos carries 99.0% of the corpus either to a definite result or into proof search, even when that search eventually exhausts its budget. The cross-tool intersections show that this broader support translates into verified results. Of the 118 pairs unsupported by SQLSolver, Logos solves 94 (79.7%); another 20 reach proof search but time out. Conversely, among the 108 pairs solved by Logos but not by SQLSolver, 94 (87.0%) lie outside SQLSolver’s supported fragment, while only 14 are SQLSolver timeouts. The principal gain is therefore semantic reach rather than merely a stronger decision procedure over the same fragment: a comparatively comprehensive typed core, combined with agent-guided proof construction, makes proof-producing verification effective on application-scale query pairs that existing models cannot represent. This support gap is most visible in the 101 feature-rich cases from R-Bot DSB, TPC-DS variants, and WeTune: Logos solves 67, compared with 36 for QED, 27 for SQLSolver, and none for Cosette. QED is designed to establish equivalence rather than certify inequivalence, and its bag-semantics model leaves ordering and concrete aggregate behavior largely abstract. SQLSolver’s linear-arithmetic reduction loses completeness on nonlinear expressions, supports only a restricted range of aggregate reasoning, and handles ordering when the two queries have compatible outer ordering and slicing structures rather than compositionally nested top-𝑘. Cosette is further constrained by its DSL and integer-encoded, unordered relational model. By contrast, Logos covers these features within one typed, order-sensitive semantics. Its four unsupported cases

Logos SQLSolver QED Cosette

96h 48h 24h 4h 1h 10m

1m 10s

1s 0

50

100

150

200

250

300

350

Case rank, sorted by per-tool runtime

Figure 4: Cumulative runtime on solved cases, sorted by each tool’s per-case wall-clock time.

arise from isolated frontend and formalization gaps; we analyze the much larger set of timeouts, together with the resulting optimization opportunities, in RQ2. Answer to RQ1. Logos provides the greatest coverage overall and in every benchmark family, solving 22.9 percentage points more pairs than the strongest unbounded baseline while leaving only 1.0% of the corpus unsupported. Its advantage is particularly pronounced for order-sensitive pairs, where it improves the solved rate from 41.3% to 73.1%.

5.3

RQ2: Runtime and Bottlenecks

Figure 4 compares end-to-end wall-clock time only on the cases each tool solves. The baseline medians are 1.4 seconds for QED, 1.7 seconds for SQLSolver, and 8.5 seconds for Cosette. Logos is substantially slower: its median is 3,632 seconds (60.5 minutes), and its 338 solved cases accumulate 396.3 hours, compared with 1.70 hours for SQLSolver, 0.20 hours for QED, and 0.12 hours for Cosette. This gap is the tradeoff of Logos’s Rocq-plus-agent route: the same general semantics that yields high solved and support rates also leaves proof construction to a comparatively expensive synthesis loop. We analyze all 332 cases that enter agent-guided verification, including both completed proofs and timeouts. Their proof-agent rounds consume 563.3 hours. Of this time, 493.2 hours (87.6%) occur outside diagnostic Rocq invocations and cover model deliberation and proof orchestration; 70.1 hours (12.4%) are spent compiling 10

candidate proofs. The bottleneck is therefore proof synthesis rather than Rocq compilation alone. The 338 solved cases comprise 243 equivalence results and 95 non-equivalence results. Every equivalence result has a Rocq certificate; among these 243 certificate modules, 224 (92.2%) directly invoke the Logos-specific lemma library, while 58 (23.9%) use a bag-to-list bridge. Each diagnostic request submits the current candidate Rocq module to the checker. Across all 332 agent cases, 53,565 such submissions contain 20,834,738 lines of candidate Rocq source in total, with a mean of 62,755 lines and a median of 32,002 lines per case. Of these submissions, 50,841 do not compile, consuming 67.9 of the 70.1 diagnostic hours. The agent thus automates Rocq proof development, but currently pays for that automation through many iterations over incomplete proof states. The lemma library and bagto-list bridges reduce this repeated work by packaging proof-term combinations that would otherwise have to be reconstructed from the execution semantics. This cost is not an intended property of the semantics. Off-theshelf SMT theories do not natively provide the combination required here: a set of alternative legal row sequences together with the type- and NULL-aware semantics of SQL aggregates such as AVG, MIN, and MAX. cvc5 provides distinct finite-bag and sequence theories [3], but their primitives define neither the correspondence between a bag and all row orders admitted by SQL nor SQL-specific aggregate behavior. An SMT encoding could represent result sequences using arrays and explicit lengths, but equivalence proofs would then require auxiliary invariants relating indices, legal orders, and aggregate states, together with solver guidance to instantiate these invariants across operators. Rocq lets us define this combination directly and kernel-check the result, while the measurements identify deterministic proof templates, more selective lemma retrieval, and incremental diagnostics as the main avenues for reducing synthesis cost.

across the corpus but does not eliminate dialect-specific discrepancies. Agent-guided proof search is also not fully deterministic. Variation in model serving, response latency, and proof-step selection can change both the route taken through the proof space and the wall-clock time of an individual run. Consequently, the reported runtime distribution and timeout boundary may vary under repeated campaigns, even with fixed prompts and budgets.

6

This section reviews order-aware query semantics and SQL equivalence verification. Table 3 compares representative foundations and systems along five dimensions. Unbounded checking ranges over databases of arbitrary finite cardinality. Alternative ordered lists records whether a model retains every order permitted by SQL, while compositional top-𝑘 further requires these alternatives to survive slicing and remain visible to enclosing queries. Thus, although [𝑎, 𝑏] and [𝑏, 𝑎] denote the same bag, fetch1 may yield either [𝑎] or [𝑏]. Bag semantics denotes a multiplicity-based query meaning. Typed aggregate semantics distinguishes concrete, NULL- and type-aware aggregation from restricted encodings or uninterpreted aggregate operators. Ordered relational semantics and order-aware optimization. Ordered relational models long predate modern SQL equivalence verifiers. Coburn and Weddell propose an ordered-list model for graphbased data in which a query denotes a nonempty set of tuple lists. Declarative operators can thus admit alternative legal orders, while lower-level access plans select more specific results [10]. Their objective is wide-spectrum plan refinement: an implementation is valid when its possible results are contained in those of the request. Slivinskas, Jensen, and Snodgrass give each expression a listvalued semantics and classify plan equivalence as list, multiset, or set equality. The required equivalence propagates inward from the query root. Without an outermost ORDER BY, the root requires multiset equality; a sort clears OrderRequired for its child, permitting multiset-preserving rules below it. For ORDER BY 𝐴, two results need only have the same multiset and the same sequence of projected 𝐴-values, thereby identifying permutations within ties [21]. This treatment does not extend directly to top-𝑘 operators such as FETCH: a prefix can distinguish tied permutations, requiring either full list equality or an explicit semantics of alternative lists rather than multiset equality. Chinaei reduces an ordered-bag SQL algebra to set algebra by adding interpreted multiplicity and order-priority columns [6]. This enables reuse of set-based containment techniques. An augmented relation, however, records one computed priority assignment, encoding order within ordinary set rows. Similarly, Amarilli et al. represent order-incomplete data as partially ordered relations whose linear extensions are possible output lists, but each po-relation fixes one underlying bag [1]. It therefore cannot represent grouping or tie-sensitive top-𝑘 when possible worlds induce different result bags. Mechanized bag semantics over lists imposes a known proof cost. Bag equality becomes equality modulo permutation, while set equality also requires duplicate elimination. Proofs therefore

Answer to RQ2. The existing unbounded verifiers are much faster on the cases they solve. Logos trades that speed for broader, proof-producing coverage; its principal bottleneck is LLM-guided proof construction: 87.6% of agent-round time lies outside Rocq diagnostic compilation. Reusable lemmas and bagto-list bridges already reduce repeated reasoning, while deterministic fast paths, better retrieval, and incremental diagnostics provide the main opportunities for narrowing the remaining gap.

5.4

RELATED WORK

Threats to Validity

Our benchmark families span several SQL dialects. Although the tool-specific materialization adapters use SQLGlot to normalize each case, the transpiler cannot guarantee semantic preservation across dialects. A small number of cases may therefore acquire semantic differences during translation, leading to false positive or false negative benchmark outcomes. We mitigate this risk by designing Logos around a broad common SQL language and, where the SQL standard leaves behavior unspecified, adopting PostgreSQL’s documented execution behavior. This choice improves consistency 11

Table 3: Comparison of order-aware query models and SQL equivalence systems. System or framework

Unbounded checking

Order-aware semantics and optimization Coburn and Weddell [10] Slivinskas et al. [20, 21] Chinaei [6] Amarilli et al. [1] SQL query-pair verification Cosette/HoTTSQL [8, 9] SQLSolver [12] QED [26] VeriEQL [13] Logos supported;

partially supported;

Alternative ordered lists

Compositional top-𝑘

— — — —

Bag semantics

Typed aggregate semantics

— —

unsupported; — outside scope. Ratings concern each published fragment; Logos’s ratings concern its stated typed SQL fragment, rather than all PostgreSQL or ISO SQL.

proceed by list induction while carrying permutation and duplicateelimination invariants through operators; HoTTSQL reports that this bookkeeping makes even simple rewrite proofs lengthy and scales poorly to optimizer rules [9]. Logos instead retains all legal ordered lists, including alternatives with different bags, while recovering multiplicity-level reasoning through a closure-based lifting from bag equivalence to ordered-list equivalence at bag-closed boundaries.

syntax rather than a semantics for arbitrarily nested order-sensitive queries. VeriEQL instead gives bounded SMT verification over finite tuple lists and uses bag equivalence for unordered outputs. Its five core aggregates have concrete encodings over an integer/Boolean/NULL value model. It encodes LIMIT, OFFSET, and FETCH, including in combination with ORDER BY, but observes list order only for an outermost ORDER BY. It therefore does not provide a compositional semantics of legal result orders in which every tie-induced top-𝑘 result remains visible to enclosing queries [13]. Earlier symbolic systems include SPES, which targets bag semantics, and EQUITAS, which targets set semantics; both use SMTbacked symbolic representations to reason about concrete predicates, but neither provides semantics for order-sensitive queries [29, 30]. The U-semiring decision procedure (UDP) supplies unbounded bag reasoning, while abstracting scalar and aggregate semantics and omitting order-sensitive operators [7]. Testing and fuzzing tools such as NoREC expose optimizer bugs by constructing differential or metamorphic test oracles [19]. Such techniques are effective at finding concrete counterexamples, but they do not provide universally quantified rewrite proofs.

SQL query equivalence, rewrite verification, and optimizer testing. SQL query equivalence has been studied through proof assistants, algebraic decision procedures, and solver-backed verification. Recent industrial evidence nevertheless shows that real-world rewrite verification remains challenging [16]. One line of work uses mechanized semantics and proof-oriented SQL provers. Cosette and HoTTSQL are closely related systems from the same line of work: Cosette emphasizes an automated prover pipeline that combines bounded counterexample search with Coq-checked reasoning over K-relations and UniNomials for bag-semantics rewrites, while HoTTSQL develops the HoTT-based denotational semantics in more depth [7–9]. Their reasoning is primarily about relational structure and multiplicities; scalar predicates and expressions are largely treated as uninterpreted functions. The semantics also does not give compositional meaning to alternative result orders, leaving order-sensitive operators outside the main model. In addition, the systems do not model the full behavior of industrial SQL dialects, including null-sensitive three-valued logic and type coercions. A second line develops algebraic or solver-backed decision procedures. QED combines semiring normalization with first-order reasoning and gives unbounded guarantees for its supported bagsemantics fragment. It represents operators such as LIMIT abstractly and can pass through matching instances by recursive congruence, but does not model their order-sensitive behavior; casts remain abstract, and aggregate functions are treated as uninterpreted higherorder operators [26]. SQLSolver reduces U-expressions to linear integer arithmetic and adds a divide-and-conquer ordered-bag procedure. It gives concrete encodings for core aggregates, but its value reasoning is restricted to the supported linear-integer-arithmetic fragment. It simplifies ordering operators, matches two ORDER BY nodes only when their keys and following LIMIT/OFFSET structures agree, and recursively invokes its bag verifier below them [12]. Consequently, its sound ordered reasoning is tied to compatible query

LLM-assisted theorem proving. Recent theorem-proving agents use language models to retrieve relevant facts, predict proof steps, or coordinate automated provers. LeanDojo studies retrieval-based theorem proving over Lean libraries [28], and Thor integrates language models with automated theorem provers for formal proof search [14]. These advances are orthogonal to our SQL-specific semantic development, but inform Logos’s use of language models to guide proof search while leaving certificate acceptance to Rocq.

7

CONCLUSION

We presented Logos, a proof-producing verifier for SQL rewrites over arbitrary finite databases. FormalSQL gives a mechanized, compositional semantics for possible ordered lists and observable failures, while its closure-based bag-to-list lifting theorem enables local multiplicity reasoning without erasing order. Logos combines typed lowering with LLM-guided Rocq proof construction. Across 389 query pairs, it solves 338 (86.9%), compared with 249 (64.0%) for the strongest baseline. These results demonstrate the practical value of combining ordered-list semantics with local bag reasoning. 12

REFERENCES

[19] Manuel Rigger and Zhendong Su. 2020. Detecting Optimization Bugs in Database Engines via Non-Optimizing Reference Engine Construction. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Association for Computing Machinery, 1140–1152. https://doi.org/10.1145/3368089.3409710 [20] Giedrius Slivinskas and Christian S. Jensen. 2001. Enhancing an Extensible Query Optimizer with Support for Multiple Equivalence Types. In Advances in Databases and Information Systems (Lecture Notes in Computer Science), Vol. 2151. Springer, 55–69. https://doi.org/10.1007/3-540-44803-9_6 [21] Giedrius Slivinskas, Christian S. Jensen, and Richard T. Snodgrass. 2001. A Foundation for Conventional and Temporal Query Optimization Addressing Duplicates and Ordering. IEEE Transactions on Knowledge and Data Engineering 13, 1 (2001), 21–49. https://doi.org/10.1109/69.908979 [22] Zhaoyan Sun, Xuanhe Zhou, Guoliang Li, Xiang Yu, Jianhua Feng, and Yong Zhang. 2025. R-Bot: An LLM-Based Query Rewrite System. Proceedings of the VLDB Endowment 18, 12 (2025), 5031–5044. https://doi.org/10.14778/3750601. 3750625 [23] Emina Torlak and Rastislav Bodík. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, 530–541. https://doi.org/10.1145/2594291.2594340 [24] Transaction Processing Performance Council. 2017. TPC Benchmark H (Decision Support): Standard Specification, Revision 2.17.3. https://www.tpc.org/tpc_ documents_current_versions/pdf/TPC-H_v2.17.3.pdf Accessed: 2026-07-31. [25] Transaction Processing Performance Council. 2024. TPC Benchmark DS: Standard Specification, Version 4.0.0. https://www.tpc.org/TPC_Documents_Current_ Versions/pdf/TPC-DS_v4.0.0.pdf Accessed: 2026-07-31. [26] Shuxian Wang, Sicheng Pan, and Alvin Cheung. 2024. QED: A Powerful Query Equivalence Decider for SQL. Proceedings of the VLDB Endowment 17, 11 (2024), 3602–3614. https://doi.org/10.14778/3681954.3682024 [27] Zhaoguo Wang, Zhou Zhou, Yicun Yang, Haoran Ding, Gansen Hu, Ding Ding, Chuzhe Tang, Haibo Chen, and Jinyang Li. 2022. WeTune: Automatic Discovery and Verification of Query Rewrite Rules. In Proceedings of the 2022 International Conference on Management of Data. Association for Computing Machinery, 94– 107. https://doi.org/10.1145/3514221.3526125 [28] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems 36. 21573–21612. https://doi.org/10.52202/ 075280-0944 [29] Qi Zhou, Joy Arulraj, Shamkant B. Navathe, William Harris, and Jinpeng Wu. 2022. SPES: A Symbolic Approach to Proving Query Equivalence Under Bag Semantics. In 2022 IEEE 38th International Conference on Data Engineering. IEEE, 2735–2748. https://doi.org/10.1109/ICDE53745.2022.00250 [30] Qi Zhou, Joy Arulraj, Shamkant B. Navathe, William Harris, and Dong Xu. 2019. Automated Verification of Query Equivalence Using Satisfiability Modulo Theories. Proceedings of the VLDB Endowment 12, 11 (2019), 1276–1288. https: //doi.org/10.14778/3342263.3342267

[1] Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart. 2017. Possible and Certain Answers for Queries over Order-Incomplete Data. In 24th International Symposium on Temporal Representation and Reasoning (Leibniz International Proceedings in Informatics), Vol. 90. Schloss Dagstuhl–LeibnizZentrum für Informatik, 4:1–4:19. https://doi.org/10.4230/LIPIcs.TIME.2017.4 [2] Qiushi Bai, Sadeem Alsudais, and Chen Li. 2023. QueryBooster: Improving SQL Performance Using Middleware Services for Human-Centered Query Rewriting. Proceedings of the VLDB Endowment 16, 11 (2023), 2911–2924. https://doi.org/10. 14778/3611479.3611497 [3] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), Vol. 13243. Springer, 415–442. https://doi. org/10.1007/978-3-030-99524-9_24 [4] Edmon Begoli, Jesús Camacho-Rodríguez, Julian Hyde, Michael J. Mior, and Daniel Lemire. 2018. Apache Calcite: A Foundational Framework for Optimized Query Processing Over Heterogeneous Data Sources. In Proceedings of the 2018 International Conference on Management of Data. Association for Computing Machinery, 221–230. https://doi.org/10.1145/3183713.3190662 [5] Véronique Benzaken and Évelyne 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. Association for Computing Machinery, 249–261. https://doi.org/10.1145/3293880.3294107 [6] Hamid R. Chinaei. 2007. An Ordered Bag Semantics for SQL. Master’s thesis. University of Waterloo. https://hdl.handle.net/10012/3062 [7] Shumo Chu, Brendan Murphy, Jared Roesch, Alvin Cheung, and Dan Suciu. 2018. Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries. Proceedings of the VLDB Endowment 11, 11 (2018), 1482–1495. https://doi.org/10.14778/3236187.3236200 [8] Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017. Cosette: An Automated Prover for SQL. In 8th Biennial Conference on Innovative Data Systems Research. www.cidrdb.org. https://www.cidrdb.org/cidr2017/ papers/p51-chu-cidr17.pdf [9] Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. 2017. HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, 510–524. https://doi.org/10.1145/3062341. 3062348 [10] Neil Coburn and Grant E. Weddell. 1993. A Logic for Rule-Based Query Optimization in Graph-Based Data Models. In Deductive and Object-Oriented Databases (Lecture Notes in Computer Science), Vol. 760. Springer, 120–145. https://doi.org/10.1007/3-540-57530-8_8 [11] Bailu Ding, Surajit Chaudhuri, Johannes Gehrke, and Vivek Narasayya. 2021. DSB: A Decision Support Benchmark for Workload-Driven and Traditional Database Systems. Proceedings of the VLDB Endowment 14, 13 (2021), 3376–3388. https://doi.org/10.14778/3484224.3484234 [12] Haoran Ding, Zhaoguo Wang, Yicun Yang, Dexin Zhang, Zhenglin Xu, Haibo Chen, Ruzica Piskac, and Jinyang Li. 2023. Proving Query Equivalence Using Linear Integer Arithmetic. Proceedings of the ACM on Management of Data 1, 4, Article 227 (2023), 26 pages. https://doi.org/10.1145/3626768 [13] Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang. 2024. VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints. Proceedings of the ACM on Programming Languages 8, OOPSLA1 (2024), 1071– 1099. https://doi.org/10.1145/3649849 [14] Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems 35. 8360–8373. https://doi.org/10.52202/068431-0608 [15] Toby Mao and Contributors. 2026. SQLGlot: Python SQL Parser and Transpiler, Version 30.11.0. https://pypi.org/project/sqlglot/30.11.0/ Accessed: 2026-07-07. [16] Vivek R. Narasayya and Surajit Chaudhuri. 2026. Leveraging Query Optimizers to Verify the Soundness of LLM-Based Query Rewrites for Real-World Workloads, and More!. In 16th Conference on Innovative Data Systems Research. www.cidrdb.org, Chaminade, CA, USA, 12. https://www.cidrdb.org/cidr2026/ papers/p33-narasayya.pdf [17] Hamid Pirahesh, Joseph M. Hellerstein, and Waqar Hasan. 1992. Extensible/Rule Based Query Rewrite Optimization in Starburst. In Proceedings of the 1992 ACM SIGMOD International Conference on Management of Data. Association for Computing Machinery, 39–48. https://doi.org/10.1145/130283.130294 [18] PostgreSQL Global Development Group. 2026. PostgreSQL 18.4: SELECT. https: //www.postgresql.org/docs/18/sql-select.html Accessed: 2026-07-28.

13

Related documents

• Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance#616853
• Logos: Certified Order-Sensitive SQL Rewrites with Mechanized Semantics and LLM Guidance#616353
• LASER: A Data-Centric Method for Low-Cost and Efficient SQL Rewriting based on SQL-GRPO#2752
• DBRepro: Automated Database Synthesis via a Hybrid Constraint-Solving Approach for Reproducing Slow Queries#618639
• SQL-RewriteBench: A Correctness-Gated, Full-Denominator Benchmark for Statement-Level SQL Rewriting [Experiment,Analysis &amp; Benchmark]#361536