check.bend checks

raw source on the hub · import 0x738b30530890e825e0ab81092b94cbfc/check.bend as Check

bendcheck: property-based testing for Bend.

A property is a def from an input to a Verdict. Check.run draws inputs from a generator, tests each, and on the first failure shrinks the input to a minimal counterexample. Generators, properties, shrinkers and printers are passed as templates (~), so they may be used many times.

1 import

import Base

Types

type Both source · line 12 · raw

@-A:Data -> @-B:Data -> Data

a pair whose parts may both be reused (a datatype rather than Sigma, so nested pairs take apart without annotations)

Both

@-A:Data -> @-B:Data -> @fst:A -> @snd:B -> Both<A, B>

type Rand source · line 19 · raw

Data

a 32-bit counter hashed by lowbias32; size bounds sized generators

Rand
```
@seed:U32 -> @size:U32 -> Rand
```

type Verdict source · line 319 · raw

Data

Holds
```
Verdict
```
Fails
```
Verdict
```
Skip
```
Verdict
```

type Report source · line 342 · raw

Data

Passed
```
@tests:Nat -> @skipped:Nat -> Report
```

Failed

@tests:Nat -> @shrinks:Nat -> @input:String -> Report

GaveUp
```
@tests:Nat -> @skipped:Nat -> Report
```

type St source · line 349 · raw

@-A:Data -> Data

The runner is one state machine, since Bend has no mutual recursion. i is the test index; it sets the size, which grows up to 100.

Next

@-A:Data -> @done:Nat -> @skipped:Nat -> @left:Nat -> @i:U32 -> @r:Rand -> St<A>

Drawn

@-A:Data -> @done:Nat -> @skipped:Nat -> @left:Nat -> @i:U32 -> @xr:Both<A, Rand> -> St<A>

Tested

@-A:Data -> @done:Nat -> @skipped:Nat -> @left:Nat -> @i:U32 -> @r:Rand -> @x:A -> @v:Verdict -> St<A>

Shrinking

@-A:Data -> @done:Nat -> @x:A -> @cands:List<&2, A> -> @steps:Nat -> St<A>

Retest

@-A:Data -> @done:Nat -> @x:A -> @c:A -> @rest:List<&2, A> -> @steps:Nat -> @v:Verdict -> St<A>

Definitions

def Rand.mix source · line 23 · raw

@+x:U32 -> U32

lowbias32 (C. Wellons): a fast, well-mixed 32-bit hash

def Rand.new source · line 28 · raw

@seed:U32 -> Rand

def Rand.next source · line 31 · raw

@r:Rand -> Both<U32, Rand>

def Rand.sized source · line 37 · raw

@r:Rand -> @size:U32 -> Rand

def Gen source · line 45 · raw

@-A:Data -> Type

def Gen.pure source · line 48 · raw

@-A:Data -> @x:A -> Gen(A)

def Gen.bind.k source · line 51 · raw

@-A:Data -> @-B:Data -> @f:(@_:A -> Gen(B)) -> @ar:Both<A, Rand> -> Both<B, Rand>

def Gen.bind source · line 55 · raw

@-A:Data -> @-B:Data -> @m:Gen(A) -> @f:(@_:A -> Gen(B)) -> Gen(B)

def Gen.map.k source · line 58 · raw

@-A:Data -> @-B:Data -> @f:(@_:A -> B) -> @ar:Both<A, Rand> -> Both<B, Rand>

def Gen.map source · line 62 · raw

@-A:Data -> @-B:Data -> @f:(@_:A -> B) -> @m:Gen(A) -> Gen(B)

def Gen.bits source · line 66 · raw

@r:Rand -> Both<U32, Rand>

32 uniform bits

def Gen.size source · line 70 · raw

@r:Rand -> Both<U32, Rand>

the current size (grows with the test index)

def Gen.below source · line 76 · raw

@+n:U32 -> Gen(U32)

uniform in [0, n); 0 when n is 0

def Gen.bool source · line 81 · raw

Gen(Bool)

def Gen.edges source · line 87 · raw

List<&2, U32>

values that break code: zero, one, powers of two and their neighbours

def List.nth_u32 source · line 91 · raw

@xs:List<&2, U32> -> @i:Nat -> U32

def Gen.u32.pick source · line 100 · raw

@edge:Bool -> @k:U32 -> @x:U32 -> U32

def Gen.u32 source · line 108 · raw

Gen(U32)

any U32, one draw in eight an edge value

def Gen.small source · line 115 · raw

Gen(U32)

a U32 in [0, size]

def Gen.nat source · line 122 · raw

Gen(Nat)

a Nat in [0, size]

def Gen.word source · line 126 · raw

@n:Nat -> Gen(Word(n))

a Word of n random bits

def Shrink.none source · line 164 · raw

@-A:Data -> @x:A -> List<&2, A>

def Shrink.u32.go source · line 168 · raw

@fuel:Nat -> @stop:Bool -> @+x:U32 -> @+d:U32 -> List<&2, U32>

x - x, x - x/2, x - x/4, ..., x - 1: a binary search towards 0

def Shrink.u32 source · line 178 · raw

@x:U32 -> List<&2, U32>

def Shrink.nat.half source · line 182 · raw

@n:Nat -> Nat

def Shrink.nat source · line 193 · raw

@x:Nat -> List<&2, Nat>

def Shrink.bool source · line 200 · raw

@b:Bool -> List<&2, Bool>

def Shrink.word.tails source · line 207 · raw

@+p:Nat -> @+b:Bool -> @ts:List<&2, Word(p)> -> List<&2, Word(1n+p)>

def Shrink.word.head source · line 214 · raw

@+p:Nat -> @b:Bool -> @+t:Word(p) -> @ts:List<&2, Word(p)> -> List<&2, Word(1n+p)>

def Shrink.word.bits source · line 222 · raw

@n:Nat -> @w:Word(n) -> List<&2, Word(n)>

clear one set bit at a time, lowest first

def Shrink.word.nonzero source · line 229 · raw

@+n:Nat -> @+w:Word(n) -> @zero:Bool -> List<&2, Word(n)>

def Shrink.word source · line 237 · raw

@+n:Nat -> @w:Word(n) -> List<&2, Word(n)>

zero, then half, then one bit fewer

def Show.word source · line 313 · raw

@n:Nat -> @w:Word(n) -> String

a word by its value

def Check.holds source · line 324 · raw

@b:Bool -> Verdict

def Check.when source · line 332 · raw

@pre:Bool -> @b:Bool -> Verdict

a property with a precondition: inputs failing pre are skipped

def Check.size source · line 356 · raw

@+i:U32 -> U32

def Check.skips source · line 421 · raw

@s:Nat -> String

def Check.print source · line 428 · raw

@name:String -> @seed:U32 -> @rep:Report -> IO(Bool)

def Check.count_failed source · line 449 · raw

@bs:List<&2, Bool> -> Nat

def Check.summary.end source · line 460 · raw

@total:Nat -> @failed:Nat -> @ok:Bool -> IO(Unit)

def Check.summary source · line 468 · raw

@+bs:List<&2, Bool> -> IO(Unit)

print a summary; exit with status 1 if any property failed

Templates

template Gen.pair source · line 136 · raw

@-A:Data -> @-B:Data -> @-ga:Gen(A) -> @-gb:Gen(B) -> Gen(Both<A, B>)

template Gen.list.n source · line 142 · raw

@-A:Data -> @-g:Gen(A) -> @n:Nat -> Gen(List<&2, A>)

template Gen.list source · line 153 · raw

@-A:Data -> @-g:Gen(A) -> Gen(List<&2, A>)

a list of up to size elements

template Shrink.pair.l source · line 241 · raw

@-A:Data -> @-B:Data -> @+b:B -> @xs:List<&2, A> -> List<&2, Both<A, B>>

template Shrink.pair.r source · line 248 · raw

@-A:Data -> @-B:Data -> @+a:A -> @ys:List<&2, B> -> List<&2, Both<A, B>>

template List.cat source · line 255 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> List<&2, A>

template Shrink.pair source · line 263 · raw

@-A:Data -> @-B:Data -> @-sa:(@_:A -> List<&2, A>) -> @-sb:(@_:B -> List<&2, B>) -> @p:Both<A, B> -> List<&2, Both<A, B>>

shrink the left, then the right

template Shrink.list.cons source · line 269 · raw

@-A:Data -> @+h:A -> @ts:List<&2, List<&2, A>> -> List<&2, List<&2, A>>

template Shrink.list.heads source · line 276 · raw

@-A:Data -> @hs:List<&2, A> -> @+t:List<&2, A> -> List<&2, List<&2, A>>

template Shrink.list source · line 284 · raw

@-A:Data -> @-s:(@_:A -> List<&2, A>) -> @xs:List<&2, A> -> List<&2, List<&2, A>>

the empty list, the tail, then a smaller head, then a smaller tail

template Show.pair source · line 294 · raw

@-A:Data -> @-B:Data -> @-sa:(@_:A -> String) -> @-sb:(@_:B -> String) -> @p:Both<A, B> -> String

template Show.list.tail source · line 298 · raw

@-A:Data -> @-s:(@_:A -> String) -> @xs:List<&2, A> -> String

template Show.list source · line 305 · raw

@-A:Data -> @-s:(@_:A -> String) -> @xs:List<&2, A> -> String

template Check.stop source · line 360 · raw

@-A:Data -> @-show:(@_:A -> String) -> @st:St<A> -> Report

when fuel runs out: a failure keeps its best counterexample so far

template Check.go source · line 373 · raw

@-A:Data -> @-gen:Gen(A) -> @-prop:(@_:A -> Verdict) -> @-shrink:(@_:A -> List<&2, A>) -> @-show:(@_:A -> String) -> @fuel:Nat -> @st:St<A> -> Report

template Check.run source · line 416 · raw

@-A:Data -> @-gen:Gen(A) -> @-prop:(@_:A -> Verdict) -> @-shrink:(@_:A -> List<&2, A>) -> @-show:(@_:A -> String) -> @+count:Nat -> @seed:U32 -> Report

test prop on count inputs from gen; skipped inputs are redrawn, up to ten skips per test

template Check.prop source · line 445 · raw

@-A:Data -> @-gen:Gen(A) -> @-prop:(@_:A -> Verdict) -> @-shrink:(@_:A -> List<&2, A>) -> @-show:(@_:A -> String) -> @name:String -> @count:Nat -> @+seed:U32 -> IO(Bool)