diff --git a/docs/SQLSOLVER.md b/docs/SQLSOLVER.md index d73a99f..177b54e 100644 --- a/docs/SQLSOLVER.md +++ b/docs/SQLSOLVER.md @@ -150,6 +150,17 @@ What it rewrites, in the order the ladder runs it: so the only order fact it is given is that `a <= b` is `NOT (b < a)`. That holds wherever it is used: every order comparison sits under its operands' not-null guard, and the non-`NULL` values of one type are totally ordered. +* **Row slices**, where the IR settles them, not through the fork's `OrderbySupport`. A literal + `LIMIT` of one or more over a query that cannot return two rows keeps every row (`card`): a table + whose NOT NULL unique key a conjunct of the `WHERE` or of an inner join's `ON` holds to one value + (a literal, a parameter, a column equated with one) contributes one row at most, and so does a + group whose keys are all held. `LIMIT 0` keeps none and `OFFSET 0` all. Before translation, the + same slice — same sort keys and counts — of two sources proved to return the same bag is replaced + on both sides by one fresh table (`opaque`), and so is the same opaque aggregate (the frontend's + `DISTINCT ON` carrier) over equal sources. That reads a slice as a function of its source's bag, + the reading QED's opaque `limit` and the frontend's `strip_identical_pagination` already take; a + slice over an `ORDER BY` translation erases is not replaced unless its own keys cover every + column, since that order decides the ties. Not rewritten: the **LIA\* rung**. What it adds over the rungs above is mostly reasoning across summands (a disjoint `OR` against a `UNION ALL`, a count compared with a constant), and several of @@ -158,7 +169,8 @@ one: `ts >= k AND ts < k + 1` is not `ts = k` for a timestamp, and `'infinity':: `infinity`, so even `d + 1 > d` fails. The IR names every temporal operation and conversion (`q_arith_add_date_integer`, `q_conv_date_timestamp` and the like), which is what such a rung would have to interpret, infinities included. **`LIMIT`/`OFFSET`** (`OrderbySupport`) is not rewritten -either; a bare `ORDER BY` is erased, which is sound under the bag semantics `sqleq` decides. +either: any slice the rule above does not settle is refused (`unsupported-sort`). A bare `ORDER BY` +is erased, which is sound under the bag semantics `sqleq` decides. ### Where it deliberately differs from the fork @@ -201,8 +213,9 @@ Each difference is there for soundness: So the two disagree in both directions: some pairs the fork proves `sqleq-solver` does not (the LIA\* rung, pairs that rely on a parameter never being `NULL`, and the false proofs listed at the -top), and some `sqleq-solver` proves the fork does not (rewrites the fork does not normalize, and -pairs where it runs out of time). Either way an `EQ` is a claim to be checked against `sqleq-fuzz`. +top), and some `sqleq-solver` proves the fork does not (rewrites the fork does not normalize, pairs +where it runs out of time, and plans the bridge refuses: a `FROM`-less query, lowered over the bare +`"singleton"`, and a `VALUES` cell that computes its value). Either way an `EQ` is a claim to be checked against `sqleq-fuzz`. ### How it is checked diff --git a/sqleq-solver/src/card.rs b/sqleq-solver/src/card.rs new file mode 100644 index 0000000..2b0336f --- /dev/null +++ b/sqleq-solver/src/card.rs @@ -0,0 +1,562 @@ +// Unless explicitly stated otherwise all files in this repository are licensed under the +// Apache License Version 2.0. +// This product includes software developed at Datadog (https://www.datadoghq.com/). +// Copyright 2026-Present Datadog, Inc. + +//! Which relations return at most one row, read off the IR, and what that makes of a row slice. +//! +//! A `LIMIT 1` over a query that cannot return two rows keeps every row it gets, so the slice is +//! the identity there: `SELECT b FROM t WHERE k = $1` and the same query with `LIMIT 1` are one +//! query when `k` is a key of `t`. [`slice()`] says when a slice can be read that way, and [`shape`] +//! is the analysis it asks. +//! +//! The claims hold on every database that satisfies the schemas' integrity constraints, which is +//! what the constraint rewrites (`ic`, `normalize::Normalizer::with_ics`) already assume. A unique +//! key whose columns are all NOT NULL ([`Schema::enforced_keys`]) is the only source of a bound: +//! no two rows of its table agree on it. A conjunct of a `WHERE` or of an inner join's `ON` that +//! equates a column with a value constant across the rows (a literal, a parameter, a cast of one, +//! a column of an enclosing query) holds that column to one value in every row the conjunct +//! passes, provided `=` on its type is identity of the values; two columns equated that way are +//! one value. A table whose key is held that way contributes at most one row. Nothing else is +//! read: an `OR`, an order comparison, a function call or a subquery holds nothing, so the +//! analysis can only miss a bound, never invent one. + +use std::collections::BTreeSet; + +use crate::ir::{Expr, JoinKind, Relation, Schema, Type}; + +/// What a slice does to its source: nothing ([`Slice::Identity`]), remove every row +/// ([`Slice::Empty`]), or something that depends on the rows and their order ([`Slice::Opaque`]). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Slice { + Identity, + Empty, + Opaque, +} + +/// The effect of `ORDER BY … LIMIT limit OFFSET offset` over `source`, which sits at level `base`. +/// Only literal counts are read: a parameter may be bound to 0, or to more rows than there are. +pub fn slice(source: &Relation, offset: Option<&Expr>, limit: Option<&Expr>, base: usize, schemas: &[Schema]) -> Slice { + let limit = limit.map(literal_count); + if limit == Some(Some(0)) { + return Slice::Empty; + } + if offset.is_some_and(|o| literal_count(o) != Some(0)) { + return Slice::Opaque; + } + match limit { + None => Slice::Identity, + Some(Some(n)) if n >= 1 && shape(source, base, schemas).max_one() => Slice::Identity, + Some(_) => Slice::Opaque, + } +} + +/// A literal row count, as `LIMIT`/`OFFSET` carry one. `None` for anything else, `LIMIT NULL` and a +/// parameter included, and for a negative count, which Postgres rejects. +fn literal_count(e: &Expr) -> Option { + match e { + Expr::Literal { value, ty: Type::Integer } => value.parse::().ok().filter(|n| *n >= 0), + _ => None, + } +} + +/// `query` with the slices removed that cannot make it empty when it is not: a literal `LIMIT` of +/// one or more with no `OFFSET`, at its top or under a projection or deduplication, which keep +/// emptiness as well. `None` when there is none. For an `EXISTS`, which reads only whether its +/// query returns a row. +pub fn strip_nonempty_slices(query: &Relation) -> Option { + match query { + Relation::Sort { source, offset, limit, .. } + if offset.as_ref().is_none_or(|o| literal_count(o) == Some(0)) + && limit.as_ref().and_then(literal_count).is_some_and(|n| n >= 1) => + { + Some(strip_nonempty_slices(source).unwrap_or_else(|| (**source).clone())) + } + Relation::Project { source, target } => { + strip_nonempty_slices(source).map(|s| Relation::Project { source: Box::new(s), target: target.clone() }) + } + Relation::Distinct(source) => strip_nonempty_slices(source).map(|s| Relation::Distinct(Box::new(s))), + _ => None, + } +} + +/// What [`shape`] knows about a relation's rows. Positions are 0-based in its output. +#[derive(Debug, Clone)] +pub struct Shape { + /// The relation's rows are a sub-bag of the product of these: one per scanned input of an inner + /// join tree, one for any other relation. + comps: Vec, + /// Positions that hold one value in every row. + consts: BTreeSet, + /// Pairs of positions that hold the same value in every row, kept while the rows are still a + /// product of `comps` so that a filter above an inner join can use the join's equalities. + equal: Vec<(usize, usize)>, + /// Per position: whether SQL's `=` on it is identity of the values, so that equating it with a + /// constant holds it to one value. Its length is the relation's width. + ident: Vec, +} + +#[derive(Debug, Clone)] +struct Comp { + /// The positions it supplies. + cols: BTreeSet, + /// Position sets no two of its rows agree on. + keys: Vec>, + /// It contributes at most one row. + max_one: bool, +} + +/// How many key combinations [`Shape::keys`] builds before it stops; a bound, not a tuning knob. +const MAX_KEYS: usize = 8; + +impl Shape { + /// The relation returns at most one row. + pub fn max_one(&self) -> bool { + self.comps.iter().all(|c| c.max_one) + } + + /// Position sets no two rows of the relation agree on: one key of every component that may + /// contribute several rows. + pub fn keys(&self) -> Vec> { + let mut acc = vec![BTreeSet::new()]; + for c in self.comps.iter().filter(|c| !c.max_one) { + let mut next = Vec::new(); + for a in &acc { + for k in &c.keys { + if next.len() < MAX_KEYS { + next.push(a.union(k).copied().collect()); + } + } + } + acc = next; + } + acc + } + + fn width(&self) -> usize { + self.ident.len() + } + + /// One component over all positions, for a relation whose rows are no longer a product. + fn collapsed(width: usize, keys: Vec>, max_one: bool, consts: BTreeSet, ident: Vec) -> Shape { + let comp = Comp { cols: (0..width).collect(), keys, max_one }; + Shape { comps: vec![comp], consts, equal: Vec::new(), ident }.settled() + } + + /// Nothing known: one component, no key. + fn unknown(ident: Vec) -> Shape { + Shape::collapsed(ident.len(), Vec::new(), false, BTreeSet::new(), ident) + } + + /// A relation with at most one row holds one value in each position. + fn settled(mut self) -> Shape { + if self.max_one() { + self.consts = (0..self.width()).collect(); + } + self + } + + /// `self` followed by `right`, as an inner join's input rows. + fn concat(mut self, right: Shape) -> Shape { + let w = self.width(); + let shift = |s: &BTreeSet| s.iter().map(|p| p + w).collect::>(); + self.comps.extend(right.comps.into_iter().map(|c| Comp { + cols: shift(&c.cols), + keys: c.keys.iter().map(shift).collect(), + max_one: c.max_one, + })); + self.consts.extend(right.consts.iter().map(|p| p + w)); + self.equal.extend(right.equal.iter().map(|(p, q)| (p + w, q + w))); + self.ident.extend(right.ident); + self + } + + /// Restrict to the rows `condition` passes, at level `base`: hold each column its conjuncts + /// equate with a constant, merge the columns they equate with each other, and close over the + /// components whose key that holds. + fn filtered(mut self, condition: &Expr, base: usize) -> Shape { + let w = self.width(); + let mut class: Vec = (0..w).collect(); + for &(p, q) in &self.equal { + union(&mut class, p, q); + } + let mut pinned = self.consts.clone(); + for c in conjuncts(condition) { + let Expr::Call { operator, operand, .. } = c else { continue }; + let [a, b] = operand.as_slice() else { continue }; + if operator != "=" || a.ty() != b.ty() { + continue; + } + // The column's own reading of `=` decides, since Postgres reads the other operand, of + // the same IR type, at the column's type. + match (self.local(a, base), self.local(b, base)) { + (Some(p), Some(q)) if self.ident[p] && self.ident[q] => { + union(&mut class, p, q); + self.equal.push((p, q)); + } + (Some(p), None) if self.ident[p] && row_constant(b, base) => { + pinned.insert(p); + } + (None, Some(q)) if self.ident[q] && row_constant(a, base) => { + pinned.insert(q); + } + _ => {} + } + } + loop { + let held: BTreeSet = pinned.iter().map(|p| find(&mut class, *p)).collect(); + pinned.extend((0..w).filter(|p| held.contains(&find(&mut class, *p)))); + let mut changed = false; + for comp in self.comps.iter_mut().filter(|c| !c.max_one) { + if comp.keys.iter().any(|k| k.is_subset(&pinned)) { + comp.max_one = true; + pinned.extend(comp.cols.iter().copied()); + changed = true; + } + } + if !changed { + break; + } + } + self.consts = pinned; + self.settled() + } + + /// The position a bare column reference at level `base` names in this relation, if any. + fn local(&self, e: &Expr, base: usize) -> Option { + match e { + Expr::Column { index, .. } => (*index as usize).checked_sub(base).filter(|p| *p < self.width()), + _ => None, + } + } +} + +/// `e`'s top-level `AND` operands, flattened; `e` itself when it is not an `AND`. +fn conjuncts(e: &Expr) -> Vec<&Expr> { + match e { + Expr::Call { operator, operand, .. } if operator == "AND" => operand.iter().flat_map(conjuncts).collect(), + other => vec![other], + } +} + +/// A value that is the same in every row at level `base`: a literal, a parameter, a column of an +/// enclosing query, or one of the frontend's casts or conversions of such a value. No other +/// function, so a volatile one (`random()`, `clock_timestamp()`) is never taken for a constant. +fn row_constant(e: &Expr, base: usize) -> bool { + match e { + Expr::Literal { .. } => true, + Expr::Column { index, .. } => (*index as usize) < base, + Expr::Cast { operand, .. } => row_constant(operand, base), + Expr::Call { operator, operand, .. } => { + let numbered = |prefix: &str| { + operator.strip_prefix(prefix).is_some_and(|k| !k.is_empty() && k.bytes().all(|b| b.is_ascii_digit())) + }; + (numbered("QP") || numbered("QCAST") || operator.starts_with("q_cast_") || operator.starts_with("q_conv_")) + && operand.iter().all(|o| row_constant(o, base)) + } + Expr::Subquery { .. } => false, + } +} + +fn find(class: &mut [usize], p: usize) -> usize { + let mut root = p; + while class[root] != root { + root = class[root]; + } + class[p] = root; + root +} + +fn union(class: &mut [usize], p: usize, q: usize) { + let (rp, rq) = (find(class, p), find(class, q)); + class[rp] = rq; +} + +/// Whether `=` on a value of IR type `ty` is identity of the values, as `translate::EqType::of` +/// reads it: every type but REAL, INTERVAL and the opaque VARBINARY. +fn identity_type(ty: Type) -> bool { + !matches!(ty, Type::Real | Type::Interval | Type::Varbinary) +} + +/// What is known about `r`'s rows, `r` sitting at level `base` (its own columns are `base..`). +pub fn shape(r: &Relation, base: usize, schemas: &[Schema]) -> Shape { + match r { + Relation::Scan(i) => { + let Some(s) = schemas.get(*i) else { return Shape::unknown(Vec::new()) }; + let vouched = |c: usize| s.opaque_identity.get(c).copied().unwrap_or(false); + let ident = + s.types.iter().enumerate().map(|(c, ty)| identity_type(*ty) || (*ty == Type::Varbinary && vouched(c))).collect(); + let keys = s.enforced_keys().map(|k| k.iter().copied().collect()).collect(); + Shape::collapsed(s.types.len(), keys, false, BTreeSet::new(), ident) + } + Relation::Filter { source, condition } => shape(source, base, schemas).filtered(condition, base), + Relation::Join { left, right, kind, condition } => { + let (l, r) = (shape(left, base, schemas), shape(right, base, schemas)); + match kind { + JoinKind::Inner => l.concat(r).filtered(condition, base), + // Every row of the preserved side appears, matched or padded with NULLs, so the + // other side's columns hold nothing constant; with that side at most one row, + // each preserved row appears once. + JoinKind::Left | JoinKind::Right => { + let (kept, other, offset) = if *kind == JoinKind::Left { (&l, &r, 0) } else { (&r, &l, l.width()) }; + let keys = if other.max_one() { + kept.keys().iter().map(|k| k.iter().map(|p| p + offset).collect()).collect() + } else { + Vec::new() + }; + let consts = kept.consts.iter().map(|p| p + offset).collect(); + let mut ident = l.ident.clone(); + ident.extend(r.ident.iter().copied()); + Shape::collapsed(ident.len(), keys, l.max_one() && r.max_one(), consts, ident) + } + JoinKind::Full => { + let mut ident = l.ident.clone(); + ident.extend(r.ident.iter().copied()); + Shape::unknown(ident) + } + } + } + Relation::Project { source, target } => { + let src = shape(source, base, schemas); + // The position in the source each output column passes through bare, if it does. + let bare: Vec> = target.iter().map(|e| src.local(e, base)).collect(); + let ident = target + .iter() + .zip(&bare) + .map(|(e, b)| match b { + Some(p) => src.ident[*p], + None => identity_type(e.ty()), + }) + .collect(); + let consts = (0..target.len()) + .filter(|j| match bare[*j] { + Some(p) => src.consts.contains(&p), + None => row_constant(&target[*j], base), + }) + .collect(); + let keys = src + .keys() + .into_iter() + .filter_map(|k| k.iter().map(|p| bare.iter().position(|b| *b == Some(*p))).collect::>>()) + .collect(); + Shape::collapsed(target.len(), keys, src.max_one(), consts, ident) + } + Relation::Distinct(source) => { + let src = shape(source, base, schemas); + let mut keys = src.keys(); + keys.push((0..src.width()).collect()); + Shape::collapsed(src.width(), keys, src.max_one(), src.consts.clone(), src.ident.clone()) + } + Relation::Group { source, keys, function } => { + let src = shape(source, base, schemas); + let Some(at) = keys.iter().map(|k| src.local(k, base)).collect::>>() else { + return Shape::unknown(Relation::output_types(r, schemas).iter().map(|t| t.is_some_and(identity_type)).collect()); + }; + let max_one = keys.is_empty() || src.max_one() || at.iter().all(|p| src.consts.contains(p)); + let consts = (0..at.len()).filter(|i| src.consts.contains(&at[*i])).collect(); + let ident = at.iter().map(|p| src.ident[*p]).chain(function.iter().map(|f| identity_type(f.ty))).collect(); + Shape::collapsed(at.len() + function.len(), vec![(0..at.len()).collect()], max_one, consts, ident) + } + // Any slice keeps a sub-bag of its source, which keeps every bound; `LIMIT 1` adds one. + Relation::Sort { source, limit, .. } => { + let src = shape(source, base, schemas); + if limit.as_ref().and_then(literal_count).is_some_and(|n| n <= 1) { + Shape::collapsed(src.width(), src.keys(), true, src.consts.clone(), src.ident.clone()) + } else { + src + } + } + Relation::Values { schema, content } => { + let ident = schema.iter().map(|t| identity_type(*t)).collect(); + Shape::collapsed(schema.len(), Vec::new(), content.len() <= 1, BTreeSet::new(), ident) + } + Relation::Union(_) => Shape::unknown(Relation::output_types(r, schemas).iter().map(|t| t.is_some_and(identity_type)).collect()), + // Deduplicated rows of the left side, or some of them. + Relation::Except(sides) | Relation::Intersect(sides) => { + let src = shape(&sides[0], base, schemas); + let mut keys = src.keys(); + keys.push((0..src.width()).collect()); + Shape::collapsed(src.width(), keys, src.max_one(), src.consts.clone(), src.ident.clone()) + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::ir::Input; + use serde_json::{json, Value}; + + /// `t(k INTEGER NOT NULL, a INTEGER, b INTEGER NOT NULL, c INTEGER NOT NULL)`, keys `(k)` and + /// `(b, c)`; and `u(id INTEGER NOT NULL, t_k INTEGER)`, key `(id)`; and `n(x INTEGER)`, whose key + /// is over a nullable column. + fn schemas() -> Vec { + let input = json!({ "schemas": [ + { "name": "t", "types": ["INTEGER", "INTEGER", "INTEGER", "INTEGER"], "nullable": [false, true, false, false], "key": [[0], [2, 3]] }, + { "name": "u", "types": ["INTEGER", "INTEGER"], "nullable": [false, true], "key": [[0]] }, + { "name": "n", "types": ["INTEGER"], "nullable": [true], "key": [[0]] }, + ], "queries": [{ "scan": 0 }, { "scan": 0 }] }); + Input::parse(&input).unwrap().schemas + } + + fn rel(v: Value) -> Relation { + Relation::parse(&v, 3).unwrap() + } + + fn col(i: u32) -> Value { + json!({ "column": i, "type": "INTEGER" }) + } + + fn param(n: u32) -> Value { + json!({ "operator": format!("QP{n}"), "type": "INTEGER", "operand": [{ "operator": "0", "operand": [], "type": "INTEGER" }] }) + } + + fn eq(a: Value, b: Value) -> Value { + json!({ "operator": "=", "type": "BOOLEAN", "operand": [a, b] }) + } + + fn and(parts: Vec) -> Value { + json!({ "operator": "AND", "type": "BOOLEAN", "operand": parts }) + } + + fn filter(source: Value, cond: Value) -> Value { + json!({ "filter": { "source": source, "condition": cond } }) + } + + fn max_one(v: Value) -> bool { + shape(&rel(v), 0, &schemas()).max_one() + } + + #[test] + fn a_key_held_to_a_parameter_bounds_the_rows() { + assert!(max_one(filter(json!({ "scan": 0 }), eq(col(0), param(1))))); + assert!(max_one(filter(json!({ "scan": 0 }), eq(param(1), col(0))))); + // Through a projection that drops the key. + assert!(max_one(json!({ "project": { "source": filter(json!({ "scan": 0 }), eq(col(0), param(1))), "target": [col(1)] } }))); + // Both columns of the composite key. + assert!(max_one(filter(json!({ "scan": 0 }), and(vec![eq(col(2), param(1)), eq(col(3), param(2))])))); + } + + #[test] + fn anything_short_of_a_held_key_does_not() { + assert!(!max_one(json!({ "scan": 0 }))); + // A column that is no key. + assert!(!max_one(filter(json!({ "scan": 0 }), eq(col(1), param(1))))); + // Half of the composite key. + assert!(!max_one(filter(json!({ "scan": 0 }), eq(col(2), param(1))))); + // A key over a nullable column holds nothing. + assert!(!max_one(filter(json!({ "scan": 2 }), eq(col(0), param(1))))); + // An order comparison, a disjunction, an equality with another column of the same row. + let le = json!({ "operator": "<=", "type": "BOOLEAN", "operand": [col(0), param(1)] }); + assert!(!max_one(filter(json!({ "scan": 0 }), le))); + let or = json!({ "operator": "OR", "type": "BOOLEAN", "operand": [eq(col(0), param(1)), eq(col(0), param(2))] }); + assert!(!max_one(filter(json!({ "scan": 0 }), or))); + assert!(!max_one(filter(json!({ "scan": 0 }), eq(col(0), col(1))))); + // A function of a parameter that is not one of the frontend's casts. + let f = json!({ "operator": "ABS", "type": "INTEGER", "operand": [param(1)] }); + assert!(!max_one(filter(json!({ "scan": 0 }), eq(col(0), f)))); + } + + #[test] + fn a_held_key_carries_through_an_inner_join() { + // `u JOIN t ON t.k = u.t_k WHERE u.id = $1`: `u` is one row, so its `t_k` is one value, + // which holds `t`'s key. `t`'s columns follow `u`'s. + let join = json!({ "join": { "kind": "INNER", "left": { "scan": 1 }, "right": { "scan": 0 }, "condition": eq(col(2), col(1)) } }); + assert!(max_one(filter(join.clone(), eq(col(0), param(1))))); + // Held on `t` alone, `u` may still match many rows. + assert!(!max_one(filter(join, eq(col(2), param(1))))); + } + + #[test] + fn groups_and_slices() { + let grouped = |source: Value, keys: Vec| json!({ "group": { "source": source, "keys": keys, "function": [] } }); + // A scalar aggregate has exactly one row; a group whose keys are all held has at most one. + assert!(max_one(grouped(json!({ "scan": 0 }), vec![]))); + assert!(max_one(grouped(filter(json!({ "scan": 0 }), eq(col(1), param(1))), vec![col(1)]))); + assert!(!max_one(grouped(json!({ "scan": 0 }), vec![col(1)]))); + let page = |source: Value, n: &str| { + json!({ "sort": { "source": source, "collation": [], "limit": { "operator": n, "operand": [], "type": "INTEGER" } } }) + }; + assert!(max_one(page(json!({ "scan": 0 }), "1"))); + assert!(!max_one(page(json!({ "scan": 0 }), "2"))); + } + + /// What the analysis claims holds on concrete databases that keep the keys: each relation is + /// translated and evaluated on random small contents of `t` and `u`, and one it calls at most + /// one row never has two. + #[test] + fn at_most_one_row_holds_on_databases_that_keep_the_keys() { + use crate::eval::{Db, Env}; + use crate::translate::{translate_input, OUT_VAR_ID}; + use crate::uterm::{mk_sum, UConst, UVar}; + use std::collections::{HashMap, HashSet}; + + let lit = |n: &str| json!({ "operator": n, "operand": [], "type": "INTEGER" }); + let scan = |i: u32| json!({ "scan": i }); + let join = json!({ "join": { "kind": "INNER", "left": scan(1), "right": scan(0), "condition": eq(col(2), col(1)) } }); + let grouped = |source: Value| json!({ "group": { "source": source, "keys": [col(1)], "function": [] } }); + let rels = [ + filter(scan(0), eq(col(0), param(1))), + filter(scan(0), eq(col(0), lit("1"))), + filter(scan(0), and(vec![eq(col(2), lit("1")), eq(col(3), param(2))])), + filter(join.clone(), eq(col(0), param(1))), + filter(join.clone(), eq(col(0), lit("2"))), + filter(join.clone(), eq(col(2), lit("1"))), + grouped(filter(scan(0), eq(col(1), lit("1")))), + grouped(scan(0)), + filter(scan(0), eq(col(2), lit("1"))), + scan(1), + ]; + let s = schemas(); + let universe = vec![UConst::Null, UConst::Int(0), UConst::Int(1), UConst::Int(2)]; + let mut seed: u64 = 7; + let mut next = |m: u64| { + seed = seed.wrapping_mul(6364136223846793005).wrapping_add(1442695040888963407); + (seed >> 33) % m + }; + let mut saw_many = false; + for _ in 0..60 { + let (mut t, mut ks, mut bcs) = (Vec::new(), HashSet::new(), HashSet::new()); + for _ in 0..next(6) { + let (k, a, b, c) = (next(3) as i64, universe[next(4) as usize].clone(), next(3) as i64, next(3) as i64); + if ks.insert(k) && bcs.insert((b, c)) { + t.push(vec![UConst::Int(k), a, UConst::Int(b), UConst::Int(c)]); + } + } + let (mut u, mut ids) = (Vec::new(), HashSet::new()); + for _ in 0..next(5) { + let id = next(3) as i64; + if ids.insert(id) { + u.push(vec![UConst::Int(id), universe[next(4) as usize].clone()]); + } + } + let tables: HashMap>> = [("t".into(), t), ("u".into(), u), ("n".into(), vec![])].into(); + for v in &rels { + let r = rel(v.clone()); + let claimed = shape(&r, 0, &s).max_one(); + let [q, _] = translate_input(&Input { schemas: s.clone(), queries: [r.clone(), r] }).unwrap(); + let db = Db::new(tables.clone(), universe.clone(), q.widths.clone()); + let rows = db.count(&mk_sum(vec![UVar::Base(OUT_VAR_ID)], q.term.clone()), &mut Env::new()).unwrap(); + assert!(!claimed || rows <= 1, "{v} has {rows} rows on {tables:?}"); + saw_many |= rows > 1; + } + } + assert!(saw_many, "no relation ever had two rows, so the check above checked nothing"); + } + + #[test] + fn a_slice_is_the_identity_only_where_it_keeps_every_row() { + let lit = |n: &str| Expr::Literal { value: n.to_string(), ty: Type::Integer }; + let one_row = rel(filter(json!({ "scan": 0 }), eq(col(0), param(1)))); + let many = rel(json!({ "scan": 0 })); + let s = schemas(); + assert_eq!(slice(&one_row, None, Some(&lit("1")), 0, &s), Slice::Identity); + assert_eq!(slice(&one_row, Some(&lit("0")), Some(&lit("5")), 0, &s), Slice::Identity); + assert_eq!(slice(&many, None, Some(&lit("0")), 0, &s), Slice::Empty); + assert_eq!(slice(&many, Some(&lit("0")), None, 0, &s), Slice::Identity); + assert_eq!(slice(&many, None, Some(&lit("1")), 0, &s), Slice::Opaque); + assert_eq!(slice(&one_row, Some(&lit("1")), Some(&lit("1")), 0, &s), Slice::Opaque); + let p = Expr::parse(¶m(1), 3).unwrap(); + assert_eq!(slice(&one_row, None, Some(&p), 0, &s), Slice::Opaque); + } +} diff --git a/sqleq-solver/src/ic.rs b/sqleq-solver/src/ic.rs index 8cf6011..12e93d8 100644 --- a/sqleq-solver/src/ic.rs +++ b/sqleq-solver/src/ic.rs @@ -30,12 +30,7 @@ impl Ics { // An absent `nullable` list says nothing, so every column stays nullable. let not_null: HashSet = s.nullable.iter().enumerate().filter(|(_, n)| !**n).map(|(i, _)| i as u32).collect(); - let keys: Vec> = s - .key - .iter() - .map(|k| k.iter().map(|c| *c as u32).collect::>()) - .filter(|k| !k.is_empty() && k.iter().all(|c| not_null.contains(c))) - .collect(); + let keys: Vec> = s.enforced_keys().map(|k| k.iter().map(|c| *c as u32).collect()).collect(); if !not_null.is_empty() { ics.not_null.insert(s.name.clone(), not_null); } diff --git a/sqleq-solver/src/ir.rs b/sqleq-solver/src/ir.rs index bea60bd..278d878 100644 --- a/sqleq-solver/src/ir.rs +++ b/sqleq-solver/src/ir.rs @@ -131,12 +131,15 @@ pub enum TranslateError { /// harmless on real input (which is always well-formed), and strictly safer than a panic. MalformedShape(String), /// Translation-stage-only, not part of `IrToRel`'s taxonomy: a `Sort` with an `offset`/`limit` - /// present. Bare `ORDER BY` (no offset/limit) is a no-op under bag semantics and passes through; - /// real LIMIT/OFFSET semantics (SQLSolver's `OrderbySupport`) is not ported. + /// that changes which rows it keeps. Bare `ORDER BY` (no offset/limit) is a no-op under bag + /// semantics and passes through, and so do `OFFSET 0`, `LIMIT 0` (no rows), and a literal + /// `LIMIT` of one or more over a source with at most one row (see `card`). Any other slice is + /// translated only where the same slice of an equal source stands on the other side (see + /// `opaque`); real LIMIT/OFFSET semantics (SQLSolver's `OrderbySupport`) is not ported. UnsupportedSort, - /// Translation-stage-only: an aggregate call with `distinct: true`. SQLSolver's own translator - /// handles this via a second nested existential sum; this phase deliberately doesn't port that - /// and refuses instead, deferring it rather than half-building it. + /// Translation-stage-only: an aggregate call with `distinct: true` other than `COUNT`, `MAX` + /// and `MIN`. `COUNT(DISTINCT x)` is SQLSolver's nested existential sum, and a `MAX`/`MIN` + /// ignores `DISTINCT`; `SUM`/`AVG(DISTINCT)` would need a sum over values, which is refused. DistinctAggregateUnsupported, /// Translation-stage-only: a scalar subquery (`$SCALAR_QUERY`) whose inner relation doesn't have /// exactly one output column. @@ -213,9 +216,9 @@ impl JoinKind { } } -/// Checks one `[columnIndex, type, "ASCENDING NULLS LAST"]` sort key's shape, which is all that is -/// done with it: a sort is translated only when it has no `offset` or `limit`, and then its order -/// is erased (bag semantics), so nothing reads the key itself. +/// Checks one `[columnIndex, type, "ASCENDING NULLS LAST"]` sort key's shape. Translation erases a +/// sort's order (bag semantics); the keys are read only to tell whether two slices are the same +/// slice (see `opaque`). fn check_collation(v: &Value) -> Result<(), TranslateError> { let arr = v.as_array().filter(|a| a.len() >= 3).ok_or(TranslateError::CollationShape)?; arr[0].as_u64().ok_or(TranslateError::CollationShape)?; @@ -224,6 +227,26 @@ fn check_collation(v: &Value) -> Result<(), TranslateError> { Ok(()) } +/// One key of an `ORDER BY`: the column, whether it sorts descending, and whether nulls come first, +/// read off a `collation` entry `[column, type, "ASCENDING NULLS LAST"]` (see `check_collation`). +/// The column is a position in the sort's own source, not a level: the frontend's `sort_sandwich` +/// widens that source with any key the query does not output. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SortKey { + pub column: u32, + pub descending: bool, + pub nulls_first: bool, +} + +impl SortKey { + fn parse(v: &Value) -> Result { + let arr = v.as_array().filter(|a| a.len() >= 3).ok_or(TranslateError::CollationShape)?; + let column = arr[0].as_u64().ok_or(TranslateError::CollationShape)? as u32; + let spec = arr[2].as_str().ok_or(TranslateError::CollationShape)?; + Ok(SortKey { column, descending: spec.starts_with("DESC"), nulls_first: spec.ends_with("FIRST") }) + } +} + /// One `GROUP BY`/global aggregate function call. `distinct` and `operand` are both optional on the /// wire (`f.path("distinct")`/`f.has("operand")` in `IrToRel.agg()`), defaulting to `false`/`[]`. #[derive(Debug, Clone, PartialEq, Eq)] @@ -250,12 +273,11 @@ impl AggCall { } } -/// A relation node: exactly the 11 tags `IrToRel.rel()` dispatches on (`scan`/`distinct`/`filter`/ -/// `project`/`join`/`group`/`sort`/`values`/`union`/`except`/`intersect`). A bare `"singleton"` -/// string relation (a `FROM`-less query) is *not* a variant here, deliberately: `IrToRel.rel()` -/// requires `r.isObject()` unconditionally and refuses a bare string as `rel-not-object`, so this -/// bridge already can't reach a FROM-less query and this port must refuse it the same way rather -/// than add a case Java doesn't have. +/// A relation node: the 11 tags `IrToRel.rel()` dispatches on (`scan`/`distinct`/`filter`/ +/// `project`/`join`/`group`/`sort`/`values`/`union`/`except`/`intersect`). The bare `"singleton"` +/// string the frontend lowers a `FROM`-less query over is read as what it stands for, a `values` +/// of one row and no columns. `IrToRel.rel()` refuses it (`rel-not-object`, since it requires +/// `r.isObject()`); the JVM fork is a cross-check of this port now, not a contract it must match. #[derive(Debug, Clone, PartialEq, Eq)] pub enum Relation { Scan(usize), @@ -264,8 +286,9 @@ pub enum Relation { Project { source: Box, target: Vec }, Join { left: Box, right: Box, kind: JoinKind, condition: Expr }, Group { source: Box, keys: Vec, function: Vec }, - /// A sort's keys are checked when parsed (see `check_collation`) and not kept. - Sort { source: Box, offset: Option, limit: Option }, + /// A sort's keys are checked when parsed (see `check_collation`) and kept, in clause order, for a + /// prover that compares row slices. + Sort { source: Box, offset: Option, limit: Option, keys: Vec }, Values { schema: Vec, content: Vec> }, Union([Box; 2]), Except([Box; 2]), @@ -277,6 +300,9 @@ impl Relation { /// everything scope-dependent (`correlated`, aggregate-name support, ordinal resolution of group /// keys/agg args) is the translation stage's job, not this one's (see the module doc). pub fn parse(v: &Value, schema_count: usize) -> Result { + if v.as_str() == Some("singleton") { + return Ok(Relation::Values { schema: Vec::new(), content: vec![Vec::new()] }); + } let o = v.as_object().ok_or(TranslateError::RelNotObject)?; if let Some(x) = o.get("scan") { @@ -327,10 +353,12 @@ impl Relation { } if let Some(x) = o.get("sort") { let source = Relation::parse(field(x, "source")?, schema_count)?; - array(field(x, "collation")?)?.iter().try_for_each(check_collation)?; + let collation = array(field(x, "collation")?)?; + collation.iter().try_for_each(check_collation)?; + let keys = collation.iter().map(SortKey::parse).collect::>()?; let offset = opt_expr(x, "offset", schema_count)?; let limit = opt_expr(x, "limit", schema_count)?; - return Ok(Relation::Sort { source: Box::new(source), offset, limit }); + return Ok(Relation::Sort { source: Box::new(source), offset, limit, keys }); } if let Some(x) = o.get("values") { let schema = array(field(x, "schema")?)? @@ -347,11 +375,12 @@ impl Relation { array(row)? .iter() .map(|cell| match Expr::parse(cell, schema_count)? { - // `LogicalValues` holds literals only (`IrToRel.values()`): a computed - // cell would need a `Project` over a one-row values, which our frontend - // never emits. - lit @ Expr::Literal { .. } => Ok(lit), - _ => Err(TranslateError::ValuesNonLiteral), + // `LogicalValues` holds literals only (`IrToRel.values()`), but the + // frontend also writes a parameter, a cast or a call into a cell (a + // `VALUES` row, a closed `FROM`-less `SELECT`), which translation reads + // as the value it computes. A subquery cell is still refused. + Expr::Subquery { .. } => Err(TranslateError::ValuesNonLiteral), + cell => Ok(cell), }) .collect::>() }) @@ -577,6 +606,14 @@ impl Schema { .unwrap_or_default(); Ok(Schema { name, types, key, nullable, opaque_identity }) } + + /// The key groups Postgres enforces on every row: non-empty, with every column NOT NULL. A + /// unique key over a nullable column admits any number of rows holding NULL in it, so it is + /// dropped (the frontend emits only these already; `ic` and `card` both read them here). + pub fn enforced_keys(&self) -> impl Iterator> { + let not_null = |c: &usize| self.nullable.get(*c) == Some(&false); + self.key.iter().filter(move |k| !k.is_empty() && k.iter().all(not_null)) + } } /// The top-level `Input`: `{"schemas": [...], "queries": [Relation, Relation], "help": [String, @@ -689,12 +726,17 @@ mod tests { #[test] fn refuses_a_non_object_relation() { - // The bug `IrToRel.rel()` guards against with `r.isObject()`: a FROM-less "singleton" query - // is a bare string on the wire, which this bridge has never been able to accept. - let err = Relation::parse(&json!("singleton"), 1).unwrap_err(); + let err = Relation::parse(&json!("elsewhere"), 1).unwrap_err(); assert_eq!(err.to_string(), "rel-not-object"); } + #[test] + fn reads_the_singleton_relation_as_one_empty_row() { + // A FROM-less query is lowered over the bare string `"singleton"`. + let r = Relation::parse(&json!("singleton"), 0).unwrap(); + assert_eq!(r, Relation::Values { schema: vec![], content: vec![vec![]] }); + } + #[test] fn refuses_scan_out_of_range() { let err = Relation::parse(&json!({ "scan": 5 }), 1).unwrap_err(); @@ -777,15 +819,38 @@ mod tests { } #[test] - fn refuses_a_non_literal_values_cell() { - let err = Relation::parse( - &json!({ "values": { - "schema": ["INTEGER"], - "content": [[{ "operator": "ABS", "type": "INTEGER", "operand": [{ "operator": "1", "type": "INTEGER" }] }]], + fn reads_a_computed_values_cell_and_refuses_a_subquery_cell() { + let computed = json!({ "values": { + "schema": ["INTEGER"], + "content": [[{ "operator": "ABS", "type": "INTEGER", "operand": [{ "operator": "1", "type": "INTEGER" }] }]], + }}); + assert!(matches!(Relation::parse(&computed, 0), Ok(Relation::Values { .. }))); + let subquery = json!({ "values": { + "schema": ["BOOLEAN"], + "content": [[{ "operator": "EXISTS", "type": "BOOLEAN", "operand": [], "query": { "scan": 0 } }]], + }}); + assert_eq!(Relation::parse(&subquery, 1).unwrap_err().to_string(), "values-nonliteral"); + } + + #[test] + fn keeps_a_sorts_keys_in_clause_order() { + let r = Relation::parse( + &json!({ "sort": { + "source": { "scan": 0 }, + "collation": [[1, "INTEGER", "DESCENDING NULLS FIRST"], [0, "INTEGER", "ASCENDING NULLS LAST"]], + "limit": { "operator": "1", "operand": [], "type": "INTEGER" }, }}), - 0, + 1, ) - .unwrap_err(); - assert_eq!(err.to_string(), "values-nonliteral"); + .unwrap(); + let Relation::Sort { keys, limit, offset, .. } = r else { panic!("not a sort") }; + assert_eq!( + keys, + vec![ + SortKey { column: 1, descending: true, nulls_first: true }, + SortKey { column: 0, descending: false, nulls_first: false }, + ] + ); + assert!(limit.is_some() && offset.is_none()); } } diff --git a/sqleq-solver/src/lib.rs b/sqleq-solver/src/lib.rs index c60f896..07c457f 100644 --- a/sqleq-solver/src/lib.rs +++ b/sqleq-solver/src/lib.rs @@ -18,6 +18,9 @@ //! both sides toward a canonical sum-of-products form, using the schemas' integrity constraints //! (`ic`); `alpha` compares them up to renaming of bound variables (SQLSolver's rung 2); //! `setsolver` hands set-shaped leftovers to Z3 (rung 3); `prove` is the ladder over all of it. +//! Row slices are read where the IR settles them: `card` finds the relations that return at most +//! one row, over which a `LIMIT` keeps everything, and `opaque` replaces the same slice (or opaque +//! aggregate) of equal sources on the two sides by one shared table before translation. //! `eval` evaluates a term on a small concrete database, which is how the tests check that a //! rewrite preserves meaning. SQLSolver's LIA* rung is not rewritten. What it adds is mostly //! reasoning across summands (a disjoint `OR` against a `UNION ALL`), and its integer reading of @@ -27,10 +30,12 @@ //! infinities included. pub mod alpha; +pub mod card; pub mod eval; pub mod ic; pub mod ir; pub mod normalize; +pub mod opaque; pub mod prove; pub mod setsolver; pub mod translate; diff --git a/sqleq-solver/src/opaque.rs b/sqleq-solver/src/opaque.rs new file mode 100644 index 0000000..eb6e3c2 --- /dev/null +++ b/sqleq-solver/src/opaque.rs @@ -0,0 +1,291 @@ +// Unless explicitly stated otherwise all files in this repository are licensed under the +// Apache License Version 2.0. +// This product includes software developed at Datadog (https://www.datadoghq.com/). +// Copyright 2026-Present Datadog, Inc. + +//! Congruence for the nodes translation cannot read: the same slice, or the same opaque aggregate, +//! of equal sources on the two sides is one relation, whatever it computes. +//! +//! Two nodes are refused by translation however they stand: a row slice that keeps some of its +//! rows and not others (`ORDER BY … LIMIT $1`, which `card::slice` cannot read), and a `GROUP BY` +//! whose aggregate translation does not model (the frontend's `DISTINCT_ON#…` carriers, `SUM` of +//! the distinct values). Where one stands on each side with the same specification — the same sort +//! keys, counts, group keys and calls — and the two sources are proved to return the same bag, the +//! two nodes return the same rows, so both are replaced by a scan of one fresh table and the rest +//! of the pair is proved over it. A proof over a table that may hold anything holds in particular +//! for the rows the nodes return. +//! +//! "The same rows" rests on reading a slice as a function of its source's bag, which real SQL does +//! not promise: rows the ordering ties are kept in whatever order the plan reads them. That is the +//! reading QED's opaque `limit`, the frontend's own `strip_identical_pagination` and its lowering +//! (`lower::apply_pagination`) already take, and this module takes nothing beyond it. The frontend +//! keeps it honest where a slice could see more than its source's bag: an order key the query does +//! not output is added to the slice's source (`sort_sandwich`), so the sources compared here carry +//! every key; a slice or `DISTINCT ON` over a subquery whose `ORDER BY` lowering drops is refused +//! there; and so is a slice ordered by a string where a column declares a collation. +//! +//! A node that reads a column of an enclosing query is left alone (its rows differ from one outer +//! row to the next), and so is a pair in which any refused node finds no partner: translation then +//! refuses it as before. Matching is one to one, so two nodes on one side never share a table. + +use crate::card::{self, Slice}; +use crate::ir::{AggCall, Expr, Input, Relation, Schema}; +use crate::prove::{prove_at, Verdict}; + +/// How many sub-proofs deep a source comparison may nest (a slice inside a slice's source). +pub const MAX_DEPTH: usize = 3; + +/// More refused nodes than this on one side and the pair is left to translation to refuse. +const MAX_NODES: usize = 8; + +/// `input` with each refused node replaced by a scan of a fresh table shared with its partner on the +/// other side, when every refused node has one. `None` when there is no refused node, or some node +/// is correlated or has no partner. `depth` is how many sub-proofs deep this pair already is. +pub fn abstract_opaque(input: &Input, depth: usize) -> Option { + let schemas = &input.schemas; + let nodes = |q: &Relation| { + let mut found = Vec::new(); + each_node(&mut q.clone(), 0, schemas, &mut |r, base| { + if !refused(r, base, schemas) { + return false; + } + found.push(rebased(r, base)); + true + }); + found + }; + let (left, right) = (nodes(&input.queries[0]), nodes(&input.queries[1])); + if left.is_empty() || left.len() != right.len() || left.len() > MAX_NODES { + return None; + } + let left: Vec = left.into_iter().collect::>()?; + let right: Vec = right.into_iter().collect::>()?; + + // `partner[j]`: the left node right node `j` is matched with. + let mut partner: Vec> = vec![None; right.len()]; + for (i, l) in left.iter().enumerate() { + let j = (0..right.len()).find(|&j| partner[j].is_none() && congruent(l, &right[j], schemas, depth))?; + partner[j] = Some(i); + } + + let mut schemas = schemas.clone(); + let first = schemas.len(); + for (i, l) in left.iter().enumerate() { + let types = l.output_types(&schemas).into_iter().collect::>>()?; + let nullable = vec![true; types.len()]; + schemas.push(Schema { name: format!("#opaque{i}"), types, key: Vec::new(), nullable, opaque_identity: Vec::new() }); + } + let replace = |q: &Relation, table: &dyn Fn(usize) -> usize| { + let mut q = q.clone(); + let mut seen = 0; + each_node(&mut q, 0, &schemas, &mut |r, base| { + if !refused(r, base, &schemas) { + return false; + } + *r = Relation::Scan(first + table(seen)); + seen += 1; + true + }); + q + }; + let l = replace(&input.queries[0], &|i| i); + let r = replace(&input.queries[1], &|j| partner[j].expect("every right node was matched above")); + Some(Input { schemas, queries: [l, r] }) +} + +/// Whether translation refuses `r`, at level `base`, for being a node it cannot read. +fn refused(r: &Relation, base: usize, schemas: &[Schema]) -> bool { + match r { + Relation::Sort { source, offset, limit, .. } => { + card::slice(source, offset.as_ref(), limit.as_ref(), base, schemas) == Slice::Opaque + } + Relation::Group { function, .. } => function.iter().any(|f| !translated_aggregate(f)), + _ => false, + } +} + +/// The aggregate calls `translate::Translator::agg_eq` models, by name and distinctness. +fn translated_aggregate(f: &AggCall) -> bool { + match f.operator.as_str() { + "COUNT" | "MAX" | "MIN" => true, + "SUM" | "AVG" => !f.distinct, + _ => false, + } +} + +/// `r`, at level `base`, renumbered to stand alone at level 0; `None` when it reads a column of an +/// enclosing query. Every level inside it is at least `base`, so one shift renumbers all of them. +fn rebased(r: &Relation, base: usize) -> Option { + let mut r = r.clone(); + let mut correlated = false; + each_expr(&mut r, &mut |e| { + if let Expr::Column { index, .. } = e { + match (*index as usize).checked_sub(base) { + Some(i) => *index = i as u32, + None => correlated = true, + } + } + }); + (!correlated).then_some(r) +} + +/// Whether two refused nodes, each standing alone at level 0, return the same rows: the same kind +/// and specification, output types known and equal, and sources proved to return the same bag. +fn congruent(l: &Relation, r: &Relation, schemas: &[Schema], depth: usize) -> bool { + let (ls, rs) = match (l, r) { + ( + Relation::Sort { source: ls, offset: lo, limit: ll, keys: lk }, + Relation::Sort { source: rs, offset: ro, limit: rl, keys: rk }, + ) if lk == rk && ll == rl && lo == ro => { + // Keys over every column leave no tie the arrival order could settle. + let width = ls.output_types(schemas).len(); + let total = (0..width).all(|c| lk.iter().any(|k| k.column as usize == c)); + if !total && (erases_an_order(ls, schemas) || erases_an_order(rs, schemas)) { + return false; + } + (ls, rs) + } + ( + Relation::Group { source: ls, keys: lk, function: lf }, + Relation::Group { source: rs, keys: rk, function: rf }, + ) if lk == rk && lf == rf => { + if erases_an_order(ls, schemas) || erases_an_order(rs, schemas) { + return false; + } + (ls, rs) + } + _ => return false, + }; + let (lt, rt) = (l.output_types(schemas), r.output_types(schemas)); + if lt != rt || lt.iter().any(Option::is_none) { + return false; + } + ls == rs + || (depth < MAX_DEPTH + && matches!( + prove_at(&Input { schemas: schemas.to_vec(), queries: [(**ls).clone(), (**rs).clone()] }, depth + 1), + Verdict::Eq { .. } + )) +} + +/// Whether `source` holds an `ORDER BY` translation erases (one with keys that keeps every row). +/// Postgres hands a slice or a `DISTINCT ON` its rows in that order, so where their own keys tie, +/// it decides which rows they keep, and two sources equal as bags but ordered two ways give two +/// answers. The frontend refuses such a node (`lower::refuse_slice_over_dropped_order` and +/// `refuse_distinct_on_over_dropped_order`); the same refusal is kept here so that the claim this +/// module makes does not rest on it. Conservative: an `ORDER BY` anywhere below counts. +fn erases_an_order(source: &Relation, schemas: &[Schema]) -> bool { + let mut found = false; + each_node(&mut source.clone(), 0, schemas, &mut |r, base| { + if let Relation::Sort { source, offset, limit, keys } = r { + found |= !keys.is_empty() + && card::slice(source, offset.as_ref(), limit.as_ref(), base, schemas) == Slice::Identity + && !card::shape(source, base, schemas).max_one(); + } + found + }); + found +} + +/// Visits every relation node of `r` in pre-order, subqueries inside its expressions included, with +/// the level each sits at; `f` returning `true` stops the descent below that node. A subquery's +/// level is its enclosing expression's level plus the width of the row that expression reads, +/// exactly as translation numbers it. +fn each_node(r: &mut Relation, base: usize, schemas: &[Schema], f: &mut dyn FnMut(&mut Relation, usize) -> bool) { + if f(r, base) { + return; + } + let width = |s: &Relation| s.output_types(schemas).len(); + match r { + Relation::Scan(_) | Relation::Values { .. } => {} + Relation::Distinct(source) => each_node(source, base, schemas, f), + Relation::Filter { source, condition } => { + let inner = base + width(source); + each_node(source, base, schemas, f); + each_node_in(condition, inner, schemas, f); + } + Relation::Project { source, target } => { + let inner = base + width(source); + each_node(source, base, schemas, f); + target.iter_mut().for_each(|e| each_node_in(e, inner, schemas, f)); + } + Relation::Join { left, right, condition, .. } => { + let inner = base + width(left) + width(right); + each_node(left, base, schemas, f); + each_node(right, base, schemas, f); + each_node_in(condition, inner, schemas, f); + } + Relation::Group { source, keys, function } => { + let inner = base + width(source); + each_node(source, base, schemas, f); + keys.iter_mut().chain(function.iter_mut().flat_map(|c| c.operand.iter_mut())).for_each(|e| each_node_in(e, inner, schemas, f)); + } + Relation::Sort { source, offset, limit, .. } => { + let inner = base + width(source); + each_node(source, base, schemas, f); + offset.iter_mut().chain(limit.iter_mut()).for_each(|e| each_node_in(e, inner, schemas, f)); + } + Relation::Union(sides) | Relation::Except(sides) | Relation::Intersect(sides) => { + sides.iter_mut().for_each(|s| each_node(s, base, schemas, f)); + } + } +} + +fn each_node_in(e: &mut Expr, base: usize, schemas: &[Schema], f: &mut dyn FnMut(&mut Relation, usize) -> bool) { + match e { + Expr::Column { .. } | Expr::Literal { .. } => {} + Expr::Cast { operand, .. } => each_node_in(operand, base, schemas, f), + Expr::Call { operand, .. } => operand.iter_mut().for_each(|o| each_node_in(o, base, schemas, f)), + Expr::Subquery { operand, query, .. } => { + operand.iter_mut().for_each(|o| each_node_in(o, base, schemas, f)); + each_node(query, base, schemas, f); + } + } +} + +/// Visits every expression node of `r`, those inside its subqueries included. Sort keys are +/// positions in the sort's source, not levels, and are not expressions. +fn each_expr(r: &mut Relation, f: &mut dyn FnMut(&mut Expr)) { + match r { + Relation::Scan(_) => {} + Relation::Values { content, .. } => content.iter_mut().flatten().for_each(|e| each_subexpr(e, f)), + Relation::Distinct(source) => each_expr(source, f), + Relation::Filter { source, condition } => { + each_expr(source, f); + each_subexpr(condition, f); + } + Relation::Project { source, target } => { + each_expr(source, f); + target.iter_mut().for_each(|e| each_subexpr(e, f)); + } + Relation::Join { left, right, condition, .. } => { + each_expr(left, f); + each_expr(right, f); + each_subexpr(condition, f); + } + Relation::Group { source, keys, function } => { + each_expr(source, f); + keys.iter_mut().chain(function.iter_mut().flat_map(|c| c.operand.iter_mut())).for_each(|e| each_subexpr(e, f)); + } + Relation::Sort { source, offset, limit, .. } => { + each_expr(source, f); + offset.iter_mut().chain(limit.iter_mut()).for_each(|e| each_subexpr(e, f)); + } + Relation::Union(sides) | Relation::Except(sides) | Relation::Intersect(sides) => { + sides.iter_mut().for_each(|s| each_expr(s, f)); + } + } +} + +fn each_subexpr(e: &mut Expr, f: &mut dyn FnMut(&mut Expr)) { + f(e); + match e { + Expr::Column { .. } | Expr::Literal { .. } => {} + Expr::Cast { operand, .. } => each_subexpr(operand, f), + Expr::Call { operand, .. } => operand.iter_mut().for_each(|o| each_subexpr(o, f)), + Expr::Subquery { operand, query, .. } => { + operand.iter_mut().for_each(|o| each_subexpr(o, f)); + each_expr(query, f); + } + } +} diff --git a/sqleq-solver/src/prove.rs b/sqleq-solver/src/prove.rs index 44b620c..db79281 100644 --- a/sqleq-solver/src/prove.rs +++ b/sqleq-solver/src/prove.rs @@ -13,6 +13,7 @@ use crate::alpha::alpha_eq; use crate::ic::Ics; use crate::ir::{Input, TranslateError}; use crate::normalize::Normalizer; +use crate::opaque; use crate::setsolver; use crate::translate::{translate_input, Query}; @@ -82,6 +83,15 @@ pub fn verify(ir: &serde_json::Value) -> Verdict { /// The prover proper, for a pair tier 0 did not answer. pub fn prove(input: &Input) -> Verdict { + prove_at(input, 0) +} + +/// [`prove`] for a pair met `depth` sub-proofs deep: the sources of two slices compared by +/// [`opaque`], which first replaces the nodes translation cannot read by tables shared between the +/// two sides, where it can. +pub fn prove_at(input: &Input, depth: usize) -> Verdict { + let abstracted = opaque::abstract_opaque(input, depth); + let input = abstracted.as_ref().unwrap_or(input); let [l, r] = match translate_input(input) { Ok(sides) => sides, Err(e) => return Verdict::Refused(e), diff --git a/sqleq-solver/src/translate.rs b/sqleq-solver/src/translate.rs index b4b65cf..0d8c83c 100644 --- a/sqleq-solver/src/translate.rs +++ b/sqleq-solver/src/translate.rs @@ -52,6 +52,7 @@ //! other (see `dedup_by_identity`). So does `MAX`/`MIN`, which binds the extremum to an input by //! identity, and is refused the same way (see `extremum_by_identity`). +use crate::card::{self, Slice}; use crate::ir::{AggCall, Expr, JoinKind, Relation, Schema, TranslateError, Type}; use crate::uterm::{mk_add, mk_mul, mk_neg, mk_or, mk_squash, mk_sum, PredKind, UConst, UTerm, UVar}; @@ -401,17 +402,21 @@ impl<'s> Translator<'s> { fn rel(&mut self, r: &Relation, base: usize) -> Result { match r { Relation::Scan(i) => self.scan(*i), - Relation::Values { schema, content } => self.values(schema, content), + Relation::Values { schema, content } => self.values(schema, content, base), Relation::Filter { source, condition } => self.filter(source, condition, base), Relation::Project { source, target } => self.project(source, target, base), Relation::Distinct(source) => self.distinct(source, base), Relation::Join { left, right, kind, condition } => self.join(left, right, *kind, condition, base), Relation::Group { source, keys, function } => self.group(source, keys, function, base), + // The order is erased (bag semantics). A slice is read only where it keeps every row or + // none (`card::slice`); any other is refused here, and translated only as the same slice + // of an equal source on both sides (`opaque`). Relation::Sort { source, offset, limit, .. } => { - if offset.is_some() || limit.is_some() { - return Err(TranslateError::UnsupportedSort); + match card::slice(source, offset.as_ref(), limit.as_ref(), base, self.schemas) { + Slice::Identity => self.rel(source, base), + Slice::Empty => Ok(Translated { term: UTerm::Const(UConst::Int(0)), ..self.rel(source, base)? }), + Slice::Opaque => Err(TranslateError::UnsupportedSort), } - self.rel(source, base) } Relation::Union(sides) => self.set_op(SetOpKind::Union, sides, base), Relation::Except(sides) => self.set_op(SetOpKind::Except, sides, base), @@ -437,20 +442,34 @@ impl<'s> Translator<'s> { Ok(Translated { term, local, types, exposed: vec![var] }) } - fn values(&mut self, schema: &[Type], content: &[Vec]) -> Result { + /// A computed cell is the value it computes over no columns of its own: a parameter or a cast + /// is read as anywhere else, and a column reference can only reach an enclosing query, which is + /// refused (`correlated`). Its IR type must be its column's, since the cell's value is bound to + /// the column as is. With no columns at all (the `"singleton"` a `FROM`-less query is lowered + /// over) the rows are copies of the empty tuple, a multiplicity with no var to sum over. + fn values(&mut self, schema: &[Type], content: &[Vec], base: usize) -> Result { + if schema.is_empty() { + if content.iter().any(|row| !row.is_empty()) { + return Err(TranslateError::MalformedShape("values row width does not match schema".into())); + } + let term = UTerm::Const(UConst::Int(content.len() as i64)); + return Ok(Translated { term, local: Vec::new(), types: Vec::new(), exposed: Vec::new() }); + } let var = self.fresh_var(schema.len()); let local: Vec = (0..schema.len() as u32).map(|idx| UVar::proj(idx, var.clone())).collect(); + let no_columns = Scope { base, local: Vec::new(), types: Vec::new() }; let mut rows = Vec::with_capacity(content.len()); for row in content { if row.len() != local.len() { return Err(TranslateError::MalformedShape("values row width does not match schema".into())); } let mut factors = Vec::with_capacity(row.len()); - for (col, cell) in local.iter().zip(row.iter()) { + for ((col, cell), ty) in local.iter().zip(row.iter()).zip(schema) { let v = match cell { Expr::Literal { value, ty } => self.literal_value(value, *ty)?, - // `ir::Relation::parse` already guarantees every `values` cell is a literal - // before this stage ever runs. + // `ir::Relation::parse` refuses a subquery cell before this stage runs. + Expr::Subquery { .. } => return Err(TranslateError::ValuesNonLiteral), + computed if computed.ty() == *ty => self.translate_value(computed, &no_columns)?, _ => return Err(TranslateError::ValuesNonLiteral), }; factors.push(value_eq(&UTerm::Var(col.clone()), &v)); @@ -601,11 +620,24 @@ impl<'s> Translator<'s> { scope: &Scope, col: &UVar, ) -> Result { - if call.distinct { + // `MAX`/`MIN` of the distinct values is `MAX`/`MIN` of the values. + if call.distinct && !matches!(call.operator.as_str(), "COUNT" | "MAX" | "MIN") { return Err(TranslateError::DistinctAggregateUnsupported); } let outcol = UTerm::Var(col.clone()); match call.operator.as_str() { + // `COUNT(DISTINCT x)`: one per value some non-NULL `x` of the group is, SQLSolver's + // nested existential sum. Telling values apart by identity is deduplication, faithful + // only where `=` is identity ([`dedup_by_identity`]). + "COUNT" if call.distinct => { + let [Expr::Column { .. }] = call.operand.as_slice() else { return Err(TranslateError::AggArgNonRef) }; + let x = Self::agg_arg(&call.operand, scope)?; + dedup_by_identity(&[Some(scope.eq_type(&call.operand[0]))])?; + let v = self.fresh_var(1); + let is_v = UTerm::Pred { kind: PredKind::Eq, args: vec![UTerm::Var(UVar::proj(0, v.clone())), x.value] }; + let some_row = mk_squash(mk_sum(source_exposed.to_vec(), mk_mul([group_by_term.clone(), mk_neg(x.is_null), is_v]))); + Ok(value_eq(&outcol, &Value::not_null(mk_sum(vec![v], some_row)))) + } "COUNT" => { let count = if call.operand.is_empty() { mk_sum(source_exposed.to_vec(), group_by_term.clone()) @@ -778,8 +810,11 @@ impl<'s> Translator<'s> { } } + /// Whether `query` returns a row, which a `LIMIT` of one or more does not change + /// ([`card::strip_nonempty_slices`]). fn exists_predicate(&mut self, query: &Relation, scope: &Scope) -> Result { - let inner = self.rel(query, scope.base + scope.local.len())?; + let stripped = card::strip_nonempty_slices(query); + let inner = self.rel(stripped.as_ref().unwrap_or(query), scope.base + scope.local.len())?; Ok(mk_squash(mk_sum(inner.exposed, inner.term))) } diff --git a/sqleq-solver/tests/limit_slices.rs b/sqleq-solver/tests/limit_slices.rs new file mode 100644 index 0000000..ba2ede6 --- /dev/null +++ b/sqleq-solver/tests/limit_slices.rs @@ -0,0 +1,260 @@ +// Unless explicitly stated otherwise all files in this repository are licensed under the +// Apache License Version 2.0. +// This product includes software developed at Datadog (https://www.datadoghq.com/). +// Copyright 2026-Present Datadog, Inc. + +//! Row slices: a `LIMIT` that keeps every row of a source with at most one row (`card`), and the +//! same slice of equal sources on both sides (`opaque`). Each "not proved" pair below differs in +//! Postgres, or is one only the frontend's refusals keep from reaching the prover. + +mod support; + +use serde_json::{json, Value}; +use sqleq_solver::ir::TranslateError; +use sqleq_solver::prove::Verdict; +use support::*; + +/// `t(k, a, b, c)`, keys `(k)` and `(b, c)`, `a` nullable; `u(id, t_k)`, key `(id)`; `n(x)`, a +/// unique key over a nullable column; `v(a, b)` and `w(a, b)`, no keys; `r(k REAL)`, key `(k)`. +fn schemas() -> Vec { + let int4 = ["INTEGER"; 4]; + vec![ + table("t", &int4, &[false, true, false, false], &[&[0], &[2, 3]]), + table("u", &int4[..2], &[false, true], &[&[0]]), + table("n", &int4[..1], &[true], &[&[0]]), + table("v", &int4[..2], &[true, true], &[]), + table("w", &int4[..2], &[true, true], &[]), + table("r", &["REAL"], &[false], &[&[0]]), + ] +} + +fn int(i: u32) -> Value { + col(i, "INTEGER") +} + +fn param(n: u32) -> Value { + call(&format!("QP{n}"), "INTEGER", vec![lit("0", "INTEGER")]) +} + +fn eq(a: Value, b: Value) -> Value { + pred("=", vec![a, b]) +} + +fn and(parts: Vec) -> Value { + pred("AND", parts) +} + +/// `ORDER BY keys LIMIT limit OFFSET offset` over `source`; `keys` are `(position, descending)`. +fn page(source: Value, keys: &[(u32, bool)], limit: Option, offset: Option) -> Value { + let collation: Vec = keys + .iter() + .map(|(c, desc)| json!([c, "INTEGER", if *desc { "DESCENDING NULLS FIRST" } else { "ASCENDING NULLS LAST" }])) + .collect(); + json!({ "sort": { "source": source, "collation": collation, "limit": limit, "offset": offset } }) +} + +fn limit(source: Value, n: Value) -> Value { + page(source, &[], Some(n), None) +} + +fn one() -> Value { + lit("1", "INTEGER") +} + +/// `SELECT a FROM t WHERE cond`. +fn a_where(cond: Value) -> Value { + project(filter(scan(0), cond), vec![int(1)]) +} + +fn in_(operand: Vec, query: Value) -> Value { + json!({ "operator": "IN", "type": "BOOLEAN", "operand": operand, "query": query }) +} + +fn verdict(a: Value, b: Value) -> Verdict { + pair(schemas(), a, b) +} + +#[test] +fn limit_one_over_a_key_held_to_a_parameter_keeps_every_row() { + let q = || a_where(eq(int(0), param(1))); + assert_eq!(verdict(q(), limit(q(), one())), Verdict::Eq { literal: false }); + // Any literal count of one or more, and an `OFFSET 0`. + assert!(proved(&verdict(q(), page(q(), &[(0, false)], Some(lit("10", "INTEGER")), Some(lit("0", "INTEGER")))))); + // Both columns of the composite key. + let bc = || a_where(and(vec![eq(int(2), param(1)), eq(param(2), int(3))])); + assert!(proved(&verdict(bc(), limit(bc(), one())))); +} + +#[test] +fn a_key_held_through_a_join_or_a_group_keeps_every_row() { + // `SELECT t.a FROM u JOIN t ON t.k = u.t_k WHERE u.id = $1`: `t`'s columns follow `u`'s. + let joined = || { + let join = json!({ "join": { "kind": "INNER", "left": scan(1), "right": scan(0), "condition": eq(int(2), int(1)) } }); + project(filter(join, eq(int(0), param(1))), vec![int(3)]) + }; + assert!(proved(&verdict(joined(), limit(joined(), one())))); + // `SELECT a, count(*) FROM t WHERE a = $1 GROUP BY a`: one group at most. + let grouped = || group(project(filter(scan(0), eq(int(1), param(1))), vec![int(1)]), vec![int(0)], vec![agg("COUNT", "INTEGER", vec![])]); + assert!(proved(&verdict(grouped(), limit(grouped(), one())))); +} + +#[test] +fn limit_zero_and_offset_zero() { + let all = || project(scan(0), vec![int(1)]); + assert!(proved(&verdict(limit(all(), lit("0", "INTEGER")), a_where(lit("FALSE", "BOOLEAN"))))); + assert!(proved(&verdict(page(all(), &[(0, false)], None, Some(lit("0", "INTEGER"))), all()))); +} + +#[test] +fn a_limit_under_exists_keeps_its_answer() { + // `EXISTS (SELECT 1 FROM u WHERE u.t_k = $1 [LIMIT 1])`: `u`'s columns follow `t`'s. + let sub = || project(filter(scan(1), eq(int(5), param(1))), vec![one()]); + let ks = |cond: Value| project(filter(scan(0), cond), vec![int(0)]); + assert!(proved(&verdict(ks(exists(sub())), ks(exists(limit(sub(), one())))))); + // `OFFSET 1` can make it empty. + let skipped = page(sub(), &[], Some(one()), Some(one())); + assert!(!proved(&verdict(ks(exists(sub())), ks(exists(skipped))))); +} + +#[test] +fn a_limit_over_rows_no_key_holds_is_not_the_identity() { + let cases = [ + (0, eq(int(1), param(1))), // `a` is no key + (0, eq(int(2), param(1))), // half of `(b, c)` + (0, pred("<=", vec![int(0), param(1)])), // an order comparison + (0, pred("OR", vec![eq(int(0), param(1)), eq(int(0), param(2))])), + (2, eq(int(0), param(1))), // a key over a nullable column + (5, eq(col(0, "REAL"), call("QP1", "REAL", vec![lit("0", "INTEGER")]))), // `=` on REAL + ]; + for (table, cond) in cases { + let q = || project(filter(scan(table), cond.clone()), vec![int(0)]); + assert!(!proved(&verdict(q(), limit(q(), one()))), "{cond}"); + } + // A parameter count may be 0; an offset may skip the one row. + let q = || a_where(eq(int(0), param(1))); + assert!(!proved(&verdict(q(), limit(q(), param(2))))); + assert!(!proved(&verdict(q(), page(q(), &[], Some(one()), Some(one()))))); +} + +/// `SELECT k FROM t WHERE ORDER BY c LIMIT $3`, lowered with +/// the order key in the slice's source (`sort_sandwich`) and trimmed above it. +fn page_of_t(swapped: bool, keys: &[(u32, bool)], limit: Value) -> Value { + let (x, y) = (eq(int(1), param(1)), eq(int(2), param(2))); + let cond = if swapped { and(vec![y, x]) } else { and(vec![x, y]) }; + project(page(project(filter(scan(0), cond), vec![int(0), int(3)]), keys, Some(limit), None), vec![int(0)]) +} + +#[test] +fn the_same_slice_of_equal_sources_is_one_relation() { + let by_c = [(1, false)]; + assert_eq!(verdict(page_of_t(false, &by_c, param(3)), page_of_t(true, &by_c, param(3))), Verdict::Eq { literal: false }); + // Nested in an `IN` subquery, whose columns follow the outer `t`'s. + let sub = |swapped: bool| { + let (x, y) = (eq(int(5), param(1)), eq(int(6), param(2))); + let cond = if swapped { and(vec![y, x]) } else { and(vec![x, y]) }; + project(page(project(filter(scan(0), cond), vec![int(4), int(7)]), &by_c, Some(param(3)), None), vec![int(4)]) + }; + let outer = |swapped| project(filter(scan(0), in_(vec![int(0)], sub(swapped))), vec![int(1)]); + assert!(proved(&verdict(outer(false), outer(true)))); +} + +#[test] +fn a_different_slice_is_not_the_same_relation() { + let p3 = || param(3); + for (keys, lim) in [(vec![(1, true)], p3()), (vec![(0, false)], p3()), (vec![(1, false)], param(4))] { + let v = verdict(page_of_t(false, &[(1, false)], p3()), page_of_t(true, &keys, lim)); + assert_eq!(v, Verdict::Refused(TranslateError::UnsupportedSort)); + } + // Two slices on one side, one on the other. + let two = json!({ "union": [page_of_t(false, &[(1, false)], p3()), page_of_t(false, &[(1, false)], p3())] }); + let one_and_scan = json!({ "union": [page_of_t(true, &[(1, false)], p3()), project(scan(0), vec![int(0)])] }); + assert_eq!(verdict(two, one_and_scan), Verdict::Refused(TranslateError::UnsupportedSort)); +} + +#[test] +fn a_slice_of_a_correlated_source_is_left_refused() { + // `SELECT k FROM t WHERE c = $2 AND a = (SELECT t_k FROM u WHERE u.t_k = t.b ORDER BY id LIMIT $1)`. + let sub = || { + let src = filter(scan(1), eq(int(5), int(2))); + scalar(project(page(src, &[(0, false)], Some(param(1)), None), vec![int(5)]), "INTEGER") + }; + let (x, y) = (|| eq(int(3), param(2)), || eq(int(1), sub())); + let a = project(filter(scan(0), and(vec![x(), y()])), vec![int(0)]); + let b = project(filter(scan(0), and(vec![y(), x()])), vec![int(0)]); + assert_eq!(verdict(a, b), Verdict::Refused(TranslateError::UnsupportedSort)); +} + +#[test] +fn equal_bags_under_a_slice_are_not_enough_when_the_slice_reads_more() { + // `SELECT a FROM v ORDER BY b LIMIT 1` against the same over `w`: as `SELECT a`, both may be + // the bag {1, 2}, but over v = {(1,1), (2,2)} and w = {(1,2), (2,1)} one yields 1, the other 2. + // The order key is in the slice's source, so the sources differ. + let first_a = |table| project(page(project(scan(table), vec![int(0), int(1)]), &[(1, false)], Some(one()), None), vec![int(0)]); + assert!(!proved(&verdict(first_a(3), first_a(4)))); + // `SELECT k FROM (SELECT k FROM t ORDER BY k [DESC]) s LIMIT 1`: min(k) against max(k). The + // frontend refuses a slice over a subquery order it drops; this module refuses it as well. + let first_of = |desc| limit(page(project(scan(0), vec![int(0)]), &[(0, desc)], None, None), one()); + assert!(!proved(&verdict(first_of(false), first_of(true)))); + // Ordered by every column it returns, ties are equal rows and the order beneath does not matter. + let ordered = |desc| page(page(project(scan(0), vec![int(0)]), &[(0, desc)], None, None), &[(0, false)], Some(one()), None); + assert!(proved(&verdict(ordered(false), ordered(true)))); +} + +#[test] +fn the_same_distinct_on_of_equal_sources_is_one_relation() { + // `SELECT DISTINCT ON (a) a, k FROM t WHERE ORDER BY a, k`. + let distinct_on = |swapped: bool| { + let (x, y) = (eq(int(2), param(1)), eq(int(3), param(2))); + let cond = if swapped { and(vec![y, x]) } else { and(vec![x, y]) }; + let pick = json!({ "operator": "DISTINCT_ON#0<0:ASCENDING NULLS LAST;1:ASCENDING NULLS LAST;>", + "type": "INTEGER", "distinct": false, "ignoreNulls": false, "operand": [int(1), int(0)] }); + group(filter(scan(0), cond), vec![int(1)], vec![pick]) + }; + assert!(proved(&verdict(distinct_on(false), distinct_on(true)))); +} + +#[test] +fn a_from_less_select_reads_its_one_row() { + // `SELECT EXISTS (SELECT 1 FROM t WHERE [LIMIT 1])`. + let sub = |swapped: bool| { + let (x, y) = (eq(int(1), param(1)), eq(int(2), param(2))); + project(filter(scan(0), if swapped { and(vec![y, x]) } else { and(vec![x, y]) }), vec![one()]) + }; + let select = |e: Value| project(json!("singleton"), vec![e]); + assert!(proved(&verdict(select(exists(sub(false))), select(exists(sub(true)))))); + assert!(proved(&verdict(select(exists(sub(false))), select(exists(limit(sub(false), one())))))); +} + +#[test] +fn a_values_cell_may_compute_its_value() { + let values = |cell: Value| json!({ "values": { "schema": ["INTEGER"], "content": [[cell]] } }); + // `SELECT x FROM (VALUES ($1)) v(x)`, filtered on TRUE or not. + let plain = project(values(param(1)), vec![int(0)]); + let filtered = project(filter(values(param(1)), lit("TRUE", "BOOLEAN")), vec![int(0)]); + assert!(proved(&verdict(plain, filtered))); + // A cell of another type than its column is refused, not coerced. + let text = call("QP1", "VARCHAR", vec![lit("0", "INTEGER")]); + assert_eq!(verdict(project(values(text), vec![int(0)]), project(scan(1), vec![int(0)])), Verdict::Refused(TranslateError::ValuesNonLiteral)); +} + +#[test] +fn count_distinct_counts_the_distinct_non_null_values() { + let count_distinct = |c: u32| { + let call = json!({ "operator": "COUNT", "type": "INTEGER", "distinct": true, "ignoreNulls": true, "operand": [int(0)] }); + group(project(filter(scan(0), eq(int(0), param(1))), vec![int(c)]), vec![], vec![call]) + }; + // `SELECT count(*) FROM (SELECT DISTINCT FROM t WHERE k = $1) d`. + let count_of_distinct = |c: u32| { + let distinct_c = distinct(project(filter(scan(0), eq(int(0), param(1))), vec![int(c)]), &["INTEGER"]); + group(distinct_c, vec![], vec![agg("COUNT", "INTEGER", vec![])]) + }; + // `b` is NOT NULL: the two agree. + assert!(proved(&verdict(count_distinct(2), count_of_distinct(2)))); + // `a` is nullable: `count(DISTINCT a)` skips the NULL that `SELECT DISTINCT a` keeps. + assert!(!proved(&verdict(count_distinct(1), count_of_distinct(1)))); + // `sum(DISTINCT ...)` stays refused. + let sum = json!({ "operator": "SUM", "type": "INTEGER", "distinct": true, "ignoreNulls": true, "operand": [int(0)] }); + let summed = group(project(scan(0), vec![int(2)]), vec![], vec![sum]); + let plain = group(project(scan(0), vec![int(2)]), vec![], vec![agg("SUM", "INTEGER", vec![int(0)])]); + assert_eq!(verdict(summed, plain), Verdict::Refused(TranslateError::DistinctAggregateUnsupported)); +} diff --git a/tests/pairs/dml/insert_values_stores_numeric_literal_as_text.sql b/tests/pairs/dml/insert_values_stores_numeric_literal_as_text.sql index 361a77a..ac4b88f 100644 --- a/tests/pairs/dml/insert_values_stores_numeric_literal_as_text.sql +++ b/tests/pairs/dml/insert_values_stores_numeric_literal_as_text.sql @@ -7,7 +7,7 @@ -- expect frontend: emit -- expect fuzz: counterexample -- expect qed: no-proof --- expect sqleq-solver: unsupported +-- expect sqleq-solver: no-proof -- expect lean: unsupported -- origin: issue #107: an INSERT ... VALUES stored a numeric literal in a text column by its value, and -- 2.0 = 2.00 diff --git a/tests/pairs/pagination/nested_limit_ties_under_filter.sql b/tests/pairs/pagination/nested_limit_ties_under_filter.sql index 739c14f..f4bef48 100644 --- a/tests/pairs/pagination/nested_limit_ties_under_filter.sql +++ b/tests/pairs/pagination/nested_limit_ties_under_filter.sql @@ -7,7 +7,7 @@ -- expect frontend: emit -- expect fuzz: nondet-skip -- expect qed: proved --- expect sqleq-solver: unsupported +-- expect sqleq-solver: proved -- expect lean: unsupported -- origin: issue #124: sqleq-fuzz compared a trial whose LIMIT leaves ties by cardinality alone even under a -- filter, where the tied row the LIMIT keeps decides how many rows survive diff --git a/tests/pairs/types/union_null_branch.sql b/tests/pairs/types/union_null_branch.sql index 1d37585..d6d89d5 100644 --- a/tests/pairs/types/union_null_branch.sql +++ b/tests/pairs/types/union_null_branch.sql @@ -7,7 +7,7 @@ -- expect frontend: emit -- expect fuzz: no-counterexample -- expect qed: proved --- expect sqleq-solver: unsupported +-- expect sqleq-solver: proved -- expect lean: unsupported -- origin: issue #177: a NULL branch is typed INTEGER, and a text column under it reached the prover -- ill-typed diff --git a/tests/pairs/types/values_integer_beside_numeric.sql b/tests/pairs/types/values_integer_beside_numeric.sql index aecc7bb..4872eb5 100644 --- a/tests/pairs/types/values_integer_beside_numeric.sql +++ b/tests/pairs/types/values_integer_beside_numeric.sql @@ -7,7 +7,7 @@ -- expect frontend: emit -- expect fuzz: no-counterexample -- expect qed: proved --- expect sqleq-solver: unsupported +-- expect sqleq-solver: no-proof -- expect lean: unsupported -- origin: issue #177: a VALUES column took its first row's type, so the integer row reached the -- prover under a numeric column and QED panicked