cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Backend.SBV

Description

# Documentation

data SBV Source #

Constructors

SBV |

Fields

- sbvStateVar :: MVar State
- sbvDefRelations :: MVar SVal

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

- sbvEval :: Eval (SBVResult a)

#### Instances

Instances details

MonadIO SBVEval Source # |
Instance details Defined in Cryptol.Backend.SBV Methods liftIO :: IO a -> SBVEval a Source #
Applicative SBVEval Source # |
Instance details Defined in Cryptol.Backend.SBV Methods pure :: a -> SBVEval a Source # (<*>) :: SBVEval (a -> b) -> SBVEval a -> SBVEval b Source # liftA2 :: (a -> b -> c) -> SBVEval a -> SBVEval b -> SBVEval c Source # (*>) :: SBVEval a -> SBVEval b -> SBVEval b Source # (<*) :: SBVEval a -> SBVEval b -> SBVEval a Source #
Functor SBVEval Source # |
Instance details Defined in Cryptol.Backend.SBV Methods fmap :: (a -> b) -> SBVEval a -> SBVEval b Source # (<$) :: a -> SBVEval b -> SBVEval a Source #
Monad SBVEval Source # |
Instance details Defined in Cryptol.Backend.SBV Methods (>>=) :: SBVEval a -> (a -> SBVEval b) -> SBVEval b Source # (>>) :: SBVEval a -> SBVEval b -> SBVEval b Source # return :: a -> SBVEval a Source #

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 Source # (<*>) :: SBVResult (a -> b) -> SBVResult a -> SBVResult b Source # liftA2 :: (a -> b -> c) -> SBVResult a -> SBVResult b -> SBVResult c Source # (*>) :: SBVResult a -> SBVResult b -> SBVResult b Source # (<*) :: SBVResult a -> SBVResult b -> SBVResult a Source #
Functor SBVResult Source # |
Instance details Defined in Cryptol.Backend.SBV Methods fmap :: (a -> b) -> SBVResult a -> SBVResult b Source # (<$) :: a -> SBVResult b -> SBVResult a Source #
Monad SBVResult Source # |
Instance details Defined in Cryptol.Backend.SBV Methods (>>=) :: SBVResult a -> (a -> SBVResult b) -> SBVResult b Source # (>>) :: SBVResult a -> SBVResult b -> SBVResult b Source # return :: a -> SBVResult a Source #

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 #