cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright(c) 2020 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Safe HaskellNone
LanguageHaskell2010

Cryptol.Eval.What4

Description

 
Synopsis

Documentation

data What4 sym Source #

Constructors

What4 sym 
Instances
IsExprBuilder sym => Backend (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

Associated Types

type SBit (What4 sym) :: Type Source #

type SWord (What4 sym) :: Type Source #

type SInteger (What4 sym) :: Type Source #

type SFloat (What4 sym) :: Type Source #

type SEval (What4 sym) :: Type -> Type Source #

Methods

isReady :: What4 sym -> SEval (What4 sym) a -> Bool Source #

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

sDelayFill :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source #

sSpark :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source #

mergeEval :: What4 sym -> (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a) -> SBit (What4 sym) -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) () Source #

raiseError :: What4 sym -> EvalError -> SEval (What4 sym) a Source #

ppBit :: What4 sym -> SBit (What4 sym) -> Doc Source #

ppWord :: What4 sym -> PPOpts -> SWord (What4 sym) -> Doc Source #

ppInteger :: What4 sym -> PPOpts -> SInteger (What4 sym) -> Doc Source #

ppFloat :: What4 sym -> PPOpts -> SFloat (What4 sym) -> Doc Source #

bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool Source #

wordLen :: What4 sym -> SWord (What4 sym) -> Integer Source #

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

wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char Source #

integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer Source #

bitLit :: What4 sym -> Bool -> SBit (What4 sym) Source #

wordLit :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym)) Source #

integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym)) Source #

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

iteBit :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

iteWord :: What4 sym -> SBit (What4 sym) -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

iteInteger :: What4 sym -> SBit (What4 sym) -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

bitEq :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitOr :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitAnd :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitXor :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitComplement :: What4 sym -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

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

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

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

unpackWord :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)] Source #

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

joinWord :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

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

extractWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordOr :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordAnd :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordXor :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordComplement :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordPlus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMinus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMult :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordSignedDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordSignedMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordNegate :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordLg2 :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordEq :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordSignedLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordGreaterThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordToInt :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intPlus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intNegate :: What4 sym -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMinus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMult :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intDiv :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMod :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intEq :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intLessThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intGreaterThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intToZn :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znToInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znPlus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znNegate :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znMinus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znMult :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

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

fpEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpLessThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpGreaterThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpPlus :: FPArith2 (What4 sym) Source #

fpMinus :: FPArith2 (What4 sym) Source #

fpMult :: FPArith2 (What4 sym) Source #

fpDiv :: FPArith2 (What4 sym) Source #

fpNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

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

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

type SBit (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

type SBit (What4 sym) = Pred sym
type SWord (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

type SWord (What4 sym) = SWord sym
type SInteger (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

type SInteger (What4 sym) = SymInteger sym
type SFloat (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

type SFloat (What4 sym) = SFloat sym
type SEval (What4 sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

type SEval (What4 sym) = W4Eval sym

data W4Result sym a Source #

The symbolic value we computed.

Constructors

W4Error !EvalError

A malformed value

W4Result !(Pred sym) !a

safety predicate and result: the result only makes sense when the predicate holds.

data W4Defs sym a Source #

Keep track of a value and a context defining uninterpeted vairables.

Constructors

W4Defs 

Fields

data W4Eval sym a Source #

This is the monad used for symbolic evaluation. It adds to aspects to Eval' keeps track of the backend and collects definitional predicates, and W4Eval adds support for partially defined values

Instances
IsExprBuilder sym => Monad (W4Eval sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

Methods

(>>=) :: W4Eval sym a -> (a -> W4Eval sym b) -> W4Eval sym b #

(>>) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym b #

return :: a -> W4Eval sym a #

fail :: String -> W4Eval sym a #

IsExprBuilder sym => Functor (W4Eval sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

Methods

fmap :: (a -> b) -> W4Eval sym a -> W4Eval sym b #

(<$) :: a -> W4Eval sym b -> W4Eval sym a #

IsExprBuilder sym => Applicative (W4Eval sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

Methods

pure :: a -> W4Eval sym a #

(<*>) :: W4Eval sym (a -> b) -> W4Eval sym a -> W4Eval sym b #

liftA2 :: (a -> b -> c) -> W4Eval sym a -> W4Eval sym b -> W4Eval sym c #

(*>) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym b #

(<*) :: W4Eval sym a -> W4Eval sym b -> W4Eval sym a #

IsExprBuilder sym => MonadIO (W4Eval sym) Source # 
Instance details

Defined in Cryptol.Eval.What4.Value

Methods

liftIO :: IO a -> W4Eval sym a #

w4Eval :: W4Eval sym a -> sym -> Eval (W4Defs sym (W4Result sym a)) Source #

type Value sym = GenValue (What4 sym) Source #