cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Trustworthy
Language | Haskell2010

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

- type Gen g x = Integer -> g -> (SEval x (GenValue x), g)
- randomValue :: (Backend sym, RandomGen g) => sym -> TValue -> Maybe (Gen g sym)
- dumpableType :: forall g. RandomGen g => TValue -> Maybe [Gen g Concrete]
- testableType :: RandomGen g => TValue -> Maybe (Maybe Integer, [TValue], [[Value]], [Gen g Concrete])
- data TestResult
  - = Pass
  - | FailFalse [Value]
  - | FailError EvalErrorEx [Value]
- isPass :: TestResult -> Bool
- returnTests :: RandomGen g => g -> [Gen g Concrete] -> Value -> Int -> IO [([Value], Value)]
- returnTests' :: RandomGen g => g -> [Gen g Concrete] -> Value -> Int -> IO ([([Value], Value)], g)
- exhaustiveTests :: MonadIO m => (Integer -> m ()) -> Value -> [[Value]] -> m (TestResult, Integer)
- randomTests :: (MonadIO m, RandomGen g) => (Integer -> m ()) -> Integer -> Value -> [Gen g Concrete] -> g -> m (TestResult, Integer)
- randomTests' :: (MonadIO m, RandomGen g) => (Integer -> m ()) -> Integer -> Value -> [Gen g Concrete] -> g -> m ((TestResult, Integer), g)

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

data TestResult Source #

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 EvalErrorEx [Value] |

isPass :: TestResult -> Bool Source #

returnTests Source #

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 as well as the new state of the RNG

returnTests' Source #

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)], g) | A list of pairs of random arguments and computed outputs as well as the new state of the RNG

Return a collection of random tests.

exhaustiveTests Source #

Arguments

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

randomTests Source #

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

randomTests' Source #

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), g) |