soma.cell

Db migration — applied migrations are immutable history

Every schema-drift horror story starts the same way: someone edits a migration that already ran in production. Staging replays the edited file, prod keeps the old shape, and three weeks later a column that "must exist" doesn't. Flyway and Liquibase bolt on checksum errors; here immutability is the machine itself: `applied` is a TERMINAL state `soma verify` proves you cannot leave. Undoing means writing a NEW down-migration, never rewriting the past. The second wall is the migrator lock — the GitLab-style disaster of two operators running migrations concurrently is refused by a memory invariant that admits at most one lock holder.

A Soma program from the devops part of the verified corpus: 104 lines, cells Migrator, MigrationTests. It passes soma check with soma 3.2.4.

How it is built

The cell Migrator declares 5 signals in its face: start_apply(mig: String) -> Map, confirm_applied(mig: String) -> Map, mark_failed(mig: String) -> Map, retry(mig: String) -> Map and migration_state(mig: String) -> String; keeps 1 memory slot: lock_holders (Map<String, Int>, persistent and consistent) under the invariant lock_holders >= 0 && lock_holders <= 1. Its state machine migration starts in pending and allows 4 transitions: pending -> applying, applying -> applied, applying -> failed and failed -> applying. applied is terminal. Handlers: start_apply (line 43), confirm_applied (line 57), mark_failed (line 64), retry (line 71) and migration_state (line 75).

The file also holds 1 test cell (MigrationTests) with 11 assertions, run by soma test.

Generated from soma describe on this file.

The source

db_migration.cell

// ============================================================================
// DB MIGRATION — applied migrations are immutable history
// ============================================================================
//
// Every schema-drift horror story starts the same way: someone edits a
// migration that already ran in production. Staging replays the edited
// file, prod keeps the old shape, and three weeks later a column that
// "must exist" doesn't. Flyway and Liquibase bolt on checksum errors;
// here immutability is the machine itself: `applied` is a TERMINAL
// state `soma verify` proves you cannot leave. Undoing means writing a
// NEW down-migration, never rewriting the past.
//
// The second wall is the migrator lock — the GitLab-style disaster of
// two operators running migrations concurrently is refused by a memory
// invariant that admits at most one lock holder.
// ============================================================================

cell Migrator {
    face {
        signal start_apply(mig: String) -> Map
        signal confirm_applied(mig: String) -> Map
        signal mark_failed(mig: String) -> Map
        signal retry(mig: String) -> Map
        signal migration_state(mig: String) -> String
    }

    memory {
        // 0 = unlocked, 1 = locked. A second concurrent migrator would
        // write 2 — the memory refuses it before any DDL runs.
        lock_holders: Map<String, Int> [persistent, consistent]
        invariant lock_holders >= 0 && lock_holders <= 1
    }

    // `applied` has no exit: production history cannot be rewritten.
    state migration {
        initial: pending
        pending -> applying
        applying -> applied
        applying -> failed
        failed -> applying
    }

    on start_apply(mig: String) {
        let held = lock_holders.get("schema") ?? 0
        let w = try { lock_holders.set("schema", held + 1) }
        if w.error != () {
            return map("ok", false, "reason", "migrator lock is held — refusing concurrent DDL")
        }
        let r = try { transition(mig, "applying") }
        if r.error != () {
            lock_holders.set("schema", held)
            return map("ok", false, "reason", "{r.error}")
        }
        return map("ok", true, "state", "applying")
    }

    on confirm_applied(mig: String) {
        let r = try { transition(mig, "applied") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        lock_holders.set("schema", 0)
        return map("ok", true, "state", "applied")
    }

    on mark_failed(mig: String) {
        let r = try { transition(mig, "failed") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        lock_holders.set("schema", 0)
        return map("ok", true, "state", "failed")
    }

    on retry(mig: String) {
        return start_apply(mig)
    }

    on migration_state(mig: String) {
        return get_status(mig)
    }
}

cell test MigrationTests {
    rules {
        // happy path: pending -> applying -> applied
        assert start_apply("0042_add_orders").ok == true

        // concurrency wall: a second migrator cannot take the lock
        assert start_apply("0043_add_index").ok == false
        assert_fails lock_holders.set("schema", 2)

        assert confirm_applied("0042_add_orders").ok == true

        // THE DRIFT MOVE: re-run or rewrite an applied migration.
        // `applied` is terminal — no edge exists, verify proves it.
        assert_fails transition("0042_add_orders", "applying")
        assert_fails transition("0042_add_orders", "pending")
        assert_fails transition("0042_add_orders", "failed")

        // a failed migration may retry — failure is not terminal
        assert start_apply("0043_add_index").ok == true
        assert mark_failed("0043_add_index").ok == true
        assert retry("0043_add_index").ok == true
        assert confirm_applied("0043_add_index").ok == true
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check db_migration.cell
✓ All checks passed.
$ soma test db_migration.cell
test MigrationTests ...
  ✓ assert start_apply("0042_add_orders").ok == true
  ✓ assert start_apply("0043_add_index").ok == false
  ✓ assert_fails lock_holders.set("schema", 2) — raised memory invariant violated on 'lock_holders': lock_holders >= 0 && lock_holders <= 1 — rejected write of 2 (key "schema"); the slot is unchanged
  ✓ assert confirm_applied("0042_add_orders").ok == true
  ✓ assert_fails transition("0042_add_orders", "applying") — raised invalid transition: applied → applying. Current state: 'applied'. Valid targets: []
  ✓ assert_fails transition("0042_add_orders", "pending") — raised invalid transition: applied → pending. Current state: 'applied'. Valid targets: []
  ✓ assert_fails transition("0042_add_orders", "failed") — raised invalid transition: applied → failed. Current state: 'applied'. Valid targets: []
  ✓ assert start_apply("0043_add_index").ok == true
  ✓ assert mark_failed("0043_add_index").ok == true
  ✓ assert retry("0043_add_index").ok == true
  ✓ assert confirm_applied("0043_add_index").ok == true

11 tests: 11 passed, 0 failed
$ soma verify db_migration.cell
Verifying db_migration.cell...

State machine 'migration': 4 states, initial 'pending'
  States: [applied, applying, failed, pending]

  ✓ 4 states, 4 transitions
  ✓ all states reachable from 'pending'
  ✓ terminal states: [applied]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ✓ refinement: handler `start_apply` ⟶ {applying}
  ✓ refinement: handler `confirm_applied` ⟶ {applied}
  ✓ refinement: handler `mark_failed` ⟶ {failed}
  · transition sources: `start_apply`, `confirm_applied`, `mark_failed` call transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)

Migrator/invariants:

  ✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'confirm_applied' proven (writes 0)
  ✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'mark_failed' proven (writes 0)
  ✓ invariant lock_holders >= 0 — writer 'start_apply' proven by induction (writes held + 1)
  ✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'start_apply' proven by induction (writes held)
  ⚠ invariant lock_holders >= 0 && lock_holders <= 1 — runtime-checked (computed values): start_apply → lock_holders [lock_holders <= 1] because `held + 1` is only known to lie in [1, 2] — narrow it: `require (held + 1) <= 1 else …`

14 passed, 1 warnings, 0 failures

  Temporal properties for 'migration':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, transition

Source file: /corpus/devops/db_migration.cell · examples/corpus/devops/db_migration.cell