[zvonimir-dd]

What type of PR is this?

• Soundness fix (a prover could claim equivalence for a pair that is not equivalent)
• Coverage (the frontend now lowers something it used to refuse)
• Bug fix
• Feature / refactor
• Documentation

Description

Why

The QED prover is still the only prover that decides a share of the pairs the portfolio decides, and it is no longer maintained. sqleq-solver receives the same IR bytes (src/lib.rs emit()), so every pair QED decides and sqleq-solver does not is a gap in sqleq-solver. Most of those pairs stop at one of four refusals: a row slice (unsupported-sort, any LIMIT/OFFSET), a FROM-less query (rel-not-object), a VALUES cell that computes its value (values-nonliteral), and COUNT(DISTINCT) (aggregate-distinct-unsupported). This PR reads those where the IR settles them. The frontend is unchanged.

card: relations that return at most one row

A LIMIT 1 over a query that cannot return two rows keeps every row it gets:

create table "t" ("k" INTEGER PRIMARY KEY, "a" INTEGER);
SELECT "a" FROM "t" WHERE "k" = $1;
SELECT "a" FROM "t" WHERE "k" = $1 LIMIT 1;

card::shape decides that on the IR, for databases that keep the schemas' keys (the assumption ic and Normalizer::with_ics already make):

• Source of a bound. A NOT NULL unique key (Schema::enforced_keys, now shared with ic) whose columns a conjunct of a WHERE or of an inner join's ON holds to one value bounds its table to one row. "One value" means a literal, a parameter, one of the frontend's casts or conversions of one, a column of an enclosing query, or a column equated with any of these. It only counts where = on the column's type is identity.
• Propagation. The bound carries through inner joins (u JOIN t ON t.k = u.t_k WHERE u.id = $1), projections, deduplication, and a group whose keys are all held.
• What holds nothing. An OR, an order comparison, a function call or a subquery holds nothing, so the analysis can miss a bound but never invent one.

On top of it, card::slice:

• reads a literal LIMIT of one or more over such a source as the identity;
• reads LIMIT 0 as no rows and OFFSET 0 as every row;
• drops a literal LIMIT ≥ 1 (with no OFFSET) under EXISTS.

LIMIT $n stays refused, since $n may be bound to 0.

opaque: the same slice of equal sources

Before translation, abstract_opaque collects, on each side, the nodes translation would refuse:

• a slice card cannot read;
• a GROUP BY with an aggregate translation does not model, which in practice means the frontend's DISTINCT_ON#… carrier.

Nodes are matched one to one across the sides. Two nodes match when they have the same sort keys and counts (or the same group keys and calls), and their sources are identical or proved equal by a recursive prove_at (depth ≤ 3, which also covers nested slices). Each matched pair is replaced on both sides by a scan of one fresh table. A node that reads a column of an enclosing query is left alone. If any refused node has no partner, translation refuses the pair as before.

The reading this rests on is the one QED's opaque limit, strip_identical_pagination and lower::apply_pagination already take: a slice is a function of its source's bag. Nothing beyond it is added.

• Order keys. The frontend's sort_sandwich puts every order key into the slice's source, so comparing sources as bags covers the keys.
• Mirrored guard. A slice over an ORDER BY that translation erases is not replaced unless its own keys cover every column, because that order decides the ties. The frontend already refuses that shape (refuse_slice_over_dropped_order); the guard is kept here too so the claim does not rest on the frontend alone. The second counterexample in strip_identical_pagination's doc is a test.

Small refusals

• The bare "singleton" a FROM-less query is lowered over is read as one empty row.
• A VALUES cell may compute its value (a parameter, a cast). It is read at its column's type, and refused if its own type differs. A subquery cell is still refused.
• COUNT(DISTINCT x) is SQLSolver's nested existential sum, refused where = on x is not identity, as deduplication is.
• MAX/MIN(DISTINCT) are MAX/MIN. SUM/AVG(DISTINCT) stay refused.

IR

Relation::Sort now keeps its keys as keys: Vec<SortKey>, the same definition #209 (cvc5 axis) adds, so the two merge without a real conflict.

Pins that moved

All four are expect sqleq-solver lines, re-blessed. None is on a pair whose truth is not-equivalent and now proved. Every ordering/ pin (a non-equivalent slice or DISTINCT ON that no prover may prove) still holds.

• pagination/nested_limit_ties_under_filter.sql (equivalent): unsupported → proved. Both sides take ORDER BY "g" LIMIT 1 of sources that are equal bags, because "id" is a key so DISTINCT keeps every row. This is the reading the pair's own argument: gives.
• types/union_null_branch.sql (equivalent): unsupported → proved. The FROM-less SELECT NULL branch arrives as a computed VALUES cell.
• types/values_integer_beside_numeric.sql (equivalent): unsupported → no-proof. It is translated now, but 1 and 1.0 are two values to this prover, so it is a conservative miss.
• dml/insert_values_stores_numeric_literal_as_text.sql (not equivalent): unsupported → no-proof. Translated now, and not proved.

Left out

The largest remaining group of pairs only QED decides needs predicate and value equivalence under bag semantics: the set solver only runs where every sum is under a squash. That, correlated subqueries (correlated), and dedup over unvouched VARBINARY are the next steps.

How it was tested

• cargo test -p sqleq-solver: unit tests including card's, plus the new tests/limit_slices.rs, which pairs each rule with the negative controls it must refuse:
  • a non-key column, half a composite key, a key over a nullable column;
  • <=, OR, = on REAL;
  • LIMIT $n, OFFSET 1;
  • ASC vs DESC, another order column, LIMIT $3 vs LIMIT $4;
  • a correlated slice source;
  • two slices on one side against one on the other;
  • both counterexamples in strip_identical_pagination's doc;
  • COUNT(DISTINCT) on a nullable column.
• card also has a property test: relations it calls "at most one row" are translated and evaluated on random databases that keep the keys, and none ever has two rows. The test fails if no relation ever had two rows, so it cannot pass vacuously.
• cargo clippy -p sqleq-solver --all-targets -- -D warnings, and cargo doc --no-deps -p sqleq-solver with -D warnings, with and without private items.
• cargo test -p sqleq-check --test real_solver against the built binary.
• sqleq-check --expect pinned --axes sqleq-solver tests/pairs examples/*.sql: 471/471 after the bless above.

Corpus cross-check (CONTRIBUTING rule 2). The corpus is private, so these counts are for scale only.

The release binary was run over the IR of the latest all-axes run of the benchmark corpus, which was lowered at the same frontend revision as main, and joined row by row against that run's verdicts:

• No new proof on any of the 945 pairs sqleq-fuzz refutes, and no proof lost.
• 112 new proofs. 27 of them are on pairs nothing decided before (QED timed out or gave up). 85 of them are among the 213 pairs the portfolio decided by QED alone.
• Of the 112, sqleq-fuzz found no counterexample on 105 and skipped 7 by construction. Six are EXISTS (SELECT $1 …) against EXISTS (SELECT 1 …), a parameter on one side only. One is a slice whose ties make it nondeterministic.
• This is a join against the stored fuzz axis of that run, not a fresh sqleq-check --portfolio run.
• Solver CPU over the run roughly doubled. Slice pairs that stay refused now first attempt a sub-proof of their sources. The slowest pair stayed under the 60 s cap.

Checklist

• A construct the frontend cannot lower faithfully is refused, not approximated. (No frontend change; the solver still refuses every slice and aggregate it cannot read.)
• If this grows the provable set, the same pairs were run through sqleq-check --portfolio
  (the provers and sqleq-fuzz at once; a proof with a counterexample is an alarm), and none
  of the newly proven pairs has a counterexample. (A row-by-row join against the corpus run's stored sqleq-fuzz verdicts, as described above, not a fresh --portfolio run.)
• If this fixes a defect that can be stated as a pair, the pair is pinned under tests/pairs/
  and was seen failing on a build from before the fix. (Not a defect fix.)
• Every pin under tests/pairs/ that moved is explained in the description.
• If dependencies changed, LICENSE-3rdparty.csv was regenerated with
  sh tools/update_license_3rdparty.sh. (No dependency change.)

AI code assistants

Assisted-by: Claude Code (Claude Opus 5.5)

🤖 Generated with Claude Code

[bvolpato-dd]

Approved under Bruno Volpato's standing instruction for datadog-labs/sqleq. I checked the pull request metadata only; I did not review the diff or run the tests.

Stamped by nightwatcher, a review agent that acts for Bruno Volpato.