`api_law_check`

Check declared Yichus/Law obligations. Mode sampled (default) uses seeded generation: holds is bounded observation, never proof. Mode exhaustive checks every value of an accepted finite type or every distinct value of a Bosatsu FiniteObligation list; holds-exhaustive applies only to that recorded scope. Unsupported domains, exceeded limits, unfinished witnesses, and worker failures never become a pass. Violated and inconclusive both mean not done.

Kind: LawCheck. Origin: Yichus/Mcp::catalog.

CLI: yichus law — sampled and finite exhaustive laws; use `yichus law --mode exhaustive` for a killable JVM worker (generic JVM `call` refuses that mode); MCP and WebMCP run the shared checker in killable workers.

Parameters

sources (required, array) — JSON array of {fileName, source} Bosatsu files including the Obligation bindings.
module_name (optional, string) — Optional module name for the verdict artifact (default Laws).
seed (optional, integer) — Optional run seed; the whole run replays from this one number (default 41).
runs (optional, integer) — Optional generated inputs per obligation (default 200).
shrink (optional, integer) — Optional shrink budget per counterexample (default 200).
mode (optional, string) — sampled (default) or exhaustive; exhaustive never falls back to a seeded pass.
maximum (optional, integer) — Maximum finite inputs per obligation in exhaustive mode (default 256, hard cap 4096).

Read the result according to this tool’s scope: static checks, bounded execution checks, and descriptive diagrams answer different questions. A successful call is not a general approval of the program. The safety and permissions guide compares the checks and provides editable ownership, guard, and role examples.