Module Verdict

The labels of claims this process actually evaluated successfully, in evaluation order. Scanner-control goldens use this as causal evidence: a diagnostic marker is emitted only after the claim that would emit that diagnostic has run and passed.

Records a failure, on stdout (where the golden sees it) and stderr (where it survives the nonzero exit). msg should read as the thing that is wrong, without a "FAIL" prefix of its own.

claim name b fails the run when b is false, printing nothing on stdout: for a test that renders the boolean itself, in a column layout of its own. Prefer p, which does both.

p name b prints the named boolean fact name: b and fails the run when b is false. Booleans keep .expected files backend-stable, which is why so many tests report this way; a fact whose expected value is false should be renamed to the claim that holds, so that every line of a golden reads as an assertion that passed.

pf fmt … b is p with a COMPUTED label: the format and its arguments render the label, and the boolean follows, so the call reads in the same order as p name b — Verdict.pf "%s gradients match the oracle" label ok prints "… gradients match the oracle: true" and fails the run on false.

This is the entry point for the claims gh-ocannl-601 could not convert (gh-ocannl-624): a claim whose label names which leg, which epoch or which measured quantity it is about has to build that label from an argument, and before this it had no choice but a bare printf — which exits 0 on false and lets the failure be dune promoted into the golden, the exact hazard the literal-label sites were swept for. A computed label is not a weaker claim than a literal one, so it must not have a weaker gate.

The rendered label is what p prints and what a failure names on stderr, so it should read as the fact that holds — the same rule as p: phrase it so true is the passing reading.

claimf fmt … b is claim with a computed label: it fails the run without printing anything on stdout, for a test that renders the boolean itself in a column layout of its own. Prefer pf, which does both; reach for this only where the surrounding line is a table whose shape is the point, and bind the boolean to a name used by both the print and the claim, so the two cannot drift apart.

p_all name xs ~f claims that every element of xs satisfies f, and that there is an element — the guarded form of p name (List.for_all xs ~f). Reach for it wherever the claim reads "every …". Once the population floor is met, f runs on every element in list order, even after a refutation, so diagnostic side effects are not lost.

p_all2 name got want ~f claims that got and want agree cell for cell under f, that they have the same length, and that there is a cell — the guarded form of p name (Array.for_all2_exn got want ~f), and the executed-parity genre's entry point (gh-ocannl-746). Reach for it wherever a claim compares a readback against a reference.

Emptiness is not far-fetched here, which is why the guard matters more than it looks. Both sides usually come from Context.get_values, and a node that stopped being materialized, a reference run whose own setup collapsed, or a readback of a virtualized node answers with NOTHING ON BOTH SIDES AT ONCE — the reference does not discriminate, because it went through the same path. Array.for_all2_exn [||] [||] is true, so the line that reports the strongest kind of check AGENTS.md asks for is byte-identical to one a real readback passed.

A LENGTH MISMATCH is reported as a failed claim, <claim> (length 12 vs 16): false, rather than as the Invalid_argument Array.for_all2_exn raises: an exception fails the run too, but it fails it without a claim line and without naming which claim, and the mismatch is a finding about the run (one side was reshaped, or one readback was truncated) that deserves to be read off the transcript. Reported before emptiness, so a one-sided empty says which side it was.

?min bounds the COMMON length, as in p_all.

pf_all2 fmt … got want ~f is p_all2 with a COMPUTED label, as pf is to p. Format arguments precede the two arrays and their predicate, so the call keeps the claim-shaped order: pf_all2 "%s values match" leg got want ~f. Empty or mismatched readbacks retain p_all2's distinct refusal wording; ?min has the same common-length meaning.

p_none name xs ~f claims that no element of xs satisfies f, and that there is an element — the guarded form of p name (not (List.exists xs ~f)) and of p name (List.is_empty (List.filter xs ~f)). The mirror of p_all, and the one the "no X is …" claims want: filtering an empty collection also yields nothing, so the unguarded spelling passes on an empty input just as List.for_all does.

p_alli name xs ~f is p_all with each element's index beside it -- the guarded form of p name (List.for_alli xs ~f), for the claims that compare an element with its neighbour or with a reference at the same position. Arrays go through Array.to_list, as for p_all. Like p_all, it evaluates every element once the population floor is met.

p_empty name ~over xs claims that the derived collection xs is empty, and that the collection it was derived from, over, is not — the guarded form of p name (List.is_empty xs) where xs is a precomputed subset (the invalid seeds, the declined candidates, the offending rows) of a population that must itself exist. Prefer p_none where the predicate can simply be passed; this is for the sites that keep the derived list around to report it.

p_exists name xs ~f claims that some element of xs satisfies f, and p_exists ~min:n that at least n do. Its ?min counts WITNESSES where its siblings' counts the population, and the asymmetry is the point rather than an inconsistency: for an existential a population floor buys nothing, since List.exists already answers false on an empty collection, so the only reading of ~min:2 that adds a constraint is "two of them". Reading it as a population floor is what would produce the false green this module exists to prevent — a two-element list with one witness passing "at least two of the seeds pipeline" (Codex P2, round 1).

An empty collection still says so: <claim> (empty): false, because "nothing satisfied f" and "there was nothing to satisfy it" are different findings. Too few witnesses under an explicit floor names the shortfall as <claim> (only 1 of 2 match): false — "match", so that the line cannot be read as the population shortfall its siblings print. At the default floor of one the line is the bare <claim>: false p would print: there is no shortfall to name.

p_pairwise_distinct name xs ~equal ~to_string claims that xs contains at least two elements and that no two of them are equal. It reports the first colliding pair in source order directly: <claim> (collision: x = y): false. to_string is evaluated only on a collision, so a passing claim pays only for the comparisons and keeps the same stdout line as p.

This is the guarded form of building every unordered pair and passing it to p_none. The source-population floor belongs here rather than on the derived pairs: zero source elements produce zero pairs, but one source element does too, and neither is evidence of distinctness (gh-ocannl-815).

skipped ~backend name reports a leg the run's backend cannot evaluate: a GPU intrinsic on a CPU backend, a tf32 policy outside CUDA. It prints the same stdout line p would — the .expected goldens are backend-uniform, and a (test) stanza diffs stdout ONLY, so stderr is free — and announces the skip on stderr, naming the claim. grep SKIPPED over a run then enumerates exactly what that hardware did not verify. A second OCANNL_TOOL_VERDICT_SKIP<TAB>scope<TAB>executable<TAB>claim record on stderr is the machine-readable form, and the one the action's record file receives (the per-action records above), which is what the forced sweep intersects across backends; the executable identity keeps equal labels in different test legs distinct there. scope is backend by default. Pass ~aggregation:`Environment when the leg is gated by a host or configuration capability rather than the selected backend, such as a compiler target, preprocessing flag or filesystem feature; its human announcement remains visible, and the forced fleet sweep aggregates it across the measurement boxes declared by benchmarks/fixtures/DIGESTS.txt instead of mistaking it for unsupported backend coverage. Scope describes this observation, not the claim identity: if any declared-box log marks a claim Environment, a Backend skip carrying the same executable and claim key on another box is also evidence that box did not execute it. Pass ~aggregation:`Outside_sweep only when a separate checked matrix owns execution of the claim (for example the compiler-trace CI leg); the record remains validated and human-visible but neither sweep dimension treats its absence as evidence.

Use it in place of a bare p name true: that line is byte-identical to a verified run's, so neither the transcript nor a reviewer can tell the claim was never evaluated — which is how a Tensorize leg came to "cover" the gh-ocannl-528 interior-batch bug without ever checking it. The other honest form is putting the condition into the label itself ("… (skipped: non-C backend)"), which distinguishes the golden line; only the indistinguishable bare true is the one to reject.

~backend is the run's backend name, as each test already derives it for its own gating (String.lowercase (Utils.get_global_arg ~arg_name:"backend" ~default:"cc")). It is passed in rather than read here so that this library keeps depending on no OCANNL library, only base, stdio and unix: reporting a verdict is not a reason to link OCANNL's configuration machinery.

gated ~when_ ~on label b is a claim that is evaluated only where the gate when_ is open: there it is p — label: true, or a failure — and where the gate is closed it is skipped ~backend:on, b unread. Both outcomes print label: true on a passing run, so a host that legitimately skips cannot break the .expected golden (gh-ocannl-997).

It exists because that byte-identity was a convention the call site had to know. A gated claim written as if gate then pass_fail label b else skipped ~backend label records label: PASS in the golden on the machine that promotes it, and fails the diff with label: true on the one machine that reaches the skipping regime — which is the machine least likely to be promoting. Twice this shipped as far as review (staging#735's depth gate, and a host gate in gh-ocannl-1031's first draft). This entry point picks the dialect itself, and verdict_ratchet refuses a label that reaches both pass_fail and skipped.

~on names what the run was on when it skipped — a backend for the default `Backend aggregation, a host or configuration capability for `Environment — and is printed as SKIPPED on <on> (vacuous): <label>. It is ~on rather than skipped's ~backend because a host gate is not a backend. ?aggregation is skipped's.

?detail is what pass_fail offered and a gated claim had to give up: evaluated only on an evaluated failure, and rendered the way this dialect renders what a bare false cannot say, <label> (<detail>): false — the place for a measured number that must stay out of a passing golden.

b is an ordinary bool, evaluated by the caller whatever the gate says, so it must be computable off-gate — which is also what lets verdict_ratchet's quantifier reader treat this exactly as p. A leg that cannot even compute its boolean without the gate keeps its own branch and reports through p on one side and skipped on the other: the same dialect. A quantified claim goes through gated_all and its siblings.

gated_all ~when_ ~on label xs ~f is gated for a quantified claim: p_all where the gate is open, skipped ~on where it is closed. gated_alli and gated_exists do the same for p_alli and p_exists, and ?min and ?aggregation mean what they mean there.

gated cannot carry these: gated label (List.for_all xs ~f) is the unguarded quantifier verdict_ratchet refuses in p too, since a gate does not fill the population. Without this family the guarded spelling was a hand-written branch, if gate then p_alli label xs ~f else skipped ~backend label, repeating the label and the skip's arguments at every site.

Where the gate is closed, neither xs nor f is read. A leg whose population exists only where it ran (the seeds a GPU proposes, the files a host could create) can therefore pass the empty list it is left with off-gate, computed unconditionally; the non-emptiness floor applies exactly where the claim is evaluated. A leg whose population cannot be computed off-gate at all (a device readback) keeps its own branch, as gated says of its boolean.

pass_fail label b prints label: PASS or label: FAIL, and fails the run in the latter case. ?detail is evaluated only on failure and appended in parentheses — the place for a machine- specific number (a measured value, a difference) that must stay out of a passing golden.

Not for a claim some host skips: skipped prints label: true, never label: PASS, so that pairing breaks the golden wherever the skip fires. A gated claim goes through gated.

pass_fail_all2 label got want ~f is p_all2 in pass_fail's output dialect. It refuses empty, short, and mismatched pairs before evaluating f. On those structural refusals the automatic reason is kept even when ?detail is supplied; the caller's lazy detail follows it, separated by a semicolon, so an empty readback can report both (empty) and the useful (got []) diagnostic. On an elementwise mismatch ?detail behaves exactly as in pass_fail.

case label f runs one case of a test -- a group of claims that share a setup -- and turns an exception escaping it into a failed claim, <label>: the case ran to completion (raised <exception>): false, so that the cases after it still run (gh-ocannl-1067). It prints nothing of its own when f returns, so wrapping a case is golden-neutral.

Without it an exception ends the run at the case that raised. The teardown then says so (STOPPED EARLY on stderr, and the exception itself), but the rows after that case are never evaluated: a negative control that made one case raise learns nothing about the others. With it, each case is its own verdict, which is what a test of many independent rows wants.

The exception's text goes on the claim line (echoed to stderr like every failure), and the backtrace, when one is recorded, to stderr. What an explicit exit raises is let through, not recorded: that is the process ending, not a case failing. Once a check has failed, that ending is reported as STOPPED EARLY: an exit inside case "<label>" … on stderr (gh-ocannl-1084): a run that ended inside a case never ran the cases after it, and a reader counting rows (tools/mutation-run.sh) cannot otherwise tell it from a run whose earlier case raised and whose later ones completed.

Whether any check has failed so far. For a test that wants to say something extra about a bad run; the exit status is taken care of without it.

Ends a NEGATIVE-CONTROL run, one whose failures are the output its golden pins: exits 1 when something failed and 0 when nothing did, without the teardown's "FAILED: n checks …" line. That line totals the failure lines above it, and a total in a golden merges wrong -- two branches each adding a control merge the lines right and the count wrong (gh-ocannl-1056). The rule running such a control accepts exit 1 alone, so a control that stopped refusing still fails.

The claim surface intended for open Verdict.Claims. Keeping the open-oriented names in one module means a new combinator is exposed to every migrated test by changing this file alone; the top-level bindings above remain for compatibility with qualified call sites. State and scanner-control helpers deliberately stay outside this module.

The teardown line for n failed checks, without its newline. Exposed so that census_total_ratchet, which refuses this line in scan goldens, builds its control from the text the teardown really writes.