docs: safer-sequences page (the improve path) + post-#50 clarifications

README.md

@@ -98,6 +98,8 @@ machine-readable shape is in
 `migrate --dry-run` shows exactly what would run, as compiler-style
 diagnostics with a doc anchor per finding (exit 0 — the plan is executable).
 The demo above records the whole flow — dry run, real run, catalog proof;
+why the substituted sequence is safer — same end state, different locking
+— is worked through in [docs/safer-sequences.md](docs/safer-sequences.md);
 the machine-readable shape is in
 [docs/cli-output-examples.md](docs/cli-output-examples.md).
 

docs/README.md

@@ -34,6 +34,7 @@ Aurora-only. Why that combination is the product is [vision.md](vision.md); star
 | [tcb-model.md](tcb-model.md) | The **TCB model** — the trusted-computing-base partition of the engine: which components are the small trusted core that enforces the invariant registry vs the untrusted periphery, the never-trust-callers rule, domain types that make illegal states unrepresentable, the in-TCB engineering rules (from TigerBeetle TIGER_STYLE, s2n-tls, qmail, bitcoin-core), the verification ladder, and the per-side AI-assisted development policy. |
 | [plan-report.md](plan-report.md) | The **plan report contract** — the versioned JSON shape both front doors emit for dry-run plans: fields, closed vocabularies, the fingerprint identity, required consumer behavior for unknown versions/values, and one generated example per source (pinned by test). |
 | [cli-output-examples.md](cli-output-examples.md) | **CLI output examples** — one real, captured JSON output per shape the CLI produces: the plan report for every dry-run disposition (execute, safer-sequence substitution, rewrite-required, backend-unavailable, refusal, destructive), the execution verdict, exit codes, the linter, and diff. |
+| [safer-sequences.md](safer-sequences.md) | **Safer-sequence substitution** (the improve path) — how the planner replaces a native-but-blocking form with the ordered online sequence that reaches the same end state: a worked `ADD CONSTRAINT … UNIQUE` comparison (locking, failure modes, transactionality, cost), what the engine adds over running the idiom by hand, the substitutions made today, and the typed caveats. |
 | [execution-model.md](execution-model.md) | The **execution model** — why safer sequences run autocommit-each-step with no wrapping transaction (PostgreSQL forbids it for the online forms), the **committed prefix** a mid-sequence failure leaves, how the verdict reports the boundary, and the per-sequence partial-failure contracts with their retry paths. Read this to answer "if a multi-step change fails halfway, what state is my table in?" |
 | [capabilities.md](capabilities.md) | The **canonical support matrix** — every operation and object type tiered as supported today / planned (typed refusal now) / out of scope by design, with reasons; how peers draw the same lines differently; why pg-sprite refuses instead of passing through. The one page for "does pg-sprite support X?". |
 | [limitations.md](limitations.md) | The **current limitations** — schema changes pg-sprite refuses today, why they are unsafe or unsupported, and where an operator must act outside the engine. |

docs/execution-model.md

@@ -52,16 +52,25 @@ the sequencing across transaction boundaries *is* the safety mechanism.
 "Implicit or bounded" above is the mechanical detail behind the contract —
 autocommit-each-step has two shapes in the executor:
 
-- **Brief catalog steps and `VALIDATE CONSTRAINT`** each run as one short
-  *explicit* transaction: `BEGIN` → `SET LOCAL lock_timeout` /
-  `statement_timeout` → the statement → `COMMIT` (`pkg/executor`'s bounded
-  runner). The explicit `BEGIN` exists only because the budgets are applied
-  with `SET LOCAL`, which is scoped to that transaction — functionally it is
-  still one statement, one transaction, committed immediately, rolled back
-  atomically on failure.
-- **`CREATE INDEX CONCURRENTLY`** is true autocommit on a dedicated budgeted
-  session: it refuses to run inside any transaction block and internally
-  manages multiple transactions of its own.
+- **Brief catalog steps (step kind `brief`) and `VALIDATE CONSTRAINT` (step
+  kind `validate-constraint`)** each run as one short *explicit* transaction:
+  `BEGIN` → `SET LOCAL lock_timeout` / `statement_timeout` → the statement →
+  `COMMIT` (`pkg/executor`'s bounded runner). The explicit `BEGIN` exists
+  only because the budgets are applied with `SET LOCAL`, which is scoped to
+  that transaction — functionally it is still one statement, one
+  transaction, committed immediately, rolled back atomically on failure.
+- **`CREATE INDEX CONCURRENTLY` (step kind `concurrent-index-build`)** is
+  true autocommit on a dedicated budgeted session: it refuses to run inside
+  any transaction block and internally manages multiple transactions of its
+  own.
+
+Each step's class is the `kind` field of its step report in the JSON
+verdict — the field retry logic branches on. A failed `brief` step means
+something held a lock longer than the brief budget tolerates: retrying is
+reasonable. A failed `validate-constraint` step means the validation scan
+exceeded its own budget: retrying without raising it will fail the same
+way. A failed `concurrent-index-build` carries its own invalid-index
+verdict ([invalid-index-recovery.md](invalid-index-recovery.md)).
 
 ## The committed prefix
 
@@ -70,7 +79,29 @@ shape: steps 1 through N−1 each committed, step N rolled back, steps N+1
 onward never attempted. The leading run of completed steps is the **committed
 prefix** — no holes, no in-limbo steps.
 
-The four-step `SET NOT NULL` sequence, failing at step 3:
+The running example is a single submitted statement:
+
+```sql
+ALTER TABLE users ALTER COLUMN email SET NOT NULL;
+```
+
+Run as-is, PostgreSQL takes `ACCESS EXCLUSIVE` and scans every row to prove no
+NULLs exist — blocking all reads and writes for the whole scan. The planner
+substitutes a four-step native sequence that moves the scan off the exclusive
+lock, exploiting the fact that PostgreSQL (12+) skips the `SET NOT NULL` scan
+when a validated `CHECK` constraint already proves the invariant:
+
+| # | Statement | What it does | Lock (duration) | Budget class |
+|---|---|---|---|---|
+| 1 | `ADD CONSTRAINT … CHECK (email IS NOT NULL) NOT VALID` | Installs the scaffold: enforced for new writes immediately; existing rows not yet checked | `ACCESS EXCLUSIVE` (brief — `NOT VALID` skips the scan) | brief |
+| 2 | `VALIDATE CONSTRAINT …` | Scans the table to prove existing rows satisfy the invariant — the long part | `SHARE UPDATE EXCLUSIVE` (long, but reads and writes continue) | validate (own overall bound) |
+| 3 | `ALTER COLUMN email SET NOT NULL` | The actual change — now a pure catalog flip, because the validated `CHECK` proves the invariant so no scan is needed | `ACCESS EXCLUSIVE` (brief) | brief |
+| 4 | `DROP CONSTRAINT …` (the scaffold) | Removes the now-redundant scaffold constraint | `ACCESS EXCLUSIVE` (brief) | brief |
+
+The exclusive locks are held only for instant catalog flips; the single
+full-table scan runs under a lock that blocks neither reads nor writes.
+
+The same sequence, failing at step 3:
 
 ```diagram
 step 1  ADD CONSTRAINT ... CHECK (col IS NOT NULL) NOT VALID  ── committed ─┐ committed

docs/high-level-design.md

@@ -102,7 +102,11 @@ the planner's classifier:
   almost no parsing logic. This path lives at the `migrate` front door.
 - **Classified planning path (Phases 2.1–2.4).** Parse the statement and introspect the live schema to
   **predict the path up front** — native-safe, needs-rewrite, or refuse — without trial
-  execution. The planner drives `diff` and `migrate --dry-run`, and its classified route drives
+  execution. *Needs-rewrite* refers to a **table rewrite**: PostgreSQL would rebuild the
+  whole table (a full-table copy under `ACCESS EXCLUSIVE`), so executing the change online
+  is the future copy-and-swap executor's job — it does not mean the submitted SQL merely
+  needs rewording (that is the planner's safer-sequence substitution, which stays on the
+  native-safe path). The planner drives `diff` and `migrate --dry-run`, and its classified route drives
   `migrate`'s execution: a blocking submitted form is substituted with the planner's safer
   native sequence instead of incurring a wasted/aborted blind attempt.
 

docs/low-level-design.md

@@ -52,8 +52,11 @@ strategies rather than the whole product:
 
 - **Planner** — parse the change (imperative `--alter` or declarative desired-state diff),
   introspect the live schema, and **classify** every operation as *native-safe*,
-  *needs-rewrite*, or *refuse*. The planner decides **what** must change. It has no idea
-  *how* any executor works.
+  *needs-rewrite*, or *refuse*. *Needs-rewrite* means PostgreSQL would rewrite the
+  **table** — a full-table copy under `ACCESS EXCLUSIVE` — so the change belongs to the
+  copy-and-swap executor (not that the SQL text needs rewording; safer-sequence
+  substitution is a native-safe outcome). The planner decides **what** must change. It has
+  no idea *how* any executor works.
 - **Router** — given the classified plan plus policy and cluster facts (reversibility
   required? app schema-version aware? logical replication available? table shape?), **choose
   the executor** for each change. The router decides **which strategy**, and is the single