Cryptol.Symbolic.Prims

Documentation

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

primTable :: Map Ident Value

iteWord :: SBool -> Eval (WordValue SBool SWord) -> Eval (WordValue SBool SWord) -> Eval (WordValue SBool SWord)

shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a

Barrel-shifter algorithm. Takes a list of bits in big-endian order.

logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value

selectV :: forall a. (SBool -> Eval a -> Eval a -> Eval a) -> WordValue SBool SWord -> (Integer -> Eval a) -> Eval a

indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord -> SWord -> Eval Value

indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord -> SWord -> Eval Value

indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord -> Seq SBool -> Eval Value

indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord -> Seq SBool -> Eval Value

updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (SeqMap SBool SWord)

updateFrontSym_bits :: Nat' -> TValue -> Seq (Eval SBool) -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (Seq (Eval SBool))

updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (SeqMap SBool SWord)

updateBackSym_bits :: Nat' -> TValue -> Seq (Eval SBool) -> WordValue SBool SWord -> Eval (GenValue SBool SWord) -> Eval (Seq (Eval SBool))

asBitList :: [Eval SBool] -> Maybe [SBool]

asWordList :: [WordValue SBool SWord] -> Maybe [SWord]

liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord

sExp :: Integer -> SWord -> SWord -> Eval SWord

sLg2 :: Integer -> SWord -> Eval SWord

Ceiling (log_2 x)

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

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

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

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

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

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

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

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

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

Add two polynomials

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

degree :: [SBool] -> Int

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

nth :: [SBool] -> Int -> SBool

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

Orphan instances

EvalPrims SBool SWord

Methods

evalPrim :: Decl -> GenValue SBool SWord

iteValue :: SBool -> Eval (GenValue SBool SWord) -> Eval (GenValue SBool SWord) -> Eval (GenValue SBool SWord)