From 468a25b8627da68c80a432bb4c448c7a9e8df712 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:33:27 +0300 Subject: [PATCH] config-space: the flag matrix exhausted, and the order that breaks it Four flags and two modes, 64 combinations; the guarded operations reach exactly the 21 the product's rules allow. The shortcut's disable-sso checks authentication but not the shard latch: enable-legacy-auth, shard, disable-sso reaches a forbidden state, and only in that order. --fiber cfg.region shows the EU deployment is safe from it by accident. v2 adds a billing flag whose enable turns tenancy on: compare reports never-unsafe LOST in one move, and check reports the new operation unadmitted. final-phase names exactly the sharded configurations. Cross-check 56 -> 60 properties (58 compared); 329 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + config-space/README.md | 170 ++++++++++++++++++++++++ config-space/config-space-shortcut.writ | 95 +++++++++++++ config-space/config-space-v2.writ | 106 +++++++++++++++ config-space/config-space.claims | 35 +++++ config-space/config-space.lib.writ | 10 ++ config-space/config-space.rules | 29 ++++ config-space/config-space.writ | 94 +++++++++++++ docker-compose.yml | 6 + modality-cross-check.sh | 2 +- run-tests.sh | 63 +++++++-- 11 files changed, 601 insertions(+), 10 deletions(-) create mode 100644 config-space/README.md create mode 100644 config-space/config-space-shortcut.writ create mode 100644 config-space/config-space-v2.writ create mode 100644 config-space/config-space.claims create mode 100644 config-space/config-space.lib.writ create mode 100644 config-space/config-space.rules create mode 100644 config-space/config-space.writ diff --git a/README.md b/README.md index c964a0e..c62ee6e 100644 --- a/README.md +++ b/README.md @@ -57,6 +57,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. | | [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. | | [`payments/`](payments/) | Can a lost reply and a retry charge a customer twice? | Without an idempotency key, in six steps, each correct where it stood. The key also stops a late capture beating a cancellation. | +| [`config-space/`](config-space/) | Can the admin operations reach a flag combination the product forbids? | All 64 combinations walked: only if steps are done in one order. A release adding a flag loses the guarantee in one move. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/config-space/README.md b/config-space/README.md new file mode 100644 index 0000000..b6a143f --- /dev/null +++ b/config-space/README.md @@ -0,0 +1,170 @@ +# The configuration space: every combination, not a sample + +A product deployment has feature flags and modes: SSO on or off, legacy +password login, multi-tenancy, an audit log, a region, a database that is +single or sharded. Some combinations are forbidden by the product's own +rules, and the admin operations that change the configuration are supposed to +refuse the steps that would reach them. + +The usual check is a test matrix that samples combinations. Here there are +four flags and two two-valued modes: 2⁶ = 64 combinations. That is the whole +space, and writ walks all of it. The interesting finding is not a forbidden +combination a sample missed. It is one reached only by doing allowed steps in +a particular **order**, which no test of single configurations or single +steps can produce. + +## The model + +[`config-space.writ`](config-space.writ) has one `config` entity, `cfg`, and +four rules as laws: + +| rule | in words | +| --- | --- | +| `audit-when-multi-tenant` | tenants' actions are audited | +| `no-legacy-in-eu` | password login is not offered in the EU deployment | +| `some-auth` | somebody can log in: SSO or legacy auth is on | +| `sharded-needs-sso` | the sharded database routes on the SSO tenant id | + +Each admin operation (`enable-sso`, `disable-sso`, `enable-legacy-auth`, …, +`move-to-eu`, `move-to-us`, `shard`) checks in its `when` the rules it could +break. Writing those guards is the work: each is a rule read as a +precondition. `shard` is one-way, because sharding migrates the data and +nothing undoes it. + +[`config-space-shortcut.writ`](config-space-shortcut.writ) leaves out one +condition. `disable-sso` checks that somebody can still log in, but not that +the database is unsharded. The check that remains is the obvious one: SSO is +an authentication flag, and its guard checks authentication. The one that is +gone belongs to another subsystem, and to a mode that changes once in the +product's life. + +## What writ answers + +The questions are in [`config-space.claims`](config-space.claims). The guarded +operations, exit 0: + +``` +states: 21 edges: 67 +… +holds fully-featured + "a safe configuration with tenants, SSO and a sharded database exists" +holds never-unsafe + "no configuration the product forbids is ever reached" +holds recoverable +holds can-leave-eu +``` + +21 of the 64 combinations are reachable from the starting configuration, and +the four rules allow exactly 21. So the guarded operations reach every allowed +configuration and nothing else. The guards forbid nothing the rules allow, +and admit nothing they forbid. + +The shortcut, exit 1: + +``` +equation sharded-needs-sso + … + violated in 3 reachable situations witness: 1. enable-legacy-auth 2. shard 3. disable-sso → #15 +… +fails never-unsafe + witness: 1. enable-legacy-auth → #1 cfg.legacy-auth: no → yes + 2. shard → #7 cfg.db-mode: single → sharded + 3. disable-sso → #15 cfg.sso: yes → no +holds recoverable +``` + +Each step is allowed, and the order is the finding. Turn SSO off first and +`shard` refuses, because it checks SSO. Shard first and `disable-sso` lets you +through, because it does not check the database. A test of `disable-sso` on a +single-database configuration passes. A test of `shard` without SSO is +refused. The failing path exists only in this sequence. + +`recoverable` still holds: `enable-sso` repairs it. So the shortcut never +traps anyone, which is why the bug would ship. The broken configuration is a +state production can sit in until someone notices the router failing. + +### Per region + +FR-10's fibers answer the same question once per value of a cell: + +```sh +writ check config-space-shortcut.writ --claims config-space.claims --fiber cfg.region +``` + +``` +fails never-unsafe + … + fiber cfg.region=us FAILS witness: 1. enable-legacy-auth 2. shard 3. disable-sso → #15 + fiber cfg.region=eu holds +``` + +Only the US deployment can reach it. The EU forbids legacy auth, and turning +it on is the first step of the route. So the EU deployment is safe from this +bug because of a rule about a different thing. That protection is +accidental, and the fiber line shows it. + +## A release that adds a flag + +[`config-space-v2.writ`](config-space-v2.writ) is the guarded model plus one +flag, `new-billing`. The new billing system bills per tenant, so its enable +operation also turns multi-tenancy on. It was reviewed as a billing change. + +```sh +writ compare config-space.writ config-space-v2.writ # exit 1 +``` + +``` +equations: audit-when-multi-tenant preserved + no-legacy-in-eu preserved + some-auth preserved + sharded-needs-sso preserved +properties: fully-featured preserved + never-unsafe LOST witness: 1. enable-new-billing + recoverable preserved + can-leave-eu preserved +``` + +One move: multi-tenancy on, audit log off, the first rule broken. A release +that adds a flag adds operations, and `compare` checks the operations, not +the flag. `writ check` on v2 says the same from the other side: + +``` +unadmitted enable-new-billing may break audit-when-multi-tenant +``` + +The claims file lists every operation the team has agreed can touch each +rule. A new one that can is reported until someone either guards it or signs +it off. + +## What the latch costs + +[`config-space.rules`](config-space.rules) asks, with no goal in mind, which +configurations are in the last phase, the ones that can never get back to an +earlier one: + +```sh +writ derive config-space.writ config-space.rules final-db +``` + +All nine rows say `sharded`. Every configuration on a single database can be +left and returned to, and every sharded one can only go to other sharded ones. +That is what one irreversible operation does to a configuration space: it +divides it in two, and a deployment crosses once. + +## What is not modelled + +Values, only members: a flag is on or off, a region is one of two. A flag +whose default differs by region would be a fixed arrow on the region, not a +cell. And every operation is available at any time to whoever administers the +deployment. Who may run which operation is the entitlement problems' subject +(`../entitlement-problems/`), and the two compose. + +## Run it + +```sh +writ check config-space.writ --claims config-space.claims # exit 0 +writ check config-space-shortcut.writ --claims config-space.claims --fiber cfg.region # exit 1 +writ compare config-space.writ config-space-v2.writ # exit 1 +``` + +`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`. diff --git a/config-space/config-space-shortcut.writ b/config-space/config-space-shortcut.writ new file mode 100644 index 0000000..742e4db --- /dev/null +++ b/config-space/config-space-shortcut.writ @@ -0,0 +1,95 @@ +; The same operations, with ONE CONDITION MISSING from one of them: turning +; SSO off checks that somebody can still log in, and not that the database is +; unsharded. +; +; The check that is there is the obvious one: SSO is an authentication flag, +; and its guard checks authentication. The one that is gone is about a +; different subsystem, the database, and a mode that only changes once. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) +) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off: check that somebody can still log in. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes))) ; <- db-mode single, gone + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) diff --git a/config-space/config-space-v2.writ b/config-space/config-space-v2.writ new file mode 100644 index 0000000..2172346 --- /dev/null +++ b/config-space/config-space-v2.writ @@ -0,0 +1,106 @@ +; Version 2: the guarded operations, plus ONE NEW FLAG. +; +; `new-billing` switches to a billing system that bills per tenant, so its +; enable operation also turns multi-tenancy on. Nothing about the old +; operations changes. +; +; `writ compare config-space.writ config-space-v2.writ` exits 1. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) + ; New in v2. + (arrow new-billing (to yn))) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single) (new-billing no))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off breaks two rules if done carelessly: nobody can log in, or +; the sharded database loses its routing key. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes) (is cfg.db-mode single))) + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) + +; ---- new in v2 ---- + +; The new billing system bills per tenant, so turning it on turns tenancy on. +; It was reviewed as a billing change. +(transition enable-new-billing + (when (is cfg.new-billing no)) + (do (set cfg.new-billing yes) (set cfg.multi-tenant yes))) +(transition disable-new-billing + (when (is cfg.new-billing yes)) + (do (set cfg.new-billing no))) diff --git a/config-space/config-space.claims b/config-space/config-space.claims new file mode 100644 index 0000000..48ac6f6 --- /dev/null +++ b/config-space/config-space.claims @@ -0,0 +1,35 @@ +; The questions, put to every version. + +(load "config-space.lib.writ") + +(property fully-featured + "a safe configuration with tenants, SSO and a sharded database exists" + (possible (and (is cfg.multi-tenant yes) (is cfg.sso yes) (is cfg.db-mode sharded) safe))) + +(property never-unsafe + "no configuration the product forbids is ever reached" + (never (not safe))) + +(property recoverable + "from every configuration, a safe one is still reachable" + (live safe)) + +(property can-leave-eu + "from every configuration, the deployment can still be moved to the US" + (live (is cfg.region us))) + +; ---- ownership ---- +; Every operation that writes a cell a rule reads. The guards are what keep +; the rules; a release that adds an operation adds a line here, or writ reports +; it as unadmitted. +(accept enable-multi-tenant audit-when-multi-tenant) +(accept disable-multi-tenant audit-when-multi-tenant) +(accept enable-audit-log audit-when-multi-tenant) +(accept disable-audit-log audit-when-multi-tenant) +(accept enable-legacy-auth no-legacy-in-eu some-auth) +(accept disable-legacy-auth no-legacy-in-eu some-auth) +(accept move-to-eu no-legacy-in-eu) +(accept move-to-us no-legacy-in-eu) +(accept enable-sso some-auth sharded-needs-sso) +(accept disable-sso some-auth sharded-needs-sso) +(accept shard sharded-needs-sso) diff --git a/config-space/config-space.lib.writ b/config-space/config-space.lib.writ new file mode 100644 index 0000000..cd8275b --- /dev/null +++ b/config-space/config-space.lib.writ @@ -0,0 +1,10 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +; The product's four rules, as one test: a configuration none of them forbids. +(form safe + (and (not (and (is cfg.multi-tenant yes) (is cfg.audit-log no))) + (not (and (is cfg.legacy-auth yes) (is cfg.region eu))) + (not (and (is cfg.sso no) (is cfg.legacy-auth no))) + (not (and (is cfg.db-mode sharded) (is cfg.sso no))))) diff --git a/config-space/config-space.rules b/config-space/config-space.rules new file mode 100644 index 0000000..c65677e --- /dev/null +++ b/config-space/config-space.rules @@ -0,0 +1,29 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "config-space.lib.writ") + +(satisfies fully-featured + (and (is cfg.multi-tenant yes) (is cfg.sso yes) (is cfg.db-mode sharded) safe)) + +(satisfies never-unsafe (not safe)) + +(satisfies is-safe safe) +(can-reach can-be-safe is-safe) +(trapped recoverable can-be-safe) + +(satisfies in-us (is cfg.region us)) +(can-reach can-get-to-us in-us) +(trapped can-leave-eu can-get-to-us) + +; ---- what the latch costs ---- +; `final-phase` (ct.rules §3): the configurations in the last phase, the ones +; that can never get back to an earlier one. Asked with no goal in mind. +; Projected onto the database mode, which is the cell that says why. +(relation final-db (Situation db-t)) +(rule (final-db S D) (final-phase S) (holds S (is cfg.db-mode D))) diff --git a/config-space/config-space.writ b/config-space/config-space.writ new file mode 100644 index 0000000..b269b2d --- /dev/null +++ b/config-space/config-space.writ @@ -0,0 +1,94 @@ +; A product's runtime configuration, and the admin operations that change it. +; +; Four feature flags, a region and a database mode: 64 combinations. Four of +; the product's rules forbid some of them. Each admin operation checks the +; rules it could break before it runs. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "config-space.lib.writ") + +(schema config-space + + (type yn (no yes)) + (type region-t (eu us)) + (type db-t (single sharded)) + + ; One product deployment's runtime configuration. Four flags and two modes: + ; 2 × 2 × 2 × 2 × 2 × 2 = 64 combinations, every one of them a cell value + ; writ can enumerate. + (type config + (arrow sso (to yn)) + (arrow legacy-auth (to yn)) + (arrow multi-tenant (to yn)) + (arrow audit-log (to yn)) + (arrow region (to region-t)) + (arrow db-mode (to db-t)) +) + + ; ---- the product's rules ---- + + ; Tenants' actions are audited. + (equation audit-when-multi-tenant + (not (and (is config.multi-tenant yes) (is config.audit-log no)))) + ; Password login is not offered in the EU deployment. + (equation no-legacy-in-eu + (not (and (is config.legacy-auth yes) (is config.region eu)))) + ; Somebody can log in. + (equation some-auth + (not (and (is config.sso no) (is config.legacy-auth no)))) + ; The sharded database routes on the SSO tenant id. + (equation sharded-needs-sso + (not (and (is config.db-mode sharded) (is config.sso no))))) + +(instance start config-space + (config cfg (sso yes) (legacy-auth no) (multi-tenant no) (audit-log no) + (region us) (db-mode single))) + +(use config-space) +(initial start) + +; ---- the admin operations ---- +; Each one checks, in its `when`, the rules it could break. Writing those +; guards is the work: each is a rule read as a precondition. + +(transition enable-sso (when (is cfg.sso no)) (do (set cfg.sso yes))) +; Turning SSO off breaks two rules if done carelessly: nobody can log in, or +; the sharded database loses its routing key. +(transition disable-sso + (when (and (is cfg.sso yes) (is cfg.legacy-auth yes) (is cfg.db-mode single))) + (do (set cfg.sso no))) + +(transition enable-legacy-auth + (when (and (is cfg.legacy-auth no) (is cfg.region us))) + (do (set cfg.legacy-auth yes))) +(transition disable-legacy-auth + (when (and (is cfg.legacy-auth yes) (is cfg.sso yes))) + (do (set cfg.legacy-auth no))) + +(transition enable-multi-tenant + (when (and (is cfg.multi-tenant no) (is cfg.audit-log yes))) + (do (set cfg.multi-tenant yes))) +(transition disable-multi-tenant + (when (is cfg.multi-tenant yes)) + (do (set cfg.multi-tenant no))) + +(transition enable-audit-log + (when (is cfg.audit-log no)) + (do (set cfg.audit-log yes))) +(transition disable-audit-log + (when (and (is cfg.audit-log yes) (is cfg.multi-tenant no))) + (do (set cfg.audit-log no))) + +(transition move-to-eu + (when (and (is cfg.region us) (is cfg.legacy-auth no))) + (do (set cfg.region eu))) +(transition move-to-us + (when (is cfg.region eu)) + (do (set cfg.region us))) + +; Sharding migrates the data. There is no unsharding. +(transition shard + (when (and (is cfg.db-mode single) (is cfg.sso yes))) + (do (set cfg.db-mode sharded))) diff --git a/docker-compose.yml b/docker-compose.yml index c5c14eb..632380d 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -101,6 +101,12 @@ services: image: writ-problems command: ["payments"] + # Configuration space: the flag matrix exhausted, and the order that breaks it. + config-space: + build: . + image: writ-problems + command: ["config_space"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/modality-cross-check.sh b/modality-cross-check.sh index ce0471d..d4a05fb 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments config-space" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index f90d174..0af5247 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,19 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The twenty scenarios this script walks by convention, and their 56 + # The twenty-one scenarios this script walks by convention, and their 60 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the twenty fails this line, which is the point of it — + # property to any of the twenty-one fails this line, which is the point of it — # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, # 26 -> 31 with two-phase-commit, 31 -> 41 with the three # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, 52 -> 56 with - # payments, and this line is where each of those had to be said out loud. - has "cross-check: all 56 properties of the twenty scenarios were considered" \ - "$out" "considered 56 properties: 54 compared, 2 not compared" - # Two of the 56 are not compared, and the count above is the only place that + # payments, 56 -> 60 with config-space, and this line is where each of those + # had to be said out loud. + has "cross-check: all 60 properties of the twenty-one scenarios were considered" \ + "$out" "considered 60 properties: 58 compared, 2 not compared" + # Two of the 60 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +460,10 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval, agent-guardrails and deployment one each, payments two. + # expense-approval, agent-guardrails, deployment and config-space one each, + # payments two. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 12 properties compared" + "never: 13 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -840,9 +842,52 @@ payments() { has "payments: G. double charges hide in orders that settled and shipped" "$dv" "settled yes" } +config_space() { + d="$here/config-space" + c="$d/config-space.claims" + echo "== The configuration space — every combination, not a sample ==" + echo " Q: can the admin operations reach a combination the product forbids?" + out=$("$WRIT" check "$d/config-space.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "config-space: the guarded operations are clean" "$st" 0 + has "config-space: A. 21 of the 64 combinations are reachable" "$out" "states: 21" + has "config-space: B. a fully-featured safe configuration exists" "$out" "holds fully-featured" + has "config-space: C. none the product forbids" "$out" "holds never-unsafe" + lacks "config-space: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/config-space-shortcut.writ" --claims "$c" --fiber cfg.region 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "config-space: one forgotten check is refused" "$sst" 1 + # The order finding: every step is allowed, and only this order gets there — + # turning SSO off first would block the shard. + has "config-space: D. the forbidden state, in one order of three allowed steps" "$sc" \ + "violated in 3 reachable situations witness: 1. enable-legacy-auth 2. shard 3. disable-sso" + has "config-space: E. yet every configuration can still be made safe" "$sc" "holds recoverable" + # FR-10's fibers: the same question per region. Legacy auth is forbidden in + # the EU, and it is the first step of the route. + has "config-space: F. only the US deployment can reach it" "$sc" "fiber cfg.region=us FAILS" + has "config-space: the EU one cannot" "$sc" "fiber cfg.region=eu holds" + + cmp=$("$WRIT" compare "$d/config-space.writ" "$d/config-space-v2.writ" 2>&1) + cst=$? + printf '%s\n' "$cmp" | sed 's/^/ | /' + exit_is "config-space: compare refuses the release that adds a flag" "$cst" 1 + has "config-space: G. the new flag reaches a forbidden state in one move" "$cmp" \ + "never-unsafe LOST witness: 1. enable-new-billing" + v2=$("$WRIT" check "$d/config-space-v2.writ" --claims "$c" 2>&1) + has "config-space: an operation the claims never acknowledged" "$v2" \ + "unadmitted enable-new-billing may break audit-when-multi-tenant" + + dv=$("$WRIT" derive "$d/config-space.writ" "$d/config-space.rules" final-db 2>&1) + has "config-space: H. the last phase is the sharded configurations" "$dv" "final-db (9 rows)" + lacks "config-space: and only those" "$dv" "single" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments config_space control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):"