Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data Word512 = Word512 !Word256 !Word256
- data Int512 = Int512 !Int256 !Word256
- newtype W256 = W256 Word256
- data EType
- data Error
- data GVar (a :: EType) where
- data Expr (a :: EType) where
- Lit :: !W256 -> Expr EWord
- Var :: Text -> Expr EWord
- GVar :: GVar a -> Expr a
- LitByte :: !Word8 -> Expr Byte
- IndexWord :: Expr EWord -> Expr EWord -> Expr Byte
- EqByte :: Expr Byte -> Expr Byte -> Expr EWord
- JoinBytes :: Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte -> Expr EWord
- Revert :: [Prop] -> Expr Buf -> Expr End
- Failure :: [Prop] -> Error -> Expr End
- Return :: [Prop] -> Expr Buf -> Expr Storage -> Expr End
- ITE :: Expr EWord -> Expr End -> Expr End -> Expr End
- Add :: Expr EWord -> Expr EWord -> Expr EWord
- Sub :: Expr EWord -> Expr EWord -> Expr EWord
- Mul :: Expr EWord -> Expr EWord -> Expr EWord
- Div :: Expr EWord -> Expr EWord -> Expr EWord
- SDiv :: Expr EWord -> Expr EWord -> Expr EWord
- Mod :: Expr EWord -> Expr EWord -> Expr EWord
- SMod :: Expr EWord -> Expr EWord -> Expr EWord
- AddMod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
- MulMod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
- Exp :: Expr EWord -> Expr EWord -> Expr EWord
- SEx :: Expr EWord -> Expr EWord -> Expr EWord
- Min :: Expr EWord -> Expr EWord -> Expr EWord
- Max :: Expr EWord -> Expr EWord -> Expr EWord
- LT :: Expr EWord -> Expr EWord -> Expr EWord
- GT :: Expr EWord -> Expr EWord -> Expr EWord
- LEq :: Expr EWord -> Expr EWord -> Expr EWord
- GEq :: Expr EWord -> Expr EWord -> Expr EWord
- SLT :: Expr EWord -> Expr EWord -> Expr EWord
- SGT :: Expr EWord -> Expr EWord -> Expr EWord
- Eq :: Expr EWord -> Expr EWord -> Expr EWord
- IsZero :: Expr EWord -> Expr EWord
- And :: Expr EWord -> Expr EWord -> Expr EWord
- Or :: Expr EWord -> Expr EWord -> Expr EWord
- Xor :: Expr EWord -> Expr EWord -> Expr EWord
- Not :: Expr EWord -> Expr EWord
- SHL :: Expr EWord -> Expr EWord -> Expr EWord
- SHR :: Expr EWord -> Expr EWord -> Expr EWord
- SAR :: Expr EWord -> Expr EWord -> Expr EWord
- Keccak :: Expr Buf -> Expr EWord
- SHA256 :: Expr Buf -> Expr EWord
- Origin :: Expr EWord
- BlockHash :: Expr EWord -> Expr EWord
- Coinbase :: Expr EWord
- Timestamp :: Expr EWord
- BlockNumber :: Expr EWord
- PrevRandao :: Expr EWord
- GasLimit :: Expr EWord
- ChainId :: Expr EWord
- BaseFee :: Expr EWord
- CallValue :: Int -> Expr EWord
- Caller :: Int -> Expr EWord
- Address :: Int -> Expr EWord
- Balance :: Int -> Int -> Expr EWord -> Expr EWord
- SelfBalance :: Int -> Int -> Expr EWord
- Gas :: Int -> Int -> Expr EWord
- CodeSize :: Expr EWord -> Expr EWord
- ExtCodeHash :: Expr EWord -> Expr EWord
- LogEntry :: Expr EWord -> Expr Buf -> [Expr EWord] -> Expr Log
- Create :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> [Expr Log] -> Expr Storage -> Expr EWord
- Create2 :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> [Expr Log] -> Expr Storage -> Expr EWord
- Call :: Expr EWord -> Maybe (Expr EWord) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
- CallCode :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
- DelegeateCall :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr Log] -> Expr Storage -> Expr EWord
- EmptyStore :: Expr Storage
- ConcreteStore :: Map W256 (Map W256 W256) -> Expr Storage
- AbstractStore :: Expr Storage
- SLoad :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord
- SStore :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
- ConcreteBuf :: ByteString -> Expr Buf
- AbstractBuf :: Text -> Expr Buf
- ReadWord :: Expr EWord -> Expr Buf -> Expr EWord
- ReadByte :: Expr EWord -> Expr Buf -> Expr Byte
- WriteWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
- WriteByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
- CopySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
- BufLength :: Expr Buf -> Expr EWord
- data Prop where
- PEq :: forall a. Typeable a => Expr a -> Expr a -> Prop
- PLT :: Expr EWord -> Expr EWord -> Prop
- PGT :: Expr EWord -> Expr EWord -> Prop
- PGEq :: Expr EWord -> Expr EWord -> Prop
- PLEq :: Expr EWord -> Expr EWord -> Prop
- PNeg :: Prop -> Prop
- PAnd :: Prop -> Prop -> Prop
- POr :: Prop -> Prop -> Prop
- PImpl :: Prop -> Prop -> Prop
- PBool :: Bool -> Prop
- (.&&) :: Prop -> Prop -> Prop
- (.||) :: Prop -> Prop -> Prop
- (.<) :: Expr EWord -> Expr EWord -> Prop
- (.<=) :: Expr EWord -> Expr EWord -> Prop
- (.>) :: Expr EWord -> Expr EWord -> Prop
- (.>=) :: Expr EWord -> Expr EWord -> Prop
- (.==) :: Typeable a => Expr a -> Expr a -> Prop
- (./=) :: Typeable a => Expr a -> Expr a -> Prop
- pand :: [Prop] -> Prop
- por :: [Prop] -> Prop
- newtype FunctionSelector = FunctionSelector {}
- unlit :: Expr EWord -> Maybe W256
- unlitByte :: Expr Byte -> Maybe Word8
- newtype ByteStringS = ByteStringS ByteString
- newtype Addr = Addr {}
- maybeLitWord :: Expr EWord -> Maybe W256
- newtype W64 = W64 Word64
- toChecksumAddress :: String -> String
- strip0x :: ByteString -> ByteString
- strip0x' :: String -> String
- hexByteString :: String -> ByteString -> ByteString
- hexText :: Text -> ByteString
- readN :: Integral a => String -> a
- readNull :: Read a => a -> String -> a
- wordField :: Object -> Key -> Parser W256
- word64Field :: Object -> Key -> Parser Word64
- addrField :: Object -> Key -> Parser Addr
- addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)
- dataField :: Object -> Key -> Parser ByteString
- toWord512 :: W256 -> Word512
- fromWord512 :: Word512 -> W256
- num :: (Integral a, Num b) => a -> b
- padLeft :: Int -> ByteString -> ByteString
- padRight :: Int -> ByteString -> ByteString
- padRight' :: Int -> String -> String
- padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte)
- word256 :: ByteString -> Word256
- word :: ByteString -> W256
- fromBE :: Integral a => ByteString -> a
- asBE :: Integral a => a -> ByteString
- word256Bytes :: W256 -> ByteString
- word160Bytes :: Addr -> ByteString
- newtype Nibble = Nibble Word8
- hi :: Word8 -> Nibble
- lo :: Word8 -> Nibble
- toByte :: Nibble -> Nibble -> Word8
- unpackNibbles :: ByteString -> [Nibble]
- packNibbles :: [Nibble] -> ByteString
- toWord64 :: W256 -> Maybe Word64
- toInt :: W256 -> Maybe Int
- keccakBytes :: ByteString -> ByteString
- word32 :: [Word8] -> Word32
- keccak :: Expr Buf -> Expr EWord
- keccak' :: ByteString -> W256
- abiKeccak :: ByteString -> FunctionSelector
- concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
- regexMatches :: Text -> Text -> Bool
- data VMTrace = VMTrace {
- tracePc :: Int
- traceOp :: Int
- traceStack :: [W256]
- traceMemSize :: Word64
- traceDepth :: Int
- traceGas :: Word64
- traceError :: Maybe String
- bsToHex :: ByteString -> String
- bssToBs :: ByteStringS -> ByteString
Documentation
Instances
Instances
Instances
Expr implements an abstract respresentation of an EVM program
This type can give insight into the provenance of a term which is useful, both for the aesthetic purpose of printing terms in a richer way, but also to allow optimizations on the AST instead of letting the SMT solver do all the heavy lifting.
Memory, calldata, and returndata are all represented as a Buf. Semantically speaking a Buf is a byte array with of size 2^256.
Bufs have two base constructors: - AbstractBuf: all elements are fully abstract values - ConcreteBuf bs: all elements past (length bs) are zero
Bufs can be read from with: - ReadByte idx buf: read the byte at idx from buf - ReadWord idx buf: read the byte at idx from buf
Bufs can be written to with: - WriteByte idx val buf: write val to idx in buf - WriteWord idx val buf: write val to idx in buf - CopySlice srcOffset dstOffset size src dst: overwrite dstOffset -> dstOffset + size in dst with srcOffset -> srcOffset + size from src
Note that the shared usage of Buf
does allow for the construction of some
badly typed Expr instances (e.g. an MSTORE on top of the contents of calldata
instead of some previous instance of memory), we accept this for the
sake of simplifying pattern matches against a Buf expression.
Storage expressions are similar, but instead of writing regions of bytes, we write a word to a particular key in a given addresses storage. Note that as with a Buf, writes can be sequenced on top of concrete, empty and fully abstract starting states.
One important principle is that of local context: e.g. each term representing a write to a Buf Storage Logs will always contain a copy of the state that is being added to, this ensures that all context relevant to a given operation is contained within the term that represents that operation.
When dealing with Expr instances we assume that concrete expressions have
been reduced to their smallest possible representation (i.e. a Lit
,
ConcreteBuf
, or ConcreteStore
). Failure to adhere to this invariant will
result in your concrete term being treated as symbolic, and may produce
unexpected errors. In the future we may wish to consider encoding the
concreteness of a given term directly in the type of that term, since such
type level shenanigans tends to complicate implementation, we skip this for
now.
Invalid | |
IllegalOverflow | |
StackLimitExceeded | |
InvalidMemoryAccess | |
BadJumpDestination | |
StackUnderrun | |
SelfDestruct | |
TmpErr String |
data Expr (a :: EType) where Source #
PEq :: forall a. Typeable a => Expr a -> Expr a -> Prop | |
PLT :: Expr EWord -> Expr EWord -> Prop | |
PGT :: Expr EWord -> Expr EWord -> Prop | |
PGEq :: Expr EWord -> Expr EWord -> Prop | |
PLEq :: Expr EWord -> Expr EWord -> Prop | |
PNeg :: Prop -> Prop | |
PAnd :: Prop -> Prop -> Prop | |
POr :: Prop -> Prop -> Prop | |
PImpl :: Prop -> Prop -> Prop | |
PBool :: Bool -> Prop |
newtype FunctionSelector Source #
Instances
newtype ByteStringS Source #
Instances
Instances
Instances
FromJSON W64 Source # | |
ToJSON W64 Source # | |
Bits W64 Source # | |
Defined in EVM.Types | |
FiniteBits W64 Source # | |
Defined in EVM.Types | |
Bounded W64 Source # | |
Enum W64 Source # | |
Generic W64 Source # | |
Num W64 Source # | |
Read W64 Source # | |
Integral W64 Source # | |
Real W64 Source # | |
Defined in EVM.Types toRational :: W64 -> Rational # | |
Show W64 Source # | |
Eq W64 Source # | |
Ord W64 Source # | |
type Rep W64 Source # | |
toChecksumAddress :: String -> String Source #
strip0x :: ByteString -> ByteString Source #
hexByteString :: String -> ByteString -> ByteString Source #
hexText :: Text -> ByteString Source #
fromWord512 :: Word512 -> W256 Source #
padLeft :: Int -> ByteString -> ByteString Source #
padRight :: Int -> ByteString -> ByteString Source #
padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte) Source #
Right padding / truncating truncpad :: Int -> [SWord 8] -> [SWord 8] truncpad n xs = if m > n then take n xs else mappend xs (replicate (n - m) 0) where m = length xs
word256 :: ByteString -> Word256 Source #
word :: ByteString -> W256 Source #
fromBE :: Integral a => ByteString -> a Source #
asBE :: Integral a => a -> ByteString Source #
word256Bytes :: W256 -> ByteString Source #
word160Bytes :: Addr -> ByteString Source #
Instances
unpackNibbles :: ByteString -> [Nibble] Source #
packNibbles :: [Nibble] -> ByteString Source #
keccakBytes :: ByteString -> ByteString Source #
keccak' :: ByteString -> W256 Source #
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #
VMTrace | |
|
Instances
bsToHex :: ByteString -> String Source #
bssToBs :: ByteStringS -> ByteString Source #