feat(preflight): add CheckTableAbsent absence proof

[Kiran01bm]

Adds preflight.CheckTableAbsent, a fact-only preflight that proves a table name is unoccupied, producing a new AbsentTarget proof type. Nothing consumes it yet.

Why

CREATE TABLE support needs an inverse of the existing target preflight: instead of proving a table exists and is admissible, the engine must prove the name is free before attempting a create. Bending PreflightedTable — whose contract assumes an existing relation — would weaken both proofs, so absence gets its own check and proof type. This lands first, dormant, so the executor create path and front-door admission can each build on a reviewed foundation.

What

• CheckTableAbsent(ctx, pool, schema, table) → AbsentTarget proof, from one catalog snapshot read directly against pg_class — visible regardless of grants, so a missing privilege can never masquerade as absence (deliberately not to_regclass).
• Separated causes: ErrSchemaNotFound, ErrRelationExists (any relkind occupies the name), and unresolvable search_path; unqualified names resolve via current_schema().
• Privilege checking (USAGE/CREATE on the schema) is explicitly out of scope — this is a fact check; the privilege proof arrives with the executor create path.
• SAFETY.md proof-type registry updated; integration tests cover the absence, occupied-name, and schema-resolution cases.

Before / after

Before                                  After
┌──────────────────────────┐            ┌──────────────────────────┐
│ preflight                │            │ preflight                │
│  CheckTable ─────────────┼──▶         │  CheckTable ─────────────┼──▶ PreflightedTable
│    proves: exists,       │            │    (unchanged)           │      (existing relation)
│    admissible relkind,   │            │                          │
│    size ceiling          │            │  CheckTableAbsent ───────┼──▶ AbsentTarget
│                          │            │    proves: name free,    │      (dormant — consumed
│  (no way to prove a      │            │    schema resolvable     │       by the upcoming
│   name is free)          │            │                          │       create executor)
└──────────────────────────┘            └──────────────────────────┘

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[aparajon]

🤖 Adversarial correctness review, requested by @aparajon and performed by their agent. Reviewed at head 4f6b77c4, in a worktree, against a live PostgreSQL 16 — every claim below was reproduced on the server rather than reasoned about, and the package's own tests were mutation-tested.

No blocking defect. The central design decision — reading pg_class/pg_type directly instead of to_regclass — is not just defensible, it's demonstrably the right call, and I have the transcript to prove it. typrelid = 0 plus the array-type filter is a genuinely subtle piece of catalog work and the array case is even pinned against the server's real behaviour, which is the strongest test in the file.

Four findings. The first is the one I'd act on before the create path builds on this.

#	Finding	Kind
1	CheckTable and CheckTableAbsent resolve unqualified names in different name spaces — both can succeed for the same inputs, so "the inverse" is the wrong model	API hazard
2	The query comment's soundness argument is false for indexes, and the branch ordering actually doing the work is unpinned — two mutants survive	comment / coverage
3	AbsentTarget joins a registry whose guarantee is upheld by ST-7, and the create path has no ST-7 yet	forward-looking
4	ErrTypeExists is asserted against the check's own opinion, not against the server, unlike its neighbour	coverage

---

1. The two checks are not inverses of each other

The body frames this as "an inverse of the existing target preflight", and the signatures encourage that reading — (ctx, pool, schema, table) on both. But for an unqualified name they resolve different things:

• CheckTable("", t) → to_regclass(quote_ident(t)), which walks the entire search_path (plus pg_temp and pg_catalog).
• CheckTableAbsent("", t) → current_schema() only.

Each is correct in isolation, and CheckTableAbsent's choice is the right one — current_schema() is where an unqualified CREATE TABLE actually lands, and the doc comment says exactly that. The hazard is the pairing. On a live server:

search_path = public, z60      (z60.only_here exists, public.only_here does not)

 create_table_lands_in | checktable_resolves_to | checktableabsent_sees
-----------------------+------------------------+-----------------------
 public                | only_here              |                     0

So CheckTable("", "only_here") mints a PreflightedTable and CheckTableAbsent("", "only_here") mints an AbsentTarget, for the same arguments, in the same session. Both proofs are true. Neither is wrong. But a front door written on the natural reading —

if _, err := CheckTableAbsent(ctx, pool, schema, table); err == nil {
    // name is free -> CREATE
} else {
    // name is taken -> ALTER
}

— routes to CREATE and lands a public.only_here that shadows the z60.only_here the user meant to alter. That's a silent wrong-target write, and it's reachable with a perfectly ordinary two-entry search_path.

There's a smaller edge of the same seam in the proof types: PreflightedTable.Schema() returns the raw argument (its doc says "empty when the lookup used the session search_path"), while AbsentTarget.Schema() returns the resolved schema. Two proof types in one package, same accessor name, different meaning — a caller formatting proof.Schema() + "." + proof.Table() gets a qualified name from one and a bare name from the other.

I'd fix this in documentation rather than code, since both behaviours are individually right:

• Say on CheckTableAbsent that it is not the complement of CheckTable for unqualified names, and that a caller who needs a decision between them must qualify the schema.
• Say on CheckTable that its unqualified lookup is search_path-wide, so a success does not mean the name is occupied in the creation schema.
• Ideally add the case above as a test: table in a non-first search_path schema, assert both checks succeed. It documents the asymmetry in a form that can't drift.

2. The query's soundness comment is wrong about indexes, and the real guard is untested

The comment justifies the shape of the joins like this:

At most one occupant matches: pg_class and pg_type are each unique on (name, namespace), and every relation owns the pg_type row of its name, so the typrelid = 0 filter keeps the two joins disjoint.

Indexes have no pg_type row. So a standalone type can share a name with an index, and both joins match at once:

CREATE INDEX dup ON z60.t (id);
CREATE TYPE  z60.dup AS ENUM ('a');

 in_pg_class | standalone_type
-------------+-----------------
           1 |               1

The query still returns exactly one row and still returns the right answer — but for a different reason than the comment gives. What resolves the double occupant is the order of the two if branches, checking relkind before typtype, not the join filter. And that ordering is load-bearing precisely because an index does block a CREATE TABLE while ErrTypeExists would send an operator looking for a type that isn't the obstacle.

Two mutants confirm nothing pins any of this:

Mutation	Result
Drop AND ty.typrelid = 0	survived — redundant given the relkind-first ordering
Swap the branches: check typtype before relkind	survived — nothing exercises a double occupant

taken_idx is already in TestCheckTableAbsentRefusesOccupiedName, so the ingredients are there; it just never has a type sharing its name. Adding that pair to the table kills the second mutant, and correcting the comment to credit the ordering makes the invariant reviewable. (I'd keep typrelid = 0 — it's redundant today but it's what makes ErrTypeExists mean standalone type, and it stops the mutant from mattering if the branches are ever reordered.)

3. AbsentTarget inherits a guarantee that isn't there yet

SAFETY.md and .agents/checks/review.md — both edited here — describe proof types as having "package-private constructors — never a raw string or bool that a caller could fabricate." That claim is literally false for every proof type in the package, because Go's zero value is a legal composite literal anywhere:

$ go run ./cmd/zzprobe60          # a package outside preflight
forged AbsentTarget:     schema="" table=""
forged PreflightedTable: schema="" table="" partitioned=false bytes=0

I'm not reporting this as a live hole, because it isn't one: executeNative re-verifies with

// INV: ST-7 — the executor runs exactly the statement that was gated,
if st.Table() == "" || st.Schema() != pt.Schema() || st.Table() != pt.Table() {

which rejects a zero-valued proof outright, and RunSequence reaches sequenceTargetFacts with empty names and fails there. So the property the safety model actually rests on is ST-7's re-verification at the point of use, not constructor privacy. That's the stronger design and it's already in place — the documents just credit the wrong mechanism.

The reason it's worth saying on this PR: AbsentTarget is being added to that registry while its consumer is still unwritten, so the assumption is easy to inherit without the enforcement. When the create executor lands, it needs the ST-7 equivalent — reject an AbsentTarget whose Table() is empty, and require the CREATE TABLE statement's schema and table to equal the proof's. Worth a line in the doc comment now so the next PR doesn't have to rediscover it.

4. The type-collision refusal isn't checked against the server

TestCheckTableAbsentIgnoresAutogeneratedArrayType is the best test here because it doesn't stop at the check's opinion:

// The proof matches the server's behavior: the create really succeeds.
_, err = pool.Exec(t.Context(), fmt.Sprintf(`CREATE TABLE %s."_taken_rg" (id int)`, schema))
assert.NoError(t, err)

TestCheckTableAbsentRefusesOccupiedTypeName — the case immediately above it — doesn't do the converse, so ErrTypeExists is only ever compared against the code's own belief. It happens to be right; I checked:

CREATE TYPE  z60.myenum AS ENUM ('a');
CREATE TABLE z60.myenum (id int);
ERROR:  type "myenum" already exists
HINT:  A relation has an associated type of the same name, so you must use a name
       that doesn't conflict with any existing type.

ErrTypeExists is a refusal, so the failure mode it guards against is a false one — blocking a create that would have worked. One assert.Error per type, mirroring the array test, closes the loop and makes the whole family symmetric.

---

Out of scope, but this PR is the reason I noticed

The doc comment's rationale for reading the catalog directly is precise and correct:

visible regardless of privileges, so a missing grant can never masquerade as absence

That is exactly right, and it means CheckTable and LookupTargetFacts — which both use to_regclass — have the mirror-image defect today. As a role without USAGE on the schema:

-- qualified:
SELECT to_regclass('z60b.secret');
ERROR:  permission denied for schema z60b

-- unqualified, with z60b on the search_path:
 current_schema | to_regclass_says_absent | really_exists
----------------+-------------------------+---------------
 public         | t                       |             1

-- direct pg_class read (this PR's approach):
 visible
---------
       1

So a missing grant either raises a raw permission denied where a typed refusal belongs, or — worse, because it's silent — produces ErrTableNotFound for a table that plainly exists. The new function establishes the better pattern; the two older ones are now the odd ones out. Not this PR's job, but worth an issue while the reasoning is fresh, since ErrTableNotFound is a refusal an orchestrator will route on.

---

Verified

Mutation battery — five mutants against pkg/preflight/absent.go, run against a live PostgreSQL 16 via PG_DSN:

Mutation	Result
Drop the array-type filter (typelem = 0 OR typarray <> 0)	killed — TestCheckTableAbsentIgnoresAutogeneratedArrayType
Drop the empty-table-name guard	killed — TestCheckTableAbsentRefusesEmptyTableName
Proof carries the raw schema instead of *targetSchema	killed — TestCheckTableAbsentResolvesUnqualifiedName
Drop AND ty.typrelid = 0	survived (finding 2)
Check typtype before relkind	survived (finding 2)

Catalog reasoning, checked on the server rather than assumed:

• The array-type exclusion is right, and for the stated reason. moveArrayTypeName renames an autogenerated array type out of the way, so _taken_rg really is free — the test proves it end to end. The filter's shape (typelem = 0 OR typarray <> 0) also holds up in the other direction: every user-created type and domain gets an array type, so typarray = 0 with typelem <> 0 is effectively only an array type. Fixed-length types with an element (point) are correctly kept.
• Standalone composite types are caught by the relation branch, not the type branch — CREATE TYPE x AS (…) mints a pg_class row with relkind = 'c', so taken_comp landing under ErrRelationExists is correct, not an accident.
• Domains over arrays don't slip through: a domain's typelem is inherited from its base type, but domains get their own array type, so typarray <> 0 keeps them.
• The targetSchema == nil branch really is unreachable for a qualified check — the CASE returns the parameter unchanged, which is never NULL. The comment is accurate.
• ErrSchemaNotFound is unreachable on the unqualified path by construction: current_schema() only ever names a schema that exists. Harmless, and the separate NotErrorIs assertion in TestCheckTableAbsentRefusesEmptySearchPath pins that the two causes stay distinct.
• Temp tables don't confuse the unqualified path. current_schema() doesn't report the temp schema, and an unqualified CREATE TABLE doesn't land there either, so a shadowing pg_temp relation correctly does not count as an occupant.
• Exact-name matching is consistent with the rest of the package, not a new convention: CheckTable uses to_regclass(quote_ident(...)), which also matches the raw string exactly. TestCheckTableAbsentMatchesExactName pins both directions.
• Time-of-check honesty. The doc states plainly that nothing locks the name and the create path must still treat a duplicate-name error as a collision. That's the right contract for a fact check, and it's stated where a caller will read it.

Landing it dormant — a reviewed foundation with no consumer, rather than bundled into the create path — is the right call for a safety-critical package, and the reason this review could be about catalog semantics instead of about executor plumbing.

CI green at this head, 12/12.

Action items

1. Document that CheckTableAbsent is not the complement of CheckTable for unqualified names, on both functions, and add the two-schema search_path case as a test.
2. Correct the query comment — the relkind-first ordering, not the typrelid = 0 filter, is what resolves a double occupant — and add an index-plus-type name pair to TestCheckTableAbsentRefusesOccupiedName.
3. Note on AbsentTarget that the create path must re-verify it (empty table name, and statement target equal to the proof) the way ST-7 does for PreflightedTable.
4. Assert the converse in TestCheckTableAbsentRefusesOccupiedTypeName — the create really does fail — matching the array test.
5. File the to_regclass privilege issue against CheckTable / LookupTargetFacts.

This review was generated by Claude Code (claude-opus-5).

[aparajon]

🤖 Second pass, requested by @aparajon and performed by their agent — two lenses: OSS adoption (does the repo's own story still add up after this?) and orchestrator integration (can an embedder build the create path on this?). Nothing here blocks; the correctness pass is the other comment.

The two lenses meet at the same place they did on #59: a list kept by hand. AbsentTarget was added to SAFETY.md and .agents/checks/review.md and missed in docs/tcb-model.md, which holds the detailed proof-type table. Two docs-tests in this repo already pin exactly this shape.

#	Suggestion	Lens
1	capabilities.md still says greenfield CREATE TABLE is not this engine's job — reconcile it with the roadmap this PR starts	adoption
2	AbsentTarget is missing from docs/tcb-model.md's proof table; pin all three lists by test	both
3	The unresolvable-search_path refusal is the only untyped one, and it's the most operator-actionable	integration
4	Say on the type that the proof must be minted inside the apply, never carried across a plan boundary	integration
5	Give the create path a routing contract, and an occupancy predicate over the two "taken" sentinels	integration

---

Lens 1 — adoption

1. The capabilities page currently argues against this PR's premise. docs/capabilities.md:174 gives greenfield CREATE TABLE a ⚪ with a reasoned position, not a placeholder:

diff --sql emits the statement; applying it belongs to owner tooling or a convergence planner, not this engine

The reasoning behind it is good — the engine exists to protect existing readers and writers, and a table nobody has opened yet has none to protect. This PR's Why says the opposite is now planned: "CREATE TABLE support needs an inverse of the existing target preflight… the executor create path and front-door admission can each build on a reviewed foundation."

That's a scope decision worth stating out loud, because capabilities.md is the page an evaluator reads to decide what pg-sprite is for, and a ⚪ that turns into a ✅ without explanation reads as scope creep rather than a considered change. The honest version is short: what changed, and what the create path buys that owner tooling doesn't (my guess, from the row's own text: the REFERENCES clause's SHARE ROW EXCLUSIVE on referenced tables is a real lock hazard that owner tooling won't put a lock_timeout in front of — which is exactly this engine's job). If that's the argument, it's a good one and it belongs in the row.

2. Three lists, one of them already stale. The proof-type registry is now maintained by hand in three places:

Where	Has AbsentTarget?
SAFETY.md:70	✅ (this PR)
.agents/checks/review.md:19	✅ (this PR)
docs/tcb-model.md:91 — the detailed table, with the invariant each proof encodes	❌

tcb-model.md is the one that actually explains the model — it's where PreflightedTable gets its "carries the proven facts… encodes ST-6, RF-*" row — so it's the one an adopter reads to understand why the pattern works, and it's the one that got missed. That's not a criticism of the author's diligence; it's the predictable outcome of three hand-synced lists, and it happened on the very first PR that had to sync them.

The fix has direct precedent in this repo — pkg/verdict/docs_test.go and pkg/plan/docs_test.go both do it:

for _, name := range []string{"PreflightedTable", "AbsentTarget"} {
    assert.Contains(t, tcbModel, "`"+name+"`",
        "docs/tcb-model.md is missing a proof-type row for %s", name)
}

Better still if the list is derived rather than repeated, but even a hardcoded slice in one test beats three prose lists, because adding the fourth proof type (VerifiedShadow) is a certainty. This is the fourth time I've asked for a table pinned by test in this repo, and it's the cheapest instance yet — three files, one assertion each.

3. Landing it dormant deserves to be a documented practice. A reviewed, unconsumed foundation is why this review could be about typrelid and moveArrayTypeName instead of about executor plumbing, and it's why the array-type edge got a test that checks the server rather than the code's opinion. That discipline is rare and it's a selling point for a safety-critical engine. docs/design-principles.md would be a natural home for it — one line, "safety primitives land reviewed and dormant before the path that consumes them."

Lens 2 — orchestrator integration

4. One of the four refusals has no sentinel, and it's the one that needs operator action. Three causes are typed and matchable; the fourth is not:

Cause	Sentinel
schema missing	ErrSchemaNotFound
name held by a relation	ErrRelationExists
name held by a standalone type	ErrTypeExists
search_path names no schema	— bare fmt.Errorf, no %w

return AbsentTarget{}, fmt.Errorf("resolve creation schema for %s: the session's search_path names no schema", table)

TestCheckTableAbsentRefusesEmptySearchPath even pins that this is not ErrSchemaNotFound — which is right, and shows the distinction is deliberate — but it leaves an orchestrator with nothing positive to match on. And of the four, this is the one whose remedy is unambiguous and entirely on the caller's side: qualify the name, or fix the connection's search_path. Everything else is a database fact; this one is a configuration mistake. An ErrNoCreationSchema sentinel makes it routable, and makes the four causes a closed vocabulary rather than three plus a string.

5. The proof is time-of-check, and an orchestrator's clock is much longer than a function call's. The doc comment is admirably explicit that nothing locks the name and that a concurrent create can still win. For an embedder the sharper statement is where the proof may be held: SchemaBot plans when a PR opens and applies when someone comments — minutes to days later, across process restarts. An AbsentTarget minted at plan time and consulted at apply time isn't stale by a race window, it's stale by a weekend.

So the contract the create path needs is: mint the proof inside the apply, in the same session that runs the CREATE TABLE, and never serialize it. The type helps enforce that already — unexported fields mean it can't round-trip through JSON — but that's an accident of the shape rather than a stated rule, and docs/schemabot-integration.md's contract section is one sentence away from saying it. Worth writing down now, while the create path is still unwritten and the rule is free to adopt.

6. Give the create path its routing table. Same ask as #59, now with a concrete second consumer. The engine knows what each refusal means operationally and no document says it:

Refusal	What an orchestrator should do
ErrRelationExists / ErrTypeExists	not a failure — the declarative path routes to diff/alter, or refuses cleanly
ErrSchemaNotFound	operator action: the schema is a prerequisite the engine won't create
unresolvable search_path (untyped today)	caller configuration — qualify the name
duplicate-name error at CREATE time	lost the race after a valid proof; re-plan, don't retry blindly

The last row is the interesting one, because it's the only case where the same underlying condition arrives through a different door, and it's the one a retry loop will get wrong.

And for the first row specifically: a router asking "is this name taken?" has to match two sentinels, which is the kind of thing that decays into matching one. A three-line predicate in the package settles it and keeps the two causes distinct in messages, where the distinction actually earns its keep:

// IsNameOccupied reports whether err means the target name is already held,
// by a relation or by a standalone type. Both block a CREATE TABLE.
func IsNameOccupied(err error) bool {
    return errors.Is(err, ErrRelationExists) || errors.Is(err, ErrTypeExists)
}

---

Action items

1. Reconcile docs/capabilities.md:174 with the create-path roadmap, and state what changed.
2. Add AbsentTarget to docs/tcb-model.md's proof-type table, and pin all three lists with a docs test in the shape of pkg/verdict/docs_test.go.
3. Give the unresolvable-search_path cause a sentinel so all four refusals are matchable.
4. State in docs/schemabot-integration.md that the proof must be minted inside the apply session and never carried across a plan boundary.
5. Publish the refusal → orchestrator-action table for the create path, and add an IsNameOccupied predicate over the two occupancy sentinels.

This review was generated by Claude Code (claude-opus-5).

[aparajon]

🤖 Approving — no blocking defect. Findings are in the two comments above: the unqualified-name asymmetry with CheckTable is the one worth settling before the create path builds on this.

This review was generated by Claude Code (claude-opus-5).