cryptol-2.7.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Eval.Value

Description

 
Synopsis

Documentation

data BV Source #

Concrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1

Constructors

BV !Integer !Integer 
Instances
Show BV Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

showsPrec :: Int -> BV -> ShowS #

show :: BV -> String #

showList :: [BV] -> ShowS #

Generic BV Source # 
Instance details

Defined in Cryptol.Eval.Value

Associated Types

type Rep BV :: Type -> Type #

Methods

from :: BV -> Rep BV x #

to :: Rep BV x -> BV #

NFData BV Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

rnf :: BV -> () #

EvalPrims Bool BV Integer Source # 
Instance details

Defined in Cryptol.Prims.Eval

BitWord Bool BV Integer Source # 
Instance details

Defined in Cryptol.Eval.Value

type Rep BV Source # 
Instance details

Defined in Cryptol.Eval.Value

binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV Source #

Apply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.

unaryBV :: (Integer -> Integer) -> BV -> BV Source #

Apply an integer function to the values of a bitvector. This function assumes the function will not require masking.

mkBv :: Integer -> Integer -> BV Source #

Smart constructor for BVs that checks for the width limit

data SeqMap b w i Source #

A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.

Constructors

IndexSeqMap !(Integer -> Eval (GenValue b w i)) 
UpdateSeqMap !(Map Integer (Eval (GenValue b w i))) !(Integer -> Eval (GenValue b w i)) 
Instances
NFData (SeqMap b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

rnf :: SeqMap b w i -> () #

finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i Source #

Generate a finite sequence map from a list of values

infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i) Source #

Generate an infinite sequence map from a stream of values

enumerateSeqMap :: Integral n => n -> SeqMap b w i -> [Eval (GenValue b w i)] Source #

Create a finite list of length n of the values from [0..n-1] in the given the sequence emap.

streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)] Source #

Create an infinite stream of all the values in a sequence map

reverseSeqMap Source #

Arguments

:: Integer

Size of the sequence map

-> SeqMap b w i 
-> SeqMap b w i 

Reverse the order of a finite sequence map

updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i Source #

concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i Source #

Concatenate the first n values of the first sequence map onto the beginning of the second sequence map.

splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i) Source #

Given a number n and a sequence map, return two new sequence maps: the first containing the values from `[0..n-1]` and the next containing the values from n onward.

dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i Source #

Drop the first n elements of the given SeqMap.

memoMap :: SeqMap b w i -> Eval (SeqMap b w i) Source #

Given a sequence map, return a new sequence map that is memoized using a finite map memo table.

zipSeqMap :: (GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> SeqMap b w i -> Eval (SeqMap b w i) Source #

Apply the given evaluation function pointwise to the two given sequence maps.

mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> Eval (SeqMap b w i) Source #

Apply the given function to each value in the given sequence map

data WordValue b w i Source #

For efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).

However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.

Constructors

WordVal !w

Packed word representation for bit sequences.

BitsVal !(Seq (Eval b))

Sequence of thunks representing bits.

LargeBitsVal !Integer !(SeqMap b w i)

A large bitvector sequence, represented as a SeqMap of bits.

Instances
Generic (WordValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Associated Types

type Rep (WordValue b w i) :: Type -> Type #

Methods

from :: WordValue b w i -> Rep (WordValue b w i) x #

to :: Rep (WordValue b w i) x -> WordValue b w i #

(NFData w, NFData b) => NFData (WordValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

rnf :: WordValue b w i -> () #

type Rep (WordValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

largeBitSize :: Integer Source #

An arbitrarily-chosen number of elements where we switch from a dense sequence representation of bit-level words to SeqMap representation.

asWordVal :: BitWord b w i => WordValue b w i -> Eval w Source #

Force a word value into packed word form

asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i Source #

Force a word value into a sequence of bits

enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b] Source #

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.

enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b] Source #

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.

wordValueSize :: BitWord b w i => WordValue b w i -> Integer Source #

Compute the size of a word value

indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b Source #

Select an individual bit from a word value

updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i) Source #

Produce a new WordValue from the one given by updating the ith bit with the given bit value.

data GenValue b w i Source #

Generic value type, parameterized by bit and word types.

NOTE: we maintain an important invariant regarding sequence types. VSeq must never be used for finite sequences of bits. Always use the VWord constructor instead! Infinite sequences of bits are handled by the VStream constructor, just as for other types.

Constructors

VRecord ![(Ident, Eval (GenValue b w i))]
 { .. }
VTuple ![Eval (GenValue b w i)]
 ( .. )
VBit !b
 Bit
VInteger !i

Integer or Z n

VSeq !Integer !(SeqMap b w i)

[n]a Invariant: VSeq is never a sequence of bits

VWord !Integer !(Eval (WordValue b w i))
 [n]Bit
VStream !(SeqMap b w i)
 [inf]a
VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))

functions

VPoly (TValue -> Eval (GenValue b w i))

polymorphic values (kind *)

VNumPoly (Nat' -> Eval (GenValue b w i))

polymorphic values (kind #)

Instances
(Show b, Show w, Show i) => Show (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

showsPrec :: Int -> GenValue b w i -> ShowS #

show :: GenValue b w i -> String #

showList :: [GenValue b w i] -> ShowS #

Generic (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Associated Types

type Rep (GenValue b w i) :: Type -> Type #

Methods

from :: GenValue b w i -> Rep (GenValue b w i) x #

to :: Rep (GenValue b w i) x -> GenValue b w i #

(NFData b, NFData i, NFData w) => NFData (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Methods

rnf :: GenValue b w i -> () #

type Rep (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

type Rep (GenValue b w i) = D1 (MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (((C1 (MetaCons "VRecord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Ident, Eval (GenValue b w i))])) :+: C1 (MetaCons "VTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Eval (GenValue b w i)]))) :+: (C1 (MetaCons "VBit" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 b)) :+: (C1 (MetaCons "VInteger" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 i)) :+: C1 (MetaCons "VSeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w i)))))) :+: ((C1 (MetaCons "VWord" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Eval (WordValue b w i)))) :+: C1 (MetaCons "VStream" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (SeqMap b w i)))) :+: (C1 (MetaCons "VFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Eval (GenValue b w i) -> Eval (GenValue b w i)))) :+: (C1 (MetaCons "VPoly" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TValue -> Eval (GenValue b w i)))) :+: C1 (MetaCons "VNumPoly" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nat' -> Eval (GenValue b w i))))))))

forceWordValue :: WordValue b w i -> Eval () Source #

Force the evaluation of a word value

forceValue :: GenValue b w i -> Eval () Source #

Force the evaluation of a value

atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c) Source #

atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b) Source #

ppValue :: forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc Source #

class BitWord b w i | b -> w, w -> i, i -> b where Source #

This type class defines a collection of operations on bits and words that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.

Methods

ppBit :: b -> Doc Source #

Pretty-print an individual bit

ppWord :: PPOpts -> w -> Doc Source #

Pretty-print a word value

ppInteger :: PPOpts -> i -> Doc Source #

Pretty-print an integer value

wordAsChar :: w -> Maybe Char Source #

Attempt to render a word value as an ASCII character. Return Nothing if the character value is unknown (e.g., for symbolic values).

wordLen :: w -> Integer Source #

The number of bits in a word value.

bitLit :: Bool -> b Source #

Construct a literal bit value from a boolean.

wordLit Source #

Arguments

:: Integer

Width

-> Integer

Value

-> w 

Construct a literal word value given a bit width and a value.

integerLit Source #

Arguments

:: Integer

Value

-> i 

Construct a literal integer value from the given integer.

wordBit :: w -> Integer -> b Source #

Extract the numbered bit from the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

wordUpdate :: w -> Integer -> b -> w Source #

Update the numbered bit in the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

packWord :: [b] -> w Source #

Construct a word value from a finite sequence of bits. NOTE: this assumes that the sequence of bits is big-endian and finite, so the first element of the list will be the most significant bit.

unpackWord :: w -> [b] Source #

Deconstruct a packed word value in to a finite sequence of bits. NOTE: this produces a list of bits that represent a big-endian word, so the most significant bit is the first element of the list.

joinWord :: w -> w -> w Source #

Concatenate the two given word values. NOTE: the first argument represents the more-significant bits

splitWord Source #

Arguments

:: Integer

left width

-> Integer

right width

-> w 
-> (w, w) 

Take the most-significant bits, and return those bits and the remainder. The first element of the pair is the most significant bits. The two integer sizes must sum to the length of the given word value.

extractWord Source #

Arguments

:: Integer

Number of bits to take

-> Integer

starting bit

-> w 
-> w 

Extract a subsequence of bits from a packed word value. The first integer argument is the number of bits in the resulting word. The second integer argument is the number of less-significant digits to discard. Stated another way, the operation `extractWord n i w` is equivalent to first shifting w right by i bits, and then truncating to n bits.

wordPlus :: w -> w -> w Source #

2's complement addition of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMinus :: w -> w -> w Source #

2's complement subtraction of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMult :: w -> w -> w Source #

2's complement multiplication of packed words. The arguments must have equal bit width, and the result is of the same width. The high bits of the multiplication are silently discarded.

wordToInt :: w -> i Source #

Construct an integer value from the given packed word.

intPlus :: i -> i -> i Source #

Addition of unbounded integers.

intMinus :: i -> i -> i Source #

Subtraction of unbounded integers.

intMult :: i -> i -> i Source #

Multiplication of unbounded integers.

intModPlus :: Integer -> i -> i -> i Source #

Addition of integers modulo n, for a concrete positive integer n.

intModMinus :: Integer -> i -> i -> i Source #

Subtraction of integers modulo n, for a concrete positive integer n.

intModMult :: Integer -> i -> i -> i Source #

Multiplication of integers modulo n, for a concrete positive integer n.

wordFromInt :: Integer -> i -> w Source #

Construct a packed word of the specified width from an integer value.

Instances
BitWord Bool BV Integer Source # 
Instance details

Defined in Cryptol.Eval.Value

BitWord SBool SWord SInteger Source # 
Instance details

Defined in Cryptol.Symbolic.Value

class BitWord b w i => EvalPrims b w i where Source #

This class defines additional operations necessary to define generic evaluation functions.

Methods

evalPrim :: Decl -> GenValue b w i Source #

Eval prim binds primitive declarations to the primitive values that implement them.

iteValue Source #

Arguments

:: b

Test bit

-> Eval (GenValue b w i)

'then' value

-> Eval (GenValue b w i)

'else' value

-> Eval (GenValue b w i) 

ifthenelse operation. Choose either the 'then' value or the 'else' value depending on the value of the test bit.

mask Source #

Arguments

:: Integer

Bit-width

-> Integer

Value

-> Integer

Masked result

word :: BitWord b w i => Integer -> Integer -> GenValue b w i Source #

Create a packed word of n bits.

lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i Source #

wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i Source #

Functions that assume word inputs

tlam :: (TValue -> GenValue b w i) -> GenValue b w i Source #

A type lambda that expects a Type.

nlam :: (Nat' -> GenValue b w i) -> GenValue b w i Source #

A type lambda that expects a Type of kind #.

toStream :: [GenValue b w i] -> Eval (GenValue b w i) Source #

Generate a stream.

toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i Source #

boolToWord :: [Bool] -> Value Source #

This is strict!

toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i) Source #

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i Source #

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

fromVBit :: GenValue b w i -> b Source #

Extract a bit value.

fromVInteger :: GenValue b w i -> i Source #

Extract an integer value.

fromVSeq :: GenValue b w i -> SeqMap b w i Source #

Extract a finite sequence value.

fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i) Source #

Extract a sequence.

fromBit :: GenValue b w i -> Eval b Source #

fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w Source #

Extract a packed word.

tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w Source #

If the given list of values are all fully-evaluated thunks containing bits, return a packed word built from the same bits. However, if any value is not a fully-evaluated bit, return Nothing.

fromWord :: String -> Value -> Eval Integer Source #

Turn a value into an integer represented by w bits.

fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i) Source #

Extract a function from a value.

fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i) Source #

Extract a polymorphic function from a value.

fromVNumPoly :: GenValue b w i -> Nat' -> Eval (GenValue b w i) Source #

Extract a polymorphic function from a value.

fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)] Source #

Extract a tuple from a value.

fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))] Source #

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i) Source #

Lookup a field in a record.

toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr) Source #

Given an expected type, returns an expression that evaluates to this value, if we can determine it.

XXX: View patterns would probably clean up this definition a lot.