diff --git a/agent-guardrails/README.md b/agent-guardrails/README.md index b551dcb..f34dcbf 100644 --- a/agent-guardrails/README.md +++ b/agent-guardrails/README.md @@ -144,12 +144,13 @@ certified: every answer re-derived from the model (writ-cert) ``` `n/a` means the question names something the model no longer has, so it was -not answered. **`writ check` exits 0 on this file.** No property failed, -because the one that would have was taken away. A harness that gates on that -exit code has just been talked out of its question. +not answered. No property failed, because the one that would have was taken +away. That is why `writ check` treats an `n/a` as a finding and **exits 1** on +this file: a gate that reads the exit status cannot be talked out of its +question. (Earlier versions of writ exited 0 here. This scenario is how that +was found.) -So treat `n/a` as a failure, and gate on `compare` against the last version -the human approved, which refuses it: +`compare` against the last version the human approved says what was taken: ```sh writ compare agent-guardrails.writ attempt-forget-out.writ # exit 1 @@ -166,7 +167,8 @@ properties: useful preserved writ's MCP server already enforces both halves. It reads `.claims` from the human's directory whatever path the agent passes, and it reports what each edit lost, `n/a` included (see writ's `docs/mcp.md`). From the command line, -`--json` carries `"verdict": "n/a"` for a script to refuse. +`check` exits 1 on an `n/a`, and `--json` carries `"verdict": "n/a"` for a +script that wants to say why. ## What to take away @@ -185,7 +187,7 @@ give the secret the places it can come from, and write the policy as ```sh writ check agent-guardrails.writ --claims agent-guardrails.claims # exit 0 writ compare agent-guardrails.writ agent-guardrails-v2.writ # exit 1 -writ check attempt-forget-out.writ --claims agent-guardrails.claims # exit 0, and two n/a +writ check attempt-forget-out.writ --claims agent-guardrails.claims # exit 1: two n/a writ compare agent-guardrails.writ attempt-forget-out.writ # exit 1 ``` diff --git a/db-migration-problems/README.md b/db-migration-problems/README.md index c9f4b50..ee676d2 100644 --- a/db-migration-problems/README.md +++ b/db-migration-problems/README.md @@ -33,10 +33,11 @@ What all six share: of the six (`add-a-required-column`, 3 moves against 5; `rename-a-column`, 8 against 9) and the same length in the other four. There it does not skip a step: it allows the steps in an order the safe plan forbids. -- **`writ compare` is the wrong gate.** Both files of each pair declare the - same rules and ask the same questions, so compare reports everything - preserved. The shortcut breaks a rule rather than dropping one, and that is - what `check` finds. +- **Both gates catch it.** The shortcut breaks a rule rather than dropping + one. `check` reports the violation, and `writ compare` against the safe + plan reports that rule `LOST` with the same route, since a rule declared in + both but broken in one is a guarantee lost. (Before writ counted that, compare + read "preserved" here, and these READMEs said to gate on `check`.) From any of the directories (here, `drop-a-column/`): @@ -52,7 +53,6 @@ carry over unchanged. What `writ sql` does with the newer steps is recorded where it matters: `CHECK … IN` becomes an enumerated type (`change-an-enum/`), `REFERENCES` -becomes an arrow (`split-a-table/`), and `NOT VALID` is read as an ordinary -foreign key while `VALIDATE CONSTRAINT` is declined (`add-a-foreign-key/`). -A constraint's validation state is not part of a schema, so the models carry -it themselves. +becomes an arrow (`split-a-table/`), and `NOT VALID` and `VALIDATE CONSTRAINT` +are both declined, each saying why (`add-a-foreign-key/`). A constraint's +validation state is not part of a schema, so the models carry it themselves. diff --git a/db-migration-problems/add-a-foreign-key/README.md b/db-migration-problems/add-a-foreign-key/README.md index 4383f92..e871b90 100644 --- a/db-migration-problems/add-a-foreign-key/README.md +++ b/db-migration-problems/add-a-foreign-key/README.md @@ -20,15 +20,24 @@ The SQL is [`01-before.sql`](01-before.sql) (order `o2` points at customer `c9`, who does not exist), [`02-add-not-valid.sql`](02-add-not-valid.sql) and [`03-validate.sql`](03-validate.sql). -`writ sql` reads a foreign key's presence, not its validation state, and the -two `ALTER` statements show the difference: - -- `ADD CONSTRAINT … NOT VALID` is read as an ordinary foreign key, - `(fk customer-id customers)`. The output is the same with or without - `NOT VALID`, and `--strict` accepts it. The orphan row `o2 → c9` in that - file loads without complaint. -- `VALIDATE CONSTRAINT` is declined under `--strict`: "ALTER TABLE that adds - no constraint". +`writ sql` reads a foreign key's presence, not its validation state, and says +so for both `ALTER` statements: + +- `ADD CONSTRAINT … NOT VALID`: the key is read, `(fk customer-id customers)`, + and the clause is declined, because the model would otherwise claim the key + for rows the database never checked, like the orphan `o2 → c9` in that + file: + + ``` + declined: + 19: NOT VALID — the constraint is read, but rows already present are not checked by it, and writ reads it as holding for every row + ``` + + It is the one decline that makes a model stricter than the database rather + than laxer, which is why `--strict` fails on it. (Earlier versions of writ + dropped the clause without a word. This scenario is how that was found.) +- `VALIDATE CONSTRAINT` is declined too: it "changes whether a constraint has + been checked against existing rows, which a schema does not record". So the model carries the state itself. [`add-a-foreign-key.writ`](add-a-foreign-key.writ) has the constraint as `none`, `not-valid` or `validated`; the orders table's diff --git a/db-migration-problems/add-a-required-column/README.md b/db-migration-problems/add-a-required-column/README.md index fdd7c36..e0da25e 100644 --- a/db-migration-problems/add-a-required-column/README.md +++ b/db-migration-problems/add-a-required-column/README.md @@ -91,8 +91,8 @@ through the broken situation. `required-needs-data`, the database's own check, is untouched; only the unwatched rule breaks. The shortcut is also faster, three steps against five, because it skips a deploy and a wait. -`writ compare` would report everything preserved, since the shortcut declares -the same rules. Gate on `check`. +`writ compare` against the safe plan agrees: `required-needs-every-writer` is +`LOST`, with the same three moves. The other two rules are preserved. ## What to take away diff --git a/db-migration-problems/drop-a-column/README.md b/db-migration-problems/drop-a-column/README.md index 1333a9b..0804faa 100644 --- a/db-migration-problems/drop-a-column/README.md +++ b/db-migration-problems/drop-a-column/README.md @@ -79,9 +79,14 @@ outage: start the deploy, drop the column, two moves. Both rules break, because the old release both reads and writes the column. The shortcut still completes and never gets stuck, so only the safety question catches it. -`writ compare` is the wrong gate here: the shortcut still declares both rules, -so compare reports everything preserved. It breaks a rule rather than dropping -one, and that is what `check` finds. +`writ compare drop-a-column.writ drop-a-column-shortcut.writ` agrees. The +shortcut still declares both rules, but it breaks them, so both are `LOST` +with the same two moves: + +``` +equations: read-of-existing LOST witness: 1. deploy-r2 2. drop-column + write-of-existing LOST witness: 1. deploy-r2 2. drop-column +``` ## What to take away diff --git a/db-migration-problems/rename-a-column/README.md b/db-migration-problems/rename-a-column/README.md index 7a50f52..f8f6921 100644 --- a/db-migration-problems/rename-a-column/README.md +++ b/db-migration-problems/rename-a-column/README.md @@ -117,21 +117,22 @@ moves reach one, and the last of them, `deploy-r3`, is the step at fault. The shortcut still completes, never gets stuck, and its route is eight steps instead of nine. -`writ compare` does not catch it, because the shortcut gives up none of the -guarantees it declares: +`writ compare` against the safe plan catches it too. The shortcut declares +the same rules, but one of them it now breaks, and a rule broken that the old +plan kept is a guarantee lost: ```console $ writ compare rename-a-column.writ rename-a-column-shortcut.writ equations: read-of-existing preserved write-of-existing preserved - read-of-filled preserved + read-of-filled LOST witness: 1. add-column 2. deploy-r2 3. settle 4. deploy-r3 read-implies-every-writer preserved properties: completes preserved no-dead-ends preserved ``` -`compare` asks which guarantees a version dropped; `check` asks whether it -keeps the ones it declares. Gate CI on `check`. +`check` says the shortcut breaks a rule; `compare` says which guarantee the +change from the safe plan gave up. Either is a gate for CI. ## What to take away diff --git a/entitlement-problems/README.md b/entitlement-problems/README.md index 442fdc2..643dbc8 100644 --- a/entitlement-problems/README.md +++ b/entitlement-problems/README.md @@ -34,11 +34,10 @@ What the three have in common: `writ compare` reports the difference between the two models of each pair as guarantees `LOST`, exit 1. In `scp-escalation/` that is the natural gate, -because the change *is* the difference: one administrative step added. One -caution: an equation that both files declare compares as `preserved` even when -one of them violates it (`separation` in `separation-of-duties/`), because -`compare` matches laws by declaration. Ask the safety question as a property -if `compare` is your gate. +because the change *is* the difference: one administrative step added. A law +both files declare and one of them breaks (`separation` in +`separation-of-duties/`) is reported `LOST` too, with the route to the +violation, so `compare` and `check` agree on every pair. From any of the directories (here, `separation-of-duties/`): diff --git a/expense-approval/README.md b/expense-approval/README.md index 9ce63d0..a0f88f7 100644 --- a/expense-approval/README.md +++ b/expense-approval/README.md @@ -133,18 +133,16 @@ writ compare expense-approval.writ expense-approval-shortcut.writ # exit 1 ``` equations: no-self-approval preserved finance-after-manager preserved - two-for-large preserved + two-for-large LOST witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay properties: payable preserved never-on-one-person LOST witness: 1. submit 2. bob-approves-as-manager 3. bob-approves-for-finance 4. pay always-settleable preserved settles preserved ``` -`two-for-large` reads `preserved` although the shortcut violates it. -`compare` matches laws by declaration, and both files declare it. The -property `never-on-one-person` asks the same thing as a question, and that -is what `compare` reports lost. If `compare` is your gate, ask your safety -rules as properties too. `check` catches both. +Both files declare `two-for-large`, and the shortcut breaks it, so `compare` +reports it lost with the same four steps as the property `never-on-one-person`, +which asks the same thing as a question. Either gate catches it. ## A question for whoever owns the process diff --git a/run-tests.sh b/run-tests.sh index 167d58a..31c0223 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -281,7 +281,9 @@ gitcompare() { printf '%s\n' "$out" | sed 's/^/ | /' exit_is "git-compare: the amendment loses a guarantee" "$st" 1 has "git-compare: never-double is LOST across the two commits" "$out" "never-double LOST" - has "git-compare: one-capture is preserved" "$out" "one-capture preserved" + # The law the amendment breaks, too: declared in both commits, violated in + # the second, so LOST with the same route. + has "git-compare: one-capture is LOST as well" "$out" "one-capture LOST" rm -rf "$tmp" } @@ -398,16 +400,18 @@ rename_a_column() { has "rename-a-column: D. yet it still finishes — faster, which is the trap" "$sc" "holds completes" has "rename-a-column: and it never strands you either" "$sc" "holds no-dead-ends" - echo " 4/4: the verb that does NOT catch it" + echo " 4/4: compare, against the safe plan" cm=$("$WRIT" compare "$here/db-migration-problems/rename-a-column/rename-a-column.writ" "$here/db-migration-problems/rename-a-column/rename-a-column-shortcut.writ" 2>&1) cst=$? printf '%s\n' "$cm" | sed 's/^/ | /' - exit_is "rename-a-column: compare is content" "$cst" 0 - has "rename-a-column: E. compare says the guarantees survived" "$cm" "preserved" - lacks "rename-a-column: nothing is reported LOST" "$cm" "LOST" - echo " — the shortcut declares the same laws and keeps the same" - echo " properties; what it loses is that one law it declares is now" - echo " VIOLATED. So the gate is \`check\`, not \`compare\`." + # The shortcut declares the same laws; what it loses is that one of them is + # now VIOLATED, and compare reports that as a guarantee lost, with the route + # check gives. (Before writ counted a newly violated law, this read + # "preserved" and the gate had to be check.) + exit_is "rename-a-column: compare refuses the shortcut too" "$cst" 1 + has "rename-a-column: E. the law it now breaks is LOST, with the route" "$cm" \ + "read-of-filled LOST witness: 1. add-column 2. deploy-r2 3. settle 4. deploy-r3" + has "rename-a-column: while the others survive" "$cm" "read-of-existing preserved" } drop_a_column() { @@ -577,9 +581,8 @@ expense_approval() { cmp=$("$WRIT" compare "$d/expense-approval.writ" "$d/expense-approval-shortcut.writ" 2>&1) has "expense-approval: F. compare reports the guarantee LOST" "$cmp" "never-on-one-person LOST" - # The law that breaks compares as preserved: compare matches laws by - # declaration, and both files declare it. The property is what catches it. - has "expense-approval: while the law it breaks compares as preserved" "$cmp" "two-for-large preserved" + # And the law it breaks: declared in both, violated in the shortcut, LOST. + has "expense-approval: and so is the law it breaks" "$cmp" "two-for-large LOST" dv=$("$WRIT" derive "$d/expense-approval-shortcut.writ" "$d/expense-approval.rules" paid-by 2>&1) has "expense-approval: G. derive lists who signed each payment" "$dv" "13 bob bob" @@ -628,11 +631,10 @@ agent_guardrails() { ch=$("$WRIT" check "$d/attempt-forget-out.writ" --claims "$c" 2>&1) chst=$? - # The cheat: delete what the question reads. `check` answers n/a and EXITS 0 - # — asserted as it is, since a harness that gates on this exit code is the - # failure the README warns about. + # The cheat: delete what the question reads. `check` answers n/a — and an + # unanswered question is a finding, so it exits 1 rather than reading clean. has "agent-guardrails: F. deleting the record makes the question n/a" "$ch" "n/a no-unapproved-exfiltration" - exit_is "agent-guardrails: and check alone exits clean" "$chst" 0 + exit_is "agent-guardrails: and check refuses it" "$chst" 1 cc=$("$WRIT" compare "$d/agent-guardrails.writ" "$d/attempt-forget-out.writ" 2>&1) ccst=$? exit_is "agent-guardrails: G. compare against v1 refuses it" "$ccst" 1 @@ -841,17 +843,18 @@ add_a_foreign_key() { d="$here/db-migration-problems/add-a-foreign-key" echo "== Adding a foreign key, NOT VALID — the rows are spared, the code is not ==" echo " Q: NOT VALID skips the old rows. Does it make adding the key safe?" - # Recorded as found: writ sql reads NOT VALID as an ordinary foreign key — - # the output is the same with or without it, and --strict accepts it — - # while it declines VALIDATE CONSTRAINT. The model carries the state. - "$WRIT" sql "$d/02-add-not-valid.sql" --with-data --strict >/dev/null 2>&1 - exit_is "add-a-foreign-key: writ sql accepts NOT VALID, as a plain foreign key" "$?" 0 - has "add-a-foreign-key: reading it as an arrow" \ - "$("$WRIT" sql "$d/02-add-not-valid.sql" 2>/dev/null)" "(fk customer-id customers)" + # writ sql reads the constraint and declines NOT VALID — the model would + # otherwise claim it for rows the database never checked — and declines + # VALIDATE CONSTRAINT. The model carries the validation state itself. + nv=$("$WRIT" sql "$d/02-add-not-valid.sql" --with-data --strict 2>&1) + nvst=$? + exit_is "add-a-foreign-key: writ sql declines NOT VALID under --strict" "$nvst" 1 + has "add-a-foreign-key: saying what it means" "$nv" "NOT VALID — the constraint is read, but rows already" + has "add-a-foreign-key: and still reads the key as an arrow" "$nv" "(fk customer-id customers)" vs=$("$WRIT" sql "$d/03-validate.sql" --with-data --strict 2>&1) vst=$? - exit_is "add-a-foreign-key: and declines VALIDATE CONSTRAINT under --strict" "$vst" 1 - has "add-a-foreign-key: saying why" "$vs" "ALTER TABLE that adds no constraint" + exit_is "add-a-foreign-key: and declines VALIDATE CONSTRAINT" "$vst" 1 + has "add-a-foreign-key: saying why" "$vs" "VALIDATE CONSTRAINT — changes whether a constraint" ok_=$("$WRIT" check "$d/add-a-foreign-key.writ" --claims "$d/add-a-foreign-key.claims" 2>&1) ost=$?