soma.cell

Backup retention — the floor you cannot prune through

On January 31, 2017, a GitLab engineer cleaning up replication lag ran `rm -rf` on what turned out to be the PRIMARY database directory. That was survivable — until all five backup mechanisms turned out to be broken: pg_dump silently producing empty files, S3 uploads failing, snapshots disabled. Six hours of production data were gone forever. Two structural fixes here. First, a backup is only trusted after a restore drill: the lifecycle forces created -> verifying -> verified, and a backup that fails its drill lands in `corrupt`, a TERMINAL state that can never be counted or restored from. Second, the count of verified copies lives behind a memory invariant with a floor of 3: the prune that would leave you with two copies is refused by the MEMORY, not by a retention script somebody edits at 2 a.m.

A Soma program from the devops part of the verified corpus: 102 lines, cells BackupVault, RetentionTests. It passes soma check with soma 3.2.4.

How it is built

The cell BackupVault declares 5 signals in its face: record_backup(b: String) -> Map, drill_pass(b: String) -> Map, drill_fail(b: String) -> Map, prune_one(dataset: String) -> Map and restorable(b: String) -> Bool; keeps 1 memory slot: copies (Map<String, Int>, persistent and consistent) under the invariant copies >= 3 && copies <= 30. Its state machine backup starts in created and allows 3 transitions: created -> verifying, verifying -> verified and verifying -> corrupt. corrupt and verified are terminal. Handlers: record_backup (line 44), drill_pass (line 50), drill_fail (line 56), prune_one (line 62) and restorable (line 71).

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

Generated from soma describe on this file.

The source

backup_retention.cell

// ============================================================================
// BACKUP RETENTION — the floor you cannot prune through
// ============================================================================
//
// On January 31, 2017, a GitLab engineer cleaning up replication lag ran
// `rm -rf` on what turned out to be the PRIMARY database directory. That
// was survivable — until all five backup mechanisms turned out to be
// broken: pg_dump silently producing empty files, S3 uploads failing,
// snapshots disabled. Six hours of production data were gone forever.
//
// Two structural fixes here. First, a backup is only trusted after a
// restore drill: the lifecycle forces created -> verifying -> verified,
// and a backup that fails its drill lands in `corrupt`, a TERMINAL
// state that can never be counted or restored from. Second, the count
// of verified copies lives behind a memory invariant with a floor of 3:
// the prune that would leave you with two copies is refused by the
// MEMORY, not by a retention script somebody edits at 2 a.m.
// ============================================================================

cell BackupVault {
    face {
        signal record_backup(b: String) -> Map
        signal drill_pass(b: String) -> Map
        signal drill_fail(b: String) -> Map
        signal prune_one(dataset: String) -> Map
        signal restorable(b: String) -> Bool
    }

    memory {
        // verified copies per dataset. The floor: never below 3.
        copies: Map<String, Int> [persistent, consistent]
        invariant copies >= 3 && copies <= 30
    }

    // `corrupt` is terminal: a backup that failed its restore drill is
    // dead evidence, never a candidate for "maybe it's fine actually".
    state backup {
        initial: created
        created -> verifying
        verifying -> verified
        verifying -> corrupt
    }

    on record_backup(b: String) {
        let r = try { transition(b, "verifying") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "verifying")
    }

    on drill_pass(b: String) {
        let r = try { transition(b, "verified") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "verified")
    }

    on drill_fail(b: String) {
        let r = try { transition(b, "corrupt") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "corrupt")
    }

    on prune_one(dataset: String) {
        let n = copies.get(dataset) ?? 0
        let w = try { copies.set(dataset, n - 1) }
        if w.error != () {
            return map("ok", false, "reason", "retention floor: pruning to {n - 1} copies refused")
        }
        return map("ok", true, "copies", n - 1)
    }

    on restorable(b: String) {
        return get_status(b) == "verified"
    }
}

cell test RetentionTests {
    rules {
        // a backup is not a backup until the restore drill passes
        assert record_backup("db-0131").ok == true
        assert restorable("db-0131") == false
        // GITLAB'S DISCOVERY: you cannot restore from an unverified file
        assert_fails transition("db-0131", "restored")
        assert drill_pass("db-0131").ok == true
        assert restorable("db-0131") == true

        // a failed drill is terminal — no second opinion revives it
        assert record_backup("db-0201").ok == true
        assert drill_fail("db-0201").ok == true
        assert_fails transition("db-0201", "verified")
        assert_fails transition("db-0201", "verifying")
        assert restorable("db-0201") == false

        // the retention floor: 5 -> 4 -> 3 is fine, 3 -> 2 is refused
        assert copies.set("prod-pg", 5) == ()
        assert prune_one("prod-pg").copies == 4
        assert prune_one("prod-pg").copies == 3
        assert prune_one("prod-pg").ok == false
        assert_fails copies.set("prod-pg", 2)
        assert_fails copies.set("prod-pg", 0)
    }
}

What the toolchain says

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

$ soma check backup_retention.cell
✓ All checks passed.
$ soma test backup_retention.cell
test RetentionTests ...
  ✓ assert record_backup("db-0131").ok == true
  ✓ assert restorable("db-0131") == false
  ✓ assert_fails transition("db-0131", "restored") — raised invalid transition: verifying → restored. Current state: 'verifying'. Valid targets: [verified, corrupt]
  ✓ assert drill_pass("db-0131").ok == true
  ✓ assert restorable("db-0131") == true
  ✓ assert record_backup("db-0201").ok == true
  ✓ assert drill_fail("db-0201").ok == true
  ✓ assert_fails transition("db-0201", "verified") — raised invalid transition: corrupt → verified. Current state: 'corrupt'. Valid targets: []
  ✓ assert_fails transition("db-0201", "verifying") — raised invalid transition: corrupt → verifying. Current state: 'corrupt'. Valid targets: []
  ✓ assert restorable("db-0201") == false
  ✓ assert copies.set("prod-pg", 5) == ()
  ✓ assert prune_one("prod-pg").copies == 4
  ✓ assert prune_one("prod-pg").copies == 3
  ✓ assert prune_one("prod-pg").ok == false
  ✓ assert_fails copies.set("prod-pg", 2) — raised memory invariant violated on 'copies': copies >= 3 && copies <= 30 — rejected write of 2 (key "prod-pg"); the slot is unchanged
  ✓ assert_fails copies.set("prod-pg", 0) — raised memory invariant violated on 'copies': copies >= 3 && copies <= 30 — rejected write of 0 (key "prod-pg"); the slot is unchanged

16 tests: 16 passed, 0 failed
$ soma verify backup_retention.cell
Verifying backup_retention.cell...

State machine 'backup': 4 states, initial 'created'
  States: [corrupt, created, verified, verifying]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'created'
  ✓ terminal states: [verified, corrupt]
  ✓ 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 `record_backup` ⟶ {verifying}
  ✓ refinement: handler `drill_pass` ⟶ {verified}
  ✓ refinement: handler `drill_fail` ⟶ {corrupt}
  · transition sources: `record_backup`, `drill_pass`, `drill_fail` 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)

BackupVault/invariants:

  ✓ invariant copies <= 30 — writer 'prune_one' proven by induction (writes n - 1)
  ⚠ invariant copies >= 3 && copies <= 30 — runtime-checked (computed values): prune_one → copies [copies >= 3] because `n - 1` is only known to lie in [-1, 29] — narrow it: `require (n - 1) >= 3 else …`

11 passed, 1 warnings, 0 failures

  Temporal properties for 'backup':
  ✓ 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/backup_retention.cell · examples/corpus/devops/backup_retention.cell