Issues

• decision: sqleq-lean and VALUES cells that compute a value (now() + make_interval(days := $2), a scalar subquery): prove them under the generated-cell claim, and under which verdict?

  question
  datadog-labs/sqleq#221 · Filter by author zvonimir-dd opened on Oct 30, 2026

• decision: may a lock on one table of a join (FOR UPDATE OF t) move into a CTE over that table? Postgres 17 tells the two apart under concurrency

  question
  datadog-labs/sqleq#220 · Filter by author zvonimir-dd opened on Oct 30, 2026

• research: classify the pairs the provers leave unproved and sqleq-fuzz does not refute, and open one issue per gap

  enhancement
  datadog-labs/sqleq#219 · Filter by author zvonimir-dd opened on Oct 30, 2026

• Drop the sqlparser [patch] once a release carries apache/datafusion-sqlparser-rs#2626 and #2627

  dependencies
  datadog-labs/sqleq#218 · Filter by author zvonimir-dd opened on Oct 30, 2026

• sqleq-lean: over 500 VALUES rows no witness is attempted, and the replay then reports the skipped witness as a model disagreement

  enhancement
  datadog-labs/sqleq#217 · Filter by author zvonimir-dd opened on Oct 30, 2026

• tools/lean_replay.py: --setup installs 5 of sqleq-fuzz's 9 extensions and has no values for their types, so a Lean proof over an ltree column stays inconclusive

  bug
  datadog-labs/sqleq#216 · Filter by author zvonimir-dd opened on Oct 30, 2026

• sqleq-lean: read a schema-qualified generator, or an expression over the statement clock, as a recognised column default

  enhancement
  datadog-labs/sqleq#215 · Filter by author zvonimir-dd opened on Oct 30, 2026

• frontend: a CASE whose results are all untyped parameters is typed opaque, not text, so a set operation pairing it with a text column is refused

  enhancement
  datadog-labs/sqleq#214 · Filter by author zvonimir-dd opened on Oct 30, 2026

• frontend: lower a window call as an opaque term keyed by its input relation, so queries that differ only outside identical windows can be proved

  enhancement
  datadog-labs/sqleq#213 · Filter by author zvonimir-dd opened on Oct 30, 2026

• sqleq-lean: support an ON CONFLICT target with a WHERE predicate (a partial unique index as the arbiter)

  enhancement
  datadog-labs/sqleq#212 · Filter by author zvonimir-dd opened on Oct 30, 2026

• frontend: a locked subquery read through IN on one side and as a USING derived table on the other is refused, though both lock the same rows

  enhancement
  datadog-labs/sqleq#211 · Filter by author zvonimir-dd opened on Oct 30, 2026

• sqleq-fuzz: the date and timestamp domains have no infinity, so a cast to date is never told from a one-day range

  enhancement
  datadog-labs/sqleq#210 · Filter by author zvonimir-dd opened on Oct 30, 2026

• sqleq-fuzz: after #205, a literal compared with an expression of a column, or seen through a value-changing cast, still hides a boundary difference

  datadog-labs/sqleq#207 · Filter by author alpaylan opened on Oct 21, 2026
  1

• frontend: resolve table names through a declared search path, so a bare t and s.t can be one table

  enhancement
  datadog-labs/sqleq#91 · Filter by author zvonimir-dd opened on Oct 7, 2026
  2