# V5001 impure_contract

URL: /docs/errors/V5001
Markdown: /docs/errors/V5001.md

> Predicates in where, requires, ensures and property bodies must be pure, terminating and deterministic: no loops, no recursion, and calls only to @total functions in the contract subset (design §7.1).

An error from the `contract` phase. `sakura explain V5001` prints this explanation offline.

Predicates in `where`, `requires`, `ensures` and `property` bodies must be pure, terminating and
deterministic: no loops, no recursion, and calls only to `@total` functions in the contract
subset (design §7.1). Move effects out of the predicate and mark the helper it calls `@total`.

Wrong:

```sakura
fn noisy_positive(x: Int) -> Bool ! {Console} { Console.print("checking"); x > 0 }
fn halve(x: Int) -> Int ! {Console} requires noisy_positive(x) { x / 2 }
```

Fixed:

```sakura
@total
fn positive(x: Int) -> Bool { x > 0 }
fn halve(x: Int) -> Int requires positive(x) { x / 2 }
```

## Wrong program [#wrong-program]

[`compiler/tests/ui/V5001_impure_contract.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/V5001_impure_contract.sakura), which the compiler's ui suite runs through `sakura check`:

```sakura
fn noisy_positive(x: Int) -> Bool ! {Console} {
  Console.print("checking")
  x > 0
}

fn halve(x: Int) -> Int
  ! {Console}
  requires noisy_positive(x)
{ x / 2 }
```

`sakura check --json` reports this record (pretty-printed; `$DIR` is the fixture's directory):

```json
{
  "schema_version": "1.0",
  "kind": "diagnostic",
  "id": "d:2a33b902adb8ae85",
  "code": "V5001",
  "severity": "error",
  "phase": "effect",
  "message": "a contract must be pure, but it performs `Console`",
  "snapshot": "sha256:$SNAPSHOT",
  "symbol_id": "main::V5001_impure_contract::halve",
  "spans": [
    {
      "uri": "file://$DIR/V5001_impure_contract.sakura",
      "content_hash": "sha256:abfb78d6d4e92f712ea1eac2a86c0d3210e2eae4fc709b49544cfe375024155c",
      "start_byte": 215,
      "end_byte": 232,
      "role": "primary"
    },
    {
      "uri": "file://$DIR/V5001_impure_contract.sakura",
      "content_hash": "sha256:abfb78d6d4e92f712ea1eac2a86c0d3210e2eae4fc709b49544cfe375024155c",
      "start_byte": 215,
      "end_byte": 232,
      "role": "cause",
      "label": "`noisy_positive` performs `Console` here"
    }
  ],
  "related_ids": [],
  "expected": {
    "render": "{}",
    "row": {
      "labels": [],
      "tail": null
    }
  },
  "actual": {
    "render": "{Console}",
    "row": {
      "labels": [
        {
          "effect": "std::Console",
          "args": []
        }
      ],
      "tail": null
    }
  },
  "obligation": null,
  "counterexample": null,
  "explanation_uri": "sakura://explain/V5001",
  "fixes": []
}
```

## Fixed program [#fixed-program]

[`compiler/tests/ui/V5001_impure_contract.fixed.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/V5001_impure_contract.fixed.sakura), which `sakura check` accepts with no diagnostics:

```sakura
@total
fn positive(x: Int) -> Bool { x > 0 }

fn halve(x: Int) -> Int
  requires positive(x)
{ x / 2 }
```