From 22e82b3d2c09b1049c79b0bbf33ed069dbe1c863 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:52:27 +0300 Subject: [PATCH 1/3] on-call-rota: does a valid rota exist, and what did the policy not say? MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Six weeks, four people, leave, a new joiner, at most two weeks each — the cap carried by a scale whose top has no `up`, so a third week is absent. A rota exists and the witness is the rota; ten in all, read out by derive as rows. Handing over straight into one's own leave is a gap: the policy is silent. Giving Cat week 1 strands the planner at that gap. One more rule (not the week you come back) and no rota exists unless the gap is answered yes. Cross-check 55 -> 57 properties (55 compared); 280 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + docker-compose.yml | 6 + modality-cross-check.sh | 2 +- on-call-rota/README.md | 156 ++++++++++++++++++++++++++ on-call-rota/on-call-rota-strict.writ | 114 +++++++++++++++++++ on-call-rota/on-call-rota.claims | 11 ++ on-call-rota/on-call-rota.lib.writ | 7 ++ on-call-rota/on-call-rota.rules | 22 ++++ on-call-rota/on-call-rota.writ | 114 +++++++++++++++++++ run-tests.sh | 50 +++++++-- 10 files changed, 474 insertions(+), 9 deletions(-) create mode 100644 on-call-rota/README.md create mode 100644 on-call-rota/on-call-rota-strict.writ create mode 100644 on-call-rota/on-call-rota.claims create mode 100644 on-call-rota/on-call-rota.lib.writ create mode 100644 on-call-rota/on-call-rota.rules create mode 100644 on-call-rota/on-call-rota.writ 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/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..e468699 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 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..82fadad 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -293,18 +293,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The eighteen scenarios this script walks by convention, and their 55 - # properties. Adding a property to any of the eighteen fails this line, which is the point of it — + # The nineteen scenarios this script walks by convention, and their 57 + # properties. Adding a property to any of the nineteen fails this line, which is the point of it — # the 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, and this line is where each + # of those had to be said out loud. + has "cross-check: all 57 properties of the nineteen scenarios were considered" \ + "$out" "considered 57 properties: 55 compared, 2 not compared" + # Two of the 57 are not compared, and the count above is the only place that # 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 +746,43 @@ 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" +} + # 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 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'):" From 80a55e242c25fee3cee41ff36be7a7fac7439151 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:59:17 +0300 Subject: [PATCH 2/3] =?UTF-8?q?db-migration-problems:=20three=20more=20?= =?UTF-8?q?=E2=80=94=20change=20an=20enum,=20split=20a=20table,=20add=20a?= =?UTF-8?q?=20foreign=20key?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit change-an-enum: widening the CHECK is instant; the first WRITE of the new value is the migration, and the shortcut writes it while r1 still reads. split-a-table: dual write and backfill; the shortcut switches reads once the backfill has started — five steps, the longest route in the collection. add-a-foreign-key: NOT VALID spares the old rows, not the running code; adding it mid-rollout makes the old release's deletes fail, in two steps. writ sql reads CHECK … IN as an enum and REFERENCES as an arrow, as planned; it reads NOT VALID as a plain foreign key (identical output, --strict accepts it) while declining VALIDATE CONSTRAINT — asserted as found. The parent README's "the shortcut is always shorter" is now what was measured: shorter in two of six, never longer. Cross-check 57 -> 63 properties (61 compared); 305 checks. Co-Authored-By: Claude Opus 5.5 --- db-migration-problems/README.md | 37 ++++-- .../add-a-foreign-key/01-before.sql | 19 ++++ .../add-a-foreign-key/02-add-not-valid.sql | 26 +++++ .../add-a-foreign-key/03-validate.sql | 23 ++++ .../add-a-foreign-key/README.md | 77 +++++++++++++ .../add-a-foreign-key-shortcut.writ | 84 ++++++++++++++ .../add-a-foreign-key.claims | 18 +++ .../add-a-foreign-key.lib.writ | 13 +++ .../add-a-foreign-key/add-a-foreign-key.rules | 14 +++ .../add-a-foreign-key/add-a-foreign-key.writ | 88 ++++++++++++++ .../change-an-enum/01-before.sql | 12 ++ .../change-an-enum/02-add-value.sql | 14 +++ .../change-an-enum/README.md | 73 ++++++++++++ .../change-an-enum-shortcut.writ | 78 +++++++++++++ .../change-an-enum/change-an-enum.claims | 17 +++ .../change-an-enum/change-an-enum.lib.writ | 13 +++ .../change-an-enum/change-an-enum.rules | 14 +++ .../change-an-enum/change-an-enum.writ | 84 ++++++++++++++ .../split-a-table/01-before.sql | 13 +++ .../split-a-table/02-create-addresses.sql | 25 ++++ .../split-a-table/03-drop-column.sql | 18 +++ db-migration-problems/split-a-table/README.md | 72 ++++++++++++ .../split-a-table/split-a-table-shortcut.writ | 102 +++++++++++++++++ .../split-a-table/split-a-table.claims | 19 ++++ .../split-a-table/split-a-table.lib.writ | 13 +++ .../split-a-table/split-a-table.rules | 14 +++ .../split-a-table/split-a-table.writ | 107 ++++++++++++++++++ modality-cross-check.sh | 2 +- run-tests.sh | 105 +++++++++++++++-- 29 files changed, 1177 insertions(+), 17 deletions(-) create mode 100644 db-migration-problems/add-a-foreign-key/01-before.sql create mode 100644 db-migration-problems/add-a-foreign-key/02-add-not-valid.sql create mode 100644 db-migration-problems/add-a-foreign-key/03-validate.sql create mode 100644 db-migration-problems/add-a-foreign-key/README.md create mode 100644 db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ create mode 100644 db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims create mode 100644 db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ create mode 100644 db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules create mode 100644 db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ create mode 100644 db-migration-problems/change-an-enum/01-before.sql create mode 100644 db-migration-problems/change-an-enum/02-add-value.sql create mode 100644 db-migration-problems/change-an-enum/README.md create mode 100644 db-migration-problems/change-an-enum/change-an-enum-shortcut.writ create mode 100644 db-migration-problems/change-an-enum/change-an-enum.claims create mode 100644 db-migration-problems/change-an-enum/change-an-enum.lib.writ create mode 100644 db-migration-problems/change-an-enum/change-an-enum.rules create mode 100644 db-migration-problems/change-an-enum/change-an-enum.writ create mode 100644 db-migration-problems/split-a-table/01-before.sql create mode 100644 db-migration-problems/split-a-table/02-create-addresses.sql create mode 100644 db-migration-problems/split-a-table/03-drop-column.sql create mode 100644 db-migration-problems/split-a-table/README.md create mode 100644 db-migration-problems/split-a-table/split-a-table-shortcut.writ create mode 100644 db-migration-problems/split-a-table/split-a-table.claims create mode 100644 db-migration-problems/split-a-table/split-a-table.lib.writ create mode 100644 db-migration-problems/split-a-table/split-a-table.rules create mode 100644 db-migration-problems/split-a-table/split-a-table.writ diff --git a/db-migration-problems/README.md b/db-migration-problems/README.md index 8add075..c9f4b50 100644 --- a/db-migration-problems/README.md +++ b/db-migration-problems/README.md @@ -1,28 +1,42 @@ # Database migration problems -Three schema changes that look routine, each with a plan that reads correctly +Six schema changes that look routine, each with a plan that reads correctly and goes wrong anyway, mid-rollout. Each directory writes the expand/contract plan down as a writ model and checks it at every instant, including while two releases serve traffic at once. The safe plan passes. A "shortcut" with one -condition removed fails, and writ names the broken rule and the shortest route -to it. +condition removed or weakened fails, and writ names the broken rule and the +shortest route to it. | problem | the mistake | route to the fault | | --- | --- | --- | | [`drop-a-column/`](drop-a-column/) | dropping a column while a release that reads it is still live | 2 moves | +| [`add-a-foreign-key/`](add-a-foreign-key/) | adding the key `NOT VALID` while the old code still makes orphans | 2 moves | | [`add-a-required-column/`](add-a-required-column/) | adding `NOT NULL` before every live release writes the column | 3 moves | +| [`change-an-enum/`](change-an-enum/) | writing the new value while a release that cannot read it is live | 3 moves | | [`rename-a-column/`](rename-a-column/) | switching readers to the new column before the backfill finishes | 4 moves | +| [`split-a-table/`](split-a-table/) | switching reads to the new table once the backfill has *started* | 5 moves | Start with `drop-a-column/`, the smallest. Each directory holds the SQL for each step (with one representative row), the safe plan, the shortcut, one `.claims` file asked of both, and a `.rules` file that answers the same questions through `writ derive` as a cross-check (`../modality-cross-check.sh`). -What the three share: the shortcut is always shorter, because the removed -condition is always a wait. It still completes and never gets stuck, so every -question except "is it safe on the way" answers in its favour. And in most of -them every SQL file is correct on its own; the mistake is in the order, which -no single file records. +What all six share: + +- **The mistake is in the order, not in a file.** Every SQL file is a valid + schema, and in most of them every statement is right. The defect is a step + allowed to start before another has finished, which no single file records. +- **The shortcut still completes and never gets stuck**, so every question + except "is it safe on the way" answers in its favour. +- **It is never slower.** The removed condition is always a wait. Measured as + the shortest route to a finished migration, the shortcut is shorter in two + of the six (`add-a-required-column`, 3 moves against 5; `rename-a-column`, + 8 against 9) and the same length in the other four. There it does not skip + a step: it allows the steps in an order the safe plan forbids. +- **`writ compare` is the wrong gate.** Both files of each pair declare the + same rules and ask the same questions, so compare reports everything + preserved. The shortcut breaks a rule rather than dropping one, and that is + what `check` finds. From any of the directories (here, `drop-a-column/`): @@ -35,3 +49,10 @@ To adapt one to your own migration, change the columns, what each release reads and writes (taken from the code, not the plan), and the steps' `when` conditions. The rules are about columns and releases in general and usually carry over unchanged. + +What `writ sql` does with the newer steps is recorded where it matters: +`CHECK … IN` becomes an enumerated type (`change-an-enum/`), `REFERENCES` +becomes an arrow (`split-a-table/`), and `NOT VALID` is read as an ordinary +foreign key while `VALIDATE CONSTRAINT` is declined (`add-a-foreign-key/`). +A constraint's validation state is not part of a schema, so the models carry +it themselves. diff --git a/db-migration-problems/add-a-foreign-key/01-before.sql b/db-migration-problems/add-a-foreign-key/01-before.sql new file mode 100644 index 0000000..3e3e554 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/01-before.sql @@ -0,0 +1,19 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- orders.customer_id points at a customer, but nothing says so: there is no +-- foreign key. So the data has drifted. The code deployed today deletes a +-- customer without touching their orders, and order o2 below belongs to a +-- customer who no longer exists — an ORPHAN. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL +); + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); +INSERT INTO orders (id, customer_id) VALUES ('o2', 'c9'); diff --git a/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql b/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql new file mode 100644 index 0000000..33a9fca --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/02-add-not-valid.sql @@ -0,0 +1,26 @@ +-- STEP 1 — the constraint arrives, NOT VALID. +-- +-- A plain ADD CONSTRAINT … FOREIGN KEY scans the whole table under a lock, +-- and fails if any row is an orphan. NOT VALID skips the scan: rows already +-- there are not checked, but every INSERT, UPDATE and DELETE from now on is. +-- That last part is easy to miss, and it is the one that matters: the release +-- still running deletes customers without touching their orders, and from +-- this moment the database refuses those deletes. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL +); + +ALTER TABLE orders + ADD CONSTRAINT orders_customer_fk + FOREIGN KEY (customer_id) REFERENCES customers (id) + NOT VALID; + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); +INSERT INTO orders (id, customer_id) VALUES ('o2', 'c9'); diff --git a/db-migration-problems/add-a-foreign-key/03-validate.sql b/db-migration-problems/add-a-foreign-key/03-validate.sql new file mode 100644 index 0000000..580b61d --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/03-validate.sql @@ -0,0 +1,23 @@ +-- STEP 2 — the constraint is validated. +-- +-- VALIDATE CONSTRAINT scans the existing rows, without the heavy lock. It +-- fails if an orphan is left, so the orphans are deleted (or re-pointed) first; +-- order o2 is gone below. After this the database guarantees what the code +-- always assumed. +-- +-- `writ sql --strict` declines this ALTER: it changes the validation state of +-- a constraint, and a schema has no such state. The model carries it instead. + +CREATE TABLE customers ( + id uuid PRIMARY KEY +); + +CREATE TABLE orders ( + id uuid PRIMARY KEY, + customer_id uuid NOT NULL REFERENCES customers (id) +); + +ALTER TABLE orders VALIDATE CONSTRAINT orders_customer_fk; + +INSERT INTO customers (id) VALUES ('c1'); +INSERT INTO orders (id, customer_id) VALUES ('o1', 'c1'); diff --git a/db-migration-problems/add-a-foreign-key/README.md b/db-migration-problems/add-a-foreign-key/README.md new file mode 100644 index 0000000..4383f92 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/README.md @@ -0,0 +1,77 @@ +# Adding a foreign key NOT VALID: the rows are spared, the code is not + +`orders.customer_id` should point at a customer, and nothing enforces it. +The code deployed today deletes a customer and leaves their orders behind, so +the table has **orphans**. The textbook plan: + +1. deploy code that re-points a customer's orders before deleting them; +2. clean up the existing orphans; +3. add the foreign key `NOT VALID`: no table scan and no long lock; +4. `VALIDATE CONSTRAINT`: checks the old rows, under a lighter lock. + +`NOT VALID` is known as the safe way to add a foreign key, and it does spare +the rows already there. What it does not spare is the code still running. +From the moment the constraint exists, every write is checked, and the old +release's delete is now one the database refuses. + +## The model + +The SQL is [`01-before.sql`](01-before.sql) (order `o2` points at customer +`c9`, who does not exist), [`02-add-not-valid.sql`](02-add-not-valid.sql) and +[`03-validate.sql`](03-validate.sql). + +`writ sql` reads a foreign key's presence, not its validation state, and the +two `ALTER` statements show the difference: + +- `ADD CONSTRAINT … NOT VALID` is read as an ordinary foreign key, + `(fk customer-id customers)`. The output is the same with or without + `NOT VALID`, and `--strict` accepts it. The orphan row `o2 → c9` in that + file loads without complaint. +- `VALIDATE CONSTRAINT` is declined under `--strict`: "ALTER TABLE that adds + no constraint". + +So the model carries the state itself. [`add-a-foreign-key.writ`](add-a-foreign-key.writ) +has the constraint as `none`, `not-valid` or `validated`; the orders table's +orphans as `none` or `some`; and releases `r1`, which makes orphans, and `r2`, +which does not. + +Two rules: + +- `validated-means-no-orphans`: the database's own check, because + `VALIDATE CONSTRAINT` fails while an orphan is left; +- `enforced-means-every-writer-complies`: once the constraint is enforced at + all, no running release makes orphans. The database cannot check this one + ahead of time. It finds out on the first refused delete. + +The safe plan adds the constraint once the fleet has **settled** on r2. +[`add-a-foreign-key-shortcut.writ`](add-a-foreign-key-shortcut.writ) adds it +as soon as r2 is deploying. + +## What writ answers + +The safe plan exits 0. The shortcut, exit 1: + +``` +equation enforced-means-every-writer-complies + … + violated in 1 reachable situations witness: 1. deploy-r2 2. add-not-valid → #3 +``` + +Two steps. r1 is still serving, and from now until the rollout completes, +deleting a customer fails on every r1 instance. `validated-means-no-orphans` +is never broken: validation still waits for the cleanup. The half of the +plan everyone checks is fine. + +This is the shape of `../add-a-required-column/` again: a constraint the +database enforces on behalf of code that does not yet keep it. `NOT NULL` +there, a foreign key here: two costumes for one mistake. + +## Run it + +```sh +writ check add-a-foreign-key.writ --claims add-a-foreign-key.claims # exit 0 +writ check add-a-foreign-key-shortcut.writ --claims add-a-foreign-key.claims # exit 1 +``` + +Siblings: [`../change-an-enum/`](../change-an-enum/), +[`../split-a-table/`](../split-a-table/), and the first three. diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ new file mode 100644 index 0000000..97a2f1f --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key-shortcut.writ @@ -0,0 +1,84 @@ +; The same plan, with ONE CONDITION REMOVED from adding the constraint: it no +; longer waits for the rollout to settle. NOT VALID is the "safe" way to add a +; foreign key, so it feels safe to add early. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "add-a-foreign-key.lib.writ") + +(schema add-a-foreign-key + + (type yn (no yes)) + + ; The constraint's life: absent, enforced on new writes only (NOT VALID), + ; or validated. `writ sql` reads the schema, which has a foreign key or not; + ; this is the part of the database's state it does not carry. + (type fk-state (none not-valid validated)) + (type constraint (arrow state (to fk-state))) + + ; Whether any order points at a customer that does not exist. + (type amount (none some)) + (type table (arrow orphans (to amount))) + + ; r1 is today's code: deleting a customer leaves their orders behind. r2 + ; re-points them first. + (type release (arrow makes-orphans (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. A validated constraint means no orphans. The database's own check: + ; VALIDATE CONSTRAINT fails outright while one exists. + (equation validated-means-no-orphans + (not (and (is constraint.state validated) + (some (t table) (is t.orphans some))))) + + ; 2. Once the constraint is enforced at all, no running release makes + ; orphans: the database now refuses what that code does, and it fails in + ; production. The required-needs-every-writer shape of + ; ../add-a-required-column, in a third costume. + (equation enforced-means-every-writer-complies + (not (and (not (is constraint.state none)) + (some (f fleet) (or (is f.old.makes-orphans yes) + (is f.new.makes-orphans yes))))))) + +(instance start add-a-foreign-key + (constraint customer-fk (state none)) + (table orders-table (orphans some)) ; o2, in 01-before.sql + (release r1 (makes-orphans yes)) + (release r2 (makes-orphans no)) + (fleet prod (old r1) (new r1))) + +(use add-a-foreign-key) +(initial start) + +; ---- the runbook ---- + +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Delete or re-point the orphans. Only once nothing makes new ones. +(transition clean-orphans + (when (and (is orders-table.orphans some) settled (is prod.new r2))) + (do (set orders-table.orphans none))) + +; 02-add-not-valid.sql, as soon as r2 is deploying. NOT VALID is "the safe +; way to add a foreign key", and it does skip the old rows. +(transition add-not-valid + (when (and (is customer-fk.state none) (is prod.new r2))) ; <- settled, gone + (do (set customer-fk.state not-valid))) + +; 03-validate.sql. The database refuses it while an orphan is left. +(transition validate + (when (and (is customer-fk.state not-valid) (is orders-table.orphans none))) + (do (set customer-fk.state validated))) + diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims new file mode 100644 index 0000000..30141b9 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.claims @@ -0,0 +1,18 @@ +; The questions, put to both plans. + +(load "add-a-foreign-key.lib.writ") + +(property completes + "the constraint can end up validated, with no orphans and the fleet settled on r2" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept clean-orphans validated-means-no-orphans) +(accept add-not-valid validated-means-no-orphans enforced-means-every-writer-complies) +(accept validate validated-means-no-orphans enforced-means-every-writer-complies) +(accept deploy-r2 enforced-means-every-writer-complies) +(accept settle enforced-means-every-writer-complies) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ new file mode 100644 index 0000000..787523b --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.lib.writ @@ -0,0 +1,13 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the constraint validated, no orphans, the fleet settled +; on r2. (Old and new spelled out rather than `settled`, which compares two +; paths and so cannot appear in a .rules guard.) +(form done (and (is customer-fk.state validated) + (is orders-table.orphans none) + (is prod.old r2) (is prod.new r2))) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules new file mode 100644 index 0000000..9c28cb5 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.rules @@ -0,0 +1,14 @@ +; The same two questions, answered a second time by a different part of `writ`, +; so that `modality-cross-check.sh` can compare them. A disagreement is a bug in +; one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "add-a-foreign-key.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ new file mode 100644 index 0000000..d8a65e1 --- /dev/null +++ b/db-migration-problems/add-a-foreign-key/add-a-foreign-key.writ @@ -0,0 +1,88 @@ +; Adding a foreign key to a table that has drifted. +; +; orders.customer_id should point at a customer, and today nothing enforces it, +; so some orders are orphans. The textbook plan: deploy code that stops making +; orphans, clean up the old ones, add the constraint NOT VALID (no table scan, +; no long lock), then VALIDATE it. NOT VALID spares the rows already there. It +; does not spare the code still running. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "add-a-foreign-key.lib.writ") + +(schema add-a-foreign-key + + (type yn (no yes)) + + ; The constraint's life: absent, enforced on new writes only (NOT VALID), + ; or validated. `writ sql` reads the schema, which has a foreign key or not; + ; this is the part of the database's state it does not carry. + (type fk-state (none not-valid validated)) + (type constraint (arrow state (to fk-state))) + + ; Whether any order points at a customer that does not exist. + (type amount (none some)) + (type table (arrow orphans (to amount))) + + ; r1 is today's code: deleting a customer leaves their orders behind. r2 + ; re-points them first. + (type release (arrow makes-orphans (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. A validated constraint means no orphans. The database's own check: + ; VALIDATE CONSTRAINT fails outright while one exists. + (equation validated-means-no-orphans + (not (and (is constraint.state validated) + (some (t table) (is t.orphans some))))) + + ; 2. Once the constraint is enforced at all, no running release makes + ; orphans: the database now refuses what that code does, and it fails in + ; production. The required-needs-every-writer shape of + ; ../add-a-required-column, in a third costume. + (equation enforced-means-every-writer-complies + (not (and (not (is constraint.state none)) + (some (f fleet) (or (is f.old.makes-orphans yes) + (is f.new.makes-orphans yes))))))) + +(instance start add-a-foreign-key + (constraint customer-fk (state none)) + (table orders-table (orphans some)) ; o2, in 01-before.sql + (release r1 (makes-orphans yes)) + (release r2 (makes-orphans no)) + (fleet prod (old r1) (new r1))) + +(use add-a-foreign-key) +(initial start) + +; ---- the runbook ---- + +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Delete or re-point the orphans. Only once nothing makes new ones. +(transition clean-orphans + (when (and (is orders-table.orphans some) settled (is prod.new r2))) + (do (set orders-table.orphans none))) + +; 02-add-not-valid.sql. Once the fleet has SETTLED on the code that complies: +; NOT VALID spares the old rows, not the running code. +(transition add-not-valid + (when (and (is customer-fk.state none) settled (is prod.new r2))) + (do (set customer-fk.state not-valid))) + +; 03-validate.sql. The database refuses it while an orphan is left. +(transition validate + (when (and (is customer-fk.state not-valid) (is orders-table.orphans none))) + (do (set customer-fk.state validated))) + diff --git a/db-migration-problems/change-an-enum/01-before.sql b/db-migration-problems/change-an-enum/01-before.sql new file mode 100644 index 0000000..aa4911a --- /dev/null +++ b/db-migration-problems/change-an-enum/01-before.sql @@ -0,0 +1,12 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- A ticket is open or closed, and the database says so: the CHECK lists the +-- values. `writ sql` reads a CHECK … IN as an enumerated type, so the members +-- below are the members of a type, not a comment. + +CREATE TABLE tickets ( + id uuid PRIMARY KEY, + status text NOT NULL CHECK (status IN ('open', 'closed')) +); + +INSERT INTO tickets (id, status) VALUES ('t1', 'closed'); diff --git a/db-migration-problems/change-an-enum/02-add-value.sql b/db-migration-problems/change-an-enum/02-add-value.sql new file mode 100644 index 0000000..f285059 --- /dev/null +++ b/db-migration-problems/change-an-enum/02-add-value.sql @@ -0,0 +1,14 @@ +-- STEP 1 — the new value arrives. Tickets can now be archived. +-- +-- This is instantaneous and safe: widening a CHECK rewrites nothing, and no +-- row changes. The row below is the same ticket, still closed. The migration +-- in the sense that matters has not happened yet. It happens the first time +-- something WRITES 'archived', and every release still running then has to be +-- able to read it. + +CREATE TABLE tickets ( + id uuid PRIMARY KEY, + status text NOT NULL CHECK (status IN ('open', 'closed', 'archived')) +); + +INSERT INTO tickets (id, status) VALUES ('t1', 'closed'); diff --git a/db-migration-problems/change-an-enum/README.md b/db-migration-problems/change-an-enum/README.md new file mode 100644 index 0000000..9750d37 --- /dev/null +++ b/db-migration-problems/change-an-enum/README.md @@ -0,0 +1,73 @@ +# Adding a value to an enum, and writing it too early + +Tickets are `open` or `closed`, and the database says so with a `CHECK`. +The product wants a third state, `archived`. Widening the `CHECK` is +instantaneous and safe: no row changes. The code change is small too. The new +release knows the third value. + +The migration that matters is neither of those. It is the first time +something **writes** `'archived'`. Every release still running at that moment +has to be able to read it, and the old one maps the column onto a two-value +enum in code: an unknown value is a deserialisation error, on every read of +that row. + +## The model + +The SQL is [`01-before.sql`](01-before.sql) and +[`02-add-value.sql`](02-add-value.sql). `writ sql` reads a `CHECK … IN` as an +enumerated type, so the two steps differ in the type's members: + +``` +(type tickets-status (open closed)) ; 01-before.sql +(type tickets-status (open closed archived)) ; 02-add-value.sql +``` + +[`change-an-enum.writ`](change-an-enum.writ) carries the `CHECK` as one fact +(`allows-archived`), one ticket `t1`, and the fleet as two slots `old` and +`new` over releases `r1` (does not know `archived`) and `r2` (does). The moves +are `add-value`, `deploy-r2`, `settle`, and `archive-t1`: the first write. + +Two rules: + +- `check-allows`: no row holds a value the `CHECK` does not list. The loud + one: break it and the `UPDATE` fails at once; +- `readable`: no row holds a value a running release cannot read. The quiet + one: the `UPDATE` succeeds, and the failure is the next read by an old + instance. + +The safe plan switches the archive feature on once the fleet has **settled** +on r2. [`change-an-enum-shortcut.writ`](change-an-enum-shortcut.writ) switches +it on with the deploy. + +## What writ answers + +Both plans are asked the questions in +[`change-an-enum.claims`](change-an-enum.claims). The safe plan exits 0. The +shortcut, exit 1: + +``` +equation readable + can be broken by: deploy-r2, settle, archive-t1 (acknowledge in claims) + violated in 1 reachable situations witness: 1. add-value 2. deploy-r2 3. archive-t1 → #6 +``` + +Widen the `CHECK`, start the deploy, archive a ticket. r1 is still serving, +and every read of `t1` on an r1 instance fails until the rollout completes. +`check-allows` is satisfied throughout: the database allowed the value. Only +the rule it cannot check breaks. + +## What to take away + +For an enum, the schema change is not the migration: the first write of the +new value is. Gate that write, usually a feature flag, on the rollout having +finished, not on the code having shipped. + +## Run it + +```sh +writ check change-an-enum.writ --claims change-an-enum.claims # exit 0 +writ check change-an-enum-shortcut.writ --claims change-an-enum.claims # exit 1 +``` + +Siblings: [`../split-a-table/`](../split-a-table/), +[`../add-a-foreign-key/`](../add-a-foreign-key/), and the first three. diff --git a/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ b/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ new file mode 100644 index 0000000..b48afa1 --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum-shortcut.writ @@ -0,0 +1,78 @@ +; The same plan, with ONE CONDITION REMOVED from the first write: the +; archive feature turns on with the deploy instead of after it settles. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "change-an-enum.lib.writ") + +(schema change-an-enum + + (type yn (no yes)) + + ; The members as `writ sql` reads them from the final step's CHECK. + (type tickets-status (open closed archived)) + + ; The CHECK itself: whether the database accepts 'archived' yet. + (type check (arrow allows-archived (to yn))) + + (type ticket (arrow status (to tickets-status))) + + ; r1 is deployed today and maps the column onto a two-value enum in code: an + ; unknown value is a deserialisation error. r2 knows all three. + (type release (arrow knows-archived (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. The database refuses a value its CHECK does not list. It is the loud + ; rule: break it and the UPDATE fails at once. + (equation check-allows + (not (and (is ticket.status archived) + (some (c check) (is c.allows-archived no))))) + + ; 2. Every running release can read every row. The quiet rule: the UPDATE + ; succeeds, and the failure is the next read by an old instance. + (equation readable + (not (and (is ticket.status archived) + (some (f fleet) (or (is f.old.knows-archived no) + (is f.new.knows-archived no))))))) + +(instance start change-an-enum + (check status-check (allows-archived no)) + (ticket t1 (status closed)) + (release r1 (knows-archived no)) + (release r2 (knows-archived yes)) + (fleet prod (old r1) (new r1))) + +(use change-an-enum) +(initial start) + +; ---- the runbook ---- + +; Widen the CHECK (02-add-value.sql). Safe at any time: nothing writes the +; value yet. +(transition add-value + (when (is status-check.allows-archived no)) + (do (set status-check.allows-archived yes))) + +; Ship the code that knows the new value. +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Archive a closed ticket as soon as r2 is deploying: the feature ships with +; the code. +(transition archive-t1 + (when (and (is t1.status closed) + (is status-check.allows-archived yes) + (is prod.new r2))) ; <- settled, gone + (do (set t1.status archived))) + diff --git a/db-migration-problems/change-an-enum/change-an-enum.claims b/db-migration-problems/change-an-enum/change-an-enum.claims new file mode 100644 index 0000000..292653b --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.claims @@ -0,0 +1,17 @@ +; The questions, put to both plans. + +(load "change-an-enum.lib.writ") + +(property completes + "a ticket can end up archived, with the fleet settled on the release that knows the value" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept add-value check-allows) +(accept archive-t1 check-allows readable) +(accept deploy-r2 readable) +(accept settle readable) diff --git a/db-migration-problems/change-an-enum/change-an-enum.lib.writ b/db-migration-problems/change-an-enum/change-an-enum.lib.writ new file mode 100644 index 0000000..65f80ee --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.lib.writ @@ -0,0 +1,13 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the value exists, the fleet has settled on the release +; that knows it (old and new both r2, spelled without `settled`, which compares +; two paths and so cannot appear in a .rules guard), and a ticket is archived. +(form done (and (is status-check.allows-archived yes) + (is prod.old r2) (is prod.new r2) + (is t1.status archived))) diff --git a/db-migration-problems/change-an-enum/change-an-enum.rules b/db-migration-problems/change-an-enum/change-an-enum.rules new file mode 100644 index 0000000..bc07137 --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.rules @@ -0,0 +1,14 @@ +; The same two questions, answered a second time by a different part of `writ`, +; so that `modality-cross-check.sh` can compare them. A disagreement is a bug in +; one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "change-an-enum.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/change-an-enum/change-an-enum.writ b/db-migration-problems/change-an-enum/change-an-enum.writ new file mode 100644 index 0000000..b4a8eaa --- /dev/null +++ b/db-migration-problems/change-an-enum/change-an-enum.writ @@ -0,0 +1,84 @@ +; Adding a value to an enum — and writing it before every reader knows it. +; +; Tickets are open or closed, and the product wants a third state, archived. +; The schema change is trivial: widen the CHECK. The code change is trivial: +; r2 knows the new value. The trap is the first WRITE of 'archived' while r1, +; which maps the column onto a two-value enum, is still serving reads. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "change-an-enum.lib.writ") + +(schema change-an-enum + + (type yn (no yes)) + + ; The members as `writ sql` reads them from the final step's CHECK. + (type tickets-status (open closed archived)) + + ; The CHECK itself: whether the database accepts 'archived' yet. + (type check (arrow allows-archived (to yn))) + + (type ticket (arrow status (to tickets-status))) + + ; r1 is deployed today and maps the column onto a two-value enum in code: an + ; unknown value is a deserialisation error. r2 knows all three. + (type release (arrow knows-archived (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. The database refuses a value its CHECK does not list. It is the loud + ; rule: break it and the UPDATE fails at once. + (equation check-allows + (not (and (is ticket.status archived) + (some (c check) (is c.allows-archived no))))) + + ; 2. Every running release can read every row. The quiet rule: the UPDATE + ; succeeds, and the failure is the next read by an old instance. + (equation readable + (not (and (is ticket.status archived) + (some (f fleet) (or (is f.old.knows-archived no) + (is f.new.knows-archived no))))))) + +(instance start change-an-enum + (check status-check (allows-archived no)) + (ticket t1 (status closed)) + (release r1 (knows-archived no)) + (release r2 (knows-archived yes)) + (fleet prod (old r1) (new r1))) + +(use change-an-enum) +(initial start) + +; ---- the runbook ---- + +; Widen the CHECK (02-add-value.sql). Safe at any time: nothing writes the +; value yet. +(transition add-value + (when (is status-check.allows-archived no)) + (do (set status-check.allows-archived yes))) + +; Ship the code that knows the new value. +(transition deploy-r2 + (when (and settled (is prod.new r1))) + (do (set prod.new r2))) + +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Archive a closed ticket: the first write of the new value. The feature is +; switched on only once the fleet has SETTLED on r2. `allows-archived` is the +; condition the database would enforce anyway; `settled` is the one it cannot. +(transition archive-t1 + (when (and (is t1.status closed) + (is status-check.allows-archived yes) + (is prod.new r2) + settled)) + (do (set t1.status archived))) + diff --git a/db-migration-problems/split-a-table/01-before.sql b/db-migration-problems/split-a-table/01-before.sql new file mode 100644 index 0000000..b0eccf2 --- /dev/null +++ b/db-migration-problems/split-a-table/01-before.sql @@ -0,0 +1,13 @@ +-- STEP 0 — the schema as it stands in production today. +-- +-- A user has one address, and it lives on the users table. The product now +-- wants several addresses per user, so the address moves to a table of its +-- own. One representative user below. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL, + address text NOT NULL +); + +INSERT INTO users (id, email, address) VALUES ('u1', 'ada@example.com', '1 Main St'); diff --git a/db-migration-problems/split-a-table/02-create-addresses.sql b/db-migration-problems/split-a-table/02-create-addresses.sql new file mode 100644 index 0000000..559dd27 --- /dev/null +++ b/db-migration-problems/split-a-table/02-create-addresses.sql @@ -0,0 +1,25 @@ +-- STEP 1 — the new table arrives beside the old column. +-- +-- Nothing is moved yet. The code deployed next writes BOTH places (the +-- "dual write"), and a backfill copies the rows that existed before it. Until +-- the backfill finishes, the new table holds some addresses and not others, +-- and no row in this file says which: that is exactly what the model has to +-- carry as state of its own. Here, mid-backfill, Ada's address has not been +-- copied yet, so `addresses` has no row. +-- +-- `user_id REFERENCES users` is a foreign key, and `writ sql` reads it as an +-- arrow from an address to a user. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL, + address text NOT NULL +); + +CREATE TABLE addresses ( + id uuid PRIMARY KEY, + user_id uuid NOT NULL REFERENCES users (id), + address text NOT NULL +); + +INSERT INTO users (id, email, address) VALUES ('u1', 'ada@example.com', '1 Main St'); diff --git a/db-migration-problems/split-a-table/03-drop-column.sql b/db-migration-problems/split-a-table/03-drop-column.sql new file mode 100644 index 0000000..2a2b8e3 --- /dev/null +++ b/db-migration-problems/split-a-table/03-drop-column.sql @@ -0,0 +1,18 @@ +-- STEP 2 — the old column goes, once nothing reads or writes it. +-- +-- By now every address is in the new table: the backfill copied the old ones, +-- and every release deployed since step 1 writes there. + +CREATE TABLE users ( + id uuid PRIMARY KEY, + email text NOT NULL +); + +CREATE TABLE addresses ( + id uuid PRIMARY KEY, + user_id uuid NOT NULL REFERENCES users (id), + address text NOT NULL +); + +INSERT INTO users (id, email) VALUES ('u1', 'ada@example.com'); +INSERT INTO addresses (id, user_id, address) VALUES ('a1', 'u1', '1 Main St'); diff --git a/db-migration-problems/split-a-table/README.md b/db-migration-problems/split-a-table/README.md new file mode 100644 index 0000000..46e1f0a --- /dev/null +++ b/db-migration-problems/split-a-table/README.md @@ -0,0 +1,72 @@ +# Splitting a table: switching reads before the copy finishes + +A user's address moves out of `users` into a table of its own, so a user can +have several. The safe order is well known: create the new table; deploy code +that writes both places (the **dual write**); copy the rows that existed +before it (the **backfill**); switch reads to the new table; drop the old +column. + +The switch must wait for the backfill to *finish*. Nothing in any SQL file +says when that is. Until then the new table holds some addresses and not +others, and a read from it returns nothing for every user the backfill has +not reached yet. No error is raised: those users simply have no address. + +## The model + +The SQL is [`01-before.sql`](01-before.sql), +[`02-create-addresses.sql`](02-create-addresses.sql) and +[`03-drop-column.sql`](03-drop-column.sql). `writ sql` reads the new table's +`user_id uuid NOT NULL REFERENCES users (id)` as an arrow from an address to a +user: `(fk user-id users)`. + +How far the backfill has got is not in any file, so +[`split-a-table.writ`](split-a-table.writ) carries it as a cell: `filled` is +`no`, `partial` or `yes`. Not a row count. The rules only ever ask which of +those three it is. Three releases, each described by what its code reads and +writes: `r1` (old column only), `r2` (writes both, reads the old one), `r3` +(the new table only). + +Three rules: + +- `read-of-existing`: nobody reads a column that is gone; +- `no-lost-writes`: once the backfill has started, every running release + writes the new table too, or its writes land after the copy and are never + moved; +- `complete-before-read`: nobody reads the new table before it holds every + address. + +The safe plan deploys r3 once r2 has settled **and** `filled` is `yes`. +[`split-a-table-shortcut.writ`](split-a-table-shortcut.writ) deploys it once +the backfill has started. + +## What writ answers + +The safe plan exits 0. The shortcut, exit 1: + +``` +equation complete-before-read + … + violated in 3 reachable situations witness: 1. create-table 2. deploy-r2 3. settle 4. backfill-start 5. deploy-r3 → #6 +``` + +Five steps, the longest route to a fault in this collection, and every one is +in the runbook's order. The mistake is the word "started" where the runbook +meant "finished". The backfill in a real system takes hours, so that word +covers most of the migration's wall-clock time. + +## What to take away + +The migration's real state includes the progress of a job, and a job's +progress is exactly what no schema file records. Make it a fact the deploy +can check: a completion row the backfill writes last, for instance. Then gate +the switch on that row rather than on the job having been launched. + +## Run it + +```sh +writ check split-a-table.writ --claims split-a-table.claims # exit 0 +writ check split-a-table-shortcut.writ --claims split-a-table.claims # exit 1 +``` + +Siblings: [`../change-an-enum/`](../change-an-enum/), +[`../add-a-foreign-key/`](../add-a-foreign-key/), and the first three. diff --git a/db-migration-problems/split-a-table/split-a-table-shortcut.writ b/db-migration-problems/split-a-table/split-a-table-shortcut.writ new file mode 100644 index 0000000..9bb0e1e --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table-shortcut.writ @@ -0,0 +1,102 @@ +; The same plan, with ONE CONDITION WEAKENED: reads switch to the new table +; once the backfill has STARTED, not finished. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "split-a-table.lib.writ") + +(schema split-a-table + + (type yn (no yes)) + + ; users.address, the column that is moving out. + (type column (arrow present (to yn))) + + ; The new table. Whether it exists, and how much of it is filled: no, partly + ; (the backfill has started), or completely. Not a row count — the rules + ; only ever ask which of those three it is. + (type fill (no partial yes)) + (type table + (arrow exists (to yn)) + (arrow filled (to fill))) + + ; What each release does, taken from its code. r1 is today's. r2 writes + ; both places and still reads the old one. r3 uses only the new table. + (type release + (arrow reads-old (to yn) fixed) + (arrow reads-new (to yn) fixed) + (arrow writes-new (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. Nobody reads a column that is gone. + (equation read-of-existing + (not (and (is column.present no) + (some (f fleet) (or (is f.old.reads-old yes) (is f.new.reads-old yes)))))) + + ; 2. Once the backfill has started, every running release writes the new + ; table too; otherwise its writes land after the copy and are never moved. + (equation no-lost-writes + (not (and (not (is table.filled no)) + (some (f fleet) (or (is f.old.writes-new no) (is f.new.writes-new no)))))) + + ; 3. Nobody reads the new table before it holds every address. The one the + ; shortcut breaks: the reads succeed, and return nothing for the users the + ; backfill has not reached. + (equation complete-before-read + (not (and (not (is table.filled yes)) + (some (f fleet) (or (is f.old.reads-new yes) (is f.new.reads-new yes))))))) + +(instance start split-a-table + (column address-col (present yes)) + (table addresses (exists no) (filled no)) + (release r1 (reads-old yes) (reads-new no) (writes-new no)) + (release r2 (reads-old yes) (reads-new no) (writes-new yes)) + (release r3 (reads-old no) (reads-new yes) (writes-new yes)) + (fleet prod (old r1) (new r1))) + +(use split-a-table) +(initial start) + +; ---- the runbook ---- + +; 02-create-addresses.sql. +(transition create-table + (when (is addresses.exists no)) + (do (set addresses.exists yes))) + +; Dual write. +(transition deploy-r2 + (when (and settled (is prod.new r1) (is addresses.exists yes))) + (do (set prod.new r2))) + +; Every rollout ends the same way. +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Copy the addresses that existed before the dual write. Only once nothing +; still writes the old place alone. +(transition backfill-start + (when (and (is addresses.filled no) settled (is prod.new r2))) + (do (set addresses.filled partial))) +(transition backfill-finish + (when (is addresses.filled partial)) + (do (set addresses.filled yes))) + +; Switch reads to the new table once the backfill is under way: it is "nearly +; done", and r3 writes there too. +(transition deploy-r3 + (when (and settled (is prod.new r2) (not (is addresses.filled no)))) ; <- yes, weakened to "started" + (do (set prod.new r3))) + +; 03-drop-column.sql, once nothing reads it. +(transition drop-column + (when (and (is address-col.present yes) settled (is prod.new r3))) + (do (set address-col.present no))) + diff --git a/db-migration-problems/split-a-table/split-a-table.claims b/db-migration-problems/split-a-table/split-a-table.claims new file mode 100644 index 0000000..6f4b52c --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.claims @@ -0,0 +1,19 @@ +; The questions, put to both plans. + +(load "split-a-table.lib.writ") + +(property completes + "the move can finish: settled on r3, every address copied, the old column gone" + (possible done)) + +(property no-dead-ends + "from every reachable situation, that end can still be reached" + (live done)) + +; ---- ownership ---- +(accept deploy-r2 read-of-existing no-lost-writes complete-before-read) +(accept settle read-of-existing no-lost-writes complete-before-read) +(accept deploy-r3 read-of-existing no-lost-writes complete-before-read) +(accept drop-column read-of-existing) +(accept backfill-start no-lost-writes complete-before-read) +(accept backfill-finish no-lost-writes complete-before-read) diff --git a/db-migration-problems/split-a-table/split-a-table.lib.writ b/db-migration-problems/split-a-table/split-a-table.lib.writ new file mode 100644 index 0000000..571f293 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.lib.writ @@ -0,0 +1,13 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +(form settled (is prod.old prod.new)) +(form rolling (differ prod.old prod.new)) + +; Where we are going: the fleet settled on r3, every address in the new table, +; the old column gone. (Old and new are spelled out rather than `settled`, +; which compares two paths and so cannot appear in a .rules guard.) +(form done (and (is prod.old r3) (is prod.new r3) + (is addresses.filled yes) + (is address-col.present no))) diff --git a/db-migration-problems/split-a-table/split-a-table.rules b/db-migration-problems/split-a-table/split-a-table.rules new file mode 100644 index 0000000..d1345a7 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.rules @@ -0,0 +1,14 @@ +; The same two questions, answered a second time by a different part of `writ`, +; so that `modality-cross-check.sh` can compare them. A disagreement is a bug in +; one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `live F` is the COUNTEREXAMPLE set — EMPTY means it holds. +(load "ct.rules") +(load "split-a-table.lib.writ") + +(satisfies completes done) + +(can-reach can-still-finish completes) +(trapped no-dead-ends can-still-finish) diff --git a/db-migration-problems/split-a-table/split-a-table.writ b/db-migration-problems/split-a-table/split-a-table.writ new file mode 100644 index 0000000..f60a4e4 --- /dev/null +++ b/db-migration-problems/split-a-table/split-a-table.writ @@ -0,0 +1,107 @@ +; Splitting a table — dual write, backfill, switch, contract. +; +; The address moves from users to a table of its own. The safe order is the +; one everyone knows: create the table, deploy code that writes both places, +; copy the old rows, switch reads to the new table, drop the old column. The +; switch must wait for the copy to FINISH, and nothing in any SQL file says +; when that is. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "split-a-table.lib.writ") + +(schema split-a-table + + (type yn (no yes)) + + ; users.address, the column that is moving out. + (type column (arrow present (to yn))) + + ; The new table. Whether it exists, and how much of it is filled: no, partly + ; (the backfill has started), or completely. Not a row count — the rules + ; only ever ask which of those three it is. + (type fill (no partial yes)) + (type table + (arrow exists (to yn)) + (arrow filled (to fill))) + + ; What each release does, taken from its code. r1 is today's. r2 writes + ; both places and still reads the old one. r3 uses only the new table. + (type release + (arrow reads-old (to yn) fixed) + (arrow reads-new (to yn) fixed) + (arrow writes-new (to yn) fixed)) + + (type fleet + (arrow old (to release)) + (arrow new (to release))) + + ; ---- the rules ---- + + ; 1. Nobody reads a column that is gone. + (equation read-of-existing + (not (and (is column.present no) + (some (f fleet) (or (is f.old.reads-old yes) (is f.new.reads-old yes)))))) + + ; 2. Once the backfill has started, every running release writes the new + ; table too; otherwise its writes land after the copy and are never moved. + (equation no-lost-writes + (not (and (not (is table.filled no)) + (some (f fleet) (or (is f.old.writes-new no) (is f.new.writes-new no)))))) + + ; 3. Nobody reads the new table before it holds every address. The one the + ; shortcut breaks: the reads succeed, and return nothing for the users the + ; backfill has not reached. + (equation complete-before-read + (not (and (not (is table.filled yes)) + (some (f fleet) (or (is f.old.reads-new yes) (is f.new.reads-new yes))))))) + +(instance start split-a-table + (column address-col (present yes)) + (table addresses (exists no) (filled no)) + (release r1 (reads-old yes) (reads-new no) (writes-new no)) + (release r2 (reads-old yes) (reads-new no) (writes-new yes)) + (release r3 (reads-old no) (reads-new yes) (writes-new yes)) + (fleet prod (old r1) (new r1))) + +(use split-a-table) +(initial start) + +; ---- the runbook ---- + +; 02-create-addresses.sql. +(transition create-table + (when (is addresses.exists no)) + (do (set addresses.exists yes))) + +; Dual write. +(transition deploy-r2 + (when (and settled (is prod.new r1) (is addresses.exists yes))) + (do (set prod.new r2))) + +; Every rollout ends the same way. +(transition settle + (when rolling) + (do (set prod.old prod.new))) + +; Copy the addresses that existed before the dual write. Only once nothing +; still writes the old place alone. +(transition backfill-start + (when (and (is addresses.filled no) settled (is prod.new r2))) + (do (set addresses.filled partial))) +(transition backfill-finish + (when (is addresses.filled partial)) + (do (set addresses.filled yes))) + +; Switch reads to the new table: once r2 has settled AND the backfill has +; finished. +(transition deploy-r3 + (when (and settled (is prod.new r2) (is addresses.filled yes))) + (do (set prod.new r3))) + +; 03-drop-column.sql, once nothing reads it. +(transition drop-column + (when (and (is address-col.present yes) settled (is prod.new r3))) + (do (set address-col.present no))) + diff --git a/modality-cross-check.sh b/modality-cross-check.sh index e468699..bbc9a2e 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments config-space on-call-rota" +scenarios="river island queens jobshop-possible jobshop-best arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column db-migration-problems/change-an-enum db-migration-problems/split-a-table db-migration-problems/add-a-foreign-key entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments config-space on-call-rota" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index 82fadad..167d58a 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -293,18 +293,19 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The nineteen scenarios this script walks by convention, and their 57 - # properties. Adding a property to any of the nineteen fails this line, which is the point of it — + # The twenty-two scenarios this script walks by convention, and their 63 + # properties. Adding a property to any of the twenty-two fails this line, which is the point of it — # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, # 26 -> 31 with two-phase-commit, 31 -> 41 with the three # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, 52 -> 56 with # payments, 56 -> 60 with config-space, 60 -> 55 as oversight, workflow - # and access left, 55 -> 57 with on-call-rota, and this line is where each - # of those had to be said out loud. - has "cross-check: all 57 properties of the nineteen scenarios were considered" \ - "$out" "considered 57 properties: 55 compared, 2 not compared" - # Two of the 57 are not compared, and the count above is the only place that + # and access left, 55 -> 57 with on-call-rota, 57 -> 63 with the second + # batch of db-migration-problems (2 + 2 + 2), and this line is where each of + # those had to be said out loud. + has "cross-check: all 63 properties of the twenty-two scenarios were considered" \ + "$out" "considered 63 properties: 61 compared, 2 not compared" + # Two of the 63 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -780,9 +781,97 @@ on_call_rota() { has "on-call-rota: one row per week" "$dv" "17 w6 bob" } +change_an_enum() { + d="$here/db-migration-problems/change-an-enum" + echo "== Adding a value to an enum — and writing it before every reader knows it ==" + echo " Q: widening a CHECK is instant. When is the migration, really?" + has "change-an-enum: writ sql reads the CHECK as two members before" \ + "$("$WRIT" sql "$d/01-before.sql" 2>/dev/null)" "(type tickets-status (open closed))" + has "change-an-enum: and three after" \ + "$("$WRIT" sql "$d/02-add-value.sql" 2>/dev/null)" "(type tickets-status (open closed archived))" + + ok_=$("$WRIT" check "$d/change-an-enum.writ" --claims "$d/change-an-enum.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "change-an-enum: the plan is clean" "$ost" 0 + has "change-an-enum: A. a ticket can be archived" "$ok_" "holds completes" + lacks "change-an-enum: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/change-an-enum-shortcut.writ" --claims "$d/change-an-enum.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "change-an-enum: archiving during the rollout is refused" "$sst" 1 + has "change-an-enum: B. the first write of the value, while r1 still reads" "$sc" \ + "violated in 1 reachable situations witness: 1. add-value 2. deploy-r2 3. archive-t1" + # The database's own check is satisfied throughout: the value is allowed. + nviol=$(printf '%s\n' "$sc" | grep -c "violated in") + if [ "$nviol" = "1" ]; then + ok "change-an-enum: C. and only the rule the database cannot check breaks" + else + bad "change-an-enum: C. expected exactly one violated rule, got $nviol" + fi +} + +split_a_table() { + d="$here/db-migration-problems/split-a-table" + echo "== Splitting a table — dual write, backfill, switch, contract ==" + echo " Q: when may reads switch to the new table?" + has "split-a-table: writ sql reads the new table's foreign key as an arrow" \ + "$("$WRIT" sql "$d/02-create-addresses.sql" 2>/dev/null)" "(fk user-id users)" + + ok_=$("$WRIT" check "$d/split-a-table.writ" --claims "$d/split-a-table.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "split-a-table: the plan is clean" "$ost" 0 + has "split-a-table: A. the move can finish" "$ok_" "holds completes" + lacks "split-a-table: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/split-a-table-shortcut.writ" --claims "$d/split-a-table.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "split-a-table: switching on a started backfill is refused" "$sst" 1 + # The longest route to a fault in the collection: five steps, every one of + # them in the runbook's order. + has "split-a-table: B. reads switch to a half-filled table, five steps in" "$sc" \ + "violated in 3 reachable situations witness: 1. create-table 2. deploy-r2 3. settle 4. backfill-start 5. deploy-r3" + has "split-a-table: and it is the completeness rule that breaks" "$sc" "equation complete-before-read" +} + +add_a_foreign_key() { + d="$here/db-migration-problems/add-a-foreign-key" + echo "== Adding a foreign key, NOT VALID — the rows are spared, the code is not ==" + echo " Q: NOT VALID skips the old rows. Does it make adding the key safe?" + # Recorded as found: writ sql reads NOT VALID as an ordinary foreign key — + # the output is the same with or without it, and --strict accepts it — + # while it declines VALIDATE CONSTRAINT. The model carries the state. + "$WRIT" sql "$d/02-add-not-valid.sql" --with-data --strict >/dev/null 2>&1 + exit_is "add-a-foreign-key: writ sql accepts NOT VALID, as a plain foreign key" "$?" 0 + has "add-a-foreign-key: reading it as an arrow" \ + "$("$WRIT" sql "$d/02-add-not-valid.sql" 2>/dev/null)" "(fk customer-id customers)" + vs=$("$WRIT" sql "$d/03-validate.sql" --with-data --strict 2>&1) + vst=$? + exit_is "add-a-foreign-key: and declines VALIDATE CONSTRAINT under --strict" "$vst" 1 + has "add-a-foreign-key: saying why" "$vs" "ALTER TABLE that adds no constraint" + + ok_=$("$WRIT" check "$d/add-a-foreign-key.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) + ost=$? + printf '%s\n' "$ok_" | sed 's/^/ | /' + exit_is "add-a-foreign-key: the plan is clean" "$ost" 0 + has "add-a-foreign-key: A. the constraint can end up validated" "$ok_" "holds completes" + lacks "add-a-foreign-key: nothing is violated" "$ok_" "violated in" + + sc=$("$WRIT" check "$d/add-a-foreign-key-shortcut.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "add-a-foreign-key: adding it mid-rollout is refused" "$sst" 1 + has "add-a-foreign-key: B. two steps: the old code's deletes now fail" "$sc" \ + "violated in 1 reachable situations witness: 1. deploy-r2 2. add-not-valid" + has "add-a-foreign-key: the every-writer rule, a third time" "$sc" "equation enforced-means-every-writer-complies" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best two_phase_commit arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments config_space on_call_rota control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best two_phase_commit arch timetable rename_a_column drop_a_column add_a_required_column change_an_enum split_a_table add_a_foreign_key separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments config_space on_call_rota control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From e3f55ac70bed5e2d2260ac0b6ef91ae29ee8e1e1 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 21:14:44 +0300 Subject: [PATCH 3/3] follow writ's four fixes: n/a is a finding, compare loses a broken law, NOT VALID declined Assertions and READMEs that recorded the old behaviour now record the new: - agent-guardrails: the cheat that deletes `out` makes check exit 1 (was 0); - compare reports a law declared in both and broken in the new model as LOST with its route (rename-a-column's "the verb that does NOT catch it", drop, add-required, expense-approval, entitlement-problems, git-compare's one-capture); the migration READMEs no longer say compare is the wrong gate; - add-a-foreign-key: writ sql declines NOT VALID (exit 1 under --strict) and VALIDATE CONSTRAINT, each with its reason. Needs writ with branch writ-gaps; 306 checks against it. Co-Authored-By: Claude Opus 5.5 --- agent-guardrails/README.md | 16 +++--- db-migration-problems/README.md | 16 +++--- .../add-a-foreign-key/README.md | 27 ++++++---- .../add-a-required-column/README.md | 4 +- db-migration-problems/drop-a-column/README.md | 11 ++-- .../rename-a-column/README.md | 11 ++-- entitlement-problems/README.md | 9 ++-- expense-approval/README.md | 10 ++-- run-tests.sh | 51 ++++++++++--------- 9 files changed, 86 insertions(+), 69 deletions(-) diff --git a/agent-guardrails/README.md b/agent-guardrails/README.md index b551dcb..f34dcbf 100644 --- a/agent-guardrails/README.md +++ b/agent-guardrails/README.md @@ -144,12 +144,13 @@ certified: every answer re-derived from the model (writ-cert) ``` `n/a` means the question names something the model no longer has, so it was -not answered. **`writ check` exits 0 on this file.** No property failed, -because the one that would have was taken away. A harness that gates on that -exit code has just been talked out of its question. +not answered. No property failed, because the one that would have was taken +away. That is why `writ check` treats an `n/a` as a finding and **exits 1** on +this file: a gate that reads the exit status cannot be talked out of its +question. (Earlier versions of writ exited 0 here. This scenario is how that +was found.) -So treat `n/a` as a failure, and gate on `compare` against the last version -the human approved, which refuses it: +`compare` against the last version the human approved says what was taken: ```sh writ compare agent-guardrails.writ attempt-forget-out.writ # exit 1 @@ -166,7 +167,8 @@ properties: useful preserved writ's MCP server already enforces both halves. It reads `.claims` from the human's directory whatever path the agent passes, and it reports what each edit lost, `n/a` included (see writ's `docs/mcp.md`). From the command line, -`--json` carries `"verdict": "n/a"` for a script to refuse. +`check` exits 1 on an `n/a`, and `--json` carries `"verdict": "n/a"` for a +script that wants to say why. ## What to take away @@ -185,7 +187,7 @@ give the secret the places it can come from, and write the policy as ```sh writ check agent-guardrails.writ --claims agent-guardrails.claims # exit 0 writ compare agent-guardrails.writ agent-guardrails-v2.writ # exit 1 -writ check attempt-forget-out.writ --claims agent-guardrails.claims # exit 0, and two n/a +writ check attempt-forget-out.writ --claims agent-guardrails.claims # exit 1: two n/a writ compare agent-guardrails.writ attempt-forget-out.writ # exit 1 ``` diff --git a/db-migration-problems/README.md b/db-migration-problems/README.md index c9f4b50..ee676d2 100644 --- a/db-migration-problems/README.md +++ b/db-migration-problems/README.md @@ -33,10 +33,11 @@ What all six share: 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. +- **Both gates catch it.** The shortcut breaks a rule rather than dropping + one. `check` reports the violation, and `writ compare` against the safe + plan reports that rule `LOST` with the same route, since a rule declared in + both but broken in one is a guarantee lost. (Before writ counted that, compare + read "preserved" here, and these READMEs said to gate on `check`.) From any of the directories (here, `drop-a-column/`): @@ -52,7 +53,6 @@ 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. +becomes an arrow (`split-a-table/`), and `NOT VALID` and `VALIDATE CONSTRAINT` +are both declined, each saying why (`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/README.md b/db-migration-problems/add-a-foreign-key/README.md index 4383f92..e871b90 100644 --- a/db-migration-problems/add-a-foreign-key/README.md +++ b/db-migration-problems/add-a-foreign-key/README.md @@ -20,15 +20,24 @@ 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". +`writ sql` reads a foreign key's presence, not its validation state, and says +so for both `ALTER` statements: + +- `ADD CONSTRAINT … NOT VALID`: the key is read, `(fk customer-id customers)`, + and the clause is declined, because the model would otherwise claim the key + for rows the database never checked, like the orphan `o2 → c9` in that + file: + + ``` + declined: + 19: NOT VALID — the constraint is read, but rows already present are not checked by it, and writ reads it as holding for every row + ``` + + It is the one decline that makes a model stricter than the database rather + than laxer, which is why `--strict` fails on it. (Earlier versions of writ + dropped the clause without a word. This scenario is how that was found.) +- `VALIDATE CONSTRAINT` is declined too: it "changes whether a constraint has + been checked against existing rows, which a schema does not record". 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 diff --git a/db-migration-problems/add-a-required-column/README.md b/db-migration-problems/add-a-required-column/README.md index fdd7c36..e0da25e 100644 --- a/db-migration-problems/add-a-required-column/README.md +++ b/db-migration-problems/add-a-required-column/README.md @@ -91,8 +91,8 @@ through the broken situation. `required-needs-data`, the database's own check, is untouched; only the unwatched rule breaks. The shortcut is also faster, three steps against five, because it skips a deploy and a wait. -`writ compare` would report everything preserved, since the shortcut declares -the same rules. Gate on `check`. +`writ compare` against the safe plan agrees: `required-needs-every-writer` is +`LOST`, with the same three moves. The other two rules are preserved. ## What to take away diff --git a/db-migration-problems/drop-a-column/README.md b/db-migration-problems/drop-a-column/README.md index 1333a9b..0804faa 100644 --- a/db-migration-problems/drop-a-column/README.md +++ b/db-migration-problems/drop-a-column/README.md @@ -79,9 +79,14 @@ outage: start the deploy, drop the column, two moves. Both rules break, because the old release both reads and writes the column. The shortcut still completes and never gets stuck, so only the safety question catches it. -`writ compare` is the wrong gate here: the shortcut still declares both rules, -so compare reports everything preserved. It breaks a rule rather than dropping -one, and that is what `check` finds. +`writ compare drop-a-column.writ drop-a-column-shortcut.writ` agrees. The +shortcut still declares both rules, but it breaks them, so both are `LOST` +with the same two moves: + +``` +equations: read-of-existing LOST witness: 1. deploy-r2 2. drop-column + write-of-existing LOST witness: 1. deploy-r2 2. drop-column +``` ## What to take away diff --git a/db-migration-problems/rename-a-column/README.md b/db-migration-problems/rename-a-column/README.md index 7a50f52..f8f6921 100644 --- a/db-migration-problems/rename-a-column/README.md +++ b/db-migration-problems/rename-a-column/README.md @@ -117,21 +117,22 @@ moves reach one, and the last of them, `deploy-r3`, is the step at fault. The shortcut still completes, never gets stuck, and its route is eight steps instead of nine. -`writ compare` does not catch it, because the shortcut gives up none of the -guarantees it declares: +`writ compare` against the safe plan catches it too. The shortcut declares +the same rules, but one of them it now breaks, and a rule broken that the old +plan kept is a guarantee lost: ```console $ writ compare rename-a-column.writ rename-a-column-shortcut.writ equations: read-of-existing preserved write-of-existing preserved - read-of-filled preserved + read-of-filled LOST witness: 1. add-column 2. deploy-r2 3. settle 4. deploy-r3 read-implies-every-writer preserved properties: completes preserved no-dead-ends preserved ``` -`compare` asks which guarantees a version dropped; `check` asks whether it -keeps the ones it declares. Gate CI on `check`. +`check` says the shortcut breaks a rule; `compare` says which guarantee the +change from the safe plan gave up. Either is a gate for CI. ## What to take away diff --git a/entitlement-problems/README.md b/entitlement-problems/README.md index 442fdc2..643dbc8 100644 --- a/entitlement-problems/README.md +++ b/entitlement-problems/README.md @@ -34,11 +34,10 @@ What the three have in common: `writ compare` reports the difference between the two models of each pair as guarantees `LOST`, exit 1. In `scp-escalation/` that is the natural gate, -because the change *is* the difference: one administrative step added. One -caution: an equation that both files declare compares as `preserved` even when -one of them violates it (`separation` in `separation-of-duties/`), because -`compare` matches laws by declaration. Ask the safety question as a property -if `compare` is your gate. +because the change *is* the difference: one administrative step added. A law +both files declare and one of them breaks (`separation` in +`separation-of-duties/`) is reported `LOST` too, with the route to the +violation, so `compare` and `check` agree on every pair. From any of the directories (here, `separation-of-duties/`): diff --git a/expense-approval/README.md b/expense-approval/README.md index 9ce63d0..a0f88f7 100644 --- a/expense-approval/README.md +++ b/expense-approval/README.md @@ -133,18 +133,16 @@ writ compare expense-approval.writ expense-approval-shortcut.writ # exit 1 ``` equations: no-self-approval preserved finance-after-manager preserved - two-for-large preserved + two-for-large LOST witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay properties: payable preserved never-on-one-person LOST witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay always-settleable preserved settles preserved ``` -`two-for-large` reads `preserved` although the shortcut violates it. -`compare` matches laws by declaration, and both files declare it. The -property `never-on-one-person` asks the same thing as a question, and that -is what `compare` reports lost. If `compare` is your gate, ask your safety -rules as properties too. `check` catches both. +Both files declare `two-for-large`, and the shortcut breaks it, so `compare` +reports it lost with the same four steps as the property `never-on-one-person`, +which asks the same thing as a question. Either gate catches it. ## A question for whoever owns the process diff --git a/run-tests.sh b/run-tests.sh index 167d58a..31c0223 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -281,7 +281,9 @@ gitcompare() { printf '%s\n' "$out" | sed 's/^/ | /' exit_is "git-compare: the amendment loses a guarantee" "$st" 1 has "git-compare: never-double is LOST across the two commits" "$out" "never-double LOST" - has "git-compare: one-capture is preserved" "$out" "one-capture preserved" + # The law the amendment breaks, too: declared in both commits, violated in + # the second, so LOST with the same route. + has "git-compare: one-capture is LOST as well" "$out" "one-capture LOST" rm -rf "$tmp" } @@ -398,16 +400,18 @@ rename_a_column() { has "rename-a-column: D. yet it still finishes — faster, which is the trap" "$sc" "holds completes" has "rename-a-column: and it never strands you either" "$sc" "holds no-dead-ends" - echo " 4/4: the verb that does NOT catch it" + echo " 4/4: compare, against the safe plan" cm=$("$WRIT" compare "$here/db-migration-problems/rename-a-column/rename-a-column.writ" "$here/db-migration-problems/rename-a-column/rename-a-column-shortcut.writ" 2>&1) cst=$? printf '%s\n' "$cm" | sed 's/^/ | /' - exit_is "rename-a-column: compare is content" "$cst" 0 - has "rename-a-column: E. compare says the guarantees survived" "$cm" "preserved" - lacks "rename-a-column: nothing is reported LOST" "$cm" "LOST" - echo " — the shortcut declares the same laws and keeps the same" - echo " properties; what it loses is that one law it declares is now" - echo " VIOLATED. So the gate is \`check\`, not \`compare\`." + # The shortcut declares the same laws; what it loses is that one of them is + # now VIOLATED, and compare reports that as a guarantee lost, with the route + # check gives. (Before writ counted a newly violated law, this read + # "preserved" and the gate had to be check.) + exit_is "rename-a-column: compare refuses the shortcut too" "$cst" 1 + has "rename-a-column: E. the law it now breaks is LOST, with the route" "$cm" \ + "read-of-filled LOST witness: 1. add-column 2. deploy-r2 3. settle 4. deploy-r3" + has "rename-a-column: while the others survive" "$cm" "read-of-existing preserved" } drop_a_column() { @@ -577,9 +581,8 @@ expense_approval() { cmp=$("$WRIT" compare "$d/expense-approval.writ" "$d/expense-approval-shortcut.writ" 2>&1) has "expense-approval: F. compare reports the guarantee LOST" "$cmp" "never-on-one-person LOST" - # The law that breaks compares as preserved: compare matches laws by - # declaration, and both files declare it. The property is what catches it. - has "expense-approval: while the law it breaks compares as preserved" "$cmp" "two-for-large preserved" + # And the law it breaks: declared in both, violated in the shortcut, LOST. + has "expense-approval: and so is the law it breaks" "$cmp" "two-for-large LOST" dv=$("$WRIT" derive "$d/expense-approval-shortcut.writ" "$d/expense-approval.rules" paid-by 2>&1) has "expense-approval: G. derive lists who signed each payment" "$dv" "13 bob bob" @@ -628,11 +631,10 @@ agent_guardrails() { ch=$("$WRIT" check "$d/attempt-forget-out.writ" --claims "$c" 2>&1) chst=$? - # The cheat: delete what the question reads. `check` answers n/a and EXITS 0 - # — asserted as it is, since a harness that gates on this exit code is the - # failure the README warns about. + # The cheat: delete what the question reads. `check` answers n/a — and an + # unanswered question is a finding, so it exits 1 rather than reading clean. has "agent-guardrails: F. deleting the record makes the question n/a" "$ch" "n/a no-unapproved-exfiltration" - exit_is "agent-guardrails: and check alone exits clean" "$chst" 0 + exit_is "agent-guardrails: and check refuses it" "$chst" 1 cc=$("$WRIT" compare "$d/agent-guardrails.writ" "$d/attempt-forget-out.writ" 2>&1) ccst=$? exit_is "agent-guardrails: G. compare against v1 refuses it" "$ccst" 1 @@ -841,17 +843,18 @@ 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)" + # writ sql reads the constraint and declines NOT VALID — the model would + # otherwise claim it for rows the database never checked — and declines + # VALIDATE CONSTRAINT. The model carries the validation state itself. + nv=$("$WRIT" sql "$d/02-add-not-valid.sql" --with-data --strict 2>&1) + nvst=$? + exit_is "add-a-foreign-key: writ sql declines NOT VALID under --strict" "$nvst" 1 + has "add-a-foreign-key: saying what it means" "$nv" "NOT VALID — the constraint is read, but rows already" + has "add-a-foreign-key: and still reads the key as an arrow" "$nv" "(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" + exit_is "add-a-foreign-key: and declines VALIDATE CONSTRAINT" "$vst" 1 + has "add-a-foreign-key: saying why" "$vs" "VALIDATE CONSTRAINT — changes whether a constraint" ok_=$("$WRIT" check "$d/add-a-foreign-key.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) ost=$?