Idea
What a result means
What holds, violated and inconclusive mean
A check that says a property holds is only useful if you know what it covered. A search that stopped at a bound and a search that finished can both come back without a failure, so the answer has to say which one happened.
Each Yichus check gives one of three answers for a named property:
holds, violated, or inconclusive. Some
checks spell the first proven and the last blocked. A result reads holds
only when the check finished over its stated scope. A check that found no failure
but did not finish reads inconclusive.
Credit: a third answer beside true and false comes from Kleene’s three-valued logic; SMT solvers report sat, unsat, or unknown, and model checkers such as TLC distinguish a completed search from a cut-off one. Yichus applies that discipline to its checkers’ results.
Three answers, each with one meaning
violated names what failed: a schedule or an input that breaks
the property, or, in an access check, a database operation that could not be
proven guarded. That last kind means not proven safe, not a demonstrated leak. holds means
the method completed over the recorded scope. Everything else is
inconclusive: a search that hit its bound, a construct the checker
does not support, an unfilled witness, a missing proof host, or an effect whose
meaning the checker cannot see. A tool call that ran successfully says only
that it ran; read each property’s own outcome.
A holds is always relative to something: the model, its fault
budget, the finite domain, the sampled inputs, and the engine behavior
assumed at the boundary. Read the subject, method, scope, and completion together.
Where the line falls in each checker
yichus dist searches
schedules depth-first; by default each schedule is cut at 12 events and the
search at 20,000 schedules. If any schedule is cut off, a violation found is still
reported, but no property can read holds. A final property also
stays inconclusive when no schedule settled.
A sampled law check reports
holds for the inputs that ran and records them as its scope; a completed finite check reports
holds-exhaustive for its listed scope; a Lean receipt reports
proved for the translated theorem. An unfilled
WitnessTodo keeps the law inconclusive even when no input fails.
A native Spec verdict treats an unclassified effect as able to write any state cell, so it cannot support a race-freedom claim. Access checks mark an operation on an unknown table inconclusive; an owner key they cannot follow through a helper function is reported violated because no proof was found, which does not by itself demonstrate a leak.
How the rule is enforced in the tests
The dist verdict corpus labels each program correct or defective. Its golden test labels a case defective only when some verdict is violated, and correct only when every verdict is conclusively good over a complete search. A case that is neither fails the test instead of inheriting the happy label.
Structure pages list facts; the reader judges
Correctness questions get verdicts. Organization questions do not.
yichus organize page, stack, and
conventions show how a Bosatsu
program is built: which blocks each layer is built from, how often a block is
used above, which shapes recur. They print literal counts and never a score,
share, threshold, or “off-convention” mark. Whether a layer of single-use
helpers is a problem is your call.
Start from the stack lens guide.
Heuristics and authored views stay separate
yichus organize aid is a separate program over the conventions
page for readers who cannot judge from it. Every line it prints is labeled a
heuristic and is never evidence. An author can add a view that orders and
captions a page; the checker refuses a view whose caption carries a verdict
word or that leaves out a mandatory fact.
Limits
A conclusive holds is still no stronger than its assumptions.
External implementations, the compiler, the analyzers, and runtime adapters
are trusted; a transaction model assumes the storage adapter is atomic.
A declared model does not prove that handlers implement it, and a
holds about a model is not a claim about every deployment.
An access check verifies that the declared guard is used, not that the
guard expresses the policy you intended.