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

Cryptol.Backend.Concrete

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

Instances details

Show BV Source #
Instance details Defined in Cryptol.Backend.Concrete 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 #

data Concrete Source #

Constructors

Concrete

Instances

Instances details

Show Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete Methods showsPrec :: Int -> Concrete -> ShowS # show :: Concrete -> String # showList :: [Concrete] -> ShowS #
Backend Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete Associated Types type SBit Concrete Source # type SWord Concrete Source # type SInteger Concrete Source # type SFloat Concrete 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 -> Maybe (SEval Concrete a) -> String -> SEval Concrete (SEval Concrete a) Source # sSpark :: Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a) Source # sPushFrame :: Concrete -> Name -> Range -> SEval Concrete a -> SEval Concrete a Source # sWithCallStack :: Concrete -> CallStack -> SEval Concrete a -> SEval Concrete a Source # sModifyCallStack :: Concrete -> (CallStack -> CallStack) -> SEval Concrete a -> SEval Concrete a Source # sGetCallStack :: Concrete -> SEval Concrete CallStack 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 # 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 # fpAsLit :: Concrete -> SFloat Concrete -> Maybe BF 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 # fpExactLit :: Concrete -> BF -> 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 # iteFloat :: Concrete -> SBit Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat 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 # znRecip :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger 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 # fpLogicalEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpNaN :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete) Source # fpPosInf :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat 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 # fpAbs :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source # fpSqrt :: Concrete -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source # fpFMA :: Concrete -> SWord Concrete -> SFloat Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source # fpIsZero :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpIsNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpIsNaN :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpIsInf :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpIsNorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpIsSubnorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source # fpToBits :: Concrete -> SFloat Concrete -> SEval Concrete (SWord Concrete) Source # fpFromBits :: Concrete -> Integer -> Integer -> SWord 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 # fpToRational :: Concrete -> SFloat Concrete -> SEval Concrete (SRational Concrete) Source # fpFromRational :: Concrete -> Integer -> Integer -> SWord Concrete -> SRational Concrete -> SEval Concrete (SFloat Concrete) Source #
type SBit Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete type SBit Concrete = Bool
type SWord Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete type SWord Concrete = BV
type SInteger Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete type SInteger Concrete = Integer
type SFloat Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete type SFloat Concrete = BF
type SEval Concrete Source #
Instance details Defined in Cryptol.Backend.Concrete 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 #