cryptol-2.8.0: Cryptol: The Language of Cryptography

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

# Documentation

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

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.

Arguments

 :: RandomGen g => EvalOpts How to evaluate things -> Value Function to be used to calculate tests -> [Gen g Bool BV Integer] Argument generators -> Integer Size -> g Initial random state -> IO ([Value], Value, g) Arguments, result, and new random state

Arguments

 :: RandomGen g => g The random generator state -> EvalOpts How to evaluate things -> [Gen g Bool BV Integer] Generators for the function arguments -> Value The function itself -> Int How many tests? -> IO [([Value], Value)] A list of pairs of random arguments and computed outputs

Return a collection of random tests.

dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer] Source #

Given a (function) type, compute generators for the function's arguments. This is like testableType, but allows the result to be any finite type instead of just Bit.

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) Source #

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 Source #

Generate a random bit value.

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

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

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 Source #

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

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 Source #

Generate a random infinite stream value.

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

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 Source #

Generate a random tuple value.

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

Generate a random record value.