on-call-rota: does a valid rota exist, and what did the policy not say?

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. |

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.

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');

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');

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');

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.

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)))
+

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)

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)))

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)