cryptol-2.11.0: Cryptol: The Language of Cryptography
Copyright(c) 2020 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Safe HaskellNone
LanguageHaskell2010

Cryptol.Backend.What4

Description

 
Synopsis

Documentation

data What4 sym Source #

Constructors

What4 

Fields

Instances

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

Defined in Cryptol.Backend.What4

Associated Types

type SBit (What4 sym) Source #

type SWord (What4 sym) Source #

type SInteger (What4 sym) Source #

type SFloat (What4 sym) 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 -> Maybe (SEval (What4 sym) a) -> String -> SEval (What4 sym) (SEval (What4 sym) a) Source #

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

sPushFrame :: What4 sym -> Name -> Range -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sWithCallStack :: What4 sym -> CallStack -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sModifyCallStack :: What4 sym -> (CallStack -> CallStack) -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sGetCallStack :: What4 sym -> SEval (What4 sym) CallStack 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 #

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 #

fpAsLit :: What4 sym -> SFloat (What4 sym) -> Maybe BF 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 #

fpExactLit :: What4 sym -> BF -> 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 #

iteFloat :: What4 sym -> SBit (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (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 #

znRecip :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (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 #

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

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

fpPosInf :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SFloat (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 #

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

fpSqrt :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpFMA :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

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

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

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

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

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

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

fpToBits :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

fpFromBits :: What4 sym -> Integer -> Integer -> SWord (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 #

fpToRational :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym)) Source #

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

type SBit (What4 sym) Source # 
Instance details

Defined in Cryptol.Backend.What4

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

Defined in Cryptol.Backend.What4

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

Defined in Cryptol.Backend.What4

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

Defined in Cryptol.Backend.What4

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

Defined in Cryptol.Backend.What4

type SEval (What4 sym) = W4Eval sym

data SomeSymFn sym Source #

Constructors

forall args ret. SomeSymFn (SymFn sym args ret) 

newtype W4Eval sym a Source #

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

Constructors

W4Eval 

Fields

Instances

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

Defined in Cryptol.Backend.What4

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 #

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

Defined in Cryptol.Backend.What4

Methods

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

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

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

Defined in Cryptol.Backend.What4

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 #

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

Defined in Cryptol.Backend.What4

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

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

Defined in Cryptol.Backend.What4

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 #

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

Defined in Cryptol.Backend.What4

Methods

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

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

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

Defined in Cryptol.Backend.What4

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 #

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

Defined in Cryptol.Backend.What4

Methods

liftIO :: IO a -> W4Conn sym a #

data W4Result sym a Source #

The symbolic value we computed.

Constructors

W4Error !EvalErrorEx

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 (W4Result sym a) Source #

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

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

A value with no context.

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

A total value.

getSym :: W4Conn sym sym Source #

Access the symbolic back-end

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

Record a definition. addDef :: W4.Pred sym -> W4Conn sym () addDef p = W4Conn _ -> pure W4Defs { w4Defs = p, w4Result = () }

Compute conjunction.

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

Compute negation.

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

Compute if-then-else.

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

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

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

Add s safety condition.

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

A fully undefined symbolic value

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

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

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

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

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

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

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

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

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

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

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

fpCvtToInteger :: (IsSymExprBuilder 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 :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym) Source #