diff --git a/README.md b/README.md index 61b062e..000072c 100644 --- a/README.md +++ b/README.md @@ -49,6 +49,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding |---|---|---| | [`jobshop-possible/`](jobshop-possible/) | Can three jobs on three blocking machines all finish? | Yes — but three moves can deadlock the shop. | | [`jobshop-best/`](jobshop-best/) | What is the shortest schedule? | 5 ticks: `done-by-4` fails, `done-by-5` holds. | +| [`on-call-rota/`](on-call-rota/) | Does a valid on-call rota exist, and what does the policy not say? | Ten exist, and writ prints one. Add one kind rule and none does, unless a question the policy never answered is answered yes. | | [`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. | 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/docker-compose.yml b/docker-compose.yml index 0b83780..6912ddd 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -93,6 +93,12 @@ services: image: writ-problems command: ["config_space"] + # An on-call rota: produced, the policy's gap found, and the rule that ends it. + on-call-rota: + build: . + image: writ-problems + command: ["on_call_rota"] + # 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 15c9865..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" +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/on-call-rota/README.md b/on-call-rota/README.md new file mode 100644 index 0000000..ba74947 --- /dev/null +++ b/on-call-rota/README.md @@ -0,0 +1,156 @@ +# An on-call rota: does one exist, and what did the policy not say? + +A team of four covers six weeks of on-call. The policy: + +- every week has a primary; +- nobody is primary two weeks in a row; +- nobody is primary more than two weeks in the six; +- nobody is primary in a week they are on leave (Bob is away in week 3, Cat + in week 4); +- Dan joined last month, and may not be primary until his second month + (weeks 5 and 6). + +The question is not which rota is best, but whether any rota satisfies the +policy, and if so, what one looks like. writ answers by building rotas +week by week, and the witness it prints *is* a rota. + +## The model + +[`on-call-rota.writ`](on-call-rota.writ) has six **weeks** on a ladder +(`w1` … `w6`, then `done`), each with a `primary` slot. A **cursor** walks +the ladder, so weeks are filled in order and every situation is a partial +rota. There is one move per person and week: `ann-takes-w1`, `bob-takes-w4`, +and so on. Each one checks the policy in its guard and moves the cursor on. + +"At most two weeks" is counting, and the model does no arithmetic. Each +person carries a `load` on a three-step scale, `l0 → l1 → l2`, and the top +step has no `up`. Taking a week moves the load one step up, so a third week +isn't refused by a guard. It's absent: there is no step to move to. + +## What writ answers + +The questions are in [`on-call-rota.claims`](on-call-rota.claims): + +``` +states: 27 edges: 30 +regime: committing — no move can be undone +gaps: 2 + bob-takes-w2 — "the policy does not say whether a primary may hand over straight into their own leave" (min 1 moves) + cat-takes-w3 — "the policy does not say whether a primary may hand over straight into their own leave" (min 2 moves) +dead ends: 10 +… +holds rota-exists + "six weeks can be covered under the policy" + witness: 1. ann-takes-w1 … + 2. cat-takes-w2 … + 3. ann-takes-w3 … + 4. bob-takes-w4 … + 5. cat-takes-w5 … + 6. bob-takes-w6 … +fails no-dead-end-prefix + "from every partial rota, a complete one can still be reached" + stuck at: #3 (w1.primary=cat …) + witness: 1. cat-takes-w1 +``` + +The witness, as a rota: + +| week | 1 | 2 | 3 | 4 | 5 | 6 | +| --- | --- | --- | --- | --- | --- | --- | +| primary | Ann | Cat | Ann | Bob | Cat | Bob | + +There are ten in all. Each complete rota is a dead end of six moves (there is +nothing left to fill), and the ten dead ends are the ten rotas. +[`on-call-rota.rules`](on-call-rota.rules) reads them all out as rows: + +```sh +writ derive on-call-rota.writ on-call-rota.rules rota +``` + +``` +rota (60 rows) + 17 w1 ann + 17 w2 cat + … +``` + +Ten rotas, six rows each. + +**The planner's trap:** give Cat week 1 and no rota can be finished. +`no-dead-end-prefix` fails at that first step. Week 2 then has to be Ann: +Bob's week 2 is a gap (below), and Dan is too new. Week 3 has nobody: Ann +just did week 2, Bob is away, Cat's week 3 is a gap, and Dan is still too +new. A planner filling the calendar from the top finds out two weeks later, +at the one question the policy never answered. + +## The question the policy never answers + +Bob is away in week 3. May he be primary in week 2 and hand over straight +into his leave, with nobody back the next week to answer for what happened +on his watch? Cat has the same question for week 3. The policy does not +say. In the model, those two assignments are not moves but **gaps**: + +```lisp +(do (gap "the policy does not say whether a primary may hand over straight into their own leave")) +``` + +writ lists each gap with the shortest route to it. That is the question to +put back to whoever owns the policy, the way `../timetable/` puts back what a +curriculum never said. Ten rotas exist without those two assignments, so the +policy as written does not need an answer. The trap above does: it is a dead +end only because the one way out is a gap. + +## One more rule + +[`on-call-rota-strict.writ`](on-call-rota-strict.writ) adds a rule teams +add after someone comes back from holiday straight into an incident: **nobody +is primary in the week they come back from leave**. + +``` +fails rota-exists + "six weeks can be covered under the policy" +… +dead ends: 2 + reached by: ann-takes-w1, cat-takes-w2, ann-takes-w3 + reached by: bob-takes-w1, cat-takes-w2, ann-takes-w3 +``` + +No rota exists, and every attempt stops after week 3. The reason can be read +backwards from week 4: + +- in **week 4**, Cat is away, Bob has just come back, and Dan is too new, so + it has to be Ann; +- so **week 3** cannot be Ann, Bob is away, and Dan is still too new, so it + has to be Cat; +- and Cat in week 3 is the week before her leave, which is one of the gaps. + +So under the stricter policy, a rota exists **only if** the question nobody +answered is answered yes. The gap went from a loose end to the deciding +question. `writ compare` reports it as a lost guarantee with no witness: + +``` +properties: rota-exists LOST +``` + +A failed `possible` has no route to print. The absence is the answer, and the +dead ends show how far the policy gets. + +## What to take away + +Staffing rules are each reasonable, and a rota usually exists, until one more +rule meets the calendar's particular leave. Asking "does one exist" each time +the policy changes is cheap. Here it also turned up the question the policy +should have answered first. + +To adapt it, add people with their leave and start dates, and weeks as rungs +of the ladder. Each rule is a conjunct in the `assign` form's guard. + +## Run it + +```sh +writ check on-call-rota.writ --claims on-call-rota.claims # exit 1: the planner's trap +writ check on-call-rota-strict.writ --claims on-call-rota.claims # exit 1: no rota +writ derive on-call-rota.writ on-call-rota.rules rota +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. diff --git a/on-call-rota/on-call-rota-strict.writ b/on-call-rota/on-call-rota-strict.writ new file mode 100644 index 0000000..0a0f269 --- /dev/null +++ b/on-call-rota/on-call-rota-strict.writ @@ -0,0 +1,114 @@ +; The same policy with ONE MORE RULE: nobody is primary in the week they come +; back from leave. It is a kind rule, and it is the sort of thing a team adds +; after someone returns from holiday straight into an incident. +; +; `writ check` exits 1 on this file: no rota exists, unless the question the +; policy never answered is answered yes. + +(load "stdlib.writ") +(load "on-call-rota.lib.writ") + +(schema on-call-rota + + (type yn (no yes)) + + ; How many weeks someone has taken so far. The policy caps it at two, so the + ; count is a three-step scale; the top step has no `up`, so a third week is + ; not refused but absent: there is no value to move to. + (type level (arrow up (to level) fixed vacatable)) + + ; Six weeks, filled in order. `next` is the ladder; the last week has none. + ; `late` marks the weeks a new joiner may take: their second month. + (type week + (arrow next (to week) fixed vacatable) + (arrow late (to yn) fixed) + (maybe primary person)) + + (type person + (arrow new (to yn) fixed) + (arrow leave (to week) fixed vacatable) + (arrow back (to week) fixed vacatable) ; the week they return + (arrow load (to level))) + + ; Where the planner is: the week being filled, or `done`. + (type cursor (arrow at (to week) vacatable))) + +(instance start on-call-rota + + (level l0 (up l1)) + (level l1 (up l2)) + (level l2 (up vacant)) + + (week w1 (next w2) (late no) (primary vacant)) + (week w2 (next w3) (late no) (primary vacant)) + (week w3 (next w4) (late no) (primary vacant)) + (week w4 (next w5) (late no) (primary vacant)) + (week w5 (next w6) (late yes) (primary vacant)) + (week w6 (next done) (late yes) (primary vacant)) + ; Past the last week. The cursor lands here when the rota is complete, and + ; no move fills it: its `next` is vacant, so an assignment to it is absent. + (week done (next vacant) (late no) (primary vacant)) + + (person ann (new no) (leave vacant) (back vacant) (load l0)) + (person bob (new no) (leave w3) (back w4) (load l0)) ; away in week 3 + (person cat (new no) (leave w4) (back w5) (load l0)) ; away in week 4 + (person dan (new yes) (leave vacant) (back vacant) (load l0)) ; joined last month + + (cursor cur (at w1))) + +(use on-call-rota) +(initial start) + +; ---- the policy ---- +; +; Person P is primary for week W, whose previous week is PREV: +; - not on leave that week; +; - not primary the week before (nobody does two in a row); +; - a new joiner only in their second month; +; - at most two weeks in the six: carried by the load scale, whose `up` +; runs out after two. +; Week 1 has no previous week; it passes itself as PREV, whose primary is +; still empty when it is being filled. +(form (assign N P W PREV) + (transition N + (when (and (is cur.at W) + (not (is P.leave W)) + (not (is PREV.primary P)) + (or (is P.new no) (is W.late yes)) + ; the new rule: not the week you come back + (not (is P.back W)))) + (do (set W.primary P) (set P.load P.load.up) (set cur.at W.next)))) + +; The week before someone's leave. Whether the primary may hand over straight +; into their own leave, with nobody back the next week to answer for what they +; did, the policy does not say. So it is not a move but a question: a gap, +; reported with its route, for whoever owns the policy to answer. +(form (handover-into-leave N P W PREV) + (transition N + (when (and (is cur.at W) (not (is PREV.primary P)))) + (do (gap "the policy does not say whether a primary may hand over straight into their own leave")))) + +(assign ann-takes-w1 ann w1 w1) +(assign bob-takes-w1 bob w1 w1) +(assign cat-takes-w1 cat w1 w1) +(assign dan-takes-w1 dan w1 w1) +(assign ann-takes-w2 ann w2 w1) +(handover-into-leave bob-takes-w2 bob w2 w1) +(assign cat-takes-w2 cat w2 w1) +(assign dan-takes-w2 dan w2 w1) +(assign ann-takes-w3 ann w3 w2) +(assign bob-takes-w3 bob w3 w2) +(handover-into-leave cat-takes-w3 cat w3 w2) +(assign dan-takes-w3 dan w3 w2) +(assign ann-takes-w4 ann w4 w3) +(assign bob-takes-w4 bob w4 w3) +(assign cat-takes-w4 cat w4 w3) +(assign dan-takes-w4 dan w4 w3) +(assign ann-takes-w5 ann w5 w4) +(assign bob-takes-w5 bob w5 w4) +(assign cat-takes-w5 cat w5 w4) +(assign dan-takes-w5 dan w5 w4) +(assign ann-takes-w6 ann w6 w5) +(assign bob-takes-w6 bob w6 w5) +(assign cat-takes-w6 cat w6 w5) +(assign dan-takes-w6 dan w6 w5) diff --git a/on-call-rota/on-call-rota.claims b/on-call-rota/on-call-rota.claims new file mode 100644 index 0000000..9c73970 --- /dev/null +++ b/on-call-rota/on-call-rota.claims @@ -0,0 +1,11 @@ +; The planner's questions, put to both policies. + +(load "on-call-rota.lib.writ") + +(property rota-exists + "six weeks can be covered under the policy" + (possible complete)) + +(property no-dead-end-prefix + "from every partial rota, a complete one can still be reached" + (live complete)) diff --git a/on-call-rota/on-call-rota.lib.writ b/on-call-rota/on-call-rota.lib.writ new file mode 100644 index 0000000..9829986 --- /dev/null +++ b/on-call-rota/on-call-rota.lib.writ @@ -0,0 +1,7 @@ +; 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 complete + (and (defined w1.primary) (defined w2.primary) (defined w3.primary) + (defined w4.primary) (defined w5.primary) (defined w6.primary))) diff --git a/on-call-rota/on-call-rota.rules b/on-call-rota/on-call-rota.rules new file mode 100644 index 0000000..54270a4 --- /dev/null +++ b/on-call-rota/on-call-rota.rules @@ -0,0 +1,22 @@ +; 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 "on-call-rota.lib.writ") + +(satisfies rota-exists complete) +(can-reach can-complete rota-exists) +(trapped no-dead-end-prefix can-complete) + +; ---- the rotas, as rows ---- +; Every complete rota, one row per week: the situation that IS the rota, the +; week, and its primary. A query cannot say this (its binders cannot be +; compared, and a rota is a join); a rule can. +(relation rota (Situation week person)) +(rule (rota S W P) + (rota-exists S) + (holds S (is W.primary P))) diff --git a/on-call-rota/on-call-rota.writ b/on-call-rota/on-call-rota.writ new file mode 100644 index 0000000..72a3192 --- /dev/null +++ b/on-call-rota/on-call-rota.writ @@ -0,0 +1,114 @@ +; An on-call rota: six weeks, four people, the policy as written. +; +; Every week needs a primary. Nobody does two weeks in a row, or more than two +; weeks in the six, or a week they are on leave. Dan joined last month and may +; not be primary until his second month, weeks 5 and 6. +; +; `writ check` exits 1 on this file. A rota exists, and its witness IS the +; rota; but one first assignment leaves no way to finish. See the README. + +(load "stdlib.writ") +(load "on-call-rota.lib.writ") + +(schema on-call-rota + + (type yn (no yes)) + + ; How many weeks someone has taken so far. The policy caps it at two, so the + ; count is a three-step scale; the top step has no `up`, so a third week is + ; not refused but absent: there is no value to move to. + (type level (arrow up (to level) fixed vacatable)) + + ; Six weeks, filled in order. `next` is the ladder; the last week has none. + ; `late` marks the weeks a new joiner may take: their second month. + (type week + (arrow next (to week) fixed vacatable) + (arrow late (to yn) fixed) + (maybe primary person)) + + (type person + (arrow new (to yn) fixed) + (arrow leave (to week) fixed vacatable) + (arrow back (to week) fixed vacatable) ; the week they return + (arrow load (to level))) + + ; Where the planner is: the week being filled, or `done`. + (type cursor (arrow at (to week) vacatable))) + +(instance start on-call-rota + + (level l0 (up l1)) + (level l1 (up l2)) + (level l2 (up vacant)) + + (week w1 (next w2) (late no) (primary vacant)) + (week w2 (next w3) (late no) (primary vacant)) + (week w3 (next w4) (late no) (primary vacant)) + (week w4 (next w5) (late no) (primary vacant)) + (week w5 (next w6) (late yes) (primary vacant)) + (week w6 (next done) (late yes) (primary vacant)) + ; Past the last week. The cursor lands here when the rota is complete, and + ; no move fills it: its `next` is vacant, so an assignment to it is absent. + (week done (next vacant) (late no) (primary vacant)) + + (person ann (new no) (leave vacant) (back vacant) (load l0)) + (person bob (new no) (leave w3) (back w4) (load l0)) ; away in week 3 + (person cat (new no) (leave w4) (back w5) (load l0)) ; away in week 4 + (person dan (new yes) (leave vacant) (back vacant) (load l0)) ; joined last month + + (cursor cur (at w1))) + +(use on-call-rota) +(initial start) + +; ---- the policy ---- +; +; Person P is primary for week W, whose previous week is PREV: +; - not on leave that week; +; - not primary the week before (nobody does two in a row); +; - a new joiner only in their second month; +; - at most two weeks in the six: carried by the load scale, whose `up` +; runs out after two. +; Week 1 has no previous week; it passes itself as PREV, whose primary is +; still empty when it is being filled. +(form (assign N P W PREV) + (transition N + (when (and (is cur.at W) + (not (is P.leave W)) + (not (is PREV.primary P)) + (or (is P.new no) (is W.late yes)))) + (do (set W.primary P) (set P.load P.load.up) (set cur.at W.next)))) + +; The week before someone's leave. Whether the primary may hand over straight +; into their own leave, with nobody back the next week to answer for what they +; did, the policy does not say. So it is not a move but a question: a gap, +; reported with its route, for whoever owns the policy to answer. +(form (handover-into-leave N P W PREV) + (transition N + (when (and (is cur.at W) (not (is PREV.primary P)))) + (do (gap "the policy does not say whether a primary may hand over straight into their own leave")))) + +(assign ann-takes-w1 ann w1 w1) +(assign bob-takes-w1 bob w1 w1) +(assign cat-takes-w1 cat w1 w1) +(assign dan-takes-w1 dan w1 w1) +(assign ann-takes-w2 ann w2 w1) +(handover-into-leave bob-takes-w2 bob w2 w1) +(assign cat-takes-w2 cat w2 w1) +(assign dan-takes-w2 dan w2 w1) +(assign ann-takes-w3 ann w3 w2) +(assign bob-takes-w3 bob w3 w2) +(handover-into-leave cat-takes-w3 cat w3 w2) +(assign dan-takes-w3 dan w3 w2) +(assign ann-takes-w4 ann w4 w3) +(assign bob-takes-w4 bob w4 w3) +(assign cat-takes-w4 cat w4 w3) +(assign dan-takes-w4 dan w4 w3) +(assign ann-takes-w5 ann w5 w4) +(assign bob-takes-w5 bob w5 w4) +(assign cat-takes-w5 cat w5 w4) +(assign dan-takes-w5 dan w5 w4) +(assign ann-takes-w6 ann w6 w5) +(assign bob-takes-w6 bob w6 w5) +(assign cat-takes-w6 cat w6 w5) +(assign dan-takes-w6 dan w6 w5) diff --git a/run-tests.sh b/run-tests.sh index a62b794..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 eighteen scenarios this script walks by convention, and their 55 - # properties. Adding a property to any of the eighteen 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, and this line is where each of those had to be - # said out loud. - has "cross-check: all 55 properties of the eighteen scenarios were considered" \ - "$out" "considered 55 properties: 53 compared, 2 not compared" - # Two of the 55 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. @@ -746,9 +747,131 @@ config_space() { lacks "config-space: and only those" "$dv" "single" } +on_call_rota() { + d="$here/on-call-rota" + c="$d/on-call-rota.claims" + echo "== An on-call rota — does one exist, and what did the policy not say? ==" + echo " Q: six weeks, four people, the policy as written: is there a rota?" + out=$("$WRIT" check "$d/on-call-rota.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "on-call-rota: the policy reports a finding" "$st" 1 + has "on-call-rota: A. a rota exists" "$out" "holds rota-exists" + near "on-call-rota: and the witness IS the rota, week 1 first" "$out" "holds rota-exists" "1. ann-takes-w1" + has "on-call-rota: through to week 6" "$out" "6. bob-takes-w6" + has "on-call-rota: B. ten rotas in all, every one a dead end of six moves" "$out" "dead ends: 10" + has "on-call-rota: C. the policy is silent on handing over into leave, twice" "$out" "gaps: 2" + has "on-call-rota: Bob before his week away" "$out" "bob-takes-w2 — \"the policy does not say" + has "on-call-rota: D. and one first assignment strands the planner" "$out" "fails no-dead-end-prefix" + near "on-call-rota: giving Cat week 1" "$out" "fails no-dead-end-prefix" "1. cat-takes-w1" + + sc=$("$WRIT" check "$d/on-call-rota-strict.writ" --claims "$c" 2>&1) + printf '%s\n' "$sc" | sed 's/^/ | /' + has "on-call-rota: E. one more rule, and no rota exists" "$sc" "fails rota-exists" + # How far it gets: three weeks. Week 4 has nobody left, which is the + # argument the README spells out, ending at the gap. + has "on-call-rota: every attempt stops after week 3" "$sc" "reached by: ann-takes-w1, cat-takes-w2, ann-takes-w3" + has "on-call-rota: unless the gap is answered" "$sc" "cat-takes-w3 — \"the policy does not say" + + cmp=$("$WRIT" compare "$d/on-call-rota.writ" "$d/on-call-rota-strict.writ" 2>&1) + has "on-call-rota: F. compare: the rota is LOST, with no witness to give" "$cmp" "rota-exists LOST" + + dv=$("$WRIT" derive "$d/on-call-rota.writ" "$d/on-call-rota.rules" rota 2>&1) + has "on-call-rota: G. derive reads every rota out as rows" "$dv" "rota (60 rows)" + 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 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'):"