Verdicts

A Cella check ends in a verdict, not a boolean.

Verdict	Means	Comes with
Accept	Checked by both kernels	The assumptions it rests on: a postulate, a rewrite rule, termination as judged by the elaborator, a modelled choice of the implementation
Reject	Wrong	Where, and which rule
Unknown	Not known yet	Why: a hole, the step budget ran out, the kernel cannot express it, it depends on something unknown

Accept is built, not returned

An Accept can only be made by combining verdicts: no part of the checker can return true and have it count as passed. The budget is counted in steps, not time, so a verdict is reproducible.

Unknown spreads

A definition that depends on an Unknown is not Accept. An underdetermined answer (a circuit missing its ground) is an Unknown with evidence: it says what is missing. A numeric conclusion with an error bound is an Accept with a rating assumption; a solver that cannot give a certificate can appear only as an assumption.

For programs in other languages

For a C, C++, Arduino or Python program, the verdict also says how the program ended: its exit code and output, the undefined behavior it reached and the clause of the standard, or the implementation-defined choice it depended on (for example, which way an unspecified evaluation order went), listed under assumes.

Each problem in such a verdict has a kind (the specific reason, such as ubOverflow) and a category, one of six, by which a host decides how to show it:

category	Means
error	The program is wrong: it did not check, or it reached undefined behavior
unsupported	The model does not have this construct yet (the program may be fine)
indeterminate	The result could not be settled: the step budget ran out, the behavior is unspecified, the program waits for input
termination	The program ended in a defined way: abort, an uncaught exception
incomplete	The program has an empty slot
invalid	The program’s JSON is not a program

assumes is always there (empty when the verdict depends on no choice), each entry naming the implementation and the choice, so a host can check them against itself before it runs the program.