feat(preflight): add CheckTableAbsent absence proof

.agents/checks/review.md

@@ -16,7 +16,8 @@ the reviewer's distillation.
 - Core packages: every loop, queue, retry, and wait must be bounded. An unbounded anything in
   a core package is a review-blocking defect.
 - Dangerous APIs accept proof types (`statement.Classified`, `PreflightedTable`,
-  `VerifiedShadow`, `CleanWatermark`, `TableLock`) with package-private constructors — never a
+  `AbsentTarget`, `VerifiedShadow`, `CleanWatermark`, `TableLock`) with package-private
+  constructors — never a
   raw string or bool that a caller could fabricate. Core code re-verifies its own
   preconditions; it never trusts that the planner or CLI checked.
 - Invariant enforcement points carry a `// INV: <id>` comment matching

SAFETY.md

@@ -67,7 +67,8 @@ The short version — the full rules live in [docs/tcb-model.md](docs/tcb-model.
 - **Never trust callers.** Every dangerous operation re-verifies its preconditions, whoever the
   requester is (CLI, planner, orchestrator). The periphery may request; the core enforces.
 - **Domain types make illegal states unrepresentable.** Validating passages return proof types
-  with package-private constructors (today `preflight.PreflightedTable`; later phases add
+  with package-private constructors (today `preflight.PreflightedTable` and
+  `preflight.AbsentTarget`; later phases add
   `VerifiedShadow`, `CleanWatermark`, and `TableLock`); dangerous APIs accept only proof types —
   e.g. the planned cutover swap will accept only a `VerifiedShadow`.
 - **Put a limit on everything.** Every loop bounded, every queue bounded, every retry counted,

docs/capabilities.md

@@ -171,7 +171,7 @@ Status legend: ✅ T1 (supported today) · 🟡 T2 (planned; typed refusal today
 | Unlogged tables | 🟡 | Yes | Typed refusal: persistence is not modeled, converging it (`SET LOGGED`) is a full rewrite, and rendering the table as plain `CREATE TABLE` would silently change crash-safety |
 | Explicit column collations | 🟡 | Yes | Typed refusal: dropping a `COLLATE` clause from a rendered baseline silently changes sort order and index semantics; a collation delta cannot converge without a rewrite |
 | Columns whose default uses a sequence the column does not own | 🟡 | Yes | Typed refusal: in a desired-state model that sequence exists only inside the scratch transaction, so no derived plan can reference it. Column-owned (`serial`-style) sequences are fine |
-| Greenfield `CREATE TABLE` apply (the table does not exist yet — a fresh database or a new table in a live one) | ⚪ | No — owner tooling or a convergence planner | The new table has no readers or writers to protect, but a `REFERENCES` clause takes a brief `SHARE ROW EXCLUSIVE` on each **referenced** table and queues behind long-running queries — run it under a `lock_timeout`. `diff --sql` emits the statement; applying it belongs to owner tooling or a convergence planner, not this engine |
+| Greenfield `CREATE TABLE` apply (the table does not exist yet — a fresh database or a new table in a live one) | 🟡 | Yes — a `REFERENCES` clause takes a brief `SHARE ROW EXCLUSIVE` on each **referenced** live table | Planned as an owned operation. The new table itself has no readers or writers to protect; the online-safety problem is the `REFERENCES` clause, whose lock on each referenced live table queues behind long-running queries and blocks writers behind it — exactly the run-it-under-a-bounded-`lock_timeout` job this engine owns and owner tooling does not do. The absence preflight (`CheckTableAbsent`) is in place; the executor create path and front-door admission build on it. `diff --sql` already emits the statement |
 
 ### Types and non-table objects
 

docs/design-principles.md

@@ -61,6 +61,9 @@ the phased build plan should be traceable back to one of these.
   `max_replication_slots` / `max_wal_senders` headroom, and enough free disk for the shadow copy
   (copy-and-swap roughly **doubles** the table's storage). See
   [low-level-design's preconditions](low-level-design.md#configuration--privilege-preconditions).
+- **Safety primitives land reviewed and dormant.** A proof type and its check can merge with
+  no production caller: the primitive gets its own focused review and full test coverage, and
+  the feature that later consumes it arrives as a smaller, safer diff.
 - **Long migrations must be resumable.** A multi-hour/-day copy must survive process restarts:
   persist a durable checkpoint (`{copied-PK watermark, slot name, confirmed LSN}`) and resume
   with minimal lost work rather than restarting from zero — bounded by slot/WAL retention and,

docs/schemabot-integration.md

@@ -141,6 +141,25 @@ package. Landing this is one of:
   deferred-cutover recovery (Spirit implements it).
 - `engine.Drainer` — `Drain()` to flush in-flight background work on sequential resume.
 
+### Routing the create path's refusals
+
+The planned greenfield `CREATE TABLE` path opens with `preflight.CheckTableAbsent`, and its
+proof has a rule the adapter must respect: an `AbsentTarget` is **minted inside the apply
+session and consumed there** — never serialized into `SchemaChange.Metadata`, carried across
+the plan/apply boundary, or reused across retries. Absence at plan time proves nothing about
+apply time; the executor re-verifies inside the session that runs the `CREATE`, the same way
+ST-7 re-verifies a `PreflightedTable`.
+
+Each refusal from the check maps to a different orchestrator action — route them, don't
+retry them uniformly:
+
+| Refusal | What it means | Orchestrator action |
+| --- | --- | --- |
+| `ErrRelationExists` / `ErrTypeExists` (grouped by `preflight.IsNameOccupied`) | The name is already taken — this is not a create, it's a change to something that exists | Route to the diff/alter path, not to a failure state |
+| `ErrSchemaNotFound` | The qualified schema does not exist on the target | Operator action (create the schema or fix the desired file); retrying cannot succeed |
+| `ErrNoCreationSchema` | Unqualified name and the role's `search_path` yields no creation schema | Caller configuration: schema-qualify the name or fix the role's `search_path` |
+| Duplicate-name error from the `CREATE` itself | A concurrent writer won the race after a valid proof | Re-plan from scratch — the world changed; do not blindly retry the create |
+
 ## Execution-mode verdicts and direct execution
 
 SchemaBot records a per-statement **execution-mode verdict** on each planned `TableChange`:

docs/tcb-model.md

@@ -91,6 +91,7 @@ to obtain the type is through the function that validates it.
 | --- | --- | --- | --- |
 | `string` (user SQL) | `statement.ParseOne` / `statement.ParseOps`, then `planner.Classify` | `planner.Plan` / `planner.Decision` | CO-7 — classification consumes parsed operation descriptors |
 | table name | preflight | `PreflightedTable` (carries the proven facts: PK, no FKs/views, replica identity, headroom) | ST-6, RF-* |
+| table name (create target) | `preflight.CheckTableAbsent` | `AbsentTarget` (carries the resolved creation schema and the verified-free name; time-of-check — minted inside the apply session, never carried across a plan boundary, and re-verified at use the way ST-7 re-verifies `PreflightedTable`) | ST-6 for the create path |
 | shadow table | full checksum pass (planned) | `VerifiedShadow` — its constructor will be private to `pkg/checksum`; the planned `cutover.Swap` will accept **only** this type | CO-1 in the type system |
 | chunker low-watermark | all-checkers-clean pass (planned) | `CleanWatermark` — will be unobtainable in a pass that repaired anything | CO-2 |
 | — | planned table-lock acquisition | `TableLock` token, planned as a required parameter of every mutating operation | LK-1 |

pkg/preflight/absent.go

@@ -0,0 +1,147 @@
+package preflight
+
+import (
+	"context"
+	"errors"
+	"fmt"
+
+	"github.com/jackc/pgx/v5/pgxpool"
+)
+
+// ErrSchemaNotFound is returned when the schema a create would target does
+// not exist. Creating a table cannot fix a missing schema, so the cause is
+// separated from a free name.
+var ErrSchemaNotFound = errors.New("schema not found")
+
+// ErrRelationExists is returned when the target name is already occupied by
+// a relation of any kind — a table, view, index, or sequence all block a
+// CREATE TABLE at that name the same way.
+var ErrRelationExists = errors.New("a relation already exists at the target name")
+
+// ErrTypeExists is returned when the target name is already occupied by a
+// standalone type — an enum, domain, range, or shell type. Every table gets
+// a composite type of the same name, so a CREATE TABLE collides with these
+// exactly as it does with a relation.
+var ErrTypeExists = errors.New("a type already exists at the target name")
+
+// ErrNoCreationSchema is returned when an unqualified check cannot resolve
+// the session's creation schema: the search_path names no usable schema, so
+// there is no schema to verify the absence in. Unlike the other refusals
+// this one is not a database fact — the remedy is entirely on the caller's
+// side: qualify the name, or fix the connection's search_path.
+var ErrNoCreationSchema = errors.New("the session's search_path names no creation schema")
+
+// IsNameOccupied reports whether err means the target name is already held,
+// by a relation or by a standalone type. Both block a CREATE TABLE the same
+// way, so a caller routing "name taken" versus "name free" matches this
+// predicate rather than the two sentinels separately — the sentinels stay
+// distinct for messages, where the difference tells an operator what the
+// obstacle actually is.
+func IsNameOccupied(err error) bool {
+	return errors.Is(err, ErrRelationExists) || errors.Is(err, ErrTypeExists)
+}
+
+// AbsentTarget proves the target name is free: the schema exists and no
+// relation or standalone type occupies schema.table. It can only be
+// constructed by CheckTableAbsent in this package. The schema it carries is
+// always resolved — an unqualified check records the session's creation
+// schema, so the proof names the exact schema a create would land in.
+//
+// The proof is time-of-check and session-scoped: mint it inside the apply,
+// in the same session that will run the CREATE TABLE, and never serialize
+// it or carry it across a plan/apply boundary — an absence verified at plan
+// time proves nothing about apply time. The create path must also re-verify
+// it at the point of use, the way ST-7 does for PreflightedTable: reject a
+// proof whose Table() is empty (the zero value is forgeable by any package),
+// and require the CREATE TABLE statement's schema and table to equal the
+// proof's before executing.
+type AbsentTarget struct {
+	schema string
+	table  string
+}
+
+// Schema returns the resolved schema the absence was verified in. A proof
+// minted by CheckTableAbsent always carries one: an unqualified check
+// resolves the session's creation schema before verifying.
+func (a AbsentTarget) Schema() string { return a.schema }
+
+// Table returns the verified-absent table name.
+func (a AbsentTarget) Table() string { return a.table }
+
+// CheckTableAbsent verifies that schema.table names no existing relation or
+// standalone type, so a CREATE TABLE at that name has nothing to collide
+// with. When schema is empty the session's creation schema
+// (current_schema()) is resolved first — the schema an unqualified CREATE
+// TABLE would land in — and the proof carries it. The facts come from one
+// catalog snapshot read directly from pg_class and pg_type, which are
+// visible regardless of privileges, so a missing grant can never masquerade
+// as absence; whether the role may create in the schema is a separate
+// privilege check, not this fact check. The proof is time-of-check: nothing
+// locks the name, so a concurrent create can still take it before the
+// CREATE TABLE runs — the create path must still treat a duplicate-name
+// error as a collision; the proof turns the common case into a clean
+// refusal, not a guarantee.
+//
+// This check is NOT the complement of CheckTable for an unqualified name:
+// CheckTable resolves across the whole search_path (to_regclass), while
+// this check resolves current_schema() only — the one schema an unqualified
+// CREATE TABLE lands in. A table in a later search_path schema makes both
+// checks succeed for the same arguments: CheckTable finds it, and this
+// check correctly reports the creation schema free. A caller deciding
+// between create and alter on that pairing would create a new table that
+// shadows the one the user meant — so such a caller must pass an explicit
+// schema, where the two checks share one namespace and are true inverses.
+func CheckTableAbsent(ctx context.Context, pool *pgxpool.Pool, schema, table string) (AbsentTarget, error) {
+	if table == "" {
+		return AbsentTarget{}, fmt.Errorf("check absence in schema %q: empty table name", schema)
+	}
+	// One row always comes back: the LEFT JOINs turn "schema missing" and
+	// "name free" into NULL columns instead of absent rows, so the causes
+	// are separated from one snapshot that cannot disagree with itself —
+	// pg_class and pg_type are each unique on (name, namespace), so each
+	// join matches at most once. The two joins are NOT always disjoint:
+	// an index has no pg_type row, so a standalone type can share its
+	// name and both columns come back non-NULL. The relkind-before-typtype
+	// branch order below resolves that double occupant deliberately — the
+	// relation is what blocks a CREATE TABLE, and reporting ErrTypeExists
+	// would send an operator chasing a type that is not the obstacle. The
+	// typrelid = 0 filter keeps ErrTypeExists meaning *standalone* type
+	// (every relation owns the pg_type row of its name), so the branch
+	// order stays a tie-break rather than load-bearing correctness. The
+	// typelem/typarray filter drops autogenerated array types (typelem set,
+	// no array of their own): CREATE TABLE renames those out of the way
+	// rather than colliding.
+	const q = `
+		SELECT s.nspname,
+		       n.nspname IS NOT NULL,
+		       c.relkind::text,
+		       ty.typtype::text
+		FROM (SELECT CASE WHEN $1 = '' THEN current_schema() ELSE $1 END AS nspname) s
+		LEFT JOIN pg_namespace n ON n.nspname = s.nspname
+		LEFT JOIN pg_class c ON c.relnamespace = n.oid AND c.relname = $2
+		LEFT JOIN pg_type ty ON ty.typnamespace = n.oid AND ty.typname = $2
+			AND ty.typrelid = 0 AND (ty.typelem = 0 OR ty.typarray <> 0)`
+	var targetSchema, relkind, typtype *string
+	var schemaExists bool
+	if err := pool.QueryRow(ctx, q, schema, table).Scan(&targetSchema, &schemaExists, &relkind, &typtype); err != nil {
+		return AbsentTarget{}, fmt.Errorf("check absence of %s: %w", qualifiedName(schema, table), err)
+	}
+	if targetSchema == nil {
+		// Only an unqualified check can land here: current_schema() is
+		// NULL when the search_path names no usable schema, so there is
+		// no schema to verify the absence in.
+		return AbsentTarget{}, fmt.Errorf("resolve creation schema for %s: %w", table, ErrNoCreationSchema)
+	}
+	if !schemaExists {
+		return AbsentTarget{}, fmt.Errorf("%w: schema %s does not exist", ErrSchemaNotFound, *targetSchema)
+	}
+	if relkind != nil {
+		return AbsentTarget{}, fmt.Errorf("%w: %s has relkind %q",
+			ErrRelationExists, qualifiedName(*targetSchema, table), *relkind)
+	}
+	if typtype != nil {
+		return AbsentTarget{}, fmt.Errorf("%w: %s has typtype %q",
+			ErrTypeExists, qualifiedName(*targetSchema, table), *typtype)
+	}
+	return AbsentTarget{schema: *targetSchema, table: table}, nil
+}