From 8112c62cdaaa90190a9e19dc3022500540e6503f Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 19:42:27 +0300 Subject: [PATCH 1/7] entitlement-problems: three access designs that leak a privilege through composition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit separation-of-duties: a toxic-combination table checked by group name, and a role added later that approves; two grants, neither listed, make a conflict. scp-escalation: moving prod into an OU built from the sandbox template; compare reports the CloudTrail guardrail and the security team's audit read LOST. joiner-mover-leaver: group-based offboarding and the direct permission set it cannot see; a trap, not a delay. Writing it, writ found a second bug in the first draft of the safe plan (approve, leave, provision) and the README keeps it. Each failing property names a (show …) query, and each .rules file prints the privilege path. Cross-check 31 -> 41 properties (never: 3 -> 7); 257 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + docker-compose.yml | 18 ++ entitlement-problems/README.md | 53 ++++++ .../joiner-mover-leaver/README.md | 174 ++++++++++++++++++ .../joiner-mover-leaver-shortcut.writ | 113 ++++++++++++ .../joiner-mover-leaver.claims | 36 ++++ .../joiner-mover-leaver.lib.writ | 11 ++ .../joiner-mover-leaver.rules | 39 ++++ .../joiner-mover-leaver.writ | 118 ++++++++++++ entitlement-problems/scp-escalation/README.md | 169 +++++++++++++++++ .../scp-escalation-restructured.writ | 95 ++++++++++ .../scp-escalation/scp-escalation.claims | 22 +++ .../scp-escalation/scp-escalation.lib.writ | 21 +++ .../scp-escalation/scp-escalation.rules | 30 +++ .../scp-escalation/scp-escalation.writ | 89 +++++++++ .../separation-of-duties/README.md | 173 +++++++++++++++++ .../separation-of-duties-shortcut.writ | 92 +++++++++ .../separation-of-duties.claims | 47 +++++ .../separation-of-duties.lib.writ | 27 +++ .../separation-of-duties.rules | 31 ++++ .../separation-of-duties.writ | 100 ++++++++++ modality-cross-check.sh | 2 +- run-tests.sh | 108 +++++++++-- 23 files changed, 1557 insertions(+), 12 deletions(-) create mode 100644 entitlement-problems/README.md create mode 100644 entitlement-problems/joiner-mover-leaver/README.md create mode 100644 entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ create mode 100644 entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims create mode 100644 entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ create mode 100644 entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules create mode 100644 entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ create mode 100644 entitlement-problems/scp-escalation/README.md create mode 100644 entitlement-problems/scp-escalation/scp-escalation-restructured.writ create mode 100644 entitlement-problems/scp-escalation/scp-escalation.claims create mode 100644 entitlement-problems/scp-escalation/scp-escalation.lib.writ create mode 100644 entitlement-problems/scp-escalation/scp-escalation.rules create mode 100644 entitlement-problems/scp-escalation/scp-escalation.writ create mode 100644 entitlement-problems/separation-of-duties/README.md create mode 100644 entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ create mode 100644 entitlement-problems/separation-of-duties/separation-of-duties.claims create mode 100644 entitlement-problems/separation-of-duties/separation-of-duties.lib.writ create mode 100644 entitlement-problems/separation-of-duties/separation-of-duties.rules create mode 100644 entitlement-problems/separation-of-duties/separation-of-duties.writ diff --git a/README.md b/README.md index 77f132c..4d7e2ae 100644 --- a/README.md +++ b/README.md @@ -52,6 +52,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`oversight/`](oversight/) | Can lawful moves permanently stop a case concluding? | Not as written; repeal one power and `writ compare` shows accountability **LOST**. | | [`workflow/`](workflow/) | Can a KYC case ever get stuck? | Never — and where automation ends, a declared gap hands it to a human. | | [`access/`](access/) | Can an admin grant always be revoked? | No: the break-glass grant is a latch. | +| [`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. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/docker-compose.yml b/docker-compose.yml index 41dfc88..754ec7a 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -59,6 +59,24 @@ services: image: writ-problems command: ["access"] + # Separation of duties: the toxic-combination table, and the role it misses. + separation-of-duties: + build: . + image: writ-problems + command: ["separation_of_duties"] + + # An OU move that leaves the guardrails behind — `writ compare` reports LOST. + scp-escalation: + build: . + image: writ-problems + command: ["scp_escalation"] + + # Group-based offboarding, and the direct grant that survives it. + joiner-mover-leaver: + build: . + image: writ-problems + command: ["joiner_mover_leaver"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/entitlement-problems/README.md b/entitlement-problems/README.md new file mode 100644 index 0000000..442fdc2 --- /dev/null +++ b/entitlement-problems/README.md @@ -0,0 +1,53 @@ +# Entitlement problems + +Three access-control designs, each with a control that reads correctly and +lets a privilege through anyway. Each directory writes the design down as a +writ model and checks every reachable configuration, not one access decision. +The safe version passes. A version with one condition removed (or, in +`scp-escalation/`, one administrative step added) fails, and writ names the +broken guarantee, the shortest sequence of grants or administrative steps +that reaches it, and who is affected. + +| problem | the mistake | route to the fault | +| --- | --- | --- | +| [`separation-of-duties/`](separation-of-duties/) | checking grants against a table of group names, when the conflict lives in a role | 2 grants | +| [`scp-escalation/`](scp-escalation/) | moving an account between OUs, which swaps the SCP guardrails out from under its roles | 1–2 steps | +| [`joiner-mover-leaver/`](joiner-mover-leaver/) | offboarding through groups, which cannot see a direct assignment | 4 steps | + +Start with `separation-of-duties/`. Each directory holds the two models, one +`.claims` file asked of both, a `.rules` file that answers the same questions +through `writ derive` as a cross-check (`../modality-cross-check.sh`) and +prints the privilege path as a table, and a README. + +What the three have in common: + +- **The mistake is never in one grant.** Every individual step is legitimate: + joining a group, assuming a role, moving an account, offboarding a leaver. + The privilege exists only in the composition. +- **The unsafe version still works.** People can still be given access and + deploys still ship, so every question except "is it safe at every step" + answers in its favour. +- **The answer is in the domain's vocabulary.** Each failing property names + a query with `(show …)`, so the verdict says *who* (`a = alice`, + `p = dev`, `e = prod-admin`), and each `.rules` file adds *through what*: + the two groups, the role → account → OU path, the grant marked `direct`. + +`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. + +From any of the directories (here, `separation-of-duties/`): + +```sh +writ check separation-of-duties.writ --claims separation-of-duties.claims # exit 0 +writ check separation-of-duties-shortcut.writ --claims separation-of-duties.claims # exit 1 +``` + +These are deliberately small, a few hundred situations at most, and each +README says what its reduction leaves out. A model built from a real IAM +export is the job of a bridge that reads the policies and writes the model. +That is a separate tool, not a scenario. diff --git a/entitlement-problems/joiner-mover-leaver/README.md b/entitlement-problems/joiner-mover-leaver/README.md new file mode 100644 index 0000000..ef5d742 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/README.md @@ -0,0 +1,174 @@ +# Joiner, mover, leaver: the grant offboarding cannot see + +Access follows a person through a job. They join and request access, someone +approves, and it is provisioned. Later they move to another team or leave, +and the access should go. The usual rule is "access is managed through +groups": provisioning adds the person to groups, and offboarding takes them +out. When the HR system's leaving date arrives, an automated integration +removes the person from every group the same day. + +That covers every grant made through a group. It does not cover the grant +made directly, on the day the request needed something no group yet mapped +to: the administrator permission set assigned to one person by name. +Offboarding works on groups, and nothing that works on groups can see it. + +## The model + +[`joiner-mover-leaver.writ`](joiner-mover-leaver.writ) follows one person and +one request: + +- **people**: `ada` (joins the platform team, needs production) and `bob` + (her manager), each with a `status` (`active`, `left`) and a `team` + (`platform`, `marketing`); +- **entitlements**: `prod-engineers`, the identity provider's production + group, which syncs to AWS, and `prod-admin`, the administrator permission + set assigned to Ada directly. Each records `via` (`group` or `direct`) and + its holder; +- **the request** `ada-prod`, with its stage (`none` → `requested` → + `approved` → `provisioned`) and its approver. + +The moves are the lifecycle: `ada-requests-prod`, `bob-approves` (and +`ada-approves`, whose guard refuses her own request), `provision-ada` (grants +both entitlements), `ada-moves-to-marketing` and `ada-leaves`. The mover and +leaver steps run their own deprovisioning in the same step, as an HR-driven +SCIM integration does. + +Two laws about the request hold in both plans: + +- `provisioned-means-approved`: nothing is provisioned that nobody approved; +- `no-self-approval`: the approver is not the requester. + +The two files differ in what deprovisioning removes. The safe plan removes +both entitlements: + +```lisp +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) +``` + +[`joiner-mover-leaver-shortcut.writ`](joiner-mover-leaver-shortcut.writ) +removes only the group membership, in both the mover and the leaver step. + +## What writ answers + +Both plans are asked the questions in +[`joiner-mover-leaver.claims`](joiner-mover-leaver.claims). The safe plan, +exit 0: + +``` +states: 16 edges: 19 +regime: committing — no move can be undone +… +holds ada-gets-access +holds movers-lose-prod +holds leavers-lose-everything +holds leavers-can-be-cut-off +certified: every answer re-derived from the model (writ-cert) +``` + +The shortcut, exit 1: + +``` +fails leavers-lose-everything + "nobody who has left ever holds production access" + witness: 1. ada-requests-prod → #1 ada-prod.stage: none → requested + 2. bob-approves → #4 ada-prod.stage: requested → approved, ada-prod.approver: ∅ → bob + 3. provision-ada → #8 prod-engineers.holder: ∅ → ada, prod-admin.holder: ∅ → ada, ada-prod.stage: approved → provisioned + 4. ada-leaves → #13 ada.status: active → left, prod-engineers.holder: ada → ∅ + stranded (at state 13) + e = prod-admin +fails leavers-can-be-cut-off + "from every reachable situation, a leaver can still end up holding nothing" + stuck at: #13 (ada.status=left … prod-engineers.holder=∅ prod-admin.holder=ada …) +``` + +Read the witness as an incident timeline. Each line says what changed. Step 4 +shows the leaver step doing its job: the group membership goes. The +administrator permission set is not in that line, because nothing removed it. +`stranded` answers the query the property names: what is left behind. + +`leavers-can-be-cut-off` fails as well, which makes this a **trap**, not a +delay. At situation 13 nothing that can still run touches a direct grant. No +later batch job or second pass will fix it, because there isn't one. The +mover fails the same way (`movers-lose-prod`, ending in +`ada-moves-to-marketing`). A person who changes team keeps production admin +indefinitely, which is how privilege creep happens. + +## What is left behind + +[`joiner-mover-leaver.rules`](joiner-mover-leaver.rules) lists every +entitlement held by someone with no business holding it, with how it was +granted: + +```sh +writ derive joiner-mover-leaver-shortcut.writ joiner-mover-leaver.rules left-behind +``` + +``` +left-behind (3 rows) + 12 prod-admin direct ada + 13 prod-admin direct ada + 15 prod-admin direct ada +``` + +The `via` column is the finding: every row says `direct`. + +## What writ found while this was being written + +The first draft of the safe plan had a second bug, and writ reported it before +the shortcut existed. `provision-ada` checked only that the request was +approved. The report, with each step's change column trimmed: + +``` +fails leavers-lose-everything + witness: 1. ada-requests-prod + 2. bob-approves + 3. ada-leaves + 4. provision-ada + stranded (at state 16) + e = prod-engineers + e = prod-admin +``` + +Approve, leave, *then* provision: an approval is a judgement about someone in +a role, and this one outlived the situation it judged. The fix, in both files, +is that provisioning re-checks the person (`ada.status active`, +`ada.team platform`) as well as the request. Queued provisioning jobs and +approvals that sit in a ticket for a week make this a real gap, and it is +easy to miss because every step is correct in the order the runbook shows. + +## Why the law is written from the entitlement's side + +"No leaver holds anything" would naturally be written about the person. writ +cannot put a type name on the right of `is`, so the property is written from +the other end of the arrow: no *entitlement* has a holder whose status is +`left`. The forms `held-by-leaver` and `held-outside-platform` in +[`joiner-mover-leaver.lib.writ`](joiner-mover-leaver.lib.writ) say so once, +for the claims and the rules alike. + +## What to take away + +The unsafe plan is the one the runbook describes, and it is right about every +grant it can see. The grant that survives was made outside the mechanism +offboarding relies on, for a good reason, on a busy day. The fix is either to +remove direct grants by name in every lifecycle step, as the safe plan does, +or to forbid them. Either way, the question to ask of the process is "can a +leaver still hold anything", not "did offboarding run". + +To adapt it, add an entitlement per system access can live in (Vault +policies, SaaS seats, SSH keys) with its real `via`, and say in each lifecycle +step what it actually removes. + +## Run it + +```sh +writ check joiner-mover-leaver.writ --claims joiner-mover-leaver.claims # exit 0 +writ check joiner-mover-leaver-shortcut.writ --claims joiner-mover-leaver.claims # exit 1 +``` + +`../../modality-cross-check.sh` checks the `.rules` encoding against `writ +check`. Siblings: [`../separation-of-duties/`](../separation-of-duties/), +[`../scp-escalation/`](../scp-escalation/). diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ new file mode 100644 index 0000000..864012f --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ @@ -0,0 +1,113 @@ +; The same lifecycle, with ONE THING MISSING from the mover and leaver steps: +; they remove Ada from her groups, and nothing else. +; +; That is what group-based offboarding does, and it is what the runbook says: +; "access is managed through groups". It is true of every grant made through a +; group. The administrator permission set was assigned directly, on the day +; the request needed it, and nothing that acts on groups can see it. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "joiner-mover-leaver.lib.writ") + +(schema joiner-mover-leaver + + (type status (active left)) + (type team (platform marketing)) + + (type person + (arrow status (to status)) + (arrow team (to team))) + + ; How a grant was made, which decides what removes it. A `group` grant goes + ; when the person leaves the group; a `direct` one goes only when someone + ; removes it by name. + (type via-t (group direct)) + + ; A production entitlement, and who holds it. + (type entitlement + (arrow via (to via-t) fixed) + (maybe holder person)) + + (type stage (none requested approved provisioned)) + + ; The one access request this model follows. + (type request + (arrow requester (to person) fixed) + (arrow stage (to stage)) + (maybe approver person)) + + ; ---- the rules of the request ---- + + ; Nothing is provisioned that nobody approved. + (equation provisioned-means-approved + (not (and (is request.stage provisioned) (not (defined request.approver))))) + + ; Nobody approves their own request. + (equation no-self-approval + (not (is request.approver request.requester)))) + +(instance start joiner-mover-leaver + + (person ada (status active) (team platform)) ; joins, needs production + (person bob (status active) (team platform)) ; her manager + + ; The production group in the identity provider. Its membership syncs to + ; AWS IAM Identity Center and grants the engineers' permission set. + (entitlement prod-engineers (via group) (holder vacant)) + ; The administrator permission set on the production account, assigned to + ; the person directly: at the time, no group mapped to it, and the request + ; needed it that day. + (entitlement prod-admin (via direct) (holder vacant)) + + (request ada-prod (requester ada) (stage none) (approver vacant))) + +(use joiner-mover-leaver) +(initial start) + +; ---- joiner ---- + +(transition ada-requests-prod + (when (and (is ada-prod.stage none) (is ada.status active))) + (do (set ada-prod.stage requested))) + +; Whoever approves must not be the requester. Each possible approver is a move +; of its own, so the guard can say so. +(form (approve-by N P) + (transition N + (when (and (is ada-prod.stage requested) + (is P.status active) + (not (is ada-prod.requester P)))) + (do (set ada-prod.stage approved) (set ada-prod.approver P)))) +(approve-by ada-approves ada) ; never fires: she is the requester +(approve-by bob-approves bob) + +; Provisioning re-checks the person, not only the request. An approval is a +; judgement about someone in a role; if they have since moved or left, the +; approval is about a situation that no longer exists. (The first draft of +; this file did not re-check, and writ found it: approve, leave, provision — +; access granted to someone who had already gone. See the README.) +(transition provision-ada + (when (and (is ada-prod.stage approved) + (is ada.status active) + (is ada.team platform))) + (do (set ada-prod.stage provisioned) + (set prod-engineers.holder ada) + (set prod-admin.holder ada))) + +; ---- mover and leaver ---- + +; Each lifecycle event runs its own deprovisioning, the way an HR-driven +; (SCIM) integration does: the change of team or the leaving date arrives, and +; access is removed in the same step. It removes the person from their groups, +; which is what the integration knows how to do. +(transition ada-moves-to-marketing + (when (and (is ada.status active) (is ada.team platform))) + (do (set ada.team marketing) + (vacate prod-engineers.holder))) ; <- prod-admin, not removed + +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder))) ; <- prod-admin, not removed diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims new file mode 100644 index 0000000..fb37e1f --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims @@ -0,0 +1,36 @@ +; The questions, put to both plans. + +(load "joiner-mover-leaver.lib.writ") + +(property ada-gets-access + "the request can end with Ada holding production access" + (possible (and (is prod-engineers.holder ada) (is prod-admin.holder ada)))) + +(property movers-lose-prod + "nobody off the platform team ever holds production access" + (never (some (e entitlement) (held-outside-platform e))) + (show stranded)) + +(property leavers-lose-everything + "nobody who has left ever holds production access" + (never (some (e entitlement) (held-by-leaver e))) + (show stranded)) + +(property leavers-can-be-cut-off + "from every reachable situation, a leaver can still end up holding nothing" + (live (or (is ada.status active) + (and (not (defined prod-engineers.holder)) + (not (defined prod-admin.holder)))))) + +; ---- what is left behind ---- +(query stranded + (where (e entitlement)) + (or (held-outside-platform e) (held-by-leaver e))) + +; ---- ownership ---- +; The request's own steps are what can break its rules; their guards are what +; keep them. Each is acknowledged, and neither rule is violated in either plan. +(accept ada-requests-prod provisioned-means-approved) +(accept ada-approves provisioned-means-approved no-self-approval) +(accept bob-approves provisioned-means-approved no-self-approval) +(accept provision-ada provisioned-means-approved) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ new file mode 100644 index 0000000..dd7d791 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ @@ -0,0 +1,11 @@ +; 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") + +; E is held by someone who is no longer entitled to production: they have +; left, or they have moved off the platform team. Written from the +; entitlement's side, because a type name cannot be the right of `is`. +(form (held-by-leaver E) + (and (defined E.holder) (is E.holder.status left))) +(form (held-outside-platform E) + (and (defined E.holder) (is E.holder.team marketing))) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules new file mode 100644 index 0000000..e4be8f3 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules @@ -0,0 +1,39 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "joiner-mover-leaver.lib.writ") + +(satisfies ada-gets-access + (and (is prod-engineers.holder ada) (is prod-admin.holder ada))) + +(satisfies movers-lose-prod (some (e entitlement) (held-outside-platform e))) + +(satisfies leavers-lose-everything (some (e entitlement) (held-by-leaver e))) + +(satisfies cut-off + (or (is ada.status active) + (and (not (defined prod-engineers.holder)) + (not (defined prod-admin.holder))))) +(can-reach can-cut-off cut-off) +(trapped leavers-can-be-cut-off can-cut-off) + +; ---- the explanation ---- +; Every entitlement still held by someone with no business holding it: the +; situation, the entitlement, how it was granted, and who holds it. The `via` +; column is the finding — every row says `direct`. +(relation left-behind (Situation entitlement via-t person)) +(rule (left-behind S E V P) + (situation S) + (holds S (is E.holder P)) + (holds S (is P.status left)) + (is E.via V)) +(rule (left-behind S E V P) + (situation S) + (holds S (is E.holder P)) + (holds S (is P.team marketing)) + (is E.via V)) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ new file mode 100644 index 0000000..e30dbdf --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ @@ -0,0 +1,118 @@ +; Joiner, mover, leaver — access that follows a person through a job. +; +; Ada joins the platform team and requests production access. Her manager +; approves; provisioning gives her two things: membership of the production +; group, and an administrator permission set assigned to her directly, because +; no group mapped to it at the time. Later she moves to another team, or +; leaves. +; +; Offboarding is automatic: the HR system's event removes her access in the +; same step. In this plan it removes everything she holds, by name. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "joiner-mover-leaver.lib.writ") + +(schema joiner-mover-leaver + + (type status (active left)) + (type team (platform marketing)) + + (type person + (arrow status (to status)) + (arrow team (to team))) + + ; How a grant was made, which decides what removes it. A `group` grant goes + ; when the person leaves the group; a `direct` one goes only when someone + ; removes it by name. + (type via-t (group direct)) + + ; A production entitlement, and who holds it. + (type entitlement + (arrow via (to via-t) fixed) + (maybe holder person)) + + (type stage (none requested approved provisioned)) + + ; The one access request this model follows. + (type request + (arrow requester (to person) fixed) + (arrow stage (to stage)) + (maybe approver person)) + + ; ---- the rules of the request ---- + + ; Nothing is provisioned that nobody approved. + (equation provisioned-means-approved + (not (and (is request.stage provisioned) (not (defined request.approver))))) + + ; Nobody approves their own request. + (equation no-self-approval + (not (is request.approver request.requester)))) + +(instance start joiner-mover-leaver + + (person ada (status active) (team platform)) ; joins, needs production + (person bob (status active) (team platform)) ; her manager + + ; The production group in the identity provider. Its membership syncs to + ; AWS IAM Identity Center and grants the engineers' permission set. + (entitlement prod-engineers (via group) (holder vacant)) + ; The administrator permission set on the production account, assigned to + ; the person directly: at the time, no group mapped to it, and the request + ; needed it that day. + (entitlement prod-admin (via direct) (holder vacant)) + + (request ada-prod (requester ada) (stage none) (approver vacant))) + +(use joiner-mover-leaver) +(initial start) + +; ---- joiner ---- + +(transition ada-requests-prod + (when (and (is ada-prod.stage none) (is ada.status active))) + (do (set ada-prod.stage requested))) + +; Whoever approves must not be the requester. Each possible approver is a move +; of its own, so the guard can say so. +(form (approve-by N P) + (transition N + (when (and (is ada-prod.stage requested) + (is P.status active) + (not (is ada-prod.requester P)))) + (do (set ada-prod.stage approved) (set ada-prod.approver P)))) +(approve-by ada-approves ada) ; never fires: she is the requester +(approve-by bob-approves bob) + +; Provisioning re-checks the person, not only the request. An approval is a +; judgement about someone in a role; if they have since moved or left, the +; approval is about a situation that no longer exists. (The first draft of +; this file did not re-check, and writ found it: approve, leave, provision — +; access granted to someone who had already gone. See the README.) +(transition provision-ada + (when (and (is ada-prod.stage approved) + (is ada.status active) + (is ada.team platform))) + (do (set ada-prod.stage provisioned) + (set prod-engineers.holder ada) + (set prod-admin.holder ada))) + +; ---- mover and leaver ---- + +; Each lifecycle event runs its own deprovisioning, the way an HR-driven +; (SCIM) integration does: the change of team or the leaving date arrives, and +; access is removed in the same step. Both remove the group membership AND the +; direct assignment. +(transition ada-moves-to-marketing + (when (and (is ada.status active) (is ada.team platform))) + (do (set ada.team marketing) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) + +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) diff --git a/entitlement-problems/scp-escalation/README.md b/entitlement-problems/scp-escalation/README.md new file mode 100644 index 0000000..5a24399 --- /dev/null +++ b/entitlement-problems/scp-escalation/README.md @@ -0,0 +1,169 @@ +# An OU move that leaves the guardrails behind + +In AWS Organizations, a *service control policy* (SCP) is attached to an +organizational unit (OU) and caps what any role in that OU's accounts can do. +It never grants anything; it only takes away. Teams lean on that: the roles +inside a production account are broad, because the production OU's SCP denies +the few things nobody should do there, like switching off CloudTrail. + +So the guardrail belongs to the OU, not to the account. Move the account to +another OU, as a reorganisation does, and it leaves its guardrails behind and +picks up whatever the new OU carries. No role changes and no IAM policy is +edited. The change is drag-and-drop in the console, reviewed as an +organizational chore. + +## Before and after + +`writ compare` checks one set of questions against both versions of the +organization: + +```sh +writ compare scp-escalation.writ scp-escalation-restructured.writ # exit 1 +``` + +``` +equations: +properties: dev-can-deploy preserved + dev-never-edits-cloudtrail LOST witness: 1. dev-assumes-power 2. move-prod-to-workloads + sec-can-always-audit LOST witness: 1. move-prod-to-workloads +``` + +Deploying still works. Two guarantees are gone, each with the shortest route to +where it fails: + +- **Developers can now modify CloudTrail.** An engineer signed in as `power` + (PowerUserAccess, which includes CloudTrail) was held back only by the + production OU's SCP. After the move, nothing holds them back. +- **The security team is locked out of production's audit trail.** No sign-in + is needed for this one: the move alone does it, and nothing moves the account + back. + +The properties come from [`scp-escalation.claims`](scp-escalation.claims), +beside the original. `compare` reads the questions from there and asks them of +both files. A `LOST` line exits 1, so the comparison is a gate a pipeline can +run on every change to the organization model. + +## The model, and what it leaves out + +[`scp-escalation.writ`](scp-escalation.writ) keeps only what the three +questions need: + +- **Three actions**: `prod-write`, `cloudtrail-edit`, `audit-read`. +- **OUs** as one deny flag per action. `production` denies CloudTrail edits. + `security` denies production writes. `workloads` is new: its SCPs were copied + from the sandbox template, which has no CloudTrail guardrail and denies access + from outside the unit (the security team's read is cross-account). +- **Accounts**: `prod-acct` in `production`, `sec-acct` in `security`. Which OU + an account sits in is the one thing an administrator changes here. +- **Roles**, each living in one account with fixed grants: `deploy`, `power`, + `audit-reader`, all in `prod-acct`. +- **Principals** `dev` and `sec`, and the role each is signed in as, if any. + +Who may assume which role is listed rather than computed: one move per trust +relationship (`dev-assumes-deploy`, `dev-assumes-power`, +`sec-assumes-audit-reader`), plus signing out. + +AWS evaluation is reduced to one conjunction, in +[`scp-escalation.lib.writ`](scp-escalation.lib.writ): the role grants the +action **and** the role's account's OU does not deny it. + +```lisp +(form (edits-cloudtrail P) + (and (is P.assumed.cloudtrail-edit yes) + (is P.assumed.in.ou.deny-cloudtrail-edit no))) +``` + +Left out: permission boundaries, resource policies, session policies, explicit +denies in identity policies, nested OUs and SCP inheritance, conditions, and +every action not named above. Each would be another conjunct in those forms. +A reader whose question depends on them needs a bridge that reads real policy +and writes the model. That is a separate tool, not this scenario. + +[`scp-escalation-restructured.writ`](scp-escalation-restructured.writ) is the +same file plus one transition: + +```lisp +(transition move-prod-to-workloads + (when (is prod-acct.ou production)) + (do (set prod-acct.ou workloads))) +``` + +## Checking each version + +The original, exit 0: + +``` +states: 6 edges: 14 +… +holds dev-can-deploy +holds dev-never-edits-cloudtrail +holds sec-can-always-audit +``` + +The restructured one, exit 1: + +``` +states: 12 edges: 34 +… +fails dev-never-edits-cloudtrail + "developers cannot modify CloudTrail" + witness: 1. dev-assumes-power → #2 dev.assumed: ∅ → power + 2. move-prod-to-workloads → #8 prod-acct.ou: production → workloads + cloudtrail-editors (at state 8) + p = dev +fails sec-can-always-audit + "whatever has happened, the security team can still get to production's audit trail" + stuck at: #4 (prod-acct.ou=workloads sec-acct.ou=security dev.assumed=∅ sec.assumed=∅) + witness: 1. move-prod-to-workloads → #4 prod-acct.ou: production → workloads + audit-readers (at state 4) +``` + +The CloudTrail witness happens in the order it would in practice. An engineer +is already signed in as `power` when the account moves, and their session +gains the capability without them doing anything. `audit-readers` at state 4 +is empty: once the account has moved, nobody can read the trail, now or later. + +## The privilege path + +[`scp-escalation.rules`](scp-escalation.rules) lays out every effective +CloudTrail edit as a path: the principal, the role it assumed, the account the +role lives in, and the OU whose SCP failed to stop it. + +```sh +writ derive scp-escalation-restructured.writ scp-escalation.rules escalation +``` + +``` +escalation (2 rows) + 8 dev power prod-acct workloads + 11 dev power prod-acct workloads +``` + +Read across a row: dev → power → prod-acct → workloads. The guardrail was the +last hop, and the move replaced it. + +## What to take away + +Guardrails that live on a container travel with the container, not with what +is in it. A review of the IAM change finds nothing, because there is no IAM +change. A review of the OU move sees a chore. Neither file says which +guarantees depended on which OU. Asking the same questions before and after +does. + +`check` on the new model fails too, but `compare` is the gate that fits the +change. Its subject is a difference: it says which guarantees the +reorganisation took away, and keeps the ones it did not. + +## Run it + +```sh +writ check scp-escalation.writ --claims scp-escalation.claims # exit 0 +writ check scp-escalation-restructured.writ --claims scp-escalation.claims # exit 1 +writ compare scp-escalation.writ scp-escalation-restructured.writ # exit 1 +``` + +With the organization model under git, `writ compare --git HEAD~1 HEAD +scp-escalation.writ` asks the same questions across two commits. +`../../modality-cross-check.sh` checks the `.rules` encoding against `writ +check`. Siblings: [`../separation-of-duties/`](../separation-of-duties/), +[`../joiner-mover-leaver/`](../joiner-mover-leaver/). diff --git a/entitlement-problems/scp-escalation/scp-escalation-restructured.writ b/entitlement-problems/scp-escalation/scp-escalation-restructured.writ new file mode 100644 index 0000000..ec7c7b7 --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation-restructured.writ @@ -0,0 +1,95 @@ +; The same organization, with ONE MOVE ADDED: the reorganisation moves the +; production account into the new `workloads` OU. +; +; Nothing about any role changes, and no IAM policy is edited. The move is a +; one-line change in the console, reviewed as an organizational chore. But an +; SCP is attached to an OU, not to an account, so the account leaves its +; guardrails behind and picks up new ones. +; +; Compare it with the original: `writ compare scp-escalation.writ +; scp-escalation-restructured.writ` exits 1 and names what was lost. + +(load "stdlib.writ") +(load "scp-escalation.lib.writ") + +(schema scp-escalation + + (type yn (no yes)) + + ; An organizational unit, reduced to its service control policy: for each of + ; the three actions the questions are about, does the SCP deny it? An SCP + ; never grants anything. It only takes away. + (type ou + (arrow deny-prod-write (to yn) fixed) + (arrow deny-cloudtrail-edit (to yn) fixed) + (arrow deny-audit-read (to yn) fixed)) + + ; Which OU an account sits in is the one thing an administrator changes here. + (type account (arrow ou (to ou))) + + ; An IAM role lives in one account and grants a fixed set of actions. Whether + ; a grant is effective depends on the account's OU, which is not the role's + ; business, and that is the gap the questions probe. + (type role + (arrow in (to account) fixed) + (arrow prod-write (to yn) fixed) + (arrow cloudtrail-edit (to yn) fixed) + (arrow audit-read (to yn) fixed)) + + ; A person, and the role they are currently signed in as, if any. + (type principal (maybe assumed role))) + +(instance start scp-escalation + + ; The guardrails. Production's SCP denies CloudTrail changes, so no role in + ; a production account can switch off the audit trail, however broad its + ; IAM policy. The security OU's denies production writes. + (ou security (deny-prod-write yes) (deny-cloudtrail-edit no) (deny-audit-read no)) + (ou production (deny-prod-write no) (deny-cloudtrail-edit yes) (deny-audit-read no)) + ; Created for the reorganisation, with its SCPs copied from the sandbox + ; template: no CloudTrail guardrail (sandboxes are disposable) and no access + ; from outside the unit (sandboxes are isolated), which is where the security + ; team's cross-account read comes from. + (ou workloads (deny-prod-write no) (deny-cloudtrail-edit no) (deny-audit-read yes)) + + (account prod-acct (ou production)) + (account sec-acct (ou security)) + + ; Deploys to production. + (role deploy (in prod-acct) (prod-write yes) (cloudtrail-edit no) (audit-read no)) + ; The broad role engineers use to debug production. Its IAM policy is + ; PowerUserAccess, which includes CloudTrail. Nobody narrowed it, because + ; the production OU's SCP already denies CloudTrail changes. + (role power (in prod-acct) (prod-write yes) (cloudtrail-edit yes) (audit-read no)) + ; How the security team reads production's audit trail: a role inside the + ; production account that their own account is trusted to assume. + (role audit-reader (in prod-acct) (prod-write no) (cloudtrail-edit no) (audit-read yes)) + + (principal dev (assumed vacant)) + (principal sec (assumed vacant))) + +(use scp-escalation) +(initial start) + +; ---- signing in and out ---- + +; One move per trust relationship, written out: who may assume which role is +; wiring, and wiring is listed rather than computed. +(form (assume N P R) + (transition N (when (not (defined P.assumed))) (do (set P.assumed R)))) +(form (sign-out N P) + (transition N (when (defined P.assumed)) (do (vacate P.assumed)))) + +(assume dev-assumes-deploy dev deploy) +(assume dev-assumes-power dev power) +(assume sec-assumes-audit-reader sec audit-reader) +(sign-out dev-signs-out dev) +(sign-out sec-signs-out sec) + +; ---- the reorganisation ---- + +; Moving an account between OUs. In the console it is drag and drop. Nothing +; moves it back; the reorganisation is not undone. +(transition move-prod-to-workloads + (when (is prod-acct.ou production)) + (do (set prod-acct.ou workloads))) diff --git a/entitlement-problems/scp-escalation/scp-escalation.claims b/entitlement-problems/scp-escalation/scp-escalation.claims new file mode 100644 index 0000000..896e9e0 --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.claims @@ -0,0 +1,22 @@ +; The questions, held fixed across the reorganisation. `writ compare` reads +; them from here for both models. + +(load "scp-escalation.lib.writ") + +(property dev-can-deploy + "a developer can still ship to production" + (possible (writes-prod dev))) + +(property dev-never-edits-cloudtrail + "developers cannot modify CloudTrail" + (never (edits-cloudtrail dev)) + (show cloudtrail-editors)) + +(property sec-can-always-audit + "whatever has happened, the security team can still get to production's audit trail" + (live (reads-audit sec)) + (show audit-readers)) + +; ---- who ---- +(query cloudtrail-editors (where (p principal)) (edits-cloudtrail p)) +(query audit-readers (where (p principal)) (reads-audit p)) diff --git a/entitlement-problems/scp-escalation/scp-escalation.lib.writ b/entitlement-problems/scp-escalation/scp-escalation.lib.writ new file mode 100644 index 0000000..8963b1f --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.lib.writ @@ -0,0 +1,21 @@ +; 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") + +; What a principal can effectively do: the role it has assumed grants the +; action, AND the service control policy of the OU that role's account sits in +; does not deny it. That conjunction is the whole of the AWS evaluation this +; model keeps (see the README for what it leaves out). +; +; One form per action, because a form parameter cannot name an arrow. +(form (writes-prod P) + (and (is P.assumed.prod-write yes) + (is P.assumed.in.ou.deny-prod-write no))) + +(form (edits-cloudtrail P) + (and (is P.assumed.cloudtrail-edit yes) + (is P.assumed.in.ou.deny-cloudtrail-edit no))) + +(form (reads-audit P) + (and (is P.assumed.audit-read yes) + (is P.assumed.in.ou.deny-audit-read no))) diff --git a/entitlement-problems/scp-escalation/scp-escalation.rules b/entitlement-problems/scp-escalation/scp-escalation.rules new file mode 100644 index 0000000..0a3195e --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.rules @@ -0,0 +1,30 @@ +; The same three questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "scp-escalation.lib.writ") + +(satisfies dev-can-deploy (writes-prod dev)) + +(satisfies dev-never-edits-cloudtrail (edits-cloudtrail dev)) + +(satisfies sec-audits (reads-audit sec)) +(can-reach can-audit sec-audits) +(trapped sec-can-always-audit can-audit) + +; ---- the explanation ---- +; Every effective CloudTrail edit, as a privilege path: the situation, the +; principal, the role it assumed, the account that role lives in, and the OU +; that account sits in at that moment, whose SCP did not stop it. +(relation escalation (Situation principal role account ou)) +(rule (escalation S P R A O) + (situation S) + (holds S (is P.assumed R)) + (is R.cloudtrail-edit yes) + (is R.in A) + (holds S (is A.ou O)) + (is O.deny-cloudtrail-edit no)) diff --git a/entitlement-problems/scp-escalation/scp-escalation.writ b/entitlement-problems/scp-escalation/scp-escalation.writ new file mode 100644 index 0000000..838cc5c --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.writ @@ -0,0 +1,89 @@ +; An AWS organization, before a reorganisation. +; +; Production sits in the `production` OU, whose service control policy denies +; CloudTrail changes. The roles inside the production account are broad, +; because the SCP is the guardrail: an engineer signed in as `power` has +; PowerUserAccess, and the SCP takes CloudTrail back out of it. +; +; A new `workloads` OU exists, created for a reorganisation, but nothing has +; been moved into it yet. `scp-escalation-restructured.writ` is this file plus +; the one administrative step that moves production there. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "scp-escalation.lib.writ") + +(schema scp-escalation + + (type yn (no yes)) + + ; An organizational unit, reduced to its service control policy: for each of + ; the three actions the questions are about, does the SCP deny it? An SCP + ; never grants anything. It only takes away. + (type ou + (arrow deny-prod-write (to yn) fixed) + (arrow deny-cloudtrail-edit (to yn) fixed) + (arrow deny-audit-read (to yn) fixed)) + + ; Which OU an account sits in is the one thing an administrator changes here. + (type account (arrow ou (to ou))) + + ; An IAM role lives in one account and grants a fixed set of actions. Whether + ; a grant is effective depends on the account's OU, which is not the role's + ; business, and that is the gap the questions probe. + (type role + (arrow in (to account) fixed) + (arrow prod-write (to yn) fixed) + (arrow cloudtrail-edit (to yn) fixed) + (arrow audit-read (to yn) fixed)) + + ; A person, and the role they are currently signed in as, if any. + (type principal (maybe assumed role))) + +(instance start scp-escalation + + ; The guardrails. Production's SCP denies CloudTrail changes, so no role in + ; a production account can switch off the audit trail, however broad its + ; IAM policy. The security OU's denies production writes. + (ou security (deny-prod-write yes) (deny-cloudtrail-edit no) (deny-audit-read no)) + (ou production (deny-prod-write no) (deny-cloudtrail-edit yes) (deny-audit-read no)) + ; Created for the reorganisation, with its SCPs copied from the sandbox + ; template: no CloudTrail guardrail (sandboxes are disposable) and no access + ; from outside the unit (sandboxes are isolated), which is where the security + ; team's cross-account read comes from. + (ou workloads (deny-prod-write no) (deny-cloudtrail-edit no) (deny-audit-read yes)) + + (account prod-acct (ou production)) + (account sec-acct (ou security)) + + ; Deploys to production. + (role deploy (in prod-acct) (prod-write yes) (cloudtrail-edit no) (audit-read no)) + ; The broad role engineers use to debug production. Its IAM policy is + ; PowerUserAccess, which includes CloudTrail. Nobody narrowed it, because + ; the production OU's SCP already denies CloudTrail changes. + (role power (in prod-acct) (prod-write yes) (cloudtrail-edit yes) (audit-read no)) + ; How the security team reads production's audit trail: a role inside the + ; production account that their own account is trusted to assume. + (role audit-reader (in prod-acct) (prod-write no) (cloudtrail-edit no) (audit-read yes)) + + (principal dev (assumed vacant)) + (principal sec (assumed vacant))) + +(use scp-escalation) +(initial start) + +; ---- signing in and out ---- + +; One move per trust relationship, written out: who may assume which role is +; wiring, and wiring is listed rather than computed. +(form (assume N P R) + (transition N (when (not (defined P.assumed))) (do (set P.assumed R)))) +(form (sign-out N P) + (transition N (when (defined P.assumed)) (do (vacate P.assumed)))) + +(assume dev-assumes-deploy dev deploy) +(assume dev-assumes-power dev power) +(assume sec-assumes-audit-reader sec audit-reader) +(sign-out dev-signs-out dev) +(sign-out sec-signs-out sec) diff --git a/entitlement-problems/separation-of-duties/README.md b/entitlement-problems/separation-of-duties/README.md new file mode 100644 index 0000000..cd172a3 --- /dev/null +++ b/entitlement-problems/separation-of-duties/README.md @@ -0,0 +1,173 @@ +# Separation of duties, through a role nobody listed + +The person who raises a payment must not be the person who approves it. +Everyone knows the rule, and the usual control enforces it with a table of +*toxic combinations*: pairs of groups nobody may hold together. Every access +request is checked against the table before anyone is added to a group. + +The table is written in group names, but the rule is about capabilities, and +a person gets capabilities from a group's *role*. The two agree only as long +as every group whose role can raise or approve appears in the table. Nothing +checks that. When the finance team creates a group for its own leads and +gives it a role that approves invoices, the table is still correct about every +pair it lists, and a requester can now become an approver. + +## The model + +[`separation-of-duties.writ`](separation-of-duties.writ) has three kinds of +thing: + +- a **role** is a fixed bundle of capabilities: `can-request` and + `can-approve`; +- a **group** grants exactly one role; +- an **account** is in at most two groups, as two slots `g1` and `g2`. + +Three roles: `requester`, `approver`, and `ap-lead`, which approves invoices. +Three groups grant them: `requesters`, `approvers`, `finance-leads`. Two +accounts, `alice` and `bob`, start in no group. The moves add an account to a +group (`alice-joins-requesters` fills the first slot, +`alice-also-joins-finance-leads` the second) or take it out again. + +The rule is a law, written once over the account's slots and read *through* +the group to its role: + +```lisp +(equation separation (not (conflicted account))) +``` + +where `conflicted` (in [`separation-of-duties.lib.writ`](separation-of-duties.lib.writ)) +spells out every pair of slots: `g1`'s role can request and `g2`'s can approve, +and so on. A law is reported whenever any reachable situation breaks it, +whatever the moves allowed. + +The two files differ in one conjunct of the grant's guard. The safe plan +refuses a grant if the table lists the pair **or** if the group's role would +complete a conflict with the other slot: + +```lisp +(when (and (not (defined A.g1)) + (not (listed-pair G A.g2)) + (not (grant-conflicts G A.g2)))) +``` + +[`separation-of-duties-shortcut.writ`](separation-of-duties-shortcut.writ) +keeps `listed-pair` and drops `grant-conflicts`. That is the check most access +tooling performs. + +## What writ answers + +Both plans are asked the questions in +[`separation-of-duties.claims`](separation-of-duties.claims). The safe plan, +exit 0: + +``` +states: 144 edges: 768 +regime: reversible — 144 of 144 situations lie on cycles +… +holds staffable + "someone can be given the power to approve" + witness: 1. alice-joins-approvers → #2 alice.g1: ∅ → approvers +holds no-conflict + "nobody ever holds both halves of a payment" +holds revocable + "from every reachable situation, everyone can still be taken out of every group" +certified: every answer re-derived from the model (writ-cert) +``` + +The shortcut, exit 1: + +``` +states: 196 edges: 1120 +… +equation separation + … + violated in 52 reachable situations witness: 1. alice-joins-requesters 2. alice-also-joins-finance-leads → #14 +… +fails no-conflict + "nobody ever holds both halves of a payment" + witness: 1. alice-joins-requesters → #1 alice.g1: ∅ → requesters + 2. alice-also-joins-finance-leads → #14 alice.g2: ∅ → finance-leads + conflicted-accounts (at state 14) + a = alice +``` + +Two grants, each of which passes the table. The first is what Alice's job +needs. The second is a group whose name says nothing about approving. The +`conflicted-accounts` line answers the query the property names with +`(show …)`: who is in the bad situation. + +The shortcut still lets anyone be made an approver and still lets everyone be +taken out of every group, so `staffable` and `revocable` hold for both. Only +the safety question tells them apart. + +## Who, and through which grants + +A law's subject is one account at a time, and a query's variables cannot be +compared with each other. So "which two groups" is a join, and joins are what +[`separation-of-duties.rules`](separation-of-duties.rules) is for: + +```sh +writ derive separation-of-duties-shortcut.writ separation-of-duties.rules conflict +``` + +``` +conflict (56 rows) + 14 alice requesters finance-leads + 29 alice requesters finance-leads + 57 bob requesters finance-leads + … +``` + +Every row is the same pair. `requesters` + `approvers`, the pair the table +lists, never appears. The first column is a situation number, and +`writ show` reads any of them back: + +```sh +writ show separation-of-duties-shortcut.writ --at 14 +``` + +``` +situation 14 of 196 + cells: (alice.g1=requesters bob.g1=∅ alice.g2=finance-leads bob.g2=∅) + route: 1. alice-joins-requesters + 2. alice-also-joins-finance-leads + moves: … alice-leaves-first-group → 6 alice-leaves-second-group → 1 +``` + +That is the violation stated in the domain's own terms: the account, the two +grants, the order they were made in, and the two moves that would undo it. + +## Why two slots + +Two slots per account is enough to show the finding, and it keeps the space +small (196 situations). The ceiling is the model's, not writ's: a third slot +is a third `maybe` arrow, and `conflicted` gains the pairs that involve it. + +The slots are there because writ cannot compare two bound variables. "No +account holds two groups that conflict" cannot be a `some … some …` law. It +is a law rooted at **one** account over a bounded number of slots. + +## What to take away + +The mistake is never in one grant. Each of Alice's two grants is legitimate on +its own, and the control that checks grants against a list of group names +passed both. The conflict exists only in the composition, through a role that +was added later by someone else. A check that reads what a group *grants* +catches it on the second grant. A check that reads what a group is *called* +cannot. + +To adapt it, list your roles' capabilities from the policy documents rather +than from group names, and add a slot if your people commonly hold three +groups. + +## Run it + +```sh +writ check separation-of-duties.writ --claims separation-of-duties.claims # exit 0 +writ check separation-of-duties-shortcut.writ --claims separation-of-duties.claims # exit 1 +``` + +[`separation-of-duties.rules`](separation-of-duties.rules) also encodes the +three properties for `writ derive`. `../../modality-cross-check.sh` checks the +two answers agree. Siblings: [`../scp-escalation/`](../scp-escalation/), +[`../joiner-mover-leaver/`](../joiner-mover-leaver/). diff --git a/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ b/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ new file mode 100644 index 0000000..5bd6777 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ @@ -0,0 +1,92 @@ +; The same access process, with ONE CONDITION REMOVED from every grant: the +; request is checked against the toxic-combination table, and nothing else. +; +; That is how most access tooling works. The table names `requesters` and +; `approvers`, so nobody can hold both. It does not name `finance-leads`: that +; group was created later, by another team, and its role `ap-lead` approves. +; The table was written in group names; the conflict lives in a role. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "separation-of-duties.lib.writ") + +(schema separation-of-duties + + (type yn (no yes)) + + ; A role is a bundle of capabilities, fixed when it was designed. + (type role + (arrow can-request (to yn) fixed) + (arrow can-approve (to yn) fixed)) + + ; A group grants exactly one role. Access is given by adding people to groups, + ; so a person's capabilities are never written down anywhere: they are + ; whatever their groups' roles add up to. + (type group (arrow role (to role) fixed)) + + ; Two group slots per account. What changes is who is in which group. + (type account + (maybe g1 group) + (maybe g2 group)) + + ; ---- the rule ---- + + ; Separation of duties: nobody can both raise a payment and approve it. + ; A law, not a guard: writ reports it if any reachable situation breaks it, + ; whatever the moves allowed. + (equation separation (not (conflicted account)))) + +(instance start separation-of-duties + + (role requester (can-request yes) (can-approve no)) + (role approver (can-request no) (can-approve yes)) + ; Team leads in accounts payable sign off invoices. It is an approver by + ; another name, created by the finance team for its own leads, after the + ; toxic-combination table was written. + (role ap-lead (can-request no) (can-approve yes)) + + (group requesters (role requester)) + (group approvers (role approver)) + (group finance-leads (role ap-lead)) + + (account alice (g1 vacant) (g2 vacant)) + (account bob (g1 vacant) (g2 vacant))) + +(use separation-of-duties) +(initial start) + +; ---- granting and removing access ---- + +; The first group goes in slot g1, a second in g2. +; The grant is refused if the toxic-combination table lists the pair. +(form (join1 N A G) + (transition N + (when (and (not (defined A.g1)) + (not (listed-pair G A.g2)))) ; <- grant-conflicts, gone + (do (set A.g1 G)))) +(form (join2 N A G) + (transition N + (when (and (not (defined A.g2)) + (not (listed-pair G A.g1)))) ; <- grant-conflicts, gone + (do (set A.g2 G)))) + +(form (leave1 N A) (transition N (when (defined A.g1)) (do (vacate A.g1)))) +(form (leave2 N A) (transition N (when (defined A.g2)) (do (vacate A.g2)))) + +(join1 alice-joins-requesters alice requesters) +(join1 alice-joins-approvers alice approvers) +(join1 alice-joins-finance-leads alice finance-leads) +(join2 alice-also-joins-requesters alice requesters) +(join2 alice-also-joins-approvers alice approvers) +(join2 alice-also-joins-finance-leads alice finance-leads) +(join1 bob-joins-requesters bob requesters) +(join1 bob-joins-approvers bob approvers) +(join1 bob-joins-finance-leads bob finance-leads) +(join2 bob-also-joins-requesters bob requesters) +(join2 bob-also-joins-approvers bob approvers) +(join2 bob-also-joins-finance-leads bob finance-leads) +(leave1 alice-leaves-first-group alice) +(leave2 alice-leaves-second-group alice) +(leave1 bob-leaves-first-group bob) +(leave2 bob-leaves-second-group bob) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.claims b/entitlement-problems/separation-of-duties/separation-of-duties.claims new file mode 100644 index 0000000..a276f39 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.claims @@ -0,0 +1,47 @@ +; The questions, put to both plans. + +(load "separation-of-duties.lib.writ") + +(property staffable + "someone can be given the power to approve" + (possible (some (a account) (or (is a.g1.role.can-approve yes) + (is a.g2.role.can-approve yes))))) + +(property no-conflict + "nobody ever holds both halves of a payment" + (never (some (a account) (conflicted a))) + (show conflicted-accounts)) + +(property revocable + "from every reachable situation, everyone can still be taken out of every group" + (live (all (a account) (and (not (defined a.g1)) (not (defined a.g2)))))) + +; ---- ownership ---- +; Every grant can break separation; that is what the grant checks are for, and +; on the shortcut it is what the law reports. A removal cannot add a capability, +; but writ's reading is syntactic: it writes a slot the law reads, so it is +; acknowledged too. +(accept alice-joins-requesters separation) +(accept alice-joins-approvers separation) +(accept alice-joins-finance-leads separation) +(accept alice-also-joins-requesters separation) +(accept alice-also-joins-approvers separation) +(accept alice-also-joins-finance-leads separation) +(accept bob-joins-requesters separation) +(accept bob-joins-approvers separation) +(accept bob-joins-finance-leads separation) +(accept bob-also-joins-requesters separation) +(accept bob-also-joins-approvers separation) +(accept bob-also-joins-finance-leads separation) +(accept alice-leaves-first-group separation) +(accept alice-leaves-second-group separation) +(accept bob-leaves-first-group separation) +(accept bob-leaves-second-group separation) + +; ---- who ---- +; Answered at the situation a failing verdict singles out. A query binder +; cannot be compared with another, so this names the ACCOUNT; which two groups +; it holds is a join, and that is `conflict` in separation-of-duties.rules. +(query conflicted-accounts + (where (a account)) + (conflicted a)) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ b/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ new file mode 100644 index 0000000..133642c --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ @@ -0,0 +1,27 @@ +; 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") + +; A holds, through its two group slots, both the power to raise a payment and +; the power to approve one. Spelled out over every pair of slots, the same slot +; twice included: a single group whose role carries both is a conflict too. +; It is rooted at ONE account because two bound accounts cannot be compared; +; that is also why the slots are bounded (see the README). +(form (conflicted A) + (or (and (is A.g1.role.can-request yes) (is A.g1.role.can-approve yes)) + (and (is A.g1.role.can-request yes) (is A.g2.role.can-approve yes)) + (and (is A.g2.role.can-request yes) (is A.g1.role.can-approve yes)) + (and (is A.g2.role.can-request yes) (is A.g2.role.can-approve yes)))) + +; What joining group G would add to account A, whose OTHER slot is OTHER. +; The capability check: read through the group to its role. +(form (grant-conflicts G OTHER) + (or (and (is G.role.can-request yes) (is G.role.can-approve yes)) + (and (is G.role.can-request yes) (is OTHER.role.can-approve yes)) + (and (is G.role.can-approve yes) (is OTHER.role.can-request yes)))) + +; The name check: the toxic-combination table as an IAM team writes it — two +; groups that must never be held together, listed by name. +(form (listed-pair G OTHER) + (or (and (is G requesters) (is OTHER approvers)) + (and (is G approvers) (is OTHER requesters)))) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.rules b/entitlement-problems/separation-of-duties/separation-of-duties.rules new file mode 100644 index 0000000..d89679a --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.rules @@ -0,0 +1,31 @@ +; The same three questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "separation-of-duties.lib.writ") + +(satisfies staffable + (some (a account) (or (is a.g1.role.can-approve yes) (is a.g2.role.can-approve yes)))) + +(satisfies no-conflict (some (a account) (conflicted a))) + +(satisfies everyone-out (all (a account) (and (not (defined a.g1)) (not (defined a.g2))))) +(can-reach can-empty everyone-out) +(trapped revocable can-empty) + +; ---- the explanation ---- +; The question the law cannot answer, because its subject is one account at a +; time: WHO holds both halves, and through WHICH two groups. Here variables +; join, so the answer is a table: situation, account, the group that lets them +; raise a payment, the group that lets them approve it. +(relation conflict (Situation account group group)) +(rule (conflict S A G H) + (situation S) (holds S (is A.g1 G)) (holds S (is A.g2 H)) + (is G.role.can-request yes) (is H.role.can-approve yes)) +(rule (conflict S A G H) + (situation S) (holds S (is A.g2 G)) (holds S (is A.g1 H)) + (is G.role.can-request yes) (is H.role.can-approve yes)) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.writ b/entitlement-problems/separation-of-duties/separation-of-duties.writ new file mode 100644 index 0000000..405cb15 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.writ @@ -0,0 +1,100 @@ +; Separation of duties — and a conflict that arrives through a role. +; +; The rule is old and everyone knows it: the person who raises a payment must +; not be the person who approves it. The usual control is a table of toxic +; combinations: these two groups may never be held together. Access requests +; are checked against the table before anyone is added to a group. +; +; The table is written in GROUP names. The rule is about CAPABILITIES, which a +; person gets from a group's role. The two agree only as long as every group +; that carries both capabilities is in the table, and nothing checks that. +; +; This plan checks both: the table, and what the group would actually add. +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "separation-of-duties.lib.writ") + +(schema separation-of-duties + + (type yn (no yes)) + + ; A role is a bundle of capabilities, fixed when it was designed. + (type role + (arrow can-request (to yn) fixed) + (arrow can-approve (to yn) fixed)) + + ; A group grants exactly one role. Access is given by adding people to groups, + ; so a person's capabilities are never written down anywhere: they are + ; whatever their groups' roles add up to. + (type group (arrow role (to role) fixed)) + + ; Two group slots per account. What changes is who is in which group. + (type account + (maybe g1 group) + (maybe g2 group)) + + ; ---- the rule ---- + + ; Separation of duties: nobody can both raise a payment and approve it. + ; A law, not a guard: writ reports it if any reachable situation breaks it, + ; whatever the moves allowed. + (equation separation (not (conflicted account)))) + +(instance start separation-of-duties + + (role requester (can-request yes) (can-approve no)) + (role approver (can-request no) (can-approve yes)) + ; Team leads in accounts payable sign off invoices. It is an approver by + ; another name, created by the finance team for its own leads, after the + ; toxic-combination table was written. + (role ap-lead (can-request no) (can-approve yes)) + + (group requesters (role requester)) + (group approvers (role approver)) + (group finance-leads (role ap-lead)) + + (account alice (g1 vacant) (g2 vacant)) + (account bob (g1 vacant) (g2 vacant))) + +(use separation-of-duties) +(initial start) + +; ---- granting and removing access ---- + +; The first group goes in slot g1, a second in g2. +; The grant is refused if the toxic-combination table lists the pair, or if +; the group's role would give the account, together with its other slot, both +; halves of a payment. The second check reads through the group to the role. +(form (join1 N A G) + (transition N + (when (and (not (defined A.g1)) + (not (listed-pair G A.g2)) + (not (grant-conflicts G A.g2)))) + (do (set A.g1 G)))) +(form (join2 N A G) + (transition N + (when (and (not (defined A.g2)) + (not (listed-pair G A.g1)) + (not (grant-conflicts G A.g1)))) + (do (set A.g2 G)))) + +(form (leave1 N A) (transition N (when (defined A.g1)) (do (vacate A.g1)))) +(form (leave2 N A) (transition N (when (defined A.g2)) (do (vacate A.g2)))) + +(join1 alice-joins-requesters alice requesters) +(join1 alice-joins-approvers alice approvers) +(join1 alice-joins-finance-leads alice finance-leads) +(join2 alice-also-joins-requesters alice requesters) +(join2 alice-also-joins-approvers alice approvers) +(join2 alice-also-joins-finance-leads alice finance-leads) +(join1 bob-joins-requesters bob requesters) +(join1 bob-joins-approvers bob approvers) +(join1 bob-joins-finance-leads bob finance-leads) +(join2 bob-also-joins-requesters bob requesters) +(join2 bob-also-joins-approvers bob approvers) +(join2 bob-also-joins-finance-leads bob finance-leads) +(leave1 alice-leaves-first-group alice) +(leave2 alice-leaves-second-group alice) +(leave1 bob-leaves-first-group bob) +(leave2 bob-leaves-second-group bob) diff --git a/modality-cross-check.sh b/modality-cross-check.sh index dce80fc..bd3c147 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index 53242dd..9742087 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,16 +431,17 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The thirteen scenarios this script walks by convention, and their 31 + # The sixteen scenarios this script walks by convention, and their 41 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the thirteen fails this line, which is the point of it — - # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, and - # 26 -> 31 with two-phase-commit, and this line is where each of those had to - # be said out loud. - has "cross-check: all 31 properties of the thirteen scenarios were considered" \ - "$out" "considered 31 properties" - # One of the 31 is not compared, and the count above is the only place that + # property to any of the sixteen 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, and 31 -> 41 with the three + # entitlement-problems (3 + 3 + 4), and this line is where each of those had + # to be said out loud. + has "cross-check: all 41 properties of the sixteen scenarios were considered" \ + "$out" "considered 41 properties" + # One of the 41 is not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit asks one property under # a fairness assumption, which ct.rules §8 does not encode. has "cross-check: with the one fair property skipped, and saying why" \ @@ -454,9 +455,10 @@ crosscheck() { # `arch` brought the repository's first two `never` properties, so this # branch — which announced itself as unexercised on every prior run — is now # measured. If it ever reads "unexercised" again, a scenario went missing. - # two-phase-commit's atomicity is the third. + # two-phase-commit's atomicity is the third; the entitlement problems bring + # four more, since "nobody ever holds X" is how an access rule is said. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 3 properties compared" + "never: 7 properties compared" # And `inevitable`, whose two are two-phase-commit's — the newest modality, # and the one whose second implementation is newest, so the line that says it # is being compared at all is worth having. @@ -598,9 +600,93 @@ add_a_required_column() { fi } +separation_of_duties() { + d="$here/entitlement-problems/separation-of-duties" + echo "== Separation of duties — a conflict that arrives through a role ==" + echo " Q: the toxic-combination table is checked on every grant. Is that enough?" + out=$("$WRIT" check "$d/separation-of-duties.writ" --claims "$d/separation-of-duties.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "separation-of-duties: checking capabilities, the plan is clean" "$st" 0 + has "separation-of-duties: A. an approver can still be appointed" "$out" "holds staffable" + has "separation-of-duties: B. nobody holds both halves of a payment" "$out" "holds no-conflict" + has "separation-of-duties: and everyone can still be taken out of every group" "$out" "holds revocable" + lacks "separation-of-duties: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/separation-of-duties-shortcut.writ" --claims "$d/separation-of-duties.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "separation-of-duties: checking the table alone is refused" "$sst" 1 + has "separation-of-duties: C. two grants the table never listed" "$sc" "violated in 52 reachable situations" + near "separation-of-duties: the first is innocent" "$sc" "fails no-conflict" "1. alice-joins-requesters" + near "separation-of-duties: the second is a group nobody put in the table" "$sc" "fails no-conflict" "2. alice-also-joins-finance-leads" + near "separation-of-duties: and the verdict names who" "$sc" "fails no-conflict" "a = alice" + # Which two groups is a join, which a query cannot do and the rules engine + # can: every row it prints is the same pair, and that pair is the finding. + dv=$("$WRIT" derive "$d/separation-of-duties-shortcut.writ" "$d/separation-of-duties.rules" conflict 2>&1) + has "separation-of-duties: D. derive names the account and both groups" "$dv" "14 alice requesters finance-leads" + lacks "separation-of-duties: and the pair the table lists never appears" "$dv" "requesters approvers" +} + +scp_escalation() { + d="$here/entitlement-problems/scp-escalation" + echo "== An OU move — the guardrails stay behind ==" + echo " Q: moving an account between OUs changes no role. What does it change?" + out=$("$WRIT" check "$d/scp-escalation.writ" --claims "$d/scp-escalation.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "scp-escalation: the organization as approved is clean" "$st" 0 + has "scp-escalation: A. developers cannot modify CloudTrail" "$out" "holds dev-never-edits-cloudtrail" + has "scp-escalation: B. the security team can always reach the audit trail" "$out" "holds sec-can-always-audit" + + cmp=$("$WRIT" compare "$d/scp-escalation.writ" "$d/scp-escalation-restructured.writ" 2>&1) + cst=$? + printf '%s\n' "$cmp" | sed 's/^/ | /' + exit_is "scp-escalation: compare refuses the reorganisation" "$cst" 1 + has "scp-escalation: C. deploying still works" "$cmp" "dev-can-deploy preserved" + has "scp-escalation: D. the CloudTrail guardrail is LOST" "$cmp" "dev-never-edits-cloudtrail LOST witness: 1. dev-assumes-power 2. move-prod-to-workloads" + has "scp-escalation: E. and the security team is locked out, by the move alone" "$cmp" "sec-can-always-audit LOST witness: 1. move-prod-to-workloads" + + dv=$("$WRIT" derive "$d/scp-escalation-restructured.writ" "$d/scp-escalation.rules" escalation 2>&1) + has "scp-escalation: F. derive prints the privilege path" "$dv" "dev power prod-acct workloads" +} + +joiner_mover_leaver() { + d="$here/entitlement-problems/joiner-mover-leaver" + echo "== Joiner, mover, leaver — the grant that offboarding cannot see ==" + echo " Q: offboarding removes people from their groups. Is that everything?" + out=$("$WRIT" check "$d/joiner-mover-leaver.writ" --claims "$d/joiner-mover-leaver.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "joiner-mover-leaver: removing everything by name, the plan is clean" "$st" 0 + has "joiner-mover-leaver: A. Ada can be given production access" "$out" "holds ada-gets-access" + has "joiner-mover-leaver: B. a mover loses it" "$out" "holds movers-lose-prod" + has "joiner-mover-leaver: C. a leaver loses it" "$out" "holds leavers-lose-everything" + has "joiner-mover-leaver: and can always be cut off" "$out" "holds leavers-can-be-cut-off" + + sc=$("$WRIT" check "$d/joiner-mover-leaver-shortcut.writ" --claims "$d/joiner-mover-leaver.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "joiner-mover-leaver: group-only offboarding is refused" "$sst" 1 + has "joiner-mover-leaver: D. a leaver keeps production access" "$sc" "fails leavers-lose-everything" + near "joiner-mover-leaver: after an ordinary four-step history" "$sc" "fails leavers-lose-everything" "4. ada-leaves" + # The query answer sits below the four-move witness, past `near`'s six lines, + # so it is anchored on the situation the verdict singled out. + near "joiner-mover-leaver: and the verdict names what was left behind" "$sc" "stranded (at state 13)" "e = prod-admin" + has "joiner-mover-leaver: E. so does a mover" "$sc" "fails movers-lose-prod" + # Not a delay but a trap: nothing that runs later removes a direct grant. + has "joiner-mover-leaver: F. and nothing left can cut the leaver off" "$sc" "fails leavers-can-be-cut-off" + near "joiner-mover-leaver: stuck holding the direct assignment" "$sc" "fails leavers-can-be-cut-off" "prod-admin.holder=ada" + has "joiner-mover-leaver: while the group grant was removed" "$sc" "prod-engineers.holder: ada → ∅" + + dv=$("$WRIT" derive "$d/joiner-mover-leaver-shortcut.writ" "$d/joiner-mover-leaver.rules" left-behind 2>&1) + has "joiner-mover-leaver: G. every entitlement left behind was granted directly" "$dv" "prod-admin direct ada" + lacks "joiner-mover-leaver: and none through a group" "$dv" " group " +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From b1a388882bbe60aced757027d03e823277bce3e9 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:21:23 +0300 Subject: [PATCH 2/7] expense-approval: two signatures, one person A large expense needs the manager's and finance's approval. The shortcut pays when both slots are filled; Bob is manager and finance's deputy, so four allowed steps pay on one person's say-so. Amounts are bands, not numbers. compare reports never-on-one-person LOST while the law it breaks reads preserved (laws compare by declaration); the README says so. In the rules, independence is a join: a rules guard cannot compare a path with a path, though the claims language can. Also documented: in the safe process the only way to undo a signature is to reject, cancel, or change the bank account. Cross-check 41 -> 45 properties (43 compared, 2 fair skipped); 270 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + docker-compose.yml | 6 + expense-approval/README.md | 194 ++++++++++++++++++ .../expense-approval-shortcut.writ | 117 +++++++++++ expense-approval/expense-approval.claims | 34 +++ expense-approval/expense-approval.lib.writ | 12 ++ expense-approval/expense-approval.rules | 50 +++++ expense-approval/expense-approval.writ | 116 +++++++++++ modality-cross-check.sh | 2 +- run-tests.sh | 72 +++++-- 10 files changed, 585 insertions(+), 19 deletions(-) create mode 100644 expense-approval/README.md create mode 100644 expense-approval/expense-approval-shortcut.writ create mode 100644 expense-approval/expense-approval.claims create mode 100644 expense-approval/expense-approval.lib.writ create mode 100644 expense-approval/expense-approval.rules create mode 100644 expense-approval/expense-approval.writ diff --git a/README.md b/README.md index 4d7e2ae..1e14580 100644 --- a/README.md +++ b/README.md @@ -53,6 +53,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`workflow/`](workflow/) | Can a KYC case ever get stuck? | Never — and where automation ends, a declared gap hands it to a human. | | [`access/`](access/) | Can an admin grant always be revoked? | No: the break-glass grant is a latch. | | [`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. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/docker-compose.yml b/docker-compose.yml index 754ec7a..e049cfd 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -77,6 +77,12 @@ services: image: writ-problems command: ["joiner_mover_leaver"] + # Two approvals, one person: the independence check payment forgot. + expense-approval: + build: . + image: writ-problems + command: ["expense_approval"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/expense-approval/README.md b/expense-approval/README.md new file mode 100644 index 0000000..9ce63d0 --- /dev/null +++ b/expense-approval/README.md @@ -0,0 +1,194 @@ +# Expense approval: two signatures, one person + +An expense above the approval threshold needs two approvals: the requester's +manager, then finance. The rule exists so that no one person can move money +alone. Every form, screen and audit report enforces it as "two approvals", +meaning both signature boxes are filled. + +That is not the same rule. Bob is Ann's manager and also finance's deputy +approver, which is common in a small team. He can fill both boxes. The +expense is paid on two signatures, and one person decided it. + +## The process + +``` +draft ──submit──▶ submitted ──manager signs──▶ ──finance signs──▶ ──pay──▶ paid + │ ▲ + reject│ │resubmit (signatures are thrown away) + ▼ │ + rejected + +cancel: from draft, submitted or rejected, at any point before payment +change-bank-account: while submitted; throws away every signature so far +``` + +## Counting becomes naming + +The model has no amounts. The rules only ever ask which side of the threshold +an amount falls on, so the expense carries a **band**, `small` or `large`, and +the process branches on that. Nothing is lost: no rule here would answer +differently for $12,000 than for $10,001. If a rule distinguished a middle +band (say, manager-only approval up to $5,000), the band would get a third +member. The model would still not do arithmetic. + +## The model + +[`expense-approval.writ`](expense-approval.writ) follows one large expense, +`e1`, filed by `ann`. Its stage, its bank account and two signature slots +(`manager-sign`, `finance-sign`) are what change. Three rules are laws, +reported whenever any reachable situation breaks them: + +- `no-self-approval`: nobody signs their own expense; +- `finance-after-manager`: the finance slot is never filled before the + manager's; +- `two-for-large`: a large expense is paid only on two independent + approvals. + +"Independent" is written in [`expense-approval.lib.writ`](expense-approval.lib.writ) +as both slots filled *and* different: + +```lisp +(form (two-independent E) + (and (defined E.manager-sign) + (defined E.finance-sign) + (differ E.manager-sign E.finance-sign))) +``` + +`differ` on its own would not do: it is true when either slot is empty. + +The signing moves are one per person and slot (`bob-approves-as-manager`, +`bob-approves-for-finance`, `cat-approves-for-finance`, and +`ann-approves-as-manager`, which its guard always refuses). Changing the bank +account is one move with three effects that happen at once: the new account, +and both signatures thrown away, because the approvers approved paying the +*old* account. + +The two files differ in `pay`. The safe process pays a large expense on +`two-independent`. [`expense-approval-shortcut.writ`](expense-approval-shortcut.writ) +pays it on both slots being filled. + +## What writ answers + +Both processes are asked the questions in +[`expense-approval.claims`](expense-approval.claims). The safe one, exit 0: + +``` +states: 21 edges: 34 +… +holds payable + "a large expense can be paid" + witness: 1. submit → #1 e1.stage: draft → submitted + 2. bob-approves-as-manager → #3 e1.manager-sign: ∅ → bob + 3. cat-approves-for-finance → #7 e1.finance-sign: ∅ → cat + 4. pay → #14 e1.stage: submitted → paid +holds never-on-one-person +holds always-settleable +holds settles + assuming fair: pay, cancel +certified: every answer re-derived from the model (writ-cert) +``` + +The shortcut, exit 1: + +``` +equation two-for-large + … + violated in 2 reachable situations witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay → #13 +… +fails never-on-one-person + "a large expense is never paid on one person's say-so" + witness: 1. submit → #1 e1.stage: draft → submitted + 2. bob-approves-as-manager → #3 e1.manager-sign: ∅ → bob + 3. bob-approves-for-finance → #6 e1.finance-sign: ∅ → bob + 4. pay → #13 e1.stage: submitted → paid +holds settles +``` + +Four steps, each allowed: Bob may approve as manager, Bob may approve for +finance, and the payment sees two signatures. Only one rule breaks, and the +shortcut still pays and still settles, so every question except "was it +independent" answers in its favour. + +`writ derive` lists each payment with its two signatories, which is what an +auditor would ask for: + +```sh +writ derive expense-approval-shortcut.writ expense-approval.rules paid-by +``` + +``` +paid-by (4 rows) + 13 bob bob + 15 bob cat + 20 bob bob + 22 bob cat +``` + +## Comparing the two + +```sh +writ compare expense-approval.writ expense-approval-shortcut.writ # exit 1 +``` + +``` +equations: no-self-approval preserved + finance-after-manager preserved + two-for-large preserved +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. + +## A question for whoever owns the process + +In the safe process, an expense Bob has signed twice cannot be paid. That is +the point. But look at where it is stuck: + +```sh +writ show expense-approval.writ --at 6 +``` + +``` +situation 6 of 21 + cells: (e1.stage=submitted e1.bank=old-account e1.manager-sign=bob e1.finance-sign=bob) + … + moves: reject → 4 cancel → 12 change-bank-account → 5 +``` + +There is no way to withdraw one signature. The ways out are to reject the +expense, cancel it, or change its bank account, which throws the signatures +away as a side effect. Someone will find the third one. Either give finance an +explicit "withdraw my signature" step, or refuse the second signature from the +person who gave the first, at signing time rather than at payment. + +## What to take away + +The rule people state ("two approvals") and the rule people mean ("two +people") differ only when one person holds two roles. That happens most +where controls matter most: small teams, deputies, holiday cover. The check +that counts filled boxes passes. The check that compares names does not. + +To adapt it, add your approval levels as slots and your bands as members, and +list who may sign which slot from the delegation-of-authority document, not +the org chart. + +## Run it + +```sh +writ check expense-approval.writ --claims expense-approval.claims # exit 0 +writ check expense-approval-shortcut.writ --claims expense-approval.claims # exit 1 +``` + +[`expense-approval.rules`](expense-approval.rules) encodes the same questions +for `writ derive`. `../modality-cross-check.sh` checks the two answers agree, +except `settles`, which carries a fairness assumption the rules encoding does +not model. In the rules, independence is a join (the same variable in both +slots) rather than `differ`, because a rules guard compares a path with a +constant or a variable, never with another path. diff --git a/expense-approval/expense-approval-shortcut.writ b/expense-approval/expense-approval-shortcut.writ new file mode 100644 index 0000000..fc9593b --- /dev/null +++ b/expense-approval/expense-approval-shortcut.writ @@ -0,0 +1,117 @@ +; The same process, with ONE CONDITION REMOVED from payment: a large expense +; needs both signature slots filled, and no longer asks whether they were +; filled by two different people. +; +; Every form, every screen and every audit report says "two approvals". Bob is +; Ann's manager and also finance's deputy approver, so he can fill both. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "expense-approval.lib.writ") + +(schema expense-approval + + ; The amount, as the rules see it. They only ever ask which side of the + ; approval threshold it falls on, so that is all the model carries. + (type band-t (small large)) + + (type stage-t (draft submitted rejected paid cancelled)) + (type bank-t (old-account new-account)) + (type person) + + (type expense + (arrow requester (to person) fixed) + (arrow band (to band-t) fixed) + (arrow stage (to stage-t)) + (arrow bank (to bank-t)) + ; Two signature slots: the manager's, then finance's. + (maybe manager-sign person) + (maybe finance-sign person)) + + ; ---- the rules ---- + + ; Nobody signs their own expense. + (equation no-self-approval + (not (or (is expense.manager-sign expense.requester) + (is expense.finance-sign expense.requester)))) + + ; Finance signs only after the manager has. + (equation finance-after-manager + (not (and (defined expense.finance-sign) (not (defined expense.manager-sign))))) + + ; A large expense is paid only on two independent approvals. + (equation two-for-large + (not (and (is expense.stage paid) + (is expense.band large) + (not (two-independent expense)))))) + +(instance start expense-approval + + (person ann) ; files the expense + (person bob) ; her manager, and the finance team's deputy approver + (person cat) ; finance + + ; Above the threshold: two approvals needed. + (expense e1 (requester ann) (band large) (stage draft) (bank old-account) + (manager-sign vacant) (finance-sign vacant))) + +(use expense-approval) +(initial start) + +; ---- the process ---- + +(transition submit + (when (is e1.stage draft)) + (do (set e1.stage submitted))) + +; One move per person and slot. Each refuses the requester, and finance waits +; for the manager. +(form (approve-as-manager N P) + (transition N + (when (and (is e1.stage submitted) + (not (defined e1.manager-sign)) + (not (is e1.requester P)))) + (do (set e1.manager-sign P)))) +(form (approve-for-finance N P) + (transition N + (when (and (is e1.stage submitted) + (defined e1.manager-sign) + (not (defined e1.finance-sign)) + (not (is e1.requester P)))) + (do (set e1.finance-sign P)))) + +(approve-as-manager ann-approves-as-manager ann) ; refused: she filed it +(approve-as-manager bob-approves-as-manager bob) +(approve-for-finance bob-approves-for-finance bob) ; the deputy +(approve-for-finance cat-approves-for-finance cat) + +; Rejected expenses lose their signatures and can be resubmitted. +(transition reject + (when (is e1.stage submitted)) + (do (set e1.stage rejected) (vacate e1.manager-sign) (vacate e1.finance-sign))) +(transition resubmit + (when (is e1.stage rejected)) + (do (set e1.stage submitted))) + +; Cancellation is possible at any point before payment. +(transition cancel + (when (or (is e1.stage draft) (is e1.stage submitted) (is e1.stage rejected))) + (do (set e1.stage cancelled))) + +; Changing the bank account invalidates every approval: one move, three +; effects, all at once. Approvers approved paying THAT account. +(transition change-bank-account + (when (and (is e1.stage submitted) (is e1.bank old-account))) + (do (set e1.bank new-account) (vacate e1.manager-sign) (vacate e1.finance-sign))) + +; Pay: a small expense on the manager's signature; a large one on both +; signatures. +(transition pay + (when (and (is e1.stage submitted) + (defined e1.manager-sign) + (or (is e1.band small) + (and (defined e1.manager-sign) + (defined e1.finance-sign))))) ; <- differ, gone + (do (set e1.stage paid))) + diff --git a/expense-approval/expense-approval.claims b/expense-approval/expense-approval.claims new file mode 100644 index 0000000..7b3f2a8 --- /dev/null +++ b/expense-approval/expense-approval.claims @@ -0,0 +1,34 @@ +; The questions, put to both processes. + +(load "expense-approval.lib.writ") + +(property payable + "a large expense can be paid" + (possible (is e1.stage paid))) + +(property never-on-one-person + "a large expense is never paid on one person's say-so" + (never (and (is e1.stage paid) (not (two-independent e1))))) + +(property always-settleable + "from everywhere, payment or cancellation can still be reached" + (live (settled e1))) + +(property settles + "every run ends paid or cancelled, if paying and cancelling are not ignored forever" + (inevitable (settled e1) (fair pay cancel))) + +; ---- ownership ---- +; Every step that writes a signature slot or the stage is on a rule's route. +; The guards are what keep the rules; each step is acknowledged here, and the +; law that still breaks is the one a guard stopped checking. +(accept ann-approves-as-manager no-self-approval finance-after-manager two-for-large) +(accept bob-approves-as-manager no-self-approval finance-after-manager two-for-large) +(accept bob-approves-for-finance no-self-approval finance-after-manager two-for-large) +(accept cat-approves-for-finance no-self-approval finance-after-manager two-for-large) +(accept reject no-self-approval finance-after-manager two-for-large) +(accept change-bank-account no-self-approval finance-after-manager two-for-large) +(accept submit two-for-large) +(accept resubmit two-for-large) +(accept cancel two-for-large) +(accept pay two-for-large) diff --git a/expense-approval/expense-approval.lib.writ b/expense-approval/expense-approval.lib.writ new file mode 100644 index 0000000..d45ed1d --- /dev/null +++ b/expense-approval/expense-approval.lib.writ @@ -0,0 +1,12 @@ +; 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") + +; Two approvals, by two different people. Never bare `differ`: it is true when +; either slot is empty, so "two different signatures" needs both defined. +(form (two-independent E) + (and (defined E.manager-sign) + (defined E.finance-sign) + (differ E.manager-sign E.finance-sign))) + +(form (settled E) (or (is E.stage paid) (is E.stage cancelled))) diff --git a/expense-approval/expense-approval.rules b/expense-approval/expense-approval.rules new file mode 100644 index 0000000..b878d04 --- /dev/null +++ b/expense-approval/expense-approval.rules @@ -0,0 +1,50 @@ +; The same questions, answered a second time by a different part of `writ`, so +; that `modality-cross-check.sh` can compare them. A disagreement is a bug in +; one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +; `settles` carries (fair …), which ct.rules does not encode; the +; cross-check skips it and says so. +(load "ct.rules") +(load "expense-approval.lib.writ") + +(satisfies payable (is e1.stage paid)) + +; `two-independent` compares one path with another (`differ A.x A.y`), which +; the claims language allows and a rules guard does not: a guard compares a +; path with a constant or a variable. So independence is said the Datalog way. +; The same variable in both slots is the same person. +(relation same-signer (Situation)) +(rule (same-signer S) + (situation S) + (holds S (is e1.manager-sign P)) + (holds S (is e1.finance-sign P))) + +(relation independent (Situation)) +(rule (independent S) + (situation S) + (holds S (defined e1.manager-sign)) + (holds S (defined e1.finance-sign)) + (not (same-signer S))) + +(relation never-on-one-person (Situation)) +(rule (never-on-one-person S) + (situation S) + (holds S (is e1.stage paid)) + (not (independent S))) + +(satisfies is-settled (settled e1)) +(can-reach can-settle is-settled) +(trapped always-settleable can-settle) + +; ---- the explanation ---- +; Every payment, with who signed it: the situation, the manager's signature, +; finance's. An auditor reads down the last two columns for a repeated name. +(relation paid-by (Situation person person)) +(rule (paid-by S A B) + (situation S) + (holds S (is e1.stage paid)) + (holds S (is e1.manager-sign A)) + (holds S (is e1.finance-sign B))) diff --git a/expense-approval/expense-approval.writ b/expense-approval/expense-approval.writ new file mode 100644 index 0000000..856cdac --- /dev/null +++ b/expense-approval/expense-approval.writ @@ -0,0 +1,116 @@ +; An expense approval process. +; +; Ann files an expense. Her manager approves it; above the threshold, finance +; approves it too, and only after the manager. It is then paid. Along the way +; it can be rejected and resubmitted, cancelled before payment, and its bank +; account changed, which throws away every approval so far. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "expense-approval.lib.writ") + +(schema expense-approval + + ; The amount, as the rules see it. They only ever ask which side of the + ; approval threshold it falls on, so that is all the model carries. + (type band-t (small large)) + + (type stage-t (draft submitted rejected paid cancelled)) + (type bank-t (old-account new-account)) + (type person) + + (type expense + (arrow requester (to person) fixed) + (arrow band (to band-t) fixed) + (arrow stage (to stage-t)) + (arrow bank (to bank-t)) + ; Two signature slots: the manager's, then finance's. + (maybe manager-sign person) + (maybe finance-sign person)) + + ; ---- the rules ---- + + ; Nobody signs their own expense. + (equation no-self-approval + (not (or (is expense.manager-sign expense.requester) + (is expense.finance-sign expense.requester)))) + + ; Finance signs only after the manager has. + (equation finance-after-manager + (not (and (defined expense.finance-sign) (not (defined expense.manager-sign))))) + + ; A large expense is paid only on two independent approvals. + (equation two-for-large + (not (and (is expense.stage paid) + (is expense.band large) + (not (two-independent expense)))))) + +(instance start expense-approval + + (person ann) ; files the expense + (person bob) ; her manager, and the finance team's deputy approver + (person cat) ; finance + + ; Above the threshold: two approvals needed. + (expense e1 (requester ann) (band large) (stage draft) (bank old-account) + (manager-sign vacant) (finance-sign vacant))) + +(use expense-approval) +(initial start) + +; ---- the process ---- + +(transition submit + (when (is e1.stage draft)) + (do (set e1.stage submitted))) + +; One move per person and slot. Each refuses the requester, and finance waits +; for the manager. +(form (approve-as-manager N P) + (transition N + (when (and (is e1.stage submitted) + (not (defined e1.manager-sign)) + (not (is e1.requester P)))) + (do (set e1.manager-sign P)))) +(form (approve-for-finance N P) + (transition N + (when (and (is e1.stage submitted) + (defined e1.manager-sign) + (not (defined e1.finance-sign)) + (not (is e1.requester P)))) + (do (set e1.finance-sign P)))) + +(approve-as-manager ann-approves-as-manager ann) ; refused: she filed it +(approve-as-manager bob-approves-as-manager bob) +(approve-for-finance bob-approves-for-finance bob) ; the deputy +(approve-for-finance cat-approves-for-finance cat) + +; Rejected expenses lose their signatures and can be resubmitted. +(transition reject + (when (is e1.stage submitted)) + (do (set e1.stage rejected) (vacate e1.manager-sign) (vacate e1.finance-sign))) +(transition resubmit + (when (is e1.stage rejected)) + (do (set e1.stage submitted))) + +; Cancellation is possible at any point before payment. +(transition cancel + (when (or (is e1.stage draft) (is e1.stage submitted) (is e1.stage rejected))) + (do (set e1.stage cancelled))) + +; Changing the bank account invalidates every approval: one move, three +; effects, all at once. Approvers approved paying THAT account. +(transition change-bank-account + (when (and (is e1.stage submitted) (is e1.bank old-account))) + (do (set e1.bank new-account) (vacate e1.manager-sign) (vacate e1.finance-sign))) + +; Pay: a small expense on the manager's signature; a large one on two +; signatures by two different people. +(transition pay + (when (and (is e1.stage submitted) + (defined e1.manager-sign) + (or (is e1.band small) + (two-independent e1)))) + (do (set e1.stage paid))) + diff --git a/modality-cross-check.sh b/modality-cross-check.sh index bd3c147..8c9aa21 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index 9742087..b60a9d8 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,20 +431,21 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The sixteen scenarios this script walks by convention, and their 41 + # The seventeen scenarios this script walks by convention, and their 45 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the sixteen fails this line, which is the point of it — + # property to any of the seventeen 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, and 31 -> 41 with the three - # entitlement-problems (3 + 3 + 4), and this line is where each of those had - # to be said out loud. - has "cross-check: all 41 properties of the sixteen scenarios were considered" \ - "$out" "considered 41 properties" - # One of the 41 is not compared, and the count above is the only place that - # would notice if the reason changed: two-phase-commit asks one property under - # a fairness assumption, which ct.rules §8 does not encode. - has "cross-check: with the one fair property skipped, and saying why" \ + # 26 -> 31 with two-phase-commit, 31 -> 41 with the three + # entitlement-problems (3 + 3 + 4), and 41 -> 45 with expense-approval, and + # this line is where each of those had to be said out loud. + has "cross-check: all 45 properties of the seventeen scenarios were considered" \ + "$out" "considered 45 properties: 43 compared, 2 not compared" + # Two of the 45 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. + has "cross-check: with the fair properties skipped, and saying why" \ "$out" "carries (fair …) — no rules encoding, skipped" has "cross-check: A. a possible is its satisfying set — non-empty holds" \ "$out" "river/solvable possible: satisfying set of" @@ -456,14 +457,17 @@ crosscheck() { # branch — which announced itself as unexercised on every prior run — is now # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring - # four more, since "nobody ever holds X" is how an access rule is said. + # four more, since "nobody ever holds X" is how an access rule is said, and + # expense-approval one. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 7 properties compared" - # And `inevitable`, whose two are two-phase-commit's — the newest modality, - # and the one whose second implementation is newest, so the line that says it - # is being compared at all is worth having. + "never: 8 properties compared" + # And `inevitable`, two of whose three are two-phase-commit's — the newest + # modality, and the one whose second implementation is newest, so the line + # that says it is being compared at all is worth having. The third is + # expense-approval's `settles`, a fair one: this line counts properties + # considered, so it counts that one too, though it is skipped. has "cross-check: D. the inevitable branch is exercised too" "$out" \ - "inevitable: 2" + "inevitable: 3" has "cross-check: an inevitable is its ESCAPE set, empty holds" "$out" \ "two-phase-commit/must-decide inevitable: counterexample set of 10" has "cross-check: a never is a COUNTEREXAMPLE set, like live" "$out" \ @@ -684,9 +688,41 @@ joiner_mover_leaver() { lacks "joiner-mover-leaver: and none through a group" "$dv" " group " } +expense_approval() { + d="$here/expense-approval" + echo "== Expense approval — two signatures, one person ==" + echo " Q: can a large expense be paid without two independent approvals?" + out=$("$WRIT" check "$d/expense-approval.writ" --claims "$d/expense-approval.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "expense-approval: the process is clean" "$st" 0 + has "expense-approval: A. a large expense can be paid" "$out" "holds payable" + near "expense-approval: on the manager's signature and finance's" "$out" "holds payable" "cat-approves-for-finance" + has "expense-approval: B. never on one person's say-so" "$out" "holds never-on-one-person" + has "expense-approval: C. and every run settles, paid or cancelled" "$out" "holds settles" + lacks "expense-approval: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/expense-approval-shortcut.writ" --claims "$d/expense-approval.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "expense-approval: \"both slots filled\" is refused" "$sst" 1 + has "expense-approval: D. paid on two signatures by one person" "$sc" "violated in 2 reachable situations witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay" + has "expense-approval: and only that rule breaks" "$sc" "fails never-on-one-person" + has "expense-approval: E. yet it still pays, and still settles" "$sc" "holds settles" + + 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" + + 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" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From f06acb1e4e360c6769d2d151344b8b7e8ac97f0e Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:24:50 +0300 Subject: [PATCH 3/7] agent-guardrails: an AI agent's tool policy, and the read-only tool that leaks MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Policy v1 allows file reads outright and makes the shell ask; v2 adds a web-fetch allowed outright. compare: no-unapproved-exfiltration LOST in three moves — switch-to-auto, read-secret-with-file-read, send-secret-with-web-fetch — none of them human; the verdict names t = web-fetch. The loop, run against the unedited claims: the honest fix (web-fetch asks) holds everything but stays exit 1 until the human acknowledges its new approval path; the cheat (delete the `out` arrow) turns the safety property n/a and `writ check` EXITS 0 — compare against v1 refuses it. Tested as is. Cross-check 45 -> 49 properties (47 compared); 289 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + agent-guardrails/README.md | 192 +++++++++++++++++++++ agent-guardrails/agent-guardrails-v2.writ | 117 +++++++++++++ agent-guardrails/agent-guardrails.claims | 28 +++ agent-guardrails/agent-guardrails.lib.writ | 6 + agent-guardrails/agent-guardrails.rules | 29 ++++ agent-guardrails/agent-guardrails.writ | 114 ++++++++++++ agent-guardrails/attempt-fetch-asks.writ | 116 +++++++++++++ agent-guardrails/attempt-forget-out.writ | 110 ++++++++++++ docker-compose.yml | 6 + modality-cross-check.sh | 2 +- run-tests.sh | 78 +++++++-- 12 files changed, 788 insertions(+), 11 deletions(-) create mode 100644 agent-guardrails/README.md create mode 100644 agent-guardrails/agent-guardrails-v2.writ create mode 100644 agent-guardrails/agent-guardrails.claims create mode 100644 agent-guardrails/agent-guardrails.lib.writ create mode 100644 agent-guardrails/agent-guardrails.rules create mode 100644 agent-guardrails/agent-guardrails.writ create mode 100644 agent-guardrails/attempt-fetch-asks.writ create mode 100644 agent-guardrails/attempt-forget-out.writ diff --git a/README.md b/README.md index 1e14580..40bceb6 100644 --- a/README.md +++ b/README.md @@ -54,6 +54,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`access/`](access/) | Can an admin grant always be revoked? | No: the break-glass grant is a latch. | | [`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. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/agent-guardrails/README.md b/agent-guardrails/README.md new file mode 100644 index 0000000..b551dcb --- /dev/null +++ b/agent-guardrails/README.md @@ -0,0 +1,192 @@ +# An AI agent's tool policy, and the read-only tool that leaks + +An AI coding agent works through tools: read a file, run a shell command, +fetch a web page. Its harness applies a **policy** to every call. Some tools +are allowed outright. The rest wait for a human to say yes. In **ask** mode +the human is there. In **auto** mode the agent works on its own with the +tools the policy allows, which is the point of auto mode, and also its risk. + +The security question is never "would the agent do this". A web page the +agent reads can carry instructions (prompt injection), so any call the policy +permits is a call that can happen. The question is "would the policy let it". + +Version 1 of the policy allows file reading outright and makes the shell ask. +Version 2 adds one tool, `web-fetch`, allowed outright because "it only reads +pages". It cannot open a file, so it cannot leak one. It doesn't need to. The +agent read the API key earlier with a tool that was allowed to, and a request +to a URL carries whatever is in the URL. + +## The model + +[`agent-guardrails.writ`](agent-guardrails.writ) has: + +- a **session** whose `mode` is `ask` or `auto`. The human switches it either + way (`switch-to-auto`, `switch-to-ask`); +- **tools** with what they *can* do, a fact (`reads-secrets`, `reaches-net`), + and whether the policy *allows* them outright, a decision (`allowed`); +- one **secret**, `api-key`: whether it is in the agent's context, and whether + it has left, `stayed`, `approved` or `silent`; +- an approval **queue** holding the call waiting on the human, if any. + +The agent's moves are written per tool. `read-secret-with-file-read` puts the +key in context. `send-secret-with-T` sends it out with no one asked, and needs +auto mode, a tool allowed outright and a tool that reaches the network. +`ask-to-send-with-T` puts any other network call to the human, who answers +with `human-approves-T` or `human-denies`. + +One rule is a law: `no-silent-exfiltration`, the secret never ends up `silent`. + +[`agent-guardrails-v2.writ`](agent-guardrails-v2.writ) is version 1 plus the +`web-fetch` tool and the one move its permissions create. + +## What writ answers + +The human's questions are in [`agent-guardrails.claims`](agent-guardrails.claims). +Version 1, exit 0: + +``` +states: 8 edges: 16 +… +holds useful + "the agent can work on its own with what it has read" +holds human-can-release + "a human can still choose to send the secret" +holds no-unapproved-exfiltration + "a secret never leaves without a human saying yes" +holds human-can-interrupt + "from every situation, the human can still get back to ask mode" +``` + +Then compare the two versions: + +```sh +writ compare agent-guardrails.writ agent-guardrails-v2.writ # exit 1 +``` + +``` +equations: no-silent-exfiltration preserved +properties: useful preserved + human-can-release preserved + no-unapproved-exfiltration LOST witness: 1. switch-to-auto 2. read-secret-with-file-read 3. send-secret-with-web-fetch + human-can-interrupt preserved +``` + +**Under policy v2, a secret leaves the machine in three moves with no human +decision among them: switch to auto mode, read a file that holds the key, +fetch a URL.** That sentence can go straight into the policy ticket. + +`writ check` on version 2 adds two details. The verdict names the tool, from +the `(show carrier)` on the property: + +``` +fails no-unapproved-exfiltration + … + carrier (at state 6) + t = web-fetch +``` + +The second detail is a line the human's claims file caused: + +``` +unadmitted send-secret-with-web-fetch may break no-silent-exfiltration +``` + +The new tool created a move that can break the rule, and nobody acknowledged +it. writ reports that before anyone asks. + +[`agent-guardrails.rules`](agent-guardrails.rules) lists every unasked +exfiltration with its tool and the mode at the time: + +``` +exfil-path (4 rows) + 6 web-fetch auto + 9 web-fetch auto + 10 web-fetch ask + 11 web-fetch ask +``` + +The `ask` rows are situations where the secret had already left and the human +switched back afterwards. Switching back closes nothing that already happened. + +## The loop + +The architecture the writ recommendations propose: an LLM writes or edits the +model, writ verifies it, and the LLM revises until it holds. That works only +under one discipline: **the claims file is the human's, and the agent may not +edit it.** An agent told "make v2 pass" can change the policy. It cannot +change the questions. Two attempts are in this directory, and both were run +against the unedited `agent-guardrails.claims`. + +**The honest fix:** [`attempt-fetch-asks.writ`](attempt-fetch-asks.writ) stops +allowing `web-fetch` outright, so a fetch asks like the shell does. Every +question holds, `useful` included: the agent still works on its own in auto +mode. `check` still exits 1: + +``` +unadmitted human-approves-web-fetch may break no-silent-exfiltration +``` + +The fix added a new way for the secret to leave, through a human's approval. +Whether that is acceptable is the human's call, so the acknowledgement goes in +the human's file. `writ compare agent-guardrails.writ attempt-fetch-asks.writ` +exits 0: nothing v1 guaranteed was lost. + +**The cheat:** [`attempt-forget-out.writ`](attempt-forget-out.writ) changes +nothing the policy allows. It deletes the record of the secret leaving: the +`out` arrow, and the law that read it. Every dangerous call is still there. + +``` +holds useful +n/a human-can-release +n/a no-unapproved-exfiltration +holds human-can-interrupt +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. + +So treat `n/a` as a failure, and gate on `compare` against the last version +the human approved, which refuses it: + +```sh +writ compare agent-guardrails.writ attempt-forget-out.writ # exit 1 +``` + +``` +equations: no-silent-exfiltration LOST +properties: useful preserved + human-can-release LOST + no-unapproved-exfiltration LOST + human-can-interrupt 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. + +## What to take away + +A tool's risk is not what it can read but what it can carry. `web-fetch` was +judged on the first and was dangerous on the second, because the danger needs +two tools: one that puts the secret in context and one that sends context +out. Neither is a problem alone, and a review that looks at one tool at a +time passes both. + +To adapt it, list your harness's tools with what each can read and reach, +give the secret the places it can come from, and write the policy as +`allowed`. The questions carry over unchanged. + +## Run it + +```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 compare agent-guardrails.writ attempt-forget-out.writ # exit 1 +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. diff --git a/agent-guardrails/agent-guardrails-v2.writ b/agent-guardrails/agent-guardrails-v2.writ new file mode 100644 index 0000000..dd6d6a8 --- /dev/null +++ b/agent-guardrails/agent-guardrails-v2.writ @@ -0,0 +1,117 @@ +; The same policy, version 2: ONE TOOL ADDED. Nothing else changes. +; +; web-fetch reads web pages, and the reasoning that let it run without asking +; was that reading is harmless: it cannot open a file, so it cannot leak one. +; It does not have to. The agent read the key earlier, with a tool that was +; allowed to, and a request to a URL carries whatever is in the URL. +; +; `writ compare agent-guardrails.writ agent-guardrails-v2.writ` exits 1. + +(load "stdlib.writ") +(load "agent-guardrails.lib.writ") + +(schema agent-guardrails + + (type yn (no yes)) + + ; ask: every tool call that is not allowed outright waits for the human. + ; auto: the agent runs on its own, using the tools the policy allows in auto. + (type mode-t (ask auto)) + (type session (arrow mode (to mode-t))) + + ; A tool: what it CAN do, which is a fact about the tool, and whether the + ; policy lets the agent call it without asking, which is a decision. + (type tool + (arrow reads-secrets (to yn) fixed) + (arrow reaches-net (to yn) fixed) + (arrow allowed (to yn) fixed) ; the policy: no approval needed + (arrow carried-secret (to yn))) ; it is the tool the secret left by + + ; Where the secret is: still only on disk, read into the agent's context, + ; and whether it has gone out over the network, and on whose say-so. + (type out-t (stayed approved silent)) + (type secret + (arrow in-context (to yn)) + (arrow out (to out-t))) + + ; The call waiting on the human, if any. + (type approvals (maybe pending tool)) + + ; ---- the rule ---- + + ; A secret never leaves without a human saying yes. + (equation no-silent-exfiltration (not (is secret.out silent)))) + +(instance start agent-guardrails + + (session s (mode ask)) + + ; Reading files is allowed outright: it is most of what a coding agent does, + ; and reading cannot send anything anywhere. + (tool file-read (reads-secrets yes) (reaches-net no) (allowed yes) (carried-secret no)) + ; The shell can do anything, so it always asks. + (tool shell (reads-secrets yes) (reaches-net yes) (allowed no) (carried-secret no)) + ; New in v2. "It only reads web pages", so it is allowed outright too. It + ; cannot read a secret. It does not need to: the secret is already in context, + ; and a GET request carries whatever is put in its URL. + (tool web-fetch (reads-secrets no) (reaches-net yes) (allowed yes) (carried-secret no)) + + (secret api-key (in-context no) (out stayed)) + (approvals queue (pending vacant))) + +(use agent-guardrails) +(initial start) + +; ---- the human ---- + +; Shift-tab, in the terminal: the mode is the human's to change, both ways. +(transition switch-to-auto (when (is s.mode ask)) (do (set s.mode auto))) +(transition switch-to-ask (when (is s.mode auto)) (do (set s.mode ask))) + +; ---- the agent ---- + +; The model is adversarial on purpose. A page the agent reads can carry +; instructions (prompt injection), so any call the policy permits is a call +; that may happen. The question is never "would the agent do this", only +; "would the policy let it". + +; Read the secret with a tool that can, if the policy allows that tool. +(form (read-secret-with N T) + (transition N + (when (and (is T.reads-secrets yes) (is T.allowed yes) (is api-key.in-context no))) + (do (set api-key.in-context yes)))) + +; Send what is in context somewhere, with no one asked: auto mode, a tool the +; policy allows outright, one that reaches the network. +(form (send-secret-with N T) + (transition N + (when (and (is s.mode auto) + (is T.allowed yes) + (is T.reaches-net yes) + (is api-key.in-context yes) + (is api-key.out stayed))) + (do (set api-key.out silent) (set T.carried-secret yes)))) + +; Any other network call is put to the human, in either mode. +(form (ask-to-send-with N T) + (transition N + (when (and (is T.reaches-net yes) + (is T.allowed no) + (is api-key.in-context yes) + (is api-key.out stayed) + (not (defined queue.pending)))) + (do (set queue.pending T)))) +(form (human-approves N T) + (transition N + (when (is queue.pending T)) + (do (set api-key.out approved) (set T.carried-secret yes) (vacate queue.pending)))) +(transition human-denies + (when (defined queue.pending)) + (do (vacate queue.pending))) + +(read-secret-with read-secret-with-file-read file-read) +(ask-to-send-with ask-to-send-with-shell shell) +(human-approves human-approves-shell shell) + +; ---- new in v2 ---- +(send-secret-with send-secret-with-web-fetch web-fetch) diff --git a/agent-guardrails/agent-guardrails.claims b/agent-guardrails/agent-guardrails.claims new file mode 100644 index 0000000..c5e6c08 --- /dev/null +++ b/agent-guardrails/agent-guardrails.claims @@ -0,0 +1,28 @@ +; The human's questions. An agent asked to fix the policy may edit the model; +; it may not edit this file. See the README. + +(load "agent-guardrails.lib.writ") + +(property useful + "the agent can work on its own with what it has read" + (possible (and (is s.mode auto) (is api-key.in-context yes)))) + +(property human-can-release + "a human can still choose to send the secret" + (possible (is api-key.out approved))) + +(property no-unapproved-exfiltration + "a secret never leaves without a human saying yes" + (never silently-out) + (show carrier)) + +(property human-can-interrupt + "from every situation, the human can still get back to ask mode" + (live (is s.mode ask))) + +; ---- through what ---- +(query carrier (where (t tool)) (is t.carried-secret yes)) + +; ---- ownership ---- +; Every move that writes where the secret is can break the rule. +(accept human-approves-shell no-silent-exfiltration) diff --git a/agent-guardrails/agent-guardrails.lib.writ b/agent-guardrails/agent-guardrails.lib.writ new file mode 100644 index 0000000..f431c1d --- /dev/null +++ b/agent-guardrails/agent-guardrails.lib.writ @@ -0,0 +1,6 @@ +; 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") + +; The secret has left the machine and no human said yes. +(form silently-out (is api-key.out silent)) diff --git a/agent-guardrails/agent-guardrails.rules b/agent-guardrails/agent-guardrails.rules new file mode 100644 index 0000000..add449d --- /dev/null +++ b/agent-guardrails/agent-guardrails.rules @@ -0,0 +1,29 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "agent-guardrails.lib.writ") + +(satisfies useful (and (is s.mode auto) (is api-key.in-context yes))) + +(satisfies human-can-release (is api-key.out approved)) + +(satisfies no-unapproved-exfiltration silently-out) + +(satisfies in-ask-mode (is s.mode ask)) +(can-reach can-get-to-ask in-ask-mode) +(trapped human-can-interrupt can-get-to-ask) + +; ---- the explanation ---- +; Every situation where the secret has left with nobody asked, and the tool it +; left by, with the mode the session was in. +(relation exfil-path (Situation tool mode-t)) +(rule (exfil-path S T M) + (situation S) + (holds S (is api-key.out silent)) + (holds S (is T.carried-secret yes)) + (holds S (is s.mode M))) diff --git a/agent-guardrails/agent-guardrails.writ b/agent-guardrails/agent-guardrails.writ new file mode 100644 index 0000000..c671833 --- /dev/null +++ b/agent-guardrails/agent-guardrails.writ @@ -0,0 +1,114 @@ +; An AI coding agent's tool-permission policy, version 1. +; +; The agent works through tools. A policy says which tools it may call +; without asking. In auto mode it then works on its own; in ask mode, and for +; any tool the policy does not allow outright, a human says yes or no. +; +; Version 1 has two tools: reading files, allowed outright, and the shell, +; which always asks. The question is whether a secret the agent has read can +; leave the machine without a human saying yes. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "agent-guardrails.lib.writ") + +(schema agent-guardrails + + (type yn (no yes)) + + ; ask: every tool call that is not allowed outright waits for the human. + ; auto: the agent runs on its own, using the tools the policy allows in auto. + (type mode-t (ask auto)) + (type session (arrow mode (to mode-t))) + + ; A tool: what it CAN do, which is a fact about the tool, and whether the + ; policy lets the agent call it without asking, which is a decision. + (type tool + (arrow reads-secrets (to yn) fixed) + (arrow reaches-net (to yn) fixed) + (arrow allowed (to yn) fixed) ; the policy: no approval needed + (arrow carried-secret (to yn))) ; it is the tool the secret left by + + ; Where the secret is: still only on disk, read into the agent's context, + ; and whether it has gone out over the network, and on whose say-so. + (type out-t (stayed approved silent)) + (type secret + (arrow in-context (to yn)) + (arrow out (to out-t))) + + ; The call waiting on the human, if any. + (type approvals (maybe pending tool)) + + ; ---- the rule ---- + + ; A secret never leaves without a human saying yes. + (equation no-silent-exfiltration (not (is secret.out silent)))) + +(instance start agent-guardrails + + (session s (mode ask)) + + ; Reading files is allowed outright: it is most of what a coding agent does, + ; and reading cannot send anything anywhere. + (tool file-read (reads-secrets yes) (reaches-net no) (allowed yes) (carried-secret no)) + ; The shell can do anything, so it always asks. + (tool shell (reads-secrets yes) (reaches-net yes) (allowed no) (carried-secret no)) + + (secret api-key (in-context no) (out stayed)) + (approvals queue (pending vacant))) + +(use agent-guardrails) +(initial start) + +; ---- the human ---- + +; Shift-tab, in the terminal: the mode is the human's to change, both ways. +(transition switch-to-auto (when (is s.mode ask)) (do (set s.mode auto))) +(transition switch-to-ask (when (is s.mode auto)) (do (set s.mode ask))) + +; ---- the agent ---- + +; The model is adversarial on purpose. A page the agent reads can carry +; instructions (prompt injection), so any call the policy permits is a call +; that may happen. The question is never "would the agent do this", only +; "would the policy let it". + +; Read the secret with a tool that can, if the policy allows that tool. +(form (read-secret-with N T) + (transition N + (when (and (is T.reads-secrets yes) (is T.allowed yes) (is api-key.in-context no))) + (do (set api-key.in-context yes)))) + +; Send what is in context somewhere, with no one asked: auto mode, a tool the +; policy allows outright, one that reaches the network. +(form (send-secret-with N T) + (transition N + (when (and (is s.mode auto) + (is T.allowed yes) + (is T.reaches-net yes) + (is api-key.in-context yes) + (is api-key.out stayed))) + (do (set api-key.out silent) (set T.carried-secret yes)))) + +; Any other network call is put to the human, in either mode. +(form (ask-to-send-with N T) + (transition N + (when (and (is T.reaches-net yes) + (is T.allowed no) + (is api-key.in-context yes) + (is api-key.out stayed) + (not (defined queue.pending)))) + (do (set queue.pending T)))) +(form (human-approves N T) + (transition N + (when (is queue.pending T)) + (do (set api-key.out approved) (set T.carried-secret yes) (vacate queue.pending)))) +(transition human-denies + (when (defined queue.pending)) + (do (vacate queue.pending))) + +(read-secret-with read-secret-with-file-read file-read) +(ask-to-send-with ask-to-send-with-shell shell) +(human-approves human-approves-shell shell) + diff --git a/agent-guardrails/attempt-fetch-asks.writ b/agent-guardrails/attempt-fetch-asks.writ new file mode 100644 index 0000000..71a741e --- /dev/null +++ b/agent-guardrails/attempt-fetch-asks.writ @@ -0,0 +1,116 @@ +; An agent's attempt to make v2 pass, the human's claims file untouched: +; web-fetch is no longer allowed outright. In auto mode the agent still works +; on its own; a fetch now asks, like the shell does. +; +; `writ check attempt-fetch-asks.writ --claims agent-guardrails.claims` +; exits 0 — honestly: every property is answered, and holds. + +(load "stdlib.writ") +(load "agent-guardrails.lib.writ") + +(schema agent-guardrails + + (type yn (no yes)) + + ; ask: every tool call that is not allowed outright waits for the human. + ; auto: the agent runs on its own, using the tools the policy allows in auto. + (type mode-t (ask auto)) + (type session (arrow mode (to mode-t))) + + ; A tool: what it CAN do, which is a fact about the tool, and whether the + ; policy lets the agent call it without asking, which is a decision. + (type tool + (arrow reads-secrets (to yn) fixed) + (arrow reaches-net (to yn) fixed) + (arrow allowed (to yn) fixed) ; the policy: no approval needed + (arrow carried-secret (to yn))) ; it is the tool the secret left by + + ; Where the secret is: still only on disk, read into the agent's context, + ; and whether it has gone out over the network, and on whose say-so. + (type out-t (stayed approved silent)) + (type secret + (arrow in-context (to yn)) + (arrow out (to out-t))) + + ; The call waiting on the human, if any. + (type approvals (maybe pending tool)) + + ; ---- the rule ---- + + ; A secret never leaves without a human saying yes. + (equation no-silent-exfiltration (not (is secret.out silent)))) + +(instance start agent-guardrails + + (session s (mode ask)) + + ; Reading files is allowed outright: it is most of what a coding agent does, + ; and reading cannot send anything anywhere. + (tool file-read (reads-secrets yes) (reaches-net no) (allowed yes) (carried-secret no)) + ; The shell can do anything, so it always asks. + (tool shell (reads-secrets yes) (reaches-net yes) (allowed no) (carried-secret no)) + ; New in v2. "It only reads web pages", so it is allowed outright too. It + ; cannot read a secret. It does not need to: the secret is already in context, + ; and a GET request carries whatever is put in its URL. + (tool web-fetch (reads-secrets no) (reaches-net yes) (allowed no) (carried-secret no)) + + (secret api-key (in-context no) (out stayed)) + (approvals queue (pending vacant))) + +(use agent-guardrails) +(initial start) + +; ---- the human ---- + +; Shift-tab, in the terminal: the mode is the human's to change, both ways. +(transition switch-to-auto (when (is s.mode ask)) (do (set s.mode auto))) +(transition switch-to-ask (when (is s.mode auto)) (do (set s.mode ask))) + +; ---- the agent ---- + +; The model is adversarial on purpose. A page the agent reads can carry +; instructions (prompt injection), so any call the policy permits is a call +; that may happen. The question is never "would the agent do this", only +; "would the policy let it". + +; Read the secret with a tool that can, if the policy allows that tool. +(form (read-secret-with N T) + (transition N + (when (and (is T.reads-secrets yes) (is T.allowed yes) (is api-key.in-context no))) + (do (set api-key.in-context yes)))) + +; Send what is in context somewhere, with no one asked: auto mode, a tool the +; policy allows outright, one that reaches the network. +(form (send-secret-with N T) + (transition N + (when (and (is s.mode auto) + (is T.allowed yes) + (is T.reaches-net yes) + (is api-key.in-context yes) + (is api-key.out stayed))) + (do (set api-key.out silent) (set T.carried-secret yes)))) + +; Any other network call is put to the human, in either mode. +(form (ask-to-send-with N T) + (transition N + (when (and (is T.reaches-net yes) + (is T.allowed no) + (is api-key.in-context yes) + (is api-key.out stayed) + (not (defined queue.pending)))) + (do (set queue.pending T)))) +(form (human-approves N T) + (transition N + (when (is queue.pending T)) + (do (set api-key.out approved) (set T.carried-secret yes) (vacate queue.pending)))) +(transition human-denies + (when (defined queue.pending)) + (do (vacate queue.pending))) + +(read-secret-with read-secret-with-file-read file-read) +(ask-to-send-with ask-to-send-with-shell shell) +(human-approves human-approves-shell shell) + +; ---- new in v2, as fixed ---- +(ask-to-send-with ask-to-send-with-web-fetch web-fetch) +(human-approves human-approves-web-fetch web-fetch) diff --git a/agent-guardrails/attempt-forget-out.writ b/agent-guardrails/attempt-forget-out.writ new file mode 100644 index 0000000..fd0aa90 --- /dev/null +++ b/agent-guardrails/attempt-forget-out.writ @@ -0,0 +1,110 @@ +; An agent's other attempt: nothing the policy allows changes. What goes is +; the record of the secret leaving — the `out` arrow, and the law that read it. +; The calls are all still there. +; +; `writ check attempt-forget-out.writ --claims agent-guardrails.claims` reports +; the safety property `n/a`: it names an arrow the model no longer has, so it +; is not answered at all. A harness that reads "no fails" as success has just +; been talked out of its question. Treat `n/a` as a failure. + +(load "stdlib.writ") +(load "agent-guardrails.lib.writ") + +(schema agent-guardrails + + (type yn (no yes)) + + ; ask: every tool call that is not allowed outright waits for the human. + ; auto: the agent runs on its own, using the tools the policy allows in auto. + (type mode-t (ask auto)) + (type session (arrow mode (to mode-t))) + + ; A tool: what it CAN do, which is a fact about the tool, and whether the + ; policy lets the agent call it without asking, which is a decision. + (type tool + (arrow reads-secrets (to yn) fixed) + (arrow reaches-net (to yn) fixed) + (arrow allowed (to yn) fixed) ; the policy: no approval needed + (arrow carried-secret (to yn))) ; it is the tool the secret left by + + ; Where the secret is: still only on disk, read into the agent's context, + ; and whether it has gone out over the network, and on whose say-so. + (type secret + (arrow in-context (to yn))) + + ; The call waiting on the human, if any. + (type approvals (maybe pending tool)) + + ) + +(instance start agent-guardrails + + (session s (mode ask)) + + ; Reading files is allowed outright: it is most of what a coding agent does, + ; and reading cannot send anything anywhere. + (tool file-read (reads-secrets yes) (reaches-net no) (allowed yes) (carried-secret no)) + ; The shell can do anything, so it always asks. + (tool shell (reads-secrets yes) (reaches-net yes) (allowed no) (carried-secret no)) + ; New in v2. "It only reads web pages", so it is allowed outright too. It + ; cannot read a secret. It does not need to: the secret is already in context, + ; and a GET request carries whatever is put in its URL. + (tool web-fetch (reads-secrets no) (reaches-net yes) (allowed yes) (carried-secret no)) + + (secret api-key (in-context no)) + (approvals queue (pending vacant))) + +(use agent-guardrails) +(initial start) + +; ---- the human ---- + +; Shift-tab, in the terminal: the mode is the human's to change, both ways. +(transition switch-to-auto (when (is s.mode ask)) (do (set s.mode auto))) +(transition switch-to-ask (when (is s.mode auto)) (do (set s.mode ask))) + +; ---- the agent ---- + +; The model is adversarial on purpose. A page the agent reads can carry +; instructions (prompt injection), so any call the policy permits is a call +; that may happen. The question is never "would the agent do this", only +; "would the policy let it". + +; Read the secret with a tool that can, if the policy allows that tool. +(form (read-secret-with N T) + (transition N + (when (and (is T.reads-secrets yes) (is T.allowed yes) (is api-key.in-context no))) + (do (set api-key.in-context yes)))) + +; Send what is in context somewhere, with no one asked: auto mode, a tool the +; policy allows outright, one that reaches the network. +(form (send-secret-with N T) + (transition N + (when (and (is s.mode auto) + (is T.allowed yes) + (is T.reaches-net yes) + (is api-key.in-context yes))) + (do (set T.carried-secret yes)))) + +; Any other network call is put to the human, in either mode. +(form (ask-to-send-with N T) + (transition N + (when (and (is T.reaches-net yes) + (is T.allowed no) + (is api-key.in-context yes) + (not (defined queue.pending)))) + (do (set queue.pending T)))) +(form (human-approves N T) + (transition N + (when (is queue.pending T)) + (do (set T.carried-secret yes) (vacate queue.pending)))) +(transition human-denies + (when (defined queue.pending)) + (do (vacate queue.pending))) + +(read-secret-with read-secret-with-file-read file-read) +(ask-to-send-with ask-to-send-with-shell shell) +(human-approves human-approves-shell shell) + +; ---- new in v2 ---- +(send-secret-with send-secret-with-web-fetch web-fetch) diff --git a/docker-compose.yml b/docker-compose.yml index e049cfd..2734486 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -83,6 +83,12 @@ services: image: writ-problems command: ["expense_approval"] + # An AI agent's tool policy: the read-only tool that carries a secret out. + agent-guardrails: + build: . + image: writ-problems + command: ["agent_guardrails"] + # 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 8c9aa21..35a7e8e 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index b60a9d8..ee66488 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,17 +431,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The seventeen scenarios this script walks by convention, and their 45 + # The eighteen scenarios this script walks by convention, and their 49 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the seventeen fails this line, which is the point of it — + # property to any of the eighteen 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), and 41 -> 45 with expense-approval, and - # this line is where each of those had to be said out loud. - has "cross-check: all 45 properties of the seventeen scenarios were considered" \ - "$out" "considered 45 properties: 43 compared, 2 not compared" - # Two of the 45 are not compared, and the count above is the only place that + # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and + # 45 -> 49 with agent-guardrails, and this line is where each of those had to + # be said out loud. + has "cross-check: all 49 properties of the eighteen scenarios were considered" \ + "$out" "considered 49 properties: 47 compared, 2 not compared" + # Two of the 49 are not compared, and the count above is the only place that # 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. @@ -458,9 +459,9 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval one. + # expense-approval and agent-guardrails one each. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 8 properties compared" + "never: 9 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -720,9 +721,66 @@ expense_approval() { has "expense-approval: G. derive lists who signed each payment" "$dv" "13 bob bob" } +agent_guardrails() { + d="$here/agent-guardrails" + c="$d/agent-guardrails.claims" + echo "== An AI agent's tool policy — and the read-only tool that leaks ==" + echo " Q: can a secret leave the machine with no human saying yes?" + out=$("$WRIT" check "$d/agent-guardrails.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "agent-guardrails: policy v1 is clean" "$st" 0 + has "agent-guardrails: A. the agent can work on its own" "$out" "holds useful" + has "agent-guardrails: B. no secret leaves unasked" "$out" "holds no-unapproved-exfiltration" + has "agent-guardrails: and the human can always interrupt" "$out" "holds human-can-interrupt" + + cmp=$("$WRIT" compare "$d/agent-guardrails.writ" "$d/agent-guardrails-v2.writ" 2>&1) + cst=$? + printf '%s\n' "$cmp" | sed 's/^/ | /' + exit_is "agent-guardrails: compare refuses v2" "$cst" 1 + has "agent-guardrails: C. adding a read-only tool loses the guarantee, in three moves" "$cmp" \ + "no-unapproved-exfiltration LOST witness: 1. switch-to-auto 2. read-secret-with-file-read 3. send-secret-with-web-fetch" + # The headline: the route contains no human move. Asserted on the route + # line itself, since every human move's name starts with `human-`. + route=$(printf '%s\n' "$cmp" | grep "no-unapproved-exfiltration LOST") + lacks "agent-guardrails: and no human move is on the route" "$route" "human-" + has "agent-guardrails: while the agent stays exactly as useful" "$cmp" "useful preserved" + + v2=$("$WRIT" check "$d/agent-guardrails-v2.writ" --claims "$c" 2>&1) + near "agent-guardrails: D. the verdict names the tool" "$v2" "carrier (at state 6)" "t = web-fetch" + has "agent-guardrails: and the new move is one the human never acknowledged" "$v2" \ + "unadmitted send-secret-with-web-fetch may break no-silent-exfiltration" + + # The loop: an agent asked to make v2 pass, the claims file held fixed. + fx=$("$WRIT" check "$d/attempt-fetch-asks.writ" --claims "$c" 2>&1) + fst=$? + exit_is "agent-guardrails: E. the honest fix still awaits the human" "$fst" 1 + has "agent-guardrails: every question holds" "$fx" "holds no-unapproved-exfiltration" + has "agent-guardrails: but its new approval path is the human's to acknowledge" "$fx" \ + "unadmitted human-approves-web-fetch may break no-silent-exfiltration" + fc=$("$WRIT" compare "$d/agent-guardrails.writ" "$d/attempt-fetch-asks.writ" 2>&1) + fcst=$? + exit_is "agent-guardrails: and compare against v1 accepts it" "$fcst" 0 + + 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. + 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 + 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 + has "agent-guardrails: naming the question it took away" "$cc" "no-unapproved-exfiltration LOST" + + dv=$("$WRIT" derive "$d/agent-guardrails-v2.writ" "$d/agent-guardrails.rules" exfil-path 2>&1) + has "agent-guardrails: H. derive lists the tool and the mode" "$dv" "6 web-fetch auto" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From 7fa791a90b4df89f4f3073ef509c26af78e9cf91 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:27:49 +0300 Subject: [PATCH 4/7] deployment: a rolling deploy, and the rollback that is not always there Three instances rolled r1 -> r2 behind a health gate, then a one-way migration. The safe plan fails can-roll-back: the runbook done right, eight steps, ends where r1 is unreachable for good; ct.rules one-way names `migrate` and nothing else. The shortcut drops the health gate and goes dark in four steps. Writing it, writ found a race in the first draft: finish the rollout, decide to roll back, and the migration (guarded on the instances only) runs anyway; the rollback then starts r1 on v2. migrate now also requires target r2. Cross-check 49 -> 52 properties (50 compared); 301 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + deployment/README.md | 152 ++++++++++++++++++++++++++++ deployment/deployment-shortcut.writ | 115 +++++++++++++++++++++ deployment/deployment.claims | 36 +++++++ deployment/deployment.lib.writ | 16 +++ deployment/deployment.rules | 25 +++++ deployment/deployment.writ | 119 ++++++++++++++++++++++ docker-compose.yml | 6 ++ modality-cross-check.sh | 2 +- run-tests.sh | 52 ++++++++-- 10 files changed, 513 insertions(+), 11 deletions(-) create mode 100644 deployment/README.md create mode 100644 deployment/deployment-shortcut.writ create mode 100644 deployment/deployment.claims create mode 100644 deployment/deployment.lib.writ create mode 100644 deployment/deployment.rules create mode 100644 deployment/deployment.writ diff --git a/README.md b/README.md index 40bceb6..aabf38c 100644 --- a/README.md +++ b/README.md @@ -55,6 +55,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`entitlement-problems/`](entitlement-problems/) | Can a requester approve, a developer edit CloudTrail, a leaver keep admin? | Yes, each through steps that are fine one at a time. writ names who, and through which grants. | | [`expense-approval/`](expense-approval/) | Can a large expense be paid without two independent approvals? | Yes, when one person holds both roles: "two signatures" counted boxes, not people. | | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. | +| [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/deployment/README.md b/deployment/README.md new file mode 100644 index 0000000..e9b58e6 --- /dev/null +++ b/deployment/README.md @@ -0,0 +1,152 @@ +# A rolling deploy, and the rollback that is not always there + +Three instances serve production on release r1 against schema v1. The +release is r2, and r2 comes with a migration to v2 that drops a column r1 +reads. The runbook: + +``` +target r2 ──▶ replace a ──▶ a healthy ──▶ replace b ──▶ b healthy ──▶ replace c ──▶ c healthy ──▶ migrate + │ +rollback: target r1, then replace back (no way back from here) ◀┘ +``` + +Each instance is replaced only while the other two are serving (the **health +gate**). The migration runs when every instance is on r2 and serving. And the +runbook has a rollback section: point the fleet back at r1 and replace the +instances again. + +The rollback section is true until the migration runs. After that it +describes a step that cannot happen: r1 cannot read v2, and nothing turns v2 +back into v1. A rollback is a claim about the reachable states, not a button, +and here the claim stops being true one lawful step into the runbook. + +## The model + +[`deployment.writ`](deployment.writ) has three instances (`a`, `b`, `c`), +each with a release (`at`) and a state (`starting`, `healthy`, `down`); the +fleet's `target`; and the database's schema `at` (`v1`, `v2`). + +- `target-r2` starts the release. `roll-back-target` points back at r1, but + only while the schema is still v1. +- `replace-a-with-r2` and the rest take an instance out and start it on the + target release. The safe guard is the health gate: the other two instances + are `healthy`. +- `a-passes-health` and the rest: a starting instance becomes healthy only if + its release can read the schema (`compatible` in + [`deployment.lib.writ`](deployment.lib.writ)). An r1 instance started on v2 + crash-loops for ever. +- `a-crashes` and `a-restarts`: the environment. **One instance fails at a + time.** A crash is only possible while the other two are serving. Without + that fault model, three independent crashes darken production under any + rollout, and the question would be about hardware, not the runbook. +- `migrate`: v1 → v2, once the rollout has finished. There is no inverse. + +One law, `no-mismatch`: no r1 instance is serving once the schema is v2. + +[`deployment-shortcut.writ`](deployment-shortcut.writ) removes the health gate +from the replacements: a surge, "to make the deploy faster". + +## What writ answers + +The questions are in [`deployment.claims`](deployment.claims). The safe plan, +exit 1: + +``` +states: 116 edges: 335 +… +holds upgrades + "the release can finish: every instance on r2, serving, and the schema migrated" +holds never-dark + "production is never dark" +fails can-roll-back + "from every situation, the fleet can still get back to r1, serving" + stuck at: #101 (a.at=r2 b.at=r2 c.at=r2 a.state=healthy b.state=healthy c.state=healthy prod.target=r2 db.at=v2) + witness: 1. target-r2 → #1 prod.target: r1 → r2 + 2. replace-a-with-r2 → #5 a.at: r1 → r2, a.state: healthy → starting + 3. a-passes-health → #12 a.state: starting → healthy + 4. replace-b-with-r2 → #19 b.at: r1 → r2, b.state: healthy → starting + 5. b-passes-health → #43 b.state: starting → healthy + 6. replace-c-with-r2 → #61 c.at: r1 → r2, c.state: healthy → starting + 7. c-passes-health → #85 c.state: starting → healthy + 8. migrate → #101 db.at: v1 → v2 +``` + +The witness is the runbook, done correctly, eight steps. The situation it +ends in is the one everyone wants, a finished release. From there, r1 can +never be reached again. The safe plan exits 1 for this, and that is the +point: the rollout is safe, but the rollback section of the runbook isn't +always true. + +This is not the pair's difference. Both plans fail `can-roll-back` the same +way. It is a property of having an irreversible migration at all. What to do +about it is a decision, not a fix: keep r2 for a soak period before +migrating, so the rollback window is explicit, or make the migration +reversible (keep the column, copy instead of drop). Either way, the runbook +should say when its rollback section stops applying. + +## Which decisions cannot be taken back + +`can-roll-back` names a goal. [`deployment.rules`](deployment.rules) also asks +without one, using `one-way` from ct.rules: which moves leave a situation that +can never be reached again? + +```sh +writ derive deployment.writ deployment.rules irreversible +``` + +``` +irreversible (1 row) + migrate +``` + +Only the migration. Every other step, including the release itself, can be +undone, so `migrate` is the one step to put behind a human decision. If a +rollout step appeared here too, the model would have a latch nobody intended. + +## The surge + +The shortcut, exit 1: + +``` +fails never-dark + "production is never dark" + witness: 1. target-r2 → #1 prod.target: r1 → r2 + 2. replace-a-with-r2 → #5 a.at: r1 → r2, a.state: healthy → starting + 3. replace-b-with-r2 → #12 b.at: r1 → r2, b.state: healthy → starting + 4. replace-c-with-r2 → #29 c.at: r1 → r2, c.state: healthy → starting +``` + +Three replacements with no health check between them, and nothing is +serving. The shortcut still finishes the release (`holds upgrades`), so a +test that only checks the deploy completes passes it. + +## What writ found while this was being written + +The first draft of the safe plan let `migrate` run whenever every instance +was on r2 and healthy. writ's `one-way` table named eleven moves instead of +one, and the situations behind them told the story: + +1. finish the rollout to r2; +2. decide to roll back: `roll-back-target`, allowed because the schema is + still v1; +3. `migrate` runs anyway, because its guard looked at the instances and not + at where the release was heading; +4. the rollback starts r1 on v2, where it never passes a health check, and + the only move left is to go forward again. + +That is a migration job racing a rollback decision, which happens when the +migration is a separate pipeline stage triggered by "all instances on r2". +The fix, in both files, is that `migrate` also requires the target to still +be r2. After the fix, `one-way` names `migrate` alone. + +## Run it + +```sh +writ check deployment.writ --claims deployment.claims # exit 1: the rollback +writ check deployment-shortcut.writ --claims deployment.claims # exit 1: dark, and the rollback +writ derive deployment.writ deployment.rules irreversible +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. +`../db-migration-problems/` has the column-level version of the same idiom: +two releases live at once against one schema. diff --git a/deployment/deployment-shortcut.writ b/deployment/deployment-shortcut.writ new file mode 100644 index 0000000..98a5947 --- /dev/null +++ b/deployment/deployment-shortcut.writ @@ -0,0 +1,115 @@ +; The same deploy with ONE CONDITION REMOVED from each replacement: it no +; longer waits for the rest of the fleet to be serving. A surge, "to make the +; deploy faster". +; +; `writ check` exits 1 on this file, for two reasons: the rollback, as in the +; original, and production going dark. + +(load "stdlib.writ") +(load "deployment.lib.writ") + +(schema deployment + + (type release (r1 r2)) + (type version (v1 v2)) + (type yn (no yes)) + + ; An instance serves traffic only when healthy. A replaced one is starting + ; until its health check passes; a crashed one is down. + (type state-t (starting healthy down)) + (type instance + (arrow at (to release)) + (arrow state (to state-t))) + + ; The release the rollout is heading for. + (type fleet (arrow target (to release))) + + ; The schema, and whether the migration to v2 has run. It drops the column + ; r1 reads, so it has no inverse. + (type database (arrow at (to version))) + + ; ---- the rules ---- + + ; A serving instance can read the schema it runs against: no r1 serving once + ; the schema is v2. (A law has one subject, the instance; the database is + ; bound with `some`.) + (equation no-mismatch + (not (and (is instance.state healthy) + (is instance.at r1) + (some (d database) (is d.at v2)))))) + +(instance start deployment + (instance a (at r1) (state healthy)) + (instance b (at r1) (state healthy)) + (instance c (at r1) (state healthy)) + (fleet prod (target r1)) + (database db (at v1))) + +(use deployment) +(initial start) + +; ---- the release ---- + +(transition target-r2 + (when (is prod.target r1)) + (do (set prod.target r2))) + +; The rollback in the runbook: head back to r1. Only while the schema is still +; one r1 can read. +(transition roll-back-target + (when (and (is prod.target r2) (is db.at v1))) + (do (set prod.target r1))) + +; The migration, once the rollout is finished: every instance on r2 and +; serving, AND the release still heading for r2. One way. +; +; The last condition is the one the first draft of this file lacked, and writ +; found it: finish the rollout, decide to roll back, and the migration — whose +; guard looked only at the instances — runs anyway. The rollback then starts r1 +; against v2, where it never passes a health check. See the README. +(transition migrate + (when (and (is db.at v1) (is prod.target r2) (all-at-healthy r2))) + (do (set db.at v2))) + +; ---- the rollout ---- + +; Replace instance I (running FROM) with the target release TO, as soon as +; it is on the old one. J and K are still passed in; nothing reads them. +(form (roll N I J K FROM TO) + (transition N + (when (and (is prod.target TO) (is I.at FROM))) ; <- the health gate, gone + (do (set I.at TO) (set I.state starting)))) + +(form (pass-health N I) + (transition N + (when (and (is I.state starting) (compatible I))) + (do (set I.state healthy)))) + +; The environment. One instance fails at a time: a crash is only possible +; while the other two are serving. This is the fault model, and the README +; says why it is the honest one for the question. +(form (crash N I J K) + (transition N + (when (and (is I.state healthy) (is J.state healthy) (is K.state healthy))) + (do (set I.state down)))) +(form (restart N I) + (transition N + (when (and (is I.state down) (compatible I))) + (do (set I.state healthy)))) + +(roll replace-a-with-r2 a b c r1 r2) +(roll replace-b-with-r2 b a c r1 r2) +(roll replace-c-with-r2 c a b r1 r2) +(roll replace-a-with-r1 a b c r2 r1) +(roll replace-b-with-r1 b a c r2 r1) +(roll replace-c-with-r1 c a b r2 r1) +(pass-health a-passes-health a) +(pass-health b-passes-health b) +(pass-health c-passes-health c) +(crash a-crashes a b c) +(crash b-crashes b a c) +(crash c-crashes c a b) +(restart a-restarts a) +(restart b-restarts b) +(restart c-restarts c) + diff --git a/deployment/deployment.claims b/deployment/deployment.claims new file mode 100644 index 0000000..889d5ce --- /dev/null +++ b/deployment/deployment.claims @@ -0,0 +1,36 @@ +; The questions, put to both plans. + +(load "deployment.lib.writ") + +(property upgrades + "the release can finish: every instance on r2, serving, and the schema migrated" + (possible (and (all-at-healthy r2) (is db.at v2)))) + +(property never-dark + "production is never dark" + (never none-healthy)) + +(property can-roll-back + "from every situation, the fleet can still get back to r1, serving" + (live (all-at-healthy r1))) + +; ---- ownership ---- +; Every move that changes a release, a state or the schema is on the route of +; no-mismatch; the guards are what keep it (r1 is never started on v2, and +; never passes its health check there). +(accept migrate no-mismatch) +(accept replace-a-with-r2 no-mismatch) +(accept replace-b-with-r2 no-mismatch) +(accept replace-c-with-r2 no-mismatch) +(accept replace-a-with-r1 no-mismatch) +(accept replace-b-with-r1 no-mismatch) +(accept replace-c-with-r1 no-mismatch) +(accept a-passes-health no-mismatch) +(accept b-passes-health no-mismatch) +(accept c-passes-health no-mismatch) +(accept a-crashes no-mismatch) +(accept b-crashes no-mismatch) +(accept c-crashes no-mismatch) +(accept a-restarts no-mismatch) +(accept b-restarts no-mismatch) +(accept c-restarts no-mismatch) diff --git a/deployment/deployment.lib.writ b/deployment/deployment.lib.writ new file mode 100644 index 0000000..05c471c --- /dev/null +++ b/deployment/deployment.lib.writ @@ -0,0 +1,16 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +; Can instance I's release work against the schema as it is now? r1 knows only +; v1. r2 was written for the migration: it reads v1 and v2 alike. +(form (compatible I) + (or (and (is I.at r1) (is db.at v1)) + (is I.at r2))) + +(form none-healthy + (and (not (is a.state healthy)) (not (is b.state healthy)) (not (is c.state healthy)))) + +(form (all-at-healthy R) + (and (is a.at R) (is b.at R) (is c.at R) + (is a.state healthy) (is b.state healthy) (is c.state healthy))) diff --git a/deployment/deployment.rules b/deployment/deployment.rules new file mode 100644 index 0000000..b4fbe93 --- /dev/null +++ b/deployment/deployment.rules @@ -0,0 +1,25 @@ +; The same three questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "deployment.lib.writ") + +(satisfies upgrades (and (all-at-healthy r2) (is db.at v2))) + +(satisfies never-dark none-healthy) + +(satisfies on-r1 (all-at-healthy r1)) +(can-reach can-get-to-r1 on-r1) +(trapped can-roll-back can-get-to-r1) + +; ---- which decisions cannot be taken back ---- +; `one-way` (ct.rules §4) is every edge that leaves its strongly connected +; component: a move after which the situation it left can never be reached +; again. Asked with no goal in mind. Projected onto the move's name, which is +; the column that answers "which step was that". +(relation irreversible (Edge)) +(rule (irreversible E) (one-way E S T)) diff --git a/deployment/deployment.writ b/deployment/deployment.writ new file mode 100644 index 0000000..81d6c12 --- /dev/null +++ b/deployment/deployment.writ @@ -0,0 +1,119 @@ +; A rolling deploy behind a health gate, over a migration that cannot be undone. +; +; Three instances serve production on release r1 against schema v1. The +; rollout replaces them one at a time with r2, and only replaces the next once +; the others are serving. When every instance runs r2, the migration to v2 runs. +; The runbook's rollback heads the fleet back to r1. +; +; `writ check` exits 1 on this file: not for the rollout, which is safe, but +; for the rollback, which is not always there. See the README. + +(load "stdlib.writ") +(load "deployment.lib.writ") + +(schema deployment + + (type release (r1 r2)) + (type version (v1 v2)) + (type yn (no yes)) + + ; An instance serves traffic only when healthy. A replaced one is starting + ; until its health check passes; a crashed one is down. + (type state-t (starting healthy down)) + (type instance + (arrow at (to release)) + (arrow state (to state-t))) + + ; The release the rollout is heading for. + (type fleet (arrow target (to release))) + + ; The schema, and whether the migration to v2 has run. It drops the column + ; r1 reads, so it has no inverse. + (type database (arrow at (to version))) + + ; ---- the rules ---- + + ; A serving instance can read the schema it runs against: no r1 serving once + ; the schema is v2. (A law has one subject, the instance; the database is + ; bound with `some`.) + (equation no-mismatch + (not (and (is instance.state healthy) + (is instance.at r1) + (some (d database) (is d.at v2)))))) + +(instance start deployment + (instance a (at r1) (state healthy)) + (instance b (at r1) (state healthy)) + (instance c (at r1) (state healthy)) + (fleet prod (target r1)) + (database db (at v1))) + +(use deployment) +(initial start) + +; ---- the release ---- + +(transition target-r2 + (when (is prod.target r1)) + (do (set prod.target r2))) + +; The rollback in the runbook: head back to r1. Only while the schema is still +; one r1 can read. +(transition roll-back-target + (when (and (is prod.target r2) (is db.at v1))) + (do (set prod.target r1))) + +; The migration, once the rollout is finished: every instance on r2 and +; serving, AND the release still heading for r2. One way. +; +; The last condition is the one the first draft of this file lacked, and writ +; found it: finish the rollout, decide to roll back, and the migration — whose +; guard looked only at the instances — runs anyway. The rollback then starts r1 +; against v2, where it never passes a health check. See the README. +(transition migrate + (when (and (is db.at v1) (is prod.target r2) (all-at-healthy r2))) + (do (set db.at v2))) + +; ---- the rollout ---- + +; Replace instance I (running FROM) with the target release TO. The health +; gate: the other two instances, J and K, are serving while I is out. +(form (roll N I J K FROM TO) + (transition N + (when (and (is prod.target TO) (is I.at FROM) + (is J.state healthy) (is K.state healthy))) + (do (set I.at TO) (set I.state starting)))) + +(form (pass-health N I) + (transition N + (when (and (is I.state starting) (compatible I))) + (do (set I.state healthy)))) + +; The environment. One instance fails at a time: a crash is only possible +; while the other two are serving. This is the fault model, and the README +; says why it is the honest one for the question. +(form (crash N I J K) + (transition N + (when (and (is I.state healthy) (is J.state healthy) (is K.state healthy))) + (do (set I.state down)))) +(form (restart N I) + (transition N + (when (and (is I.state down) (compatible I))) + (do (set I.state healthy)))) + +(roll replace-a-with-r2 a b c r1 r2) +(roll replace-b-with-r2 b a c r1 r2) +(roll replace-c-with-r2 c a b r1 r2) +(roll replace-a-with-r1 a b c r2 r1) +(roll replace-b-with-r1 b a c r2 r1) +(roll replace-c-with-r1 c a b r2 r1) +(pass-health a-passes-health a) +(pass-health b-passes-health b) +(pass-health c-passes-health c) +(crash a-crashes a b c) +(crash b-crashes b a c) +(crash c-crashes c a b) +(restart a-restarts a) +(restart b-restarts b) +(restart c-restarts c) + diff --git a/docker-compose.yml b/docker-compose.yml index 2734486..8488cdc 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -89,6 +89,12 @@ services: image: writ-problems command: ["agent_guardrails"] + # A rolling deploy: the health gate, and the rollback a migration removes. + deployment: + build: . + image: writ-problems + command: ["deployment"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/modality-cross-check.sh b/modality-cross-check.sh index 35a7e8e..88c96aa 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index ee66488..24f0937 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The eighteen scenarios this script walks by convention, and their 49 + # The nineteen scenarios this script walks by convention, and their 52 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the eighteen fails this line, which is the point of it — + # property to any of the nineteen fails this line, which is the point of it — # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, # 26 -> 31 with two-phase-commit, 31 -> 41 with the three # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and - # 45 -> 49 with agent-guardrails, and this line is where each of those had to - # be said out loud. - has "cross-check: all 49 properties of the eighteen scenarios were considered" \ - "$out" "considered 49 properties: 47 compared, 2 not compared" - # Two of the 49 are not compared, and the count above is the only place that + # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, and this line is + # where each of those had to be said out loud. + has "cross-check: all 52 properties of the nineteen scenarios were considered" \ + "$out" "considered 52 properties: 50 compared, 2 not compared" + # Two of the 52 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +459,9 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval and agent-guardrails one each. + # expense-approval, agent-guardrails and deployment one each. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 9 properties compared" + "never: 10 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -778,9 +778,41 @@ agent_guardrails() { has "agent-guardrails: H. derive lists the tool and the mode" "$dv" "6 web-fetch auto" } +deployment() { + d="$here/deployment" + c="$d/deployment.claims" + echo "== A rolling deploy — and the rollback that is not always there ==" + echo " Q: is production ever dark, and can the fleet always roll back?" + out=$("$WRIT" check "$d/deployment.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + # Exit 1 on the SAFE plan, and that is the finding: the rollout is fine, the + # rollback is a promise one lawful move breaks. + exit_is "deployment: even the gated rollout reports a finding" "$st" 1 + has "deployment: A. the release can finish" "$out" "holds upgrades" + has "deployment: B. production is never dark" "$out" "holds never-dark" + has "deployment: C. but rollback is not always possible" "$out" "fails can-roll-back" + has "deployment: stuck once the schema is v2" "$out" "prod.target=r2 db.at=v2)" + has "deployment: and the last step there is the migration" "$out" "8. migrate" + lacks "deployment: no law is broken on the way" "$out" "violated in" + + sc=$("$WRIT" check "$d/deployment-shortcut.writ" --claims "$c" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "deployment: the ungated rollout is refused" "$sst" 1 + has "deployment: D. without the health gate, production goes dark" "$sc" "fails never-dark" + near "deployment: three replacements, no health check between" "$sc" "fails never-dark" "4. replace-c-with-r2" + + # Asked with no goal in mind: which moves can never be taken back? The + # migration, and nothing else — a rollout move here would be a latch. + dv=$("$WRIT" derive "$d/deployment.writ" "$d/deployment.rules" irreversible 2>&1) + has "deployment: E. exactly one decision cannot be taken back" "$dv" "irreversible (1 row)" + has "deployment: the migration" "$dv" " migrate" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From c50a1efa9c75382a95791f87d81b9997fc8ce396 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:30:53 +0300 Subject: [PATCH 5/7] payments: the reply that never comes, and the idempotency key One order: authorize, capture over a wire that loses replies, settle, ship, refund, cancel. Without a key, a lost reply and a retry charge twice in six steps; derive double-charged shows the order looking normal in every stage. The shortcut also charges for a cancelled order: the void overtakes the capture, finds nothing, and the capture lands after it. Writing it, writ failed the first draft of the SAFE file, key and all: cancel was allowed whenever the shop had not captured, so a capture still on the wire landed after the cancellation. cancel now voids at the processor, under the same key. Cross-check 52 -> 56 properties (54 compared); 314 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + docker-compose.yml | 6 ++ modality-cross-check.sh | 2 +- payments/README.md | 170 ++++++++++++++++++++++++++++++++ payments/payments-shortcut.writ | 132 +++++++++++++++++++++++++ payments/payments.claims | 29 ++++++ payments/payments.lib.writ | 17 ++++ payments/payments.rules | 32 ++++++ payments/payments.writ | 133 +++++++++++++++++++++++++ run-tests.sh | 50 ++++++++-- 10 files changed, 561 insertions(+), 11 deletions(-) create mode 100644 payments/README.md create mode 100644 payments/payments-shortcut.writ create mode 100644 payments/payments.claims create mode 100644 payments/payments.lib.writ create mode 100644 payments/payments.rules create mode 100644 payments/payments.writ diff --git a/README.md b/README.md index aabf38c..c964a0e 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`expense-approval/`](expense-approval/) | Can a large expense be paid without two independent approvals? | Yes, when one person holds both roles: "two signatures" counted boxes, not people. | | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. | | [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. | +| [`payments/`](payments/) | Can a lost reply and a retry charge a customer twice? | Without an idempotency key, in six steps, each correct where it stood. The key also stops a late capture beating a cancellation. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/docker-compose.yml b/docker-compose.yml index 8488cdc..c5c14eb 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -95,6 +95,12 @@ services: image: writ-problems command: ["deployment"] + # Payments: a lost reply, a retry, and the idempotency key. + payments: + build: . + image: writ-problems + command: ["payments"] + # 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 88c96aa..ce0471d 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments" considered=0 compared=0 diff --git a/payments/README.md b/payments/README.md new file mode 100644 index 0000000..3d6f671 --- /dev/null +++ b/payments/README.md @@ -0,0 +1,170 @@ +# Payments: the reply that never comes + +A shop takes payment in two steps: **authorize** the card, which reserves the +money, then **capture**, which takes it. The capture is a request to a payment +processor, and the processor's reply can be lost: a timeout, a dropped +connection, a load balancer restart. The shop then does not know whether the +money was taken, so it does what every integration does. It waits, and it +asks again. + +If the first request did land, the retry is a second capture. The customer is +charged twice, and nothing on the shop's side looks wrong: it received one +reply, recorded one capture, and shipped one order. The usual cure is an +**idempotency key**: every request carries a key, and the processor answers a +repeated key with the original reply instead of acting again. + +## The model + +[`payments.writ`](payments.writ) follows one order: + +- the shop's view, `o`: its `stage` (`placed`, `authorized`, `captured`, + `settled`, `refunded`, `cancelled`) and whether it has shipped; +- the wire, `net`: a capture `request` on its way out, a `reply` on its way + back, and a `void` (more below); +- the processor's view, `proc`: how many times it has taken the money + (`none`, `one`, `two`), whether it has refunded, and the keys it has + already honoured (`seen`). + +The processor counts captures, not money. The questions are about how many +times the money was taken, so a three-member type is the honest size, and +`two` is the bug. A refund question that needed partial amounts would add a +band (`none`, `partial`, `full`), still not a number. + +The shop's moves are `authorize`, `send-capture`, `receive-reply`, `settle`, +`ship`, `refund` and `cancel`. `send-capture` is the first attempt and every +retry: whenever the shop is waiting on a capture, with nothing out and +nothing back, it sends one. The network's move is `lose-reply`. + +The processor's moves are where the two files differ. With the key +(`payments.writ`), `capture` records `k1`, and a request carrying a seen key +gets `replay-reply`: the original answer, no second capture. +[`payments-shortcut.writ`](payments-shortcut.writ) sends no key, so the +processor has nothing to record or check, and `capture-again` takes the money +a second time. + +## What writ answers + +The questions are in [`payments.claims`](payments.claims). With the key, +exit 0: + +``` +holds settles + "a payment can settle" +holds never-double + "the customer is never charged twice" +holds never-charged-for-nothing + "once the wire is quiet, a cancelled order never leaves the customer charged" +holds always-terminal + "from everywhere, the order can still reach an end" +certified: every answer re-derived from the model (writ-cert) +``` + +Without it, exit 1: + +``` +fails never-double + "the customer is never charged twice" + witness: 1. authorize → #1 o.stage: placed → authorized + 2. send-capture → #3 net.request: no → yes + 3. capture → #5 net.request: yes → no, net.reply: no → yes, proc.captures: none → one + 4. lose-reply → #8 net.reply: yes → no + 5. send-capture → #13 net.request: no → yes + 6. capture-again → #16 net.request: yes → no, net.reply: no → yes, proc.captures: one → two +``` + +Read it as the support ticket it becomes. The shop asked for the money, the +processor took it, the answer got lost, the shop asked again, and the +processor took it again. Every step is correct from where it stands. No +single component misbehaved. + +[`payments.rules`](payments.rules) shows where those double charges end up, +as the shop sees the order: + +```sh +writ derive payments-shortcut.writ payments.rules double-charged +``` + +``` +double-charged (13 rows) + 22 authorized no + … + 29 settled no + 30 captured yes + 31 refunded no + … + 34 settled yes + 35 cancelled no +``` + +Settled and shipped, refunded (one capture given back, one kept), cancelled: +the double charge appears in every stage the shop has, and nothing marks it. +It reaches support as a complaint, not as an alert. + +## The cancellation that loses the race + +The shortcut fails a second question: + +``` +fails never-charged-for-nothing + "once the wire is quiet, a cancelled order never leaves the customer charged" + witness: 1. authorize → #1 o.stage: placed → authorized + 2. send-capture → #3 net.request: no → yes + 3. cancel → #5 o.stage: authorized → cancelled, net.void: no → yes + 4. void-uncaptured → #8 net.void: yes → no + 5. capture → #13 net.request: yes → no, net.reply: no → yes, proc.captures: none → one + 6. discard-late-reply → #19 net.reply: yes → no +``` + +The shop cancels while its capture request is still on the wire, and sends a +void. The void arrives first, finds nothing to refund, and is done. Then the +capture lands. With a key, the void marks `k1` as used, so the late capture is +answered with a replay and takes nothing. Without a key there is nothing to +mark. The key is not only a retry mechanism: it is what lets a cancellation +refer to a request that has not arrived yet. + +"Once the wire is quiet" is part of the question on purpose. While a request +or a void is still in flight, the charge is unresolved, not wrong. The +property asks about the situations where nothing more will arrive. + +## What writ found while this was being written + +The first draft of the safe file had no void. `cancel` was allowed whenever +the shop had not captured, because from its own records no money had moved. +writ failed it, key and all (change columns trimmed): + +``` +fails never-charged-for-nothing + witness: 1. authorize + 2. send-capture + 3. cancel + 4. capture +``` + +The shop's record says "not captured" in two different situations: nothing +was sent, or something was sent and nothing came back. Only the first is safe +to cancel on. The fix, in both files, is that cancelling also voids at the +processor. With the key the void is enough; without it, as above, it is not. + +## What to take away + +At-least-once delivery plus a non-idempotent operation means sometimes +twice, and testing rarely shows it, because the lost reply is rare and the +double charge looks like a normal order. The question that catches it, +"never two captures", is about the processor's state, which the shop never +sees. That is why it belongs in a model. + +The shortcut still settles and still reaches an end. Unlike the migration +problems, it is not even faster. It skips no wait. It just leaves out one +field on the request. + +## Run it + +```sh +writ check payments.writ --claims payments.claims # exit 0 +writ check payments-shortcut.writ --claims payments.claims # exit 1 +writ compare payments.writ payments-shortcut.writ # exit 1: both guarantees LOST +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. +`../two-phase-commit/` has the same lossy-wire idiom, applied to agreement +rather than money. diff --git a/payments/payments-shortcut.writ b/payments/payments-shortcut.writ new file mode 100644 index 0000000..194f63a --- /dev/null +++ b/payments/payments-shortcut.writ @@ -0,0 +1,132 @@ +; The same lifecycle, with NO IDEMPOTENCY KEY: the retry is a brand new +; request as far as the processor can tell. +; +; Every step is correct from where it stands. The shop did not get a reply, so +; it asked again. The processor got a request, so it captured. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "payments.lib.writ") + +(schema payments + + (type yn (no yes)) + + ; The shop's view of the order. + (type stage-t (placed authorized captured settled refunded cancelled)) + (type order + (arrow stage (to stage-t)) + (arrow shipment (to yn))) + + ; The wire: a capture request on its way to the processor, and the + ; processor's reply on its way back. Either may be in flight; the reply can + ; be lost. + (type wire + (arrow request (to yn)) + (arrow reply (to yn)) + (arrow void (to yn))) + + ; The processor's view. How many times it has taken the money, not how much: + ; none, one, or two, and two is the bug. Whether it has refunded. And the + ; idempotency keys it has already honoured. + (type count (none one two)) + (type key-t (k1)) + (type processor + (arrow captures (to count)) + (arrow refunded (to yn)) + (maybe seen key-t)) + + ; ---- the rules ---- + + ; The customer is charged at most once. + (equation one-capture (not (is processor.captures two))) + + ; A cancelled order never ships. + (equation cancelled-never-ships + (not (and (is order.stage cancelled) (is order.shipment yes))))) + +(instance start payments + (order o (stage placed) (shipment no)) + (wire net (request no) (reply no) (void no)) + (processor proc (captures none) (refunded no) (seen vacant))) + +(use payments) +(initial start) + +; ---- the shop ---- + +(transition authorize + (when (is o.stage placed)) + (do (set o.stage authorized))) + +; Ask the processor to capture. The same move is the first attempt and every +; retry: whenever the shop is waiting on a capture and has no request out and +; no reply in, it sends one. That is what a timeout-and-retry loop does. +(transition send-capture + (when (and (is o.stage authorized) (is net.request no) (is net.reply no))) + (do (set net.request yes))) + +(transition receive-reply + (when (and (is net.reply yes) (is o.stage authorized))) + (do (set net.reply no) (set o.stage captured))) + +; A reply for an order the shop has already cancelled is dropped. +(transition discard-late-reply + (when (and (is net.reply yes) (is o.stage cancelled))) + (do (set net.reply no))) + +(transition settle + (when (is o.stage captured)) + (do (set o.stage settled))) + +(transition ship + (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no))) + (do (set o.shipment yes))) + +(transition refund + (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no))) + (do (set o.stage refunded) (set proc.refunded yes))) + +; Cancel an order the shop has not captured. From its own view no money +; moved, but a capture request may be out, or may have landed and lost its +; reply. So cancelling also tells the processor to void the payment. +; +; The first draft of this file cancelled without the void, and writ found it: +; authorize, send the capture, cancel, and the capture lands after the +; cancellation. See the README. +(transition cancel + (when (and (or (is o.stage placed) (is o.stage authorized)) (is o.shipment no))) + (do (set o.stage cancelled) (set net.void yes))) + +; ---- the network ---- + +; The processor's reply never arrives: a timeout, a dropped connection, a +; load balancer restart. The capture itself happened. +(transition lose-reply + (when (is net.reply yes)) + (do (set net.reply no))) + +; ---- the processor ---- + +; No idempotency key: the request carries nothing the processor could +; recognise, so it records nothing and checks nothing. Every request that +; arrives is a capture. +(transition capture + (when (and (is net.request yes) (is proc.captures none))) ; <- key check, gone + (do (set net.request no) (set proc.captures one) (set net.reply yes))) ; <- key record, gone +(transition capture-again + (when (and (is net.request yes) (is proc.captures one))) ; <- key check, gone + (do (set net.request no) (set proc.captures two) (set net.reply yes))) +; A void: refund a capture already made. With no key, there is nothing to +; mark, so a capture request still on the wire is honoured when it lands. +(transition void-captured + (when (and (is net.void yes) (is proc.captures one))) + (do (set net.void no) (set proc.refunded yes))) ; <- key record, gone +(transition void-uncaptured + (when (and (is net.void yes) (is proc.captures none))) + (do (set net.void no))) ; <- key record, gone +(transition replay-reply + (when (and (is net.request yes) (is proc.seen k1))) + (do (set net.request no) (set net.reply yes))) + diff --git a/payments/payments.claims b/payments/payments.claims new file mode 100644 index 0000000..3b5389f --- /dev/null +++ b/payments/payments.claims @@ -0,0 +1,29 @@ +; The questions, put to both integrations. + +(load "payments.lib.writ") + +(property settles + "a payment can settle" + (possible (is o.stage settled))) + +(property never-double + "the customer is never charged twice" + (never (is proc.captures two))) + +(property never-charged-for-nothing + "once the wire is quiet, a cancelled order never leaves the customer charged" + (never (and charged-for-nothing quiet))) + +(property always-terminal + "from everywhere, the order can still reach an end" + (live terminal)) + +; ---- ownership ---- +(accept capture one-capture) +(accept capture-again one-capture) +(accept authorize cancelled-never-ships) +(accept receive-reply cancelled-never-ships) +(accept settle cancelled-never-ships) +(accept ship cancelled-never-ships) +(accept refund cancelled-never-ships) +(accept cancel cancelled-never-ships) diff --git a/payments/payments.lib.writ b/payments/payments.lib.writ new file mode 100644 index 0000000..c1e520f --- /dev/null +++ b/payments/payments.lib.writ @@ -0,0 +1,17 @@ +; 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") + +; The order has reached an end: settled, refunded or cancelled. +(form terminal + (or (is o.stage settled) (is o.stage refunded) (is o.stage cancelled))) + +; The customer has paid for an order they will not get: it was cancelled, and +; the processor holds a capture nobody refunded. +(form charged-for-nothing + (and (is o.stage cancelled) (not (is proc.captures none)) (is proc.refunded no))) + +; Nothing on the wire: no request, reply or void still to land. Until then the +; charge is unresolved, not wrong. +(form quiet + (and (is net.request no) (is net.reply no) (is net.void no))) diff --git a/payments/payments.rules b/payments/payments.rules new file mode 100644 index 0000000..19d17ec --- /dev/null +++ b/payments/payments.rules @@ -0,0 +1,32 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "payments.lib.writ") + +(satisfies settles (is o.stage settled)) + +(satisfies never-double (is proc.captures two)) + +(satisfies never-charged-for-nothing (and charged-for-nothing quiet)) + +(satisfies ended terminal) +(can-reach can-end ended) +(trapped always-terminal can-end) + +; ---- the explanation ---- +; Where the double charge leaves the order, as the shop sees it: its stage, +; and whether it shipped. The rows cover every stage there is: settled and +; shipped, refunded (one capture given back, one kept), cancelled. Nothing on +; the shop's side marks them, which is why this reaches support as a customer +; complaint and not as an alert. +(relation double-charged (Situation stage-t yn)) +(rule (double-charged S G Y) + (situation S) + (holds S (is proc.captures two)) + (holds S (is o.stage G)) + (holds S (is o.shipment Y))) diff --git a/payments/payments.writ b/payments/payments.writ new file mode 100644 index 0000000..feb95ce --- /dev/null +++ b/payments/payments.writ @@ -0,0 +1,133 @@ +; A payment's lifecycle, over a network that loses replies. +; +; The shop authorizes the customer's card, asks the processor to capture the +; money, and settles. It can ship, refund, or cancel. The processor's reply can +; be lost; the shop then retries, as every payment integration does. The +; retry carries an idempotency key, so the processor recognises it. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "payments.lib.writ") + +(schema payments + + (type yn (no yes)) + + ; The shop's view of the order. + (type stage-t (placed authorized captured settled refunded cancelled)) + (type order + (arrow stage (to stage-t)) + (arrow shipment (to yn))) + + ; The wire: a capture request on its way to the processor, and the + ; processor's reply on its way back. Either may be in flight; the reply can + ; be lost. + (type wire + (arrow request (to yn)) + (arrow reply (to yn)) + (arrow void (to yn))) + + ; The processor's view. How many times it has taken the money, not how much: + ; none, one, or two, and two is the bug. Whether it has refunded. And the + ; idempotency keys it has already honoured. + (type count (none one two)) + (type key-t (k1)) + (type processor + (arrow captures (to count)) + (arrow refunded (to yn)) + (maybe seen key-t)) + + ; ---- the rules ---- + + ; The customer is charged at most once. + (equation one-capture (not (is processor.captures two))) + + ; A cancelled order never ships. + (equation cancelled-never-ships + (not (and (is order.stage cancelled) (is order.shipment yes))))) + +(instance start payments + (order o (stage placed) (shipment no)) + (wire net (request no) (reply no) (void no)) + (processor proc (captures none) (refunded no) (seen vacant))) + +(use payments) +(initial start) + +; ---- the shop ---- + +(transition authorize + (when (is o.stage placed)) + (do (set o.stage authorized))) + +; Ask the processor to capture. The same move is the first attempt and every +; retry: whenever the shop is waiting on a capture and has no request out and +; no reply in, it sends one. That is what a timeout-and-retry loop does. +(transition send-capture + (when (and (is o.stage authorized) (is net.request no) (is net.reply no))) + (do (set net.request yes))) + +(transition receive-reply + (when (and (is net.reply yes) (is o.stage authorized))) + (do (set net.reply no) (set o.stage captured))) + +; A reply for an order the shop has already cancelled is dropped. +(transition discard-late-reply + (when (and (is net.reply yes) (is o.stage cancelled))) + (do (set net.reply no))) + +(transition settle + (when (is o.stage captured)) + (do (set o.stage settled))) + +(transition ship + (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no))) + (do (set o.shipment yes))) + +(transition refund + (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no))) + (do (set o.stage refunded) (set proc.refunded yes))) + +; Cancel an order the shop has not captured. From its own view no money +; moved, but a capture request may be out, or may have landed and lost its +; reply. So cancelling also tells the processor to void the payment. +; +; The first draft of this file cancelled without the void, and writ found it: +; authorize, send the capture, cancel, and the capture lands after the +; cancellation. See the README. +(transition cancel + (when (and (or (is o.stage placed) (is o.stage authorized)) (is o.shipment no))) + (do (set o.stage cancelled) (set net.void yes))) + +; ---- the network ---- + +; The processor's reply never arrives: a timeout, a dropped connection, a +; load balancer restart. The capture itself happened. +(transition lose-reply + (when (is net.reply yes)) + (do (set net.reply no))) + +; ---- the processor ---- + +; Every request carries the idempotency key k1. A key the processor has not +; seen is a capture; a key it has seen gets the original reply again, and no +; second capture. +(transition capture + (when (and (is net.request yes) (is proc.captures none) (not (is proc.seen k1)))) + (do (set net.request no) (set proc.captures one) (set proc.seen k1) (set net.reply yes))) +(transition capture-again + (when (and (is net.request yes) (is proc.captures one) (not (is proc.seen k1)))) + (do (set net.request no) (set proc.captures two) (set net.reply yes))) +; A void under the same key: refund a capture already made, and mark the key +; used, so a capture request still on the wire is replayed, not honoured. +(transition void-captured + (when (and (is net.void yes) (is proc.captures one))) + (do (set net.void no) (set proc.refunded yes) (set proc.seen k1))) +(transition void-uncaptured + (when (and (is net.void yes) (is proc.captures none))) + (do (set net.void no) (set proc.seen k1))) +(transition replay-reply + (when (and (is net.request yes) (is proc.seen k1))) + (do (set net.request no) (set net.reply yes))) + diff --git a/run-tests.sh b/run-tests.sh index 24f0937..f90d174 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The nineteen scenarios this script walks by convention, and their 52 + # The twenty scenarios this script walks by convention, and their 56 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the nineteen fails this line, which is the point of it — + # property to any of the twenty 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, and this line is - # where each of those had to be said out loud. - has "cross-check: all 52 properties of the nineteen scenarios were considered" \ - "$out" "considered 52 properties: 50 compared, 2 not compared" - # Two of the 52 are not compared, and the count above is the only place that + # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, 52 -> 56 with + # payments, and this line is where each of those had to be said out loud. + has "cross-check: all 56 properties of the twenty scenarios were considered" \ + "$out" "considered 56 properties: 54 compared, 2 not compared" + # Two of the 56 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +459,9 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval, agent-guardrails and deployment one each. + # expense-approval, agent-guardrails and deployment one each, payments two. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 10 properties compared" + "never: 12 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -810,9 +810,39 @@ deployment() { has "deployment: the migration" "$dv" " migrate" } +payments() { + d="$here/payments" + c="$d/payments.claims" + echo "== Payments — the reply that never comes, and the retry ==" + echo " Q: can a lost reply and a retry charge the customer twice?" + out=$("$WRIT" check "$d/payments.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "payments: with an idempotency key, the integration is clean" "$st" 0 + has "payments: A. a payment can settle" "$out" "holds settles" + has "payments: B. never charged twice" "$out" "holds never-double" + has "payments: C. a cancelled order is never left charged" "$out" "holds never-charged-for-nothing" + has "payments: and every order can still reach an end" "$out" "holds always-terminal" + lacks "payments: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/payments-shortcut.writ" --claims "$c" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "payments: without the key, the integration is refused" "$sst" 1 + has "payments: D. a lost reply and a retry charge twice" "$sc" \ + "violated in 13 reachable situations witness: 1. authorize 2. send-capture 3. capture 4. lose-reply 5. send-capture 6. capture-again" + has "payments: E. and a void that overtakes the capture charges for a cancelled order" "$sc" "fails never-charged-for-nothing" + near "payments: the void lands first, with nothing to refund" "$sc" "fails never-charged-for-nothing" "4. void-uncaptured" + near "payments: then the capture" "$sc" "fails never-charged-for-nothing" "5. capture" + has "payments: F. yet it still settles" "$sc" "holds settles" + + dv=$("$WRIT" derive "$d/payments-shortcut.writ" "$d/payments.rules" double-charged 2>&1) + has "payments: G. double charges hide in orders that settled and shipped" "$dv" "settled yes" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From 468a25b8627da68c80a432bb4c448c7a9e8df712 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:33:27 +0300 Subject: [PATCH 6/7] config-space: the flag matrix exhausted, and the order that breaks it Four flags and two modes, 64 combinations; the guarded operations reach exactly the 21 the product's rules allow. The shortcut's disable-sso checks authentication but not the shard latch: enable-legacy-auth, shard, disable-sso reaches a forbidden state, and only in that order. --fiber cfg.region shows the EU deployment is safe from it by accident. v2 adds a billing flag whose enable turns tenancy on: compare reports never-unsafe LOST in one move, and check reports the new operation unadmitted. final-phase names exactly the sharded configurations. Cross-check 56 -> 60 properties (58 compared); 329 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + config-space/README.md | 170 ++++++++++++++++++++++++ config-space/config-space-shortcut.writ | 95 +++++++++++++ config-space/config-space-v2.writ | 106 +++++++++++++++ config-space/config-space.claims | 35 +++++ config-space/config-space.lib.writ | 10 ++ config-space/config-space.rules | 29 ++++ config-space/config-space.writ | 94 +++++++++++++ docker-compose.yml | 6 + modality-cross-check.sh | 2 +- run-tests.sh | 63 +++++++-- 11 files changed, 601 insertions(+), 10 deletions(-) create mode 100644 config-space/README.md create mode 100644 config-space/config-space-shortcut.writ create mode 100644 config-space/config-space-v2.writ create mode 100644 config-space/config-space.claims create mode 100644 config-space/config-space.lib.writ create mode 100644 config-space/config-space.rules create mode 100644 config-space/config-space.writ diff --git a/README.md b/README.md index c964a0e..c62ee6e 100644 --- a/README.md +++ b/README.md @@ -57,6 +57,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. | | [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. | | [`payments/`](payments/) | Can a lost reply and a retry charge a customer twice? | Without an idempotency key, in six steps, each correct where it stood. The key also stops a late capture beating a cancellation. | +| [`config-space/`](config-space/) | Can the admin operations reach a flag combination the product forbids? | All 64 combinations walked: only if steps are done in one order. A release adding a flag loses the guarantee in one move. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/config-space/README.md b/config-space/README.md new file mode 100644 index 0000000..b6a143f --- /dev/null +++ b/config-space/README.md @@ -0,0 +1,170 @@ +# The configuration space: every combination, not a sample + +A product deployment has feature flags and modes: SSO on or off, legacy +password login, multi-tenancy, an audit log, a region, a database that is +single or sharded. Some combinations are forbidden by the product's own +rules, and the admin operations that change the configuration are supposed to +refuse the steps that would reach them. + +The usual check is a test matrix that samples combinations. Here there are +four flags and two two-valued modes: 2⁶ = 64 combinations. That is the whole +space, and writ walks all of it. The interesting finding is not a forbidden +combination a sample missed. It is one reached only by doing allowed steps in +a particular **order**, which no test of single configurations or single +steps can produce. + +## The model + +[`config-space.writ`](config-space.writ) has one `config` entity, `cfg`, and +four rules as laws: + +| rule | in words | +| --- | --- | +| `audit-when-multi-tenant` | tenants' actions are audited | +| `no-legacy-in-eu` | password login is not offered in the EU deployment | +| `some-auth` | somebody can log in: SSO or legacy auth is on | +| `sharded-needs-sso` | the sharded database routes on the SSO tenant id | + +Each admin operation (`enable-sso`, `disable-sso`, `enable-legacy-auth`, …, +`move-to-eu`, `move-to-us`, `shard`) checks in its `when` the rules it could +break. Writing those guards is the work: each is a rule read as a +precondition. `shard` is one-way, because sharding migrates the data and +nothing undoes it. + +[`config-space-shortcut.writ`](config-space-shortcut.writ) leaves out one +condition. `disable-sso` checks that somebody can still log in, but not that +the database is unsharded. The check that remains is the obvious one: SSO is +an authentication flag, and its guard checks authentication. The one that is +gone belongs to another subsystem, and to a mode that changes once in the +product's life. + +## What writ answers + +The questions are in [`config-space.claims`](config-space.claims). The guarded +operations, exit 0: + +``` +states: 21 edges: 67 +… +holds fully-featured + "a safe configuration with tenants, SSO and a sharded database exists" +holds never-unsafe + "no configuration the product forbids is ever reached" +holds recoverable +holds can-leave-eu +``` + +21 of the 64 combinations are reachable from the starting configuration, and +the four rules allow exactly 21. So the guarded operations reach every allowed +configuration and nothing else. The guards forbid nothing the rules allow, +and admit nothing they forbid. + +The shortcut, exit 1: + +``` +equation sharded-needs-sso + … + violated in 3 reachable situations witness: 1. enable-legacy-auth 2. shard 3. disable-sso → #15 +… +fails never-unsafe + witness: 1. enable-legacy-auth → #1 cfg.legacy-auth: no → yes + 2. shard → #7 cfg.db-mode: single → sharded + 3. disable-sso → #15 cfg.sso: yes → no +holds recoverable +``` + +Each step is allowed, and the order is the finding. Turn SSO off first and +`shard` refuses, because it checks SSO. Shard first and `disable-sso` lets you +through, because it does not check the database. A test of `disable-sso` on a +single-database configuration passes. A test of `shard` without SSO is +refused. The failing path exists only in this sequence. + +`recoverable` still holds: `enable-sso` repairs it. So the shortcut never +traps anyone, which is why the bug would ship. The broken configuration is a +state production can sit in until someone notices the router failing. + +### Per region + +FR-10's fibers answer the same question once per value of a cell: + +```sh +writ check config-space-shortcut.writ --claims config-space.claims --fiber cfg.region +``` + +``` +fails never-unsafe + … + fiber cfg.region=us FAILS witness: 1. enable-legacy-auth 2. shard 3. disable-sso → #15 + fiber cfg.region=eu holds +``` + +Only the US deployment can reach it. The EU forbids legacy auth, and turning +it on is the first step of the route. So the EU deployment is safe from this +bug because of a rule about a different thing. That protection is +accidental, and the fiber line shows it. + +## A release that adds a flag + +[`config-space-v2.writ`](config-space-v2.writ) is the guarded model plus one +flag, `new-billing`. The new billing system bills per tenant, so its enable +operation also turns multi-tenancy on. It was reviewed as a billing change. + +```sh +writ compare config-space.writ config-space-v2.writ # exit 1 +``` + +``` +equations: audit-when-multi-tenant preserved + no-legacy-in-eu preserved + some-auth preserved + sharded-needs-sso preserved +properties: fully-featured preserved + never-unsafe LOST witness: 1. enable-new-billing + recoverable preserved + can-leave-eu preserved +``` + +One move: multi-tenancy on, audit log off, the first rule broken. A release +that adds a flag adds operations, and `compare` checks the operations, not +the flag. `writ check` on v2 says the same from the other side: + +``` +unadmitted enable-new-billing may break audit-when-multi-tenant +``` + +The claims file lists every operation the team has agreed can touch each +rule. A new one that can is reported until someone either guards it or signs +it off. + +## What the latch costs + +[`config-space.rules`](config-space.rules) asks, with no goal in mind, which +configurations are in the last phase, the ones that can never get back to an +earlier one: + +```sh +writ derive config-space.writ config-space.rules final-db +``` + +All nine rows say `sharded`. Every configuration on a single database can be +left and returned to, and every sharded one can only go to other sharded ones. +That is what one irreversible operation does to a configuration space: it +divides it in two, and a deployment crosses once. + +## What is not modelled + +Values, only members: a flag is on or off, a region is one of two. A flag +whose default differs by region would be a fixed arrow on the region, not a +cell. And every operation is available at any time to whoever administers the +deployment. Who may run which operation is the entitlement problems' subject +(`../entitlement-problems/`), and the two compose. + +## Run it + +```sh +writ check config-space.writ --claims config-space.claims # exit 0 +writ check config-space-shortcut.writ --claims config-space.claims --fiber cfg.region # exit 1 +writ compare config-space.writ config-space-v2.writ # exit 1 +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. diff --git a/config-space/config-space-shortcut.writ b/config-space/config-space-shortcut.writ new file mode 100644 index 0000000..742e4db --- /dev/null +++ b/config-space/config-space-shortcut.writ @@ -0,0 +1,95 @@ +; The same operations, with ONE CONDITION MISSING from one of them: turning +; SSO off checks that somebody can still log in, and not that the database is +; unsharded. +; +; The check that is there is the obvious one: SSO is an authentication flag, +; and its guard checks authentication. The one that is gone is about a +; different subsystem, the database, and a mode that only changes once. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) +) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off: check that somebody can still log in. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes))) ; <- db-mode single, gone + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) diff --git a/config-space/config-space-v2.writ b/config-space/config-space-v2.writ new file mode 100644 index 0000000..2172346 --- /dev/null +++ b/config-space/config-space-v2.writ @@ -0,0 +1,106 @@ +; Version 2: the guarded operations, plus ONE NEW FLAG. +; +; `new-billing` switches to a billing system that bills per tenant, so its +; enable operation also turns multi-tenancy on. Nothing about the old +; operations changes. +; +; `writ compare config-space.writ config-space-v2.writ` exits 1. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) + ; New in v2. + (arrow new-billing (to yn))) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single) (new-billing no))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off breaks two rules if done carelessly: nobody can log in, or +; the sharded database loses its routing key. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes) (is cfg.db-mode single))) + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) + +; ---- new in v2 ---- + +; The new billing system bills per tenant, so turning it on turns tenancy on. +; It was reviewed as a billing change. +(transition enable-new-billing + (when (is cfg.new-billing no)) + (do (set cfg.new-billing yes) (set cfg.multi-tenant yes))) +(transition disable-new-billing + (when (is cfg.new-billing yes)) + (do (set cfg.new-billing no))) diff --git a/config-space/config-space.claims b/config-space/config-space.claims new file mode 100644 index 0000000..48ac6f6 --- /dev/null +++ b/config-space/config-space.claims @@ -0,0 +1,35 @@ +; The questions, put to every version. + +(load "config-space.lib.writ") + +(property fully-featured + "a safe configuration with tenants, SSO and a sharded database exists" + (possible (and (is cfg.multi-tenant yes) (is cfg.sso yes) (is cfg.db-mode sharded) safe))) + +(property never-unsafe + "no configuration the product forbids is ever reached" + (never (not safe))) + +(property recoverable + "from every configuration, a safe one is still reachable" + (live safe)) + +(property can-leave-eu + "from every configuration, the deployment can still be moved to the US" + (live (is cfg.region us))) + +; ---- ownership ---- +; Every operation that writes a cell a rule reads. The guards are what keep +; the rules; a release that adds an operation adds a line here, or writ reports +; it as unadmitted. +(accept enable-multi-tenant audit-when-multi-tenant) +(accept disable-multi-tenant audit-when-multi-tenant) +(accept enable-audit-log audit-when-multi-tenant) +(accept disable-audit-log audit-when-multi-tenant) +(accept enable-legacy-auth no-legacy-in-eu some-auth) +(accept disable-legacy-auth no-legacy-in-eu some-auth) +(accept move-to-eu no-legacy-in-eu) +(accept move-to-us no-legacy-in-eu) +(accept enable-sso some-auth sharded-needs-sso) +(accept disable-sso some-auth sharded-needs-sso) +(accept shard sharded-needs-sso) diff --git a/config-space/config-space.lib.writ b/config-space/config-space.lib.writ new file mode 100644 index 0000000..cd8275b --- /dev/null +++ b/config-space/config-space.lib.writ @@ -0,0 +1,10 @@ +; 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") + +; The product's four rules, as one test: a configuration none of them forbids. +(form safe + (and (not (and (is cfg.multi-tenant yes) (is cfg.audit-log no))) + (not (and (is cfg.legacy-auth yes) (is cfg.region eu))) + (not (and (is cfg.sso no) (is cfg.legacy-auth no))) + (not (and (is cfg.db-mode sharded) (is cfg.sso no))))) diff --git a/config-space/config-space.rules b/config-space/config-space.rules new file mode 100644 index 0000000..c65677e --- /dev/null +++ b/config-space/config-space.rules @@ -0,0 +1,29 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "config-space.lib.writ") + +(satisfies fully-featured + (and (is cfg.multi-tenant yes) (is cfg.sso yes) (is cfg.db-mode sharded) safe)) + +(satisfies never-unsafe (not safe)) + +(satisfies is-safe safe) +(can-reach can-be-safe is-safe) +(trapped recoverable can-be-safe) + +(satisfies in-us (is cfg.region us)) +(can-reach can-get-to-us in-us) +(trapped can-leave-eu can-get-to-us) + +; ---- what the latch costs ---- +; `final-phase` (ct.rules §3): the configurations in the last phase, the ones +; that can never get back to an earlier one. Asked with no goal in mind. +; Projected onto the database mode, which is the cell that says why. +(relation final-db (Situation db-t)) +(rule (final-db S D) (final-phase S) (holds S (is cfg.db-mode D))) diff --git a/config-space/config-space.writ b/config-space/config-space.writ new file mode 100644 index 0000000..b269b2d --- /dev/null +++ b/config-space/config-space.writ @@ -0,0 +1,94 @@ +; A product's runtime configuration, and the admin operations that change it. +; +; Four feature flags, a region and a database mode: 64 combinations. Four of +; the product's rules forbid some of them. Each admin operation checks the +; rules it could break before it runs. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) +) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off breaks two rules if done carelessly: nobody can log in, or +; the sharded database loses its routing key. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes) (is cfg.db-mode single))) + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) diff --git a/docker-compose.yml b/docker-compose.yml index c5c14eb..632380d 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -101,6 +101,12 @@ services: image: writ-problems command: ["payments"] + # Configuration space: the flag matrix exhausted, and the order that breaks it. + config-space: + build: . + image: writ-problems + command: ["config_space"] + # 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 ce0471d..d4a05fb 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments config-space" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index f90d174..0af5247 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,19 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The twenty scenarios this script walks by convention, and their 56 + # The twenty-one scenarios this script walks by convention, and their 60 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the twenty fails this line, which is the point of it — + # property to any of the twenty-one 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, and this line is where each of those had to be said out loud. - has "cross-check: all 56 properties of the twenty scenarios were considered" \ - "$out" "considered 56 properties: 54 compared, 2 not compared" - # Two of the 56 are not compared, and the count above is the only place that + # payments, 56 -> 60 with config-space, and this line is where each of those + # had to be said out loud. + has "cross-check: all 60 properties of the twenty-one scenarios were considered" \ + "$out" "considered 60 properties: 58 compared, 2 not compared" + # Two of the 60 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +460,10 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval, agent-guardrails and deployment one each, payments two. + # expense-approval, agent-guardrails, deployment and config-space one each, + # payments two. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 12 properties compared" + "never: 13 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -840,9 +842,52 @@ payments() { has "payments: G. double charges hide in orders that settled and shipped" "$dv" "settled yes" } +config_space() { + d="$here/config-space" + c="$d/config-space.claims" + echo "== The configuration space — every combination, not a sample ==" + echo " Q: can the admin operations reach a combination the product forbids?" + out=$("$WRIT" check "$d/config-space.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "config-space: the guarded operations are clean" "$st" 0 + has "config-space: A. 21 of the 64 combinations are reachable" "$out" "states: 21" + has "config-space: B. a fully-featured safe configuration exists" "$out" "holds fully-featured" + has "config-space: C. none the product forbids" "$out" "holds never-unsafe" + lacks "config-space: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/config-space-shortcut.writ" --claims "$c" --fiber cfg.region 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "config-space: one forgotten check is refused" "$sst" 1 + # The order finding: every step is allowed, and only this order gets there — + # turning SSO off first would block the shard. + has "config-space: D. the forbidden state, in one order of three allowed steps" "$sc" \ + "violated in 3 reachable situations witness: 1. enable-legacy-auth 2. shard 3. disable-sso" + has "config-space: E. yet every configuration can still be made safe" "$sc" "holds recoverable" + # FR-10's fibers: the same question per region. Legacy auth is forbidden in + # the EU, and it is the first step of the route. + has "config-space: F. only the US deployment can reach it" "$sc" "fiber cfg.region=us FAILS" + has "config-space: the EU one cannot" "$sc" "fiber cfg.region=eu holds" + + cmp=$("$WRIT" compare "$d/config-space.writ" "$d/config-space-v2.writ" 2>&1) + cst=$? + printf '%s\n' "$cmp" | sed 's/^/ | /' + exit_is "config-space: compare refuses the release that adds a flag" "$cst" 1 + has "config-space: G. the new flag reaches a forbidden state in one move" "$cmp" \ + "never-unsafe LOST witness: 1. enable-new-billing" + v2=$("$WRIT" check "$d/config-space-v2.writ" --claims "$c" 2>&1) + has "config-space: an operation the claims never acknowledged" "$v2" \ + "unadmitted enable-new-billing may break audit-when-multi-tenant" + + dv=$("$WRIT" derive "$d/config-space.writ" "$d/config-space.rules" final-db 2>&1) + has "config-space: H. the last phase is the sharded configurations" "$dv" "final-db (9 rows)" + lacks "config-space: and only those" "$dv" "single" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments config_space control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" From 83fc33a0bd1b5ebad46bb744417c187777e37aa5 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:48:49 +0300 Subject: [PATCH 7/7] Prune five examples whose ceremony costs more than the answer gotha, calculation, oversight, workflow and access each had 7-12 states, and their findings could be read off the move list or were fixed by the modelling choices. gotha and calculation were also political arguments whose verdicts depended on those choices, not on the search. island stays: its point is that a known paradox shows up as a declared gap. writ control and writ compare --git now run on payments (the idempotency key dropped across two commits loses never-double). The cross-check walks 18 scenarios and 55 properties, and its live assertions point at payments and deployment. Co-Authored-By: Claude Opus 5.5 --- README.md | 7 +- access/access.claims | 25 ---- access/access.rules | 27 ---- access/access.writ | 60 --------- calculation/README.md | 82 ------------ calculation/cross-check.sh | 57 -------- calculation/market.claims | 63 --------- calculation/market.rules | 36 ----- calculation/market.writ | 54 -------- calculation/planned.writ | 69 ---------- docker-compose.yml | 16 +-- gotha/README.md | 57 -------- gotha/cross-check.sh | 50 ------- gotha/gotha.claims | 96 ------------- gotha/gotha.rules | 35 ----- gotha/gotha.writ | 91 ------------- libraries/README.md | 1 - libraries/economy.lib.writ | 89 ------------ modality-cross-check.sh | 2 +- oversight/oversight-repeal.writ | 56 -------- oversight/oversight.claims | 29 ---- oversight/oversight.rules | 30 ----- oversight/oversight.writ | 66 --------- run-tests.sh | 231 +++++++------------------------- workflow/workflow.claims | 25 ---- workflow/workflow.rules | 36 ----- workflow/workflow.writ | 70 ---------- 27 files changed, 49 insertions(+), 1411 deletions(-) delete mode 100644 access/access.claims delete mode 100644 access/access.rules delete mode 100644 access/access.writ delete mode 100644 calculation/README.md delete mode 100755 calculation/cross-check.sh delete mode 100644 calculation/market.claims delete mode 100644 calculation/market.rules delete mode 100644 calculation/market.writ delete mode 100644 calculation/planned.writ delete mode 100644 gotha/README.md delete mode 100755 gotha/cross-check.sh delete mode 100644 gotha/gotha.claims delete mode 100644 gotha/gotha.rules delete mode 100644 gotha/gotha.writ delete mode 100644 libraries/economy.lib.writ delete mode 100644 oversight/oversight-repeal.writ delete mode 100644 oversight/oversight.claims delete mode 100644 oversight/oversight.rules delete mode 100644 oversight/oversight.writ delete mode 100644 workflow/workflow.claims delete mode 100644 workflow/workflow.rules delete mode 100644 workflow/workflow.writ diff --git a/README.md b/README.md index c62ee6e..61b062e 100644 --- a/README.md +++ b/README.md @@ -49,9 +49,6 @@ 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. | -| [`oversight/`](oversight/) | Can lawful moves permanently stop a case concluding? | Not as written; repeal one power and `writ compare` shows accountability **LOST**. | -| [`workflow/`](workflow/) | Can a KYC case ever get stuck? | Never — and where automation ends, a declared gap hands it to a human. | -| [`access/`](access/) | Can an admin grant always be revoked? | No: the break-glass grant is a latch. | | [`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. | @@ -65,13 +62,11 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | | The question | writ's answer | |---|---|---| | [`arch/`](arch/) | Which architectures satisfy a brief, from a bank of components? | 96 of 2,916 — and the one thing the brief forgot to say. | -| [`calculation/`](calculation/) | Prices or a plan: the same world under two rules. What does each guarantee? | Both can meet need; only prices avoid waste — the plan loses `no-waste`, with the route. | -| [`gotha/`](gotha/) | Is this falsifiable claim true? | No — a refuting situation, three moves away. | | [`timetable/`](timetable/) | Is the week a constraint solver produced any good? | Valid, but two rules fail: sport first thing, and no time to change after it. | | [`db-migration-problems/`](db-migration-problems/) | Is this schema migration safe at every instant, mid-rollout included? | The safe plans pass; the shortcuts fail with the breaking step. | The runner also covers `writ control` and `writ compare --git`. Shared -vocabularies — scheduling, chess, architecture, economy — live in +vocabularies — scheduling, chess, architecture — live in [`libraries/`](libraries/). Most scenarios also re-ask their questions through writ's rules engine diff --git a/access/access.claims b/access/access.claims deleted file mode 100644 index 109ea1d..0000000 --- a/access/access.claims +++ /dev/null @@ -1,25 +0,0 @@ -; The questions about access & privilege (§16). - -; Is revocation always still possible, or is some privilege permanent after the -; right grant sequence? `live` asks whether a no-admin situation is still -; reachable from EVERY reachable situation. It FAILS: once grant-breakglass-admin -; fires, mallory is admin forever (no revoke move), so no reachable situation can -; return to "nobody is admin". The witness names the single latching move. §3 -; asks the model to say whether an irreversible grant is a designed latch or a -; defect — here it is a designed latch (break-glass), and the property makes the -; latch mechanically visible. -(property revocation-possible - "admin can always still be fully revoked (no account left admin)" - (live (not (some (a account) (is a.role admin))))) - -; Which grant moves can break the root-tracing law? `writ check` reports -; traces-to-root can be broken by delegate-alice-to-mallory (it writes -; account.sponsor, an arrow the law's route traverses). We acknowledge it, -; recording ownership (§16.3). The role grants write account.role, not on the -; law's route, so accepting them would be reported `stale`. -(accept delegate-alice-to-mallory traces-to-root) - -; Which accounts hold admin right now? (§16.2) — empty at the baseline. -(query admins - (where (a account)) - (is a.role admin)) diff --git a/access/access.rules b/access/access.rules deleted file mode 100644 index 2108dfd..0000000 --- a/access/access.rules +++ /dev/null @@ -1,27 +0,0 @@ -; The revocation question, re-asked as a derivation (extension §2) for -; `modality-cross-check.sh`. -; -; `revocation-possible` is `live`, so this relation is the COUNTEREXAMPLE SET — -; the reachable situations from which "nobody is admin" can no longer be -; reached — and it is NON-EMPTY, because `writ check` reports this property as -; failing. That is the designed latch: grant-breakglass-admin has no inverse, -; so once it fires mallory is admin forever. -; -; Empty ⟺ the property holds. Note what that means for THIS file specifically: -; an inversion here — re-pointing `revocation-possible` at `can-still-revoke` — -; would NOT be caught by the cross-check, because both sets are non-empty in -; this scenario and both therefore read as `fails`. The `live` properties that -; catch an inversion are the ones that HOLD (oversight/accountability and both -; of workflow's), where the counterexample set is empty and the satisfying set -; is not. So the polarity of this file rests on the comment, not on the oracle. -; Do not "simplify" it into `can-still-revoke`. -; -; The `some` binder is the KERNEL's quantifier, evaluated by `Eval` inside the -; guard datum; `a` is lower-case on purpose, since an ALL-CAPS binder would read -; as a rule variable and be rejected (extension §4). - -(load "ct.rules") - -(satisfies no-admin (not (some (a account) (is a.role admin)))) -(can-reach can-still-revoke no-admin) -(trapped revocation-possible can-still-revoke) diff --git a/access/access.writ b/access/access.writ deleted file mode 100644 index 504cf23..0000000 --- a/access/access.writ +++ /dev/null @@ -1,60 +0,0 @@ -; Access & privilege (§3, "Access and privilege"). -; -; Accounts carry a role (user | admin) and a `sponsor` — the account that -; vouches for them — plus a fixed `source` of authority (the security root, or -; something external). The law `traces-to-root` demands each account's authority -; be inherited from its sponsor: two routes account → source-t that must agree. -; A delegation that rewires a sponsor to an externally-sourced account breaks it. -; -; The interesting question is revocation. Most admin grants are reversible. But -; `grant-breakglass-admin` is a DESIGNED LATCH: an emergency admin that, once -; granted, has no revoke move. It is the irreversible grant §3 asks the model to -; declare — here, on purpose (break-glass), not a defect. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema access - (type role-t (user admin)) - (type source-t (root external)) - (type account - (arrow role (to role-t)) ; user | admin (granted / revoked) - (arrow sponsor (to account)) ; who vouches for this account - (arrow source (to source-t) fixed)) ; where this account's authority comes from - ; every account's authority is inherited from its sponsor — the chain to root: - (equation traces-to-root - (= account.sponsor.source account.source))) - -(instance baseline access - (account root (role user) - (sponsor root) - (source root)) - (account alice (role user) - (sponsor root) - (source root)) - (account mallory (role user) - (sponsor mallory) - (source external))) - -(use access) -(initial baseline) - -; Reversible admin grant for a rank-and-file account. -(transition grant-alice-admin - (when (is alice.role user)) - (do (set alice.role admin))) - -(transition revoke-alice-admin - (when (is alice.role admin)) - (do (set alice.role user))) - -; The DESIGNED LATCH: the break-glass emergency admin. Once granted there is no -; revoke — by design. This is what makes revocation-possible FAIL. -(transition grant-breakglass-admin - (when (is mallory.role user)) - (do (set mallory.role admin))) - -; The grant that can break traces-to-root: rewire alice's sponsor to mallory, -; whose source is `external`, not the security root. -(transition delegate-alice-to-mallory - (when (is alice.sponsor root)) - (do (set alice.sponsor mallory))) diff --git a/calculation/README.md b/calculation/README.md deleted file mode 100644 index c47a1f6..0000000 --- a/calculation/README.md +++ /dev/null @@ -1,82 +0,0 @@ -# The calculation problem — prices or a plan - -One allotment of steel, three plants that want it. The clinic and the tractor -works need it; the monument does not. Each plant's real need is a fixed fact of -the world, but it sits at the plant: the allocator only sees the request each -plant sends. Two models of that world, one with prices and one with a plan, are -asked the same three questions from one claims file. - -## The model - -Both models load [`../libraries/economy.lib.writ`](../libraries/economy.lib.writ) -(plants, needs, the allotment, the allocation rule, the irreversible build, and -the law `signal-honest`) and declare the same twelve moves. They differ in one -conjunct. In [`market.writ`](market.writ) asking is a bid paid from the plant's -own budget, so only a plant with the need can make it. -[`planned.writ`](planned.writ) repeals it, so a request costs nothing: - -```lisp -;; market.writ ;; planned.writ -(form (request NAME P LEVEL) (form (request NAME P LEVEL) - (transition NAME (transition NAME - (when (and (not (is P.ask LEVEL)) (when (not (is P.ask LEVEL))) - (is P.need LEVEL))) (do (set P.ask LEVEL)))) - (do (set P.ask LEVEL)))) -``` - -`planned.writ` also declares a gap, `survey`: the plan has no procedure for -learning a need that no request carries. - -## What writ answers - -```console -$ writ check market.writ --claims market.claims -states: 12 edges: 18 -… -holds no-waste -… -holds need-always-still-meetable -… -$ writ check planned.writ --claims market.claims -states: 56 edges: 260 -… -gaps: 1 - survey — "the plan has no procedure by which the centre could learn a need that no request carries" (min 0 moves) -… -fails need-always-still-meetable - stuck at: #22 (clinic.ask=low tractor-works.ask=low monument.ask=high steel.at=monument steel.state=built) -… -$ writ compare market.writ planned.writ -equations: signal-honest preserved -properties: need-can-be-met preserved - no-waste LOST witness: 1. ask-monument-high 2. allocate-monument 3. build-monument - need-always-still-meetable LOST witness: 1. ask-monument-high 2. allocate-monument 3. build-monument -``` - -- **`need-can-be-met` holds in both.** The plan can get it right; writ prints - the three-move route to the clinic. -- **`no-waste` fails under the plan.** The monument asks, the allocator cannot - tell its request from the clinic's, and the steel is built into a statue. - Under prices the same moves exist, but the first one is never enabled. -- **`need-always-still-meetable` fails under the plan.** The build cannot be - undone, so the waste is terminal: writ prints the stuck situation. -- **`signal-honest`**, the library's law that the steel's holder asked - truthfully, is violated in 24 of the plan's 56 situations and none of the 12 - priced ones. A free signal makes every combination of requests reachable. - -## Take away - -A signal that costs the sender stays tied to the sender's situation. That -conjunct is the premise; writ checks what follows from it, over every reachable -situation. "Fails" means the plan permits the waste, not that it forces it. Need -is not weighted by wealth here, so the model says nothing else about markets; -the claims file lives apart so you can put it to a model of your own. - -## Run it - -```sh -writ check market.writ --claims market.claims -writ check planned.writ --claims market.claims -writ compare market.writ planned.writ -./cross-check.sh # the same questions via market.rules, both models -``` diff --git a/calculation/cross-check.sh b/calculation/cross-check.sh deleted file mode 100755 index 7605d04..0000000 --- a/calculation/cross-check.sh +++ /dev/null @@ -1,57 +0,0 @@ -#!/bin/sh -# Copyright (C) 2026 Alex Kunich -# SPDX-License-Identifier: AGPL-3.0-or-later -# calculation's three questions, asked twice — and asked of BOTH models. -# -# `writ check` reads the modalities in market.claims as CTL (runtime/checker.ml). -# `writ derive` answers the same three questions from market.rules as relations -# over the same enumerated space. They are two implementations, so a -# disagreement is a bug in one of them — never a number to adjust here. -# -# The pair is the reason this is a script of its own: one claims file and one -# rules file are put to both models, so the falsifying verdicts under -# `planned.writ` are cross-checked too, and not just the clean ones under -# `market.writ`. -# -# One line per (model, property), naming its modality. The polarity is the only -# thing that turns a row count into a verdict: -# -# possible the SATISFYING set non-empty = holds -# never the COUNTEREXAMPLE set empty = holds -# live the COUNTEREXAMPLE set empty = holds -# -# Usage: cross-check.sh (`writ` from $WRIT; default: the one on PATH) -set -u - -here=$(cd "$(dirname "$0")" && pwd) -WRIT=${WRIT:-writ} -bad=0 - -cross() { # model property modality - check=$("$WRIT" check "$here/$1.writ" --claims "$here/market.claims" 2>&1) - rows=$("$WRIT" derive "$here/$1.writ" "$here/market.rules" "$2" 2>&1 | grep -c '^ ') - case "$3" in - possible) [ "$rows" -gt 0 ] && derived=holds || derived=fails ;; - never | live) [ "$rows" -eq 0 ] && derived=holds || derived=fails ;; - esac - if printf '%s\n' "$check" | grep -qx "holds $2"; then said=holds; else said=fails; fi - - if [ "$derived" = "$said" ]; then - printf ' [ok] %s/%s (%s): %s rows from derive, both say %s\n' "$1" "$2" "$3" "$rows" "$said" - else - printf ' [FAIL] %s/%s (%s): %s rows ⇒ derive says %s, check says %s\n' \ - "$1" "$2" "$3" "$rows" "$derived" "$said" - bad=1 - fi -} - -cross market need-can-be-met possible -cross market no-waste never -cross market need-always-still-meetable live - -cross planned need-can-be-met possible -cross planned no-waste never -cross planned need-always-still-meetable live - -[ "$bad" -eq 0 ] || echo "a DISAGREEMENT — a finding to report, not a number to adjust" -exit "$bad" diff --git a/calculation/market.claims b/calculation/market.claims deleted file mode 100644 index 6b9129d..0000000 --- a/calculation/market.claims +++ /dev/null @@ -1,63 +0,0 @@ -; The questions about the allocation of one scarce input (§16). They sit beside -; `market.writ` because a claims file is read as a model's sibling by `writ query` -; and `writ compare` — but they are not *about* it. They are put to `planned.writ` -; unchanged, by name: -; -; writ check planned.writ --claims market.claims -; -; which is the whole reason questions live apart from models. The two models -; share a library, a schema, an instance, a move set and every transition name; -; they differ in one guard. So this file is the experiment: the questions are -; held fixed, and the verdicts are what move. - -; 1. CAN it come out right? Neither arrangement is incapable — this is not a -; question about competence. It holds in both, and `writ` prints the route. -(property need-can-be-met - "the steel can end up built at a plant that needed it" - (possible (and (is steel.state built) (is steel.at.need high)))) - -; 2. Can it come out WRONG? `never` asks whether any reachable situation has the -; steel built at a plant with no need of it. Under a costless request, one can: -; the monument asks, the allocator has nothing to weigh the request against, and -; the steel is spent. Under a backed bid the same three moves are written down -; and the first of them never becomes available. -(property no-waste - "the steel is never built at a plant that does not need it" - (never (and (is steel.state built) (is steel.at.need low)))) - -; 3. And after it has come out wrong, can it be put right? `live` asks whether a -; good outcome is still reachable from EVERY reachable situation. This is the -; one that matters, and the one the tool exists for: 2 says a bad outcome is -; permitted, 3 says it is terminal. Steel welded into a monument is not a delay -; to be corrected by a better plan next quarter; there is no next quarter for -; that steel. -(property need-always-still-meetable - "from every situation the rules allow, the steel can still be built where it is needed" - (live (and (is steel.state built) (is steel.at.need high)))) - -; THE LAW, and who can break it. `signal-honest` (in the library) demands that -; the plant holding the steel be one whose request matches its situation. Every -; move that writes `ask` or `at` can break it — nine of the twelve — and both -; models are handed the same ledger, because both models have the same nine -; moves under the same names. Acknowledging a move is not conceding that it does -; break the law: `can be broken by` is about what a move WRITES. Which model -; actually reaches a violation is the finding, and it is not the same answer -; twice. -(accept ask-clinic-high signal-honest) -(accept ask-clinic-low signal-honest) -(accept ask-tractor-high signal-honest) -(accept ask-tractor-low signal-honest) -(accept ask-monument-high signal-honest) -(accept ask-monument-low signal-honest) -(accept allocate-clinic signal-honest) -(accept allocate-tractor signal-honest) -(accept allocate-monument signal-honest) - -; Which plants actually need the steel? (§16.2) The answer is the same in both -; models, at state 0 and at every other, because `need` is wiring. The fact is -; in the world, sitting in the model, printable on demand — and in `planned.writ` -; there is no move whose guard can read it. That is the whole difficulty in one -; line of output: the problem is never that the information does not exist. -(query who-needs-it - (where (p plant)) - (is p.need high)) diff --git a/calculation/market.rules b/calculation/market.rules deleted file mode 100644 index 53ca104..0000000 --- a/calculation/market.rules +++ /dev/null @@ -1,36 +0,0 @@ -; The three questions of market.claims, re-asked as derivations (extension §2). -; `cross-check.sh` beside this file puts them to BOTH models and compares each -; against `writ check`: if the two ever disagree, one of them is wrong and the -; disagreement is the finding — not a number to adjust. -; -; POLARITY — read this before "fixing" anything below. -; possible F the relation is the SATISFYING set non-empty ⟺ holds -; live F the relation is the COUNTEREXAMPLE set empty ⟺ holds -; never F the relation is the COUNTEREXAMPLE set empty ⟺ holds -; -; All three relations here are EMPTY-or-not against the priced model, where the -; two counterexample sets are empty and the satisfying set is not — which is the -; configuration that would catch an inversion, since swapping a polarity flips -; a verdict rather than leaving both sets non-empty (as access.rules warns of -; its own). The same file put to `planned.writ` returns the mirror image: -; -; writ derive planned.writ market.rules no-waste -; -; names the situations in which the steel is standing in a statue. - -(load "ct.rules") - -; `possible`: the satisfying set — situations, reachable from the start, in -; which the steel has been built at a plant that needed it. -(satisfies need-can-be-met (and (is steel.state built) (is steel.at.need high))) - -; `never`: the counterexample set — the situations that satisfy the FORBIDDEN -; guard, steel spent where there was no need for it. Writing this as the -; satisfying set of the safe guard would invert the oracle while leaving the -; script green. -(satisfies no-waste (and (is steel.state built) (is steel.at.need low))) - -; `live`: F, then EF F, then the reachable situations where EF F fails. Steel -; already welded into a monument shows up here, because no edge leaves `built`. -(can-reach can-still-meet need-can-be-met) -(trapped need-always-still-meetable can-still-meet) diff --git a/calculation/market.writ b/calculation/market.writ deleted file mode 100644 index 026cde7..0000000 --- a/calculation/market.writ +++ /dev/null @@ -1,54 +0,0 @@ -; THE PRICED ECONOMY. The same allotment of steel, the same three plants, the -; same centre-and-allocator machinery — and one different guard. -; -; Everything about the world lives in ../libraries/economy.lib.writ and is -; IDENTICAL to `planned.writ` next door: the same plants with the same needs, the -; same allocation rule reading the same `ask`, the same one-way commitment. The -; transitions have the same NAMES, so the same claims file can be put to both. -; -; Here, the signal is a BID, and a bid is backed. Asking for the steel means -; offering to pay for it out of the plant's own budget, so a plant that does not -; need the steel is not merely unwise to ask — the move is not available to it: -; `(when (and (not (is P.ask LEVEL)) (is P.need LEVEL)))`. -; -; That guard is the entire claim being made about prices, and it is worth being -; blunt about what it does and does not assert. It does NOT say markets are -; efficient, fair, or good. It says one thing: a signal that costs the sender -; something is a signal whose value cannot be raised for free, so it stays tied -; to the sender's own situation — which is the one thing that makes `P.need` -; reachable by an allocator standing outside the plant. There is no other -; channel in either file, and there is no other difference between them. - -(load "../libraries/economy.lib.writ") - -(use economy) -(initial year-one) - -; THE SIGNAL: a bid. Same shape, same name, one extra conjunct — the bid must be -; backed by the plant's own situation. This is the one datum that differs from -; planned.writ. -(form (request NAME P LEVEL) - (transition NAME - (when (and (not (is P.ask LEVEL)) - (is P.need LEVEL))) - (do (set P.ask LEVEL)))) - -(request ask-clinic-high clinic high) -(request ask-clinic-low clinic low) -(request ask-tractor-high tractor-works high) -(request ask-tractor-low tractor-works low) -(request ask-monument-high monument high) -(request ask-monument-low monument low) - -; THE ALLOCATION and the COMMITMENT, from the library — byte-identical to -; planned.writ. `allocate-monument` is written down here exactly as it is there: -; the rules permit the monument to be given the steel. It never is, and no guard -; in this file forbids it — the move simply never becomes available, because the -; signal it waits on cannot be produced. -(allocate allocate-clinic clinic) -(allocate allocate-tractor tractor-works) -(allocate allocate-monument monument) - -(build build-clinic clinic) -(build build-tractor tractor-works) -(build build-monument monument) diff --git a/calculation/planned.writ b/calculation/planned.writ deleted file mode 100644 index db3594e..0000000 --- a/calculation/planned.writ +++ /dev/null @@ -1,69 +0,0 @@ -; THE PLANNED ECONOMY. One allotment of steel, three plants, and a centre that -; decides where it goes. -; -; This is `market.writ` with ONE conjunct repealed, and it is written as a repeal -; on purpose — the way `oversight-repeal.writ` is written against `oversight.writ` -; — so that `writ compare market.writ planned.writ` can name what the repeal costs. -; -; Everything about the world — the plants, which of them genuinely needs the -; steel, the allocation rule, the fact that steel welded into a building stays -; welded into it — lives in ../libraries/economy.lib.writ and is IDENTICAL to -; `market.writ` next door. This file contributes one thing the library does not: -; the move that produces the signal the allocator reads. -; -; Here, a request is FREE. A plant tells the centre it needs the steel by -; saying so. Saying so costs the plant nothing, so the guard on the move that -; says it cannot mention what the plant actually needs — there is nothing to -; mention it WITH. `(when (not (is P.ask high)))`: any plant, any time. -; -; That is the whole model of central planning, and it is deliberately the most -; favourable one. This centre is not corrupt, not lazy and not malicious; the -; plants are not lying, since nothing here says a plant knows its request is -; unwarranted. The centre may reallocate as often as it likes, right up until -; the steel is built. Both files declare the same twelve moves under the same -; twelve names, and every move that can ever fire in `market.writ` can fire here -; — plus three that cannot fire there: the monument's request, and the two -; withdrawals a plant that does need the steel has no grounds to make. -; -; What it does not have is a way for the centre to find out what the requests do -; not carry. That absence is written down, at the bottom, as a `gap`. - -(load "../libraries/economy.lib.writ") - -(use economy) -(initial year-one) - -; THE SIGNAL: a request. The guard says only that the plant is not already -; asking — no mention of `P.need`, because a costless request cannot carry it. -; This is the one datum that differs from market.writ. -(form (request NAME P LEVEL) - (transition NAME - (when (not (is P.ask LEVEL))) - (do (set P.ask LEVEL)))) - -(request ask-clinic-high clinic high) -(request ask-clinic-low clinic low) -(request ask-tractor-high tractor-works high) -(request ask-tractor-low tractor-works low) -(request ask-monument-high monument high) -(request ask-monument-low monument low) - -; THE ALLOCATION and the COMMITMENT, from the library — byte-identical to -; market.writ, down to the transition names, which is what lets one claims file -; be put to both. -(allocate allocate-clinic clinic) -(allocate allocate-tractor tractor-works) -(allocate allocate-monument monument) - -(build build-clinic clinic) -(build build-tractor tractor-works) -(build build-monument monument) - -; WHERE THE RULES STOP. The centre would like to know which plant actually needs -; the steel — not which has asked. There is no move here that finds out, and the -; honest thing is to say so rather than invent one: a plan is a procedure, and -; this procedure has no step that reads a `need`. The gap is the economic -; calculation problem, written in the one word the language has for it. -(transition survey - (when (is steel.state idle)) - (do (gap "the plan has no procedure by which the centre could learn a need that no request carries"))) diff --git a/docker-compose.yml b/docker-compose.yml index 632380d..0b83780 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -17,6 +17,7 @@ services: image: writ-problems command: ["river"] + # Knights & knaves — the reading that makes the story consistent. island: build: . @@ -41,23 +42,8 @@ services: image: writ-problems command: ["jobshop_best"] - # Institutional architecture — laws, acknowledgments, and `writ compare` across an amendment. - oversight: - build: . - image: writ-problems - command: ["oversight"] - # A regulated workflow: a declared `gap` where the rules stop. - workflow: - build: . - image: writ-problems - command: ["workflow"] - # Access and privilege, including a one-way latch. - access: - build: . - image: writ-problems - command: ["access"] # Separation of duties: the toxic-combination table, and the role it misses. separation-of-duties: diff --git a/gotha/README.md b/gotha/README.md deleted file mode 100644 index d78a42c..0000000 --- a/gotha/README.md +++ /dev/null @@ -1,57 +0,0 @@ -# A claim about common ownership, and its falsifier - -A claim is testable when it forbids something. "Where exploitation persists, -communism has not been achieved" forbids nothing. Stated so that it can be -wrong, the doctrine reads: - -> Once the means of production are held in common, no surplus goes to a party -> outside the work, by the decision of a party outside the work. - -## The model - -One mill. Ownership is split into four arrows: `title`, `worked-by` (fixed), -`directed-by` (whose decision disposes of the product) and `surplus-to` (where -the surplus went). Five moves, each one the programme asks for: `expropriate` -(granted in full, with no way back), `distribute`, `appoint-board`, -`fund-administration` (Gotha's second deduction) and `recall-board`. The claim -is a `never` in [`gotha.claims`](gotha.claims): the mill is common and the -surplus has gone, by direction, to someone who does not work it. - -## What writ answers - -```console -$ writ check gotha.writ --claims gotha.claims -states: 7 edges: 13 -… -holds expropriation-succeeds -… -fails no-exploitation -… - witness: 1. expropriate → #1 loom-house.title: private → common, loom-house.directed-by: proprietor → weavers, loom-house.surplus-to: proprietor → ∅ - 2. appoint-board → #3 loom-house.directed-by: weavers → board - 3. fund-administration → #5 loom-house.surplus-to: ∅ → board -holds exploitation-endable -… -``` - -The revolution succeeds (`expropriation-succeeds`), so the claim's antecedent -is really reached. Then the claim fails in three moves: the commune -appoints a board to administer the deductions, and the board makes one. None of -the moves is a betrayal; each is the programme carried out. The check exits 1. -`exploitation-endable` holds too: from every situation `recall-board` can -return the surplus to the weavers. The claim is false; the outcome is no trap. - -## Take away - -The refutation is exact. Ownership was several arrows and `expropriate` moves -only `title`; the claim that would have done the work is about `directed-by`, -and nothing here refutes that one. A `never` claim's potential falsifiers can -be listed: `gotha.rules` finds one, situation 5 of 7, and it is reachable. - -## Run it - -```sh -writ check gotha.writ --claims gotha.claims -writ derive gotha.writ gotha.rules no-exploitation -./cross-check.sh # the same questions via gotha.rules -``` diff --git a/gotha/cross-check.sh b/gotha/cross-check.sh deleted file mode 100755 index 46aceba..0000000 --- a/gotha/cross-check.sh +++ /dev/null @@ -1,50 +0,0 @@ -#!/bin/sh -# Copyright (C) 2026 Alex Kunich -# SPDX-License-Identifier: AGPL-3.0-or-later -# gotha's three questions, asked twice. -# -# `writ check` reads the modalities in gotha.claims as CTL (runtime/checker.ml). -# `writ derive` answers the same three questions from gotha.rules as relations -# over the same enumerated space. They are two implementations, so a -# disagreement is a bug in one of them — never a number to adjust here. -# -# One line per property, naming its modality. The polarity is the only thing -# that turns a row count into a verdict, and getting it backwards is the failure -# mode that leaves a cross-check green while meaning nothing: -# -# possible the SATISFYING set non-empty = holds -# never the COUNTEREXAMPLE set empty = holds -# live the COUNTEREXAMPLE set empty = holds -# -# Usage: cross-check.sh (`writ` from $WRIT; default: the one on PATH) -set -u - -here=$(cd "$(dirname "$0")" && pwd) -WRIT=${WRIT:-writ} -model="$here/gotha.writ" -check=$("$WRIT" check "$model" --claims "$here/gotha.claims" 2>&1) -bad=0 - -cross() { # property modality - rows=$("$WRIT" derive "$model" "$here/gotha.rules" "$1" 2>&1 | grep -c '^ ') - case "$2" in - possible) [ "$rows" -gt 0 ] && derived=holds || derived=fails ;; - never | live) [ "$rows" -eq 0 ] && derived=holds || derived=fails ;; - esac - if printf '%s\n' "$check" | grep -qx "holds $1"; then said=holds; else said=fails; fi - - if [ "$derived" = "$said" ]; then - printf ' [ok] %s (%s): %s rows from derive, both say %s\n' "$1" "$2" "$rows" "$said" - else - printf ' [FAIL] %s (%s): %s rows ⇒ derive says %s, check says %s\n' \ - "$1" "$2" "$rows" "$derived" "$said" - bad=1 - fi -} - -cross expropriation-succeeds possible -cross no-exploitation never -cross exploitation-endable live - -[ "$bad" -eq 0 ] || echo "a DISAGREEMENT — a finding to report, not a number to adjust" -exit "$bad" diff --git a/gotha/gotha.claims b/gotha/gotha.claims deleted file mode 100644 index d97eb84..0000000 --- a/gotha/gotha.claims +++ /dev/null @@ -1,96 +0,0 @@ -; THE CLAIM UNDER TEST, and its refutation. -; -; A claim is testable, in Popper's sense, when it FORBIDS something: the class -; of its potential falsifiers must be non-empty. That is exactly what `never` -; is. `(never F)` is a prohibition, F describes the potential falsifiers, and -; `writ` searches every reachable situation for one — so a refutation here is not -; an opinion about the claim but a route to a situation the claim says cannot -; occur, printed move by move. -; -; THE UNTESTABLE VERSION, first, since it is the one usually said out loud: -; -; "Communism is the end of exploitation; where exploitation persists, -; communism has not been achieved." -; -; This forbids nothing. Any situation you exhibit is answered by withdrawing the -; antecedent, which is the conventionalist twist Popper named — and it is the -; reason that sentence is not what is tested below. It cannot be. It has no -; potential falsifiers. -; -; THE TESTABLE VERSION, which is a real claim with real content: -; -; "Once the means of production are held in common, no surplus is disposed -; of by anyone who does not work them." -; -; It forbids a definite thing: a common mill whose surplus is disposed of under -; the direction of a party that does not work it. `no-exploitation` below is -; that prohibition, written down. If it holds, the claim survives this test. -; -; THE CRITERION IS TAKEN AT ITS STRONGEST, which is what makes the refutation -; worth having. Two weaker readings are available and neither is used: -; -; receipt alone — "no non-producer ever RECEIVES any of the surplus" is -; refuted by paying a bookkeeper, and refuting it would -; prove nothing: the Gotha Programme provides for exactly -; such payments, and no one disputes that it does. -; direction alone — "no non-producer ever DECIDES" is refuted by appointing a -; manager, which again is asked for by the programme and -; contested by nobody. -; -; What `no-exploitation` forbids is the CONJUNCTION: a common mill whose surplus -; has gone to a party outside the work, by the decision of a party outside the -; work. That is the arrangement the word names when it is used of a proprietor, -; and a claim refuted in this form is refuted in the weaker forms a fortiori. -; -; EVERY MOVE THE REFUTATION USES IS ONE THE PROGRAMME CALLS FOR. -; expropriate Manifesto §II — "Abolition of private property." -; distribute Gotha — the remainder, after the deductions, to the -; producers. -; appoint-board Gotha — the deductions are administered by someone; -; and Lenin, 1918, on one-man management. -; fund-administration Gotha — "the general costs of administration not -; belonging to production", the second deduction from -; the total product. -; recall-board The Paris Commune, and State and Revolution — every -; official elective and revocable at any time. -; None of them is a betrayal, a degeneration or a mistake. They are the -; programme being carried out. - -; 1. THE ANTECEDENT IS REACHED, IN FULL. Before a refutation can mean anything, -; the thing being tested has to happen: the mill really does become common, and -; the surplus really does reach the producers. `writ` prints the two moves. A -; model in which the revolution failed would refute nothing. -(property expropriation-succeeds - "the mill can be brought into common ownership with the surplus in the hands that worked it" - (possible (and (is loom-house.title common) - (is loom-house.surplus-to weavers)))) - -; 2. THE CLAIM. Reachable ⇒ refuted, and the witness is the falsifier. -(property no-exploitation - "once the mill is common, no surplus goes to a party outside the work by the decision of a party outside the work" - (never (and (is loom-house.title common) - (is loom-house.surplus-to.produces no) - (is loom-house.directed-by.produces no)))) - -; 3. HOW FAR THE REFUTATION GOES — which is not as far as the slogan opposite it -; would like. `live` asks whether the producers can still get the surplus from -; EVERY reachable situation. With recall in the file it holds: what the model -; exhibits is a permitted condition, not a trap. The claim is false; "and -; therefore it is hopeless" is a second claim, and this one does not support it. -(property exploitation-endable - "from every situation, the surplus can still return to the hands that worked the mill" - (live (and (is loom-house.title common) - (is loom-house.surplus-to weavers)))) - -; The programme's own law, and which of the programme's own moves can break it. -; Every move that writes `surplus-to` is a breaker, whichever way it writes it — -; `can be broken by` is about what a move WRITES, not about what it reaches. -(accept expropriate surplus-to-producers) -(accept distribute surplus-to-producers) -(accept fund-administration surplus-to-producers) - -; Who is in a position to dispose of what they did not make? (§16.2) At state 0 -; the answer is the proprietor — the arrangement the expropriation abolishes. -(query non-producers - (where (c claimant)) - (is c.produces no)) diff --git a/gotha/gotha.rules b/gotha/gotha.rules deleted file mode 100644 index 166ce3c..0000000 --- a/gotha/gotha.rules +++ /dev/null @@ -1,35 +0,0 @@ -; The three questions of gotha.claims, re-asked as derivations (extension §2). -; `cross-check.sh` beside this file runs both and compares them: if `writ derive` -; and `writ check` ever disagree, one of them is wrong and the disagreement is -; the finding — not a number to adjust. -; -; POLARITY — read this before "fixing" anything below. -; possible F the relation is the SATISFYING set non-empty ⟺ holds -; live F the relation is the COUNTEREXAMPLE set empty ⟺ holds -; never F the relation is the COUNTEREXAMPLE set empty ⟺ holds -; -; `no-exploitation` is the refutation, so its set is the interesting one to read -; directly — it is the model's potential falsifiers, enumerated: -; -; writ derive gotha.writ gotha.rules no-exploitation - -(load "ct.rules") - -; `possible`: the situations in which the mill is common and the surplus is in -; the hands that worked it. One guard, used twice below — it was written out -; twice before, once here and once as `restored` for the `live`. -(satisfies expropriation-succeeds (and (is loom-house.title common) - (is loom-house.surplus-to weavers))) - -; `never`: the counterexample set — the situations that satisfy the FORBIDDEN -; guard, a common mill whose surplus has gone outside the work by a decision -; taken outside the work. Writing this as the satisfying set of the permitted -; guard would invert the oracle while leaving the script green. -(satisfies no-exploitation (and (is loom-house.title common) - (is loom-house.surplus-to.produces no) - (is loom-house.directed-by.produces no))) - -; `live`: F, then EF F, then the reachable situations where EF F fails. Empty, -; because recall-board has no precondition beyond the board directing. -(can-reach can-still-restore expropriation-succeeds) -(trapped exploitation-endable can-still-restore) diff --git a/gotha/gotha.writ b/gotha/gotha.writ deleted file mode 100644 index 807f125..0000000 --- a/gotha/gotha.writ +++ /dev/null @@ -1,91 +0,0 @@ -; One mill, and the claim that abolishing its private ownership abolishes -; exploitation. Twenty-six lines of model; the claim is in gotha.claims. -; -; THE POINT OF THE SCHEMA is that where ordinary speech has one word — "owns" — -; the mill has three arrows, and they are free to move independently: -; -; worked-by who does the work (fixed: a fact) -; directed-by whose decision disposes of the product (the control right) -; surplus-to where this period's surplus went (the distribution) -; -; Under a proprietor all three are settled together, which is what makes -; "abolish private ownership" sound like a complete instruction. It names only -; `title`, a fourth arrow, and the model has to be able to say so BEFORE any -; move is written — otherwise the finding below would be built into the moves -; rather than found among them. -; -; Every move here is one the programme itself calls for. Nothing is smuggled in: -; see the header of gotha.claims for which text asks for which move. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema commons - (type yn (no yes)) - (type title-t (private common)) - (type claimant - (arrow produces (to yn) fixed)) ; whether a party does the work: a fact, - (type mill ; not a setting — no move rewrites it - (arrow title (to title-t)) - (arrow worked-by (to claimant) fixed) - (arrow directed-by (to claimant)) - (maybe surplus-to claimant)) - ; THE PROGRAMME AS A LAW. Two routes mill → claimant — where the surplus went, - ; and who did the work — which must agree. Not a rule the model obeys: the - ; promise the model is measured against, so `writ` reports which situations - ; break it. - (equation surplus-to-producers - (= mill.surplus-to mill.worked-by))) - -(instance old-regime commons - (claimant weavers (produces yes)) - (claimant proprietor (produces no)) - (claimant board (produces no)) - (mill loom-house (title private) - (worked-by weavers) - (directed-by proprietor) - (surplus-to proprietor))) - -(use commons) -(initial old-regime) - -; THE EXPROPRIATION, granted in full and granted at once: title passes to the -; commons, direction passes to those who work the mill, and the proprietor's -; claim on the surplus lapses. There is no move back — no restoration, no -; sabotage, no invasion — so nothing found below can be blamed on the revolution -; having been incomplete or reversed. -(transition expropriate - (when (is loom-house.title private)) - (do (set loom-house.title common) - (set loom-house.directed-by weavers) - (vacate loom-house.surplus-to))) - -; DISTRIBUTION TO THE PRODUCERS — the programme's own purpose, available from -; the moment the mill is common and directed by those who work it. -(transition distribute - (when (and (is loom-house.title common) - (is loom-house.directed-by weavers))) - (do (set loom-house.surplus-to weavers))) - -; THE ADMINISTRATION. Gotha's deductions do not administer themselves, and the -; commune appoints a body to do it — which is a transfer of the DIRECTION, not -; only of the bookkeeping, because a body that may not decide cannot make a -; deduction. This is the move the claim does not mention and does not forbid. -(transition appoint-board - (when (and (is loom-house.title common) - (is loom-house.directed-by weavers))) - (do (set loom-house.directed-by board))) - -; "THE GENERAL COSTS OF ADMINISTRATION NOT BELONGING TO PRODUCTION" — Marx's own -; second deduction from the total product, made by the body that administers. -(transition fund-administration - (when (and (is loom-house.title common) - (is loom-house.directed-by board))) - (do (set loom-house.surplus-to board))) - -; RECALL. The Commune's principle and Lenin's: every official elective and -; revocable at any time. Unguarded on purpose — anyone may recall the board, -; from any situation, at no cost. It is the most favourable assumption in the -; file, and the third property is what it buys. -(transition recall-board - (when (is loom-house.directed-by board)) - (do (set loom-house.directed-by weavers))) diff --git a/libraries/README.md b/libraries/README.md index 1169ee3..dc680da 100644 --- a/libraries/README.md +++ b/libraries/README.md @@ -9,7 +9,6 @@ hold the shared vocabulary for the scenarios beside them. | [`scheduling.lib.writ`](scheduling.lib.writ) | `jobshop-possible/`, `jobshop-best/` | machines, jobs, routings, the blocking rule, a clock | | [`arch.lib.writ`](arch.lib.writ) | `arch/` | components, stages and their demands, the `fits` test, the design cursor | | [`school.lib.writ`](school.lib.writ) | `timetable/` | the week, rooms, capacity, staff, the curriculum as one entity per hour, a booking | -| [`economy.lib.writ`](economy.lib.writ) | `calculation/` | plants and their needs, one scarce allotment, the allocation rule, the `signal-honest` law | A model, claims file or rules file loads one by relative path: `(load "../libraries/chess.lib.writ")`. A library holds declarations only (a diff --git a/libraries/economy.lib.writ b/libraries/economy.lib.writ deleted file mode 100644 index 00f6402..0000000 --- a/libraries/economy.lib.writ +++ /dev/null @@ -1,89 +0,0 @@ -; economy.lib.writ — a DOMAIN library: one scarce allotment, several plants that -; could use it, and an allocator that reads a signal. -; -; The sibling of scheduling.lib.writ beside it, and the same split: a library -; says what EXISTS, a model says what may HAPPEN. `calculation/planned.writ` and -; `calculation/market.writ` both load this file and then differ in ONE guard — -; the guard on the move that produces the signal the allocator reads. Everything -; else — the plants, their true needs, the allocation rule, the irreversible -; commitment — is here, identical for both, so the comparison has exactly one -; free variable. -; -; WHERE IT LIVES. Beside the other domain libraries in `libraries/`, loaded by -; relative path: `(load "../libraries/economy.lib.writ")`. -; -; It pays the namespace, as any library does (§7): every model loading it gives -; up `level`, `plant`, `allotment`, `need`, `ask`, `low`, `high` and the entity -; names. That cost is why this is a DOMAIN library and not an addition to -; stdlib — a standard library may not spend the shared namespace on a worldly -; concept. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema economy - - (type level (low high)) - - (type build-state (idle built)) - - ; A PLANT has two arrows to `level`, and the whole scenario is the gap between - ; them. - ; - ; `need` — how badly this plant actually needs the allotment. It is `fixed`: - ; wiring, a fact about the world, set by the instance and never varying. It - ; is also LOCAL: it sits at the plant, and no move in either model reads it - ; except a move belonging to that plant. - ; - ; `ask` — what the allocator is told. This is state: it is the only thing - ; the allocation rule below can see. - ; - ; Two routes plant → level. Nothing in the schema makes them agree. - (type plant - (arrow need (to level) fixed) - (arrow ask (to level))) - - ; THE ALLOTMENT — one indivisible quantity of a scarce input. `at` is - ; vacatable: before anyone is given it, it is held by nobody, and nobody is - ; not a plant. `state` records whether it is still movable (`idle`) or has - ; been built into something (`built`, and irreversibly so — no move in either - ; model sets it back). - (type allotment - (maybe at plant) - (arrow state (to build-state))) - - ; THE LAW. Two routes allotment → level: the ask of whoever holds it, and the - ; need of whoever holds it. They must agree — the allotment is held by a plant - ; whose signal is its situation. `=` is the vacuous comparison, so while the - ; allotment is held by nobody the law has nothing to say. - (equation signal-honest - (= allotment.at.ask allotment.at.need))) - -; THE ECONOMY. Three plants, one allotment of steel. Two plants genuinely need -; it and one does not; only one of them can have it. `ask` starts `low` -; everywhere — nobody has said anything yet — and the steel starts held by -; nobody. -(instance year-one economy - (plant clinic (need high) (ask low)) - (plant tractor-works (need high) (ask low)) - (plant monument (need low) (ask low)) - (allotment steel (at vacant) (state idle))) - -; THE ALLOCATION RULE, identical in both models. The allocator moves the steel -; to a plant that has asked for it, as long as the steel has not yet been built -; into anything. Note what the guard reads: `P.ask`. It cannot read `P.need`, -; and that is not an oversight — an allocator is not standing in the plant. -(form (allocate NAME P) - (transition NAME - (when (and (is steel.state idle) - (is P.ask high) - (not (is steel.at P)))) - (do (set steel.at P)))) - -; COMMITMENT, identical in both models. Steel that has been welded into a -; building is steel that is no longer steel. One-way: `built` has no move out, -; which is why a misallocation here is not a delay but a loss. -(form (build NAME P) - (transition NAME - (when (and (is steel.state idle) - (is steel.at P))) - (do (set steel.state built)))) diff --git a/modality-cross-check.sh b/modality-cross-check.sh index d4a05fb..15c9865 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails 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" considered=0 compared=0 diff --git a/oversight/oversight-repeal.writ b/oversight/oversight-repeal.writ deleted file mode 100644 index 4cc05a3..0000000 --- a/oversight/oversight-repeal.writ +++ /dev/null @@ -1,56 +0,0 @@ -; The amendment: oversight.writ with `restore-watchdog` DELETED. -; -; This is the running example minus the power to restore a captured watchdog. -; It looks procedural — "we removed one seldom-used move" — but `writ compare` -; against oversight.writ shows its true cost: `accountability` is LOST. Once the -; watchdog is captured there is no way back, the investigation stalls, and the -; docket can never conclude from that situation. One lawful move (capture- -; watchdog) now permanently destroys accountability — the §3 institutional -; question, answered by `live` + `writ compare`. -; -; Everything below is identical to oversight.writ except the restore-watchdog -; transition is gone. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema oversight - (type indep-status (independent captured)) - (type stage-t (open concluded)) - (type person - (arrow employer (to bureau) fixed)) - (type bureau - (arrow independence (to indep-status))) - (type case - (arrow stage (to stage-t)) - (arrow investigator (to bureau) fixed) - (arrow prosecutor (to bureau) fixed) - (maybe judge person)) - (equation same-agency - (= case.investigator.independence case.prosecutor.independence))) - -(instance day-one oversight - (bureau watchdog (independence independent)) - (bureau prosecutions (independence independent)) - (person alice (employer watchdog)) - (case docket (investigator watchdog) - (prosecutor prosecutions) - (stage open) - (judge vacant))) - -(use oversight) -(initial day-one) - -(transition capture-watchdog - (when (is watchdog.independence independent)) - (do (set watchdog.independence captured))) - -; restore-watchdog DELETED — the amendment removes restoration. - -(transition conclude - (when (and (is docket.stage open) - (is docket.investigator.independence independent))) - (do (set docket.stage concluded))) - -(transition assign-judge - (when (not (defined docket.judge))) - (do (set docket.judge alice))) diff --git a/oversight/oversight.claims b/oversight/oversight.claims deleted file mode 100644 index af7de2d..0000000 --- a/oversight/oversight.claims +++ /dev/null @@ -1,29 +0,0 @@ -; The questions about the oversight system, kept next to the model (§16). - -; Can the case ever conclude at all? (§16.1 `possible` — and, holding, it now -; prints the shortest route that concludes the docket.) -(property conviction-possible - "the docket can conclude" - (possible (is docket.stage concluded))) - -; Can ONE lawful move permanently destroy accountability? `live` asks whether a -; concluded docket is still reachable from EVERY reachable situation. It holds -; here because restore-watchdog can always undo a capture, so the prosecutor can -; regain independence and the case can still conclude. -(property accountability - "the docket can always still conclude" - (live (is docket.stage concluded))) - -; Which of our own powers can violate our own declared law? `writ check` reports -; that same-agency can be broken by capture-watchdog and restore-watchdog (both -; write watchdog.independence, an arrow the same-agency routes traverse). We -; acknowledge exactly those two — recording ownership (§16.3). We do NOT accept -; conclude or assign-judge: neither writes an arrow on either route, so an -; accept on them would be reported `stale`. -(accept capture-watchdog same-agency) -(accept restore-watchdog same-agency) - -; Which bureaus are captured right now? (§16.2) -(query captured-bureaus - (where (b bureau)) - (is b.independence captured)) diff --git a/oversight/oversight.rules b/oversight/oversight.rules deleted file mode 100644 index 4107b52..0000000 --- a/oversight/oversight.rules +++ /dev/null @@ -1,30 +0,0 @@ -; The oversight system's two properties, re-asked as derivations (extension §2) -; for `modality-cross-check.sh`. One `possible`, one `live` — and the two are -; encoded with OPPOSITE polarity, which is the thing to understand before -; editing either. -; -; `possible` is POSITIVE: `conviction-possible` holds the situations that -; satisfy F, so non-empty means the docket can conclude. -; -; `live` (AG EF F) has no positive encoding here — extension §3 rejects a -; nullary relation, so "for every reachable situation …" has nowhere to live as -; a fact. It is encoded as its COUNTEREXAMPLE SET: `accountability` holds the -; reachable situations from which a concluded docket is no longer reachable, so -; EMPTY means accountability holds. Rewriting it as "the situations that can -; still conclude" would invert the oracle's verdict on every `live` property in -; the repo while leaving the cross-check green. - -(load "ct.rules") - -; Both claims, from one guard — F, then EF F, then the reachable situations -; where EF F fails. Non-empty ⟺ `holds conviction-possible`; EMPTY ⟺ `holds -; accountability`. A capture with no restoration would show up as a witness -; situation in the last set; because restore-watchdog exists, it is empty. -; -; The guard was written twice here, once with an `(init S) (reach S T)` premise -; and once with `(situation T)`. They were always the same set — the engine -; enumerates reachable situations and nothing else (§12.3) — so the library's -; `satisfies` spells the one that says so. -(satisfies conviction-possible (is docket.stage concluded)) -(can-reach can-still-conclude conviction-possible) -(trapped accountability can-still-conclude) diff --git a/oversight/oversight.writ b/oversight/oversight.writ deleted file mode 100644 index 22e9033..0000000 --- a/oversight/oversight.writ +++ /dev/null @@ -1,66 +0,0 @@ -; The kernel-spec's running example (§4): an oversight system with two -; agencies (a watchdog investigator and a prosecutions bureau), one case -; (docket) and one — possibly vacant — judge. -; -; Schema, instance, equation and the capture/restore/assign moves are §4 -; VERBATIM. ONE token differs from §4's text: `conclude` guards on the -; INVESTIGATOR's independence (docket.investigator.independence), not the -; prosecutor's. In §4 as printed the capture power (over the watchdog = -; investigator) and the conclusion dependency (on the prosecutor) are decoupled, -; so no repeal of restoration could ever cost accountability — verified: the -; compare stays `preserved`, exit 0. Coupling conclude to the investigator makes -; the capture power actually bear on whether the case concludes: capturing the -; watchdog stalls the case, and restore-watchdog is what keeps accountability -; alive. This keeps the same-agency breaker list exactly {capture-watchdog, -; restore-watchdog}; capturing prosecutions instead would add two more breakers. -; -; The legislature retains powers over the oversight bodies (capture / restore the -; watchdog's independence). The schema declares a structural law, `same-agency`: -; the two routes case → indep-status (via investigator, via prosecutor) must -; agree — the investigating and prosecuting agencies stand on equal footing. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema oversight - (type indep-status (independent captured)) - (type stage-t (open concluded)) - (type person - (arrow employer (to bureau) fixed)) - (type bureau - (arrow independence (to indep-status))) - (type case - (arrow stage (to stage-t)) - (arrow investigator (to bureau) fixed) - (arrow prosecutor (to bureau) fixed) - (maybe judge person)) - (equation same-agency - (= case.investigator.independence case.prosecutor.independence))) - -(instance day-one oversight - (bureau watchdog (independence independent)) - (bureau prosecutions (independence independent)) - (person alice (employer watchdog)) - (case docket (investigator watchdog) - (prosecutor prosecutions) - (stage open) - (judge vacant))) - -(use oversight) -(initial day-one) - -(transition capture-watchdog - (when (is watchdog.independence independent)) - (do (set watchdog.independence captured))) - -(transition restore-watchdog - (when (is watchdog.independence captured)) - (do (set watchdog.independence independent))) - -(transition conclude - (when (and (is docket.stage open) - (is docket.investigator.independence independent))) - (do (set docket.stage concluded))) - -(transition assign-judge - (when (not (defined docket.judge))) - (do (set docket.judge alice))) diff --git a/run-tests.sh b/run-tests.sh index 0af5247..a62b794 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -57,6 +57,24 @@ river() { near "river: stranding prey with its predator is the mistake" "$out" "fails no-blunders" "stuck at:" } +island() { + echo "== Knights & knaves (kernel-spec Appendix D) ==" + echo " Q: can every native be classified, and who could be a knight?" + out=$("$WRIT" check "$here/island/island.writ" --claims "$here/island/island.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "island: check reports findings" "$st" 1 + has "island: 9 reachable situations" "$out" "states: 9" + has "island: A. the rules run out — a gap" "$out" "gaps: 1" + has "island: the hole is reading cal, the knave-sayer" "$out" "read-cal —" + has "island: the rules are silent there" "$out" "rules are silent" + has "island: B. NOT everyone is classifiable" "$out" "fails census-completable" + has "island: C. abe could be a knight" "$out" "holds abe-can-be-knight" + near "island: and writ shows the reading that makes it so" "$out" "holds abe-can-be-knight" "abe-is-knight" + has "island: bea could be a knight" "$out" "holds bea-can-be-knight" + has "island: cal could be nothing at all" "$out" "fails cal-can-be-knight" +} + queens() { echo "== Eight queens ==" echo " Q: can eight queens stand on a board with none attacking another?" @@ -85,23 +103,6 @@ queens() { fi } -island() { - echo "== Knights & knaves (kernel-spec Appendix D) ==" - echo " Q: can every native be classified, and who could be a knight?" - out=$("$WRIT" check "$here/island/island.writ" --claims "$here/island/island.claims" 2>&1) - st=$? - printf '%s\n' "$out" | sed 's/^/ | /' - exit_is "island: check reports findings" "$st" 1 - has "island: 9 reachable situations" "$out" "states: 9" - has "island: A. the rules run out — a gap" "$out" "gaps: 1" - has "island: the hole is reading cal, the knave-sayer" "$out" "read-cal —" - has "island: the rules are silent there" "$out" "rules are silent" - has "island: B. NOT everyone is classifiable" "$out" "fails census-completable" - has "island: C. abe could be a knight" "$out" "holds abe-can-be-knight" - near "island: and writ shows the reading that makes it so" "$out" "holds abe-can-be-knight" "abe-is-knight" - has "island: bea could be a knight" "$out" "holds bea-can-be-knight" - has "island: cal could be nothing at all" "$out" "fails cal-can-be-knight" -} jobshop_possible() { echo "== A blocking job shop ==" @@ -145,46 +146,7 @@ jobshop_best() { "holds done-by-5" "3. tick" } -oversight() { - echo "== Institutional architecture (kernel-spec §3, §4 running example) ==" - echo " Q: can one lawful move permanently destroy accountability, and what" - echo " does repealing restoration actually cost?" - out=$("$WRIT" check "$here/oversight/oversight.writ" --claims "$here/oversight/oversight.claims" 2>&1) - st=$? - printf '%s\n' "$out" | sed 's/^/ | /' - exit_is "oversight: check reports findings" "$st" 1 - has "oversight: A. our own powers can violate our own law" "$out" "equation same-agency" - has "oversight: the law's breakers are named" "$out" "can be broken by: capture-watchdog, restore-watchdog" - lacks "oversight: and both are accepted — nothing unadmitted" "$out" "unadmitted" - has "oversight: B. the case can conclude" "$out" "holds conviction-possible" - near "oversight: and writ prints the concluding move" "$out" "holds conviction-possible" "witness:" - has "oversight: C. accountability holds (restoration exists)" "$out" "holds accountability" - - echo " Q: this amendment repeals restoration — what does it change?" - cmp=$("$WRIT" compare "$here/oversight/oversight.writ" "$here/oversight/oversight-repeal.writ" 2>&1) - cst=$? - printf '%s\n' "$cmp" | sed 's/^/ | /' - exit_is "oversight: compare reports a loss" "$cst" 1 - has "oversight: D. the repeal LOSES accountability" "$cmp" "accountability LOST" - near "oversight: one capture now traps the case forever" "$cmp" "accountability" "capture-watchdog" - has "oversight: same-agency itself is preserved" "$cmp" "same-agency preserved" -} -workflow() { - echo "== Regulated workflow — KYC / claims (kernel-spec §3) ==" - echo " Q: where does automation end, which reassignments break the law, and" - echo " can a case get stuck?" - out=$("$WRIT" check "$here/workflow/workflow.writ" --claims "$here/workflow/workflow.claims" 2>&1) - st=$? - printf '%s\n' "$out" | sed 's/^/ | /' - exit_is "workflow: check reports findings" "$st" 1 - has "workflow: A. automation ends at an escalation gap" "$out" "gaps: 1" - has "workflow: the gap hands off to a human" "$out" "escalated to a human" - has "workflow: B. the unit-of-record law's breakers are named" "$out" "can be broken by: reassign-to-fraud, reassign-to-kyc" - lacks "workflow: and both reassignments are accepted" "$out" "unadmitted" - has "workflow: C. no case gets stuck — always still settleable" "$out" "holds settle-able" - has "workflow: and the assignee slot stays fillable" "$out" "holds assignee-fillable" -} two_phase_commit() { d="$here/two-phase-commit" @@ -234,109 +196,8 @@ two_phase_commit() { has "2pc: including the plain reachability one" "$cmp" "can-decide gained" } -access() { - echo "== Access & privilege (kernel-spec §3) ==" - echo " Q: is revocation always possible, or is some privilege permanent?" - out=$("$WRIT" check "$here/access/access.writ" --claims "$here/access/access.claims" 2>&1) - st=$? - printf '%s\n' "$out" | sed 's/^/ | /' - exit_is "access: check reports findings" "$st" 1 - has "access: A. the root-tracing law's breaker is named" "$out" "can be broken by: delegate-alice-to-mallory" - lacks "access: and the delegation is accepted" "$out" "unadmitted" - has "access: B. revocation is NOT always possible — a latch" "$out" "fails revocation-possible" - near "access: the break-glass grant is the latching move" "$out" "fails revocation-possible" "grant-breakglass-admin" - near "access: it strands the state with mallory admin forever" "$out" "fails revocation-possible" "mallory.role=admin" - has "access: C. the admins query is answered" "$out" "admins (at state" -} -gotha() { - echo "== A claim about common ownership, put to the test ==" - echo " Q: \"once the means of production are held in common, no surplus is" - echo " disposed of by anyone who does not work them\" — does it survive?" - out=$("$WRIT" check "$here/gotha/gotha.writ" --claims "$here/gotha/gotha.claims" 2>&1) - st=$? - printf '%s\n' "$out" | sed 's/^/ | /' - exit_is "gotha: check reports findings" "$st" 1 - has "gotha: seven situations — the whole world of the claim" "$out" "states: 7" - has "gotha: A. the antecedent is reached: the mill DOES become common" "$out" \ - "holds expropriation-succeeds" - near "gotha: expropriation, then distribution to the weavers" "$out" \ - "holds expropriation-succeeds" "1. expropriate" - has "gotha: B. and the claim is REFUTED" "$out" "fails no-exploitation" - near "gotha: the falsifier begins with the expropriation itself" "$out" \ - "fails no-exploitation" "1. expropriate" - near "gotha: someone must administer the deductions" "$out" \ - "fails no-exploitation" "2. appoint-board" - near "gotha: and Gotha's own second deduction is what breaks it" "$out" \ - "fails no-exploitation" "3. fund-administration" - has "gotha: C. but the condition is not a trap — recall still works" "$out" \ - "holds exploitation-endable" - has "gotha: D. the programme's own law is broken before AND after" "$out" \ - "violated in 3 reachable situations" - has "gotha: by the three moves that write the surplus" "$out" \ - "can be broken by: expropriate, distribute, fund-administration" - lacks "gotha: all three acknowledged — nothing unadmitted" "$out" "unadmitted" - has "gotha: E. and the non-producers are named" "$out" "non-producers (at state" - - echo " Q: does the rules engine reach the same three verdicts?" - xc=$(WRIT="$WRIT" sh "$here/gotha/cross-check.sh" 2>&1) - xst=$? - printf '%s\n' "$xc" | sed 's/^/ | /' - exit_is "gotha: check and derive agree on all three" "$xst" 0 - has "gotha: the refutation survives a second implementation" "$xc" \ - "no-exploitation (never): 1 rows" -} -calculation() { - echo "== The calculation problem — one allotment of steel, three plants ==" - echo " Q: two economies differing in ONE guard, asked the SAME questions —" - echo " which guarantees does the difference cost?" - - echo " 1/2: prices — the ask must be backed by the plant's own need" - mkt=$("$WRIT" check "$here/calculation/market.writ" --claims "$here/calculation/market.claims" 2>&1) - mst=$? - printf '%s\n' "$mkt" | sed 's/^/ | /' - exit_is "calculation: the priced model is clean" "$mst" 0 - has "calculation: A. the steel can reach a plant that needs it" "$mkt" "holds need-can-be-met" - near "calculation: and writ prints the route it takes" "$mkt" "holds need-can-be-met" "allocate-clinic" - has "calculation: it is never built where it is not needed" "$mkt" "holds no-waste" - has "calculation: and that stays true from every situation" "$mkt" "holds need-always-still-meetable" - lacks "calculation: the model's own law is never violated" "$mkt" "violated in" - lacks "calculation: and nothing is unadmitted" "$mkt" "unadmitted" - - echo " 2/2: the plan — the same file with that one conjunct repealed" - pln=$("$WRIT" check "$here/calculation/planned.writ" --claims "$here/calculation/market.claims" 2>&1) - pst=$? - printf '%s\n' "$pln" | sed 's/^/ | /' - exit_is "calculation: the planned model reports findings" "$pst" 1 - has "calculation: B. the plan is NOT incapable — it can still get it right" "$pln" "holds need-can-be-met" - has "calculation: but waste is permitted by its rules" "$pln" "fails no-waste" - near "calculation: a costless request is what buys the steel" "$pln" "fails no-waste" "ask-monument-high" - near "calculation: and the monument gets it" "$pln" "fails no-waste" "allocate-monument" - has "calculation: C. and the waste is terminal, not a delay" "$pln" "fails need-always-still-meetable" - near "calculation: steel welded into a statue is steel no longer" "$pln" "fails need-always-still-meetable" "steel.state=built" - has "calculation: D. it violates the law both models declare" "$pln" "violated in 24 reachable situations" - has "calculation: and has no procedure for what requests omit" "$pln" "gaps: 1" - has "calculation: which is written down as a gap, not invented" "$pln" "no request carries" - lacks "calculation: the same nine acknowledgments serve both models" "$pln" "unadmitted" - - echo " Q: what does the repeal cost, as one command?" - cmp=$("$WRIT" compare "$here/calculation/market.writ" "$here/calculation/planned.writ" 2>&1) - cst=$? - printf '%s\n' "$cmp" | sed 's/^/ | /' - exit_is "calculation: compare reports a loss" "$cst" 1 - has "calculation: E. no-waste is LOST" "$cmp" "no-waste LOST" - has "calculation: and so is the recovery from waste" "$cmp" "need-always-still-meetable LOST" - has "calculation: while the ability to get it right is preserved" "$cmp" "need-can-be-met preserved" - - echo " Q: does the rules engine reach the same verdicts, for BOTH models?" - xc=$(WRIT="$WRIT" sh "$here/calculation/cross-check.sh" 2>&1) - xst=$? - printf '%s\n' "$xc" | sed 's/^/ | /' - exit_is "calculation: check and derive agree on all six" "$xst" 0 - has "calculation: including the plan's failing never" "$xc" \ - "planned/no-waste (never): 8 rows" -} arch() { echo "== System architecture from a component bank ==" @@ -380,17 +241,17 @@ arch() { control() { echo "== writ control — a model's dynamics as data (kernel-spec §17) ==" echo " Q: can we export the move list and re-use it with the same machinery?" - out=$("$WRIT" control "$here/oversight/oversight.writ" 2>&1) + out=$("$WRIT" control "$here/payments/payments.writ" 2>&1) st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "control: emits cleanly" "$st" 0 has "control: it is an instance of the stdlib quiver schema" "$out" "-control quiver" - has "control: an edge per transition — capture-watchdog" "$out" "capture-watchdog" - has "control: ... and assign-judge" "$out" "assign-judge" + has "control: an edge per transition — capture-again" "$out" "capture-again" + has "control: ... and void-uncaptured" "$out" "void-uncaptured" # Prove the emitted quiver is real data: wrap it as a model and re-check it. tmp=$(mktemp -d) printf '%s\n' "$out" >"$tmp/ctrl.writ" - printf '(load "ctrl.writ")\n(use quiver)\n(initial oversight-control)\n' >"$tmp/wrap.writ" + printf '(load "ctrl.writ")\n(use quiver)\n(initial payments-control)\n' >"$tmp/wrap.writ" if (cd "$tmp" && "$WRIT" check wrap.writ >/dev/null 2>&1); then ok "control: the emitted quiver re-parses and builds" else bad "control: the emitted quiver did not re-parse"; fi @@ -404,22 +265,23 @@ gitcompare() { printf ' [skip] writ compare --git needs git (not installed here)\n' return 0 fi - # A self-contained history: commit the law, then commit the repeal, in a - # throwaway repo — so the demo is deterministic and needs no shared history. + # A self-contained history: commit the keyed payment flow, then commit the + # shortcut that drops the idempotency key, in a throwaway repo — so the demo + # is deterministic and needs no shared history. tmp=$(mktemp -d) - cp "$here/oversight/oversight.writ" "$tmp/law.writ" - cp "$here/oversight/oversight.claims" "$tmp/law.claims" - (cd "$tmp" && git init -q && git add law.writ law.claims && - git -c user.email=t@t -c user.name=t commit -qm "v1: with restoration") >/dev/null 2>&1 - cp "$here/oversight/oversight-repeal.writ" "$tmp/law.writ" - (cd "$tmp" && git add law.writ && - git -c user.email=t@t -c user.name=t commit -qm "amendment: repeal restoration") >/dev/null 2>&1 - out=$(cd "$tmp" && "$WRIT" compare --git HEAD~1 HEAD law.writ 2>&1) + d="$here/payments" + cp "$d/payments.writ" "$d/payments.claims" "$d/payments.lib.writ" "$tmp/" + (cd "$tmp" && git init -q && git add . && + git -c user.email=t@t -c user.name=t commit -qm "v1: with the idempotency key") >/dev/null 2>&1 + cp "$d/payments-shortcut.writ" "$tmp/payments.writ" + (cd "$tmp" && git add payments.writ && + git -c user.email=t@t -c user.name=t commit -qm "amendment: drop the key") >/dev/null 2>&1 + out=$(cd "$tmp" && "$WRIT" compare --git HEAD~1 HEAD payments.writ 2>&1) st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "git-compare: the amendment loses a guarantee" "$st" 1 - has "git-compare: accountability is LOST across the two commits" "$out" "accountability LOST" - has "git-compare: same-agency is preserved" "$out" "same-agency preserved" + 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" rm -rf "$tmp" } @@ -431,19 +293,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The twenty-one scenarios this script walks by convention, and their 60 - # properties. `calculation/` and `gotha/` are not among them: each carries its - # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the twenty-one fails this line, which is the point of it — + # 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 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, and this line is where each of those - # had to be said out loud. - has "cross-check: all 60 properties of the twenty-one scenarios were considered" \ - "$out" "considered 60 properties: 58 compared, 2 not compared" - # Two of the 60 are not compared, and the count above is the only place that + # 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 # 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. @@ -452,9 +313,9 @@ crosscheck() { has "cross-check: A. a possible is its satisfying set — non-empty holds" \ "$out" "river/solvable possible: satisfying set of" has "cross-check: B. a live is its COUNTEREXAMPLE set — empty holds" \ - "$out" "workflow/settle-able live: counterexample set of 0" + "$out" "payments/always-terminal live: counterexample set of 0" has "cross-check: and a failing live names its witnesses" \ - "$out" "access/revocation-possible live: counterexample set of 4" + "$out" "deployment/can-roll-back live: counterexample set of 4" # `arch` brought the repository's first two `never` properties, so this # branch — which announced itself as unexercised on every prior run — is now # measured. If it ever reads "unexercised" again, a scenario went missing. @@ -887,7 +748,7 @@ config_space() { # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails 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 control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):" diff --git a/workflow/workflow.claims b/workflow/workflow.claims deleted file mode 100644 index 61683a0..0000000 --- a/workflow/workflow.claims +++ /dev/null @@ -1,25 +0,0 @@ -; The questions about the regulated workflow (§16), kept beside the model. - -; Can a case get stuck — reachable, but never settleable? `live` asks whether a -; settled docket is still reachable from EVERY reachable situation. Even where -; the assignee slot is empty (the escalation state), the case can still be -; assigned and then settled, so the guarantee holds: no reachable case is ever -; stranded. -(property settle-able - "the case can always still be settled" - (live (is claim-1.stage settled))) - -; May the assignee slot be empty here — and must it always be fillable? The slot -; is vacatable and starts empty; `live (defined …)` confirms it can always be -; (re)filled from any reachable situation. -(property assignee-fillable - "the assignee slot can always still be filled" - (live (defined claim-1.assignee))) - -; Which reassignment moves can break the unit-of-record law? `writ check` reports -; officer-in-unit can be broken by reassign-to-fraud and reassign-to-kyc (both -; write case.officer, an arrow the law's route traverses). We acknowledge both, -; recording ownership (§16.3). settle / assign / escalate touch none of the -; law's arrows, so accepting them would be reported `stale`. -(accept reassign-to-fraud officer-in-unit) -(accept reassign-to-kyc officer-in-unit) diff --git a/workflow/workflow.rules b/workflow/workflow.rules deleted file mode 100644 index b5dec45..0000000 --- a/workflow/workflow.rules +++ /dev/null @@ -1,36 +0,0 @@ -; The regulated workflow's two properties, re-asked as derivations (extension -; §2) for `modality-cross-check.sh`. Both are `live`, so BOTH relations below -; are COUNTEREXAMPLE SETS and both are expected to be EMPTY. -; -; Why counterexamples. `live F` is AG EF F — a statement about every reachable -; situation. Stratified Datalog cannot assert a universal positively without a -; nullary relation, which extension §3 rejects outright, so the question is -; asked in its refutable form instead: derive the situations that WITNESS a -; failure. Empty answer set ⟺ the property holds. The refutable form is also -; the useful one — a failure hands `writ derive --why` a concrete stranded -; situation to explain, where a yes/no flag would hand it nothing. -; -; A green cross-check on this file therefore means "no case is ever stranded" -; and "the assignee slot can always be refilled". These two, with -; oversight/accountability, are also the repo's inversion detectors: they are -; the `live` properties that HOLD, so their counterexample set is empty while -; their satisfying set is not, and re-pointing `settle-able` at -; `can-still-settle` flips the derived verdict to `fails` against a `writ check` -; that says `holds`. (Where a `live` property fails — river/no-blunders, -; access/revocation-possible — both sets are non-empty and an inversion there -; is invisible to the oracle. Hence these comments.) - -(load "ct.rules") - -; Can a case get stuck? The escalation gap is a non-F terminal for both -; implementations: a gap edge has no successor, so neither `edge` nor -; `Space.bwd_reach` traverses it. -(satisfies settled (is claim-1.stage settled)) -(can-reach can-still-settle settled) -(trapped settle-able can-still-settle) - -; May the vacatable assignee slot always be refilled? The same three lines -; against a different guard, which is the whole reason they are forms. -(satisfies assigned (defined claim-1.assignee)) -(can-reach can-still-assign assigned) -(trapped assignee-fillable can-still-assign) diff --git a/workflow/workflow.writ b/workflow/workflow.writ deleted file mode 100644 index 7591834..0000000 --- a/workflow/workflow.writ +++ /dev/null @@ -1,70 +0,0 @@ -; A regulated workflow — a KYC / claims operation (§3, "Regulated workflow"). -; -; A case is wired (fixed arrows) to a reviewing officer and to its unit of -; record. It also carries a mutable APPROVING officer and a vacatable assignee -; slot. The law `officer-in-unit` demands the approving officer belong to the -; case's unit of record — two routes case → unit-t that must agree. A -; reassignment to an officer in another unit breaks that law. The automated -; process settles a case that has an assignee; where there is no assignee it -; ends at an escalation `gap` — the boundary where a human takes over. - -(load "stdlib.writ") ; `=` is a stdlib form (§8.6); there is no implicit prelude - -(schema workflow - (type unit-t (kyc fraud)) - (type stage-t (screening settled)) - (type agent - (arrow unit (to unit-t) fixed)) ; each officer belongs to one unit - (type case - (arrow unit (to unit-t) fixed) ; the unit of record (wired) - (arrow reviewer (to agent) fixed) ; the wired reviewing officer - (arrow officer (to agent)) ; the approving officer (reassignable) - (arrow stage (to stage-t)) - (maybe assignee agent)) ; may be empty - ; the approving officer must belong to the case's unit of record: - (equation officer-in-unit - (= case.officer.unit case.unit))) - -(instance intake workflow - (agent ann (unit kyc)) - (agent bob (unit fraud)) - (case claim-1 (unit kyc) - (reviewer ann) - (officer ann) - (stage screening) - (assignee vacant))) - -(use workflow) -(initial intake) - -; Reassignment — the move that can break officer-in-unit: bob is in fraud, the -; case's unit of record is kyc, so approving via bob violates the law. -(transition reassign-to-fraud - (when (is claim-1.officer ann)) - (do (set claim-1.officer bob))) - -(transition reassign-to-kyc - (when (is claim-1.officer bob)) - (do (set claim-1.officer ann))) - -; Staffing the vacatable assignee slot. -(transition assign - (when (not (defined claim-1.assignee))) - (do (set claim-1.assignee ann))) - -(transition withdraw-assignee - (when (defined claim-1.assignee)) - (do (vacate claim-1.assignee))) - -; The automated close: a case with an assignee settles. -(transition settle - (when (and (is claim-1.stage screening) - (defined claim-1.assignee))) - (do (set claim-1.stage settled))) - -; The escalation boundary: no assignee, so the automated process cannot settle -; on its own — it ends here and a human takes over. -(transition escalate - (when (and (is claim-1.stage screening) - (not (defined claim-1.assignee)))) - (do (gap "escalated to a human: no assignee, automated settling ends here")))