From 7fa791a90b4df89f4f3073ef509c26af78e9cf91 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:27:49 +0300 Subject: [PATCH] deployment: a rolling deploy, and the rollback that is not always there Three instances rolled r1 -> r2 behind a health gate, then a one-way migration. The safe plan fails can-roll-back: the runbook done right, eight steps, ends where r1 is unreachable for good; ct.rules one-way names `migrate` and nothing else. The shortcut drops the health gate and goes dark in four steps. Writing it, writ found a race in the first draft: finish the rollout, decide to roll back, and the migration (guarded on the instances only) runs anyway; the rollback then starts r1 on v2. migrate now also requires target r2. Cross-check 49 -> 52 properties (50 compared); 301 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + deployment/README.md | 152 ++++++++++++++++++++++++++++ deployment/deployment-shortcut.writ | 115 +++++++++++++++++++++ deployment/deployment.claims | 36 +++++++ deployment/deployment.lib.writ | 16 +++ deployment/deployment.rules | 25 +++++ deployment/deployment.writ | 119 ++++++++++++++++++++++ docker-compose.yml | 6 ++ modality-cross-check.sh | 2 +- run-tests.sh | 52 ++++++++-- 10 files changed, 513 insertions(+), 11 deletions(-) create mode 100644 deployment/README.md create mode 100644 deployment/deployment-shortcut.writ create mode 100644 deployment/deployment.claims create mode 100644 deployment/deployment.lib.writ create mode 100644 deployment/deployment.rules create mode 100644 deployment/deployment.writ diff --git a/README.md b/README.md index 40bceb6..aabf38c 100644 --- a/README.md +++ b/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** diff --git a/deployment/README.md b/deployment/README.md new file mode 100644 index 0000000..e9b58e6 --- /dev/null +++ b/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. diff --git a/deployment/deployment-shortcut.writ b/deployment/deployment-shortcut.writ new file mode 100644 index 0000000..98a5947 --- /dev/null +++ b/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) + diff --git a/deployment/deployment.claims b/deployment/deployment.claims new file mode 100644 index 0000000..889d5ce --- /dev/null +++ b/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) diff --git a/deployment/deployment.lib.writ b/deployment/deployment.lib.writ new file mode 100644 index 0000000..05c471c --- /dev/null +++ b/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))) diff --git a/deployment/deployment.rules b/deployment/deployment.rules new file mode 100644 index 0000000..b4fbe93 --- /dev/null +++ b/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)) diff --git a/deployment/deployment.writ b/deployment/deployment.writ new file mode 100644 index 0000000..81d6c12 --- /dev/null +++ b/deployment/deployment.writ @@ -0,0 +1,119 @@ +; A rolling deploy behind a health gate, over a migration that cannot be undone. +; +; Three instances serve production on release r1 against schema v1. The +; rollout replaces them one at a time with r2, and only replaces the next once +; the others are serving. When every instance runs r2, the migration to v2 runs. +; The runbook's rollback heads the fleet back to r1. +; +; `writ check` exits 1 on this file: not for the rollout, which is safe, but +; for the rollback, which is not always there. See the README. + +(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. The health +; gate: the other two instances, J and K, are serving while I is out. +(form (roll N I J K FROM TO) + (transition N + (when (and (is prod.target TO) (is I.at FROM) + (is J.state healthy) (is K.state healthy))) + (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) + diff --git a/docker-compose.yml b/docker-compose.yml index 2734486..8488cdc 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -89,6 +89,12 @@ services: image: writ-problems command: ["agent_guardrails"] + # A rolling deploy: the health gate, and the rollback a migration removes. + deployment: + build: . + image: writ-problems + command: ["deployment"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/modality-cross-check.sh b/modality-cross-check.sh index 35a7e8e..88c96aa 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index ee66488..24f0937 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The eighteen scenarios this script walks by convention, and their 49 + # The nineteen scenarios this script walks by convention, and their 52 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the eighteen fails this line, which is the point of it — + # property to any of the nineteen fails this line, which is the point of it — # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, # 26 -> 31 with two-phase-commit, 31 -> 41 with the three # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and - # 45 -> 49 with agent-guardrails, and this line is where each of those had to - # be said out loud. - has "cross-check: all 49 properties of the eighteen scenarios were considered" \ - "$out" "considered 49 properties: 47 compared, 2 not compared" - # Two of the 49 are not compared, and the count above is the only place that + # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, and this line is + # where each of those had to be said out loud. + has "cross-check: all 52 properties of the nineteen scenarios were considered" \ + "$out" "considered 52 properties: 50 compared, 2 not compared" + # Two of the 52 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +459,9 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval and agent-guardrails one each. + # expense-approval, agent-guardrails and deployment one each. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 9 properties compared" + "never: 10 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -778,9 +778,41 @@ agent_guardrails() { has "agent-guardrails: H. derive lists the tool and the mode" "$dv" "6 web-fetch auto" } +deployment() { + d="$here/deployment" + c="$d/deployment.claims" + echo "== A rolling deploy — and the rollback that is not always there ==" + echo " Q: is production ever dark, and can the fleet always roll back?" + out=$("$WRIT" check "$d/deployment.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + # Exit 1 on the SAFE plan, and that is the finding: the rollout is fine, the + # rollback is a promise one lawful move breaks. + exit_is "deployment: even the gated rollout reports a finding" "$st" 1 + has "deployment: A. the release can finish" "$out" "holds upgrades" + has "deployment: B. production is never dark" "$out" "holds never-dark" + has "deployment: C. but rollback is not always possible" "$out" "fails can-roll-back" + has "deployment: stuck once the schema is v2" "$out" "prod.target=r2 db.at=v2)" + has "deployment: and the last step there is the migration" "$out" "8. migrate" + lacks "deployment: no law is broken on the way" "$out" "violated in" + + sc=$("$WRIT" check "$d/deployment-shortcut.writ" --claims "$c" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "deployment: the ungated rollout is refused" "$sst" 1 + has "deployment: D. without the health gate, production goes dark" "$sc" "fails never-dark" + near "deployment: three replacements, no health check between" "$sc" "fails never-dark" "4. replace-c-with-r2" + + # Asked with no goal in mind: which moves can never be taken back? The + # migration, and nothing else — a rollout move here would be a latch. + dv=$("$WRIT" derive "$d/deployment.writ" "$d/deployment.rules" irreversible 2>&1) + has "deployment: E. exactly one decision cannot be taken back" "$dv" "irreversible (1 row)" + has "deployment: the migration" "$dv" " migrate" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):"