nb-01 — First permit: facts, a rule and a question

← Course mapChapter 01 / 25 · Beginner

Northbridge is fictional. All acts, documents and calendars in this course are synthetic and unofficial. Verified profile: law 0.1.0, law.core/0.2, std 0.2.0.

1. Situation

Ann moves to Northbridge and applies for a residential parking permit. The clerk checks two things: does she live in the city, and is her car registered? In this first example, meeting both conditions makes her eligible.

You will write that rule, supply Ann’s two facts, and run a test that asks whether she is eligible. Then you will see what happens when one fact is missing.

2. Prerequisites

You need basic programming knowledge and a working law CLI. No previous knowledge of Law DSL is required.

The main example uses two files you will create below. The optional package check also needs a local copy of the Northbridge Municipal Permits suite. For the full reading order, see the course overview.

3. Minimal example

Create a directory named /tmp/nb01-probe/. You will put the rule in probe.law and its tests in probe.lawtest.

Write the rule. Standalone — save this complete program as probe.law:

language "law.core" version "0.2";
package demo.probe version "0.1.0";
namespace "urn:demo:probe";

entity Applicant;
relation resident(a: Applicant) kind institutional;
relation vehicle_registered(a: Applicant) kind institutional;
relation permit_eligible(a: Applicant) kind institutional;

rule PermitEligibility strict {
    for a: Applicant;
    when resident(a) and vehicle_registered(a);
    then permit_eligible(a);
}

Applicant is the kind of entity the rule concerns. The three relations name statements about an applicant: they live in the city, their car is registered, and they are eligible for a permit. Declaring a relation does not yet say that it holds for anyone.

Read the rule from for to then: for an applicant a, when both resident(a) and vehicle_registered(a) hold, conclude permit_eligible(a). The word strict means that the rule derives its conclusion whenever all its conditions hold.

Add two test cases. Start the standalone probe.lawtest with this header:

language "law.core" version "0.2";
package demo.probe version "0.1.0";
namespace "urn:demo:probe";

Append the following tests to the same standalone file. Ann’s case supplies both facts. Bob’s supplies only his residency:

test "resident with a car is eligible" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert "resident-ann": resident(entity_ref("urn:demo:probe:ann")) { origin case_input; }
        assert "vehicle-ann": vehicle_registered(entity_ref("urn:demo:probe:ann")) { origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:probe:ann")));
    expect truth_status == TRUE_ONLY;
}
test "resident without a car is unknown" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert "resident-bob": resident(entity_ref("urn:demo:probe:bob")) { origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:probe:bob")));
    expect truth_status == NEITHER;
}

Each test has three steps:

given supplies the case. Each assert adds a fact to it.
evaluate truth(...) asks about the applicant’s eligibility.
expect states the answer the test should receive.

For Ann, TRUE_ONLY means eligibility is supported and its negation is not. For Bob, NEITHER means neither side is supported. His test name says “without a car”, but the input only says there is no car record; it does not establish that he has no car.

The remaining lines set up the test case:

entity_ref("urn:demo:probe:ann") identifies Ann. Bob has a different identifier.
context sets the legal, decision and knowledge times, plus the time zone. Keep these values as shown for this lesson.
origin case_input records that the fact came from the case input.

How this example relates to the full suite

This standalone example uses the namespace urn:demo:probe and one strict rule. Later lessons use urn:demo:northbridge and the full permits package.

In permits/package.law, PermitEligibility is defeasible: it participates in a model with exceptions and conflicting rules. Those features are introduced in nb-03: Exceptions and conflicting rules.

The suite declares Applicant, resident and vehicle_registered in vocabulary/package.law. Its test general rule: resident with a car checks both TRUE_ONLY and applied(PermitEligibility).

4. Command and result

Run the two tests:

law engine test /tmp/nb01-probe/probe.lawtest --program /tmp/nb01-probe/probe.law

Recorded output (2026-10-02):

test PASS: resident with a car is eligible
test PASS: resident without a car is unknown
lawc test: 2/2 тестов прошли

Both tests pass: Ann’s answer is TRUE_ONLY, and Bob’s is NEITHER. A passing test means the answer matches its expectation; it does not mean that every applicant is eligible.

The summary is in Russian and says that 2 of 2 tests passed. It names lawc because that is the runner behind law engine test.

Optional: check the full permits package

From the repository root, run:

law test packs/examples/language-demo/permits

The recorded run (2026-10-02) includes ok [demo.northbridge.permits] tests/permits.lawtest / general rule: resident with a car and the total 28 проверено, 28 прошли, 0 не прошли — 28 tests passed, none failed. This package includes scenarios beyond the two-file example.

5. Why this construct

Ann meets both conditions: she is a resident, and her car is registered. In this example, those two facts are enough to establish eligibility. A strict rule expresses that relationship directly.

The first test checks the answer: TRUE_ONLY. To also check that PermitEligibility produced it, use expect applied(PermitEligibility);. The full suite’s first test includes that check. Section 7 shows why it matters.

Why not another construct?

A definition gives a condition a reusable name. Here we need a rule that derives a new statement about eligibility.
A classification assigns something to a kind. Here we are deriving eligibility from two facts about an applicant.
A defeasible rule allows its conclusion to be defeated. This example has no exceptions or competing rules; the full permits model introduces them in nb-03.

6. Changed condition

Now look at Bob’s test. His residency is recorded, but his car registration is not. The rule needs both facts, so it does not fire.

The result is NEITHER. No rule in this example establishes Bob’s eligibility, and none establishes that he is ineligible. The missing record therefore leaves the question unanswered; it does not produce a refusal.

nb-02: Why a missing fact is not a refusal explores that distinction and the other truth statuses.

7. Typical mistake

Suppose you assert Bob’s eligibility directly, then ask whether he is eligible. You get TRUE_ONLY, but that tells you nothing about whether the rule works: you supplied the answer yourself.

To expose the mistake, append this third test to the standalone probe.lawtest and run the same command. This test is meant to fail. It asks for evidence that the rule fired, although neither of the rule’s input facts is given. The test needs the file header from section 3; it is not runnable alone.

test "asserting the conclusion fires no rule" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
        assert "eligible-bob": permit_eligible(entity_ref("urn:demo:probe:bob")) { origin case_input; }
    }
    evaluate truth(permit_eligible(entity_ref("urn:demo:probe:bob")));
    expect applied(PermitEligibility);
}

The recorded result is test FAIL: asserting the conclusion fires no rule. The diagnostic applied(urn:demo:probe#PermitEligibility): в документе нет says that the rule’s application is absent from the result.

To test the rule successfully, supply both input facts, as Ann’s test does, and check both TRUE_ONLY and applied(PermitEligibility). Keep Bob’s missing-record test expecting NEITHER: that case should not require the rule to fire.

Remove the deliberately failing test after trying it. When testing a rule, supply its inputs and let the rule derive the conclusion.

8. Limits

This example shows one strict rule, two input facts and a question about eligibility. It also shows what happens when one required fact is missing.

The assertions are inputs, not proof that Ann really lives in Northbridge. The rule is fictional, and the tests do not establish its legal validity. Fixed timestamps make the tests reproducible; the example does not model how eligibility changes over time.

The full permits package adds fines, suspension and fraud through FinesRefusal, FraudBlocksBadge and the unless clause on PermitEligibility. This lesson’s rule does not handle those cases.

Where the course adds the remaining pieces

nb-02: missing and conflicting information.
nb-03: exceptions, priorities and defeaters.
nb-04: computed amounts.
nb-05: aggregates.
nb-06: when a register may treat absence as a negative.
nb-07: evidence and provenance.

9. Three levels

In Northbridge: residency and car registration establish eligibility in our simplified rule. The full permits package adds exceptions to that initial check.

As a reusable pattern: use a strict rule when the stated conditions are sufficient to derive a conclusion without exceptions. For example, a rule might derive a status from a filing and a paid fee. If the wording adds “unless” or introduces a conflicting rule, revisit the model.

In another formalization: the repository’s Civil Code of Kazakhstan package uses a strict rule to derive natural-person qualification. It shares the pattern of deriving a conclusion from stated conditions, though its rule has a single condition rather than our two.

Sources and scope of verification

The external example is CitizenForeignCitizenOrStatelessPersonIsNaturalPerson in kz.corpus.civilcode, at corpus/laws/kz/codes/civil-code/02-natural-persons.law:85-96. It uses rule ... strict, a header-bound variable and a single-literal body. The strict-rule research notes (section 1) document the example.

The recorded verification confirms the construct’s presence in the source. It does not establish runtime behavior, deployment or legal correctness.

Within the training suite, BigBill and CentralPays in queries/package.law also use strict rules to derive billing statements. The recorded run of law test packs/examples/language-demo/queries reports 6 проверено, 6 прошли, 0 не прошли — six tests passed.

10. Exercise

Reverse the missing-record case: Ann has a registered car, but her residency is not recorded.

Predict the status of her eligibility.
Write a test with only the car-registration fact in given.
Ask about her eligibility with evaluate truth(...) and add your expected status.
Run it against probe.law using the command from section 4.

Check your work against the full solution: test, command and result.

11. Links

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

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