Cryptol.Backend.Concrete

Documentation

data BV

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

Constructors

BV !Integer !Integer

Instances

Show BV

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

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

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

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

bvVal :: BV -> Integer

ppBV :: PPOpts -> BV -> Doc

mkBv :: Integer -> Integer -> BV

Smart constructor for BVs that checks for the width limit

mask

Arguments

:: Integer

Bit-width

-> Integer

Value

-> Integer

Masked result

signedBV :: BV -> Integer

signedValue :: Integer -> Integer -> Integer

integerToChar :: Integer -> Char

lg2 :: Integer -> Integer

data Concrete

Constructors

Concrete

Instances

Show Concrete

Defined in Cryptol.Backend.Concrete

Methods

showsPrec :: Int -> Concrete -> ShowS

show :: Concrete -> String

showList :: [Concrete] -> ShowS

Backend Concrete

Defined in Cryptol.Backend.Concrete

Associated Types

type SBit Concrete

type SWord Concrete

type SInteger Concrete

type SFloat Concrete

type SEval Concrete :: Type -> Type

Methods

isReady :: Concrete -> SEval Concrete a -> SEval Concrete (Maybe a)

sDeclareHole :: Concrete -> String -> SEval Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())

sDelayFill :: Concrete -> SEval Concrete a -> Maybe (SEval Concrete a) -> String -> SEval Concrete (SEval Concrete a)

sSpark :: Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a)

sPushFrame :: Concrete -> Name -> Range -> SEval Concrete a -> SEval Concrete a

sWithCallStack :: Concrete -> CallStack -> SEval Concrete a -> SEval Concrete a

sModifyCallStack :: Concrete -> (CallStack -> CallStack) -> SEval Concrete a -> SEval Concrete a

sGetCallStack :: Concrete -> SEval Concrete CallStack

mergeEval :: Concrete -> (SBit Concrete -> a -> a -> SEval Concrete a) -> SBit Concrete -> SEval Concrete a -> SEval Concrete a -> SEval Concrete a

assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()

raiseError :: Concrete -> EvalError -> SEval Concrete a

bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool

wordLen :: Concrete -> SWord Concrete -> Integer

wordAsLit :: Concrete -> SWord Concrete -> Maybe (Integer, Integer)

wordAsChar :: Concrete -> SWord Concrete -> Maybe Char

integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer

fpAsLit :: Concrete -> SFloat Concrete -> Maybe BF

bitLit :: Concrete -> Bool -> SBit Concrete

wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete)

integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete)

fpLit :: Concrete -> Integer -> Integer -> Rational -> SEval Concrete (SFloat Concrete)

fpExactLit :: Concrete -> BF -> SEval Concrete (SFloat Concrete)

iteBit :: Concrete -> SBit Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

iteWord :: Concrete -> SBit Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

iteInteger :: Concrete -> SBit Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

iteFloat :: Concrete -> SBit Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)

bitEq :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

bitOr :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

bitAnd :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

bitXor :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)

wordBit :: Concrete -> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete)

wordUpdate :: Concrete -> SWord Concrete -> Integer -> SBit Concrete -> SEval Concrete (SWord Concrete)

packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)

unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete]

wordFromInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete)

joinWord :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

splitWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete, SWord Concrete)

extractWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordOr :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordAnd :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordXor :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordPlus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordMinus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordMult :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordSignedDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordSignedMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordShiftLeft :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordShiftRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordSignedShiftRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordRotateLeft :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordRotateRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)

wordEq :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete)

wordSignedLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete)

wordLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete)

wordGreaterThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete)

wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)

wordToSignedInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)

intPlus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intMinus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intMult :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intDiv :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intMod :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

intEq :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete)

intLessThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete)

intGreaterThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete)

intToZn :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znToInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znPlus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znNegate :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znMinus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znMult :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

znEq :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete)

znRecip :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)

fpEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpLessThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpGreaterThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpLogicalEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpNaN :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)

fpPosInf :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)

fpPlus :: FPArith2 Concrete

fpMinus :: FPArith2 Concrete

fpMult :: FPArith2 Concrete

fpDiv :: FPArith2 Concrete

fpNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)

fpAbs :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)

fpSqrt :: Concrete -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)

fpFMA :: Concrete -> SWord Concrete -> SFloat Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)

fpIsZero :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpIsNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpIsNaN :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpIsInf :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpIsNorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpIsSubnorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)

fpToBits :: Concrete -> SFloat Concrete -> SEval Concrete (SWord Concrete)

fpFromBits :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SFloat Concrete)

fpToInteger :: Concrete -> String -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SInteger Concrete)

fpFromInteger :: Concrete -> Integer -> Integer -> SWord Concrete -> SInteger Concrete -> SEval Concrete (SFloat Concrete)

fpToRational :: Concrete -> SFloat Concrete -> SEval Concrete (SRational Concrete)

fpFromRational :: Concrete -> Integer -> Integer -> SWord Concrete -> SRational Concrete -> SEval Concrete (SFloat Concrete)

type SBit Concrete

Defined in Cryptol.Backend.Concrete

type SBit Concrete = Bool

type SEval Concrete

Defined in Cryptol.Backend.Concrete

type SEval Concrete = Eval

type SFloat Concrete

Defined in Cryptol.Backend.Concrete

type SFloat Concrete = BF

type SInteger Concrete

Defined in Cryptol.Backend.Concrete

type SInteger Concrete = Integer

type SWord Concrete

Defined in Cryptol.Backend.Concrete

type SWord Concrete = BV

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

fpBinArith

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