Safe Haskell	Safe
Language	Haskell2010

Cryptol.Eval.Concrete.Value

Description

Synopsis

data BV = BV !Integer !Integer
binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV
unaryBV :: (Integer -> Integer) -> BV -> BV
bvVal :: BV -> Integer
ppBV :: PPOpts -> BV -> Doc
mkBv :: Integer -> Integer -> BV
mask :: Integer -> Integer -> Integer
signedBV :: BV -> Integer
signedValue :: Integer -> Integer -> Integer
integerToChar :: Integer -> Char
lg2 :: Integer -> Integer
type Value = GenValue Concrete
data Concrete = Concrete
liftBinIntMod :: Monad m => (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
fpBinArith :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)) -> Concrete -> SWord Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)
fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete RoundMode

Documentation

data BV Source #

Concrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1

Constructors

BV !Integer !Integer

Instances

Show BV Source #
Instance details Defined in Cryptol.Eval.Concrete.Value Methods showsPrec :: Int -> BV -> ShowS # show :: BV -> String # showList :: [BV] -> ShowS #

binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV Source #

Apply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.

unaryBV :: (Integer -> Integer) -> BV -> BV Source #

Apply an integer function to the values of a bitvector. This function assumes the function will not require masking.

bvVal :: BV -> Integer Source #

ppBV :: PPOpts -> BV -> Doc Source #

mkBv :: Integer -> Integer -> BV Source #

Smart constructor for BVs that checks for the width limit

mask Source #

Arguments

:: Integer	Bit-width
-> Integer	Value
-> Integer	Masked result

signedBV :: BV -> Integer Source #

signedValue :: Integer -> Integer -> Integer Source #

integerToChar :: Integer -> Char Source #

lg2 :: Integer -> Integer Source #

type Value = GenValue Concrete Source #

data Concrete Source #

Constructors

Concrete

Instances

Show Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value Methods showsPrec :: Int -> Concrete -> ShowS # show :: Concrete -> String # showList :: [Concrete] -> ShowS #
Backend Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value Associated Types type SBit Concrete :: Type Source # type SWord Concrete :: Type Source # type SInteger Concrete :: Type Source # type SFloat Concrete :: Type Source # type SEval Concrete :: Type -> Type Source # Methods isReady :: Concrete -> SEval Concrete a -> Bool Source # sDeclareHole :: Concrete -> String -> SEval Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ()) Source # sDelayFill :: Concrete -> SEval Concrete a -> SEval Concrete a -> SEval Concrete (SEval Concrete a) Source # sSpark :: Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a) Source # mergeEval :: Concrete -> (SBit Concrete -> a -> a -> SEval Concrete a) -> SBit Concrete -> SEval Concrete a -> SEval Concrete a -> SEval Concrete a Source # assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete () Source # raiseError :: Concrete -> EvalError -> SEval Concrete a Source # ppBit :: Concrete -> SBit Concrete -> Doc Source # ppWord :: Concrete -> PPOpts -> SWord Concrete -> Doc Source # ppInteger :: Concrete -> PPOpts -> SInteger Concrete -> Doc Source # ppFloat :: Concrete -> PPOpts -> SFloat Concrete -> Doc Source # bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool Source # wordLen :: Concrete -> SWord Concrete -> Integer Source # wordAsLit :: Concrete -> SWord Concrete -> Maybe (Integer, Integer) Source # wordAsChar :: Concrete -> SWord Concrete -> Maybe Char Source # integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer Source # bitLit :: Concrete -> Bool -> SBit Concrete Source # wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete) Source # integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete) Source # fpLit :: Concrete -> Integer -> Integer -> Rational -> SEval Concrete (SFloat Concrete) Source # iteBit :: Concrete -> SBit Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # iteWord :: Concrete -> SBit Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # iteInteger :: Concrete -> SBit Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # bitEq :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # bitOr :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # bitAnd :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # bitXor :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source # wordBit :: Concrete -> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete) Source # wordUpdate :: Concrete -> SWord Concrete -> Integer -> SBit Concrete -> SEval Concrete (SWord Concrete) Source # packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete) Source # unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete] Source # wordFromInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete) Source # joinWord :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # splitWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete, SWord Concrete) Source # extractWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordOr :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordAnd :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordXor :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordPlus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordMinus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordMult :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordSignedDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordSignedMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source # wordEq :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source # wordSignedLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source # wordLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source # wordGreaterThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source # wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete) Source # intPlus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intMinus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intMult :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intDiv :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intMod :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # intEq :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source # intLessThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source # intGreaterThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source # intToZn :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znToInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znPlus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znNegate :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znMinus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znMult :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source # znEq :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source # fpEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpLessThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpGreaterThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpPlus :: FPArith2 Concrete Source # fpMinus :: FPArith2 Concrete Source # fpMult :: FPArith2 Concrete Source # fpDiv :: FPArith2 Concrete Source # fpNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source # fpToInteger :: Concrete -> String -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SInteger Concrete) Source # fpFromInteger :: Concrete -> Integer -> Integer -> SWord Concrete -> SInteger Concrete -> SEval Concrete (SFloat Concrete) Source #
type SBit Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value type SBit Concrete = Bool
type SWord Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value type SWord Concrete = BV
type SInteger Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value type SInteger Concrete = Integer
type SFloat Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value type SFloat Concrete = BF
type SEval Concrete Source #
Instance details Defined in Cryptol.Eval.Concrete.Value type SEval Concrete = Eval

liftBinIntMod :: Monad m => (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer Source #

fpBinArith Source #

Arguments

:: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
-> Concrete
-> SWord Concrete	Rouding mode
-> SFloat Concrete
-> SFloat Concrete
-> SEval Concrete (SFloat Concrete)

fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete RoundMode Source #