Markdown for LLMs

LDC-E2403 — A function whose purity is not proved

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

# LDC-E2403 — A function whose purity is not proved

## What it means

A plain function may lower only when its complete local call graph proves
it free of effects: no snapshot reads, no judgment relations, no opaque
or unknown calls, no recursion without a termination certificate. An
explicit purity claim raises the same bar and adds the author's word to
it. When any dependency lacks an effect descriptor — an imported name the
unit cannot see into, for example — purity is unproved and the compiler
refuses the function at its name.

The fix proves purity or drops the claim: compute from data alone with
local pure calls, or declare the heavier effect through the channel the
language provides for it. A body of plain arithmetic over its parameters
lowers without a word.

## Example

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

pure function Unproved(x: Integer) -> Integer = foreign.pkg::rate(x);
```

## Fix

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

function Increment(x: Integer) -> Integer = x + 1;
```

## Engine message

The engine reports this in its own wording:

```text
example.law:5:15: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): pure function "Unproved" is not proven PURE_DETERMINISTIC: call "foreign::pkg::rate" has no available effect descriptor (imported/unknown dependency) (§46/§47.5)
```

## Related

- [Expressions and quantities](/constructs/expressions-quantities/) — what function bodies may compute.