cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2020 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Backend.What4

Description

Synopsis

- data What4 sym = What4 {
  - w4 :: sym
  - w4defs :: MVar (Pred sym)
  - w4funs :: MVar (What4FunCache sym)
  - w4uninterpWarns :: MVar (Set Text)
  }
- type What4FunCache sym = Map Text (SomeSymFn sym)
- data SomeSymFn sym = forall args ret. SomeSymFn (SymFn sym args ret)
- newtype W4Eval sym a = W4Eval {
  - evalPartial :: W4Conn sym (W4Result sym a)
  }
- newtype W4Conn sym a = W4Conn {
  - evalConn :: sym -> Eval a
  }
- data W4Result sym a
  - = W4Error !EvalErrorEx
  - | W4Result !(Pred sym) !a
- w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
- w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a
- doEval :: IsSymExprBuilder sym => Eval a -> W4Conn sym a
- total :: IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
- getSym :: W4Conn sym sym
- w4And :: IsSymExprBuilder sym => Pred sym -> Pred sym -> W4Conn sym (Pred sym)
- w4Not :: IsSymExprBuilder sym => Pred sym -> W4Conn sym (Pred sym)
- w4ITE :: IsSymExprBuilder sym => Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
- addDefEqn :: IsSymExprBuilder sym => What4 sym -> Pred sym -> W4Eval sym ()
- addSafety :: IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
- evalError :: IsSymExprBuilder sym => EvalError -> W4Eval sym a
- assertBVDivisor :: IsSymExprBuilder sym => What4 sym -> SWord sym -> W4Eval sym ()
- assertIntDivisor :: IsSymExprBuilder sym => What4 sym -> SymInteger sym -> W4Eval sym ()
- sModAdd :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
- sModSub :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
- sModMult :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
- sModNegate :: IsSymExprBuilder sym => sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
- sLg2 :: IsSymExprBuilder sym => sym -> SWord sym -> SEval (What4 sym) (SWord sym)
- evalPanic :: String -> [String] -> a
- lazyIte :: (IsExpr p, Monad m) => (p BaseBoolType -> a -> a -> m a) -> p BaseBoolType -> m a -> m a -> m a
- w4bvShl :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
- w4bvLshr :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
- w4bvAshr :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
- w4bvRol :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
- w4bvRor :: IsSymExprBuilder sym => sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
- fpRoundingMode :: IsSymExprBuilder sym => What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
- fpBinArith :: IsSymExprBuilder sym => SFloatBinArith sym -> What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
- fpCvtToInteger :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
- fpCvtToRational :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> SFloat sym -> SEval sym (SRational sym)
- fpCvtFromRational :: (IsSymExprBuilder sy, sym ~ What4 sy) => sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym)
- sModRecip :: IsSymExprBuilder sym => What4 sym -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)

# Documentation

data What4 sym Source #

Constructors

What4 |

Fields

- w4 :: sym
- w4defs :: MVar (Pred sym)
- w4funs :: MVar (What4FunCache sym)
- w4uninterpWarns :: MVar (Set Text)

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

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

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

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

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

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

wordToSignedInt :: 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 SEval (What4 sym) Source # |
Instance details Defined in Cryptol.Backend.What4 type SEval (What4 sym) = W4Eval sym
type SFloat (What4 sym) Source # |
Instance details Defined in Cryptol.Backend.What4 type SFloat (What4 sym) = SFloat sym
type SInteger (What4 sym) Source # |
Instance details Defined in Cryptol.Backend.What4 type SInteger (What4 sym) = SymInteger sym
type SWord (What4 sym) Source # |
Instance details Defined in Cryptol.Backend.What4 type SWord (What4 sym) = SWord sym

type What4FunCache sym = Map Text (SomeSymFn sym) Source #

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

- evalPartial :: W4Conn sym (W4Result sym a)

#### Instances

Instances details

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

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

- evalConn :: sym -> Eval a

#### Instances

Instances details

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

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.

#### Instances

Instances details

Functor (W4Result sym) Source # |
Instance details Defined in Cryptol.Backend.What4 Methods fmap :: (a -> b) -> W4Result sym a -> W4Result sym b Source # (<$) :: a -> W4Result sym b -> W4Result sym a Source #

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 #

assertIntDivisor :: IsSymExprBuilder sym => What4 sym -> SymInteger 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 #

sModNegate :: IsSymExprBuilder sym => sym -> Integer -> 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...

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

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 #

fpRoundingMode :: IsSymExprBuilder sym => What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode 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 #

sModRecip :: IsSymExprBuilder sym => What4 sym -> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym) Source #