V5001 impure_contract
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:
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:
@total
fn positive(x: Int) -> Bool { x > 0 }
fn halve(x: Int) -> Int requires positive(x) { x / 2 }Wrong program
compiler/tests/ui/V5001_impure_contract.sakura, which the compiler's ui suite runs through sakura check:
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):
{
"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
compiler/tests/ui/V5001_impure_contract.fixed.sakura, which sakura check accepts with no diagnostics:
@total
fn positive(x: Int) -> Bool { x > 0 }
fn halve(x: Int) -> Int
requires positive(x)
{ x / 2 }