W5005 linear_contract_on_hot_path
A requires, ensures, where or property requires clause calls List.all, List.any, List.contains or String.contains on a parameter (or it), so every check scans the whole value (design §7.2, §17.72).
A warning from the contract phase. sakura explain W5005 prints this explanation offline.
A requires, ensures, where or property requires clause calls List.all, List.any,
List.contains or String.contains on a parameter (or it), so every check scans the whole
value (design §7.2, §17.72). One warning per clause; std is exempt. Keep the clause when a linear
check is what you want, or move the invariant into a refined type so it is checked once, where
values are introduced.
Warning:
fn total(xs: List<Int>) -> Int
requires List.all(xs, fn(x) { x > 0 })
{ List.sum(xs) }Fixed (the invariant is a type):
type Positive = Int where it > 0
fn total(xs: List<Positive>) -> Int { List.fold(xs, 0, fn(acc, x) { acc + x }) }Wrong program
compiler/tests/ui/W5005_linear_contract_on_hot_path.sakura, which the compiler's ui suite runs through sakura check:
fn count_positive(xs: List<Int>) -> Int
requires List.all(xs, fn(x) { x > 0 })
{ List.len(xs) }
fn many(xs: List<Int>) -> Int {
var n = 0
for _ in 0..1000 { n = n + count_positive(xs) }
n
}sakura check --json reports this record (pretty-printed; $DIR is the fixture's directory):
{
"schema_version": "1.0",
"kind": "diagnostic",
"id": "d:1883ce8ec9916d2c",
"code": "W5005",
"severity": "warning",
"phase": "contract",
"message": "this contract calls `List.all` on `xs`, so every check scans all of it (design §7.2)",
"snapshot": "sha256:$SNAPSHOT",
"symbol_id": "main::W5005_linear_contract_on_hot_path::count_positive",
"spans": [
{
"uri": "file://$DIR/W5005_linear_contract_on_hot_path.sakura",
"content_hash": "sha256:35940e368c4fd7ed2cdb57ef5c876e16d024aabc8759a11012858d797d05f8c3",
"start_byte": 134,
"end_byte": 163,
"role": "primary"
}
],
"related_ids": [],
"expected": null,
"actual": null,
"obligation": null,
"counterexample": null,
"explanation_uri": "sakura://explain/W5005",
"fixes": []
}Fixed program
compiler/tests/ui/W5005_linear_contract_on_hot_path.fixed.sakura, which sakura check accepts with no diagnostics:
type Positive = Int where it > 0
fn count_positive(xs: List<Positive>) -> Int { List.len(xs) }
fn many(xs: List<Positive>) -> Int {
var n = 0
for _ in 0..1000 { n = n + count_positive(xs) }
n
}