# 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`.

## 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.

```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`):

```text
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.