# nb-12 solutions — Allocation in rounds *Checkable against `law test packs/examples/language-demo/allocation` (5 checked, 5 passed). Identifiers and code as written.* ## 1. Which single fact turns admission to NEITHER **Answer: the resident filing; the `rounds are empty without seed` test already proves the outcome.** The admitting test asserts two inputs: the register filing (via `demo.northbridge.register::filed_resident`) and the 10 points. `Admit` needs `supported(shortlisted(a, r))` — a frozen round-1 shortlisting that only `Seed` can produce, and `Seed` fires only on the filing. Remove the filing and round 1 closes empty, so the `supported` conjunct fails and `admitted(ann, 2)` is NEITHER no matter how many points are asserted. The empty-rounds test is exactly that configuration (10 points, no filing → NEITHER). ## 2. The failing comparison and the smallest passing score **Answer: `p >= MIN_POINTS` fails with p = 3 against MIN_POINTS = 5; the smallest flipping score is 5.** With `points(bob, 3)`, the conjunct `p >= MIN_POINTS` instantiates to `3 >= 5`, which is false, so `Admit` derives nothing and `admitted(bob, 2)` stays NEITHER. The comparison is `>=`, not `>`, so 5 already satisfies it: re-asserting `points(bob, 5)` with the filing kept would make all three conjuncts true (frozen shortlist, `r < 2`, threshold met) and flip the query to TRUE_ONLY with `applied(Admit)`. ## 3. Why the closed total reads closed tours, not input **Answer: reading input directly would announce completion for applicants no round ever admitted — including the seedless and below-threshold cases the suite reports as NEITHER.** `CloseAllocation` concludes `allocation_done()` from `supported(admitted(a, r))`: at least one admission from a closed tour. If it read `points(a, p)` instead, then Bob (3 points, never admitted) and seedless Ann (10 points, never shortlisted) would each spuriously complete the allocation — the total would no longer mean "the rounds produced a seat". The `supported` indirection is what ties the announcement to work the frozen rounds actually did. ## 4. Adding a procedure to the allocation package **Answer: it fails at the static check, `law engine check`, with `LDC-E4126` (`STAGE_PROCEDURE_UNSUPPORTED`).** A stage and a procedure in one program are refused before any test runs: the tour fold the stage needs is undefined alongside a procedure automaton. The observed diagnostic on a scratch package combining the `Allotment` stage with a minimal two-state procedure is `error LDC-E4126: STAGE_PROCEDURE_UNSUPPORTED`. No `law test` line is reached — the package does not compile, so there is nothing to execute. This is an implementation-support fact about the verified profile (`law 0.1.0`, `law.core/0.2`), not a language-wide claim. ## How to verify ```sh law test packs/examples/language-demo/allocation ``` Expected: `итого: 5 проверено, 5 прошли, 0 не прошли, 0 не исполнены`. The deciding tests are `round 1 shortlists from the register`, `rounds are empty without seed`, `round 2 admits by points`, `insufficient points — no seat granted`, and `closed total reads after the rounds`. Static shape: ```sh law engine check packs/examples/language-demo/allocation/package.law ``` Expected: `check OK: packs/examples/language-demo/allocation/package.law`.