Explain a policy decision with the rule that decided and a counterexample

How a DSAIL check names the assertion that failed and the values under which it fails, so a person can be told exactly why — and why there is no combined verdict.

A result nobody can explain is a result nobody will act on. When a document fails a policy check, the next question is always which rule, and why. DSAIL answers it structurally: every FALSE carries the rule that decided, with a counterexample.

What comes back

A check returns every rule in the ruleset, each with the assertions it states, each with the engine's own result:

{"rules": [
  {"rule": "receipt_over_75", "assertions": [
    {"name": "receipt_over_75", "check": "FALSE", "unknown_policy": "neutral",
     "counterexample": "[amount = 120, has_receipt = False]"}]},
  {"rule": "within_cap", "assertions": [
    {"name": "within_cap", "check": "TRUE", "unknown_policy": "neutral"}]}]}

The counterexample is not a message the service composed; it is the model the solver found, printed as the solver prints it — an assignment of the claim values under which the assertion is violated. Here it says: with the amount at 120 (USD, the claim's declared unit) and no receipt, receipt_over_75 cannot hold. A person reads it and knows which fact to check. Each rule holds a list of assertions, so a rule that one day states several is read the same way.

Why there is no overall verdict

The service publishes no compliant/non-compliant, no severity and no ranking, on purpose. Choosing which of two violated assertions "really" describes a document requires knowing what each rule costs the business, and the service does not know that. What it knows — exactly what each assertion concluded — it reports in full, and the system reading the results folds them with its own knowledge. A model relaying the results is told to use the four words and attribute them to the rules: *the rules concluded that receipt_over_75 is FALSE*.

The four results

Result	Meaning
`TRUE`	The assertion holds over the submitted values.
`FALSE`	It is violated; the counterexample says under which values.
`UNKNOWN`	A claim it needs was submitted as unknown, or is unconstrained. Unknown is an answer, not a guess.
`AMBIGUOUS`	Its evidence was contradicted (declared in the contract; produced when an instance axis carries conflicting answers).

Accounting for the values judged

When a numeric claim arrives in one unit and the rule compares in another, the response's claims.quantities block records the submitted value, the value bound, the unit it was measured in and the conversion the engine applied — with by: "engine" stating that nothing outside the solver touched the number. The factor shown is a description for a person to verify, never an input to the arithmetic, which runs in exact rationals.

Reproducing the explanation later

The response names ruleset_hash and unit_library_hash. Re-run the same claim dictionary against that pair and the bytes are identical — the same answer every time. An approval recorded against the hash says which person signed off on exactly those rules.

Try it

Quickstart: REST — the full check response, in three calls.
Enforce a policy and get the same answer every time — why the seam is the claim dictionary.