LDC-E2401 — A computability promise the body contradicts

What it means

A declaration may state the computability class it claims — pure, snapshot-bound, or one of the heavier dependencies. The compiler independently infers the lower bound of what the body actually depends on: a rule that reads a judgment relation can never be pure, no matter what the annotation says. When the claimed class is weaker than the inferred bound, the annotation hides a real dependency and the compiler refuses it at the annotation.

The fix aligns the claim with the body: state the inferred class, or rewrite the body so it no longer reaches the heavier dependency. Claiming a stricter class than the bound stays silent — the bound is a floor, not an exact measure.

Example

Arxo Law

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

external judgment relation confirmed(x: Integer) { authority Court; }
relation flagged(x: Integer) kind institutional;
@expected_computability("PURE_DETERMINISTIC")
rule R defeasible { for x: Integer; when confirmed(x); then flagged(x); }

Fix

Arxo Law

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

external judgment relation confirmed(x: Integer) { authority Court; }
relation flagged(x: Integer) kind institutional;
@expected_computability("JUDGMENT_DEPENDENT")
rule R defeasible { for x: Integer; when confirmed(x); then flagged(x); }

Engine message

The engine reports this in its own wording:

Output

example.law:7:1: error LDC-E2401: @expected_computability(PURE_DETERMINISTIC) on "R": inferred lower bound — JUDGMENT_DEPENDENT (§47.5: the author cannot hide by declaration judgment/external dependency)

Related

• Expressions and quantities — what function bodies may compute.