W0009: cost_advisory

W0009 cost_advisory — a cost bound that is an estimate, not a proof.

A warning of soma check, the checker of the Soma programming language (soma explain W0009).

The rule

W0009 was the warning for a cost bound that is only an estimate. In this compiler a declared cost { tokens: N } is either proven (a note) or refused: a bound that cannot be proven, such as a think() without a literal max_tokens or in a loop of unknown length, is error E0100 cost_unprovable. Give every think() a literal max_tokens and bound its loops (for [loop_bound(50)] x in xs { … }) so the bound can be proven.

When you see it

The compiler declares the CostAdvisory warning but never constructs it (grep -rn CostAdvisory compiler/src finds only its definition and display code). Since a cost bound that cannot be proven became a check error (E0100 cost_unprovable), soma check has no path that reports W0009.