follow writ#19: n/a is a finding, compare loses a broken law, NOT VALID declined

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
 ```
 

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.

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

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
 

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
 

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
 

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/`):
 

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
 

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=$?