The specification does not collect failure names

`legalFailures` had no business in properties.lean. It returned a
`List String` — a diagnostic, useful when a sweep goes red — and I
defended it as a design principle when it is a runtime concern. The
specification says what `Legal` is. Reporting is the implementer's
problem, and the harness's.

  properties.lean   legalAt is the fold, directly:

                      catalogue.all fun l => match l.property with
                        | .state f => f now a && f now b
                        | .trans f => f now a b

  properties-check  failingNames, three lines, where debugging happens

What made this cheap is unchanged and is the actual portable part: each
entry carries its `name` as data, so anyone — Go, TypeScript, Verus, a
harness in this repo — can collect them in three lines. The
specification does not have to provide the facility to make the names
useful; it has to carry the names.

Everything builds; the sweeps pass; report and transReport still return
[] over the battery.

Author: claude

spec/02-abstract/properties.lean

@@ -1266,36 +1266,31 @@ def catalogue : List Named :=
 
 /-! ### The walk
 
-ONE fold, matching `Legal` in `04-theorems/system.lean`: take the
-catalogue, and apply each entry to whatever its constructor says it
-takes — a `.state` property to a state, a `.trans` property to the pair.
-There is no second notion and no lemma between them; the sweep evaluates
-this and `Legal` quantifies it.
-
-A `.state` entry is checked at BOTH endpoints of the pair. `Legal`
-applies it at every index of an infinite trace, where every state is
-some step's pre-state; a finite run has a last state that is nobody's
-pre-state, and checking both ends is what covers it without a special
-case. The redundancy is free — the initial state satisfies everything.
-
-Both endpoints are checked at the instant of the STEP, not at some later
-reading. That is stricter, not weaker: the two `_lte_now` entries are
-monotone in `now`, so passing at the earlier instant implies passing at
-the later one.
-
-Report by NAME. It is the same string in Lean, Go, TypeScript and Verus,
-so a violation means the same thing everywhere. -/
-
-def legalFailures (now : Nat) (a b : ServerState) : List String :=
-  catalogue.filterMap fun l =>
-    match l.property with
-    | .state f => if f now a && f now b then none else some l.name
-    | .trans f => if f now a b then none else some l.name
+ONE fold, and it is the definition `Legal` in `04-theorems/system.lean`
+quantifies: take the catalogue, apply each entry to whatever its
+constructor says it takes — a `.state` property to a state, a `.trans`
+property to the pair.
+
+A `.state` entry is checked at BOTH endpoints. `Legal` applies it at
+every index of an infinite trace, where every state is some step's
+pre-state; a finite run has a last state that is nobody's pre-state, and
+checking both ends covers it with no special case. Both at the STEP's
+instant, which is stricter rather than weaker — the two `_lte_now`
+entries are monotone in `now`.
+
+Each entry carries its `name`, and that is the portable part: an
+implementation reporting a violation reports the same string in Go,
+TypeScript or Verus. Collecting those names is the implementation's
+business — and the harness's, when something breaks. Not the
+specification's. -/
 
 def legalAt (now : Nat) (a b : ServerState) : Bool :=
-  (legalFailures now a b).isEmpty
+  catalogue.all fun l =>
+    match l.property with
+    | .state f => f now a && f now b
+    | .trans f => f now a b
 
-/-- The SAME fold, restricted to the `.state` half — `legalAt` with the
+/-- The same fold restricted to the `.state` half — `legalAt` with the
     `.trans` entries answering `true`. Not a second notion of legality:
     it is what an induction HYPOTHESIS needs, a claim about one state
     with no successor in hand. -/

spec/04-theorems/properties-check.lean

@@ -67,10 +67,19 @@ def allPairs (w : List (Step × Nat)) :=
 def legalRun (w : List (Step × Nat)) : Bool :=
   (allPairs w).all (fun (n, a, b) => legalAt n a b)
 
-/-- Which entries fail, by name — the shape a counterexample report
-    needs, and the reason the catalogue carries its names as data. -/
+/-- Which entries fail, by name. A HARNESS concern: the specification
+    says what `legalAt` is, and collecting the names of what broke is
+    for whoever is debugging a red sweep. The catalogue carries the
+    names as data, which is what makes this three lines here rather
+    than a facility the specification has to provide. -/
+def failingNames (now : Nat) (a b : AbstractModel.ServerState) : List String :=
+  AbstractModel.Properties.catalogue.filterMap fun l =>
+    match l.property with
+    | .state f => if f now a && f now b then none else some l.name
+    | .trans f => if f now a b          then none else some l.name
+
 def report (ws : List (List (Step × Nat))) : List String :=
-  (ws.flatMap fun w => (allPairs w).flatMap (fun (n, a, b) => legalFailures n a b)).eraseDups
+  (ws.flatMap fun w => (allPairs w).flatMap (fun (n, a, b) => failingNames n a b)).eraseDups
 
 def witnesses (ws : List (List (Step × Nat))) (p : AbstractModel.ServerState → Bool) : Bool :=
   ws.any fun w => (trace w).any (fun (_, s) => p s)

spec/04-theorems/properties-step.lean

@@ -34,7 +34,7 @@ def transHoldsRun (w : List (Step × Nat)) : Bool :=
   (steps w).all (fun (n, a, b) => legalAt n a b)
 
 def transReport (ws : List (List (Step × Nat))) : List String :=
-  (ws.flatMap fun w => (steps w).flatMap (fun (n, a, b) => legalFailures n a b)).eraseDups
+  (ws.flatMap fun w => (steps w).flatMap (fun (n, a, b) => failingNames n a b)).eraseDups
 
 def stepWitnesses (ws : List (List (Step × Nat)))
     (p : ServerState → ServerState → Bool) : Bool :=