W7001 property_discard_budget

A warning from the verify phase. sakura explain W7001 prints this explanation offline.

A property discarded more than 90% of its generated inputs, so it tested almost nothing (design §7.4, §17.64). For a property synthesized by sakura test --contracts, inputs come from the parameter types and requires: ranges, lengths, enums and non-empty lists are generated directly, anything else is a filter. The test fails rather than passing vacuously. Restate the parameters so the generator builds valid inputs.

Warning (under sakura test --contracts):

pub fn sku(code: String) -> String
  requires String.starts_with(code, "SKU-")
{ code }

Fixed (a range the generator constructs):

pub fn sku(number: Int) -> String
  requires number >= 0
{ "SKU-{number}" }

Wrong programCopy Anchor Link

compiler/tests/ui/W7001_property_discard_budget.sakura, which the compiler's ui suite runs through sakura test --contracts:

pub fn exact(x: Int) -> Int
  requires x == 123_456
{ x }

sakura test --contracts reports W7001.

Fixed programCopy Anchor Link

compiler/tests/ui/W7001_property_discard_budget.fixed.sakura, which sakura test --contracts accepts with no diagnostics:

pub fn exact(x: Int) -> Int
  requires x >= 0 && x <= 123_456
{ x }