First package: from rule to answer

Dana sent Aigerim a model of access to the rare collections and an example of its application. Researcher Ivanova is listed in the registry, and her accreditation is valid. Under the archive rule she may enter the room. Aigerim wants to check how this conclusion follows from the record Dana prepared.

First she will repeat the example unchanged. Then she will remove the accreditation evidence and ask the same question. If access can no longer be established, will that mean Ivanova was refused?

We will carry out both checks together with her. The Archive of Veliky Ustin, its rules, and the people in the story are fictional; the example is given in full on this page. If you want to run it right away, go to the “Run” section.

Question: does access follow from this evidence?

The archive rule requires two conditions: the reader must be listed in the researcher registry and hold a valid accreditation. About Ivanova we know both. That should be enough to conclude access. We do not add the conclusion itself to the input evidence: the check has to derive it by the rule.

First, let us write down the expected answers in plain words:

Evidence about Ivanova	Expected answer about access
Registry entry and a valid accreditation	Established
Registry entry; no accreditation evidence	Neither established nor refuted

In the second row, evidence of accreditation is missing for the conclusion. At the same time, nothing in our example states that Ivanova was refused. We cannot yet justify either access or its denial. Below we will see how Arxo denotes these answers.

Record: the rule

This page can be passed to the compiler as a package source file. It reads together all blocks marked law and skips the explanations between them. So there is no need to move the code into a separate file to check the example.

Let us start with the rule itself. The variable p denotes the person in question; Person states its type. After when come two conditions joined by and. After then stands the conclusion that follows when they hold.

Arxo Law

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

RareRoomAccess is the rule name: by it we will recognise this rule in the explanation of the answer. The strict marker sets a strict rule. There are no exceptions or priorities in our example yet.

The names in_researcher_registry, accredited, and may_enter_rare_room denote three relations: a person is listed in the registry, is accredited, and is admitted to the room. Their full declarations are in the “Record, continued” section below. First we will get the answer, then return to the structure of the package.

The @source(ARCHIVE_RULES_P4) reference points to the fragment of the archive rules, which is also given at the end of the page. Compare the record after when with the Russian phrase: both must keep the two conditions required at the same time.

Run: get the answer

To run it you will need a copy of the repository and Rust with Cargo installed. Open a terminal at the repository root and run the commands below. Run all later commands in the same terminal window: it will keep the directory and file names we are about to set. The first run may take some time to build.

Terminal

cd engines/lawc
tutorial_dir=../../docs/tutorials
tutorial_page="$tutorial_dir/01-first-package.en.law.md"
cargo run -q --profile gate -p law-cli -- check \
    "$tutorial_page"
tutorial_work=$(mktemp -d)
cargo run -q --profile gate -p law-cli -- lower \
    "$tutorial_page" > "$tutorial_work/program.lawir.json"

The check command verifies that the package is written correctly: whether the names used are declared, whether the types agree, and whether the source text matches the pinned hash. The lower command prepares the program for running and saves it into a temporary directory.

Warning LDC-E1314 means that tests are not part of the program itself. Their evidence and expectations are used only when checking concrete cases. That is why below we will pass the program and the test as separate command arguments.

Now let us state the evidence about Ivanova and the question of her access. For this we use a test. The given section lists what is given; the evaluate line states the question; the expect line states the expected answer. The first row of our table corresponds to the designation TRUE_ONLY: the statement is established, with no grounds to deny it.

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 truth_status == TRUE_ONLY;
}

The test name reads: “Ivanova: registry and accreditation grant access.”

Two assert records state that Ivanova is listed in the registry and holds an accreditation. Both use the same reference entity_ref("urn:tutorial:ivanova"), so they speak about one person. Each record has its own id name; the origin case_input marker means the evidence is entered as input data of this case.

The context section fixes the date on which we ask the question, the moment of decision, the moment bounding our evidence, and the time zone. We will examine these distinctions in detail in the chapter on time. For now we keep the context the same in both experiments, so that only one change is tested.

A ready-made test for this case ships with the tutorial. The first command runs the check, and the second shows the explanation of the answer:

Terminal

cargo run -q --profile gate -p law-cli -- test \
    "$tutorial_dir/tests/01-with-accreditation.lawtest" \
    --lawtest --program "$tutorial_work/program.lawir.json"
cargo run -q --profile gate -p law-cli -- explain \
    "$tutorial_dir/tests/01-with-accreditation.lawtest" \
    --program "$tutorial_work/program.lawir.json"

A test PASS message means the answer obtained matched the expected TRUE_ONLY. In the explanation, find the RareRoomAccess rule and the two records: Ivanova’s registry entry and her accreditation. Together they allow the access conclusion to be derived.

The expect line is there to compare the result with our expectation. It adds no facts and does not affect the derivation. Had we entered the access itself into the input evidence in advance, such an example would not show whether the rule can derive it from the two conditions.

Practice: change one ground

Now prepare the second case yourself. Copy the first test into a temporary directory:

Terminal

tutorial_try=$(mktemp -d)
cp "$tutorial_dir/tests/01-with-accreditation.lawtest" \
    "$tutorial_try/try.lawtest"

Open the try.lawtest file in the created directory. Delete from it the whole assert accredited(...) { … } block, including the id and origin lines inside the braces. Keep the registry record, the question, and the TRUE_ONLY expectation unchanged. Before running the test, explain why the previous answer should no longer be obtained.

Terminal

cargo run -q --profile gate -p law-cli -- test \
    "$tutorial_try/try.lawtest" \
    --lawtest --program "$tutorial_work/program.lawir.json"

The check should finish with a FAIL message: we expected TRUE_ONLY but got NEITHER. The second designation means “neither established nor refuted”. The accreditation evidence is gone, so the rule no longer allows access to be derived. No grounds for a negative conclusion appeared in our example either.

Now correct the expectation to NEITHER and repeat the command. The test should pass. We changed the expectation for a clear reason: one of the necessary conditions is no longer confirmed. In other tasks, an unexpected result likewise needs to be explained first; simply replacing the expectation with the obtained answer would drain the test of meaning.

A ready-made solution ships with the tutorial. Compare your record with it. Then try adding a rule yourself in the two-reading-rooms exercise.

Record, continued: vocabulary and source

Let us return to those parts of the package that were needed for the run but have so far been left without a detailed explanation.

At the start of the record come the language and its version, the package name and version, and the namespace. It lets same-named designations from different packages be told apart. The language version and the version of the particular package are stated separately.

Arxo Law

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

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;

The entity Person line declares the type of objects — people. Each relation line introduces a relation that can be used in statements and rules. The p: Person parameter states that this relation concerns a person.

The institutional marker means the relation is tied to an institutional status or decision. In this example accredited reports a valid accreditation on the date of the question. We do not yet compute its period of validity: the needed evidence is already given in the setup. More about objects and ways of describing them can be read on the vocabulary page.

It remains to state the source of the rule. This takes three declarations: source names the document, edition its edition, fragment the fragment we used. The @source reference before the RareRoomAccess rule leads exactly to this fragment.

Arxo Law

source ARCHIVE_RULES {
    kind municipal_act;
    jurisdiction VELIKY_USTIN;
    number "2026-14";
}

edition ARCHIVE_RULES_2026_RU of ARCHIVE_RULES {
    language ru;
    officiality official;
    adopted @2026-01-15;
    in_force [@2026-02-01, infinity);
}

fragment ARCHIVE_RULES_P4 in ARCHIVE_RULES_2026_RU {
    kind paragraph;
    locator "paragraph/4";
    text ru official """Читатель допускается в зал редких фондов, если он состоит в реестре
исследователей и имеет действующую аккредитацию.
""";
    content_hash "sha256:7f76a4311e52b9af58fcf3175f613794316583ae19c4f0767d0570774a456688";
}

The quoted act text reads: “A reader is admitted to the rare-collections room if listed in the researcher registry and holding a valid accreditation.”

Here the edition was adopted on 15 January 2026 and is in force from 1 February inclusive. No end date is set. These dates, like the official marker, belong to the fictional rules of the teaching archive.

The content_hash field holds the hash of the text. During checking it is recomputed and compared with the recorded value. Exact bytes count, including line breaks. This is how a changed fragment can be detected. The hash does not confirm that we read it correctly: the meaning of the Russian phrase and of the recorded rule must be compared separately. We will return to working with documents and editions in the lesson about the real source.

Acceptance: what you can check yourself

Before moving on, make sure you can repeat the experiment and explain its result.

• With both pieces of input evidence present, access is established: the answer is TRUE_ONLY.
• After removing the accreditation evidence, the answer changes to NEITHER.
• If the previous expectation is kept, the test fails.
• In the explanation of the first answer, the rule and both of its premises are visible.
• The access statement itself is absent from the input evidence.

Also check how a change of the source is detected. Make a copy of the page and replace in the fragment text «зал редких фондов» (“rare-collections room”) with «зал редкого фонда», keeping the same content_hash. Run the check command for that copy. It should report an LDC-E5201 error: the hash of the changed text does not match the recorded one. After the experiment, restore the original phrase.

Boundary: what this answer does not yet establish

Aigerim managed to repeat Dana’s result and found out which evidence it needs. But in this experiment we did not check the authenticity of the pass, the completeness of the registry, or the actual visit to the archive. Established access alone does not mean Ivanova has already entered the room. Such questions will need other evidence and rules.

We also saw that removing the accreditation evidence changes the answer about access but does not turn it into a refusal. If there are not enough grounds for a conclusion, that does not yet give grounds for its denial.

So far we have needed two designations: TRUE_ONLY and NEITHER. What happens with a negative statement or a contradiction is covered in the lesson “Four states of support”.