| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
EVM.Symbolic
Synopsis
- litWord :: Word -> SymWord
- litAddr :: Addr -> SAddr
- maybeLitAddr :: SAddr -> Maybe Addr
- maybeLitBytes :: [SWord 8] -> Maybe ByteString
- forceLit :: SymWord -> Word
- forceLitBytes :: [SWord 8] -> ByteString
- forceBuffer :: Buffer -> ByteString
- sdiv :: SymWord -> SymWord -> SymWord
- smod :: SymWord -> SymWord -> SymWord
- addmod :: SymWord -> SymWord -> SymWord -> SymWord
- mulmod :: SymWord -> SymWord -> SymWord -> SymWord
- slt :: SymWord -> SymWord -> SymWord
- sgt :: SymWord -> SymWord -> SymWord
- swordAt :: Int -> [SWord 8] -> SymWord
- readByteOrZero' :: Int -> [SWord 8] -> SWord 8
- sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
- writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
- readMemoryWord' :: Word -> [SWord 8] -> SymWord
- readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
- setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
- setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
- readSWord' :: Word -> [SWord 8] -> SymWord
- select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
- readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord
- len :: Buffer -> Int
- readByteOrZero :: Int -> Buffer -> SWord 8
- sliceWithZero :: Int -> Int -> Buffer -> Buffer
- writeMemory :: Buffer -> Word -> Word -> Word -> Buffer -> Buffer
- readMemoryWord :: Word -> Buffer -> SymWord
- readMemoryWord32 :: Word -> Buffer -> SWord 32
- setMemoryWord :: Word -> SymWord -> Buffer -> Buffer
- setMemoryByte :: Word -> SWord 8 -> Buffer -> Buffer
- readSWord :: Word -> Buffer -> SymWord
- index :: Int -> Buffer -> SWord8
- symSHA256N :: SInteger -> SInteger -> SWord 256
- symkeccakN :: SInteger -> SInteger -> SWord 256
- toSInt :: [SWord 8] -> SInteger
- symkeccak' :: [SWord 8] -> SWord 256
- symSHA256 :: [SWord 8] -> [SWord 8]
- rawVal :: SymWord -> SWord 256
- whiffValue :: Whiff -> SWord 256
- simplifyCondition :: SBool -> Whiff -> SBool
Documentation
maybeLitBytes :: [SWord 8] -> Maybe ByteString Source #
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
forceLitBytes :: [SWord 8] -> ByteString Source #
forceBuffer :: Buffer -> ByteString Source #
Operations over symbolic memory (list of symbolic bytes)
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.
whiffValue :: Whiff -> SWord 256 Source #
Reconstruct the smt/sbv value from a whiff Should satisfy (rawVal x .== whiffValue x)