A test in the language of law: .lawtest files

All checks in the previous tutorials lived outside the language: an external check assembled a case, called the engine, and compared the status. It works — but such a check is read by a programmer. The lawyer who signs the formalisation will not read it and will not be able to verify it.

The test form closes exactly this gap: the test is written in the same language as the norm and speaks the same words — which facts are given, what is asked, which answer is expected.

Program

Arxo Law

language "law.core" version "0.2";
package tutorial.archive.tested version "0.1.0";
namespace "urn:law:tutorial:archive:tested";

entity Person;

relation in_researcher_registry(p: Person) kind institutional;
relation accredited(p: Person) kind institutional;
relation may_enter_rare_room(p: Person) kind institutional;

rule RareRoomAccess strict {
    for p: Person;
    when in_researcher_registry(p) and accredited(p);
    then may_enter_rare_room(p);
}

Test

Arxo Law

test "аккредитованный исследователь допускается в зал редких фондов" {
    given {
        context {
            decision_time @2026-03-01T09:00:00+05:00;
            knowledge_time @2026-03-01T09:00:00+05:00;
            legal_time @2026-03-01;
            timezone "Asia/Almaty";
        }

        assert in_researcher_registry(entity_ref("urn:tutorial:ivanova")) {
            id "assert-reg";
            origin case_input;
        }
        assert accredited(entity_ref("urn:tutorial:ivanova")) {
            id "assert-acc";
            origin case_input;
        }
    }

    evaluate truth(may_enter_rare_room(entity_ref("urn:tutorial:ivanova")));

    expect result_kind == PROPOSITION;
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

The test name reads: “An accredited researcher is admitted to the rare-collections room.”

The three parts read in sequence like a problem statement: given is the case (context and statements), evaluate the question, expect the expected fields of the result.

Note the context: four technical axes are declared explicitly. Without them the engine substitutes defaults and writes about it in the report — a test depending on defaults checks something other than what you meant.

The id and origin on each statement are not decoration: they travel into the proof. When the answer comes back wrong, you will want to know exactly which fact produced it.

A case does not change law

The test lies next to the norm but does not become a norm. Compile this page and the compiler will say so directly:

Output

warning LDC-E1314: тест "…" не входит в программу пакета: §267 описывает вход
и ожидание, а не норму; узел в CLIR не порождается

The warning reads: ‘test ”…” is not part of the package program: it describes input and expectation, not a norm; no CLIR node is produced’.

This is the separation in action: a case may not change law rules. Hence the run form: the program is presented as a separate argument, not taken from the same file:

Terminal

cargo run -q -p law-cli -- lower ../docs/tutorials/06-writing-tests.en.law.md > /tmp/program.lawir.json
cargo run -q -p law-cli -- test ../docs/tutorials/tests/06-rare-room-access.lawtest \
    --lawtest --program /tmp/program.lawir.json

Output

test PASS: аккредитованный исследователь допускается в зал редких фондов
lawc test: 1/1 тестов прошли

The output reads: ‘test PASS: an accredited researcher is admitted to the rare-collections room; 1/1 tests passed’.

The .lawtest file next to the page carries the package header and the very same test block you read above — the runner requires a byte-for-byte match. The runner finds tests by extension, hence a separate file is needed; but you read and it executes one and the same thing.

The expectation vocabulary

After expect stands not an arbitrary expression but a comparison of a result field against a value from its vocabulary. There are seven fields, six of them enumerable:

Field	Vocabulary	Values
truth_status	TruthStatus	TRUE_ONLY, FALSE_ONLY, BOTH, NEITHER
result_kind	ResultKind	DATA, COLLECTION, PROPOSITION, RULE_APPLICATION, NORM_POSITION, COMPLIANCE, CONSTRAINT, GRAPH
applicability_status	ApplicabilityStatus	APPLICABLE, NOT_APPLICABLE, UNDETERMINED, CONFLICTED
trigger_status	TriggerStatus	SATISFIED, NOT_SATISFIED, UNDETERMINED, CONFLICTED
evaluation_status	EvaluationStatus	COMPUTED, MISSING_INPUT, MISSING_POLICY, REQUIRES_JUDGMENT, NON_EXECUTABLE, … (14 values)
normative_status	NormativeStatus	CREATED, PENDING, ACTIVE, SATISFIED, VIOLATED, WAIVED, … (15 values)
value	—	no vocabulary: this is DATA, any term arrives here

The lists live in the evaluation schema and are built into the compiler from the same place — there are deliberately no copies of the list in code, otherwise two copies would diverge at the first added status.

This vocabulary is not found in the grammar itself, which knows only "expect", pure_expression, ";". That is why it is absent from the keyword reference too — terminals live there, and truth_status is not a terminal.

When a test fails

The report names the field, the expectation, and what stands in the document:

Output

test FAIL: аккредитованный исследователь допускается в зал редких фондов
  truth_status == FALSE_ONLY: в документе TRUE_ONLY

The output reads: ‘test FAIL …; truth_status == FALSE_ONLY: the document holds TRUE_ONLY’.

That is enough to see the cause without rerunning by hand — across a corpus of two and a half hundred tests the property is no luxury.

One trap. A typo not in the expectation but in the value itself — TRUE instead of TRUE_ONLY, DEFINITELY_YES instead of anything — gives something else:

Output

lawc: …/06-rare-room-access.lawtest: тест не лоуверится

The output reads: ‘…the test does not lower’.

No code, no line, no word it disliked. Inside the compiler such an error is called LDC-E1319, “expectation value outside the result-field vocabulary”, but that code never reaches the user — neither in normal mode nor under --json. Until it does, check against the table above.

Where this works for real

Corpus regression scenarios are written in the same test form. They run package by package with a ratchet on the count: a dropped scenario would shrink both numerator and denominator, and “N/N PASS” would print at a smaller N.

The point of these checks is not that regression is green — it is green without them. The point is that the same scenarios, written as a lawyer will read them, give the same answers. Were they to diverge, the test form would speak about law something other than what the engine speaks.

Properties over a finite domain

property_decl already has an AST, lowering, and execution through the same test run: a test file, the test flag, and a prepared program. A property is not part of programHash: for the check the compiler builds observer rules, and the runner prints the domain size, counterexamples, and unexecuted checks.

The v1 slice is deliberately narrow: the first forall executes, the domain must have the collect v: T where … form, and the expectation must be a single atom or comparison. Multiple binders, arbitrary generation/seed, and composite expectations are not yet supported; the boundary is returned as a diagnostic, not a silent skip.

Next step: check the test’s strength by mutation

A green .lawtest confirms the expected example but does not yet prove the decisive premise really affects the answer. Mutation testing deliberately spoils a boundary, a binding, or a fail-closed guard and requires the named test to turn red on an observable legal result.

The practical model keeps an ordered list of operators for adding a new witness; mutation testing is covered in its own guide in the repository.

The exercise for this page is /tutorials/exercise-writing-tests/.