hevm-0.47.0: Ethereum virtual machine evaluator
Safe HaskellNone
LanguageHaskell2010

EVM.Symbolic

Synopsis

Documentation

forceLit :: SymWord -> Word Source #

Note: the (force*) functions are crude and in general, the continuation passing style forceConcrete alternatives should be prefered for better error handling when used during EVM execution

slt :: SymWord -> SymWord -> SymWord Source #

Signed less than

sgt :: SymWord -> SymWord -> SymWord Source #

Signed greater than

Operations over symbolic memory (list of symbolic bytes)

sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8] Source #

writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8] Source #

setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8] Source #

select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a Source #

readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord Source #

Read 32 bytes from index from a bounded list of bytes.

Uninterpreted functions

symkeccak' :: [SWord 8] -> SWord 256 Source #

Although we'd like to define this directly as an uninterpreted function, we cannot because [a] is not a symbolic type. We must convert the list into a suitable symbolic type first. The only important property of this conversion is that it is injective. We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.

symSHA256 :: [SWord 8] -> [SWord 8] Source #

whiffValue :: Whiff -> SWord 256 Source #

Reconstruct the smt/sbv value from a whiff Should satisfy (rawVal x .== whiffValue x)

simplifyCondition :: SBool -> Whiff -> SBool Source #

Special cases that have proven useful in practice