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
- 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
- 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
- unlit :: Expr EWord -> Maybe W256
- unlitByte :: Expr Byte -> Maybe Word8
- newtype ByteStringS = ByteStringS ByteString
- newtype Addr = Addr {}
- maybeLitWord :: Expr EWord -> Maybe W256
- 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
- padLeftStr :: Int -> String -> String
- padRight :: Int -> ByteString -> ByteString
- padRight' :: Int -> String -> String
- padLeft' :: Int -> Vector (Expr Byte) -> Vector (Expr Byte)
- word256 :: ByteString -> Word256
- word :: ByteString -> W256
- byteAt :: (Bits a, Bits b, Integral a, Num b) => a -> Int -> b
- 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 -> Word32
- concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
- regexMatches :: Text -> Text -> Bool
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 | |
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 | |
PBool :: Bool -> Prop |
newtype ByteStringS Source #
Instances
ToJSON ByteStringS Source # | |
Defined in EVM.Types toJSON :: ByteStringS -> Value # toEncoding :: ByteStringS -> Encoding # toJSONList :: [ByteStringS] -> Value # toEncodingList :: [ByteStringS] -> Encoding # | |
Show ByteStringS Source # | |
Defined in EVM.Types showsPrec :: Int -> ByteStringS -> ShowS # show :: ByteStringS -> String # showList :: [ByteStringS] -> ShowS # | |
Eq ByteStringS Source # | |
Defined in EVM.Types (==) :: ByteStringS -> ByteStringS -> Bool # (/=) :: ByteStringS -> ByteStringS -> Bool # |
Instances
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 #
abiKeccak :: ByteString -> Word32 Source #
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #