feat(migrate): drop orphaned ck_* under migrate_destructive

AGENTS.md

@@ -85,6 +85,19 @@ For a single model, every emitter must agree on:
     executes the byte-identical statements. Pinned by
     `tests/test_table_check_rebuild.py`. See ADR-0015 (canonical render vs
     catalog, both through one normalizer) and ADR-0014 (SQLite warn-skip).
+14. **Check leftovers / drops** — the leftover-name decision (which live
+    ferro-owned `ck_*` names a table carries that the model no longer
+    declares) and the rendered DROP are decided by ONE trio of functions:
+    `ferro_ddl_lowering::extra_check_names` /
+    `extra_check_names_warning` / `render_check_drop`. The auto-migrate
+    reconciliation pass consumes them through
+    `ferro_migrate::plan_check_drops` (ops only under
+    `migrate_destructive`; the warning always fires on `migrate_updates`).
+    The Alembic autogenerate comparator consumes them over FFI
+    (`_core._plan_check_drop`) with **no** destructive gate and executes
+    the byte-identical statements. Pinned by
+    `tests/test_table_check_orphans.py`. See ADR-0013 (leftover warning +
+    destructive ladder) and ADR-0014 (SQLite warn-skip).
 
 ### Why this invariant exists
 

crates/ferro-ddl-lowering/src/lib.rs

@@ -949,6 +949,71 @@ fn declared_check_body(model: &ferro_schema_ir::SchemaModel, name: &str) -> Opti
         .map(render_check_body)
 }
 
+/// Live ferro-owned CHECK names the model no longer declares, in live order
+/// (ADR-0013, #345).
+///
+/// Set-difference only: callers pass *already-filtered* ferro-owned names
+/// (`LiveCheck.ferro_owned`, Alembic `ck_*`). This function does not inspect
+/// the prefix — a user-owned name that leaked into `live_ferro_owned_names`
+/// would be reported as extra. Missing names are an add
+/// (`missing_check_names`, #343); same-name body drift is a rebuild
+/// (`drifted_check_names`, #344).
+pub fn extra_check_names(
+    declared_names: &[String],
+    live_ferro_owned_names: &[String],
+) -> Vec<String> {
+    live_ferro_owned_names
+        .iter()
+        .filter(|name| !declared_names.contains(name))
+        .cloned()
+        .collect()
+}
+
+/// The leftover-CHECK warning for one table, or `None` when nothing is extra.
+/// Single-sourced like [`extra_enum_labels_warning`]: callers emit it verbatim,
+/// never re-derive the wording. Names every leftover and points at
+/// `migrate_destructive` / Alembic.
+pub fn extra_check_names_warning(table: &str, extra: &[String]) -> Option<String> {
+    if extra.is_empty() {
+        return None;
+    }
+    let listed: Vec<String> = extra.iter().map(|name| format!("'{name}'")).collect();
+    Some(format!(
+        "Table '{table}' has CHECK constraint(s) {} that the model no longer \
+         declares. Leftover CHECKs keep rejecting rows the model now allows. \
+         They stay in place unless you pass migrate_destructive=True (Postgres) \
+         or drop them with a reviewed Alembic migration.",
+        listed.join(", "),
+    ))
+}
+
+/// Render the DROP for one leftover CHECK constraint (ADR-0013, ADR-0014).
+///
+/// Postgres: one `ALTER TABLE … DROP CONSTRAINT`. SQLite: no statement, a
+/// warning that names the constraint and points at Alembic batch mode — SQLite
+/// cannot drop a table constraint without a full table rebuild.
+pub fn render_check_drop(table: &str, name: &str, dialect: Dialect) -> CheckEmission {
+    match dialect {
+        Dialect::Postgres => CheckEmission {
+            statement: Some(format!(
+                "ALTER TABLE {} DROP CONSTRAINT {}",
+                quote_ident(table),
+                quote_ident(name),
+            )),
+            warning: None,
+        },
+        Dialect::Sqlite => CheckEmission {
+            statement: None,
+            warning: Some(format!(
+                "CHECK constraint '{name}' on table '{table}' is no longer declared, \
+                 and SQLite cannot drop a table constraint in place (it requires a \
+                 full table rebuild). The live constraint remains; use Alembic's \
+                 batch mode to drop it."
+            )),
+        },
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq)]
 enum CheckToken {
     Word(String),
@@ -1784,6 +1849,85 @@ mod tests {
         );
     }
 
+    // Leftover ferro-owned CHECKs (#345; ADR-0013): live name not in the
+    // declared set. extra_check_names is a set-difference only — the
+    // ferro_owned / ck_* filter is the caller's (migrate.rs / Alembic).
+
+    #[test]
+    fn extra_check_names_returns_undeclared_live_names_in_live_order() {
+        let declared = vec![
+            "ck_transfer_at_most_one_outflow".to_string(),
+            "ck_transfer_kind".to_string(),
+        ];
+        let live = vec![
+            "ck_transfer_orphan".to_string(),
+            "ck_transfer_kind".to_string(),
+            "ck_transfer_old".to_string(),
+        ];
+        assert_eq!(
+            extra_check_names(&declared, &live),
+            vec!["ck_transfer_orphan", "ck_transfer_old"]
+        );
+        assert!(extra_check_names(&declared, &declared).is_empty());
+    }
+
+    #[test]
+    fn extra_check_names_is_a_set_difference_only() {
+        let declared = vec!["ck_transfer_kind".to_string()];
+        let live = vec![
+            "ck_transfer_kind".to_string(),
+            "transfer_positive_amount".to_string(),
+        ];
+        assert_eq!(
+            extra_check_names(&declared, &live),
+            vec!["transfer_positive_amount"],
+            "prefix filtering is the caller's; this function does not drop non-ck_* names"
+        );
+        assert!(extra_check_names(&declared, &[]).is_empty());
+    }
+
+    #[test]
+    fn extra_check_names_warning_is_pinned_and_names_every_leftover() {
+        assert_eq!(
+            extra_check_names_warning(
+                "transfer",
+                &[
+                    "ck_transfer_orphan".to_string(),
+                    "ck_transfer_kind".to_string(),
+                ],
+            ),
+            Some(
+                "Table 'transfer' has CHECK constraint(s) 'ck_transfer_orphan', \
+                 'ck_transfer_kind' that the model no longer declares. Leftover \
+                 CHECKs keep rejecting rows the model now allows. They stay in \
+                 place unless you pass migrate_destructive=True (Postgres) or \
+                 drop them with a reviewed Alembic migration."
+                    .to_string()
+            )
+        );
+        assert_eq!(extra_check_names_warning("transfer", &[]), None);
+    }
+
+    #[test]
+    fn render_check_drop_is_one_alter_on_postgres() {
+        let emission = render_check_drop("transfer", "ck_transfer_orphan", Dialect::Postgres);
+        assert_eq!(
+            emission.statement.as_deref(),
+            Some(r#"ALTER TABLE "transfer" DROP CONSTRAINT "ck_transfer_orphan""#)
+        );
+        assert!(emission.warning.is_none());
+    }
+
+    #[test]
+    fn render_check_drop_warns_and_skips_on_sqlite() {
+        let emission = render_check_drop("transfer", "ck_transfer_orphan", Dialect::Sqlite);
+        assert!(emission.statement.is_none(), "ADR-0014: no SQLite ALTER");
+        let warning = emission.warning.expect("SQLite must never skip silently");
+        assert!(warning.contains("ck_transfer_orphan"), "{warning}");
+        assert!(warning.contains("Alembic"), "{warning}");
+        assert!(warning.contains("batch"), "{warning}");
+    }
+
     #[test]
     fn render_check_expr_covers_cmp_in_and_like() {
         use ferro_schema_ir::{CheckCmpOp, CheckExpr, CheckOperand};

crates/ferro-migrate/src/emit.rs

@@ -5,7 +5,8 @@ use ferro_ddl_lowering::{
     self, ResolvedStorage, apply_canonical_type_for, canonical_from_schema_column,
     canonical_to_db_type_token, db_check_constraint_name, fk_action_from_str, fk_action_sql,
     fk_name, literal_default_value, pg_alter_type_target, quote_ident, refused_conversion,
-    refused_conversion_warning, render_check_addition, render_check_rebuild, render_db_check,
+    refused_conversion_warning, render_check_addition, render_check_drop, render_check_rebuild,
+    render_db_check,
     render_pg_enum_create_type, render_table_check_body, resolve_column_storage, single_index_name,
     single_unique_index_name, sqlite_declared_type, sqlite_type_storage_drift,
 };
@@ -788,6 +789,26 @@ pub fn emit_sql_with_ir(
                     result.warnings.push(warning);
                 }
             }
+            MigrationOp::DropCheck { table, name } => {
+                let model = find_model(&new_models, table)?;
+                let still_declared = model.table_checks.iter().any(|check| check.name == *name)
+                    || model.checks.iter().any(|check| check.name == *name);
+                if still_declared {
+                    return Err(EmissionError {
+                        message: format!(
+                            "Check-drop operation for '{name}' on table '{table}' is still \
+                             declared in the model IR"
+                        ),
+                    });
+                }
+                let emission = render_check_drop(table, name, dialect);
+                if let Some(statement) = emission.statement {
+                    result.statements.push(statement);
+                }
+                if let Some(warning) = emission.warning {
+                    result.warnings.push(warning);
+                }
+            }
             MigrationOp::RebuildForeignKey {
                 table,
                 column,

crates/ferro-migrate/src/lib.rs

@@ -7,8 +7,8 @@ mod emit;
 mod order;
 
 use ferro_ddl_lowering::{
-    drifted_check_names, fk_action_from_str, fk_action_sql, fk_name, is_ferro_fk_name,
-    missing_check_names, schema_columns_storage_drift,
+    drifted_check_names, extra_check_names, fk_action_from_str, fk_action_sql, fk_name,
+    is_ferro_fk_name, missing_check_names, schema_columns_storage_drift,
 };
 use ferro_schema_ir::{IrEnvelope, SchemaIrPayload, SchemaModel};
 use std::collections::{BTreeMap, BTreeSet};
@@ -128,6 +128,16 @@ pub enum MigrationOp {
         /// Canonical constraint name (`ck_<table>_<suffix>`).
         name: String,
     },
+    /// A live ferro-owned CHECK the model no longer declares (#345;
+    /// ADR-0013). Planned only under `migrate_destructive`; Alembic
+    /// autogenerate always proposes the drop. The name must *not* still
+    /// be declared — emitting a drop for a declared name is a loud error.
+    DropCheck {
+        /// Owning table.
+        table: String,
+        /// Live constraint name (`ck_<table>_<suffix>`).
+        name: String,
+    },
     /// A live ferro-owned FK whose definition (`on_delete`, target) drifted
     /// from the declared FK on the same column — rebuilt as
     /// `DROP CONSTRAINT` + `ADD CONSTRAINT` where the backend allows it.
@@ -216,7 +226,9 @@ pub fn emit_sql(plan: &MigrationPlan, dialect: Dialect) -> Vec<String> {
                     table, column
                 ));
             }
-            MigrationOp::AddCheck { name, .. } | MigrationOp::RebuildCheck { name, .. } => {
+            MigrationOp::AddCheck { name, .. }
+            | MigrationOp::RebuildCheck { name, .. }
+            | MigrationOp::DropCheck { name, .. } => {
                 sql.push(format!("-- check '{}' handled by emit_sql_with_ir", name));
             }
         }
@@ -335,6 +347,39 @@ pub fn plan_check_rebuilds(
         .collect()
 }
 
+/// Plan the [`MigrationOp::DropCheck`] operations for one table (#345;
+/// ADR-0013): every live ferro-owned CHECK name the model no longer
+/// declares, in live order.
+///
+/// Callers append the result **after** [`plan_check_rebuilds`]. The
+/// `live_ferro_owned_names` slice is already filtered (`ferro_owned`);
+/// [`extra_check_names`] is a set-difference only. Connect-time callers
+/// gate the ops on `migrate_destructive`; the warning for leftovers is
+/// planned separately so a non-destructive retain-filter cannot swallow it.
+pub fn plan_check_drops(
+    table: &str,
+    new_ir: &IrEnvelope<SchemaIrPayload>,
+    live_ferro_owned_names: &[String],
+) -> Vec<MigrationOp> {
+    let new_models = index_models(&new_ir.payload.models);
+    let Some(new_model) = new_models.get(table) else {
+        return Vec::new();
+    };
+    let declared: Vec<String> = new_model
+        .table_checks
+        .iter()
+        .map(|check| check.name.clone())
+        .chain(new_model.checks.iter().map(|check| check.name.clone()))
+        .collect();
+    extra_check_names(&declared, live_ferro_owned_names)
+        .into_iter()
+        .map(|name| MigrationOp::DropCheck {
+            table: table.to_string(),
+            name,
+        })
+        .collect()
+}
+
 fn index_models<'a>(models: &'a [SchemaModel]) -> BTreeMap<String, &'a SchemaModel> {
     let mut indexed = BTreeMap::new();
     for model in models {

crates/ferro-migrate/src/tests.rs

@@ -1768,6 +1768,94 @@ fn emit_sql_with_ir_rebuild_check_fails_loudly_for_an_undeclared_name() {
     assert!(err.message.contains("ck_transfer_nope"), "{}", err.message);
 }
 
+// ---------------------------------------------------------------------------
+// Leftover ferro-owned CHECKs (#345; ADR-0013): live name gone from the model.
+// Planned after rebuilds. User-owned names never enter live_ferro_owned_names.
+// ---------------------------------------------------------------------------
+
+#[test]
+fn plan_check_drops_plans_live_ferro_owned_names_the_model_does_not_declare() {
+    let new_ir = envelope(vec![transfer_model_with_table_checks(vec![
+        transfer_outflow_table_check(),
+    ])]);
+    let live = vec![
+        "ck_transfer_orphan".to_string(),
+        "ck_transfer_at_most_one_outflow".to_string(),
+        "ck_transfer_old".to_string(),
+    ];
+    assert_eq!(
+        plan_check_drops("transfer", &new_ir, &live),
+        vec![
+            MigrationOp::DropCheck {
+                table: "transfer".to_string(),
+                name: "ck_transfer_orphan".to_string(),
+            },
+            MigrationOp::DropCheck {
+                table: "transfer".to_string(),
+                name: "ck_transfer_old".to_string(),
+            },
+        ]
+    );
+}
+
+#[test]
+fn plan_check_drops_is_a_noop_when_every_live_name_is_declared() {
+    let new_ir = envelope(vec![transfer_model_with_table_checks(vec![
+        transfer_outflow_table_check(),
+    ])]);
+    let live = vec!["ck_transfer_at_most_one_outflow".to_string()];
+    assert!(plan_check_drops("transfer", &new_ir, &live).is_empty());
+}
+
+#[test]
+fn emit_sql_with_ir_drop_check_drops_on_postgres_and_warns_on_sqlite() {
+    let new_ir = envelope(vec![transfer_model_with_table_checks(vec![])]);
+    let plan = MigrationPlan {
+        operations: vec![MigrationOp::DropCheck {
+            table: "transfer".to_string(),
+            name: "ck_transfer_orphan".to_string(),
+        }],
+        warnings: Vec::new(),
+    };
+
+    let pg = emit_sql_with_ir(&plan, &live_transfer_ir(), &new_ir, Dialect::Postgres).unwrap();
+    assert_eq!(
+        pg.statements,
+        vec![r#"ALTER TABLE "transfer" DROP CONSTRAINT "ck_transfer_orphan""#.to_string()]
+    );
+    assert!(pg.warnings.is_empty(), "{:?}", pg.warnings);
+
+    let lite = emit_sql_with_ir(&plan, &live_transfer_ir(), &new_ir, Dialect::Sqlite).unwrap();
+    assert!(lite.statements.is_empty(), "{:?}", lite.statements);
+    assert_eq!(lite.warnings.len(), 1);
+    assert!(
+        lite.warnings[0].contains("ck_transfer_orphan"),
+        "{}",
+        lite.warnings[0]
+    );
+    assert!(lite.warnings[0].contains("Alembic"), "{}", lite.warnings[0]);
+}
+
+#[test]
+fn emit_sql_with_ir_drop_check_fails_loudly_for_a_still_declared_name() {
+    let new_ir = envelope(vec![transfer_model_with_table_checks(vec![
+        transfer_outflow_table_check(),
+    ])]);
+    let plan = MigrationPlan {
+        operations: vec![MigrationOp::DropCheck {
+            table: "transfer".to_string(),
+            name: "ck_transfer_at_most_one_outflow".to_string(),
+        }],
+        warnings: Vec::new(),
+    };
+    let err = emit_sql_with_ir(&plan, &live_transfer_ir(), &new_ir, Dialect::Postgres).unwrap_err();
+    assert!(
+        err.message.contains("ck_transfer_at_most_one_outflow"),
+        "{}",
+        err.message
+    );
+}
+
 #[test]
 fn render_check_body_quotes_column_and_joins_values() {
     let check = SchemaCheck {