Markdown for LLMs

LDC-E4120 — A round rule reading a future round

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# LDC-E4120 — A round rule reading a future round

## What it means

In a staged package, rounds compute in order: a rule heading a round
relation may only read the current round or earlier ones. A read with a
negative index shift looks into a round that has not been computed yet,
and the compiler refuses it whether or not the read sits on a cycle.

Restate the read so it stays within the current round or reaches back to
an earlier one.

## Example

```law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

relation seed(i: Integer) kind empirical;
relation counter(i: Integer) kind institutional;
relation flag(i: Integer) kind institutional;
stage Rounds {
index i: Integer from 1 to 5;
bind counter index 1;
bind flag index 1;
}
rule Start strict { for i: Integer; when seed(i); then counter(1); }
rule Peek strict { for i: Integer; when counter(i) and not_known(counter(i + 1)); then flag(i); }
```

## Fix

```law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

relation seed(i: Integer) kind empirical;
relation counter(i: Integer) kind institutional;
relation flag(i: Integer) kind institutional;
stage Rounds {
index i: Integer from 1 to 5;
bind counter index 1;
bind flag index 1;
}
rule Start strict { for i: Integer; when seed(i); then counter(1); }
rule Peek strict { for i: Integer; when counter(i); then flag(i); }
```

## Engine message

The engine reports this in its own wording:

```text
example.law:14:6: error LDC-E4120: STAGE_CYCLE_WITHOUT_DESCENT: rule "Peek" reads the round relation "counter" of the next round (index shift -1) — reading a future round is forbidden regardless of cycling (§110, errata E-0263)
```

## Related

- [Time](/constructs/time/) — how rounds and indices are written.