Cryptol.Testing.Random

This module generates random values for Cryptol types.

Documentation

type Gen g x = Integer -> g -> (SEval x (GenValue x), g)

randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym)

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

dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]

Given a (function) type, compute generators for the function's arguments.

testableType :: RandomGen g => TValue -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])

Given a (function) type, compute data necessary for random or exhaustive testing.

The first returned component is a count of the number of possible input test vectors, if the input types are finite. The second component is a list of all the types of the function inputs. The third component is a list of all input test vectors for exhaustive testing. This will be empty unless the input types are finite. The final argument is a list of generators for the inputs of the function.

This function will return Nothing if the input type does not eventually return Bit, or if we cannot compute a generator for one of the inputs.

data TestReport

Constructors

TestReport

Fields

• reportResult :: TestResult
• reportProp :: String

  The property as entered by the user

• reportTestsRun :: Integer
• reportTestsPossible :: Maybe Integer

data TestResult

A test result is either a pass, a failure due to evaluating to False, or a failure due to an exception raised during evaluation

Constructors

Pass

FailFalse [Value]

FailError EvalError [Value]

isPass :: TestResult -> Bool

returnTests

Arguments

:: RandomGen g

=> g

The random generator state

-> [Gen g Concrete]

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.

exhaustiveTests

Arguments

:: MonadIO m

=> (Integer -> m ())

progress callback

-> Value

function under test

-> [[Value]]

exhaustive set of test values

-> m (TestResult, Integer)

randomTests

Arguments

:: (MonadIO m, RandomGen g)

=> (Integer -> m ())

progress callback

-> Integer

Maximum number of tests to run

-> Value

function under test

-> [Gen g Concrete]

input value generators

-> g

Inital random generator

-> m (TestResult, Integer)