nb-07 — A document is not yet a proven fact

← Course mapChapter 07 / 25 · Intermediate

Northbridge course, intermediate (nb-05 → nb-06 → nb-07 → nb-08 → nb-09). All law is fictional; every act, document, verifier and hash in this article is synthetic and unofficial. Nothing here is a claim about real legislation or a real deployment. Engine law 0.1.0, semantics law.core/0.2, std 0.2.0.

Situation

Ann applies for a Northbridge parking permit and brings a paper certificate that says she lives in Northbridge. The clerk scans it, files it, and asks the question the whole permit case turns on: does this piece of paper prove that Ann is a resident?

The tempting answer — “the document says so, so it is proven” — is exactly what Law DSL refuses to give for free. A document sitting in a folder is only a stored item with a hash and a status. A proven fact is stronger: a proposition the engine will stand behind, with a recorded chain showing how it got there.

Between the two sits a pipeline with three gates: the case must select a policy, link the document to the claim with support, and pin a verification. This article walks that pipeline using five evidence tests from the register package: one document admitted end to end (TRUE_ONLY), three setups that yield no support either way (NEITHER), and one accepted refutation — a verified document speaking against the claim, which yields an explicit negative (FALSE_ONLY) rather than silence.

Prerequisites

nb-02: Why a missing fact is not a refusal — the four truth statuses (TRUE_ONLY, FALSE_ONLY, BOTH, NEITHER). This article’s results are all truth statuses, so you need to read NEITHER as “not established” rather than “refused”.
nb-06: When the register may stay silent — closure, domain and snapshot: when absence on file may be treated as a negative and when it must stay silence. This article covers the other half of the register: when presence of a document counts as proof.

No advanced constructs are required. Everything below uses facts, rules, and three new declarations that are explained where they first appear.

Minimal example

Excerpt 1 from packs/examples/language-demo/register/package.law (lines 39–47, identifiers as written; the surrounding closure rules and the snapshot tariff at the end of the file are cut):

rule Accept strict {
    for e: Text;
    for d: Text;
    for link: Text;
    when edge(e, d, link) and evidence_status(d, "verified")
        and authentic(d, "urn:demo:northbridge:verifier", "verified")
        and available(d) and current(d);
    then accepted(e);
}

The Accept rule is the clerk’s checklist for when a document counts as accepted. edge(e, d, link) links a claim to its document; the status must read verified; a pinned verifier must have marked the document authentic with outcome verified; and the document must be available and current. All five conjuncts are required — miss one and acceptance never fires.

Excerpt 2 from the same file (lines 49–59; the rule above and the tariff rules below are cut):

evidence policy FilePolicy {
    profile "law.core.evidence-policy/0.1";
    accepts accepted;
    protects residency_proof;
    input edge edge;
    input status evidence_status;
    input authentic authentic;
    input available available;
    input current current;
    rule Accept;
}

An evidence policy is a declaration that selects which acceptance machinery governs a case. FilePolicy says: claims about residency_proof are protected (they cannot enter through a bare assertion — more on that below), acceptance is computed by the accepted relation, and the inputs plus the Accept rule feed it. A case opts into the policy by naming it in its context (evidence_policy FilePolicy); without that line, the whole pipeline stays switched off and documents remain mere transport.

Two more declarations appear only in the test scenarios. Support links a stored document to the proposition it backs: support PassDoc supports residency_proof(...) means “document PassDoc speaks for Ann’s residency”, while refutes means it speaks against it. Support alone carries nothing — it is transport, a labelled arrow from paper to claim.

Verification records that somebody actually checked: verification VPass { evidence PassDoc; ... verifier "urn:demo:northbridge:verifier"; outcome verified; ... } pins the document hash, the verifier identity and the outcome together with a timestamp.

Provenance is the recorded origin of every such step — which document, which verifier, which hashes — so that an answer can later show why a fact counts as proven rather than merely claimed.

Command and result

The register package is self-contained (its test world is the register plus vocabulary), so one command checks everything:

law test packs/examples/language-demo/register

Observed result (engine law 0.1.0):

law test demo.northbridge.register: мир demo.northbridge.register, demo.northbridge.vocabulary
  ok   [demo.northbridge.register] tests/register.lawtest / on file without a record — not a resident
  ok   [demo.northbridge.register] tests/register.lawtest / outside the domain silence is silence
  ok   [demo.northbridge.register] tests/register.lawtest / file record accepted
  ok   [demo.northbridge.register] tests/register.lawtest / key conflict: two filing dates
  ok   [demo.northbridge.register] tests/register.lawtest / policy selected, authenticity pinned
  ok   [demo.northbridge.register] tests/register.lawtest / without pinned authenticity support is rejected
  ok   [demo.northbridge.register] tests/register.lawtest / without a policy support stays transport
  ok   [demo.northbridge.register] tests/register.lawtest / bare assertion of the protected under a policy
  ok   [demo.northbridge.register] tests/register.lawtest / refuting document
итого: 9 проверено, 9 прошли, 0 не прошли, 0 не исполнены; код 0

The package also passes the static check:

law engine check packs/examples/language-demo/register/package.law

check OK: packs/examples/language-demo/register/package.law

Five of the nine tests carry this article. The first four belong to nb-06: When the register may stay silent (closure and key conflict) and are shown here only to prove the suite is green as a whole:

Test	Setup	Asks	Expects
`policy selected, authenticity pinned`	policy + evidence + support + verification	`resident_admitted`	`TRUE_ONLY`, `COMPUTED`
`without pinned authenticity support is rejected`	as above minus verification	`resident_admitted`	`NEITHER`
`without a policy support stays transport`	evidence + support + verification + five hand asserts, no policy	`resident_admitted`	`NEITHER`
`bare assertion of the protected under a policy`	bare `assert` replaces evidence + support + verification, policy on	`resident_admitted`	`NEITHER`
`refuting document`	policy + evidence + verification, `refutes` instead of `supports`	`residency_proof`	`FALSE_ONLY`

Note the last row asks a different question: residency_proof, the protected mid-chain predicate, rather than the end-of-chain resident_admitted. Its FALSE_ONLY is an accepted negative conclusion, not a failed acceptance.

All nine tests pass: each answer matched its expectation. A passing test is not a ruling in anyone’s favour — it only says the engine’s answer agreed with the test’s expect line.

The summary line is in Russian: итого: 9 проверено, 9 прошли, 0 не прошли, 0 не исполнены; код 0 — 9 checked, 9 passed, 0 failed, 0 skipped, exit code 0. The first line names the test world (мир): the register package plus the vocabulary it reads.

The admitted case works because it passes every gate: the context selects FilePolicy, PassDoc is a stored record with a content hash, support links it to residency_proof(ann), and verification VPass pins the same hash with verifier urn:demo:northbridge:verifier and outcome verified. The engine accepts the document and the ProofAdmits rule turns the protected proof into resident_admitted(ann): TRUE_ONLY.

Why this construct

The task is to decide when a filed document may promote a claim from “said on paper” to an engine-backed truth — and to keep a checkable record of every step that promotion relied on.

Splitting the pipeline into policy, support and verification keeps the three silent outcomes distinguishable. Only the first is a one-element removal: dropping the verification VPass block from the admitted case (without pinned authenticity support is rejected). The second drops the policy line while adding five hand-asserted inputs that change nothing (without a policy support stays transport). The third replaces the whole evidence chain with a single bare assertion (bare assertion of the protected under a policy). All three answer NEITHER, each for its own declared reason.

The fourth outcome runs the full pipeline with refutes instead of supports, asks the protected predicate residency_proof directly, and yields FALSE_ONLY (refuting document) — an accepted negative conclusion, not a failure. One fused “document proves claim” rule could not distinguish these four outcomes.

All five expectations (TRUE_ONLY, NEITHER, FALSE_ONLY) are executed by law test, not asserted in prose.

What is not proven: that Ann really lives in Northbridge. The tests prove the machine admits a document only through the full chain; no test can prove the paper tells the truth about the world. Residency data here is fictional, and verification checks document integrity and origin — not ground truth about where anyone sleeps.

Why not a bare assertion or a status-only rule?

A bare assert of residency_proof works for unprotected facts (the closure tests in nb-06: When the register may stay silent rely on exactly that), but the policy protects residency_proof, so assertion is no longer a lawful entry route. A plain rule deriving admission from evidence_status alone would skip the verifier pin and admit anything stamped “verified” by anyone — the authentic conjunct with its pinned verifier URN exists to close that hole.

Changed condition

Start from the admitted case (policy selected, authenticity pinned: TRUE_ONLY) and delete exactly one block — the verification VPass declaration — keeping the policy, the stored record and the support line. That is precisely the next test (without pinned authenticity support is rejected).

The answer collapses to NEITHER. Nothing about the document changed: same bytes, same hash, same link to the claim. What changed is the check: nobody with standing recorded an outcome, so the authentic conjunct of Accept has no support and acceptance never fires. The paper is still filed and still linked — support as transport survives — but transport is not proof.

The mirror change is symmetric: restore verification but drop the evidence_policy FilePolicy line from the context (without a policy support stays transport). Now even a fully verified document plus all five Accept inputs asserted by hand change nothing — the policy that would run the rule was never selected, so acceptance is never computed and the answer is again NEITHER.

Typical mistake

The mistake is asserting the protected fact directly. A newcomer who wants Ann admitted writes the shortest possible given block:

Excerpt — the bare assertion from packs/examples/language-demo/register/tests/register.lawtest line 101 (single line; indentation normalized in print).

assert "bare-proof": residency_proof(entity_ref("urn:demo:northbridge:ann")) { origin case_input; }

with the policy selected — and expects TRUE_ONLY, since the fact is right there. The observed answer is NEITHER (bare assertion of the protected under a policy).

The consequence is silent, which is what makes this mistake sharp: no error, no conflict issue, just NEITHER. Protection means the fact’s only lawful entry route is the evidence pipeline; a bare assertion of a protected predicate is discarded rather than honoured.

The fix: if a predicate appears in a policy’s protects list, stop asserting it and start filing documents — the fact must be earned through support plus verification, never injected.

Limits

Protected facts need the full chain. Policy selected, support linked, verification pinned with matching hash and verifier. The suite removes the verification and the policy in turn; each removal yields NEITHER, and hand-asserting the rule inputs changes nothing while the policy is off. There is no partial credit and no fallback to assertion for protected predicates.
Refutation is first-class. A verified document linked with refutes yields FALSE_ONLY (refuting document) — support can speak against a claim through the same pipeline, not only for it.
Support without a policy is transport only. Filed, hashed and linked documents change nothing until a case selects the policy that runs acceptance. Storage is not decision.
Verified profile: engine law 0.1.0, semantics law.core/0.2. Refusals and silent outcomes described here are facts about this profile and implementation, never claims about what the language could express in principle.

Exercise

Answer from the suite output and the test sources — no new runs needed. Predict first, then confirm with law test:

In without pinned authenticity support is rejected, which conjunct of the Accept rule loses its support, and why does the stored record plus the support line not compensate?
In without a policy support stays transport, the scenario asserts all five Accept inputs by hand (edge, evidence_status, authentic, available, current) — yet the answer is NEITHER. What single context line is missing, and what does its absence switch off?
Why does bare assertion of the protected under a policy answer NEITHER rather than raising an error — and what would change if residency_proof were removed from the policy’s protects list?
What is the status of truth(residency_proof(ann)) in the refuting document test, and which single word in the support line explains why it is FALSE_ONLY rather than NEITHER?

Checkable solution: solutions/nb-07-solutions.md.

Sources

Teaching package: packs/examples/language-demo/register/package.law (rules Accept and ProofAdmits, evidence policy FilePolicy protecting residency_proof).
Scenarios: packs/examples/language-demo/register/tests/register.lawtest (policy selected, authenticity pinned, without pinned authenticity support is rejected, without a policy support stays transport, bare assertion of the protected under a policy, refuting document).
Suite tour: packs/examples/language-demo/README.md.
Prerequisite: nb-06: When the register may stay silent; next: nb-08: Which edition applies and when the term expires.
Level 1 — Northbridge use: this article (fictional permit office; a filed certificate becomes proof only through support plus pinned verification under a selected policy).
Level 2 — domain template: whenever a claim may enter only through checked documents, protect the predicate in an evidence policy, require support plus a pinned verifier outcome for acceptance, and write one scenario per missing gate so each failure stays distinguishable.
Level 3 — confirmed external formalization: burden of proof on cancellation notification (EU Regulation 261/2004, art. 5(4)) — package eu.transport.air_passenger_rights, corpus/laws/eu/air-passenger-rights/04-cancellation.law:190-197, construct presumption with a contrary exception (PassengerUninformedUnlessCarrierProves: presume uninformed unless carrier_proved_notification(p, f) then not ...). Why this form fits: burden allocation as ground plus presumption plus a named exit — the same “who must show what, and what rebuts it” question as the FilePolicy acceptance pipeline. Evidence: docs/research/constructs/09-presumption-fiction/corpus-forms.en.md section 1 (rated exemplary there). Limit of verification: presence of the named construct at the cited lines only, confirmed by direct source read; no claim about deployment, runtime behavior, or legal correctness.

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

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