Formatter.Audit.PredicateAgreement

A render-truth audit of the "will this break?" predicates in Formatter.Render.NodeClassify.

This module backs the CLI's --audit-predicates flag:

gren-format --audit-predicates MyFile.gren

which walks a file's LPT and prints, as JSON, every predicate that promised a break the renderer did not deliver. Like Formatter.Audit.DecisionTrace it sits off to the side of the pipeline; nothing in Formatter.Logical or Formatter.Render consults it. tests/audit-predicates.py is the gate that drives it over the fixture corpus, and docs/testing.md describes how to run that and how to read what it prints.

Why it exists

Layout here is decided in two stages. A predicate in NodeClassify answers "does this subtree force a hard break?" before anything is rendered, so its callers can lay out the code around it. Any such predicate is a hand-written mirror of what the renderer will do, and nothing forces the two to agree. When one over-approximates -- claims a break the renderer never emits -- callers commit to a vertical shape for content that lands on one line.

Nothing else in the repo catches that. Such output is still deterministic, AST-equivalent, idempotent, and stable under both fuzzers; only the layout is wrong. This module is the missing oracle: it checks each predicate against the renderer itself.

The property

For the predicates in auditedPredicates the implication is one-directional:

predicate node == True   ==>   the node's own box renders multi-line

An under-approximation -- False on a node that does render multi-line -- is deliberately not reported. These predicates claim only the breaks that are unconditional, and a node can still break for reasons they do not model, most often the author's own row layout (forceVertical).

commentBreaksFlowRow is audited separately and in both directions, because it is a different kind of mirror and its dangerous direction is the other one. See flowCommentFindings.

Why the one-directional half is nearly empty

That is the intended end state rather than missing coverage. This module was written when NodeClassify carried a whole mirror layer -- subtreeHasVerticalBox, nodeSpansRows, bracketOpenGate and friends, each predicting verticality from source rows. All of them are gone: verticality is now decided by rendering the child and asking isSingleLine / B.allSingles, which cannot disagree with the renderer because it is the renderer. What remains is isMultilineLambdaParenBlockBox, a structural query over shape kinds rather than a prediction from rows -- so that half of the audit is close to vacuous by construction, and shrinking it to that was the goal.

type alias Finding =
{ predicate : String
, boxKind : String
, row : Int
, col : Int
, rendered : String
, propagated : Bool
, claim : Bool
}

One disagreement: predicate claimed the boxKind node at row:col would break, but it rendered as the single line rendered.

propagated distinguishes a wrong answer from its echo. A predicate whose fallback arm is Array.any thePredicate children -- as the retired subtreeHasVerticalBox's was -- turns one wrong answer at a leaf into a wrong answer at every ancestor above it, and at every caller reading those. A propagated finding is real but not separately fixable: it disappears once the node below it is fixed. Only propagated == False findings are a work-list.

Neither predicate audited today is recursive (see the module doc), so nothing they report can be an echo and this flag should always be False. It is kept because it is the shape any future recursive predicate would need, and because a True here would itself be worth investigating.

claim is what the predicate answered. Findings of the one-directional property all carry claim == True by construction; flowCommentFindings also reports False, and the two read as opposite complaints.

boxKind is misnamed: it holds shapeKindName (lpnShape node), an LPShape constructor name, not a Formatter.Render.Box -- the two are different things (a shape says what kind of node this is, a Box says where its characters land), and the name dates from before LPBox was renamed to LPShape. shapeKind is what it should be called. It is deliberately NOT renamed: the field is a JSON key in the --audit-predicates output, read by audit-predicates.py, matrix-syntax.py, gen-random.py and the two _run_predicate_* instruments, and named in tests/GENERATOR.md and docs/testing.md. Renaming it is a one-shot flag day across all of those, for a field whose only consumers are our own gates -- not worth breaking a saved finding or a half-updated instrument over. Read it as "shape kind".
auditLpt : LPNode -> Array Finding

Walk every node of an LPT and report each predicate that promised a break the renderer did not deliver.
findingsToJson : Array Finding -> String

Encode findings for the --audit-predicates flag.