diff --git a/db-migration-problems/README.md b/db-migration-problems/README.md index 8add075..c9f4b50 100644 --- a/db-migration-problems/README.md +++ b/db-migration-problems/README.md @@ -1,28 +1,42 @@ # Database migration problems -Three schema changes that look routine, each with a plan that reads correctly +Six schema changes that look routine, each with a plan that reads correctly and goes wrong anyway, mid-rollout. Each directory writes the expand/contract plan down as a writ model and checks it at every instant, including while two releases serve traffic at once. The safe plan passes. A "shortcut" with one -condition removed fails, and writ names the broken rule and the shortest route -to it. +condition removed or weakened fails, and writ names the broken rule and the +shortest route to it. | problem | the mistake | route to the fault | | --- | --- | --- | | [`drop-a-column/`](drop-a-column/) | dropping a column while a release that reads it is still live | 2 moves | +| [`add-a-foreign-key/`](add-a-foreign-key/) | adding the key `NOT VALID` while the old code still makes orphans | 2 moves | | [`add-a-required-column/`](add-a-required-column/) | adding `NOT NULL` before every live release writes the column | 3 moves | +| [`change-an-enum/`](change-an-enum/) | writing the new value while a release that cannot read it is live | 3 moves | | [`rename-a-column/`](rename-a-column/) | switching readers to the new column before the backfill finishes | 4 moves | +| [`split-a-table/`](split-a-table/) | switching reads to the new table once the backfill has *started* | 5 moves | Start with `drop-a-column/`, the smallest. Each directory holds the SQL for each step (with one representative row), the safe plan, the shortcut, one `.claims` file asked of both, and a `.rules` file that answers the same questions through `writ derive` as a cross-check (`../modality-cross-check.sh`). -What the three share: the shortcut is always shorter, because the removed -condition is always a wait. It still completes and never gets stuck, so every -question except "is it safe on the way" answers in its favour. And in most of -them every SQL file is correct on its own; the mistake is in the order, which -no single file records. +What all six share: + +- **The mistake is in the order, not in a file.** Every SQL file is a valid + schema, and in most of them every statement is right. The defect is a step + allowed to start before another has finished, which no single file records. +- **The shortcut still completes and never gets stuck**, so every question + except "is it safe on the way" answers in its favour. +- **It is never slower.** The removed condition is always a wait. Measured as + the shortest route to a finished migration, the shortcut is shorter in two + of the six (`add-a-required-column`, 3 moves against 5; `rename-a-column`, + 8 against 9) and the same length in the other four. There it does not skip + a step: it allows the steps in an order the safe plan forbids. +- **`writ compare` is the wrong gate.** Both files of each pair declare the + same rules and ask the same questions, so compare reports everything + preserved. The shortcut breaks a rule rather than dropping one, and that is + what `check` finds. From any of the directories (here, `drop-a-column/`): @@ -35,3 +49,10 @@ To adapt one to your own migration, change the columns, what each release reads and writes (taken from the code, not the plan), and the steps' `when` conditions. The rules are about columns and releases in general and usually carry over unchanged. + +What `writ sql` does with the newer steps is recorded where it matters: +`CHECK … IN` becomes an enumerated type (`change-an-enum/`), `REFERENCES` +becomes an arrow (`split-a-table/`), and `NOT VALID` is read as an ordinary +foreign key while `VALIDATE CONSTRAINT` is declined (`add-a-foreign-key/`). +A constraint's validation state is not part of a schema, so the models carry +it themselves. diff --git a/db-migration-problems/add-a-foreign-key/01-before.sql b/db-migration-problems/add-a-foreign-key/01-before.sql new file mode 100644 index 0000000..3e3e554 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/01-before.sql @@ -0,0 +1,19 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- orders.customer_id points at a customer, but nothing says so: there is no +-- foreign key. So the data has drifted. The code deployed today deletes a +-- customer without touching their orders, and order o2 below belongs to a +-- customer who no longer exists — an ORPHAN. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL +); + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); +INSERT INTO orders (id, customer_id) VALUES ('o2', 'c9'); diff --git a/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql b/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql new file mode 100644 index 0000000..33a9fca --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql @@ -0,0 +1,26 @@ +-- STEP 1 — the constraint arrives, NOT VALID. +-- +-- A plain ADD CONSTRAINT … FOREIGN KEY scans the whole table under a lock, +-- and fails if any row is an orphan. NOT VALID skips the scan: rows already +-- there are not checked, but every INSERT, UPDATE and DELETE from now on is. +-- That last part is easy to miss, and it is the one that matters: the release +-- still running deletes customers without touching their orders, and from +-- this moment the database refuses those deletes. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL +); + +ALTER TABLE orders + ADD CONSTRAINT orders_customer_fk + FOREIGN KEY (customer_id) REFERENCES customers (id) + NOT VALID; + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); +INSERT INTO orders (id, customer_id) VALUES ('o2', 'c9'); diff --git a/db-migration-problems/add-a-foreign-key/03-validate.sql b/db-migration-problems/add-a-foreign-key/03-validate.sql new file mode 100644 index 0000000..580b61d --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/03-validate.sql @@ -0,0 +1,23 @@ +-- STEP 2 — the constraint is validated. +-- +-- VALIDATE CONSTRAINT scans the existing rows, without the heavy lock. It +-- fails if an orphan is left, so the orphans are deleted (or re-pointed) first; +-- order o2 is gone below. After this the database guarantees what the code +-- always assumed. +-- +-- `writ sql --strict` declines this ALTER: it changes the validation state of +-- a constraint, and a schema has no such state. The model carries it instead. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL REFERENCES customers (id) +); + +ALTER TABLE orders VALIDATE CONSTRAINT orders_customer_fk; + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); diff --git a/db-migration-problems/add-a-foreign-key/README.md b/db-migration-problems/add-a-foreign-key/README.md new file mode 100644 index 0000000..4383f92 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/README.md @@ -0,0 +1,77 @@ +# Adding a foreign key NOT VALID: the rows are spared, the code is not + +`orders.customer_id` should point at a customer, and nothing enforces it. +The code deployed today deletes a customer and leaves their orders behind, so +the table has **orphans**. The textbook plan: + +1. deploy code that re-points a customer's orders before deleting them; +2. clean up the existing orphans; +3. add the foreign key `NOT VALID`: no table scan and no long lock; +4. `VALIDATE CONSTRAINT`: checks the old rows, under a lighter lock. + +`NOT VALID` is known as the safe way to add a foreign key, and it does spare +the rows already there. What it does not spare is the code still running. +From the moment the constraint exists, every write is checked, and the old +release's delete is now one the database refuses. + +## The model + +The SQL is [`01-before.sql`](01-before.sql) (order `o2` points at customer +`c9`, who does not exist), [`02-add-not-valid.sql`](02-add-not-valid.sql) and +[`03-validate.sql`](03-validate.sql). + +`writ sql` reads a foreign key's presence, not its validation state, and the +two `ALTER` statements show the difference: + +- `ADD CONSTRAINT … NOT VALID` is read as an ordinary foreign key, + `(fk customer-id customers)`. The output is the same with or without + `NOT VALID`, and `--strict` accepts it. The orphan row `o2 → c9` in that + file loads without complaint. +- `VALIDATE CONSTRAINT` is declined under `--strict`: "ALTER TABLE that adds + no constraint". + +So the model carries the state itself. [`add-a-foreign-key.writ`](add-a-foreign-key.writ) +has the constraint as `none`, `not-valid` or `validated`; the orders table's +orphans as `none` or `some`; and releases `r1`, which makes orphans, and `r2`, +which does not. + +Two rules: + +- `validated-means-no-orphans`: the database's own check, because + `VALIDATE CONSTRAINT` fails while an orphan is left; +- `enforced-means-every-writer-complies`: once the constraint is enforced at + all, no running release makes orphans. The database cannot check this one + ahead of time. It finds out on the first refused delete. + +The safe plan adds the constraint once the fleet has **settled** on r2. +[`add-a-foreign-key-shortcut.writ`](add-a-foreign-key-shortcut.writ) adds it +as soon as r2 is deploying. + +## What writ answers + +The safe plan exits 0. The shortcut, exit 1: + +``` +equation enforced-means-every-writer-complies + … + violated in 1 reachable situations witness: 1. deploy-r2 2. add-not-valid → #3 +``` + +Two steps. r1 is still serving, and from now until the rollout completes, +deleting a customer fails on every r1 instance. `validated-means-no-orphans` +is never broken: validation still waits for the cleanup. The half of the +plan everyone checks is fine. + +This is the shape of `../add-a-required-column/` again: a constraint the +database enforces on behalf of code that does not yet keep it. `NOT NULL` +there, a foreign key here: two costumes for one mistake. + +## Run it + +```sh +writ check add-a-foreign-key.writ --claims add-a-foreign-key.claims # exit 0 +writ check add-a-foreign-key-shortcut.writ --claims add-a-foreign-key.claims # exit 1 +``` + +Siblings: [`../change-an-enum/`](../change-an-enum/), +[`../split-a-table/`](../split-a-table/), and the first three. diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ new file mode 100644 index 0000000..97a2f1f --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ @@ -0,0 +1,84 @@ +; The same plan, with ONE CONDITION REMOVED from adding the constraint: it no +; longer waits for the rollout to settle. NOT VALID is the "safe" way to add a +; foreign key, so it feels safe to add early. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "add-a-foreign-key.lib.writ") + +(schema add-a-foreign-key + + (type yn (no yes)) + + ; The constraint's life: absent, enforced on new writes only (NOT VALID), + ; or validated. `writ sql` reads the schema, which has a foreign key or not; + ; this is the part of the database's state it does not carry. + (type fk-state (none not-valid validated)) + (type constraint (arrow state (to fk-state))) + + ; Whether any order points at a customer that does not exist. + (type amount (none some)) + (type table (arrow orphans (to amount))) + + ; r1 is today's code: deleting a customer leaves their orders behind. r2 + ; re-points them first. + (type release (arrow makes-orphans (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. A validated constraint means no orphans. The database's own check: + ; VALIDATE CONSTRAINT fails outright while one exists. + (equation validated-means-no-orphans + (not (and (is constraint.state validated) + (some (t table) (is t.orphans some))))) + + ; 2. Once the constraint is enforced at all, no running release makes + ; orphans: the database now refuses what that code does, and it fails in + ; production. The required-needs-every-writer shape of + ; ../add-a-required-column, in a third costume. + (equation enforced-means-every-writer-complies + (not (and (not (is constraint.state none)) + (some (f fleet) (or (is f.old.makes-orphans yes) + (is f.new.makes-orphans yes))))))) + +(instance start add-a-foreign-key + (constraint customer-fk (state none)) + (table orders-table (orphans some)) ; o2, in 01-before.sql + (release r1 (makes-orphans yes)) + (release r2 (makes-orphans no)) + (fleet prod (old r1) (new r1))) + +(use add-a-foreign-key) +(initial start) + +; ---- the runbook ---- + +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Delete or re-point the orphans. Only once nothing makes new ones. +(transition clean-orphans + (when (and (is orders-table.orphans some) settled (is prod.new r2))) + (do (set orders-table.orphans none))) + +; 02-add-not-valid.sql, as soon as r2 is deploying. NOT VALID is "the safe +; way to add a foreign key", and it does skip the old rows. +(transition add-not-valid + (when (and (is customer-fk.state none) (is prod.new r2))) ; <- settled, gone + (do (set customer-fk.state not-valid))) + +; 03-validate.sql. The database refuses it while an orphan is left. +(transition validate + (when (and (is customer-fk.state not-valid) (is orders-table.orphans none))) + (do (set customer-fk.state validated))) + diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims new file mode 100644 index 0000000..30141b9 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims @@ -0,0 +1,18 @@ +; The questions, put to both plans. + +(load "add-a-foreign-key.lib.writ") + +(property completes + "the constraint can end up validated, with no orphans and the fleet settled on r2" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept clean-orphans validated-means-no-orphans) +(accept add-not-valid validated-means-no-orphans enforced-means-every-writer-complies) +(accept validate validated-means-no-orphans enforced-means-every-writer-complies) +(accept deploy-r2 enforced-means-every-writer-complies) +(accept settle enforced-means-every-writer-complies) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ new file mode 100644 index 0000000..787523b --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ @@ -0,0 +1,13 @@ +; 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") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the constraint validated, no orphans, the fleet settled +; on r2. (Old and new spelled out rather than `settled`, which compares two +; paths and so cannot appear in a .rules guard.) +(form done (and (is customer-fk.state validated) + (is orders-table.orphans none) + (is prod.old r2) (is prod.new r2))) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules new file mode 100644 index 0000000..9c28cb5 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules @@ -0,0 +1,14 @@ +; The same two 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. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "add-a-foreign-key.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ new file mode 100644 index 0000000..d8a65e1 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ @@ -0,0 +1,88 @@ +; Adding a foreign key to a table that has drifted. +; +; orders.customer_id should point at a customer, and today nothing enforces it, +; so some orders are orphans. The textbook plan: deploy code that stops making +; orphans, clean up the old ones, add the constraint NOT VALID (no table scan, +; no long lock), then VALIDATE it. NOT VALID spares the rows already there. It +; does not spare the code still running. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "add-a-foreign-key.lib.writ") + +(schema add-a-foreign-key + + (type yn (no yes)) + + ; The constraint's life: absent, enforced on new writes only (NOT VALID), + ; or validated. `writ sql` reads the schema, which has a foreign key or not; + ; this is the part of the database's state it does not carry. + (type fk-state (none not-valid validated)) + (type constraint (arrow state (to fk-state))) + + ; Whether any order points at a customer that does not exist. + (type amount (none some)) + (type table (arrow orphans (to amount))) + + ; r1 is today's code: deleting a customer leaves their orders behind. r2 + ; re-points them first. + (type release (arrow makes-orphans (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. A validated constraint means no orphans. The database's own check: + ; VALIDATE CONSTRAINT fails outright while one exists. + (equation validated-means-no-orphans + (not (and (is constraint.state validated) + (some (t table) (is t.orphans some))))) + + ; 2. Once the constraint is enforced at all, no running release makes + ; orphans: the database now refuses what that code does, and it fails in + ; production. The required-needs-every-writer shape of + ; ../add-a-required-column, in a third costume. + (equation enforced-means-every-writer-complies + (not (and (not (is constraint.state none)) + (some (f fleet) (or (is f.old.makes-orphans yes) + (is f.new.makes-orphans yes))))))) + +(instance start add-a-foreign-key + (constraint customer-fk (state none)) + (table orders-table (orphans some)) ; o2, in 01-before.sql + (release r1 (makes-orphans yes)) + (release r2 (makes-orphans no)) + (fleet prod (old r1) (new r1))) + +(use add-a-foreign-key) +(initial start) + +; ---- the runbook ---- + +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Delete or re-point the orphans. Only once nothing makes new ones. +(transition clean-orphans + (when (and (is orders-table.orphans some) settled (is prod.new r2))) + (do (set orders-table.orphans none))) + +; 02-add-not-valid.sql. Once the fleet has SETTLED on the code that complies: +; NOT VALID spares the old rows, not the running code. +(transition add-not-valid + (when (and (is customer-fk.state none) settled (is prod.new r2))) + (do (set customer-fk.state not-valid))) + +; 03-validate.sql. The database refuses it while an orphan is left. +(transition validate + (when (and (is customer-fk.state not-valid) (is orders-table.orphans none))) + (do (set customer-fk.state validated))) + diff --git a/db-migration-problems/change-an-enum/01-before.sql b/db-migration-problems/change-an-enum/01-before.sql new file mode 100644 index 0000000..aa4911a --- /dev/null +++ b/db-migration-problems/change-an-enum/01-before.sql @@ -0,0 +1,12 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- A ticket is open or closed, and the database says so: the CHECK lists the +-- values. `writ sql` reads a CHECK … IN as an enumerated type, so the members +-- below are the members of a type, not a comment. + +CREATE TABLE tickets ( + id uuid PRIMARY KEY, + status text NOT NULL CHECK (status IN ('open', 'closed')) +); + +INSERT INTO tickets (id, status) VALUES ('t1', 'closed'); diff --git a/db-migration-problems/change-an-enum/02-add-value.sql b/db-migration-problems/change-an-enum/02-add-value.sql new file mode 100644 index 0000000..f285059 --- /dev/null +++ b/db-migration-problems/change-an-enum/02-add-value.sql @@ -0,0 +1,14 @@ +-- STEP 1 — the new value arrives. Tickets can now be archived. +-- +-- This is instantaneous and safe: widening a CHECK rewrites nothing, and no +-- row changes. The row below is the same ticket, still closed. The migration +-- in the sense that matters has not happened yet. It happens the first time +-- something WRITES 'archived', and every release still running then has to be +-- able to read it. + +CREATE TABLE tickets ( + id uuid PRIMARY KEY, + status text NOT NULL CHECK (status IN ('open', 'closed', 'archived')) +); + +INSERT INTO tickets (id, status) VALUES ('t1', 'closed'); diff --git a/db-migration-problems/change-an-enum/README.md b/db-migration-problems/change-an-enum/README.md new file mode 100644 index 0000000..9750d37 --- /dev/null +++ b/db-migration-problems/change-an-enum/README.md @@ -0,0 +1,73 @@ +# Adding a value to an enum, and writing it too early + +Tickets are `open` or `closed`, and the database says so with a `CHECK`. +The product wants a third state, `archived`. Widening the `CHECK` is +instantaneous and safe: no row changes. The code change is small too. The new +release knows the third value. + +The migration that matters is neither of those. It is the first time +something **writes** `'archived'`. Every release still running at that moment +has to be able to read it, and the old one maps the column onto a two-value +enum in code: an unknown value is a deserialisation error, on every read of +that row. + +## The model + +The SQL is [`01-before.sql`](01-before.sql) and +[`02-add-value.sql`](02-add-value.sql). `writ sql` reads a `CHECK … IN` as an +enumerated type, so the two steps differ in the type's members: + +``` +(type tickets-status (open closed)) ; 01-before.sql +(type tickets-status (open closed archived)) ; 02-add-value.sql +``` + +[`change-an-enum.writ`](change-an-enum.writ) carries the `CHECK` as one fact +(`allows-archived`), one ticket `t1`, and the fleet as two slots `old` and +`new` over releases `r1` (does not know `archived`) and `r2` (does). The moves +are `add-value`, `deploy-r2`, `settle`, and `archive-t1`: the first write. + +Two rules: + +- `check-allows`: no row holds a value the `CHECK` does not list. The loud + one: break it and the `UPDATE` fails at once; +- `readable`: no row holds a value a running release cannot read. The quiet + one: the `UPDATE` succeeds, and the failure is the next read by an old + instance. + +The safe plan switches the archive feature on once the fleet has **settled** +on r2. [`change-an-enum-shortcut.writ`](change-an-enum-shortcut.writ) switches +it on with the deploy. + +## What writ answers + +Both plans are asked the questions in +[`change-an-enum.claims`](change-an-enum.claims). The safe plan exits 0. The +shortcut, exit 1: + +``` +equation readable + can be broken by: deploy-r2, settle, archive-t1 (acknowledge in claims) + violated in 1 reachable situations witness: 1. add-value 2. deploy-r2 3. archive-t1 → #6 +``` + +Widen the `CHECK`, start the deploy, archive a ticket. r1 is still serving, +and every read of `t1` on an r1 instance fails until the rollout completes. +`check-allows` is satisfied throughout: the database allowed the value. Only +the rule it cannot check breaks. + +## What to take away + +For an enum, the schema change is not the migration: the first write of the +new value is. Gate that write, usually a feature flag, on the rollout having +finished, not on the code having shipped. + +## Run it + +```sh +writ check change-an-enum.writ --claims change-an-enum.claims # exit 0 +writ check change-an-enum-shortcut.writ --claims change-an-enum.claims # exit 1 +``` + +Siblings: [`../split-a-table/`](../split-a-table/), +[`../add-a-foreign-key/`](../add-a-foreign-key/), and the first three. diff --git a/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ b/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ new file mode 100644 index 0000000..b48afa1 --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ @@ -0,0 +1,78 @@ +; The same plan, with ONE CONDITION REMOVED from the first write: the +; archive feature turns on with the deploy instead of after it settles. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "change-an-enum.lib.writ") + +(schema change-an-enum + + (type yn (no yes)) + + ; The members as `writ sql` reads them from the final step's CHECK. + (type tickets-status (open closed archived)) + + ; The CHECK itself: whether the database accepts 'archived' yet. + (type check (arrow allows-archived (to yn))) + + (type ticket (arrow status (to tickets-status))) + + ; r1 is deployed today and maps the column onto a two-value enum in code: an + ; unknown value is a deserialisation error. r2 knows all three. + (type release (arrow knows-archived (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. The database refuses a value its CHECK does not list. It is the loud + ; rule: break it and the UPDATE fails at once. + (equation check-allows + (not (and (is ticket.status archived) + (some (c check) (is c.allows-archived no))))) + + ; 2. Every running release can read every row. The quiet rule: the UPDATE + ; succeeds, and the failure is the next read by an old instance. + (equation readable + (not (and (is ticket.status archived) + (some (f fleet) (or (is f.old.knows-archived no) + (is f.new.knows-archived no))))))) + +(instance start change-an-enum + (check status-check (allows-archived no)) + (ticket t1 (status closed)) + (release r1 (knows-archived no)) + (release r2 (knows-archived yes)) + (fleet prod (old r1) (new r1))) + +(use change-an-enum) +(initial start) + +; ---- the runbook ---- + +; Widen the CHECK (02-add-value.sql). Safe at any time: nothing writes the +; value yet. +(transition add-value + (when (is status-check.allows-archived no)) + (do (set status-check.allows-archived yes))) + +; Ship the code that knows the new value. +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Archive a closed ticket as soon as r2 is deploying: the feature ships with +; the code. +(transition archive-t1 + (when (and (is t1.status closed) + (is status-check.allows-archived yes) + (is prod.new r2))) ; <- settled, gone + (do (set t1.status archived))) + diff --git a/db-migration-problems/change-an-enum/change-an-enum.claims b/db-migration-problems/change-an-enum/change-an-enum.claims new file mode 100644 index 0000000..292653b --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.claims @@ -0,0 +1,17 @@ +; The questions, put to both plans. + +(load "change-an-enum.lib.writ") + +(property completes + "a ticket can end up archived, with the fleet settled on the release that knows the value" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept add-value check-allows) +(accept archive-t1 check-allows readable) +(accept deploy-r2 readable) +(accept settle readable) diff --git a/db-migration-problems/change-an-enum/change-an-enum.lib.writ b/db-migration-problems/change-an-enum/change-an-enum.lib.writ new file mode 100644 index 0000000..65f80ee --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.lib.writ @@ -0,0 +1,13 @@ +; 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") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the value exists, the fleet has settled on the release +; that knows it (old and new both r2, spelled without `settled`, which compares +; two paths and so cannot appear in a .rules guard), and a ticket is archived. +(form done (and (is status-check.allows-archived yes) + (is prod.old r2) (is prod.new r2) + (is t1.status archived))) diff --git a/db-migration-problems/change-an-enum/change-an-enum.rules b/db-migration-problems/change-an-enum/change-an-enum.rules new file mode 100644 index 0000000..bc07137 --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.rules @@ -0,0 +1,14 @@ +; The same two 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. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "change-an-enum.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/change-an-enum/change-an-enum.writ b/db-migration-problems/change-an-enum/change-an-enum.writ new file mode 100644 index 0000000..b4a8eaa --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.writ @@ -0,0 +1,84 @@ +; Adding a value to an enum — and writing it before every reader knows it. +; +; Tickets are open or closed, and the product wants a third state, archived. +; The schema change is trivial: widen the CHECK. The code change is trivial: +; r2 knows the new value. The trap is the first WRITE of 'archived' while r1, +; which maps the column onto a two-value enum, is still serving reads. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "change-an-enum.lib.writ") + +(schema change-an-enum + + (type yn (no yes)) + + ; The members as `writ sql` reads them from the final step's CHECK. + (type tickets-status (open closed archived)) + + ; The CHECK itself: whether the database accepts 'archived' yet. + (type check (arrow allows-archived (to yn))) + + (type ticket (arrow status (to tickets-status))) + + ; r1 is deployed today and maps the column onto a two-value enum in code: an + ; unknown value is a deserialisation error. r2 knows all three. + (type release (arrow knows-archived (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. The database refuses a value its CHECK does not list. It is the loud + ; rule: break it and the UPDATE fails at once. + (equation check-allows + (not (and (is ticket.status archived) + (some (c check) (is c.allows-archived no))))) + + ; 2. Every running release can read every row. The quiet rule: the UPDATE + ; succeeds, and the failure is the next read by an old instance. + (equation readable + (not (and (is ticket.status archived) + (some (f fleet) (or (is f.old.knows-archived no) + (is f.new.knows-archived no))))))) + +(instance start change-an-enum + (check status-check (allows-archived no)) + (ticket t1 (status closed)) + (release r1 (knows-archived no)) + (release r2 (knows-archived yes)) + (fleet prod (old r1) (new r1))) + +(use change-an-enum) +(initial start) + +; ---- the runbook ---- + +; Widen the CHECK (02-add-value.sql). Safe at any time: nothing writes the +; value yet. +(transition add-value + (when (is status-check.allows-archived no)) + (do (set status-check.allows-archived yes))) + +; Ship the code that knows the new value. +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Archive a closed ticket: the first write of the new value. The feature is +; switched on only once the fleet has SETTLED on r2. `allows-archived` is the +; condition the database would enforce anyway; `settled` is the one it cannot. +(transition archive-t1 + (when (and (is t1.status closed) + (is status-check.allows-archived yes) + (is prod.new r2) + settled)) + (do (set t1.status archived))) + diff --git a/db-migration-problems/split-a-table/01-before.sql b/db-migration-problems/split-a-table/01-before.sql new file mode 100644 index 0000000..b0eccf2 --- /dev/null +++ b/db-migration-problems/split-a-table/01-before.sql @@ -0,0 +1,13 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- A user has one address, and it lives on the users table. The product now +-- wants several addresses per user, so the address moves to a table of its +-- own. One representative user below. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL, + address text NOT NULL +); + +INSERT INTO users (id, email, address) VALUES ('u1', 'ada@example.com', '1 Main St'); diff --git a/db-migration-problems/split-a-table/02-create-addresses.sql b/db-migration-problems/split-a-table/02-create-addresses.sql new file mode 100644 index 0000000..559dd27 --- /dev/null +++ b/db-migration-problems/split-a-table/02-create-addresses.sql @@ -0,0 +1,25 @@ +-- STEP 1 — the new table arrives beside the old column. +-- +-- Nothing is moved yet. The code deployed next writes BOTH places (the +-- "dual write"), and a backfill copies the rows that existed before it. Until +-- the backfill finishes, the new table holds some addresses and not others, +-- and no row in this file says which: that is exactly what the model has to +-- carry as state of its own. Here, mid-backfill, Ada's address has not been +-- copied yet, so `addresses` has no row. +-- +-- `user_id REFERENCES users` is a foreign key, and `writ sql` reads it as an +-- arrow from an address to a user. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL, + address text NOT NULL +); + +CREATE TABLE addresses ( + id uuid PRIMARY KEY, + user_id uuid NOT NULL REFERENCES users (id), + address text NOT NULL +); + +INSERT INTO users (id, email, address) VALUES ('u1', 'ada@example.com', '1 Main St'); diff --git a/db-migration-problems/split-a-table/03-drop-column.sql b/db-migration-problems/split-a-table/03-drop-column.sql new file mode 100644 index 0000000..2a2b8e3 --- /dev/null +++ b/db-migration-problems/split-a-table/03-drop-column.sql @@ -0,0 +1,18 @@ +-- STEP 2 — the old column goes, once nothing reads or writes it. +-- +-- By now every address is in the new table: the backfill copied the old ones, +-- and every release deployed since step 1 writes there. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL +); + +CREATE TABLE addresses ( + id uuid PRIMARY KEY, + user_id uuid NOT NULL REFERENCES users (id), + address text NOT NULL +); + +INSERT INTO users (id, email) VALUES ('u1', 'ada@example.com'); +INSERT INTO addresses (id, user_id, address) VALUES ('a1', 'u1', '1 Main St'); diff --git a/db-migration-problems/split-a-table/README.md b/db-migration-problems/split-a-table/README.md new file mode 100644 index 0000000..46e1f0a --- /dev/null +++ b/db-migration-problems/split-a-table/README.md @@ -0,0 +1,72 @@ +# Splitting a table: switching reads before the copy finishes + +A user's address moves out of `users` into a table of its own, so a user can +have several. The safe order is well known: create the new table; deploy code +that writes both places (the **dual write**); copy the rows that existed +before it (the **backfill**); switch reads to the new table; drop the old +column. + +The switch must wait for the backfill to *finish*. Nothing in any SQL file +says when that is. Until then the new table holds some addresses and not +others, and a read from it returns nothing for every user the backfill has +not reached yet. No error is raised: those users simply have no address. + +## The model + +The SQL is [`01-before.sql`](01-before.sql), +[`02-create-addresses.sql`](02-create-addresses.sql) and +[`03-drop-column.sql`](03-drop-column.sql). `writ sql` reads the new table's +`user_id uuid NOT NULL REFERENCES users (id)` as an arrow from an address to a +user: `(fk user-id users)`. + +How far the backfill has got is not in any file, so +[`split-a-table.writ`](split-a-table.writ) carries it as a cell: `filled` is +`no`, `partial` or `yes`. Not a row count. The rules only ever ask which of +those three it is. Three releases, each described by what its code reads and +writes: `r1` (old column only), `r2` (writes both, reads the old one), `r3` +(the new table only). + +Three rules: + +- `read-of-existing`: nobody reads a column that is gone; +- `no-lost-writes`: once the backfill has started, every running release + writes the new table too, or its writes land after the copy and are never + moved; +- `complete-before-read`: nobody reads the new table before it holds every + address. + +The safe plan deploys r3 once r2 has settled **and** `filled` is `yes`. +[`split-a-table-shortcut.writ`](split-a-table-shortcut.writ) deploys it once +the backfill has started. + +## What writ answers + +The safe plan exits 0. The shortcut, exit 1: + +``` +equation complete-before-read + … + violated in 3 reachable situations witness: 1. create-table 2. deploy-r2 3. settle 4. backfill-start 5. deploy-r3 → #6 +``` + +Five steps, the longest route to a fault in this collection, and every one is +in the runbook's order. The mistake is the word "started" where the runbook +meant "finished". The backfill in a real system takes hours, so that word +covers most of the migration's wall-clock time. + +## What to take away + +The migration's real state includes the progress of a job, and a job's +progress is exactly what no schema file records. Make it a fact the deploy +can check: a completion row the backfill writes last, for instance. Then gate +the switch on that row rather than on the job having been launched. + +## Run it + +```sh +writ check split-a-table.writ --claims split-a-table.claims # exit 0 +writ check split-a-table-shortcut.writ --claims split-a-table.claims # exit 1 +``` + +Siblings: [`../change-an-enum/`](../change-an-enum/), +[`../add-a-foreign-key/`](../add-a-foreign-key/), and the first three. diff --git a/db-migration-problems/split-a-table/split-a-table-shortcut.writ b/db-migration-problems/split-a-table/split-a-table-shortcut.writ new file mode 100644 index 0000000..9bb0e1e --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table-shortcut.writ @@ -0,0 +1,102 @@ +; The same plan, with ONE CONDITION WEAKENED: reads switch to the new table +; once the backfill has STARTED, not finished. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "split-a-table.lib.writ") + +(schema split-a-table + + (type yn (no yes)) + + ; users.address, the column that is moving out. + (type column (arrow present (to yn))) + + ; The new table. Whether it exists, and how much of it is filled: no, partly + ; (the backfill has started), or completely. Not a row count — the rules + ; only ever ask which of those three it is. + (type fill (no partial yes)) + (type table + (arrow exists (to yn)) + (arrow filled (to fill))) + + ; What each release does, taken from its code. r1 is today's. r2 writes + ; both places and still reads the old one. r3 uses only the new table. + (type release + (arrow reads-old (to yn) fixed) + (arrow reads-new (to yn) fixed) + (arrow writes-new (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. Nobody reads a column that is gone. + (equation read-of-existing + (not (and (is column.present no) + (some (f fleet) (or (is f.old.reads-old yes) (is f.new.reads-old yes)))))) + + ; 2. Once the backfill has started, every running release writes the new + ; table too; otherwise its writes land after the copy and are never moved. + (equation no-lost-writes + (not (and (not (is table.filled no)) + (some (f fleet) (or (is f.old.writes-new no) (is f.new.writes-new no)))))) + + ; 3. Nobody reads the new table before it holds every address. The one the + ; shortcut breaks: the reads succeed, and return nothing for the users the + ; backfill has not reached. + (equation complete-before-read + (not (and (not (is table.filled yes)) + (some (f fleet) (or (is f.old.reads-new yes) (is f.new.reads-new yes))))))) + +(instance start split-a-table + (column address-col (present yes)) + (table addresses (exists no) (filled no)) + (release r1 (reads-old yes) (reads-new no) (writes-new no)) + (release r2 (reads-old yes) (reads-new no) (writes-new yes)) + (release r3 (reads-old no) (reads-new yes) (writes-new yes)) + (fleet prod (old r1) (new r1))) + +(use split-a-table) +(initial start) + +; ---- the runbook ---- + +; 02-create-addresses.sql. +(transition create-table + (when (is addresses.exists no)) + (do (set addresses.exists yes))) + +; Dual write. +(transition deploy-r2 + (when (and settled (is prod.new r1) (is addresses.exists yes))) + (do (set prod.new r2))) + +; Every rollout ends the same way. +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Copy the addresses that existed before the dual write. Only once nothing +; still writes the old place alone. +(transition backfill-start + (when (and (is addresses.filled no) settled (is prod.new r2))) + (do (set addresses.filled partial))) +(transition backfill-finish + (when (is addresses.filled partial)) + (do (set addresses.filled yes))) + +; Switch reads to the new table once the backfill is under way: it is "nearly +; done", and r3 writes there too. +(transition deploy-r3 + (when (and settled (is prod.new r2) (not (is addresses.filled no)))) ; <- yes, weakened to "started" + (do (set prod.new r3))) + +; 03-drop-column.sql, once nothing reads it. +(transition drop-column + (when (and (is address-col.present yes) settled (is prod.new r3))) + (do (set address-col.present no))) + diff --git a/db-migration-problems/split-a-table/split-a-table.claims b/db-migration-problems/split-a-table/split-a-table.claims new file mode 100644 index 0000000..6f4b52c --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.claims @@ -0,0 +1,19 @@ +; The questions, put to both plans. + +(load "split-a-table.lib.writ") + +(property completes + "the move can finish: settled on r3, every address copied, the old column gone" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept deploy-r2 read-of-existing no-lost-writes complete-before-read) +(accept settle read-of-existing no-lost-writes complete-before-read) +(accept deploy-r3 read-of-existing no-lost-writes complete-before-read) +(accept drop-column read-of-existing) +(accept backfill-start no-lost-writes complete-before-read) +(accept backfill-finish no-lost-writes complete-before-read) diff --git a/db-migration-problems/split-a-table/split-a-table.lib.writ b/db-migration-problems/split-a-table/split-a-table.lib.writ new file mode 100644 index 0000000..571f293 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.lib.writ @@ -0,0 +1,13 @@ +; 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") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the fleet settled on r3, every address in the new table, +; the old column gone. (Old and new are spelled out rather than `settled`, +; which compares two paths and so cannot appear in a .rules guard.) +(form done (and (is prod.old r3) (is prod.new r3) + (is addresses.filled yes) + (is address-col.present no))) diff --git a/db-migration-problems/split-a-table/split-a-table.rules b/db-migration-problems/split-a-table/split-a-table.rules new file mode 100644 index 0000000..d1345a7 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.rules @@ -0,0 +1,14 @@ +; The same two 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. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "split-a-table.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/split-a-table/split-a-table.writ b/db-migration-problems/split-a-table/split-a-table.writ new file mode 100644 index 0000000..f60a4e4 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.writ @@ -0,0 +1,107 @@ +; Splitting a table — dual write, backfill, switch, contract. +; +; The address moves from users to a table of its own. The safe order is the +; one everyone knows: create the table, deploy code that writes both places, +; copy the old rows, switch reads to the new table, drop the old column. The +; switch must wait for the copy to FINISH, and nothing in any SQL file says +; when that is. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "split-a-table.lib.writ") + +(schema split-a-table + + (type yn (no yes)) + + ; users.address, the column that is moving out. + (type column (arrow present (to yn))) + + ; The new table. Whether it exists, and how much of it is filled: no, partly + ; (the backfill has started), or completely. Not a row count — the rules + ; only ever ask which of those three it is. + (type fill (no partial yes)) + (type table + (arrow exists (to yn)) + (arrow filled (to fill))) + + ; What each release does, taken from its code. r1 is today's. r2 writes + ; both places and still reads the old one. r3 uses only the new table. + (type release + (arrow reads-old (to yn) fixed) + (arrow reads-new (to yn) fixed) + (arrow writes-new (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. Nobody reads a column that is gone. + (equation read-of-existing + (not (and (is column.present no) + (some (f fleet) (or (is f.old.reads-old yes) (is f.new.reads-old yes)))))) + + ; 2. Once the backfill has started, every running release writes the new + ; table too; otherwise its writes land after the copy and are never moved. + (equation no-lost-writes + (not (and (not (is table.filled no)) + (some (f fleet) (or (is f.old.writes-new no) (is f.new.writes-new no)))))) + + ; 3. Nobody reads the new table before it holds every address. The one the + ; shortcut breaks: the reads succeed, and return nothing for the users the + ; backfill has not reached. + (equation complete-before-read + (not (and (not (is table.filled yes)) + (some (f fleet) (or (is f.old.reads-new yes) (is f.new.reads-new yes))))))) + +(instance start split-a-table + (column address-col (present yes)) + (table addresses (exists no) (filled no)) + (release r1 (reads-old yes) (reads-new no) (writes-new no)) + (release r2 (reads-old yes) (reads-new no) (writes-new yes)) + (release r3 (reads-old no) (reads-new yes) (writes-new yes)) + (fleet prod (old r1) (new r1))) + +(use split-a-table) +(initial start) + +; ---- the runbook ---- + +; 02-create-addresses.sql. +(transition create-table + (when (is addresses.exists no)) + (do (set addresses.exists yes))) + +; Dual write. +(transition deploy-r2 + (when (and settled (is prod.new r1) (is addresses.exists yes))) + (do (set prod.new r2))) + +; Every rollout ends the same way. +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Copy the addresses that existed before the dual write. Only once nothing +; still writes the old place alone. +(transition backfill-start + (when (and (is addresses.filled no) settled (is prod.new r2))) + (do (set addresses.filled partial))) +(transition backfill-finish + (when (is addresses.filled partial)) + (do (set addresses.filled yes))) + +; Switch reads to the new table: once r2 has settled AND the backfill has +; finished. +(transition deploy-r3 + (when (and settled (is prod.new r2) (is addresses.filled yes))) + (do (set prod.new r3))) + +; 03-drop-column.sql, once nothing reads it. +(transition drop-column + (when (and (is address-col.present yes) settled (is prod.new r3))) + (do (set address-col.present no))) + diff --git a/modality-cross-check.sh b/modality-cross-check.sh index e468699..bbc9a2e 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 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 payments config-space on-call-rota" +scenarios="river island queens jobshop-possible jobshop-best arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column db-migration-problems/change-an-enum db-migration-problems/split-a-table db-migration-problems/add-a-foreign-key entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments config-space on-call-rota" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index 82fadad..167d58a 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -293,18 +293,19 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The nineteen scenarios this script walks by convention, and their 57 - # properties. Adding a property to any of the nineteen fails this line, which is the point of it — + # The twenty-two scenarios this script walks by convention, and their 63 + # properties. Adding a property to any of the twenty-two 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, 49 -> 52 with deployment, 52 -> 56 with # payments, 56 -> 60 with config-space, 60 -> 55 as oversight, workflow - # and access left, 55 -> 57 with on-call-rota, and this line is where each - # of those had to be said out loud. - has "cross-check: all 57 properties of the nineteen scenarios were considered" \ - "$out" "considered 57 properties: 55 compared, 2 not compared" - # Two of the 57 are not compared, and the count above is the only place that + # and access left, 55 -> 57 with on-call-rota, 57 -> 63 with the second + # batch of db-migration-problems (2 + 2 + 2), and this line is where each of + # those had to be said out loud. + has "cross-check: all 63 properties of the twenty-two scenarios were considered" \ + "$out" "considered 63 properties: 61 compared, 2 not compared" + # Two of the 63 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. @@ -780,9 +781,97 @@ on_call_rota() { has "on-call-rota: one row per week" "$dv" "17 w6 bob" } +change_an_enum() { + d="$here/db-migration-problems/change-an-enum" + echo "== Adding a value to an enum — and writing it before every reader knows it ==" + echo " Q: widening a CHECK is instant. When is the migration, really?" + has "change-an-enum: writ sql reads the CHECK as two members before" \ + "$("$WRIT" sql "$d/01-before.sql" 2>/dev/null)" "(type tickets-status (open closed))" + has "change-an-enum: and three after" \ + "$("$WRIT" sql "$d/02-add-value.sql" 2>/dev/null)" "(type tickets-status (open closed archived))" + + ok_=$("$WRIT" check "$d/change-an-enum.writ" --claims "$d/change-an-enum.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "change-an-enum: the plan is clean" "$ost" 0 + has "change-an-enum: A. a ticket can be archived" "$ok_" "holds completes" + lacks "change-an-enum: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/change-an-enum-shortcut.writ" --claims "$d/change-an-enum.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "change-an-enum: archiving during the rollout is refused" "$sst" 1 + has "change-an-enum: B. the first write of the value, while r1 still reads" "$sc" \ + "violated in 1 reachable situations witness: 1. add-value 2. deploy-r2 3. archive-t1" + # The database's own check is satisfied throughout: the value is allowed. + nviol=$(printf '%s\n' "$sc" | grep -c "violated in") + if [ "$nviol" = "1" ]; then + ok "change-an-enum: C. and only the rule the database cannot check breaks" + else + bad "change-an-enum: C. expected exactly one violated rule, got $nviol" + fi +} + +split_a_table() { + d="$here/db-migration-problems/split-a-table" + echo "== Splitting a table — dual write, backfill, switch, contract ==" + echo " Q: when may reads switch to the new table?" + has "split-a-table: writ sql reads the new table's foreign key as an arrow" \ + "$("$WRIT" sql "$d/02-create-addresses.sql" 2>/dev/null)" "(fk user-id users)" + + ok_=$("$WRIT" check "$d/split-a-table.writ" --claims "$d/split-a-table.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "split-a-table: the plan is clean" "$ost" 0 + has "split-a-table: A. the move can finish" "$ok_" "holds completes" + lacks "split-a-table: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/split-a-table-shortcut.writ" --claims "$d/split-a-table.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "split-a-table: switching on a started backfill is refused" "$sst" 1 + # The longest route to a fault in the collection: five steps, every one of + # them in the runbook's order. + has "split-a-table: B. reads switch to a half-filled table, five steps in" "$sc" \ + "violated in 3 reachable situations witness: 1. create-table 2. deploy-r2 3. settle 4. backfill-start 5. deploy-r3" + has "split-a-table: and it is the completeness rule that breaks" "$sc" "equation complete-before-read" +} + +add_a_foreign_key() { + d="$here/db-migration-problems/add-a-foreign-key" + echo "== Adding a foreign key, NOT VALID — the rows are spared, the code is not ==" + echo " Q: NOT VALID skips the old rows. Does it make adding the key safe?" + # Recorded as found: writ sql reads NOT VALID as an ordinary foreign key — + # the output is the same with or without it, and --strict accepts it — + # while it declines VALIDATE CONSTRAINT. The model carries the state. + "$WRIT" sql "$d/02-add-not-valid.sql" --with-data --strict >/dev/null 2>&1 + exit_is "add-a-foreign-key: writ sql accepts NOT VALID, as a plain foreign key" "$?" 0 + has "add-a-foreign-key: reading it as an arrow" \ + "$("$WRIT" sql "$d/02-add-not-valid.sql" 2>/dev/null)" "(fk customer-id customers)" + vs=$("$WRIT" sql "$d/03-validate.sql" --with-data --strict 2>&1) + vst=$? + exit_is "add-a-foreign-key: and declines VALIDATE CONSTRAINT under --strict" "$vst" 1 + has "add-a-foreign-key: saying why" "$vs" "ALTER TABLE that adds no constraint" + + ok_=$("$WRIT" check "$d/add-a-foreign-key.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "add-a-foreign-key: the plan is clean" "$ost" 0 + has "add-a-foreign-key: A. the constraint can end up validated" "$ok_" "holds completes" + lacks "add-a-foreign-key: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/add-a-foreign-key-shortcut.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "add-a-foreign-key: adding it mid-rollout is refused" "$sst" 1 + has "add-a-foreign-key: B. two steps: the old code's deletes now fail" "$sc" \ + "violated in 1 reachable situations witness: 1. deploy-r2 2. add-not-valid" + has "add-a-foreign-key: the every-writer rule, a third time" "$sc" "equation enforced-means-every-writer-complies" +} + # 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 two_phase_commit 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 payments config_space on_call_rota control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best two_phase_commit arch timetable rename_a_column drop_a_column add_a_required_column change_an_enum split_a_table add_a_foreign_key separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments config_space on_call_rota control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):"