Cryptol.Symbolic.Prims

Documentation

traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)

evalPrim :: Decl -> Value

primTable :: Map Ident Value

selectV :: (Integer -> Value) -> Value -> Value

asWordList :: [Value] -> Maybe [SWord]

atV_list :: Bool -> Bool -> Value -> [Value] -> Value -> Value

atV :: Bool -> Value -> [Value] -> Value -> Value

iteAtV :: Value -> [Value] -> Value -> Value

replicateV

Arguments

:: Integer

number of elements

-> TValue

type of element

-> Value

element

-> Value

nth :: a -> [a] -> Int -> a

nthV :: Value -> Value -> Integer -> Value

mapV :: Bool -> (Value -> Value) -> Value -> Value

catV :: Value -> Value -> Value

dropV :: Integer -> Value -> Value

takeV :: Integer -> Value -> Value

ecDemoteV :: Value

Make a numeric constant. { val, bits } (fin val, fin bits, bits >= width val) => [bits]

type Binary = TValue -> Value -> Value -> Value

type Unary = TValue -> Value -> Value

arithBinary :: (SWord -> SWord -> SWord) -> Binary

Models functions of type `{a} (Arith a) => a -> a -> a`

arithUnary :: (SWord -> SWord) -> Unary

Models functions of type `{a} (Arith a) => a -> a`

sExp :: SWord -> SWord -> SWord

sLg2 :: SWord -> SWord

Ceiling (log_2 x)

cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> Value -> Value -> a -> a

cmpEq :: SWord -> SWord -> SBool -> SBool

cmpNotEq :: SWord -> SWord -> SBool -> SBool

cmpLt :: SWord -> SWord -> SBool -> SBool

cmpGt :: SWord -> SWord -> SBool -> SBool

cmpLtEq :: SWord -> SWord -> SBool -> SBool

cmpGtEq :: SWord -> SWord -> SBool -> SBool

cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary

errorV :: String -> TValue -> Value

zeroV :: TValue -> Value

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

Join a sequence of sequences into a single sequence.

ecSplitV :: Value

Split implementation.

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

Split into infinitely many chunks

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

Split into finitely many chunks

logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary

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

logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary

fromThenV :: Value

fromToV :: Value

fromThenToV :: Value

addPoly :: [SBool] -> [SBool] -> [SBool]

Add two polynomials

ites :: SBool -> [SBool] -> [SBool] -> [SBool]

degree :: [SBool] -> Int

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])

idx :: [SBool] -> Int -> SBool

divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])