Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell2010

Cryptol.Symbolic.Prims

Contents

Orphan instances

Description

Synopsis

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
logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value
selectV :: forall a. (SBool -> Eval a -> Eval a -> Eval a) -> WordValue SBool SWord SInteger -> (Integer -> Eval a) -> Eval a
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
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
sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger
sLg2 :: Integer -> SWord -> Eval SWord
svLg2 :: SInteger -> Eval SInteger
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

Documentation

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

primTable :: Map Ident Value Source #

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

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

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

selectV Source #

Arguments

:: (SBool -> Eval a -> Eval a -> Eval a)	Mux function on `a`s
-> WordValue SBool SWord SInteger	Symbolic index value
-> (Integer -> Eval a)	Function from concrete indices to answers
-> Eval a	overall answer

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

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

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

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

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

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

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

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

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

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

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

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

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

sExp :: Integer -> SWord -> SWord -> Eval SWord Source #

sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger Source #

sLg2 :: Integer -> SWord -> Eval SWord Source #

Ceiling (log_2 x)

svLg2 :: SInteger -> Eval SInteger Source #

Ceiling (log_2 x)

svModLg2 :: Integer -> SInteger -> Eval SInteger Source #

cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpLt :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpLtEq :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

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

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

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

svDivisible :: Integer -> SInteger -> SBool Source #

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 Source #

signedQuot :: SWord -> SWord -> SWord Source #

signedRem :: SWord -> SWord -> SWord Source #

sshrV :: Value Source #

carry :: SWord -> SWord -> Eval Value Source #

scarry :: SWord -> SWord -> Eval Value Source #

Orphan instances

EvalPrims SBool SWord SInteger Source #
Instance details Methods evalPrim :: Decl -> GenValue SBool SWord SInteger Source # iteValue :: SBool -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) Source #