nb-14 — Why this answer and what would change it

← Course mapChapter 14 / 25 · Advanced

Northbridge course, advanced (nb-10 → nb-11 → nb-12 → nb-13, 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: 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: 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.

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.

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.

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).

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.

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:

law test packs/examples/language-demo/queries

Observed result (engine law 0.1.0) — five tests plus one property, all passing:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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

big_bill(1) versus big_bill(12): which truth status each, and which two proof steps would explain list for the established one?
What does evaluate demo.northbridge.queries::DoubleFee(12) from law ask return, and which declaration-vs-question confusion does it expose?
Which single declared fact flips big_bill(6), at what cost, and what does the --verify replay report?
If the counterfactual input listed two different cost-1 candidates, how many solutions would you expect, and what would cutoffCost be?
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.

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, nb-04: The permit fee; next: nb-15: Quantities and dimensions

Three levels:

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.
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.
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.
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 (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.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.