cryptol-2.4.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 | Haskell98

Cryptol.Prims.Eval

Description

Synopsis

- evalPrim :: Decl -> Value
- primTable :: Map Ident Value
- ecDemoteV :: Value
- divModPoly :: Integer -> Int -> Integer -> Int -> (Integer, Integer)
- modExp :: Integer -> Integer -> Integer -> Integer
- doubleAndAdd :: Integer -> Integer -> Integer -> Integer
- type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w
- type Binary = GenBinary Bool BV
- binary :: GenBinary b w -> GenValue b w
- type GenUnary b w = TValue -> GenValue b w -> GenValue b w
- type Unary = GenUnary Bool BV
- unary :: GenUnary b w -> GenValue b w
- liftBinArith :: (Integer -> Integer -> Integer) -> BinArith
- type BinArith = Integer -> Integer -> Integer -> Integer
- arithBinary :: BinArith -> Binary
- arithUnary :: (Integer -> Integer) -> Unary
- lg2 :: Integer -> Integer
- divWrap :: Integral a => a -> a -> a
- modWrap :: Integral a => a -> a -> a
- lexCompare :: TValue -> Value -> Value -> Ordering
- zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering
- cmpOrder :: (Ordering -> Bool) -> Binary
- withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary
- maxV :: Ordering -> TValue -> Value -> Value -> Value
- minV :: Ordering -> TValue -> Value -> Value -> Value
- funCmp :: (Ordering -> Bool) -> Value
- zeroV :: TValue -> Value
- joinV :: Nat' -> Nat' -> TValue -> Value -> Value
- splitAtV :: Nat' -> Nat' -> TValue -> Value -> Value
- ecSplitV :: Value
- infChunksOf :: Integer -> [a] -> [[a]]
- finChunksOf :: Integer -> Integer -> [a] -> [[a]]
- ccatV :: Nat' -> Nat' -> TValue -> Value -> Value -> Value
- logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary
- logicUnary :: (forall a. Bits a => a -> a) -> Unary
- logicShift :: (Integer -> Integer -> Integer -> Integer) -> (Nat' -> TValue -> [Value] -> Integer -> [Value]) -> Value
- shiftLW :: Integer -> Integer -> Integer -> Integer
- shiftLS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
- shiftRW :: Integer -> Integer -> Integer -> Integer
- shiftRS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
- rotateLW :: Integer -> Integer -> Integer -> Integer
- rotateLS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
- rotateRW :: Integer -> Integer -> Integer -> Integer
- rotateRS :: Nat' -> TValue -> [Value] -> Integer -> [Value]
- indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value
- indexFront :: Maybe Integer -> [Value] -> Integer -> Value
- indexBack :: Maybe Integer -> [Value] -> Integer -> Value
- indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value
- indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
- indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value]
- fromThenV :: Value
- fromToV :: Value
- fromThenToV :: Value
- randomV :: TValue -> Integer -> Value

# Documentation

evalPrim :: Decl -> Value Source #

primTable :: Map Ident Value Source #

ecDemoteV :: Value Source #

Make a numeric constant.

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

modExp Source #

Arguments

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

Create a packed word

doubleAndAdd Source #

Arguments

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

type GenBinary b w = TValue -> GenValue b w -> GenValue b w -> GenValue b w Source #

type Binary = GenBinary Bool BV Source #

binary :: GenBinary b w -> GenValue b w Source #

type GenUnary b w = TValue -> GenValue b w -> GenValue b w Source #

type Unary = GenUnary Bool BV Source #

unary :: GenUnary b w -> GenValue b w Source #

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

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

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

arithBinary :: BinArith -> Binary Source #

arithUnary :: (Integer -> Integer) -> Unary Source #

lg2 :: Integer -> Integer Source #

divWrap :: Integral a => a -> a -> a Source #

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

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

Lexicographic ordering on two values.

zipLexCompare :: [TValue] -> [Value] -> [Value] -> Ordering Source #

cmpOrder :: (Ordering -> Bool) -> Binary Source #

Process two elements based on their lexicographic ordering.

withOrder :: (Ordering -> TValue -> Value -> Value -> Value) -> Binary Source #

maxV :: Ordering -> TValue -> Value -> Value -> Value Source #

minV :: Ordering -> TValue -> Value -> Value -> Value Source #

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

zeroV :: TValue -> Value Source #

joinV :: Nat' -> Nat' -> TValue -> Value -> Value Source #

Join a sequence of sequences into a single sequence.

splitAtV :: Nat' -> Nat' -> TValue -> Value -> Value Source #

ecSplitV :: Value Source #

Split implementation.

infChunksOf :: Integer -> [a] -> [[a]] Source #

Split into infinitely many chunks

finChunksOf :: Integer -> Integer -> [a] -> [[a]] Source #

Split into finitely many chunks

ccatV :: Nat' -> Nat' -> TValue -> Value -> Value -> Value Source #

logicBinary :: (forall a. Bits a => a -> a -> a) -> Binary Source #

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

logicUnary :: (forall a. Bits a => a -> a) -> Unary 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.
-> (Nat' -> TValue -> [Value] -> Integer -> [Value]) |
-> Value |

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

shiftLS :: Nat' -> TValue -> [Value] -> Integer -> [Value] Source #

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

shiftRS :: Nat' -> TValue -> [Value] -> Integer -> [Value] Source #

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

rotateLS :: Nat' -> TValue -> [Value] -> Integer -> [Value] Source #

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

rotateRS :: Nat' -> TValue -> [Value] -> Integer -> [Value] Source #

indexPrimOne :: (Maybe Integer -> [Value] -> Integer -> Value) -> Value Source #

Indexing operations that return one element.

indexFront :: Maybe Integer -> [Value] -> Integer -> Value Source #

indexBack :: Maybe Integer -> [Value] -> Integer -> Value Source #

indexPrimMany :: (Maybe Integer -> [Value] -> [Integer] -> [Value]) -> Value Source #

Indexing operations that return many elements.

indexFrontRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] Source #

indexBackRange :: Maybe Integer -> [Value] -> [Integer] -> [Value] Source #

fromThenV :: Value Source #

fromToV :: Value Source #

fromThenToV :: Value Source #

randomV :: TValue -> Integer -> Value 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