[zvonimir-dd]

What type of PR is this?

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

Description

Fixes #202.

Why

-- truth: not-equivalent
create table "pg_attribute" ("attname" TEXT PRIMARY KEY, "attnum" INTEGER);
SELECT DISTINCT "attname" FROM "pg_attribute";
SELECT "attname" FROM "pg_attribute";

Postgres searches pg_catalog before the search path unless the path names it. So after CREATE TABLE "pg_attribute", which puts a table in public, both queries read pg_catalog.pg_attribute. On a fresh Postgres 17.11 database, side A returns 1188 rows, side B 3146, and public.pg_attribute holds 0.

The frontend lowered the reference against the declared table and its key, so DISTINCT was redundant and qed and sqleq-solver proved the pair:

1. resolve_tables asks safe_to_strip, which is false for any bare pg_* name.
2. ResolveTable then leaves the name as written. That guard only stops the schema strip; it refuses nothing.
3. lower::factor_instance then finds the declared table with Catalog::find.

dml::find_target's doc stated the assumption that broke: that a reference the guards leave unstripped "then fails to resolve" in lower.

Two more channels the issue does not name

Neither raises a --portfolio alarm on main. sqleq-fuzz cannot create their DDL and answers error, so the false proof is silent.

• A table the DDL declares under a system schema. create table "pg_catalog"."pg_attribute" (…) with FROM "pg_catalog"."pg_attribute" lowered against the declared key. Postgres refuses that CREATE TABLE, so the queries always read the catalog. The issue's proposed exemption ("qualified by a schema the DDL declares it in") would have let this through.
• A stripped system qualifier. safe_to_strip matched qualifiers against a fixed list (pg_catalog, information_schema, pg_temp, sys). So pg_toast.t and pg_temp_3.t were stripped to t and lowered against the DDL's t. pg_temp_3.t is a session's own temporary table, which is a real witness.

The rule

A relation reference names a system relation, and is refused as unsupported whatever the DDL declares, when either holds:

• it is a bare name starting with pg_;
• any qualifier part is a system schema: information_schema, or any name starting with pg_, a prefix Postgres reserves for its own schemas (CREATE SCHEMA pg_x is an error).

A pg_* table in a user's schema, read through that schema (public.pg_attribute, s.pg_x), is the user's table and still lowers. A WITH binding named like a catalog relation is the binding, as in Postgres; inline_ctes removes it before lowering.

The rule is the prefix, not a per-major list of catalog relations:

• Postgres documents that its system relations keep the pg_ prefix so that they cannot collide with user tables that avoid it.
• On Postgres 17.11, no pg_catalog relation lacks the prefix (SELECT count(*) FROM pg_class WHERE relnamespace = 'pg_catalog'::regnamespace AND relname NOT LIKE 'pg\_%' is 0).
• A list would go stale in the unsound direction, since every major adds relations. PG_CATALOG_TYPES is a list only because types share no prefix.

Where it is checked

• normalize::system_relation (with system_schema and system_key) implements the rule, beside safe_to_strip.
• safe_to_strip uses system_schema for qualifiers, so no pg_ schema is stripped. sys is kept.
• lower::factor_instance refuses before the catalog lookup. This is the one place a table becomes a scan, so it covers declared, raw-DDL, corpus and inferred catalogs, and the UPDATE/DELETE reductions, whose targets and USING/FROM lists become FROM items.
• dml::insert_pair refuses an INSERT target, because the target is replaced by its source and never reaches lowering. The check runs before the short-circuit that skips safe_to_strip for declared targets. It also covers the key a bare target resolves to (t to a declared pg_catalog.t).
• sqleq-lean refuses the same INSERT targets in recognize::extract, since its schema keys tables by bare name. The helper is re-exported through internals.
• docs/SOUNDNESS.md gains the rule, why it is a prefix, and what it costs.

What it costs

Each of these is a refusal where Postgres would read the user's table:

• a user's pg_* table read bare (read through its schema, it lowers);
• a temporary table of such a name;
• a table a DDL creates as pg_temp.t;
• a new table a superuser adds to information_schema;
• a query over the catalog under an inferred catalog.

Undeclared catalog relations change refusal kind, from schema ("unknown table") to unsupported. Postgres accepts those queries, so unsupported is the right kind under tests/refusal_kinds.rs's rule.

Pins that moved

None. Four new pins under tests/pairs/names/, blessed on frontend, fuzz, qed, sqleq-solver and lean:

Pin	Truth	Pre-fix build (29c3d05)	After
catalog_relation_shadows_declared_table.sql (the issue's pair)	not-equivalent	qed proved, sqleq-solver proved, fuzz counterexample: alarm	refuse:unsupported, no-plan
catalog_qualified_declared_table.sql	not-equivalent	qed proved, sqleq-solver proved, fuzz error: silent	refuse:unsupported, no-plan
temp_schema_qualifier_not_stripped.sql	not-equivalent	qed proved, sqleq-solver proved, fuzz error: silent	refuse:unsupported, no-plan
public_qualified_pg_named_table.sql (control)	equivalent	emit, proved	unchanged

How it was tested

• Pre-fix run. The four pins on a pre-fix build (29c3d05, whose frontend matches main): 0/4 hold, with six false proofs, as tabled above.
• Post-fix run. The same four pins: 4/4 hold on all five axes.
• New tests.
  • tests/system_relations.rs runs each channel through both DDL readers and all three catalog modes: bare names, system-schema qualifiers, INSERT/UPDATE/DELETE targets, and a bare target resolving to a declared pg_catalog.t. Its controls are public.pg_attribute, s.pg_x, an INSERT into public.pg_attribute, and a WITH "pg_class" binding.
  • Unit tests in normalize cover the rule and the pg_toast/pg_temp_N/pg_toast_temp_N strip cases. sqleq-lean has a unit test for the refused targets.
  • tests/refusal_kinds.rs gets a row: SELECT "relname" FROM "pg_class" prepares on Postgres 17 and is refused unsupported.
• Workspace tests. cargo test --workspace: 1301 passed, 0 failed.
• Lints. cargo clippy --all-targets, --features internals --all-targets and -p sqleq-lean --all-targets, each with -D warnings: clean.
• Full pin suite. sqleq-check --expect pinned --axes frontend,qed,sqleq-solver,fuzz,lean tests/pairs examples/*.sql: 473/475. The two that fail are aggregates/scalar_agg_empty_group.sql and aggregates/unlisted_var_pop_under_exists.sql, where qed says proved against a pinned no-proof. Their IR is byte-identical before and after this change, and a pre-fix build fails them the same way with the same qed-prover (the newest of several builds in the local Nix store). They come from that prover build, not from this PR. Every other axis holds on both.
• Postgres 17.11 checks.
  • The issue's row counts reproduce.
  • CREATE TABLE in pg_catalog and pg_toast is refused, and CREATE SCHEMA pg_x is rejected.
  • A WITH pg_class binding shadows the catalog.
  • search_path = public, pg_catalog does reach the user's table, which is the opening frontend: resolve table names through a declared search path, so a bare t and s.t can be one table #91 could later use.

Frontend A/B over the benchmark corpus. The corpus is private, so these counts are for scale only. The main and post-fix sqleq-frontend were run over all 90,145 rows, under the declared and the inferred-seeded catalogs, and compared row by row:

• No verdict moved. Emitted rows (788 and 49,043) and reflexive rows (41,344 and 2,915) are unchanged.
• IR is byte-identical for every row both builds emit.
• The only change: 12 rows (declared) and 13 (inferred-seeded) move from refuse:schema to refuse:unsupported, each with the new system-relation reason. Two of those rows are in the latest all-axes run, and stay refused.

This change only refuses, so it shrinks the provable set, and rule 2's cross-check does not apply.

Checklist

• A construct the frontend cannot lower faithfully is refused, not approximated.
• If this grows the provable set, the same pairs were run through sqleq-check --portfolio
  (the provers and sqleq-fuzz at once; a proof with a counterexample is an alarm), and none
  of the newly proven pairs has a counterexample. (It only refuses; the corpus A/B shows no row gaining a proof.)
• If this fixes a defect that can be stated as a pair, the pair is pinned under tests/pairs/
  and was seen failing on a build from before the fix.
• Every pin under tests/pairs/ that moved is explained in the description. (None moved.)
• If dependencies changed, LICENSE-3rdparty.csv was regenerated with
  sh tools/update_license_3rdparty.sh. (No dependency change.)

Out of scope

• frontend: resolve table names through a declared search path, so a bare t and s.t can be one table #91: a declared search path naming pg_catalog after the user's schemas could later relax the bare-name rule.
• frontend: a quoted schema qualifier is folded to lower case, so "S".t is read as s.t and proved equal to it #203: quoted-name folding. This rule lower-cases, which only refuses more.
• PG_CATALOG_TYPES has the same stale-list hazard for domains, and is worth its own issue.

AI code assistants

Assisted-by: Claude Code (Claude Opus 5.5)

🤖 Generated with Claude Code

[bvolpato-dd]

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

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