cryptol-2.8.0: Cryptol: The Language of Cryptography

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

Cryptol.Testing.Random

Description

This module generates random values for Cryptol types.

Synopsis

- type Gen g b w i = Integer -> g -> (GenValue b w i, g)
- runOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Bool BV Integer] -> Integer -> g -> IO (TestResult, g)
- returnOneTest :: RandomGen g => EvalOpts -> Value -> [Gen g Bool BV Integer] -> Integer -> g -> IO ([Value], Value, g)
- returnTests :: RandomGen g => g -> EvalOpts -> [Gen g Bool BV Integer] -> Value -> Int -> IO [([Value], Value)]
- dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
- testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV Integer]
- randomValue :: (BitWord b w i, RandomGen g) => Type -> Maybe (Gen g b w i)
- randomBit :: (BitWord b w i, RandomGen g) => Gen g b w i
- randomSize :: RandomGen g => Int -> Int -> g -> (Int, g)
- randomInteger :: (BitWord b w i, RandomGen g) => Gen g b w i
- 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
- randomStream :: RandomGen g => Gen g b w i -> Gen g b w i
- randomSequence :: RandomGen g => Integer -> Gen g b w i -> Gen g b w i
- randomTuple :: RandomGen g => [Gen g b w i] -> Gen g b w i
- randomRecord :: RandomGen g => [(Ident, Gen g b w i)] -> Gen g b w i

# Documentation

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

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

returnOneTest Source #

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

returnTests Source #

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

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

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.