deployment: a rolling deploy, and the rollback that is not always there

README.md

@@ -55,6 +55,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding
 | [`entitlement-problems/`](entitlement-problems/) | Can a requester approve, a developer edit CloudTrail, a leaver keep admin? | Yes, each through steps that are fine one at a time. writ names who, and through which grants. |
 | [`expense-approval/`](expense-approval/) | Can a large expense be paid without two independent approvals? | Yes, when one person holds both roles: "two signatures" counted boxes, not people. |
 | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. |
+| [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. |
 | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. |
 
 **Design, judgement and change**

deployment/README.md

@@ -0,0 +1,152 @@
+# A rolling deploy, and the rollback that is not always there
+
+Three instances serve production on release r1 against schema v1. The
+release is r2, and r2 comes with a migration to v2 that drops a column r1
+reads. The runbook:
+
+```
+target r2 ──▶ replace a ──▶ a healthy ──▶ replace b ──▶ b healthy ──▶ replace c ──▶ c healthy ──▶ migrate
+                                                                                                    │
+rollback: target r1, then replace back                                     (no way back from here) ◀┘
+```
+
+Each instance is replaced only while the other two are serving (the **health
+gate**). The migration runs when every instance is on r2 and serving. And the
+runbook has a rollback section: point the fleet back at r1 and replace the
+instances again.
+
+The rollback section is true until the migration runs. After that it
+describes a step that cannot happen: r1 cannot read v2, and nothing turns v2
+back into v1. A rollback is a claim about the reachable states, not a button,
+and here the claim stops being true one lawful step into the runbook.
+
+## The model
+
+[`deployment.writ`](deployment.writ) has three instances (`a`, `b`, `c`),
+each with a release (`at`) and a state (`starting`, `healthy`, `down`); the
+fleet's `target`; and the database's schema `at` (`v1`, `v2`).
+
+- `target-r2` starts the release. `roll-back-target` points back at r1, but
+  only while the schema is still v1.
+- `replace-a-with-r2` and the rest take an instance out and start it on the
+  target release. The safe guard is the health gate: the other two instances
+  are `healthy`.
+- `a-passes-health` and the rest: a starting instance becomes healthy only if
+  its release can read the schema (`compatible` in
+  [`deployment.lib.writ`](deployment.lib.writ)). An r1 instance started on v2
+  crash-loops for ever.
+- `a-crashes` and `a-restarts`: the environment. **One instance fails at a
+  time.** A crash is only possible while the other two are serving. Without
+  that fault model, three independent crashes darken production under any
+  rollout, and the question would be about hardware, not the runbook.
+- `migrate`: v1 → v2, once the rollout has finished. There is no inverse.
+
+One law, `no-mismatch`: no r1 instance is serving once the schema is v2.
+
+[`deployment-shortcut.writ`](deployment-shortcut.writ) removes the health gate
+from the replacements: a surge, "to make the deploy faster".
+
+## What writ answers
+
+The questions are in [`deployment.claims`](deployment.claims). The safe plan,
+exit 1:
+
+```
+states: 116   edges: 335
+…
+holds  upgrades
+  "the release can finish: every instance on r2, serving, and the schema migrated"
+holds  never-dark
+  "production is never dark"
+fails  can-roll-back
+  "from every situation, the fleet can still get back to r1, serving"
+  stuck at: #101 (a.at=r2 b.at=r2 c.at=r2 a.state=healthy b.state=healthy c.state=healthy prod.target=r2 db.at=v2)
+  witness:  1. target-r2           → #1   prod.target: r1 → r2
+            2. replace-a-with-r2   → #5   a.at: r1 → r2, a.state: healthy → starting
+            3. a-passes-health     → #12   a.state: starting → healthy
+            4. replace-b-with-r2   → #19   b.at: r1 → r2, b.state: healthy → starting
+            5. b-passes-health     → #43   b.state: starting → healthy
+            6. replace-c-with-r2   → #61   c.at: r1 → r2, c.state: healthy → starting
+            7. c-passes-health     → #85   c.state: starting → healthy
+            8. migrate             → #101   db.at: v1 → v2
+```
+
+The witness is the runbook, done correctly, eight steps. The situation it
+ends in is the one everyone wants, a finished release. From there, r1 can
+never be reached again. The safe plan exits 1 for this, and that is the
+point: the rollout is safe, but the rollback section of the runbook isn't
+always true.
+
+This is not the pair's difference. Both plans fail `can-roll-back` the same
+way. It is a property of having an irreversible migration at all. What to do
+about it is a decision, not a fix: keep r2 for a soak period before
+migrating, so the rollback window is explicit, or make the migration
+reversible (keep the column, copy instead of drop). Either way, the runbook
+should say when its rollback section stops applying.
+
+## Which decisions cannot be taken back
+
+`can-roll-back` names a goal. [`deployment.rules`](deployment.rules) also asks
+without one, using `one-way` from ct.rules: which moves leave a situation that
+can never be reached again?
+
+```sh
+writ derive deployment.writ deployment.rules irreversible
+```
+
+```
+irreversible  (1 row)
+  migrate
+```
+
+Only the migration. Every other step, including the release itself, can be
+undone, so `migrate` is the one step to put behind a human decision. If a
+rollout step appeared here too, the model would have a latch nobody intended.
+
+## The surge
+
+The shortcut, exit 1:
+
+```
+fails  never-dark
+  "production is never dark"
+  witness:  1. target-r2           → #1   prod.target: r1 → r2
+            2. replace-a-with-r2   → #5   a.at: r1 → r2, a.state: healthy → starting
+            3. replace-b-with-r2   → #12   b.at: r1 → r2, b.state: healthy → starting
+            4. replace-c-with-r2   → #29   c.at: r1 → r2, c.state: healthy → starting
+```
+
+Three replacements with no health check between them, and nothing is
+serving. The shortcut still finishes the release (`holds upgrades`), so a
+test that only checks the deploy completes passes it.
+
+## What writ found while this was being written
+
+The first draft of the safe plan let `migrate` run whenever every instance
+was on r2 and healthy. writ's `one-way` table named eleven moves instead of
+one, and the situations behind them told the story:
+
+1. finish the rollout to r2;
+2. decide to roll back: `roll-back-target`, allowed because the schema is
+   still v1;
+3. `migrate` runs anyway, because its guard looked at the instances and not
+   at where the release was heading;
+4. the rollback starts r1 on v2, where it never passes a health check, and
+   the only move left is to go forward again.
+
+That is a migration job racing a rollback decision, which happens when the
+migration is a separate pipeline stage triggered by "all instances on r2".
+The fix, in both files, is that `migrate` also requires the target to still
+be r2. After the fix, `one-way` names `migrate` alone.
+
+## Run it
+
+```sh
+writ check deployment.writ --claims deployment.claims           # exit 1: the rollback
+writ check deployment-shortcut.writ --claims deployment.claims  # exit 1: dark, and the rollback
+writ derive deployment.writ deployment.rules irreversible
+```
+
+`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`.
+`../db-migration-problems/` has the column-level version of the same idiom:
+two releases live at once against one schema.

deployment/deployment-shortcut.writ

@@ -0,0 +1,115 @@
+; The same deploy with ONE CONDITION REMOVED from each replacement: it no
+; longer waits for the rest of the fleet to be serving. A surge, "to make the
+; deploy faster".
+;
+; `writ check` exits 1 on this file, for two reasons: the rollback, as in the
+; original, and production going dark.
+
+(load "stdlib.writ")
+(load "deployment.lib.writ")
+
+(schema deployment
+
+  (type release (r1 r2))
+  (type version (v1 v2))
+  (type yn (no yes))
+
+  ; An instance serves traffic only when healthy. A replaced one is starting
+  ; until its health check passes; a crashed one is down.
+  (type state-t (starting healthy down))
+  (type instance
+    (arrow at    (to release))
+    (arrow state (to state-t)))
+
+  ; The release the rollout is heading for.
+  (type fleet (arrow target (to release)))
+
+  ; The schema, and whether the migration to v2 has run. It drops the column
+  ; r1 reads, so it has no inverse.
+  (type database (arrow at (to version)))
+
+  ; ---- the rules ----
+
+  ; A serving instance can read the schema it runs against: no r1 serving once
+  ; the schema is v2. (A law has one subject, the instance; the database is
+  ; bound with `some`.)
+  (equation no-mismatch
+    (not (and (is instance.state healthy)
+              (is instance.at r1)
+              (some (d database) (is d.at v2))))))
+
+(instance start deployment
+  (instance a (at r1) (state healthy))
+  (instance b (at r1) (state healthy))
+  (instance c (at r1) (state healthy))
+  (fleet prod (target r1))
+  (database db (at v1)))
+
+(use deployment)
+(initial start)
+
+; ---- the release ----
+
+(transition target-r2
+  (when (is prod.target r1))
+  (do (set prod.target r2)))
+
+; The rollback in the runbook: head back to r1. Only while the schema is still
+; one r1 can read.
+(transition roll-back-target
+  (when (and (is prod.target r2) (is db.at v1)))
+  (do (set prod.target r1)))
+
+; The migration, once the rollout is finished: every instance on r2 and
+; serving, AND the release still heading for r2. One way.
+;
+; The last condition is the one the first draft of this file lacked, and writ
+; found it: finish the rollout, decide to roll back, and the migration — whose
+; guard looked only at the instances — runs anyway. The rollback then starts r1
+; against v2, where it never passes a health check. See the README.
+(transition migrate
+  (when (and (is db.at v1) (is prod.target r2) (all-at-healthy r2)))
+  (do (set db.at v2)))
+
+; ---- the rollout ----
+
+; Replace instance I (running FROM) with the target release TO, as soon as
+; it is on the old one. J and K are still passed in; nothing reads them.
+(form (roll N I J K FROM TO)
+  (transition N
+    (when (and (is prod.target TO) (is I.at FROM)))   ; <- the health gate, gone
+    (do (set I.at TO) (set I.state starting))))
+
+(form (pass-health N I)
+  (transition N
+    (when (and (is I.state starting) (compatible I)))
+    (do (set I.state healthy))))
+
+; The environment. One instance fails at a time: a crash is only possible
+; while the other two are serving. This is the fault model, and the README
+; says why it is the honest one for the question.
+(form (crash N I J K)
+  (transition N
+    (when (and (is I.state healthy) (is J.state healthy) (is K.state healthy)))
+    (do (set I.state down))))
+(form (restart N I)
+  (transition N
+    (when (and (is I.state down) (compatible I)))
+    (do (set I.state healthy))))
+
+(roll replace-a-with-r2 a b c r1 r2)
+(roll replace-b-with-r2 b a c r1 r2)
+(roll replace-c-with-r2 c a b r1 r2)
+(roll replace-a-with-r1 a b c r2 r1)
+(roll replace-b-with-r1 b a c r2 r1)
+(roll replace-c-with-r1 c a b r2 r1)
+(pass-health a-passes-health a)
+(pass-health b-passes-health b)
+(pass-health c-passes-health c)
+(crash a-crashes a b c)
+(crash b-crashes b a c)
+(crash c-crashes c a b)
+(restart a-restarts a)
+(restart b-restarts b)
+(restart c-restarts c)
+

deployment/deployment.claims

@@ -0,0 +1,36 @@
+; The questions, put to both plans.
+
+(load "deployment.lib.writ")
+
+(property upgrades
+  "the release can finish: every instance on r2, serving, and the schema migrated"
+  (possible (and (all-at-healthy r2) (is db.at v2))))
+
+(property never-dark
+  "production is never dark"
+  (never none-healthy))
+
+(property can-roll-back
+  "from every situation, the fleet can still get back to r1, serving"
+  (live (all-at-healthy r1)))
+
+; ---- ownership ----
+; Every move that changes a release, a state or the schema is on the route of
+; no-mismatch; the guards are what keep it (r1 is never started on v2, and
+; never passes its health check there).
+(accept migrate no-mismatch)
+(accept replace-a-with-r2 no-mismatch)
+(accept replace-b-with-r2 no-mismatch)
+(accept replace-c-with-r2 no-mismatch)
+(accept replace-a-with-r1 no-mismatch)
+(accept replace-b-with-r1 no-mismatch)
+(accept replace-c-with-r1 no-mismatch)
+(accept a-passes-health no-mismatch)
+(accept b-passes-health no-mismatch)
+(accept c-passes-health no-mismatch)
+(accept a-crashes no-mismatch)
+(accept b-crashes no-mismatch)
+(accept c-crashes no-mismatch)
+(accept a-restarts no-mismatch)
+(accept b-restarts no-mismatch)
+(accept c-restarts no-mismatch)

deployment/deployment.lib.writ

@@ -0,0 +1,16 @@
+; Shared by the models and the questions, because a questions file has its own
+; form scope and there is no implicit prelude.
+(load "stdlib.writ")
+
+; Can instance I's release work against the schema as it is now? r1 knows only
+; v1. r2 was written for the migration: it reads v1 and v2 alike.
+(form (compatible I)
+  (or (and (is I.at r1) (is db.at v1))
+      (is I.at r2)))
+
+(form none-healthy
+  (and (not (is a.state healthy)) (not (is b.state healthy)) (not (is c.state healthy))))
+
+(form (all-at-healthy R)
+  (and (is a.at R) (is b.at R) (is c.at R)
+       (is a.state healthy) (is b.state healthy) (is c.state healthy)))

deployment/deployment.rules

@@ -0,0 +1,25 @@
+; The same three questions, answered a second time by a different part of
+; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is
+; a bug in one of them, not a number to adjust.
+;
+; POLARITY:
+;   `possible F` is the SATISFYING set — non-empty means it holds.
+;   `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds.
+(load "ct.rules")
+(load "deployment.lib.writ")
+
+(satisfies upgrades (and (all-at-healthy r2) (is db.at v2)))
+
+(satisfies never-dark none-healthy)
+
+(satisfies on-r1 (all-at-healthy r1))
+(can-reach can-get-to-r1 on-r1)
+(trapped can-roll-back can-get-to-r1)
+
+; ---- which decisions cannot be taken back ----
+; `one-way` (ct.rules §4) is every edge that leaves its strongly connected
+; component: a move after which the situation it left can never be reached
+; again. Asked with no goal in mind. Projected onto the move's name, which is
+; the column that answers "which step was that".
+(relation irreversible (Edge))
+(rule (irreversible E) (one-way E S T))