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
Instance details Defined in Cryptol.Backend.Concrete type SBit Concrete = Bool
type SWord Concrete
Instance details Defined in Cryptol.Backend.Concrete type SWord Concrete = BV
type SInteger Concrete
Instance details Defined in Cryptol.Backend.Concrete type SInteger Concrete = Integer
type SFloat Concrete
Instance details Defined in Cryptol.Backend.Concrete type SFloat Concrete = BF
type SEval Concrete
Instance details Defined in Cryptol.Backend.Concrete type SEval Concrete = Eval

Methods

isReady :: Concrete -> SEval Concrete a -> SEval Concrete (Maybe a) 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' :: proxy 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 #

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

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

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

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

wordRotateRight :: 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 #

wordToSignedInt :: 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 SEval Concrete Source #

Instance details

Defined in Cryptol.Backend.Concrete

type SEval Concrete = Eval

type SFloat Concrete Source #

Instance details

Defined in Cryptol.Backend.Concrete

type SFloat Concrete = BF

type SInteger Concrete Source #

Instance details

Defined in Cryptol.Backend.Concrete

type SInteger Concrete = Integer

type SWord Concrete Source #

Instance details

Defined in Cryptol.Backend.Concrete

type SWord Concrete = BV

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 #