Cryptol.Prims.Eval

Documentation

primTable :: Map Ident Value

ecDemoteV :: BitWord b w => GenValue b w

Make a numeric constant.

divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)

modExp

Arguments

:: Integer

bit size of the resulting word

-> BV

base

-> BV

exponent

-> Eval BV

Create a packed word

doubleAndAdd

Arguments

:: Integer

base

-> Integer

exponent mask

-> Integer

modulus

-> Integer

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

binary :: Binary b w -> GenValue b w

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

unary :: Unary b w -> GenValue b w

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

Turn a normal binop on Integers into one that can also deal with a bitsize.

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.

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

arithBinary :: forall b w. BitWord b w => BinArith w -> Binary b w

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

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

arithUnary :: forall b w. BitWord b w => UnaryArith w -> Unary b w

lg2 :: Integer -> Integer

lexCompare :: String -> TValue -> Value -> Value -> Eval Ordering

Lexicographic ordering on two values.

zipLexCompare :: String -> [TValue] -> [Eval Value] -> [Eval Value] -> Eval Ordering

cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV

Process two elements based on their lexicographic ordering.

withOrder :: String -> (Ordering -> TValue -> Value -> Value -> Value) -> Binary Bool BV

maxV :: Ordering -> TValue -> Value -> Value -> Value

minV :: Ordering -> TValue -> Value -> Value -> Value

funCmp :: (Ordering -> Bool) -> Value

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

joinWordVal :: BitWord b w => WordValue b w -> WordValue b w -> WordValue b w

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

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

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

Join a sequence of sequences into a single sequence.

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

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

extractWordVal :: BitWord b w => Integer -> Integer -> WordValue b w -> WordValue b w

ecSplitV :: BitWord b w => GenValue b w

Split implementation.

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

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

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

wordValLogicOp :: BitWord b w => (b -> b -> b) -> (w -> w -> w) -> WordValue b w -> WordValue b w -> WordValue b w

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

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

wordValUnaryOp :: BitWord b w => (b -> b) -> (w -> w) -> WordValue b w -> WordValue b w

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

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

indexPrimOne :: BitWord b w => (Maybe Integer -> TValue -> SeqMap b w -> Seq b -> Eval (GenValue b w)) -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) -> GenValue b w

Indexing operations that return one element.

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

indexPrimMany :: BitWord b w => (Maybe Integer -> TValue -> SeqMap b w -> Seq b -> Eval (GenValue b w)) -> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w)) -> GenValue b w

Indexing operations that return many elements.

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

updateFront_bits :: Nat' -> TValue -> Seq (Eval Bool) -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (Seq (Eval Bool))

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

updateBack_bits :: Nat' -> TValue -> Seq (Eval Bool) -> WordValue Bool BV -> Eval (GenValue Bool BV) -> Eval (Seq (Eval Bool))

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

fromThenV :: BitWord b w => GenValue b w

fromToV :: BitWord b w => GenValue b w

fromThenToV :: BitWord b w => GenValue b w

infFromV :: BitWord b w => GenValue b w

infFromThenV :: BitWord b w => GenValue b w

randomV :: TValue -> Integer -> Value

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. BitWord b w => TValue -> String -> Eval (GenValue b w)

Orphan instances

EvalPrims Bool BV

Methods

evalPrim :: Decl -> GenValue Bool BV

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