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

Arxo 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

Arxo 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:

Output

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 — how rounds and indices are written.