demo: walk a data fault through the tour and prove the abandon left nothing behind

demo/README.md

@@ -16,7 +16,7 @@ The tour walks five sections, each runnable on its own via
 | `diff`    | The declarative front door: a routed convergence plan for an existing table, for a missing one, and a typed create-shape refusal (exit code 2) for a missing table declared `IF NOT EXISTS` | no                  |
 | `pull`    | Existing-database onboarding: export one desired file per demo table, then prove each produces a zero-change `diff` | no                  |
 | `offline` | `lint` (gates on error findings), `suggest` (advises), `fmt` (canonicalizes) — no database                           | no                  |
-| `exec`    | Real executions: a native add, the concurrent index substitution, the four-step `SET NOT NULL` sequence, a genuine type rewrite run through copy-and-swap (`executed-via-copy-and-swap`, exit code 0), a structured refusal (exit code 2) for a rewrite the copy-and-swap engine does not carry yet, and the `--accept-blocking` passthrough: the plain `DROP INDEX` refused, refused again with a mismatched acknowledgement (exit code 1, nothing runs), then committed without online safety (exit code 3) along with a `REINDEX TABLE`, and a `DROP COLUMN` refused as `destructive-change` (exit code 2) until `--allow-destructive` names the table | yes (seeded tables) |
+| `exec`    | Real executions: a native add, the concurrent index substitution, the four-step `SET NOT NULL` sequence, a genuine type rewrite run through copy-and-swap (`executed-via-copy-and-swap`, exit code 0), a data fault — a narrowing one seeded row will not fit, reported as a `failed` verdict coded `data-fault` (exit code 1) after the run abandons itself — proven to leave nothing behind by a second copy-and-swap on the same table, a structured refusal (exit code 2) for a rewrite the copy-and-swap engine does not carry yet, and the `--accept-blocking` passthrough: the plain `DROP INDEX` refused, refused again with a mismatched acknowledgement (exit code 1, nothing runs), then committed without online safety (exit code 3) along with a `REINDEX TABLE`, and a `DROP COLUMN` refused as `destructive-change` (exit code 2) until `--allow-destructive` names the table | yes (seeded tables) |
 
 `make demo` reseeds [seed.sql](seed.sql) first, so every run starts from the
 same state and the tour is rerunnable. The compose database is left running
@@ -36,7 +36,8 @@ reasons, and classes, the `allowed_destructive` audit field, the substituted `ex
 distinguishing fragment, so a regression that drops `CONCURRENTLY` or
 collapses the `SET NOT NULL` sequence turns the job red), statement counts —
 and on exit codes (`0` success, `2` refusal, `3` accepted-blocking commit,
-`1` lint gate and mismatched acknowledgement). The `pull`
+`1` lint gate, mismatched acknowledgement, and the data-fault `failed`
+verdict). The `pull`
 step has no JSON mode, so check mode asserts only its exit code and exported
 file count, then uses each `diff --json` report to assert zero statements. It never
 asserts on human-facing prose, which is free to change. CI runs

demo/seed.sql

@@ -2,6 +2,12 @@
 -- recreates everything, so every `make demo` starts from the same state.
 -- Identity (not serial) keys so the declarative diff never meets a
 -- sequence-backed default it must refuse.
+--
+-- The tables live in public, named explicitly: the compose role shares its
+-- name with the engine's own schema, which a copy-and-swap run creates for
+-- its checkpoint table, and from then on an unqualified CREATE TABLE under
+-- the role's default search_path would land there instead.
+SET search_path = public;
 DROP TABLE IF EXISTS users, orders, widgets CASCADE;
 
 CREATE TABLE users (
@@ -21,13 +27,21 @@ FROM generate_series(1, 10000) g;
 CREATE TABLE orders (
     id      bigint GENERATED BY DEFAULT AS IDENTITY PRIMARY KEY,
     user_id integer,
-    total   numeric(10,2)
+    total   numeric(10,2),
+    note    text
 );
 
-INSERT INTO orders (user_id, total)
-SELECT (g % 10000) + 1, g
+INSERT INTO orders (user_id, total, note)
+SELECT (g % 10000) + 1, g, 'order ' || g
 FROM generate_series(1, 5000) g;
 
+-- One note wider than the varchar(32) the exec tour's data-fault step
+-- narrows the column to. It sits past the copier's first chunks, so the
+-- fault is met after rows have already landed in the shadow and the
+-- abandon has something to discard. Every other note stays well inside
+-- the width, so the later widening to varchar(200) copies cleanly.
+UPDATE orders SET note = repeat('x', 64) WHERE id = 4000;
+
 -- An index the exec tour drops with the plain (blocking) DROP INDEX under
 -- the --accept-blocking acknowledgement. It lives on orders, which no
 -- desired-state file describes, so the diff tour's plans do not see it.

demo/tour.sh

@@ -185,6 +185,32 @@ execute_copy_swap() {
     fi
 }
 
+# execute_data_fault table sql
+#
+# Runs a copy-and-swap change whose statement the seeded data cannot
+# satisfy — one row will not fit the narrowed type — and requires the
+# failed verdict coded data-fault for the table, the operational exit code
+# 1 (not the refusal's 2: the planner accepted the statement; the rows
+# rejected it), and no --force in play. The run abandons itself before it
+# returns, so the next copy-and-swap on the same table finds nothing left
+# behind — no shadow, no replication slot, no checkpoint row — which the
+# row that follows this one in run_exec proves by succeeding.
+execute_data_fault() {
+    local table="$1" sql="$2" out status=0
+    step "execute (copy-and-swap, expect a data fault): $sql"
+    if [ "$CHECK" = 1 ]; then
+        out=$("$PGS" migrate --url "$PG_DSN" --json --free-disk 1GiB --alter "$sql" 2>/dev/null) || status=$?
+        assert_eq "data-fault exit of [$sql]" 1 "$status"
+        assert_eq "outcome of [$sql]" "failed" "$(jq -r '.outcome' <<<"$out")"
+        assert_eq "code of [$sql]" "data-fault" "$(jq -r '.code' <<<"$out")"
+        assert_eq "table of [$sql]" "$table" "$(jq -r '.table' <<<"$out")"
+        assert_eq "forced of [$sql]" false "$(jq -r '.forced // false' <<<"$out")"
+    else
+        "$PGS" migrate --url "$PG_DSN" --free-disk 1GiB --alter "$sql" \
+            || echo "(exit $? — expected 1: a row will not fit the new type; the run abandoned itself and left nothing behind)"
+    fi
+}
+
 # execute_refused reason sql
 #
 # Runs a schema change the engine must refuse and requires the refusal
@@ -480,6 +506,14 @@ run_exec() {
     # retained source is dropped. It runs before the DROP INDEX rows so the
     # swap carries orders_total_idx across for them to drop.
     execute_copy_swap                   "ALTER TABLE orders ALTER COLUMN user_id TYPE bigint"
+    # A data fault: the seed plants one note wider than varchar(32), so the
+    # copy meets a row the narrowed type will not hold part-way through
+    # the table. The run abandons itself and releases everything it held;
+    # the widening that follows is the proof — it runs through
+    # copy-and-swap on the same table, which it could not if a shadow, a
+    # slot, or a checkpoint row had been left behind.
+    execute_data_fault      public.orders   "ALTER TABLE orders ALTER COLUMN note TYPE varchar(32)"
+    execute_copy_swap                       "ALTER TABLE orders ALTER COLUMN note TYPE varchar(200)"
     execute_refused backend-unavailable "ALTER TABLE users ADD COLUMN started timestamptz DEFAULT clock_timestamp()"
     # The plain DROP INDEX is refused (the concurrent drop is the safe
     # idiom); the acknowledgement runs it anyway under budgets. The mismatch
@@ -518,6 +552,7 @@ elif [ "$section" = all ]; then
     echo "Every statement above was classified before anything ran. The"
     echo "executions committed online — where the submitted form would have"
     echo "blocked, pg-sprite ran the safer native sequence instead; a genuine"
-    echo "rewrite went through copy-and-swap — and the changes it cannot yet do"
-    echo "safely were refused before they could hurt."
+    echo "rewrite went through copy-and-swap; one whose rows would not fit the new"
+    echo "type abandoned itself and left nothing behind — and the changes it cannot"
+    echo "yet do safely were refused before they could hurt."
 fi