Markdown for LLMs
nb-12 — Allocation in rounds
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-12 — Allocation in rounds
*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](/tutorials/northbridge/nb-01-first-permit/) for facts,
strict rules, and `law test` as the way to check a claim;
[nb-02: Why a missing fact is not a refusal](/tutorials/northbridge/nb-02-missing-fact/) for
the four truth statuses, where `NEITHER` means "no conclusion either
way" and never a refusal; and
[nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/) 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](/tutorials/northbridge/nb-10-parallel-procedure/).
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.
```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.
```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.
```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.
```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.
```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:
```sh
law test packs/examples/language-demo/allocation
```
Observed result (tool `law 0.1.0`):
```text
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:
```sh
law engine check packs/examples/language-demo/allocation/package.law
```
```text
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](/tutorials/northbridge/nb-01-first-permit/) through
[nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/) 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](/tutorials/northbridge/nb-10-parallel-procedure/)
— 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](/tutorials/northbridge/solutions/nb-12-solutions/).
## 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](/tutorials/northbridge/nb-01-first-permit/); see
also: [nb-10: A procedure with parallel
checks](/tutorials/northbridge/nb-10-parallel-procedure/) (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.
<details>
<summary>Sources and scope of verification</summary>
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.
</details>