cryptol-2.6.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.Prims.Eval

Contents

- Orphan instances

Description

Synopsis

- primTable :: Map Ident Value
- mkLit :: BitWord b w i => TValue -> Integer -> GenValue b w i
- ecNumberV :: BitWord b w i => GenValue b w i
- ecToIntegerV :: BitWord b w i => GenValue b w i
- ecFromIntegerV :: BitWord b w i => (Integer -> i -> i) -> GenValue b w i
- modExp :: Integer -> BV -> BV -> Eval BV
- intModExp :: Integer -> Integer -> Integer -> Eval Integer
- integerExp :: Integer -> Integer -> Eval Integer
- integerLg2 :: Integer -> Eval Integer
- integerNeg :: Integer -> Eval Integer
- intModNeg :: Integer -> Integer -> Eval Integer
- doubleAndAdd :: Integer -> Integer -> Integer -> Integer
- type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
- binary :: Binary b w i -> GenValue b w i
- type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i)
- unary :: Unary b w i -> GenValue b w i
- liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV
- liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV
- type BinArith w = Integer -> w -> w -> Eval w
- liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
- liftBinIntMod :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> Eval Integer
- liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer
- modWrap :: Integral a => a -> a -> Eval a
- arithBinary :: forall b w i. BitWord b w i => BinArith w -> (i -> i -> Eval i) -> (Integer -> i -> i -> Eval i) -> Binary b w i
- type UnaryArith w = Integer -> w -> Eval w
- liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV
- arithUnary :: forall b w i. BitWord b w i => UnaryArith w -> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i
- arithNullary :: forall b w i. BitWord b w i => (Integer -> w) -> i -> (Integer -> i) -> TValue -> GenValue b w i
- lg2 :: Integer -> Integer
- addV :: BitWord b w i => Binary b w i
- subV :: BitWord b w i => Binary b w i
- mulV :: BitWord b w i => Binary b w i
- intV :: BitWord b w i => i -> TValue -> GenValue b w i
- cmpValue :: BitWord b w i => (b -> b -> Eval a -> Eval a) -> (w -> w -> Eval a -> Eval a) -> (i -> i -> Eval a -> Eval a) -> (Integer -> i -> i -> Eval a -> Eval a) -> TValue -> GenValue b w i -> GenValue b w i -> Eval a -> Eval a
- lexCompare :: TValue -> Value -> Value -> Eval Ordering
- signedLexCompare :: TValue -> Value -> Value -> Eval Ordering
- cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
- signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer
- liftWord :: BitWord b w i => (w -> w -> Eval (GenValue b w i)) -> GenValue b w i
- liftSigned :: (Integer -> Integer -> Integer -> Eval BV) -> BinArith BV
- signedBV :: BV -> Integer
- signedValue :: Integer -> Integer -> Integer
- bvSlt :: Integer -> Integer -> Integer -> Eval Value
- bvSdiv :: Integer -> Integer -> Integer -> Eval BV
- bvSrem :: Integer -> Integer -> Integer -> Eval BV
- sshrV :: Value
- scarryV :: Value
- carryV :: Value
- zeroV :: forall b w i. BitWord b w i => TValue -> GenValue b w i
- joinWordVal :: BitWord b w i => WordValue b w i -> WordValue b w i -> WordValue b w i
- joinWords :: forall b w i. BitWord b w i => Integer -> Integer -> SeqMap b w i -> Eval (GenValue b w i)
- joinSeq :: BitWord b w i => Nat' -> Integer -> TValue -> SeqMap b w i -> Eval (GenValue b w i)
- joinV :: BitWord b w i => Nat' -> Integer -> TValue -> GenValue b w i -> Eval (GenValue b w i)
- splitWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> (WordValue b w i, WordValue b w i)
- splitAtV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
- extractWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> WordValue b w i
- ecSplitV :: BitWord b w i => GenValue b w i
- reverseV :: forall b w i. BitWord b w i => GenValue b w i -> Eval (GenValue b w i)
- transposeV :: BitWord b w i => Nat' -> Nat' -> TValue -> GenValue b w i -> Eval (GenValue b w i)
- ccatV :: (Show b, Show w, BitWord b w i) => Nat' -> Nat' -> TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i)
- wordValLogicOp :: BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> WordValue b w i -> WordValue b w i -> Eval (WordValue b w i)
- logicBinary :: forall b w i. BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> Binary b w i
- wordValUnaryOp :: BitWord b w i => (b -> b) -> (w -> w) -> WordValue b w i -> Eval (WordValue b w i)
- logicUnary :: forall b w i. BitWord b w i => (b -> b) -> (w -> w) -> Unary b w i
- logicShift :: (Integer -> Integer -> Integer -> Integer) -> (Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)) -> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) -> Value
- shiftLW :: Integer -> Integer -> Integer -> Integer
- shiftLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
- shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
- shiftRW :: Integer -> Integer -> Integer -> Integer
- shiftRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
- shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
- rotateLW :: Integer -> Integer -> Integer -> Integer
- rotateLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
- rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
- rotateRW :: Integer -> Integer -> Integer -> Integer
- rotateRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)
- rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
- indexPrim :: BitWord b w i => (Maybe Integer -> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i)) -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i)) -> GenValue b w i
- indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
- indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
- indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
- indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value
- updateFront :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer)
- updateFront_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer)
- updateBack :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer)
- updateBack_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer)
- updatePrim :: BitWord b w i => (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i)) -> (Nat' -> TValue -> SeqMap b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i)) -> GenValue b w i
- fromThenV :: BitWord b w i => GenValue b w i
- fromToV :: BitWord b w i => GenValue b w i
- fromThenToV :: BitWord b w i => GenValue b w i
- infFromV :: BitWord b w i => GenValue b w i
- infFromThenV :: BitWord b w i => GenValue b w i
- randomV :: BitWord b w i => TValue -> Integer -> GenValue b w i
- errorV :: forall b w i. BitWord b w i => TValue -> String -> Eval (GenValue b w i)

# Documentation

primTable :: Map Ident Value Source #

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

Make a numeric literal value at the given type.

ecNumberV :: BitWord b w i => GenValue b w i Source #

Make a numeric constant.

ecToIntegerV :: BitWord b w i => GenValue b w i Source #

Convert a word to a non-negative integer.

ecFromIntegerV :: BitWord b w i => (Integer -> i -> i) -> GenValue b w i Source #

Convert an unbounded integer to a packed bitvector.

modExp Source #

Arguments

:: Integer | bit size of the resulting word
-> BV | base
-> BV | exponent
-> Eval BV |

Create a packed word

intModExp :: Integer -> Integer -> Integer -> Eval Integer Source #

integerExp :: Integer -> Integer -> Eval Integer Source #

integerLg2 :: Integer -> Eval Integer Source #

integerNeg :: Integer -> Eval Integer Source #

intModNeg :: Integer -> Integer -> Eval Integer Source #

doubleAndAdd Source #

Arguments

:: Integer | base
-> Integer | exponent mask
-> Integer | modulus
-> Integer |

type Binary b w i = TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i) Source #

binary :: Binary b w i -> GenValue b w i Source #

type Unary b w i = TValue -> GenValue b w i -> Eval (GenValue b w i) Source #

unary :: Unary b w i -> GenValue b w i Source #

liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV Source #

Turn a normal binop on Integers into one that can also deal with a bitsize. However, if the bitvector size is 0, always return the 0 bitvector.

liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV Source #

Turn a normal binop on Integers into one that can also deal with a bitsize. Generate a thunk that throws a divide by 0 error when forced if the second argument is 0. However, if the bitvector size is 0, always return the 0 bitvector.

type BinArith w = Integer -> w -> w -> Eval w Source #

liftBinInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer Source #

liftBinIntMod :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> Eval Integer Source #

liftDivInteger :: (Integer -> Integer -> Integer) -> Integer -> Integer -> Eval Integer Source #

modWrap :: Integral a => a -> a -> Eval a Source #

arithBinary :: forall b w i. BitWord b w i => BinArith w -> (i -> i -> Eval i) -> (Integer -> i -> i -> Eval i) -> Binary b w i Source #

type UnaryArith w = Integer -> w -> Eval w Source #

liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV Source #

arithUnary :: forall b w i. BitWord b w i => UnaryArith w -> (i -> Eval i) -> (Integer -> i -> Eval i) -> Unary b w i Source #

arithNullary :: forall b w i. BitWord b w i => (Integer -> w) -> i -> (Integer -> i) -> TValue -> GenValue b w i Source #

lg2 :: Integer -> Integer Source #

addV :: BitWord b w i => Binary b w i Source #

subV :: BitWord b w i => Binary b w i Source #

mulV :: BitWord b w i => Binary b w i Source #

intV :: BitWord b w i => i -> TValue -> GenValue b w i Source #

cmpValue :: BitWord b w i => (b -> b -> Eval a -> Eval a) -> (w -> w -> Eval a -> Eval a) -> (i -> i -> Eval a -> Eval a) -> (Integer -> i -> i -> Eval a -> Eval a) -> TValue -> GenValue b w i -> GenValue b w i -> Eval a -> Eval a Source #

lexCompare :: TValue -> Value -> Value -> Eval Ordering Source #

signedLexCompare :: TValue -> Value -> Value -> Eval Ordering Source #

cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer Source #

Process two elements based on their lexicographic ordering.

signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV Integer Source #

Process two elements based on their lexicographic ordering, using signed comparisons

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

Lifted operation on finite bitsequences. Used for signed comparisons and arithemtic.

liftSigned :: (Integer -> Integer -> Integer -> Eval BV) -> BinArith BV Source #

signedBV :: BV -> Integer Source #

signedValue :: Integer -> Integer -> Integer Source #

bvSlt :: Integer -> Integer -> Integer -> Eval Value Source #

bvSdiv :: Integer -> Integer -> Integer -> Eval BV Source #

bvSrem :: Integer -> Integer -> Integer -> Eval BV Source #

sshrV :: Value Source #

scarryV :: Value Source #

Signed carry bit.

carryV :: Value Source #

Unsigned carry bit.

zeroV :: forall b w i. BitWord b w i => TValue -> GenValue b w i Source #

joinWordVal :: BitWord b w i => WordValue b w i -> WordValue b w i -> WordValue b w i Source #

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

joinSeq :: BitWord b w i => Nat' -> Integer -> TValue -> SeqMap b w i -> Eval (GenValue b w i) Source #

joinV :: BitWord b w i => Nat' -> Integer -> TValue -> GenValue b w i -> Eval (GenValue b w i) Source #

Join a sequence of sequences into a single sequence.

splitWordVal :: BitWord b w i => Integer -> Integer -> WordValue b w i -> (WordValue b w i, WordValue b w i) Source #

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

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

ecSplitV :: BitWord b w i => GenValue b w i Source #

Split implementation.

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

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

ccatV :: (Show b, Show w, BitWord b w i) => Nat' -> Nat' -> TValue -> GenValue b w i -> GenValue b w i -> Eval (GenValue b w i) Source #

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

logicBinary :: forall b w i. BitWord b w i => (b -> b -> b) -> (w -> w -> w) -> Binary b w i Source #

Merge two values given a binop. This is used for and, or and xor.

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

logicUnary :: forall b w i. BitWord b w i => (b -> b) -> (w -> w) -> Unary b w i Source #

logicShift Source #

Arguments

:: (Integer -> Integer -> Integer -> Integer) | The function may assume its arguments are masked. It is responsible for masking its result if needed.
-> (Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool)) |
-> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap) |
-> Value |

shiftLW :: Integer -> Integer -> Integer -> Integer Source #

shiftLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) Source #

shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap Source #

shiftRW :: Integer -> Integer -> Integer -> Integer Source #

shiftRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) Source #

shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap Source #

rotateLW :: Integer -> Integer -> Integer -> Integer Source #

rotateLB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) Source #

rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap Source #

rotateRW :: Integer -> Integer -> Integer -> Integer Source #

rotateRB :: Integer -> Seq (Eval Bool) -> Integer -> Seq (Eval Bool) Source #

rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap Source #

indexPrim :: BitWord b w i => (Maybe Integer -> TValue -> SeqMap b w i -> Seq b -> Eval (GenValue b w i)) -> (Maybe Integer -> TValue -> SeqMap b w i -> w -> Eval (GenValue b w i)) -> GenValue b w i Source #

Indexing operations.

indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value Source #

indexFront_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value Source #

indexBack :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value Source #

indexBack_bits :: Maybe Integer -> TValue -> SeqValMap -> Seq Bool -> Eval Value Source #

updateFront :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer) Source #

updateFront_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer) Source #

updateBack :: Nat' -> TValue -> SeqMap Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (SeqMap Bool BV Integer) Source #

updateBack_word :: Nat' -> TValue -> WordValue Bool BV Integer -> WordValue Bool BV Integer -> Eval (GenValue Bool BV Integer) -> Eval (WordValue Bool BV Integer) Source #

updatePrim :: BitWord b w i => (Nat' -> TValue -> WordValue b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (WordValue b w i)) -> (Nat' -> TValue -> SeqMap b w i -> WordValue b w i -> Eval (GenValue b w i) -> Eval (SeqMap b w i)) -> GenValue b w i Source #

fromThenV :: BitWord b w i => GenValue b w i Source #

fromToV :: BitWord b w i => GenValue b w i Source #

fromThenToV :: BitWord b w i => GenValue b w i Source #

infFromV :: BitWord b w i => GenValue b w i Source #

infFromThenV :: BitWord b w i => GenValue b w i Source #

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

Produce a random value with the given seed. If we do not support making values of the given type, return zero of that type. TODO: do better than returning zero

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

# Orphan instances

EvalPrims Bool BV Integer Source # |
Instance details Methods evalPrim :: Decl -> GenValue Bool BV Integer Source # iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) Source #