docs+lint: safer forms are not semantic equivalents

docs/design-principles.md

@@ -96,9 +96,13 @@ the phased build plan should be traceable back to one of these.
   volatile-default `ADD COLUMN`, `STORED` generated columns, repack). "Needs copy-and-swap? =
   No" never means "don't use the engine" — it means the engine runs the native idiom for you.
 - **Advise, never silently run the dangerous literal; force is loud and explicit.** When a
-  submitted statement is risky as written but has a safer native equivalent (`CREATE INDEX` →
+  submitted statement is risky as written but has a safer native form (`CREATE INDEX` →
   `CREATE INDEX CONCURRENTLY`, etc.), the engine surfaces the recommendation and applies the
-  safe idiom — it does **not** execute the risky literal behind the user's back. Running a
+  safe idiom — it does **not** execute the risky literal behind the user's back. The safer
+  form reaches the same end state but is not a semantic equivalent — it has different locking,
+  transactionality, and failure modes, which is exactly why the engine (not the user) owns
+  running it (see the
+  [online DDL reference](postgres-online-ddl-reference.md)). Running a
   statement exactly as submitted requires an explicit `--force`, gated by prominent DANGER/CAUTION
   output, a typed acknowledgement (not a bare `-y`), and an audit log entry. Force is an escape
   hatch, not a convenience (see

docs/high-level-design.md

@@ -185,7 +185,7 @@ diff algorithm and its safety rules are detailed in the
 ## Advisory mode: suggest the safe rewrite, don't silently run the risky one
 
 The classifier doesn't only choose an execution path — it can also act as a **suggestion
-engine**. When a submitted statement is risky *as written* but has a safer native equivalent,
+engine**. When a submitted statement is risky *as written* but has a safer native form,
 the engine's default is to **return the recommendation and stop**, rather than execute the
 literal statement:
 
@@ -202,7 +202,7 @@ literal statement:
    ┌──────────────────────────────────────────────────────────-┐
    │  RECOMMENDATION (does NOT execute):                       │
    │   you asked:   CREATE INDEX idx ON orders (customer_id)   │
-   │   run instead: CREATE INDEX CONCURRENTLY idx ON orders …  │
+   │   safer form:  CREATE INDEX CONCURRENTLY idx ON orders …  │
    │   why: a plain CREATE INDEX takes SHARE and blocks writes │
    │        for the whole build; CONCURRENTLY does not.        │
    └──────────────────────────────────────────────────────────-┘
@@ -223,10 +223,15 @@ Examples of what it suggests (the same idioms the classifier already knows):
 
 Two principles govern this:
 
-- **Never silently execute the dangerous literal.** If a safer equivalent exists, the engine
+- **Never silently execute the dangerous literal.** If a safer form exists, the engine
   surfaces it rather than running the risky form behind the user's back. This is the
   transparent, review-friendly counterpart to *classify-first* — the user still doesn't need to
-  know the idiom (the engine names it), but nothing dangerous runs unannounced.
+  know the idiom (the engine names it), but nothing dangerous runs unannounced. The safer form
+  is not a semantic equivalent: it reaches the same end state with different locking,
+  transactionality, and failure modes (a failed `CONCURRENTLY` build leaves an `INVALID` index
+  that must be detected and rebuilt — see the
+  [online DDL reference](postgres-online-ddl-reference.md)), which is why the engine owns
+  executing it rather than handing it to the user to run manually.
 - **The planned force route is loud and explicit.** Phase 3 adds a `--force`
   (run-as-submitted) flag for the rare case where the operator genuinely wants the literal
   statement. It will be gated behind

docs/lint-report.md

@@ -67,7 +67,8 @@ codes make the conservatism visible instead of burying it:
 | `code` | string | always | The typed finding kind (see Codes). Automation branches on this, never on prose. |
 | `severity` | string | always | What the engine would do about it (see Severities). |
 | `reason` | string | classifier findings | The planner's typed cause, drawn from the plan report's Reasons vocabulary. Absent for destructive findings, which are a property of the operation, not a routing decision. |
-| `suggestion` | array | when constructible | The ordered safer SQL to run instead, present only for `blocking-idiom` findings where the planner constructed the rewrite. Its absence still means the submitted form blocks — the planner does not construct rewrites for multi-operation statements or for operations that need catalog knowledge (ATTACH PARTITION's proving CHECK). |
+| `suggestion` | array | when constructible | The ordered safer SQL, present only for `blocking-idiom` findings where the planner constructed the rewrite. A safer form of the submitted statement, not a semantic equivalent — running it by hand forgoes the engine's execution-time guards (invalid-index detection after a concurrent build). Its absence still means the submitted form blocks — the planner does not construct rewrites for multi-operation statements or for operations that need catalog knowledge (ATTACH PARTITION's proving CHECK). |
+| `suggestion_execution` | string | with `suggestion` | The typed execution contract for `suggestion`, drawn from the plan report's Execution contracts vocabulary (`autocommit-each-step`: each step in its own implicit transaction, never inside an enclosing transaction block; a failed step leaves partial state the runner must detect and recover). A consumer that runs the suggestion branches on this. Present exactly when `suggestion` is. |
 
 ## Codes (`code`)
 

docs/low-level-design.md

@@ -312,9 +312,13 @@ For each parsed statement the classifier produces a record along the lines of:
 - `original` — the statement as the user wrote it.
 - `class` — `native-safe` · `needs-rewrite` (refused until in-house copy-and-swap lands) ·
   `refuse`.
-- `recommended` — the safe rewrite when the literal is risky but has a native equivalent
+- `recommended` — the safer native form when the literal is risky as written
   (e.g. `CREATE INDEX` → `CREATE INDEX CONCURRENTLY`; `ADD CONSTRAINT` → `ADD … NOT VALID` +
   `VALIDATE`; `ADD PRIMARY KEY` → unique index `CONCURRENTLY` + `ADD PRIMARY KEY USING INDEX`).
+  The recommendation converges on the same declared end state but is **not** a semantic
+  equivalent of the original — it carries different locking, transactionality, and failure
+  modes (a failed `CONCURRENTLY` build leaves an `INVALID` index the executor must detect via
+  `pg_index.indisvalid` and recover), so executing it is the engine's job, not the user's.
 - Richer `risk`, `reversible`, and `requires_app_coordination` metadata is a future extension.
 
 Classification belongs to `pkg/planner`; `pkg/statement` supplies typed operations and

docs/plan-report.md

@@ -54,6 +54,7 @@ with SQL it does not fully understand.
 | `disposition` | string | always | What execution would do with this statement now (see Dispositions). |
 | `decisions` | array | always | The planner's per-operation classifications (below). |
 | `exec_sql` | array | native route | The ordered SQL the native backend would run — the safer sequence when the planner constructed one. Absent for non-native routes. |
+| `execution` | string | with `exec_sql` | The typed execution contract for `exec_sql` (see Execution contracts). A consumer that runs the statements itself branches on this — it is what says the steps must not be wrapped in a transaction block. Present exactly when `exec_sql` is. |
 
 ## Decision fields
 
@@ -64,7 +65,8 @@ with SQL it does not fully understand.
 | `route` | string | always | Where the operation goes (see Routes). |
 | `reason` | string | always | The typed cause of the routing decision (see Reasons). Automation branches on this, never on prose. |
 | `unverified` | bool | when true | The planner failed closed to this route for lack of live facts — the route is what the engine would do, not a proven property of the change. With facts (a live introspection or a supplied column type) the same operation may classify as native. Absent means the decision is proven. |
-| `safer_sql` | array | safer-idiom only | The ordered native sequence to run instead of the submitted form, when the planner could construct it. |
+| `safer_sql` | array | safer-idiom only | The ordered safer native sequence, when the planner could construct it. A safer form of the submitted operation, not a semantic equivalent: it converges on the same declared end state with different locking, transactionality, and failure modes. |
+| `safer_sql_execution` | string | with `safer_sql` | The typed execution contract for `safer_sql` (see Execution contracts). Present exactly when `safer_sql` is. |
 
 ## Closed vocabularies
 
@@ -106,6 +108,12 @@ with SQL it does not fully understand.
 | `native` | Direct PostgreSQL DDL (the safer sequence when one exists). |
 | `copy-and-swap` | Shadow-table copy with checksum-gated cutover. |
 
+### Execution contracts (`execution`, `safer_sql_execution`)
+
+| Value | Meaning |
+|---|---|
+| `autocommit-each-step` | The steps run one at a time, in order, each in its own implicit transaction — never inside an enclosing transaction block. The CONCURRENTLY forms refuse an enclosing block outright, and a multi-step sequence inside one block holds every earlier step's locks across the steps designed to avoid them. A failed step leaves partial state the runner must detect and recover before retrying (a failed CONCURRENTLY build leaves an invalid index, `pg_index.indisvalid = false`). |
+
 ### Dispositions (`disposition`)
 
 | Value | Meaning |
@@ -187,7 +195,8 @@ Both examples are generated by the real classify-and-route pipeline and pinned b
       ],
       "exec_sql": [
         "ALTER TABLE app.orders DROP legacy_status"
-      ]
+      ],
+      "execution": "autocommit-each-step"
     }
   ]
 }
@@ -227,12 +236,14 @@ A desired state that drops an index and adds a column with a constant default:
           "reason": "safer-idiom",
           "safer_sql": [
             "DROP INDEX CONCURRENTLY app.orders_legacy_idx"
-          ]
+          ],
+          "safer_sql_execution": "autocommit-each-step"
         }
       ],
       "exec_sql": [
         "DROP INDEX CONCURRENTLY app.orders_legacy_idx"
-      ]
+      ],
+      "execution": "autocommit-each-step"
     },
     {
       "sql": "ALTER TABLE app.orders ADD COLUMN region text DEFAULT 'emea'",
@@ -251,7 +262,8 @@ A desired state that drops an index and adds a column with a constant default:
       ],
       "exec_sql": [
         "ALTER TABLE app.orders ADD COLUMN region text DEFAULT 'emea'"
-      ]
+      ],
+      "execution": "autocommit-each-step"
     }
   ]
 }

internal/cli/diff.go

@@ -107,7 +107,8 @@ func writeChangeText(out io.Writer, ps plan.Statement) error {
 		return fmt.Errorf("write plan: %w", err)
 	}
 	if len(ps.ExecSQL) > 0 && ps.ExecSQL[0] != ps.SQL {
-		if _, err := fmt.Fprintln(out, "-- the engine would run instead:"); err != nil {
+		if _, err := fmt.Fprintf(out, "-- safer form the engine would run (not equivalent; each step in its own transaction — see %s):\n",
+			onlineDDLReferenceURL); err != nil {
 			return fmt.Errorf("write plan: %w", err)
 		}
 		for _, safer := range ps.ExecSQL {

internal/cli/lint.go

@@ -15,6 +15,11 @@ import (
 // findings, so the process exits non-zero; warnings alone pass.
 var ErrLintFindings = errors.New("lint found errors")
 
+// onlineDDLReferenceURL is where output that recommends a safer form sends
+// the reader. A URL rather than a repo path: an installed build has no
+// docs/ tree, so the reference must be reachable from the string alone.
+const onlineDDLReferenceURL = "https://github.com/block/pg-sprite/blob/main/docs/postgres-online-ddl-reference.md"
+
 // runLint lints a DDL script: parse every statement through the PostgreSQL
 // grammar, classify it with zero live facts, and report typed findings.
 // Offline — no database. A clean script prints nothing.
@@ -67,8 +72,12 @@ func writeLintText(out io.Writer, name string, report lint.Report) error {
 			return fmt.Errorf("write lint report: %w", err)
 		}
 		if len(f.Suggestion) > 0 {
-			if _, err := fmt.Fprintf(out, "  run instead: %s;\n",
-				strings.Join(f.Suggestion, ";\n  ")); err != nil {
+			if _, err := fmt.Fprintf(out, "  safer form (not equivalent — see %s): %s;\n",
+				onlineDDLReferenceURL, strings.Join(f.Suggestion, ";\n  ")); err != nil {
+				return fmt.Errorf("write lint report: %w", err)
+			}
+			if _, err := fmt.Fprintln(out,
+				"  run each statement in its own transaction, never one block; after a failed CONCURRENTLY build, check pg_index.indisvalid and rebuild"); err != nil {
 				return fmt.Errorf("write lint report: %w", err)
 			}
 		}

internal/cli/lint_test.go

@@ -72,6 +72,21 @@ func TestLintTextFindingsCarryPositions(t *testing.T) {
 		out.String())
 }
 
+// The suggestion block must leave an operator who runs the safer form by
+// hand with a reachable reference and the recovery check they take on.
+// This is the renderer's own unit test — everything else asserts typed
+// fields.
+func TestLintTextSuggestionCarriesExecutionCaveat(t *testing.T) {
+	var out strings.Builder
+	cmd := LintCmd{}
+	err := cmd.runLint(strings.NewReader("CREATE INDEX i ON t (c);\n"), &out)
+	require.NoError(t, err)
+	assert.Contains(t, out.String(), onlineDDLReferenceURL,
+		"the reference must be reachable from an installed build, not a repo path")
+	assert.Contains(t, out.String(), "pg_index.indisvalid",
+		"the caveat names the recovery check a manual run takes on")
+}
+
 func TestLintParseFailureIsErrorNotFinding(t *testing.T) {
 	var out strings.Builder
 	cmd := LintCmd{}

pkg/lint/lint.go

@@ -42,7 +42,9 @@ const (
 	CodeUnsupportedOperation Code = "unsupported-operation"
 	// CodeBlockingIdiom: the submitted form blocks readers or writers and
 	// a safer native form exists; Suggestion carries it when the linter
-	// can construct one.
+	// can construct one. The safer form is not a semantic equivalent —
+	// a CONCURRENTLY build is non-transactional and a failure leaves an
+	// invalid index the engine detects and rebuilds at execution time.
 	CodeBlockingIdiom Code = "blocking-idiom"
 	// CodeTableRewrite: the operation needs a full table rewrite — only
 	// the engine's copy-and-swap path can run it online. Reason carries
@@ -85,9 +87,17 @@ type Finding struct {
 	// Reason is the classifier's typed cause, present for findings the
 	// classifier produced (blocking-idiom, table-rewrite, unsupported).
 	Reason planner.Reason `json:"reason,omitempty"`
-	// Suggestion is the ordered safer SQL to run instead, present only
-	// for blocking-idiom findings where the linter could construct it.
+	// Suggestion is the ordered safer SQL, present only for
+	// blocking-idiom findings where the linter could construct it. It is
+	// advisory: a safer form, not a semantic equivalent — running it by
+	// hand forgoes the engine's execution-time guards (invalid-index
+	// detection after a concurrent build).
 	Suggestion []string `json:"suggestion,omitempty"`
+	// SuggestionExecution is the typed execution contract for Suggestion
+	// (planner.Execution), present exactly when Suggestion is. A consumer
+	// that runs the suggestion branches on it — it is what says the steps
+	// must not be wrapped in a transaction block.
+	SuggestionExecution planner.Execution `json:"suggestion_execution,omitempty"`
 }
 
 // Report is the lint result for one script.
@@ -190,7 +200,7 @@ func decisionFinding(d planner.Decision) (Finding, bool) {
 	case planner.RouteNative:
 		if d.Reason == planner.ReasonSaferIdiom {
 			f.Code, f.Severity = CodeBlockingIdiom, SeverityWarning
-			f.Suggestion = d.SaferSQL
+			f.Suggestion, f.SuggestionExecution = d.SaferSQL, d.SaferSQLExecution
 			return f, true
 		}
 		return Finding{}, false

pkg/lint/lint_test.go

@@ -170,7 +170,8 @@ func TestReportJSONShape(t *testing.T) {
 				"code": "blocking-idiom",
 				"severity": "warning",
 				"reason": "safer-idiom",
-				"suggestion": `+string(suggestion)+`
+				"suggestion": `+string(suggestion)+`,
+				"suggestion_execution": "autocommit-each-step"
 			}
 		],
 		"errors": 0,

pkg/plan/docs_test.go

@@ -98,6 +98,9 @@ func TestDocListsEveryVocabularyValue(t *testing.T) {
 	for _, r := range planner.Reasons() {
 		values = append(values, string(r))
 	}
+	for _, e := range planner.Executions() {
+		values = append(values, string(e))
+	}
 	for _, b := range router.Backends() {
 		values = append(values, string(b))
 	}

pkg/plan/plan.go

@@ -73,6 +73,14 @@ type Statement struct {
 	// sequence when the planner constructed one. Empty for non-native
 	// routes.
 	ExecSQL []string `json:"exec_sql,omitempty"`
+	// Execution is the typed execution contract for ExecSQL
+	// (planner.Execution), present exactly when ExecSQL is. A consumer
+	// that runs the statements itself branches on it — it is what says
+	// each step runs in its own implicit transaction, never inside an
+	// enclosing transaction block. It is derived from ExecSQL's presence,
+	// so it is excluded from the fingerprint like the other explanatory
+	// fields.
+	Execution planner.Execution `json:"execution,omitempty"`
 }
 
 // Report is the dry-run plan for one change against one table.
@@ -133,6 +141,9 @@ func FromRouted(rs router.Statement) Statement {
 		Decisions:   rs.Decisions,
 		ExecSQL:     rs.ExecSQL,
 	}
+	if len(st.ExecSQL) > 0 {
+		st.Execution = planner.ExecutionAutocommit
+	}
 	for _, d := range rs.Decisions {
 		if d.Destructive {
 			st.Destructive = true

pkg/plan/plan_test.go

@@ -45,6 +45,8 @@ func TestFromRoutedMapsEveryRoutedField(t *testing.T) {
 	assert.Equal(t, router.DispositionExecute, st.Disposition)
 	assert.Equal(t, rs.Decisions, st.Decisions)
 	assert.Equal(t, rs.ExecSQL, st.ExecSQL)
+	assert.Equal(t, planner.ExecutionAutocommit, st.Execution,
+		"exec_sql carries its execution contract")
 	assert.False(t, st.Destructive, "no destructive decision means a non-destructive statement")
 }
 
@@ -64,8 +66,10 @@ func TestFromRoutedDerivesDestructiveFromDecisions(t *testing.T) {
 		Backend:     router.BackendNative,
 		Disposition: router.DispositionExecute,
 	}
-	assert.True(t, plan.FromRouted(rs).Destructive,
+	st := plan.FromRouted(rs)
+	assert.True(t, st.Destructive,
 		"one destructive decision makes the statement destructive")
+	assert.Empty(t, st.Execution, "no exec_sql means no execution contract")
 }
 
 // The JSON shape is the adapter-facing contract: exact keys, exact
@@ -94,7 +98,8 @@ func TestReportJSONShape(t *testing.T) {
 					Route:       planner.RouteNative,
 					Reason:      planner.ReasonSaferIdiom,
 				}},
-				ExecSQL: []string{"DROP INDEX CONCURRENTLY t_c_idx"},
+				ExecSQL:   []string{"DROP INDEX CONCURRENTLY t_c_idx"},
+				Execution: planner.ExecutionAutocommit,
 			},
 			{
 				SQL:         "ALTER TABLE t NO SUCH THING",
@@ -131,7 +136,8 @@ func TestReportJSONShape(t *testing.T) {
 				"decisions": [
 					{"operation": "drop index", "destructive": true, "route": "native", "reason": "safer-idiom"}
 				],
-				"exec_sql": ["DROP INDEX CONCURRENTLY t_c_idx"]
+				"exec_sql": ["DROP INDEX CONCURRENTLY t_c_idx"],
+				"execution": "autocommit-each-step"
 			},
 			{
 				"sql": "ALTER TABLE t NO SUCH THING",