# 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

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

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

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

```bash
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
```

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

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

```text
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/](/tutorials/exercise-writing-tests/).