Cryptol.Prims.Eval

Documentation

primTable :: Map Ident Value

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

Make a numeric literal value at the given type.

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

Make a numeric constant.

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

Convert a word to a non-negative integer.

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

Convert an unbounded integer to a packed bitvector.

modExp

Arguments

:: Integer

bit size of the resulting word

-> BV

base

-> BV

exponent

-> Eval BV

Create a packed word

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

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)

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

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

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

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

Process two elements based on their lexicographic ordering.

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

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

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

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

Signed carry bit.

carryV :: Value

Unsigned carry bit.

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)

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)

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

Split implementation.

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

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)

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

logicShift

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

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

Indexing operations.

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

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

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)

Orphan instances

EvalPrims Bool BV Integer

Methods

evalPrim :: Decl -> Maybe (GenValue Bool BV Integer)

iteValue :: Bool -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer) -> Eval (GenValue Bool BV Integer)