cryptol-2.10.0: Cryptol: The Language of Cryptography
Copyright (c) 2013-2016 Galois Inc. BSD3 cryptol@galois.com provisional portable Trustworthy Haskell2010

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

# Documentation

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

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

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

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

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

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.

Constructors

 TestReport FieldsreportResult :: TestResult reportProp :: StringThe property as entered by the userreportTestsRun :: Integer reportTestsPossible :: Maybe Integer

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]

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.

Arguments

 :: MonadIO m => (Integer -> m ()) progress callback -> Value function under test -> [[Value]] exhaustive set of test values -> m (TestResult, Integer)

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)