Unsound: `ignoreNulls` is forwarded from Calcite, so `COUNT(x)` proves equivalent to `COUNT(*)`

[zvonimir-dd]

RelJSONShuttle serializes every aggregate call's ignoreNulls from Calcite's
AggregateCall.ignoreNulls(). That method reports whether the SQL IGNORE NULLS null-treatment
modifier was written — a window-function concept (LAG, LEAD, FIRST_VALUE, …) — not whether the
aggregate skips NULL inputs. COUNT(x), SUM, AVG, MIN and MAX skip NULLs by definition and
never carry the modifier, so they are all serialized with "ignoreNulls": false.

The prover reads false as "fold over every row, including rows where the argument is NULL". For
COUNT the summand is the constant 1, so without the NULL restriction the argument no longer
affects the result, and every COUNT(x) becomes COUNT(*).

Reproduction

Straight through qed-parser and qed-prover, no hand-edited IR:

create table "t" ("k" INTEGER, "a" INTEGER);
select "k", count("a") from "t" group by "k";
select "k", count(*)   from "t" group by "k";

create table "t" ("k" INTEGER, "a" INTEGER, "b" INTEGER);
select "k", count("a") from "t" group by "k";
select "k", count("b") from "t" group by "k";

$ qed-parser repro.sql && qed-prover repro.json   # both
{"provable":true, ...}

Expected: not provable. One row separates all three queries — over t = [(1, NULL, 5)],
count(a) gives (1, 0) while count(b) and count(*) give (1, 1).

The emitted IR for count("a"):

{"operator": "COUNT", "operand": [{"column": 1, "type": "INTEGER"}],
 "distinct": false, "ignoreNulls": false, "type": "BIGINT"}

Changing only that field to true makes the first pair not provable.

(The reproductions use GROUP BY "k" on purpose: scalar aggregation has a separate, unrelated
problem in the prover, reported in qed-solver/prover#9.)

Root cause

src/main/java/org/qed/RelJSONShuttle.java:202, and the same expression at
JSONSerializer.java:106:

"ignoreNulls", bool(call.ignoreNulls()),

The prover consumes the flag in src/pipeline/relation.rs (inside Group and in the scalar
aggregate evaluator):

let body = if agg.ignore_nulls {
    let conditions = inner_vars.iter().map(|v| !v.clone().is_null());
    UExpr::pred(conditions.product()) * body
} else {
    body
};

and its serde default for a missing field is already true (default_ignore_nulls). So the prover
is right, and only the explicit false from the parser triggers the bug.

This is not an edge case: the prover's own tests/ contain 119 argument-bearing COUNT calls
serialized with "ignoreNulls": false, across 49 files.

Suggested fix

Derive the flag from the aggregate's own semantics instead of forwarding Calcite's:

// SQL aggregates skip NULL arguments by definition; Calcite's ignoreNulls() is the
// IGNORE NULLS window modifier, which is a different question.
boolean skipsNulls = !call.getArgList().isEmpty()
        && NULL_SKIPPING.contains(call.getAggregation().getKind());  // COUNT, SUM, SUM0, AVG, MIN, MAX, ...

Two cases must stay false, which is why this cannot be a constant true:

1. COUNT(*). The prover lowers an argument-less COUNT over the whole source row, so true
   there would require every column of the row to be non-NULL for it to be counted.
2. Aggregates whose NULL handling the parser does not know. array_agg keeps NULLs, string_agg
   drops them; false costs a proof rather than proving a non-equivalence.

Possibly related (unverified)

RelRacketShuttle.java:84 reads the same flag with what looks like the opposite polarity:

case "count" -> "aggr-count" + (agg.isDistinct() ? "-distinct" : "") +
        (agg.ignoreNulls() ? "-all" : "");

If aggr-count-all means counting every row, the JSON and Racket backends interpret the flag in
opposite directions. I have not checked this against the Racket side.

Environment

qed-parser at 684daf2, qed-prover at 31f4b6c, both built with Nix. Found by differential
testing against a concrete database; the expected results were checked in DuckDB.