diff --git a/README.md b/README.md index 77f132c..61b062e 100644 --- a/README.md +++ b/README.md @@ -49,9 +49,12 @@ 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. | +| [`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** @@ -59,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/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/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/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/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 41dfc88..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,56 @@ services: image: writ-problems command: ["jobshop_best"] - # Institutional architecture — laws, acknowledgments, and `writ compare` across an amendment. - oversight: + + + + # 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"] + + # Two approvals, one person: the independence check payment forgot. + expense-approval: + build: . + 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 rolling deploy: the health gate, and the rollback a migration removes. + deployment: build: . image: writ-problems - command: ["oversight"] + command: ["deployment"] - # A regulated workflow: a declared `gap` where the rules stop. - workflow: + # Payments: a lost reply, a retry, and the idempotency key. + payments: build: . image: writ-problems - command: ["workflow"] + command: ["payments"] - # Access and privilege, including a one-way latch. - access: + # Configuration space: the flag matrix exhausted, and the order that breaks it. + config-space: build: . image: writ-problems - command: ["access"] + command: ["config_space"] # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. 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/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/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 dce80fc..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" +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/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 53242dd..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,37 +293,45 @@ 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 - # 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 - # 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" \ + # 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, 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. + 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" 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. - # 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, and + # expense-approval, agent-guardrails, deployment and config-space one each, + # payments two. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 3 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: 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 + # 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" \ @@ -598,9 +468,287 @@ 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 " +} + +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" +} + +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" +} + +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" +} + +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" +} + +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 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")))