nb-12 — Allocation in rounds

← Course mapChapter 12 / 25 · Advanced

Minimal exampleCommand and resultExercise

Northbridge is fictional. Every applicant, seat, point score and register entry below is synthetic and unofficial. Northbridge is an invented town used only to teach Law DSL. No real municipal deployment or legal-validity claims. Verified profile: law 0.1.0, law.core/0.2.

Situation

Northbridge has 40 trading seats on the renovated market square and 60 applicants. The permit office allocates the seats in two rounds. Round 1 shortlists every applicant the residents register already knows. Round 2 admits each shortlisted applicant whose merit score reaches the published threshold — and only then does the office read the closed total and announce that allocation is done.

The order matters, and it must be frozen: round 2 may look back at the finished round 1, but nothing in round 2 may rewrite it. A clerk who runs both rounds as one undated pile risks admitting someone round 1 never shortlisted. Law DSL expresses this frozen order as a stage: a named declaration that evaluates indexed rounds in order, closing each round before the next one reads it.

Prerequisites

You need nb-01: First permit: facts, a rule and a question for facts, strict rules, and law test as the way to check a claim; nb-02: Why a missing fact is not a refusal for the four truth statuses, where NEITHER means “no conclusion either way” and never a refusal; and nb-03: Exceptions and conflicting rules for strict rules and how conflicts resolve. The parallel-checks procedure package returns as a contrast in Sources; procedures in full are nb-10: A procedure with parallel checks.

The new words all describe the allocation. The frozen round order is a stage. One round of a stage is a tour — the course calls tours “rounds”. The index counts the tours, and bind pins each relation to its tour index. Reading a fact from an already-closed tour is supported. The world is the set of packages evaluated together, pinned in the package’s law.toml. Each word is explained again where it first appears below.

Minimal example

All fragments are excerpts from packs/examples/language-demo/allocation/package.law (identifiers as written; header, imports and neighbouring declarations cut).

Excerpt 1 — the stage itself (lines 14–18). A stage names the round order: index round counts tours from 1 to 2, and each bind pins one relation to tour index 2, meaning that relation’s content is fixed at that tour.

Arxo Law

stage Allotment {
    index round: Integer from 1 to 2;
    bind shortlisted index 2;
    bind admitted index 2;
}

Look at the three lines inside the block. The index line counts tours from 1 to 2, and each bind pins one relation to tour index 2: that relation’s content is fixed at that tour. Two tours exist, in order, and the shortlist and the admission list are tour-bound — round 2 reads a closed round 1, never an open pile.

Excerpt 2 — the vocabulary of the rounds (lines 20–25). MIN_POINTS is an ordinary integer constant: the published merit threshold. The three relations carry the round number alongside the applicant, so round 1 and round 2 facts never mix.

Arxo Law

const MIN_POINTS: Integer = 5;

relation points(a: Applicant, p: Integer) kind empirical;
relation shortlisted(a: Applicant, r: Integer) kind institutional;
relation admitted(a: Applicant, r: Integer) kind institutional;
relation allocation_done() kind institutional;

Look at the kind tags. points is empirical input — supplied with the case. shortlisted, admitted and allocation_done are institutional — the rules produce them. The round number travels alongside the applicant in each relation, so round 1 and round 2 facts never mix.

Excerpt 3 — seeding round 1 from the register (lines 27–31). No supported here: round 1 reads the live register, the world outside the stage.

Arxo Law

rule Seed strict {
    for a: Applicant;
    when demo.northbridge.register::resident_admitted(a);
    then shortlisted(a, 1);
}

Look at the when line: it reads the live register, the world outside the stage — no supported here. Residency in the register shortlists the applicant at tour 1. That shortlisting is the seed everything later depends on.

Excerpt 4 — round 2 admits by points (lines 33–39). supported is the tour-closing read: supported(shortlisted(a, r)) is true only for a shortlist fact from an already-closed tour. The guard r < 2 keeps the step inside the stage, and r + 1 stamps the admission at the next tour.

Arxo Law

rule Admit strict {
    for a: Applicant;
    for p: Integer;
    for r: Integer;
    when supported(shortlisted(a, r)) and r < 2 and points(a, p) and p >= MIN_POINTS;
    then admitted(a, r + 1);
}

Look at the when line conjunct by conjunct. supported(...) is the frozen read — true only for a shortlist fact from an already-closed tour. r < 2 keeps the step inside the stage, and r + 1 in the head stamps the admission at the next tour. Admission needs three things at once: a frozen shortlisting, a tour that still has a successor, and enough points.

Excerpt 5 — reading the closed total (lines 41–46). Again supported: the office announces completion only on the strength of an admission from a closed tour.

Arxo Law

rule CloseAllocation strict {
    for a: Applicant;
    for r: Integer;
    when supported(admitted(a, r));
    then allocation_done();
}

Look at the when line once more: supported again. The office announces completion only on the strength of an admission from a closed tour. The top-level result reads the closed rounds — never the case input directly.

Command and result

Run the allocation suite:

Terminal

law test packs/examples/language-demo/allocation

Observed result (tool law 0.1.0):

Output

law test demo.northbridge.allocation: мир demo.northbridge.allocation, demo.northbridge.register, demo.northbridge.vocabulary
  ok   [demo.northbridge.allocation] tests/allocation.lawtest / round 1 shortlists from the register
  ok   [demo.northbridge.allocation] tests/allocation.lawtest / rounds are empty without seed
  ok   [demo.northbridge.allocation] tests/allocation.lawtest / round 2 admits by points
  ok   [demo.northbridge.allocation] tests/allocation.lawtest / insufficient points — no seat granted
  ok   [demo.northbridge.allocation] tests/allocation.lawtest / closed total reads after the rounds
итого: 5 проверено, 5 прошли, 0 не прошли, 0 не исполнены; код 0

All five tests pass: each answer matched its expectation. That says the machine enforces the round order as declared — it is not a ruling that any applicant deserves a seat. The first line names the world under test: the allocation, register and vocabulary packages pinned in the allocation package’s law.toml. The summary line is in Russian and says that 5 tests were checked, 5 passed, none failed and none were left unexecuted, with exit code 0.

The package also passes the static check:

Terminal

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

Output

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

check OK means the package file is well-formed; the suite run above is what exercises its behavior.

What the decisive tests assert (all ask truth(...) of a tour-stamped fact):

Test	Setup	Expects
round 1 shortlists from the register	Ann filed as resident	shortlisted(ann, 1) TRUE_ONLY, applied(Seed)
rounds are empty without seed	Ann has 10 points, no filing	admitted(ann, 2) NEITHER
round 2 admits by points	Ann filed, 10 points	admitted(ann, 2) TRUE_ONLY, applied(Admit)
insufficient points — no seat granted	Bob filed, 3 points	admitted(bob, 2) NEITHER
closed total reads after the rounds	Ann filed, 10 points	allocation_done() TRUE_ONLY, applied(CloseAllocation)

Why this construct

The task is to allocate in frozen rounds — seed from the register, admit by threshold from the frozen seed, read the closed total — with the round order enforced by the machine, not by clerk discipline. Only the stage closes a tour. supported(...) reads exclusively from closed tours, so Admit provably sees the finished round 1 and nothing that round 2 is still deriving. No other construct freezes an intermediate result this way.

A plain chain of strict rules in the style of nb-01: First permit: facts, a rule and a question through nb-03: Exceptions and conflicting rules derives everything in one pass. It has no notion of a “finished round”, so it cannot stop round 2 from seeing half-derived round 1 facts. A procedure — the StationApproval automaton from nb-10: A procedure with parallel checks — tracks an event-driven case through states: filed, reviewed, approved. But states are not tours: a procedure never closes a derivation round for later rules to read. Rules derive, procedures advance, stages stratify.

The proof is the five tests above, executed by law test, not asserted in prose. The empty-rounds test is the sharpest: Ann’s 10 points alone admit nobody — without the seed, round 1 closes empty and round 2 reads exactly that emptiness (NEITHER). What the tests do not prove is that two rounds and a threshold of 5 are fair or lawful. The tests prove the machine enforces the declared round order; no test can prove Northbridge chose the right order. All scores and seats are fictional data, not legal advice.

Changed condition

Take the admitting round-2 test and change one condition: Ann’s 10 points become Bob’s 3 — everything else identical (filing on record, same tour, same threshold).

With 10 points (round 2 admits by points), truth(admitted(ann, 2)) is TRUE_ONLY and the run records applied(Admit): frozen shortlist plus p >= MIN_POINTS, so the admission fires. With 3 points (insufficient points — no seat granted), the same query is NEITHER. The shortlist is still frozen and readable, but the threshold conjunct fails, so the rule derives nothing. One number, two outcomes — and the difference sits in the threshold comparison, not in the round machinery, which behaves identically in both tests.

The same one-change logic governs the seed. round 2 admits by points versus rounds are empty without seed differ only in whether the resident filing is asserted. Ten points with the seed admit; ten points without it leave admitted(ann, 2) NEITHER. The engine never invents a shortlist from points alone.

Typical mistake

A natural mistake is to assert strong round-2 input and expect admission without the round-1 seed: “Ann has 10 points, well above the threshold — surely she is admitted.” She is not. The rounds are empty without seed test asserts exactly those 10 points and still returns NEITHER. Admit reads supported(shortlisted(a, r)) — a closed tour — and with no filing, round 1 closed empty. Points qualify a shortlisted applicant; they never create the shortlisting.

Admission needs all three at once: the seed (the register filing feeding Seed), the frozen read (supported over a closed tour), and the threshold (p >= MIN_POINTS). Remove any one and admitted(a, 2) stays NEITHER. If you want points alone to admit, write that rule — but then say so, because this suite will hold you to the staged version.

Limits

Closed tours read only backwards. supported(...) sees finished tours; a rule can never support-read its own open tour. Round 2 observes round 1 precisely because round 1 already closed.

One program, one stratification. A package with a stage cannot also hold a procedure: a scratch package combining the Allotment stage with a minimal two-state procedure was refused at check time with error LDC-E4126: STAGE_PROCEDURE_UNSUPPORTED. The round fold the stage needs is undefined next to a procedure automaton, so the implementation rejects the combination outright.

The world is separate by design. The allocation world’s pinned set is demo.northbridge.allocation, demo.northbridge.register and demo.northbridge.vocabulary — the world list in packs/examples/language-demo/allocation/law.toml, matching the law test header line. The procedure package is nowhere in it, by no direct or transitive dependency, so round semantics can never leak into, or be disturbed by, procedure states.

Five things, not one. The tool version (law 0.1.0, from law --version), the language version (law.core version 0.2, the header line of package.law), the semantics (law.core/0.2, reported by the same command), the implementation support (the LDC-E4126 refusal and the supported closed-tour read are facts about this engine profile), and the observed run (5 checked, 5 passed) are separate claims. A newer tool could keep the language version and still change what the implementation supports — re-run the suite before assuming otherwise.

Verified profile: tool law 0.1.0, semantics law.core/0.2. The tour vocabulary (stage, index, bind, supported) is a fact about this profile’s implementation, never a claim about the language in general.

Exercise

Without running the engine, predict, then check with law test:

1. In round 2 admits by points, which single asserted fact, if removed, turns admitted(ann, 2) from TRUE_ONLY to NEITHER while leaving the 10 points untouched — and which test already proves that outcome?
2. Bob’s 3 points fail the threshold. Exactly which comparison in Admit fails, and what score is the smallest that would flip admitted(bob, 2) to TRUE_ONLY?
3. In closed total reads after the rounds, why does CloseAllocation read supported(admitted(a, r)) rather than the case input — what would go wrong if it concluded allocation_done() directly from points(a, p)?
4. What happens if you add a procedure block to the allocation package — at which command does it fail, and with which error code?

Write down each prediction first; run the suite; explain any miss in one sentence. Checkable solution: full solution: predictions and checkable answers.

Sources

• Source: packs/examples/language-demo/allocation/package.law (stage Allotment, rules Seed, Admit, CloseAllocation)
• Tests: packs/examples/language-demo/allocation/tests/allocation.lawtest (the five round/close tests)
• Suite tour: packs/examples/language-demo/allocation/README.md; world pin: packs/examples/language-demo/allocation/law.toml
• Language reference: docs/language/09-advanced-cheat-sheet.law.md (the Stages section: tours close in order; a package with a stage cannot also hold a procedure), docs/language/06-testing-a-package.law.md (the law test reference)
• Prerequisite: nb-01: First permit: facts, a rule and a question; see also: nb-10: A procedure with parallel checks (procedures in full)

Three levels:

1. Northbridge use (this article): two-round seat allocation — register seed, points threshold, closed total — verified by the five tests above.
2. Domain template: whenever a regime decides in frozen rounds, model each round as one tour of a stage, stamp every round fact with its tour index, cross tour boundaries only with supported, and read the final total only from closed tours — never from case input.
3. Confirmed example elsewhere: the procedure package, where an event-driven automaton (not tours) advances a charging-station approval through parallel document and technical regions — verified by law test packs/examples/language-demo/procedure (6 checked, 6 passed, 0 failed), including both regions ready — decision taken (TRUE_ONLY once both regions accept) and join waits for both regions (one region alone decides nothing). Procedures advance cases; stages freeze rounds — exactly as the limits say. Confirmed external formalization: ranked-choice counting rounds (Maine, US) — package us.me.ranked_choice, corpus/laws/us/maine-ranked-choice/02-procedures.law:140-161, construct stage with a bounded index and per-round binds.

Sources and scope of verification

The Maine example is CountingRounds, with index r: Integer from 1 to 32 and nineteen binds: each round is one tour of a stage, with every round fact stamped by its tour index — this article’s frozen-rounds template at full scale. Evidence: docs/research/constructs/23-stage/corpus-forms.en.md, section 1 (rated exemplary there). The recorded verification confirms the construct’s presence at the cited lines only, by direct source read; it makes no claim about deployment, runtime behavior, or legal correctness.