cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.Symbolic.Prims

Description

 
Synopsis

Documentation

traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) 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 #

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

Compare a symbolic word value with a concrete integer.

asBitList :: [Eval SBool] -> Maybe [SBool] 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 #

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

Ceiling (log_2 x)

svLg2 :: SInteger -> Eval SInteger Source #

Ceiling (log_2 x)

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

Orphan instances