bend-kit-property

Search uses release 0.4.0.0 · 67 definitions

Releases (4)

def capn, capped at 1024.
def u32A uniform U32.
def u32.rangeA uniform U32 in [lo, hi); lo when hi <= lo + 1.
def sizeA uniform size in [0, min(max, 1024)].
def nat.fin
def natA uniform Nat in [0, min(max, 1024)].
def char.fin
def charA printable ASCII char, ' ' (32) through '~' (126).
def string.gon + 1 chars prepended to acc; cr holds the next char.
def string.ofExactly n printable ASCII chars.
def string.fin
def stringPrintable ASCII of length in [0, min(max, 1024)].
def bytes.goByte i and the n bytes after it; xr holds byte i (Bytes.set keeps its low 8 bits).
def bytes.start
def bytes.ofExactly min(len, 1024) uniform octets, one draw each.
def bytes.fin
def bytesUniform octets, length in [0, min(max, 1024)].
def list.gon + 1 items prepended to acc; hr holds the next item.
def list.ofExactly n items from gen.
def list.fin
def listItems from gen, length in [0, min(max, 1024)].
def maybe.some
def maybe.if
def maybe.pick
def maybeNone one time in four, else Some from gen.
def map.fin
def mapgen's value through f.
def bind.fin
def bindgen's value picks the next generator: bind(~Nat, ~List<&2, U32>, ~(r => Gen.nat(8, r)), ~(n => r => Gen.list.of(~U32, ~Gen.u32, n, r)), r).
def pair.snd
def pair.fst
def pairga's value then gb's, drawn in that order.

type Failure
def smallerScan candidates in order; a predicate returns its input so affine values work.
def smaller.start
def attempt.pair
def attempt
def minimizeEach accepted failure restarts shrinking; fuel bounds user-supplied shrinkers.
def minimize.start
def draw.pair
def draw
def check.go
def check.start
def checkReturn the first failure and its smallest reachable counterexample.
def reportPrint the seed and draw index so a failing check can be replayed.
def run

def u32.go(n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.
def u320, n - n/2, n - n/4, ..., n - 1.
def nat.go
def nat0n, n - n/2, n - n/4, ..., n - 1.
def list.chunksEvery run of k elements at offsets o, o + k, ...
def list.delsChunk deletions for k = n, n/2, ..., 1; k = n is the lone candidate [].
def list.heads
def list.cons
def list.onesOne element replaced by one of its candidates: the head's first, then the tail's.
def list[], chunk deletions (halves down to single elements), then single-element simplifications.
def maybe.some
def maybeNone, then Some of each candidate of x.
def char.lift
def char.of
def charToward 'a': a code above it halves toward it; one below tries 'a', then halves toward 0.
def string.of
def stringA String as a list of Chars under char.
def bytes.codes
def bytes.chars
def bytes.of
def bytesBytes is affine, so this never copies b: it reads the octets out once and builds each candidate as a fresh buffer, shrinking the octets as a list with bytes toward 0.