# 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:

```json
{"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](../quickstart/rest.md) — the full check response, in three calls.
- [Enforce a policy and get the same answer every time](same-answer-every-time.md) — why the seam is the claim dictionary.