diff --git a/.agents/checks/review.md b/.agents/checks/review.md index 3968ce3..a032ffa 100644 --- a/.agents/checks/review.md +++ b/.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: ` comment matching diff --git a/SAFETY.md b/SAFETY.md index 83d5f2d..f58d66f 100644 --- a/SAFETY.md +++ b/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, diff --git a/docs/capabilities.md b/docs/capabilities.md index d246de5..f12d86d 100644 --- a/docs/capabilities.md +++ b/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 diff --git a/docs/design-principles.md b/docs/design-principles.md index b15a0e0..eacbebf 100644 --- a/docs/design-principles.md +++ b/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, diff --git a/docs/schemabot-integration.md b/docs/schemabot-integration.md index a97bcfe..b986f22 100644 --- a/docs/schemabot-integration.md +++ b/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`: diff --git a/docs/tcb-model.md b/docs/tcb-model.md index 05a3eaa..ac54fe3 100644 --- a/docs/tcb-model.md +++ b/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 | diff --git a/pkg/preflight/absent.go b/pkg/preflight/absent.go new file mode 100644 index 0000000..4b74dca --- /dev/null +++ b/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 +} diff --git a/pkg/preflight/absent_integration_test.go b/pkg/preflight/absent_integration_test.go new file mode 100644 index 0000000..8def32c --- /dev/null +++ b/pkg/preflight/absent_integration_test.go @@ -0,0 +1,253 @@ +package preflight_test + +import ( + "fmt" + "testing" + + "github.com/jackc/pgx/v5" + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" + + "github.com/block/pg-sprite/internal/testutil" + "github.com/block/pg-sprite/pkg/dbconn" + "github.com/block/pg-sprite/pkg/preflight" +) + +func TestCheckTableAbsentProvesFreeName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + at, err := preflight.CheckTableAbsent(t.Context(), pool, schema, "brand_new") + require.NoError(t, err) + assert.Equal(t, schema, at.Schema()) + assert.Equal(t, "brand_new", at.Table()) +} + +// An unqualified check resolves the schema an unqualified CREATE TABLE +// would land in, so the proof names the exact creation target. +func TestCheckTableAbsentResolvesUnqualifiedName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + + var creationSchema string + require.NoError(t, pool.QueryRow(t.Context(), "SELECT current_schema()").Scan(&creationSchema)) + + at, err := preflight.CheckTableAbsent(t.Context(), pool, "", "brand_new") + require.NoError(t, err) + assert.Equal(t, creationSchema, at.Schema()) + assert.Equal(t, "brand_new", at.Table()) +} + +// Any relation kind occupies the name: a CREATE TABLE collides with a view +// or sequence exactly as it does with a table. taken_idx is a double +// occupant — an index has no pg_type row, so a standalone type shares its +// name — pinning that the relation wins the report: the relation is what +// blocks a CREATE TABLE, and ErrTypeExists would name the wrong obstacle. +func TestCheckTableAbsentRefusesOccupiedName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + for _, ddl := range []string{ + fmt.Sprintf("CREATE TABLE %s.taken_table (id int)", schema), + fmt.Sprintf("CREATE VIEW %s.taken_view AS SELECT 1", schema), + fmt.Sprintf("CREATE SEQUENCE %s.taken_seq", schema), + fmt.Sprintf("CREATE INDEX taken_idx ON %s.taken_table (id)", schema), + fmt.Sprintf("CREATE TYPE %s.taken_idx AS ENUM ('a')", schema), + fmt.Sprintf("CREATE MATERIALIZED VIEW %s.taken_mv AS SELECT 1", schema), + fmt.Sprintf("CREATE TABLE %s.taken_part (id int) PARTITION BY RANGE (id)", schema), + fmt.Sprintf("CREATE TYPE %s.taken_comp AS (x int)", schema), + } { + _, err = pool.Exec(t.Context(), ddl) + require.NoError(t, err) + } + + for _, name := range []string{ + "taken_table", "taken_view", "taken_seq", "taken_idx", "taken_mv", "taken_part", "taken_comp", + } { + _, err := preflight.CheckTableAbsent(t.Context(), pool, schema, name) + assert.ErrorIs(t, err, preflight.ErrRelationExists, "occupied name %s", name) + assert.True(t, preflight.IsNameOccupied(err), "occupied name %s", name) + } +} + +// Standalone types occupy the name too: every table gets a composite type +// of its own name, so an enum, domain, or range at the target collides with +// a CREATE TABLE even though pg_class knows nothing about it. +func TestCheckTableAbsentRefusesOccupiedTypeName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + for _, ddl := range []string{ + fmt.Sprintf("CREATE TYPE %s.taken_enum AS ENUM ('a')", schema), + fmt.Sprintf("CREATE DOMAIN %s.taken_domain AS int", schema), + fmt.Sprintf("CREATE TYPE %s.taken_rg AS RANGE (subtype = int4)", schema), + } { + _, err = pool.Exec(t.Context(), ddl) + require.NoError(t, err) + } + + for _, name := range []string{"taken_enum", "taken_domain", "taken_rg"} { + _, err := preflight.CheckTableAbsent(t.Context(), pool, schema, name) + assert.ErrorIs(t, err, preflight.ErrTypeExists, "occupied type name %s", name) + assert.True(t, preflight.IsNameOccupied(err), "occupied type name %s", name) + + // The refusal matches the server's behavior: the create really + // does collide with the type, so refusing was not a false block. + _, err = pool.Exec(t.Context(), fmt.Sprintf("CREATE TABLE %s.%s (id int)", schema, name)) + assert.Error(t, err, "CREATE TABLE %s should collide with the type", name) + } +} + +// An autogenerated array type does not occupy its name: CREATE TABLE renames +// it out of the way, so the check must not refuse a name that a create +// would in fact win. +func TestCheckTableAbsentIgnoresAutogeneratedArrayType(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + // CREATE TYPE autogenerates the array type _taken_rg alongside taken_rg. + _, err = pool.Exec(t.Context(), fmt.Sprintf("CREATE TYPE %s.taken_rg AS RANGE (subtype = int4)", schema)) + require.NoError(t, err) + + at, err := preflight.CheckTableAbsent(t.Context(), pool, schema, "_taken_rg") + require.NoError(t, err) + assert.Equal(t, "_taken_rg", at.Table()) + + // 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) +} + +// An empty table name names nothing; the check fails closed rather than +// minting a proof for a target no CREATE TABLE could have. +func TestCheckTableAbsentRefusesEmptyTableName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + _, err = preflight.CheckTableAbsent(t.Context(), pool, schema, "") + require.Error(t, err) +} + +// Occupancy is a catalog fact, not a privilege question: a role with no +// grants on the schema still sees the occupant, so a missing grant can +// never masquerade as absence. +func TestCheckTableAbsentSeesOccupantWithoutPrivileges(t *testing.T) { + serverURL := testutil.StartPostgres(t) + admin, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: serverURL}) + require.NoError(t, err) + t.Cleanup(admin.Close) + schema := testutil.NewSchema(t, admin) + + _, err = admin.Exec(t.Context(), fmt.Sprintf("CREATE TABLE %s.hidden_table (id int)", schema)) + require.NoError(t, err) + _, err = admin.Exec(t.Context(), fmt.Sprintf("REVOKE ALL ON SCHEMA %s FROM PUBLIC", schema)) + require.NoError(t, err) + + const password = "absent-test-password" + role := testutil.NewRole(t, admin, "LOGIN PASSWORD '"+password+"'") + pool := connectAs(t, serverURL, role, password) + + _, err = preflight.CheckTableAbsent(t.Context(), pool, schema, "hidden_table") + assert.ErrorIs(t, err, preflight.ErrRelationExists) +} + +func TestCheckTableAbsentMissingSchema(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + + _, err = preflight.CheckTableAbsent(t.Context(), pool, "no_such_schema", "t") + assert.ErrorIs(t, err, preflight.ErrSchemaNotFound) + assert.False(t, preflight.IsNameOccupied(err), + "a missing schema is not an occupied name — the causes route differently") +} + +// The catalog is matched on the exact name, so a mixed-case relation blocks +// only its exact spelling — the lowercase name is genuinely free. +func TestCheckTableAbsentMatchesExactName(t *testing.T) { + pool, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: testutil.StartPostgres(t)}) + require.NoError(t, err) + t.Cleanup(pool.Close) + schema := testutil.NewSchema(t, pool) + + _, err = pool.Exec(t.Context(), fmt.Sprintf(`CREATE TABLE %s."Weird Name" (id int)`, schema)) + require.NoError(t, err) + + _, err = preflight.CheckTableAbsent(t.Context(), pool, schema, "Weird Name") + assert.ErrorIs(t, err, preflight.ErrRelationExists) + + at, err := preflight.CheckTableAbsent(t.Context(), pool, schema, "weird name") + require.NoError(t, err) + assert.Equal(t, "weird name", at.Table()) +} + +// A session whose search_path names no schema has no creation target for an +// unqualified name; the check fails rather than guessing a schema. +func TestCheckTableAbsentRefusesEmptySearchPath(t *testing.T) { + serverURL := testutil.StartPostgres(t) + admin, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: serverURL}) + require.NoError(t, err) + t.Cleanup(admin.Close) + + const password = "absent-test-password" + role := testutil.NewRole(t, admin, "LOGIN PASSWORD '"+password+"'") + _, err = admin.Exec(t.Context(), fmt.Sprintf("ALTER ROLE %s SET search_path = ''", + pgx.Identifier{role}.Sanitize())) + require.NoError(t, err) + + pool := connectAs(t, serverURL, role, password) + _, err = preflight.CheckTableAbsent(t.Context(), pool, "", "t") + assert.ErrorIs(t, err, preflight.ErrNoCreationSchema) + assert.NotErrorIs(t, err, preflight.ErrSchemaNotFound, + "an unresolvable search_path is not a missing schema — there is no schema name to report missing") +} + +// CheckTable and CheckTableAbsent are not inverses for an unqualified name: +// CheckTable resolves across the whole search_path while CheckTableAbsent +// resolves current_schema() only. A table in a later search_path schema +// makes both checks succeed for the same arguments — the documented reason +// a caller deciding between create and alter must qualify the schema. +func TestCheckTableAbsentIsNotComplementOfCheckTable(t *testing.T) { + serverURL := testutil.StartPostgres(t) + admin, err := dbconn.NewPool(t.Context(), dbconn.Config{URL: serverURL}) + require.NoError(t, err) + t.Cleanup(admin.Close) + first := testutil.NewSchema(t, admin) + second := testutil.NewSchema(t, admin) + + _, err = admin.Exec(t.Context(), fmt.Sprintf("CREATE TABLE %s.only_here (id int)", second)) + require.NoError(t, err) + + const password = "absent-test-password" + role := testutil.NewRole(t, admin, "LOGIN PASSWORD '"+password+"'") + _, err = admin.Exec(t.Context(), fmt.Sprintf("GRANT USAGE ON SCHEMA %s, %s TO %s", + first, second, pgx.Identifier{role}.Sanitize())) + require.NoError(t, err) + _, err = admin.Exec(t.Context(), fmt.Sprintf("ALTER ROLE %s SET search_path = %s, %s", + pgx.Identifier{role}.Sanitize(), first, second)) + require.NoError(t, err) + pool := connectAs(t, serverURL, role, password) + + // CheckTable finds the table through the search_path... + pt, err := preflight.CheckTable(t.Context(), pool, "", "only_here", preflight.NoSizeLimit) + require.NoError(t, err) + assert.Equal(t, "only_here", pt.Table()) + + // ...while CheckTableAbsent proves the same name free, because an + // unqualified CREATE TABLE would land in the first schema, not the + // second. Both proofs are true at once. + at, err := preflight.CheckTableAbsent(t.Context(), pool, "", "only_here") + require.NoError(t, err) + assert.Equal(t, first, at.Schema()) +} diff --git a/pkg/preflight/docs_test.go b/pkg/preflight/docs_test.go new file mode 100644 index 0000000..b676067 --- /dev/null +++ b/pkg/preflight/docs_test.go @@ -0,0 +1,34 @@ +package preflight + +import ( + "os" + "testing" + + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" +) + +// proofTypeDocs are the hand-maintained registries of proof types; each one +// must list every proof type this package exports. Three prose lists drift +// independently, so this test pins them the same way pkg/verdict and +// pkg/plan pin their contract pages. +var proofTypeDocs = []string{ + "../../SAFETY.md", + "../../.agents/checks/review.md", + "../../docs/tcb-model.md", +} + +// Every proof type exported by this package must appear in every registry +// document: a new proof type added without updating all three lists fails +// here. Extend the slice when a new proof type lands. +func TestDocsListEveryProofType(t *testing.T) { + proofTypes := []string{"PreflightedTable", "AbsentTarget"} + for _, doc := range proofTypeDocs { + raw, err := os.ReadFile(doc) + require.NoError(t, err) + for _, name := range proofTypes { + assert.Contains(t, string(raw), name, + "%s is missing the proof type %s", doc, name) + } + } +} diff --git a/pkg/preflight/preflight.go b/pkg/preflight/preflight.go index b1f8318..b8675f8 100644 --- a/pkg/preflight/preflight.go +++ b/pkg/preflight/preflight.go @@ -121,6 +121,13 @@ func LookupTargetFacts(ctx context.Context, pool *pgxpool.Pool, schema, table st // exists, is an ordinary or partitioned table, and is at most limitBytes on // disk. Above the limit it returns a *SizeError; on success it returns the // PreflightedTable proof. +// +// The unqualified lookup is search_path-wide (to_regclass), so success does +// not mean the name is occupied in the session's creation schema: a table +// in a later search_path schema satisfies this check while CheckTableAbsent +// — which resolves current_schema() only — still proves the creation schema +// free for the same name. The two checks are inverses only when the caller +// passes an explicit schema. func CheckTable(ctx context.Context, pool *pgxpool.Pool, schema, table string, limitBytes int64) (PreflightedTable, error) { if limitBytes <= 0 { return PreflightedTable{}, fmt.Errorf("size limit must be positive, got %d", limitBytes)