property.bend
bend-kit-property@0.3.0.0 · 121 lines · 0 definitions
1# Reproducible property checks with generated inputs and greedy shrinking.
2import Base
3import bend-kit-random@0.1.0.1/random.bend as Rand
4import bend-kit-property@0.3.0.0/generate.bend as Gen
5import bend-kit-property@0.3.0.0/shrink.bend as Shrink
6
7type Failure<-T: Type> is Type:
8 Failure{seed: U32, trial: Nat, value: T}
9
10# Scan candidates in order; a predicate returns its input so affine values work.
11def smaller(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>, tested: T & Bool) -> Maybe<&1, T>:
12 match xs:
13 case Nil{}:
14 (candidate, ok) = tested
15 match ok:
16 case False{}:
17 Some{candidate}
18 case True{}:
19 None{}
20 case Con{x, rest}:
21 (candidate, ok) = tested
22 match ok:
23 case False{}:
24 Some{candidate}
25 case True{}:
26 smaller(~T, ~test, rest, test(x))
27
28def smaller.start(~T: Type, ~test: T -> T & Bool, xs: List<&1, T>) -> Maybe<&1, T>:
29 match xs:
30 case Nil{}:
31 None{}
32 case Con{x, rest}:
33 smaller(~T, ~test, rest, test(x))
34
35def attempt.pair(~T: Type, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, pair: T & T) -> T & Maybe<&1, T>:
36 (original, probe) = pair
37 (original, smaller.start(~T, ~test, shrink(probe)))
38
39def attempt(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, value: T) -> T & Maybe<&1, T>:
40 attempt.pair(~T, ~shrink, ~test, copy(value))
41
42# Each accepted failure restarts shrinking; fuel bounds user-supplied shrinkers.
43def minimize(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
44 fuel: Nat, state: T & Maybe<&1, T>) -> T:
45 match fuel:
46 case 0n:
47 (original, choice) = state
48 Maybe.default(&1, T, choice, original)
49 case 1n+p:
50 (original, choice) = state
51 match choice:
52 case None{}:
53 original
54 case Some{candidate}:
55 minimize(~T, ~copy, ~shrink, ~test, p, attempt(~T, ~copy, ~shrink, ~test, candidate))
56
57def minimize.start(~T: Type, ~copy: T -> T & T, ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
58 value: T) -> T:
59 minimize(~T, ~copy, ~shrink, ~test, 1024n, attempt(~T, ~copy, ~shrink, ~test, value))
60
61def draw.pair(~T: Type, ~test: T -> T & Bool, pair: T & Rand.Rng) -> (T & Bool) & Rand.Rng:
62 (sample, next) = pair
63 (test(sample), next)
64
65def draw(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~test: T -> T & Bool, rng: Rand.Rng) -> (T & Bool) & Rand.Rng:
66 draw.pair(~T, ~test, gen(rng))
67
68def check.go(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
69 ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
70 remaining: Nat, +seed: U32, +trial: Nat, state: (T & Bool) & Rand.Rng) -> Maybe<&1, Failure<T>>:
71 match remaining:
72 case 0n:
73 None{}
74 case 1n+p:
75 match p:
76 case 0n:
77 (tested, next) = state
78 (value, ok) = tested
79 match ok:
80 case False{}:
81 Some{Failure{seed, trial, minimize.start(~T, ~copy, ~shrink, ~test, value)}}
82 case True{}:
83 None{}
84 case 1n+q:
85 (tested, next) = state
86 (value, ok) = tested
87 match ok:
88 case False{}:
89 Some{Failure{seed, trial, minimize.start(~T, ~copy, ~shrink, ~test, value)}}
90 case True{}:
91 check.go(~T, ~gen, ~copy, ~shrink, ~test, p, seed, (1n+trial), draw(~T, ~gen, ~test, next))
92
93def check.start(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
94 ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
95 remaining: Nat, seed: U32, rng: Rand.Rng) -> Maybe<&1, Failure<T>>:
96 match remaining:
97 case 0n:
98 None{}
99 case 1n+p:
100 check.go(~T, ~gen, ~copy, ~shrink, ~test, remaining, seed, 0n, draw(~T, ~gen, ~test, rng))
101
102# Return the first failure and its smallest reachable counterexample.
103def check(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
104 ~shrink: T -> List<&1, T>, ~test: T -> T & Bool,
105 +seed: U32, trials: Nat) -> Maybe<&1, Failure<T>>:
106 check.start(~T, ~gen, ~copy, ~shrink, ~test, trials, seed, Rand.seed(seed))
107
108# Print the seed and draw index so a failing check can be replayed.
109def report(~T: Type, ~show: T -> String, result: Maybe<&1, Failure<T>>) -> IO(Bool):
110 match result:
111 case None{}:
112 IO.pure(Bool, True{})
113 case Some{Failure{seed, trial, value}}:
114 do IO<Bool>:
115 IO.print("property failed: seed=" ++ U32.show(seed) ++ " trial=" ++ Nat.show(trial) ++ " counterexample=" ++ show(value))
116 return False{}
117
118def run(~T: Type, ~gen: Rand.Rng -> T & Rand.Rng, ~copy: T -> T & T,
119 ~shrink: T -> List<&1, T>, ~test: T -> T & Bool, ~show: T -> String,
120 seed: U32, trials: Nat) -> IO(Bool):
121 report(~T, ~show, check(~T, ~gen, ~copy, ~shrink, ~test, seed, trials))