Execution rounds: stage, index, bind

In one sentence: the stage construct answers the question “in which round this fact is computed”, when one step’s conclusion must rest on the finished conclusion of the previous step: round-by-round vote counts, depth deductions, stepwise ground checks. Take it when the order “first close round r, then read it from round r + 1” is part of the norm’s meaning, not just presentation convenience.

Multi-step procedures compute round by round: each round closes before the next reads it. The installed engine executes rounds — both examples below run in rounds and pass law test.

OverviewBoundariesCorpus formsPitfalls

1. When to take it and when not to

Instead of	Selection rule
stage vs a chain of strict rules without rounds	A chain concludes everything in one stratum: the reader sees an unfinished set. When a step’s total must be read only after the step closes (the round’s worst drops out, counting continues without them), a round is needed: at the start of round r all atoms of ranks < r are complete. No closure — no stage
stage vs priority between rules	Priority resolves a conflict inside one set; a round splits computation into sequential sets. Conflicts gather per round separately. “Who is stronger” is priority; “what closed earlier” is stage
stage with an Integer index vs a Date index	Round counters, depth, step number — Integer (no step). Calendar periods with a step <count> <unit> and a from + n·step grid — Date. There is no calendar step backwards
One stage vs several	Several executable stage are allowed if and only if the bound-predicate sets are pairwise disjoint. One predicate in two stage — LDC-E4124 / NON_EXECUTABLE_STAGE_MULTIPLE. In doubt about disjointness — one stage
stage vs procedure	Not an alternative but a ban: a program with a procedure and an executable stage is unsupported (LDC-E4126). Stepwise within one world — stage; process branching — a procedure, but in another package

2. Minimal example

Package research.stage.two_rounds: a counter over domain 1…3, an upper rule totals after the rounds.

Arxo Law

stage Rounds {
    index round: Integer from 1 to 3;
    bind counter index 1;
}
relation go() kind empirical { ... }
relation counter(i: Integer) kind institutional { ... }
relation reached_top() kind institutional { ... }

rule Seed strict {
    when go();
    then counter(1);
}
rule Next(i: Integer) strict {
    when supported(counter(i)) and i < 3;
    then counter(i + 1);
}
rule AnnounceTop strict {
    when supported(counter(3));
    then reached_top();
}

Case facts: go() with origin case_input. Query: evaluate truth(reached_top()).

Observed engine answer (installed law, semantics law.core/0.2):

Output

law engine check docs/research/constructs/23-stage/examples/two-rounds
check OK: docs/research/constructs/23-stage/examples/two-rounds
law test research.stage.two_rounds: мир research.stage.two_rounds
  ok   [research.stage.two_rounds#authored] tests/01-counter-reaches-top.lawtest / urn:query:research-stage-01
  ok   [research.stage.two_rounds#authored] tests/02-no-seed-stays-silent.lawtest / urn:query:research-stage-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0

Sensitivity: removing the go() fact changes the expectation from TRUE_ONLY to NEITHER (the no-seed scenario test) — the example is not vacuous. The three rule classes on one example: Seed — a round rule reading a base; Next — a round rule with a + 1 shift; AnnounceTop — an upper rule (head outside rounds, body reading a round rule), executing over the finished round union.

Nearest wrong outcome: drop the i < 3 guard — in round 3 the head counter(4) lands outside domain D, and evaluation answers fatal STAGE_INDEX_OUTSIDE_DOMAIN with the rule address instead of TRUE_ONLY. The author’s guard is the same duty as the budget in calc.long_division.

3. Example by domain

• Law: Maine ranked choice (package us.me.ranked_choice, United States) — stage CountingRounds, index — the round number, nineteen “in this round” relations bound; the ANewRoundBegins rule opens round r + 1 from a round-r removal. Nearby package nr.electoral_act_2016 (Nauru) — stage DeductionRounds, index — deduction depth (see corpus-forms.md).
• Works regulation: finishing schedule (package renovation.schedule, works regulation) — stage CoatingTours: round 1 — screed, rounds 2–5 — primer and paint coats; the hidden-works-act procedure deliberately moved to the neighbouring package because of LDC-E4126.
• Science: regularity checks (package arxo.navier_stokes, research formalization) — stage RegularityTours: three regularity-check rounds; nearby a second stage from the arxo.poincare package — a disjoint-bindings specimen.
• Teaching case: research.stage.elimination — the same device in miniature: present/out over rounds 1…2, not_known(out(c, r)) reading a finished round, the upper Survive rule totalling (law test 2/2).

4. How the engine answers

Table — observed runs of this directory’s examples (installed law, semantics law.core/0.2 of the current revision):

Facts	Question	Answer	Why
go()	reached_top()	TRUE_ONLY	rounds 1–3 executed in order, the upper rule read finished round 3
no facts	reached_top()	NEITHER	round 1 empty, no total; silence, not a refusal
running + weak	out(weakling, 1)	TRUE_ONLY	the weak dropped out in round 1
running without weak	out(weakling, 1)	NEITHER	no dropout; a scratch probe confirmed survivor(able) TRUE_ONLY
go() with stage Empty {}	done()	refusal NON_EXECUTABLE_STAGE, empty results	the reserve does not execute (confirmed by a scratch run; the binary’s message text mentions “only in 0.3” — stale wording, the refusal itself holds)

• Execution order: base rules → each stage’s rounds by rank → upper rules → norm runtime for outside-round norms. A round with not one application is still a round: maxStages counts it, execution runs to to.
• A round rule’s rule_application node carries attributes.stage: {"name", "index", "rank"}; index is a value (integer or ISO date), not a term.
• Writing into a finished round is fatal STAGE_LATE_WRITE with the rule address, not a quiet repeat. A head index value outside the domain is fatal STAGE_INDEX_OUTSIDE_DOMAIN. Counter overflow is fatal RESOURCE_LIMIT with details.counter = "maxStages".
• In why_not a round literal names the round in the blocker (stage.index); an out-of-domain index is the outside_stage_domain blocker (the engine’s form was not directly verified on these examples).

5. Common mistakes

1. Reading the next round (counter(i + 1) in a round-i rule body) — LDC-E4120 / NON_EXECUTABLE_UNSTRATIFIED even without a cycle (pitfalls.md, item 1).
2. Head without a bound index — LDC-E4121 / NON_EXECUTABLE_STAGE_PRODUCER (pitfalls.md, item 2).
3. Empty domain, non-calendar step, to off-grid, nonexistent grid date — LDC-E4122 / NON_EXECUTABLE_STAGE with a reason (pitfalls.md, item 3).
4. Bind on the wrong position or wrong type — LDC-E4123; a second stage with overlapping binds — LDC-E4124 (pitfalls.md, item 4).
5. Closure over a round predicate — LDC-E4125; a procedure next to stage — LDC-E4126 (pitfalls.md, item 5).
6. Nonmonotone read with an underived shift (literal vs another’s variable) — LDC-E4120 on par with next-round reads (pitfalls.md, item 6).
7. Empty stage {} body in a live package — loud NON_EXECUTABLE_STAGE before any conclusion, not a no-op (pitfalls.md, item 7).

6. References

• Grammar: stage_decl, stage_body, stage_index, stage_bound, stage_bind in the grammar.
• No other page covers stage — this catalogue closes that gap.