cryptol-3.2.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2020 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.Backend.Concrete

Description

 
Synopsis

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.

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

data Concrete Source #

Constructors

Concrete 

Instances

Instances details
Show Concrete Source # 
Instance details

Defined in Cryptol.Backend.Concrete

Backend Concrete Source # 
Instance details

Defined in Cryptol.Backend.Concrete

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

Defined in Cryptol.Backend.Concrete

type SFloat Concrete Source # 
Instance details

Defined in Cryptol.Backend.Concrete

type SInteger Concrete Source # 
Instance details

Defined in Cryptol.Backend.Concrete

type SWord Concrete Source # 
Instance details

Defined in Cryptol.Backend.Concrete