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

← Back to lessonChapter 14 / 25 · Advanced · Worked solution

How to verify

Checkable against law test packs/examples/language-demo/queries (6 checked, 6 passed), law ask on the CenterCity case, law engine explain, and law engine counterfactual with --verify. Identifiers and code as written.

1. big_bill(1) versus big_bill(12), and the explanation steps

Answer: big_bill(1) is NEITHER; big_bill(12) is TRUE_ONLY; explain lists the BigBill rule application and the b12 assertion.

One billed month costs 10 EUR (permit_fee is 10 EUR per month), below the 50 EUR bar in BigBill’s condition — so no rule derives big_bill(1), and with no derivation either way the status is NEITHER, not false. Twelve months cost 120 EUR, the condition holds, BigBill fires — TRUE_ONLY. The saved twelve-month vector explains itself as exactly two proof steps: the rule application (urn:proof:apply:BigBill:...) with the case assertion (urn:proof:assert:...#b12) as its premise. The one-month vector would explain with because: [], like the six-month one in the article: nothing derived, nothing to list.

2. Calling DoubleFee from law ask

Answer: refused with LDC-E1105 — DoubleFee is not exported; it exposes the declaration-vs-question confusion.

DoubleFee is a query declaration: a named computation, not a relation with truth values and not an exported symbol. law ask evaluates truth(...) over relations (or cards); handing it a query declaration is a category error, and the engine refuses it at the boundary (символ не экспортирован пакетом). The same computation is reachable only indirectly, through rules such as BigBill that call the underlying permit_fee function in their conditions. If you want the doubled number itself, read the query through its own declaration machinery — never through truth(...) from another package.

3. The single fact that flips big_bill(6)

Answer: adding billed_months(6) (candidate add-b6) at cost 1; --verify reports valid:true.

The CenterCity case holds billed_months(12) and billed_months(1) but no billed_months(6), so BigBill can never fire for m = 6 and the ask is NEITHER. FlipToBig declares billed_months mutable, so adding that one assertion is a legal move; six months at 10 EUR each reach 60 EUR ≥ 50 EUR, and the target flips to TRUE_ONLY. The solver reports FOUND, solution add-b6, cutoffCost 1, one candidate checked. The replay (--verify over the pinned world, case and input hashes) re-executes the winner and reports {"kind":"counterfactual-verification",...,"valid":true} — the flip was really re-derived, not just claimed.

4. Two different cost-1 candidates

Answer: two solutions, cutoffCost still 1.

The solver returns every candidate that achieves the target at the minimal cost; it does not pick one and hide the other. A probe with a second equal-cost candidate (a /tmp copy of the input with an extra add-b6-alt assertion, same literal, cost 1) returned FOUND with both solutions listed, cutoffCost 1, two candidates checked. The cutoff names the cheapest price at which anything flips; the solution list names everything available at that price. A tie is reported as a tie — choosing between the tied patches is the clerk’s decision, and the certificate keeps both options on the table.

How to verify

Terminal

law test packs/examples/language-demo/queries

Expected: итого: 6 проверено, 6 прошли, 0 не прошли, 0 не исполнены.

Terminal

law ask packs/examples/language-demo/cases --case CenterCity --query 'evaluate truth(demo.northbridge.queries::big_bill(12));' --query-id big-bill-12

Expected: "truthStatus":"TRUE_ONLY".

Terminal

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

Expected: Не установлено ни что «big_bill» (m: 6), ни обратное.

Terminal

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

Expected: "status":"FOUND" with candidate add-b6 at "cost":"1". Append --verify packs/examples/language-demo/cases/counterfactual/flip-to-big/nb-cf-result.json (with the same --program, --case, --input) for "valid":true.

5. One fact moves the answer

result.json and request.json diverge; ask.json stays byte-identical (the receipt has no caseHash). big_bill(12) reports NEITHER — with only billed_months(2) and billed_months(1) asserted, nothing derives the twelve-month bill either way. programHash does not move (sha256:fa858cf463d both runs): the program is unchanged, the facts changed. resultHash moves (172814eac88… → f4197e2adb5…) with caseHash. If you predicted the receipt would change, re-read the limits — compare result.json, not ask.json.