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

Cryptol.Backend.SBV

Description

 

Documentation

data SBV Source #

Constructors

SBV 

Fields

Instances

Instances details
Backend SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

Associated Types

type SBit SBV Source #

type SWord SBV Source #

type SInteger SBV Source #

type SFloat SBV Source #

type SEval SBV :: Type -> Type Source #

Methods

isReady :: SBV -> SEval SBV a -> SEval SBV (Maybe a) Source #

sDeclareHole :: SBV -> String -> SEval SBV (SEval SBV a, SEval SBV a -> SEval SBV ()) Source #

sDelayFill :: SBV -> SEval SBV a -> Maybe (SEval SBV a) -> String -> SEval SBV (SEval SBV a) Source #

sSpark :: SBV -> SEval SBV a -> SEval SBV (SEval SBV a) Source #

sPushFrame :: SBV -> Name -> Range -> SEval SBV a -> SEval SBV a Source #

sWithCallStack :: SBV -> CallStack -> SEval SBV a -> SEval SBV a Source #

sModifyCallStack :: SBV -> (CallStack -> CallStack) -> SEval SBV a -> SEval SBV a Source #

sGetCallStack :: SBV -> SEval SBV CallStack Source #

mergeEval :: SBV -> (SBit SBV -> a -> a -> SEval SBV a) -> SBit SBV -> SEval SBV a -> SEval SBV a -> SEval SBV a Source #

assertSideCondition :: SBV -> SBit SBV -> EvalError -> SEval SBV () Source #

raiseError :: SBV -> EvalError -> SEval SBV a Source #

bitAsLit :: SBV -> SBit SBV -> Maybe Bool Source #

wordLen' :: proxy SBV -> SWord SBV -> Integer Source #

wordAsLit :: SBV -> SWord SBV -> Maybe (Integer, Integer) Source #

wordAsChar :: SBV -> SWord SBV -> Maybe Char Source #

integerAsLit :: SBV -> SInteger SBV -> Maybe Integer Source #

fpAsLit :: SBV -> SFloat SBV -> Maybe BF Source #

bitLit :: SBV -> Bool -> SBit SBV Source #

wordLit :: SBV -> Integer -> Integer -> SEval SBV (SWord SBV) Source #

integerLit :: SBV -> Integer -> SEval SBV (SInteger SBV) Source #

fpLit :: SBV -> Integer -> Integer -> Rational -> SEval SBV (SFloat SBV) Source #

fpExactLit :: SBV -> BF -> SEval SBV (SFloat SBV) Source #

iteBit :: SBV -> SBit SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

iteWord :: SBV -> SBit SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

iteInteger :: SBV -> SBit SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

iteFloat :: SBV -> SBit SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

bitEq :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitOr :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitAnd :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitXor :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitComplement :: SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

wordBit :: SBV -> SWord SBV -> Integer -> SEval SBV (SBit SBV) Source #

wordUpdate :: SBV -> SWord SBV -> Integer -> SBit SBV -> SEval SBV (SWord SBV) Source #

packWord :: SBV -> [SBit SBV] -> SEval SBV (SWord SBV) Source #

unpackWord :: SBV -> SWord SBV -> SEval SBV [SBit SBV] Source #

wordFromInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV) Source #

joinWord :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

splitWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV, SWord SBV) Source #

extractWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordOr :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordAnd :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordXor :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordComplement :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordPlus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMinus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMult :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordSignedDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordSignedMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

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

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

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

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

wordRotateRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordNegate :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordLg2 :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordEq :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordSignedLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordGreaterThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordToInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV) Source #

wordToSignedInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV) Source #

intPlus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intNegate :: SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMinus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMult :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intDiv :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMod :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intEq :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intLessThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intGreaterThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intToZn :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znToInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znPlus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znMinus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znEq :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

znRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

fpEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpLessThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpGreaterThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpLogicalEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpNaN :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV) Source #

fpPosInf :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV) Source #

fpPlus :: FPArith2 SBV Source #

fpMinus :: FPArith2 SBV Source #

fpMult :: FPArith2 SBV Source #

fpDiv :: FPArith2 SBV Source #

fpNeg :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpAbs :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpSqrt :: SBV -> SWord SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpFMA :: SBV -> SWord SBV -> SFloat SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpIsZero :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNeg :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNaN :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsInf :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsSubnorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpToBits :: SBV -> SFloat SBV -> SEval SBV (SWord SBV) Source #

fpFromBits :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SFloat SBV) Source #

fpToInteger :: SBV -> String -> SWord SBV -> SFloat SBV -> SEval SBV (SInteger SBV) Source #

fpFromInteger :: SBV -> Integer -> Integer -> SWord SBV -> SInteger SBV -> SEval SBV (SFloat SBV) Source #

fpToRational :: SBV -> SFloat SBV -> SEval SBV (SRational SBV) Source #

fpFromRational :: SBV -> Integer -> Integer -> SWord SBV -> SRational SBV -> SEval SBV (SFloat SBV) Source #

type SBit SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

type SBit SBV = SVal
type SEval SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

type SEval SBV = SBVEval
type SFloat SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

type SFloat SBV = ()
type SInteger SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

type SInteger SBV = SVal
type SWord SBV Source # 
Instance details

Defined in Cryptol.Backend.SBV

type SWord SBV = SVal

newtype SBVEval a Source #

Constructors

SBVEval 

Fields

Instances

Instances details
MonadIO SBVEval Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

liftIO :: IO a -> SBVEval a #

Applicative SBVEval Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

pure :: a -> SBVEval a #

(<*>) :: SBVEval (a -> b) -> SBVEval a -> SBVEval b #

liftA2 :: (a -> b -> c) -> SBVEval a -> SBVEval b -> SBVEval c #

(*>) :: SBVEval a -> SBVEval b -> SBVEval b #

(<*) :: SBVEval a -> SBVEval b -> SBVEval a #

Functor SBVEval Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

fmap :: (a -> b) -> SBVEval a -> SBVEval b #

(<$) :: a -> SBVEval b -> SBVEval a #

Monad SBVEval Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

(>>=) :: SBVEval a -> (a -> SBVEval b) -> SBVEval b #

(>>) :: SBVEval a -> SBVEval b -> SBVEval b #

return :: a -> SBVEval a #

data SBVResult a Source #

Constructors

SBVError !EvalErrorEx 
SBVResult !SVal !a 

Instances

Instances details
Applicative SBVResult Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

pure :: a -> SBVResult a #

(<*>) :: SBVResult (a -> b) -> SBVResult a -> SBVResult b #

liftA2 :: (a -> b -> c) -> SBVResult a -> SBVResult b -> SBVResult c #

(*>) :: SBVResult a -> SBVResult b -> SBVResult b #

(<*) :: SBVResult a -> SBVResult b -> SBVResult a #

Functor SBVResult Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

fmap :: (a -> b) -> SBVResult a -> SBVResult b #

(<$) :: a -> SBVResult b -> SBVResult a #

Monad SBVResult Source # 
Instance details

Defined in Cryptol.Backend.SBV

Methods

(>>=) :: SBVResult a -> (a -> SBVResult b) -> SBVResult b #

(>>) :: SBVResult a -> SBVResult b -> SBVResult b #

return :: a -> SBVResult a #

literalSWord :: Int -> Integer -> SWord SBV Source #

freshSBool_ :: SBV -> IO (SBit SBV) Source #

freshBV_ :: SBV -> Int -> IO (SWord SBV) Source #

freshSInteger_ :: SBV -> IO (SInteger SBV) Source #

addDefEqn :: SBV -> SVal -> IO () Source #

ashr :: SVal -> SVal -> SVal Source #

lshr :: SVal -> SVal -> SVal Source #

shl :: SVal -> SVal -> SVal Source #

evalPanic :: String -> [String] -> a Source #

svFromInteger :: Integer -> SInteger SBV -> SWord SBV Source #

svToInteger :: SWord SBV -> SInteger SBV Source #