cryptol-2.9.0: Cryptol: The Language of Cryptography

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

Cryptol.Eval.What4.Value

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

type Value sym = GenValue (What4 sym) Source #

newtype 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

Constructors

W4Eval 

Fields

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 #

newtype W4Conn sym a Source #

This layer has the symbolic back-end, and can keep track of definitional predicates used when working with uninterpreted constants defined via a property.

Constructors

W4Conn 

Fields

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

Defined in Cryptol.Eval.What4.Value

Methods

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

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

return :: a -> W4Conn sym a #

fail :: String -> W4Conn sym a #

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

Defined in Cryptol.Eval.What4.Value

Methods

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

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

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

Defined in Cryptol.Eval.What4.Value

Methods

pure :: a -> W4Conn sym a #

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

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

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

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

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

Defined in Cryptol.Eval.What4.Value

Methods

liftIO :: IO a -> W4Conn sym a #

data W4Defs sym a Source #

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

Constructors

W4Defs 

Fields

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.

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

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

doEval :: IsExprBuilder sym => Eval a -> W4Conn sym a Source #

A value with no context.

total :: IsExprBuilder sym => W4Conn sym a -> W4Eval sym a Source #

A total value.

getSym :: IsExprBuilder sym => W4Conn sym sym Source #

Access the symbolic back-end

addDef :: Pred sym -> W4Conn sym () Source #

Record a definition.

w4And :: IsExprBuilder sym => Pred sym -> Pred sym -> W4Conn sym (Pred sym) Source #

Compute conjunction.

w4Not :: IsExprBuilder sym => Pred sym -> W4Conn sym (Pred sym) Source #

Compute negation.

w4ITE :: IsExprBuilder sym => Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym) Source #

Compute if-then-else.

addDefEqn :: IsExprBuilder sym => Pred sym -> W4Eval sym () Source #

Add a definitional equation. This will always be asserted when we make queries to the solver.

addSafety :: IsExprBuilder sym => Pred sym -> W4Eval sym () Source #

Add s safety condition.

evalError :: IsExprBuilder sym => EvalError -> W4Eval sym a Source #

A fully undefined symbolic value

assertBVDivisor :: IsExprBuilder sym => sym -> SWord sym -> W4Eval sym () Source #

assertIntDivisor :: IsExprBuilder sym => sym -> SymInteger sym -> W4Eval sym () Source #

sModAdd :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModSub :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModMult :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym) Source #

sModNegate :: IsExprBuilder sym => sym -> Integer -> SymInteger sym -> IO (SymInteger sym) Source #

sLg2 :: IsExprBuilder sym => sym -> SWord sym -> SEval (What4 sym) (SWord sym) Source #

Try successive powers of 2 to find the first that dominates the input. We could perhaps reduce to using CLZ instead...

lazyIte :: (IsExpr p, Monad m) => (p BaseBoolType -> a -> a -> m a) -> p BaseBoolType -> m a -> m a -> m a Source #

indexFront_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexBack_int :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SInteger (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexFront_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexBack_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> SWord (What4 sym) -> SEval (What4 sym) (Value sym) Source #

indexFront_bits :: forall sym. IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym) Source #

indexBack_bits :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> TValue -> [SBit (What4 sym)] -> SEval (What4 sym) (Value sym) Source #

wordValueEqualsInteger :: forall sym. IsExprBuilder sym => sym -> WordValue (What4 sym) -> Integer -> W4Eval sym (Pred sym) Source #

Compare a symbolic word value with a concrete integer.

updateFrontSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym)) Source #

updateBackSym :: IsExprBuilder sym => sym -> Nat' -> TValue -> SeqMap (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (Value sym) -> SEval (What4 sym) (SeqMap (What4 sym)) Source #

updateFrontSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym)) Source #

updateBackSym_word :: IsExprBuilder sym => sym -> Nat' -> TValue -> WordValue (What4 sym) -> Either (SInteger (What4 sym)) (WordValue (What4 sym)) -> SEval (What4 sym) (GenValue (What4 sym)) -> SEval (What4 sym) (WordValue (What4 sym)) Source #

sshrV :: IsExprBuilder sym => sym -> Value sym Source #

w4bvShl :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvLshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvAshr :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvRol :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

w4bvRor :: IsExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym) Source #

fpBinArith :: IsExprBuilder sym => SFloatBinArith sym -> What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpCvtToInteger :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym) Source #

fpCvtToRational :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> SFloat sym -> SEval sym (SRational sym) Source #

fpCvtFromRational :: (IsExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym) Source #