Cryptol.Symbolic.Prims

Documentation

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

primTable :: Map Ident Value

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

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

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

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

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

wordValueEqualsInteger :: WordValue SBool SWord SInteger -> Integer -> Eval SBool

Compare a symbolic word value with a concrete integer.

lazyMergeBit :: SBool -> Eval SBool -> Eval SBool -> Eval SBool

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

updateFrontSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)

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

updateBackSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)

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

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

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

liftBin :: (a -> b -> c) -> a -> b -> Eval c

liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a

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

sModAdd :: Integer -> SInteger -> SInteger -> Eval SInteger

sModSub :: Integer -> SInteger -> SInteger -> Eval SInteger

sModMult :: Integer -> SInteger -> SInteger -> Eval SInteger

sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger

sLg2 :: Integer -> SWord -> Eval SWord

Ceiling (log_2 x)

svLg2 :: SInteger -> Eval SInteger

Ceiling (log_2 x)

svModLg2 :: Integer -> SInteger -> Eval SInteger

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

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

cmpSignedLt :: 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

cmpMod :: (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool

cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool

cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool

svDivisible :: Integer -> SInteger -> SBool

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

signedQuot :: SWord -> SWord -> SWord

signedRem :: SWord -> SWord -> SWord

sshrV :: Value

carry :: SWord -> SWord -> Eval Value

scarry :: SWord -> SWord -> Eval Value

Orphan instances

EvalPrims SBool SWord SInteger

Methods

evalPrim :: Decl -> GenValue SBool SWord SInteger

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