Cryptol.Testing.Random

This module generates random values for Cryptol types.

Documentation

type Gen g b w i = Integer -> g -> (GenValue b w i, g)

runOneTest

Arguments

:: RandomGen g

=> EvalOpts

how to evaluate things

-> Value

Function under test

-> [Gen g Bool BV Integer]

Argument generators

-> Integer

Size

-> g

-> IO (TestResult, g)

Apply a testable value to some randomly-generated arguments. Returns Nothing if the function returned True, or `Just counterexample` if it returned False.

Please note that this function assumes that the generators match the supplied value, otherwise we'll panic.

testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV Integer]

Given a (function) type, compute generators for the function's arguments. Currently we do not support polymorphic functions. In principle, we could apply these to random types, and test the results.

randomValue :: (BitWord b w i, RandomGen g) => Type -> Maybe (Gen g b w i)

A generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator.

randomBit :: (BitWord b w i, RandomGen g) => Gen g b w i

Generate a random bit value.

randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)

randomInteger :: (BitWord b w i, RandomGen g) => Gen g b w i

Generate a random integer value. The size parameter is assumed to vary between 1 and 100, and we use it to generate smaller numbers first.

randomIntMod :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i

randomWord :: (BitWord b w i, RandomGen g) => Integer -> Gen g b w i

Generate a random word of the given length (i.e., a value of type [w]) The size parameter is assumed to vary between 1 and 100, and we use it to generate smaller numbers first.

randomStream :: RandomGen g => Gen g b w i -> Gen g b w i

Generate a random infinite stream value.

randomSequence :: RandomGen g => Integer -> Gen g b w i -> Gen g b w i

Generate a random sequence. This should be used for sequences other than bits. For sequences of bits use "randomWord".

randomTuple :: RandomGen g => [Gen g b w i] -> Gen g b w i

Generate a random tuple value.

randomRecord :: RandomGen g => [(Ident, Gen g b w i)] -> Gen g b w i

Generate a random record value.