# nb-14 — Why this answer and what would change it
*Northbridge course, advanced ([nb-10](/tutorials/northbridge/nb-10-parallel-procedure/) →
[nb-11](/tutorials/northbridge/nb-11-appeal/) → [nb-12](/tutorials/northbridge/nb-12-allocation-rounds/) →
[nb-13](/tutorials/northbridge/nb-13-expansions/), this article).
All law is fictional; every resident, bill, tariff and case file is
synthetic and unofficial. No real municipal deployment or legal-validity
claims. Engine `law 0.1.0`, semantics `law.core/0.2`.*
## Situation
Bob received a bill for one month and wants to know whether it counts
as a big bill. Ann was billed for twelve months and asks the same
question. The clerk answers Ann with "yes" and Bob with "neither yes
nor no" — and both customers ask the follow-up question every clerk
dreads: *why this answer, and what would change it?*
"Because the computer says so" is not an answer. This article shows the
four machine-checkable replies Law DSL offers: a stored question with
its derivation, a plain-language reading of that derivation, one claim
checked across many facts at once, and a priced what-if for flipping
an unestablished answer.
You will put the billing questions to the CenterCity case file, read
back why each answer came out as it did, and find the cheapest fact
change that would turn the six-month silence into an established big
bill. Each new term is introduced where it is first used.
## Prerequisites
[nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/):
facts, strict rules, the four truth statuses
(`TRUE_ONLY` means established, `NEITHER` means established neither
way), `law test` as the way to check a claim.
[nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/): the `permit_fee` function
(10 EUR per month) and Money comparison — the arithmetic behind
`big_bill`.
New here: `query`, `property`, `counterfactual` are *declarations* —
named objects inside a package — while `law ask` and
`law engine counterfactual` are *commands* you run. A declaration says
what exists; a command executes something. Confusing the two is the
typical mistake below.
## Minimal example
All fragments are excerpts from
`packs/examples/language-demo/queries/package.law` (identifiers as
written; package header, imports and unrelated rules cut), plus two
case facts from `packs/examples/language-demo/cases/cases/center-city.lawcase`.
Excerpt 1 — a named computation (lines 23–26). A **query** declaration
computes a value from its parameters; `DoubleFee` doubles the permit
fee through a local `let` binding.
```law
query DoubleFee(months: Integer) -> Money {
let base: Money = demo.northbridge.calculations::permit_fee(months);
return 2 * base;
}
```
Look at the shape of the block: a name (`DoubleFee`), typed
parameters, a `let` binding for the intermediate value, and a `return`.
The doubling lives in exactly one named place instead of being copied
into every rule that needs it — but note what the query does not do:
it derives no relation, so no truth question can be put to it.
Excerpt 2 — the same computation as a rule (lines 34–39). A **rule**
derives a relation from facts; `BigBill` fires when the billed months'
fee reaches 50 EUR. Rules, not queries, are what `truth(...)` asks
about.
```law
rule BigBill strict {
for m: Integer;
when billed_months(m)
and demo.northbridge.calculations::permit_fee(m) >= 50 EUR;
then big_bill(m);
}
```
Look at the condition: `billed_months(m)` supplies the month count,
and the same `permit_fee` function the query calls is compared against
the 50 EUR bar. One arithmetic source, two uses — and because this is
a rule, its conclusion `big_bill(m)` is something `truth(...)` can ask
about.
Excerpt 3 — a claim over many facts (lines 40–43 of the test file
`packs/examples/language-demo/queries/tests/queries.lawtest`; helper
`double_billed` is line 66 of the package). A **property** quantifies
over collected facts and asserts an expectation for each; here every
billed month count must not exceed its double.
```law
property BilledDoubledCoversBilled {
forall m in collect v: Integer where billed_months(v);
expect double_billed(m) >= m;
}
```
Look at the two lines inside: `forall ... collect` gathers every
month count with a billing fact, and `expect` states what must hold
for each of them. One statement is checked against every matching
fact — the engine enumerates them, so no test per fact is needed.
Excerpt 4 — a what-if declaration (lines 73–78 of the package). A
**counterfactual** names a `target` that is currently unestablished
(`big_bill(6)` — the case holds no `billed_months(6)`), which relations
may be edited (`mutable billed_months`), which may not (`immutable
city_tariff`), and which function prices an edit (`cost EditCost`).
```law
counterfactual FlipToBig {
target big_bill(6);
mutable billed_months;
immutable city_tariff;
cost EditCost;
}
```
Look at the four lines: the `target` names the currently
unestablished goal, `mutable` and `immutable` draw the boundary of
allowed edits, and `cost` names the pricing function. The declaration
fixes the rules of the what-if game — target, allowed moves, price
list — before any search runs.
Excerpt 5 — the case facts the questions run against (CenterCity case,
its two billing assertions). A **case** holds only facts and stored
questions; all norms live in the imported packages.
```law
assert "b12": demo.northbridge.queries::billed_months(12) { origin case_input; }
assert "b1": demo.northbridge.queries::billed_months(1) { origin case_input; }
```
Look at the two assertions: same relation, different month counts.
Twelve billed months reach a 120 EUR fee and clear the 50 EUR bar;
one month reaches 10 EUR, and nothing derives from that fact either
way. The same rule sees two facts and produces two outcomes.
## Command and result
First check that the billing package itself is green:
```sh
law test packs/examples/language-demo/queries
```
Observed result (engine `law 0.1.0`) — five tests plus one property,
all passing:
```text
law test demo.northbridge.queries: мир demo.northbridge.queries, demo.northbridge.calculations, demo.northbridge.vocabulary
ok [demo.northbridge.queries] tests/queries.lawtest / rule reads the same function as the query
ok [demo.northbridge.queries] tests/queries.lawtest / query does not invent support
ok [demo.northbridge.queries] tests/queries.lawtest / count of central residents leads to the charge
ok [demo.northbridge.queries] tests/queries.lawtest / charge for billed months is non-negative
ok [demo.northbridge.queries] tests/queries.lawtest / negative charge fails the gate
ok [demo.northbridge.queries] tests/queries.lawtest / urn:law:demo:northbridge:queries#BilledDoubledCoversBilled
итого: 6 проверено, 6 прошли, 0 не прошли, 0 не исполнены; код 0
```
All six lines pass: each answer matched its expectation. The summary
is in Russian and reads `итого: 6 проверено, 6 прошли, 0 не прошли,
0 не исполнены; код 0` — 6 checked, 6 passed, 0 failed, 0 unexecuted,
exit code 0. The sixth `ok` line is the property, checked by the
engine alongside the five tests.
An **ask** is a stored question put to a case — here the CenterCity
file with its two billing assertions. The engine returns a truth
status together with a **proof graph**, the derivation steps behind
the status. Run the twelve-month question first:
```sh
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12
```
Observed: `"truthStatus":"TRUE_ONLY"` with
`"evaluationStatus":"COMPUTED"`. For Ann's case this settles it:
twelve months at 10 EUR each clear the 50 EUR bar, the rule fired,
and `COMPUTED` confirms the question evaluated normally. Now the
six-month question on the same unchanged case:
```sh
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(6));' --query-id big-bill-6 --format text
```
Observed: `Не установлено ни что «big_bill» (m: 6), ни обратное` —
"established neither that big_bill (m: 6) nor the opposite," i.e.
NEITHER — with `В доказательстве ответа нет шагов вывода` ("there
are no derivation steps in the answer's proof"). For the clerk this
is the honest middle: the engine does not call six months "not big";
it reports that nothing derives either way.
An **explanation** reads the saved proof graph back as a because-list.
Save the twelve-month answer first (`--out` stores the ask vector),
then explain it:
```sh
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12 --out /tmp/nb14-ask12 --format json
law engine explain /tmp/nb14-ask12 --json
```
Observed: `{"conclusion":"big_bill(12): TRUE_ONLY","because":["urn:proof:apply:BigBill:...","urn:proof:assert:urn:law:demo:northbridge:cases#b12"],...,"ok":true}`.
The because-list names exactly two steps: the `BigBill` rule
application and the `b12` case assertion feeding it. That is the
clerk's answer to Ann's "why": your twelve-month billing fact fed
the big-bill rule. Run over the six-month vector instead, the same
command reports `"conclusion":"big_bill(6): NEITHER"` with
`"because":[]` — an explanation of silence. There is nothing to
list because nothing derived, and the empty list says so plainly.
A saved answer is evidence only if a fresh run reproduces it.
`--out` stores the ask triple (`ask.json`, `request.json`,
`result.json`); two runs at identical inputs must agree byte
for byte, stdout included — and agree with the frozen exhibit
shipped in `cases/evidence/`. The next block checks all of that at
once:
```sh
rm -rf /tmp/nb14-replay && mkdir -p /tmp/nb14-replay
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12 --format json --out /tmp/nb14-replay/a > /tmp/nb14-replay/stdout-a.json
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12 --format json --out /tmp/nb14-replay/b > /tmp/nb14-replay/stdout-b.json
cmp /tmp/nb14-replay/a/result.json /tmp/nb14-replay/b/result.json && echo RUNS-IDENTICAL
cmp /tmp/nb14-replay/a/request.json /tmp/nb14-replay/b/request.json && echo REQUESTS-IDENTICAL
cmp /tmp/nb14-replay/stdout-a.json /tmp/nb14-replay/a/result.json && echo STDOUT-EQUALS-RESULT
cmp /tmp/nb14-replay/a/result.json packs/examples/language-demo/cases/evidence/big-bill-12.ask.json && echo FROZEN-IDENTICAL
law eval /tmp/nb14-replay/a > /tmp/nb14-replay/eval-a.json
cmp /tmp/nb14-replay/eval-a.json /tmp/nb14-replay/a/result.json && echo EVAL-IDENTICAL
```
Observed: all five markers print —
`RUNS-IDENTICAL`, `REQUESTS-IDENTICAL`, `STDOUT-EQUALS-RESULT`,
`FROZEN-IDENTICAL`, `EVAL-IDENTICAL` — exit 0
(`result.json` digests to `sha256:a80b0deb…`). Each marker pins one
equality: the two runs agree with each other, stdout matches the
stored result, the fresh run matches the frozen exhibit, and `law
eval` — which replays the saved `request.json`, so this last check
needs no live package at all — reproduces the result too.
The comparison is only meaningful if a real change breaks it.
Copy the case to scratch, flip one fact (`billed_months(12)`
→ `billed_months(2)`), rerun:
```sh
rm -rf /tmp/nb14-replay && mkdir -p /tmp/nb14-replay
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12 --format json --out /tmp/nb14-replay/a > /tmp/nb14-replay/stdout-a.json
cp -r packs/examples/language-demo/cases /tmp/nb14-replay/mut
python3 - <<'EOF'
p = '/tmp/nb14-replay/mut/cases/center-city.lawcase'
s = open(p).read().replace('billed_months(12)', 'billed_months(2)')
open(p, 'w').write(s)
EOF
law ask /tmp/nb14-replay/mut --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12 --format json --out /tmp/nb14-replay/c > /tmp/nb14-replay/stdout-c.json
cmp -s /tmp/nb14-replay/a/result.json /tmp/nb14-replay/c/result.json && echo SAME || echo RESULTS-DIVERGE
cmp -s /tmp/nb14-replay/a/request.json /tmp/nb14-replay/c/request.json && echo SAME || echo REQUEST-DIVERGES
cmp -s /tmp/nb14-replay/a/ask.json /tmp/nb14-replay/c/ask.json && echo RECEIPT-IDENTICAL || echo RECEIPT-DIVERGES
python3 - <<'EOF'
import json
for tag in ('a', 'c'):
r = json.load(open(f'/tmp/nb14-replay/{tag}/result.json'))
m = r['manifest']
print(tag, r['results'][0]['truthStatus'], r['resultHash'][:18], 'case', m['caseHash'][:18], 'program', m['programHash'][:18])
EOF
```
Observed: `RESULTS-DIVERGE` (`result.json` first differs at
char 171), `REQUEST-DIVERGES`, but `RECEIPT-IDENTICAL` — the
receipt carries `programHash`/`resolutionHash` and no
`caseHash`, so comparing receipts alone cannot see a fact
change. That asymmetry is the point: the check catches real
changes, and it also shows which file sees them. The projection
reads:
```text
a TRUE_ONLY sha256:172814eac88 case sha256:f94316c7d8a program sha256:fa858cf463d
c NEITHER sha256:f4197e2adb5 case sha256:64ae656179d program sha256:fa858cf463d
```
Truth flips `TRUE_ONLY` → `NEITHER`, `resultHash` and
`caseHash` move, `programHash` stays — the program did not
change, the facts did. That scoping signal is the point of the
projection; equality itself is always the byte `cmp` of
`result.json` (the full canonical document), never a field
subset.
Three limits apply to this replay check. `ask.json` alone is blind
to facts. `eval` replays the frozen request; it does not re-resolve
the live package. And no volatile fields were found — the only
timestamps are case-context inputs, per the documented
no-ambient-reads contract — but this is still one binary on one
machine: cross-binary byte parity belongs to the vectors suite, not
to this article.
The what-if executes against frozen exhibits in
`packs/examples/language-demo/cases/counterfactual/flip-to-big/`.
A **counterfactual** names a currently unestablished target and asks
for the cheapest fact change — a **candidate** with a **cost** — that
would flip it:
```sh
law engine counterfactual --program packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-world.json --case packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-case.json --input packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-input.json
```
Observed: `"status":"FOUND"`,
`"solverProfile":"law.solver.finite-enumeration/0.1"`, one solution —
candidate `urn:law:demo:northbridge:queries#add-b6` at `"cost":"1"`
(adding `billed_months(6)`), `"cutoffCost":"1"`, one candidate
checked. For the clerk this is the priced answer to "what would
change it": assert six billed months and the target flips. A **replay
certificate** then proves the winning change was really re-executed:
```sh
law engine counterfactual --program packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-world.json --case packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-case.json --input packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-input.json --verify packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-cf-result.json
```
Observed: `{"kind":"counterfactual-verification","result":"urn:law:demo:northbridge:queries#FlipInput01/result","valid":true}`.
The flip was re-derived against the pinned inputs, not just claimed.
Both packages also pass the static check (`check OK` for each
`package.law`).
## Why this construct
Bob's "why" is answered by the stored question plus its derivation.
The ask returns the truth status together with the proof graph, and
`law engine explain` turns that graph into a because-list of rule
applications and case assertions. For the twelve-month question the
list holds exactly two steps; for the six-month question it is empty —
which is itself informative, because it says no derivation exists.
The "does this hold everywhere" question needs no test per fact.
`BilledDoubledCoversBilled` states the doubling claim once and runs
inside the same green suite as a sixth `ok` line. The engine, not
the author, enumerates the matching facts.
The "what would change it" question gets a price tag.
`FlipToBig` declares the target, the mutable and immutable relations,
and the cost model; the finite-enumeration solver searches the
declared candidates and returns the cheapest flip: add `b6`, cost 1.
Ties are admitted honestly: the solver lists every cheapest patch
and never silently picks one while hiding another.
How the tie behavior was checked
A probe with a second equal-cost candidate in a `/tmp` copy of the
input returned `FOUND` with *both* solutions at cost 1, `cutoffCost
1`, two candidates checked. The cutoff names the cheapest price; the
solution list names everything at that price.
The flip itself is trusted without re-running the search by hand.
The result carries a per-candidate `evaluationHash` and proof roots,
and `--verify` re-executes the winner against the pinned program and
case hashes, reporting `valid:true`.
Why not a second hand-written test?
A hand-written test could assert `big_bill(6)` after adding the fact —
but it would prove only the author's one guess. It could never show
minimality or the absence of cheaper alternatives. The solver's
`cutoffCost` plus the checked-candidate count is what a test cannot
say.
The evidence for all of this is the 6/6 suite, the TRUE_ONLY/NEITHER
ask pair, the two-step because-list, the FOUND result with cost 1,
and the `valid:true` replay — each executed above, none asserted in
prose. What is not proven is that six months *should* count as a big
bill, or that cost 1 is a fair price for a record change. The machine
proves the declared game was played correctly; Northbridge's choice
of target, mutables and prices is fictional data, not legal advice.
## Changed condition
Ask `big_bill(6)` on the unchanged case: NEITHER, `because: []`.
Now add the single winning fact — `billed_months(6)` at cost 1 — and
the same question becomes TRUE_ONLY. Six months at 10 EUR each reach
exactly 60 EUR, clearing the 50 EUR bar of `BigBill`, so the rule
fires where before no rule could. One added assertion, two statuses —
and the explanation grows from an empty list to the rule-plus-assertion
pair.
The twelve-versus-one pair shows the same logic without any what-if.
`billed_months(12)` feeds `BigBill` (TRUE_ONLY), while
`billed_months(1)` feeds nothing (NEITHER: the 10 EUR fee never
reaches the bar). The rule did not change; the facts did.
## Typical mistake
The mistake is calling the query declaration as if it were a
question — handing `DoubleFee(12)` to `law ask` instead of asking
about a relation:
```sh
law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate demo.northbridge.queries::DoubleFee(12);' --query-id try-query-call --format text
```
Observed: `{"error":{"code":"LDC-E1105","message":"... DoubleFee: символ не экспортирован пакетом ..."}}`.
The Russian phrase says the symbol is not exported by the package.
A `query` is a declaration, not an exported relation and not a term:
it cannot be asked about, used in a rule condition (that refusal is
`LDC-E2105`, executed in [nb-17: Numeric families and support boundaries](/tutorials/northbridge/nb-17-numeric-families/) against
`boundaries/evidence/snippets/query02.law.txt`), or addressed across
packages.
The fix is to reach the computation through a rule like `BigBill`
that reads the same underlying function — which is exactly why
Excerpts 1 and 2 mirror each other. Rule of thumb: if it ends in
`Fee(...)` with arguments, it is the function, usable in conditions.
If it is `DoubleFee`/`CentralCount`, it is the named query, runnable
only through its declaration, never through `truth(...)` or
`evaluate` from outside.
## Limits
Queries invent no support. The test `query does not invent support`
exists precisely for this: one billed month yields NEITHER for
`big_bill(1)`, never a refusal-style false. A query declaration adds
no derivation by itself.
The boundaries are profile facts. `LDC-E1105` (not exported, not
cross-package addressable) and `LDC-E2105` (not a term in
conditions), the property's `E1105/E2403` restrictions on qualified
references and pure aliases in `property-expect`, and the solver
profile `law.solver.finite-enumeration/0.1` describe this
implementation (`law 0.1.0`, semantics `law.core/0.2`), never the
language in general.
Finite search needs a finite game. The declaration must bound the
search: an explicit target, explicit mutables, and enumerated
candidates with a cost model. An unbounded "change anything" is not
expressible — the solver checks listed candidates, it does not
invent them.
Certificates pin hashes, not wisdom. `--verify` replays the result
against the pinned program, case and input hashes (`programHash`,
`caseHash`, `inputHash`); byte-different inputs are rejected before
any reasoning. It certifies correct replay, not a correct tariff.
One observed refusal remains: `law engine why-not` over a saved
*ask* vector returns `ok:false` (`подмена вида вопроса не
поддерживается` — "substituting the question kind is not
supported"). In this build why-not does not read ask vectors, so
"what is missing" for an ask is answered by the counterfactual, not
by why-not.
## Exercise
Without running the engine, predict, then check with the commands
above:
1. `big_bill(1)` versus `big_bill(12)`: which truth status each, and
which two proof steps would `explain` list for the established
one?
2. What does `evaluate demo.northbridge.queries::DoubleFee(12)` from
`law ask` return, and which declaration-vs-question confusion does
it expose?
3. Which single declared fact flips `big_bill(6)`, at what cost, and
what does the `--verify` replay report?
4. If the counterfactual input listed two different cost-1
candidates, how many solutions would you expect, and what would
`cutoffCost` be?
5. In a scratch copy of the case, change `billed_months(12)` to
`billed_months(2)`: predict which of `ask.json`,
`request.json`, `result.json` change, what truth `big_bill(12)`
reports, and whether `programHash` moves — then run the
rerun block and confirm.
Write down each prediction first; run the commands; explain any miss
in one sentence. Check your work against the
[full solution: statuses, explanation steps, flip cost and replay](/tutorials/northbridge/solutions/nb-14-solutions/).
## Sources
- Source: `packs/examples/language-demo/queries/package.law` (queries
`DoubleFee`, `CentralCount`, rules `BigBill`, `CentralPays`,
`BilledFeeGate`, property `BilledDoubledCoversBilled`,
counterfactual `FlipToBig`)
- Tests: `packs/examples/language-demo/queries/tests/queries.lawtest`
(five tests plus the property)
- Case and exhibits: `packs/examples/language-demo/cases/cases/center-city.lawcase`
(CenterCity facts), `cases/evidence/` (frozen ask exhibits,
byte-identical to fresh runs),
`cases/counterfactual/flip-to-big/` (world, case, input, result,
`verify.json`, reproduction README)
- Suite tour: `packs/examples/language-demo/README.md`
- Language reference: `docs/language/09-advanced-cheat-sheet.law.md`,
`docs/language/06-testing-a-package.law.md`
- Prerequisite: [nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/),
[nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/); next: [nb-15: Quantities and dimensions](/tutorials/northbridge/nb-15-quantities/)
Three levels:
1. **Northbridge use** (this article): the billing desk answers "is
it big" with status plus because-list, guarantees a doubling
property across all billed facts, and quotes the cheapest flip
(add six-month billing, cost 1) with a replay certificate —
verified by the 6/6 suite, the ask pair, the explanation pair and
the FOUND-plus-`valid:true` counterfactual above.
2. **Domain template:** whenever a regime must justify answers,
separate the four jobs — ask stored truth questions and explain
them from the proof graph; state universal claims as properties,
not test lists; declare what-ifs with explicit target, mutables
and cost model; ship every flip with its replay check. Never call
a `query` declaration where a relation is expected.
3. **Confirmed example elsewhere:** the frozen exhibits in
`packs/examples/language-demo/cases/evidence/` (`big-bill-12.ask.json`,
`central-pays-1.ask.json`) are byte-identical to fresh `law ask`
runs — the same ask-explain machinery reproducing identical
answers outside the queries package, per the cases README. Ask and
explain are engine capabilities over any case, not features of one
billing example.
4. **Confirmed external formalization (corpus):** consumer
association liberty (Civil Code of Kazakhstan, art. 10) — package
`kz.corpus.civilcode`,
`corpus/laws/kz/codes/civil-code/tests/10-art10-consumer-may-join-organisations.lawtest:10-11`:
`evaluate positions()` with a named position+status expectation
(`expect position(ObjedinenieVObshchestvennyeOrganizatsiiPotrebiteley, ACTIVE)`).
The literalless kind is asked bare while the expectation addresses
a named position with a status — the pointed ask form this
article's machinery generalizes. Evidence:
`docs/research/constructs/24-queries/corpus-forms.en.md` [§1](/tutorials/northbridge/nb-01-first-permit/#1-situation)
(rated exemplary). Limit of verification: presence of the named
construct at the cited lines only, confirmed by direct file read;
no claim about deployment, runtime behaviour, or legal
correctness.