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.Eval.Value

Description

Synopsis

- data BV = BV !Integer !Integer
- binBV :: (Integer -> Integer -> Integer) -> BV -> BV -> BV
- unaryBV :: (Integer -> Integer) -> BV -> BV
- bvVal :: BV -> Integer
- mkBv :: Integer -> Integer -> BV
- data SeqMap b w i
  - = IndexSeqMap !(Integer -> Eval (GenValue b w i))
  - | UpdateSeqMap !(Map Integer (Eval (GenValue b w i))) !(Integer -> Eval (GenValue b w i))
- lookupSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i)
- type SeqValMap = SeqMap Bool BV Integer
- finiteSeqMap :: [Eval (GenValue b w i)] -> SeqMap b w i
- infiniteSeqMap :: [Eval (GenValue b w i)] -> Eval (SeqMap b w i)
- enumerateSeqMap :: Integral n => n -> SeqMap b w i -> [Eval (GenValue b w i)]
- streamSeqMap :: SeqMap b w i -> [Eval (GenValue b w i)]
- reverseSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
- updateSeqMap :: SeqMap b w i -> Integer -> Eval (GenValue b w i) -> SeqMap b w i
- concatSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i -> SeqMap b w i
- splitSeqMap :: Integer -> SeqMap b w i -> (SeqMap b w i, SeqMap b w i)
- dropSeqMap :: Integer -> SeqMap b w i -> SeqMap b w i
- memoMap :: SeqMap b w i -> Eval (SeqMap b w i)
- 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)
- mapSeqMap :: (GenValue b w i -> Eval (GenValue b w i)) -> SeqMap b w i -> Eval (SeqMap b w i)
- data WordValue b w i
  - = WordVal !w
  - | BitsVal !(Seq (Eval b))
  - | LargeBitsVal !Integer !(SeqMap b w i)
- largeBitSize :: Integer
- asWordVal :: BitWord b w i => WordValue b w i -> Eval w
- asBitsMap :: BitWord b w i => WordValue b w i -> SeqMap b w i
- enumerateWordValue :: BitWord b w i => WordValue b w i -> Eval [b]
- enumerateWordValueRev :: BitWord b w i => WordValue b w i -> Eval [b]
- wordValueSize :: BitWord b w i => WordValue b w i -> Integer
- checkedSeqIndex :: Seq a -> Integer -> Eval a
- checkedIndex :: [a] -> Integer -> Eval a
- indexWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b
- updateWordValue :: BitWord b w i => WordValue b w i -> Integer -> Eval b -> Eval (WordValue b w i)
- data GenValue b w i
  - = VRecord ![(Ident, Eval (GenValue b w i))]
  - | VTuple ![Eval (GenValue b w i)]
  - | VBit !b
  - | VInteger !i
  - | VSeq !Integer !(SeqMap b w i)
  - | VWord !Integer !(Eval (WordValue b w i))
  - | VStream !(SeqMap b w i)
  - | VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))
  - | VPoly (TValue -> Eval (GenValue b w i))
  - | VNumPoly (Nat' -> Eval (GenValue b w i))
- forceWordValue :: WordValue b w i -> Eval ()
- forceValue :: GenValue b w i -> Eval ()
- type Value = GenValue Bool BV Integer
- defaultPPOpts :: PPOpts
- atFst :: Functor f => (a -> f b) -> (a, c) -> f (b, c)
- atSnd :: Functor f => (a -> f b) -> (c, a) -> f (c, b)
- ppValue :: forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
- asciiMode :: PPOpts -> Integer -> Bool
- integerToChar :: Integer -> Char
- ppBV :: PPOpts -> BV -> Doc
- class BitWord b w i | b -> w, w -> i, i -> b where
  - ppBit :: b -> Doc
  - ppWord :: PPOpts -> w -> Doc
  - ppInteger :: PPOpts -> i -> Doc
  - wordAsChar :: w -> Maybe Char
  - wordLen :: w -> Integer
  - bitLit :: Bool -> b
  - wordLit :: Integer -> Integer -> w
  - integerLit :: Integer -> i
  - wordBit :: w -> Integer -> b
  - wordUpdate :: w -> Integer -> b -> w
  - packWord :: [b] -> w
  - unpackWord :: w -> [b]
  - joinWord :: w -> w -> w
  - splitWord :: Integer -> Integer -> w -> (w, w)
  - extractWord :: Integer -> Integer -> w -> w
  - wordPlus :: w -> w -> w
  - wordMinus :: w -> w -> w
  - wordMult :: w -> w -> w
  - wordToInt :: w -> i
  - intPlus :: i -> i -> i
  - intMinus :: i -> i -> i
  - intMult :: i -> i -> i
  - intModPlus :: Integer -> i -> i -> i
  - intModMinus :: Integer -> i -> i -> i
  - intModMult :: Integer -> i -> i -> i
  - wordFromInt :: Integer -> i -> w
- class BitWord b w i => EvalPrims b w i where
  - evalPrim :: Decl -> Maybe (GenValue b w i)
  - iteValue :: b -> Eval (GenValue b w i) -> Eval (GenValue b w i) -> Eval (GenValue b w i)
- mask :: Integer -> Integer -> Integer
- word :: BitWord b w i => Integer -> Integer -> GenValue b w i
- lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
- wlam :: BitWord b w i => (w -> Eval (GenValue b w i)) -> GenValue b w i
- tlam :: (TValue -> GenValue b w i) -> GenValue b w i
- nlam :: (Nat' -> GenValue b w i) -> GenValue b w i
- toStream :: [GenValue b w i] -> Eval (GenValue b w i)
- toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i
- boolToWord :: [Bool] -> Value
- toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
- mkSeq :: Nat' -> TValue -> SeqMap b w i -> GenValue b w i
- fromVBit :: GenValue b w i -> b
- fromVInteger :: GenValue b w i -> i
- fromVSeq :: GenValue b w i -> SeqMap b w i
- fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
- fromStr :: Value -> Eval String
- fromBit :: GenValue b w i -> Eval b
- fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i)
- fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
- vWordLen :: BitWord b w i => GenValue b w i -> Maybe Integer
- tryFromBits :: BitWord b w i => [Eval (GenValue b w i)] -> Maybe w
- fromWord :: String -> Value -> Eval Integer
- fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
- fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)
- fromVNumPoly :: GenValue b w i -> Nat' -> Eval (GenValue b w i)
- fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
- fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
- lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
- toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)

# 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

Instances details

Show BV Source # |
Instance details Defined in Cryptol.Eval.Value Methods showsPrec :: Int -> BV -> ShowS Source # show :: BV -> String Source # showList :: [BV] -> ShowS Source #
Generic BV Source # |
Instance details Defined in Cryptol.Eval.Value Associated Types type Rep BV :: Type -> Type Source # Methods from :: BV -> Rep BV x Source # to :: Rep BV x -> BV Source #
NFData BV Source # |
Instance details Defined in Cryptol.Eval.Value Methods rnf :: BV -> () Source #
EvalPrims Bool BV Integer Source # |
Instance details Defined in Cryptol.Prims.Eval Methods evalPrim :: Decl -> Maybe (GenValue Bool BV Integer) Source # iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) Source #
BitWord Bool BV Integer Source # |

Instance details

Defined in Cryptol.Eval.Value

Methods

ppBit :: Bool -> Doc Source #

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

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

wordAsChar :: BV -> Maybe Char Source #

wordLen :: BV -> Integer Source #

bitLit :: Bool -> Bool Source #

wordLit :: Integer -> Integer -> BV Source #

integerLit :: Integer -> Integer Source #

wordBit :: BV -> Integer -> Bool Source #

wordUpdate :: BV -> Integer -> Bool -> BV Source #

packWord :: [Bool] -> BV Source #

unpackWord :: BV -> [Bool] Source #

joinWord :: BV -> BV -> BV Source #

splitWord :: Integer -> Integer -> BV -> (BV, BV) Source #

extractWord :: Integer -> Integer -> BV -> BV Source #

wordPlus :: BV -> BV -> BV Source #

wordMinus :: BV -> BV -> BV Source #

wordMult :: BV -> BV -> BV Source #

wordToInt :: BV -> Integer Source #

intPlus :: Integer -> Integer -> Integer Source #

intMinus :: Integer -> Integer -> Integer Source #

intMult :: Integer -> Integer -> Integer Source #

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

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

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

wordFromInt :: Integer -> Integer -> BV Source #

type Rep BV Source # |

Instance details

Defined in Cryptol.Eval.Value

type Rep BV = D1 ('MetaData "BV" "Cryptol.Eval.Value" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "BV" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer)))

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.

bvVal :: BV -> Integer Source #

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

Smart constructor for `BV`s 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

Instances details

NFData (SeqMap b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Methods rnf :: SeqMap b w i -> () Source #

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

type SeqValMap = SeqMap Bool BV Integer Source #

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

Instances details

Generic (WordValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Associated Types type Rep (WordValue b w i) :: Type -> Type Source # Methods from :: WordValue b w i -> Rep (WordValue b w i) x Source # to :: Rep (WordValue b w i) x -> WordValue b w i Source #
(NFData w, NFData b) => NFData (WordValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Methods rnf :: WordValue b w i -> () Source #
type Rep (WordValue b w i) Source # |

Instance details

Defined in Cryptol.Eval.Value

type Rep (WordValue b w i) = D1 ('MetaData "WordValue" "Cryptol.Eval.Value" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "WordVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 w)) :+: (C1 ('MetaCons "BitsVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Seq (Eval b)))) :+: C1 ('MetaCons "LargeBitsVal" '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)))))

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

checkedSeqIndex :: Seq a -> Integer -> Eval a Source #

checkedIndex :: [a] -> Integer -> Eval a Source #

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 `i`th 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

Instances details

(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 Source # show :: GenValue b w i -> String Source # showList :: [GenValue b w i] -> ShowS Source #
Generic (GenValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Associated Types type Rep (GenValue b w i) :: Type -> Type Source # Methods from :: GenValue b w i -> Rep (GenValue b w i) x Source # to :: Rep (GenValue b w i) x -> GenValue b w i Source #
(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 -> () Source #
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.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

type Value = GenValue Bool BV Integer Source #

defaultPPOpts :: PPOpts Source #

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 #

asciiMode :: PPOpts -> Integer -> Bool Source #

integerToChar :: Integer -> Char Source #

ppBV :: PPOpts -> BV -> 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

Instances details

BitWord Bool BV Integer Source # |

Instance details

Defined in Cryptol.Eval.Value

Methods

ppBit :: Bool -> Doc Source #

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

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

wordAsChar :: BV -> Maybe Char Source #

wordLen :: BV -> Integer Source #

bitLit :: Bool -> Bool Source #

wordLit :: Integer -> Integer -> BV Source #

integerLit :: Integer -> Integer Source #

wordBit :: BV -> Integer -> Bool Source #

wordUpdate :: BV -> Integer -> Bool -> BV Source #

packWord :: [Bool] -> BV Source #

unpackWord :: BV -> [Bool] Source #

joinWord :: BV -> BV -> BV Source #

splitWord :: Integer -> Integer -> BV -> (BV, BV) Source #

extractWord :: Integer -> Integer -> BV -> BV Source #

wordPlus :: BV -> BV -> BV Source #

wordMinus :: BV -> BV -> BV Source #

wordMult :: BV -> BV -> BV Source #

wordToInt :: BV -> Integer Source #

intPlus :: Integer -> Integer -> Integer Source #

intMinus :: Integer -> Integer -> Integer Source #

intMult :: Integer -> Integer -> Integer Source #

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

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

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

wordFromInt :: Integer -> Integer -> BV Source #

BitWord SBool SWord SInteger Source # |

Instance details

Defined in Cryptol.Symbolic.Value

Methods

ppBit :: SBool -> Doc Source #

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

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

wordAsChar :: SWord -> Maybe Char Source #

wordLen :: SWord -> Integer Source #

bitLit :: Bool -> SBool Source #

wordLit :: Integer -> Integer -> SWord Source #

integerLit :: Integer -> SInteger Source #

wordBit :: SWord -> Integer -> SBool Source #

wordUpdate :: SWord -> Integer -> SBool -> SWord Source #

packWord :: [SBool] -> SWord Source #

unpackWord :: SWord -> [SBool] Source #

joinWord :: SWord -> SWord -> SWord Source #

splitWord :: Integer -> Integer -> SWord -> (SWord, SWord) Source #

extractWord :: Integer -> Integer -> SWord -> SWord Source #

wordPlus :: SWord -> SWord -> SWord Source #

wordMinus :: SWord -> SWord -> SWord Source #

wordMult :: SWord -> SWord -> SWord Source #

wordToInt :: SWord -> SInteger Source #

intPlus :: SInteger -> SInteger -> SInteger Source #

intMinus :: SInteger -> SInteger -> SInteger Source #

intMult :: SInteger -> SInteger -> SInteger Source #

intModPlus :: Integer -> SInteger -> SInteger -> SInteger Source #

intModMinus :: Integer -> SInteger -> SInteger -> SInteger Source #

intModMult :: Integer -> SInteger -> SInteger -> SInteger Source #

wordFromInt :: Integer -> SInteger -> SWord Source #

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 -> Maybe (GenValue b w i) Source #

Eval prim binds primitive declarations to the primitive values that implement them. Returns `Nothing` for abstract primitives (i.e., once that are not implemented by this backend).

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.

#### Instances

Instances details

EvalPrims Bool BV Integer Source # |
Instance details Defined in Cryptol.Prims.Eval Methods evalPrim :: Decl -> Maybe (GenValue Bool BV Integer) Source # iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) Source #
EvalPrims SBool SWord SInteger Source # |
Instance details Defined in Cryptol.Symbolic.Prims Methods evalPrim :: Decl -> Maybe (GenValue SBool SWord SInteger) Source # iteValue :: SBool -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) Source #

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.

fromStr :: Value -> Eval String Source #

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

fromWordVal :: String -> GenValue b w i -> Eval (WordValue b w i) Source #

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

Extract a packed word.

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

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.