zvonimir-dd · Nov 1, 2026 · Oct 31, 2026
@@ -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
 

@@ -30,12 +30,7 @@ impl Ics {
             // An absent `nullable` list says nothing, so every column stays nullable.
             let not_null: HashSet<u32> =
                 s.nullable.iter().enumerate().filter(|(_, n)| !**n).map(|(i, _)| i as u32).collect();
-            let keys: Vec<Vec<u32>> = s
-                .key
-                .iter()
-                .map(|k| k.iter().map(|c| *c as u32).collect::<Vec<u32>>())
-                .filter(|k| !k.is_empty() && k.iter().all(|c| not_null.contains(c)))
-                .collect();
+            let keys: Vec<Vec<u32>> = 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);
             }

@@ -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<SortKey, TranslateError> {
+        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<Relation>, target: Vec<Expr> },
     Join { left: Box<Relation>, right: Box<Relation>, kind: JoinKind, condition: Expr },
     Group { source: Box<Relation>, keys: Vec<Expr>, function: Vec<AggCall> },
-    /// A sort's keys are checked when parsed (see `check_collation`) and not kept.
-    Sort { source: Box<Relation>, offset: Option<Expr>, limit: Option<Expr> },
+    /// 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<Relation>, offset: Option<Expr>, limit: Option<Expr>, keys: Vec<SortKey> },
     Values { schema: Vec<Type>, content: Vec<Vec<Expr>> },
     Union([Box<Relation>; 2]),
     Except([Box<Relation>; 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<Relation, TranslateError> {
+        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::<Result<_, _>>()?;
             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::<Result<_, _>>()
                 })
@@ -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<Item = &Vec<usize>> {
+        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());
     }
 }
@@ -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;