{-# LANGUAGE DataKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module EVM.Types where

import GHC.Stack (HasCallStack, prettyCallStack, callStack)
import Control.Arrow ((>>>))
import Control.Monad.ST (ST)
import Control.Monad.State.Strict (StateT, mzero)
import Crypto.Hash (hash, Keccak_256, Digest)
import Data.Aeson
import Data.Aeson qualified as JSON
import Data.Aeson.Types qualified as JSON
import Data.Bifunctor (first)
import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.), toIntegralSized)
import Data.Binary qualified as Binary
import Data.ByteArray qualified as BA
import Data.Char
import Data.List (foldl')
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.ByteString.Base16 qualified as BS16
import Data.ByteString.Builder (byteStringHex, toLazyByteString)
import Data.ByteString.Char8 qualified as Char8
import Data.ByteString.Lazy (toStrict)
import Data.Data
import Data.Int (Int64)
import Data.Word (Word8, Word32, Word64)
import Data.DoubleWord
import Data.DoubleWord.TH
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import Data.Sequence (Seq)
import Data.Sequence qualified as Seq
import Data.Serialize qualified as Cereal
import Data.Text qualified as T
import Data.Text.Encoding qualified as T
import Data.Tree (Forest)
import Data.Tree.Zipper qualified as Zipper
import Data.Vector qualified as V
import Data.Vector.Storable qualified as SV
import Data.Vector.Unboxed.Mutable (STVector)
import Numeric (readHex, showHex)
import Options.Generic
import Optics.TH
import EVM.FeeSchedule (FeeSchedule (..))

import Text.Regex.TDFA qualified as Regex
import Text.Read qualified
import Witch


-- Template Haskell --------------------------------------------------------------------------


-- We need a 512-bit word for doing ADDMOD and MULMOD with full precision.
mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256
  [''Typeable, ''Data, ''Generic]



-- Conversions -------------------------------------------------------------------------------------


-- We ignore hlint to suppress the warnings about `fromIntegral` and friends here
#ifndef __HLINT__

instance From Addr Integer where from :: Addr -> Integer
from = Addr -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Addr W256 where from :: Addr -> W256
from = Addr -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Int256 Integer where from :: Int256 -> Integer
from = Int256 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Nibble Int where from :: Nibble -> Int
from = Nibble -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From W256 Integer where from :: W256 -> Integer
from = W256 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word8 W256 where from :: Word8 -> W256
from = Word8 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word8 Word256 where from :: Word8 -> Word256
from = Word8 -> Word256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word32 W256 where from :: Word32 -> W256
from = Word32 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word32 Word256 where from :: Word32 -> Word256
from = Word32 -> Word256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word32 ByteString where from :: Word32 -> ByteString
from = ByteString -> ByteString
toStrict (ByteString -> ByteString)
-> (Word32 -> ByteString) -> Word32 -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode
instance From Word64 W256 where from :: Word64 -> W256
from = Word64 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From W64 W256 where from :: W64 -> W256
from = W64 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word256 Integer where from :: Word256 -> Integer
from = Word256 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance From Word256 W256 where from :: Word256 -> W256
from = Word256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance TryFrom Int W256 where tryFrom :: Int -> Either (TryFromException Int W256) W256
tryFrom = (Int -> Maybe W256)
-> Int -> Either (TryFromException Int W256) W256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Int -> Maybe W256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Int Word256 where tryFrom :: Int -> Either (TryFromException Int Word256) Word256
tryFrom = (Int -> Maybe Word256)
-> Int -> Either (TryFromException Int Word256) Word256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Int -> Maybe Word256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Int256 W256 where tryFrom :: Int256 -> Either (TryFromException Int256 W256) W256
tryFrom = (Int256 -> Maybe W256)
-> Int256 -> Either (TryFromException Int256 W256) W256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Int256 -> Maybe W256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Integer W256 where tryFrom :: Integer -> Either (TryFromException Integer W256) W256
tryFrom = (Integer -> Maybe W256)
-> Integer -> Either (TryFromException Integer W256) W256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Integer -> Maybe W256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Integer Addr where tryFrom :: Integer -> Either (TryFromException Integer Addr) Addr
tryFrom = (Integer -> Maybe Addr)
-> Integer -> Either (TryFromException Integer Addr) Addr
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Integer -> Maybe Addr
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
-- TODO: hevm relies on this behavior
instance TryFrom W256 Addr where tryFrom :: W256 -> Either (TryFromException W256 Addr) Addr
tryFrom = Addr -> Either (TryFromException W256 Addr) Addr
forall a b. b -> Either a b
Right (Addr -> Either (TryFromException W256 Addr) Addr)
-> (W256 -> Addr)
-> W256
-> Either (TryFromException W256 Addr) Addr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Addr
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance TryFrom W256 FunctionSelector where tryFrom :: W256
-> Either (TryFromException W256 FunctionSelector) FunctionSelector
tryFrom = (W256 -> Maybe FunctionSelector)
-> W256
-> Either (TryFromException W256 FunctionSelector) FunctionSelector
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe FunctionSelector
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom W256 Int where tryFrom :: W256 -> Either (TryFromException W256 Int) Int
tryFrom = (W256 -> Maybe Int)
-> W256 -> Either (TryFromException W256 Int) Int
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe Int
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom W256 Int64 where tryFrom :: W256 -> Either (TryFromException W256 Int64) Int64
tryFrom = (W256 -> Maybe Int64)
-> W256 -> Either (TryFromException W256 Int64) Int64
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe Int64
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom W256 Int256 where tryFrom :: W256 -> Either (TryFromException W256 Int256) Int256
tryFrom = (W256 -> Maybe Int256)
-> W256 -> Either (TryFromException W256 Int256) Int256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe Int256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom W256 Word8 where tryFrom :: W256 -> Either (TryFromException W256 Word8) Word8
tryFrom = (W256 -> Maybe Word8)
-> W256 -> Either (TryFromException W256 Word8) Word8
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe Word8
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom W256 Word32 where tryFrom :: W256 -> Either (TryFromException W256 Word32) Word32
tryFrom = (W256 -> Maybe Word32)
-> W256 -> Either (TryFromException W256 Word32) Word32
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom W256 -> Maybe Word32
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
-- TODO: hevm relies on this behavior
instance TryFrom W256 Word64 where tryFrom :: W256 -> Either (TryFromException W256 Word64) Word64
tryFrom = Word64 -> Either (TryFromException W256 Word64) Word64
forall a b. b -> Either a b
Right (Word64 -> Either (TryFromException W256 Word64) Word64)
-> (W256 -> Word64)
-> W256
-> Either (TryFromException W256 Word64) Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance TryFrom W256 W64 where tryFrom :: W256 -> Either (TryFromException W256 W64) W64
tryFrom = W64 -> Either (TryFromException W256 W64) W64
forall a b. b -> Either a b
Right (W64 -> Either (TryFromException W256 W64) W64)
-> (W256 -> W64) -> W256 -> Either (TryFromException W256 W64) W64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> W64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance TryFrom Word160 Word8 where tryFrom :: Word160 -> Either (TryFromException Word160 Word8) Word8
tryFrom = (Word160 -> Maybe Word8)
-> Word160 -> Either (TryFromException Word160 Word8) Word8
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word160 -> Maybe Word8
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Word256 Int where tryFrom :: Word256 -> Either (TryFromException Word256 Int) Int
tryFrom = (Word256 -> Maybe Int)
-> Word256 -> Either (TryFromException Word256 Int) Int
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word256 -> Maybe Int
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Word256 Int256 where tryFrom :: Word256 -> Either (TryFromException Word256 Int256) Int256
tryFrom = (Word256 -> Maybe Int256)
-> Word256 -> Either (TryFromException Word256 Int256) Int256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word256 -> Maybe Int256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Word256 Word8 where tryFrom :: Word256 -> Either (TryFromException Word256 Word8) Word8
tryFrom = (Word256 -> Maybe Word8)
-> Word256 -> Either (TryFromException Word256 Word8) Word8
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word256 -> Maybe Word8
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Word256 Word32 where tryFrom :: Word256 -> Either (TryFromException Word256 Word32) Word32
tryFrom = (Word256 -> Maybe Word32)
-> Word256 -> Either (TryFromException Word256 Word32) Word32
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word256 -> Maybe Word32
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized
instance TryFrom Word512 W256 where tryFrom :: Word512 -> Either (TryFromException Word512 W256) W256
tryFrom = (Word512 -> Maybe W256)
-> Word512 -> Either (TryFromException Word512 W256) W256
forall source target.
(source -> Maybe target)
-> source -> Either (TryFromException source target) target
maybeTryFrom Word512 -> Maybe W256
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized

truncateToAddr :: W256 -> Addr
truncateToAddr :: W256 -> Addr
truncateToAddr = W256 -> Addr
forall a b. (Integral a, Num b) => a -> b
fromIntegral

#endif


-- Symbolic IR -------------------------------------------------------------------------------------


-- phantom type tags for AST construction
data EType
  = Buf
  | Storage
  | Log
  | EWord
  | EAddr
  | EContract
  | Byte
  | End
  deriving (Typeable)

-- Variables referring to a global environment
data GVar (a :: EType) where
  BufVar :: Int -> GVar Buf
  StoreVar :: Int -> GVar Storage

deriving instance Show (GVar a)
deriving instance Eq (GVar a)
deriving instance Ord (GVar a)

{- |
  Expr implements an abstract representation 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.
-}
data Expr (a :: EType) where

  -- identifiers

  -- | Literal words
  Lit            :: {-# UNPACK #-} !W256 -> Expr EWord
  -- | Variables
  Var            :: Text -> Expr EWord
  -- | variables introduced during the CSE pass
  GVar           :: GVar a -> Expr a

  -- bytes

  LitByte        :: {-# UNPACK #-} !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

  -- control flow

  Partial        :: [Prop] -> Traces -> PartialExec -> Expr End
  Failure        :: [Prop] -> Traces -> EvmError -> Expr End
  Success        :: [Prop] -> Traces -> Expr Buf -> Map (Expr EAddr) (Expr EContract) -> Expr End
  ITE            :: Expr EWord -> Expr End -> Expr End -> Expr End

  -- integers

  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

  -- booleans

  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

  -- bits

  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

  -- Hashes

  Keccak         :: Expr Buf -> Expr EWord
  SHA256         :: Expr Buf -> Expr EWord

  -- block context

  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

  -- tx context

  TxValue        :: Expr EWord

  -- frame context

  Balance        :: Expr EAddr -> Expr EWord

  Gas            :: Int                -- frame idx
                 -> Expr EWord

  -- code

  CodeSize       :: Expr EAddr         -- address
                 -> Expr EWord         -- size

  CodeHash       :: Expr EAddr         -- address
                 -> Expr EWord         -- size

  -- logs

  LogEntry       :: Expr EWord         -- address
                 -> Expr Buf           -- data
                 -> [Expr EWord]       -- topics
                 -> Expr Log


  -- Contract

  -- A restricted view of a contract that does not include extraneous metadata
  -- from the full constructor defined in the VM state
  C ::
    { Expr 'EContract -> ContractCode
code    :: ContractCode
    , Expr 'EContract -> Expr 'Storage
storage :: Expr Storage
    , Expr 'EContract -> Expr 'EWord
balance :: Expr EWord
    , Expr 'EContract -> Maybe W64
nonce   :: Maybe W64
    } -> Expr EContract

  -- addresses

  -- Symbolic addresses are identified with an int. It is important that
  -- semantic equality is the same as syntactic equality here. Additionally all
  -- SAddr's in a given expression should be constrained to differ from any LitAddr's
  SymAddr        :: Text -> Expr EAddr
  LitAddr        :: Addr -> Expr EAddr
  WAddr          :: Expr EAddr -> Expr EWord

  -- storage

  ConcreteStore  :: (Map W256 W256) -> Expr Storage
  AbstractStore  :: Expr EAddr -- which contract is this store for?
                 -> Maybe W256 -- which logical store does this refer to? (e.g. solidity mappings / arrays)
                 -> Expr Storage

  SLoad          :: Expr EWord         -- key
                 -> Expr Storage       -- storage
                 -> Expr EWord         -- result

  SStore         :: Expr EWord         -- key
                 -> Expr EWord         -- value
                 -> Expr Storage       -- old storage
                 -> Expr Storage       -- new storae

  -- buffers

  ConcreteBuf    :: ByteString -> Expr Buf
  AbstractBuf    :: Text -> Expr Buf

  ReadWord       :: Expr EWord         -- index
                 -> Expr Buf           -- src
                 -> Expr EWord

  ReadByte       :: Expr EWord         -- index
                 -> Expr Buf           -- src
                 -> Expr Byte

  WriteWord      :: Expr EWord         -- dst offset
                 -> Expr EWord         -- value
                 -> Expr Buf           -- prev
                 -> Expr Buf

  WriteByte      :: Expr EWord         -- dst offset
                 -> Expr Byte          -- value
                 -> Expr Buf           -- prev
                 -> Expr Buf

  CopySlice      :: Expr EWord         -- src offset
                 -> Expr EWord         -- dst offset
                 -> Expr EWord         -- size
                 -> Expr Buf           -- src
                 -> Expr Buf           -- dst
                 -> Expr Buf

  BufLength      :: Expr Buf -> Expr EWord

deriving instance Show (Expr a)
deriving instance Eq (Expr a)
deriving instance Ord (Expr a)


-- Existential Wrapper -----------------------------------------------------------------------------


data SomeExpr = forall a . Typeable a => SomeExpr (Expr a)

deriving instance Show SomeExpr

instance Eq SomeExpr where
  SomeExpr (Expr a
a :: Expr b) == :: SomeExpr -> SomeExpr -> Bool
== SomeExpr (Expr a
c :: Expr d) =
    case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @b @d of
      Just a :~: a
Refl -> Expr a
a Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr a
c
      Maybe (a :~: a)
Nothing -> Bool
False

instance Ord SomeExpr where
  compare :: SomeExpr -> SomeExpr -> Ordering
compare (SomeExpr (Expr a
a :: Expr b)) (SomeExpr (Expr a
c :: Expr d)) =
    case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @b @d of
      Just a :~: a
Refl -> Expr a -> Expr a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Expr a
a Expr a
Expr a
c
      Maybe (a :~: a)
Nothing -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Expr a -> Int
forall (a :: EType). Typeable a => Expr a -> Int
toNum Expr a
a) (Expr a -> Int
forall (a :: EType). Typeable a => Expr a -> Int
toNum Expr a
c)

toNum :: (Typeable a) => Expr a -> Int
toNum :: forall (a :: EType). Typeable a => Expr a -> Int
toNum (Expr a
_ :: Expr a) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Buf of
    Just a :~: 'Buf
Refl -> Int
1
    Maybe (a :~: 'Buf)
Nothing -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Storage of
      Just a :~: 'Storage
Refl -> Int
2
      Maybe (a :~: 'Storage)
Nothing -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Log of
        Just a :~: 'Log
Refl -> Int
3
        Maybe (a :~: 'Log)
Nothing -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @EWord of
          Just a :~: 'EWord
Refl -> Int
4
          Maybe (a :~: 'EWord)
Nothing -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @Byte of
            Just a :~: 'Byte
Refl -> Int
5
            Maybe (a :~: 'Byte)
Nothing -> Int
6


-- Propostions -------------------------------------------------------------------------------------


-- The language of assertable expressions.
-- This is useful when generating SMT queries based on Expr instances, since
-- the translation of Eq and other boolean operators from Expr to SMT is an
-- (ite (eq a b) 1 0). We can use the boolean operators here to remove some
-- unescessary `ite` statements from our SMT encoding.
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
deriving instance (Show Prop)

infixr 3 .&&
(.&&) :: Prop -> Prop -> Prop
Prop
x .&& :: Prop -> Prop -> Prop
.&& Prop
y = Prop -> Prop -> Prop
PAnd Prop
x Prop
y

infixr 2 .||
(.||) :: Prop -> Prop -> Prop
Prop
x .|| :: Prop -> Prop -> Prop
.|| Prop
y = Prop -> Prop -> Prop
POr Prop
x Prop
y

infix 4 .<, .<=, .>, .>=
(.<) :: Expr EWord -> Expr EWord -> Prop
Expr 'EWord
x .< :: Expr 'EWord -> Expr 'EWord -> Prop
.< Expr 'EWord
y = Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
x Expr 'EWord
y
(.<=) :: Expr EWord -> Expr EWord -> Prop
Expr 'EWord
x .<= :: Expr 'EWord -> Expr 'EWord -> Prop
.<= Expr 'EWord
y = Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
x Expr 'EWord
y
(.>) :: Expr EWord -> Expr EWord -> Prop
Expr 'EWord
x .> :: Expr 'EWord -> Expr 'EWord -> Prop
.> Expr 'EWord
y = Expr 'EWord -> Expr 'EWord -> Prop
PGT Expr 'EWord
x Expr 'EWord
y
(.>=) :: Expr EWord -> Expr EWord -> Prop
Expr 'EWord
x .>= :: Expr 'EWord -> Expr 'EWord -> Prop
.>= Expr 'EWord
y = Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
x Expr 'EWord
y

infix 4 .==, ./=
(.==) :: (Typeable a) => Expr a -> Expr a -> Prop
Expr a
x .== :: forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
.== Expr a
y = Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
x Expr a
y
(./=) :: (Typeable a) => Expr a -> Expr a -> Prop
Expr a
x ./= :: forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr a
y = Prop -> Prop
PNeg (Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
x Expr a
y)

pand :: [Prop] -> Prop
pand :: [Prop] -> Prop
pand = (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop -> Prop -> Prop
PAnd (Bool -> Prop
PBool Bool
True)

por :: [Prop] -> Prop
por :: [Prop] -> Prop
por = (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Prop -> Prop -> Prop
POr (Bool -> Prop
PBool Bool
False)

instance Eq Prop where
  PBool Bool
a == :: Prop -> Prop -> Bool
== PBool Bool
b = Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b
  PEq (Expr a
a :: Expr x) (Expr a
b :: Expr x) == PEq (Expr a
c :: Expr y) (Expr a
d :: Expr y)
    = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @y of
       Just a :~: a
Refl -> Expr a
a Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr a
c Bool -> Bool -> Bool
&& Expr a
b Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr a
d
       Maybe (a :~: a)
Nothing -> Bool
False
  PLT Expr 'EWord
a Expr 'EWord
b == PLT Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c Bool -> Bool -> Bool
&& Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
d
  PGT Expr 'EWord
a Expr 'EWord
b == PGT Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c Bool -> Bool -> Bool
&& Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
d
  PGEq Expr 'EWord
a Expr 'EWord
b == PGEq Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c Bool -> Bool -> Bool
&& Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
d
  PLEq Expr 'EWord
a Expr 'EWord
b == PLEq Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c Bool -> Bool -> Bool
&& Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
d
  PNeg Prop
a == PNeg Prop
b = Prop
a Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
b
  PAnd Prop
a Prop
b == PAnd Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
c Bool -> Bool -> Bool
&& Prop
b Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
d
  POr Prop
a Prop
b == POr Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
c Bool -> Bool -> Bool
&& Prop
b Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
d
  PImpl Prop
a Prop
b == PImpl Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
c Bool -> Bool -> Bool
&& Prop
b Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
d
  Prop
_ == Prop
_ = Bool
False

instance Ord Prop where
  PBool Bool
a <= :: Prop -> Prop -> Bool
<= PBool Bool
b = Bool
a Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
<= Bool
b
  PEq (Expr a
a :: Expr x) (Expr a
b :: Expr x) <= PEq (Expr a
c :: Expr y) (Expr a
d :: Expr y)
    = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EType) (b :: EType).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @y of
       Just a :~: a
Refl -> Expr a
a Expr a -> Expr a -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr a
Expr a
c Bool -> Bool -> Bool
|| Expr a
b Expr a -> Expr a -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr a
Expr a
d
       Maybe (a :~: a)
Nothing -> Expr a -> Int
forall (a :: EType). Typeable a => Expr a -> Int
toNum Expr a
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr a -> Int
forall (a :: EType). Typeable a => Expr a -> Int
toNum Expr a
c
  PLT Expr 'EWord
a Expr 'EWord
b <= PLT Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
c Bool -> Bool -> Bool
|| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
d
  PGT Expr 'EWord
a Expr 'EWord
b <= PGT Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
c Bool -> Bool -> Bool
|| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
d
  PGEq Expr 'EWord
a Expr 'EWord
b <= PGEq Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
c Bool -> Bool -> Bool
|| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
d
  PLEq Expr 'EWord
a Expr 'EWord
b <= PLEq Expr 'EWord
c Expr 'EWord
d = Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
c Bool -> Bool -> Bool
|| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr 'EWord
d
  PNeg Prop
a <= PNeg Prop
b = Prop
a Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
b
  PAnd Prop
a Prop
b <= PAnd Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
c Bool -> Bool -> Bool
|| Prop
b Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
d
  POr Prop
a Prop
b <= POr Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
c Bool -> Bool -> Bool
|| Prop
b Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
d
  PImpl Prop
a Prop
b <= PImpl Prop
c Prop
d = Prop
a Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
c Bool -> Bool -> Bool
|| Prop
b Prop -> Prop -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop
d
  Prop
a <= Prop
b = Prop -> Int
asNum Prop
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Prop -> Int
asNum Prop
b
    where
      asNum :: Prop -> Int
      asNum :: Prop -> Int
asNum (PBool {}) = Int
0
      asNum (PEq   {}) = Int
1
      asNum (PLT   {}) = Int
2
      asNum (PGT   {}) = Int
3
      asNum (PGEq  {}) = Int
4
      asNum (PLEq  {}) = Int
5
      asNum (PNeg  {}) = Int
6
      asNum (PAnd  {}) = Int
7
      asNum (POr   {}) = Int
8
      asNum (PImpl {}) = Int
9



isPBool :: Prop -> Bool
isPBool :: Prop -> Bool
isPBool (PBool Bool
_) = Bool
True
isPBool Prop
_ = Bool
False


-- Errors ------------------------------------------------------------------------------------------


-- | Core EVM Error Types
data EvmError
  = BalanceTooLow (Expr EWord) (Expr EWord)
  | UnrecognizedOpcode Word8
  | SelfDestruction
  | StackUnderrun
  | BadJumpDestination
  | Revert (Expr Buf)
  | OutOfGas Word64 Word64
  | StackLimitExceeded
  | IllegalOverflow
  | StateChangeWhileStatic
  | InvalidMemoryAccess
  | CallDepthLimitReached
  | MaxCodeSizeExceeded W256 W256
  | MaxInitCodeSizeExceeded W256 (Expr EWord)
  | InvalidFormat
  | PrecompileFailure
  | ReturnDataOutOfBounds
  | NonceOverflow
  | BadCheatCode FunctionSelector
  | NonexistentFork Int
  deriving (Int -> EvmError -> ShowS
[EvmError] -> ShowS
EvmError -> String
(Int -> EvmError -> ShowS)
-> (EvmError -> String) -> ([EvmError] -> ShowS) -> Show EvmError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvmError -> ShowS
showsPrec :: Int -> EvmError -> ShowS
$cshow :: EvmError -> String
show :: EvmError -> String
$cshowList :: [EvmError] -> ShowS
showList :: [EvmError] -> ShowS
Show, EvmError -> EvmError -> Bool
(EvmError -> EvmError -> Bool)
-> (EvmError -> EvmError -> Bool) -> Eq EvmError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvmError -> EvmError -> Bool
== :: EvmError -> EvmError -> Bool
$c/= :: EvmError -> EvmError -> Bool
/= :: EvmError -> EvmError -> Bool
Eq, Eq EvmError
Eq EvmError
-> (EvmError -> EvmError -> Ordering)
-> (EvmError -> EvmError -> Bool)
-> (EvmError -> EvmError -> Bool)
-> (EvmError -> EvmError -> Bool)
-> (EvmError -> EvmError -> Bool)
-> (EvmError -> EvmError -> EvmError)
-> (EvmError -> EvmError -> EvmError)
-> Ord EvmError
EvmError -> EvmError -> Bool
EvmError -> EvmError -> Ordering
EvmError -> EvmError -> EvmError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: EvmError -> EvmError -> Ordering
compare :: EvmError -> EvmError -> Ordering
$c< :: EvmError -> EvmError -> Bool
< :: EvmError -> EvmError -> Bool
$c<= :: EvmError -> EvmError -> Bool
<= :: EvmError -> EvmError -> Bool
$c> :: EvmError -> EvmError -> Bool
> :: EvmError -> EvmError -> Bool
$c>= :: EvmError -> EvmError -> Bool
>= :: EvmError -> EvmError -> Bool
$cmax :: EvmError -> EvmError -> EvmError
max :: EvmError -> EvmError -> EvmError
$cmin :: EvmError -> EvmError -> EvmError
min :: EvmError -> EvmError -> EvmError
Ord)

-- | Sometimes we can only partially execute a given program
data PartialExec
  = UnexpectedSymbolicArg { PartialExec -> Int
pc :: Int, PartialExec -> String
msg  :: String, PartialExec -> [SomeExpr]
args  :: [SomeExpr] }
  | MaxIterationsReached  { pc :: Int, PartialExec -> Expr 'EAddr
addr :: Expr EAddr }
  | JumpIntoSymbolicCode  { pc :: Int, PartialExec -> Int
jumpDst :: Int }
  deriving (Int -> PartialExec -> ShowS
[PartialExec] -> ShowS
PartialExec -> String
(Int -> PartialExec -> ShowS)
-> (PartialExec -> String)
-> ([PartialExec] -> ShowS)
-> Show PartialExec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PartialExec -> ShowS
showsPrec :: Int -> PartialExec -> ShowS
$cshow :: PartialExec -> String
show :: PartialExec -> String
$cshowList :: [PartialExec] -> ShowS
showList :: [PartialExec] -> ShowS
Show, PartialExec -> PartialExec -> Bool
(PartialExec -> PartialExec -> Bool)
-> (PartialExec -> PartialExec -> Bool) -> Eq PartialExec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PartialExec -> PartialExec -> Bool
== :: PartialExec -> PartialExec -> Bool
$c/= :: PartialExec -> PartialExec -> Bool
/= :: PartialExec -> PartialExec -> Bool
Eq, Eq PartialExec
Eq PartialExec
-> (PartialExec -> PartialExec -> Ordering)
-> (PartialExec -> PartialExec -> Bool)
-> (PartialExec -> PartialExec -> Bool)
-> (PartialExec -> PartialExec -> Bool)
-> (PartialExec -> PartialExec -> Bool)
-> (PartialExec -> PartialExec -> PartialExec)
-> (PartialExec -> PartialExec -> PartialExec)
-> Ord PartialExec
PartialExec -> PartialExec -> Bool
PartialExec -> PartialExec -> Ordering
PartialExec -> PartialExec -> PartialExec
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PartialExec -> PartialExec -> Ordering
compare :: PartialExec -> PartialExec -> Ordering
$c< :: PartialExec -> PartialExec -> Bool
< :: PartialExec -> PartialExec -> Bool
$c<= :: PartialExec -> PartialExec -> Bool
<= :: PartialExec -> PartialExec -> Bool
$c> :: PartialExec -> PartialExec -> Bool
> :: PartialExec -> PartialExec -> Bool
$c>= :: PartialExec -> PartialExec -> Bool
>= :: PartialExec -> PartialExec -> Bool
$cmax :: PartialExec -> PartialExec -> PartialExec
max :: PartialExec -> PartialExec -> PartialExec
$cmin :: PartialExec -> PartialExec -> PartialExec
min :: PartialExec -> PartialExec -> PartialExec
Ord)

-- | Effect types used by the vm implementation for side effects & control flow
data Effect t s where
  Query :: Query t s -> Effect t s
  Choose :: Choose s -> Effect Symbolic s
deriving instance Show (Effect t s)

-- | Queries halt execution until resolved through RPC calls or SMT queries
data Query t s where
  PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
  PleaseDoFFI         :: [String] -> (ByteString -> EVM t s ()) -> Query t s

-- | Execution could proceed down one of two branches
data Choose s where
  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM Symbolic s ()) -> Choose s

-- | The possible return values of a SMT query
data BranchCondition = Case Bool | Unknown
  deriving Int -> BranchCondition -> ShowS
[BranchCondition] -> ShowS
BranchCondition -> String
(Int -> BranchCondition -> ShowS)
-> (BranchCondition -> String)
-> ([BranchCondition] -> ShowS)
-> Show BranchCondition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BranchCondition -> ShowS
showsPrec :: Int -> BranchCondition -> ShowS
$cshow :: BranchCondition -> String
show :: BranchCondition -> String
$cshowList :: [BranchCondition] -> ShowS
showList :: [BranchCondition] -> ShowS
Show

instance Show (Query t s) where
  showsPrec :: Int -> Query t s -> ShowS
showsPrec Int
_ = \case
    PleaseFetchContract Addr
addr BaseState
base Contract -> EVM t s ()
_ ->
      ((String
"<EVM.Query: fetch contract " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Addr -> String
forall a. Show a => a -> String
show Addr
addr String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseState -> String
forall a. Show a => a -> String
show BaseState
base String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">") ++)
    PleaseFetchSlot Addr
addr W256
slot W256 -> EVM t s ()
_ ->
      ((String
"<EVM.Query: fetch slot "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ W256 -> String
forall a. Show a => a -> String
show W256
slot String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Addr -> String
forall a. Show a => a -> String
show Addr
addr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">") ++)
    PleaseAskSMT Expr 'EWord
condition [Prop]
constraints BranchCondition -> EVM 'Symbolic s ()
_ ->
      ((String
"<EVM.Query: ask SMT about "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'EWord -> String
forall a. Show a => a -> String
show Expr 'EWord
condition String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in context "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prop] -> String
forall a. Show a => a -> String
show [Prop]
constraints String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">") ++)
    PleaseDoFFI [String]
cmd ByteString -> EVM t s ()
_ ->
      ((String
"<EVM.Query: do ffi: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([String] -> String
forall a. Show a => a -> String
show [String]
cmd)) ++)

instance Show (Choose s) where
  showsPrec :: Int -> Choose s -> ShowS
showsPrec Int
_ = \case
    PleaseChoosePath Expr 'EWord
_ Bool -> EVM 'Symbolic s ()
_ ->
      ((String
"<EVM.Choice: waiting for user to select path (0,1)") ++)

-- | The possible result states of a VM
data VMResult (t :: VMType) s where
  Unfinished :: PartialExec -> VMResult Symbolic s -- ^ Execution could not continue further
  VMFailure :: EvmError -> VMResult t s            -- ^ An operation failed
  VMSuccess :: (Expr Buf) -> VMResult t s          -- ^ Reached STOP, RETURN, or end-of-code
  HandleEffect :: (Effect t s) -> VMResult t s     -- ^ An effect must be handled for execution to continue

deriving instance Show (VMResult t s)


-- VM State ----------------------------------------------------------------------------------------

data VMType = Symbolic | Concrete

type family Gas (t :: VMType) = r | r -> t where
  Gas Symbolic = ()
  Gas Concrete = Word64

-- | The state of a stepwise EVM execution
data VM (t :: VMType) s = VM
  { forall (t :: VMType) s. VM t s -> Maybe (VMResult t s)
result         :: Maybe (VMResult t s)
  , forall (t :: VMType) s. VM t s -> FrameState t s
state          :: FrameState t s
  , forall (t :: VMType) s. VM t s -> [Frame t s]
frames         :: [Frame t s]
  , forall (t :: VMType) s. VM t s -> Env
env            :: Env
  , forall (t :: VMType) s. VM t s -> Block
block          :: Block
  , forall (t :: VMType) s. VM t s -> TxState
tx             :: TxState
  , forall (t :: VMType) s. VM t s -> [Expr 'Log]
logs           :: [Expr Log]
  , forall (t :: VMType) s. VM t s -> TreePos Empty Trace
traces         :: Zipper.TreePos Zipper.Empty Trace
  , forall (t :: VMType) s. VM t s -> Cache
cache          :: Cache
  , forall (t :: VMType) s. VM t s -> Gas t
burned         :: !(Gas t)
  , forall (t :: VMType) s.
VM t s -> Map CodeLocation (Int, [Expr 'EWord])
iterations     :: Map CodeLocation (Int, [Expr EWord])
  -- ^ how many times we've visited a loc, and what the contents of the stack were when we were there last
  , forall (t :: VMType) s. VM t s -> [Prop]
constraints    :: [Prop]
  , forall (t :: VMType) s. VM t s -> RuntimeConfig
config         :: RuntimeConfig
  , forall (t :: VMType) s. VM t s -> Seq ForkState
forks          :: Seq ForkState
  , forall (t :: VMType) s. VM t s -> Int
currentFork    :: Int
  }
  deriving ((forall x. VM t s -> Rep (VM t s) x)
-> (forall x. Rep (VM t s) x -> VM t s) -> Generic (VM t s)
forall x. Rep (VM t s) x -> VM t s
forall x. VM t s -> Rep (VM t s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: VMType) s x. Rep (VM t s) x -> VM t s
forall (t :: VMType) s x. VM t s -> Rep (VM t s) x
$cfrom :: forall (t :: VMType) s x. VM t s -> Rep (VM t s) x
from :: forall x. VM t s -> Rep (VM t s) x
$cto :: forall (t :: VMType) s x. Rep (VM t s) x -> VM t s
to :: forall x. Rep (VM t s) x -> VM t s
Generic)

data ForkState = ForkState
  { ForkState -> Env
env :: Env
  , ForkState -> Block
block :: Block
  , ForkState -> Cache
cache :: Cache
  , ForkState -> String
urlOrAlias :: String
  }
  deriving (Int -> ForkState -> ShowS
[ForkState] -> ShowS
ForkState -> String
(Int -> ForkState -> ShowS)
-> (ForkState -> String)
-> ([ForkState] -> ShowS)
-> Show ForkState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForkState -> ShowS
showsPrec :: Int -> ForkState -> ShowS
$cshow :: ForkState -> String
show :: ForkState -> String
$cshowList :: [ForkState] -> ShowS
showList :: [ForkState] -> ShowS
Show, (forall x. ForkState -> Rep ForkState x)
-> (forall x. Rep ForkState x -> ForkState) -> Generic ForkState
forall x. Rep ForkState x -> ForkState
forall x. ForkState -> Rep ForkState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ForkState -> Rep ForkState x
from :: forall x. ForkState -> Rep ForkState x
$cto :: forall x. Rep ForkState x -> ForkState
to :: forall x. Rep ForkState x -> ForkState
Generic)

deriving instance Show (VM Symbolic s)
deriving instance Show (VM Concrete s)

-- | Alias for the type of e.g. @exec1@.
type EVM (t :: VMType) s a = StateT (VM t s) (ST s) a

-- | The VM base state (i.e. should new contracts be created with abstract balance / storage?)
data BaseState
  = EmptyBase
  | AbstractBase
  deriving (Int -> BaseState -> ShowS
[BaseState] -> ShowS
BaseState -> String
(Int -> BaseState -> ShowS)
-> (BaseState -> String)
-> ([BaseState] -> ShowS)
-> Show BaseState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BaseState -> ShowS
showsPrec :: Int -> BaseState -> ShowS
$cshow :: BaseState -> String
show :: BaseState -> String
$cshowList :: [BaseState] -> ShowS
showList :: [BaseState] -> ShowS
Show)

-- | Configuration options that need to be consulted at runtime
data RuntimeConfig = RuntimeConfig
  { RuntimeConfig -> Bool
allowFFI :: Bool
  , RuntimeConfig -> Maybe (Expr 'EAddr)
overrideCaller :: Maybe (Expr EAddr)
  , RuntimeConfig -> BaseState
baseState :: BaseState
  }
  deriving (Int -> RuntimeConfig -> ShowS
[RuntimeConfig] -> ShowS
RuntimeConfig -> String
(Int -> RuntimeConfig -> ShowS)
-> (RuntimeConfig -> String)
-> ([RuntimeConfig] -> ShowS)
-> Show RuntimeConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuntimeConfig -> ShowS
showsPrec :: Int -> RuntimeConfig -> ShowS
$cshow :: RuntimeConfig -> String
show :: RuntimeConfig -> String
$cshowList :: [RuntimeConfig] -> ShowS
showList :: [RuntimeConfig] -> ShowS
Show)

-- | An entry in the VM's "call/create stack"
data Frame (t :: VMType) s = Frame
  { forall (t :: VMType) s. Frame t s -> FrameContext
context :: FrameContext
  , forall (t :: VMType) s. Frame t s -> FrameState t s
state   :: FrameState t s
  }

deriving instance Show (Frame Symbolic s)
deriving instance Show (Frame Concrete s)

-- | Call/create info
data FrameContext
  = CreationContext
    { FrameContext -> Expr 'EAddr
address         :: Expr EAddr
    , FrameContext -> Expr 'EWord
codehash        :: Expr EWord
    , FrameContext -> Map (Expr 'EAddr) Contract
createreversion :: Map (Expr EAddr) Contract
    , FrameContext -> SubState
substate        :: SubState
    }
  | CallContext
    { FrameContext -> Expr 'EAddr
target        :: Expr EAddr
    , FrameContext -> Expr 'EAddr
context       :: Expr EAddr
    , FrameContext -> Expr 'EWord
offset        :: Expr EWord
    , FrameContext -> Expr 'EWord
size          :: Expr EWord
    , codehash      :: Expr EWord
    , FrameContext -> Maybe W256
abi           :: Maybe W256
    , FrameContext -> Expr 'Buf
calldata      :: Expr Buf
    , FrameContext -> Map (Expr 'EAddr) Contract
callreversion :: Map (Expr EAddr) Contract
    , FrameContext -> SubState
subState      :: SubState
    }
  deriving (FrameContext -> FrameContext -> Bool
(FrameContext -> FrameContext -> Bool)
-> (FrameContext -> FrameContext -> Bool) -> Eq FrameContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FrameContext -> FrameContext -> Bool
== :: FrameContext -> FrameContext -> Bool
$c/= :: FrameContext -> FrameContext -> Bool
/= :: FrameContext -> FrameContext -> Bool
Eq, Eq FrameContext
Eq FrameContext
-> (FrameContext -> FrameContext -> Ordering)
-> (FrameContext -> FrameContext -> Bool)
-> (FrameContext -> FrameContext -> Bool)
-> (FrameContext -> FrameContext -> Bool)
-> (FrameContext -> FrameContext -> Bool)
-> (FrameContext -> FrameContext -> FrameContext)
-> (FrameContext -> FrameContext -> FrameContext)
-> Ord FrameContext
FrameContext -> FrameContext -> Bool
FrameContext -> FrameContext -> Ordering
FrameContext -> FrameContext -> FrameContext
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FrameContext -> FrameContext -> Ordering
compare :: FrameContext -> FrameContext -> Ordering
$c< :: FrameContext -> FrameContext -> Bool
< :: FrameContext -> FrameContext -> Bool
$c<= :: FrameContext -> FrameContext -> Bool
<= :: FrameContext -> FrameContext -> Bool
$c> :: FrameContext -> FrameContext -> Bool
> :: FrameContext -> FrameContext -> Bool
$c>= :: FrameContext -> FrameContext -> Bool
>= :: FrameContext -> FrameContext -> Bool
$cmax :: FrameContext -> FrameContext -> FrameContext
max :: FrameContext -> FrameContext -> FrameContext
$cmin :: FrameContext -> FrameContext -> FrameContext
min :: FrameContext -> FrameContext -> FrameContext
Ord, Int -> FrameContext -> ShowS
[FrameContext] -> ShowS
FrameContext -> String
(Int -> FrameContext -> ShowS)
-> (FrameContext -> String)
-> ([FrameContext] -> ShowS)
-> Show FrameContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FrameContext -> ShowS
showsPrec :: Int -> FrameContext -> ShowS
$cshow :: FrameContext -> String
show :: FrameContext -> String
$cshowList :: [FrameContext] -> ShowS
showList :: [FrameContext] -> ShowS
Show, (forall x. FrameContext -> Rep FrameContext x)
-> (forall x. Rep FrameContext x -> FrameContext)
-> Generic FrameContext
forall x. Rep FrameContext x -> FrameContext
forall x. FrameContext -> Rep FrameContext x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FrameContext -> Rep FrameContext x
from :: forall x. FrameContext -> Rep FrameContext x
$cto :: forall x. Rep FrameContext x -> FrameContext
to :: forall x. Rep FrameContext x -> FrameContext
Generic)

-- | The "accrued substate" across a transaction
data SubState = SubState
  { SubState -> [Expr 'EAddr]
selfdestructs       :: [Expr EAddr]
  , SubState -> [Expr 'EAddr]
touchedAccounts     :: [Expr EAddr]
  , SubState -> Set (Expr 'EAddr)
accessedAddresses   :: Set (Expr EAddr)
  , SubState -> Set (Expr 'EAddr, W256)
accessedStorageKeys :: Set (Expr EAddr, W256)
  , SubState -> [(Expr 'EAddr, Word64)]
refunds             :: [(Expr EAddr, Word64)]
  -- in principle we should include logs here, but do not for now
  }
  deriving (SubState -> SubState -> Bool
(SubState -> SubState -> Bool)
-> (SubState -> SubState -> Bool) -> Eq SubState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SubState -> SubState -> Bool
== :: SubState -> SubState -> Bool
$c/= :: SubState -> SubState -> Bool
/= :: SubState -> SubState -> Bool
Eq, Eq SubState
Eq SubState
-> (SubState -> SubState -> Ordering)
-> (SubState -> SubState -> Bool)
-> (SubState -> SubState -> Bool)
-> (SubState -> SubState -> Bool)
-> (SubState -> SubState -> Bool)
-> (SubState -> SubState -> SubState)
-> (SubState -> SubState -> SubState)
-> Ord SubState
SubState -> SubState -> Bool
SubState -> SubState -> Ordering
SubState -> SubState -> SubState
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SubState -> SubState -> Ordering
compare :: SubState -> SubState -> Ordering
$c< :: SubState -> SubState -> Bool
< :: SubState -> SubState -> Bool
$c<= :: SubState -> SubState -> Bool
<= :: SubState -> SubState -> Bool
$c> :: SubState -> SubState -> Bool
> :: SubState -> SubState -> Bool
$c>= :: SubState -> SubState -> Bool
>= :: SubState -> SubState -> Bool
$cmax :: SubState -> SubState -> SubState
max :: SubState -> SubState -> SubState
$cmin :: SubState -> SubState -> SubState
min :: SubState -> SubState -> SubState
Ord, Int -> SubState -> ShowS
[SubState] -> ShowS
SubState -> String
(Int -> SubState -> ShowS)
-> (SubState -> String) -> ([SubState] -> ShowS) -> Show SubState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SubState -> ShowS
showsPrec :: Int -> SubState -> ShowS
$cshow :: SubState -> String
show :: SubState -> String
$cshowList :: [SubState] -> ShowS
showList :: [SubState] -> ShowS
Show)

-- | The "registers" of the VM along with memory and data stack
data FrameState (t :: VMType) s = FrameState
  { forall (t :: VMType) s. FrameState t s -> Expr 'EAddr
contract     :: Expr EAddr
  , forall (t :: VMType) s. FrameState t s -> Expr 'EAddr
codeContract :: Expr EAddr
  , forall (t :: VMType) s. FrameState t s -> ContractCode
code         :: ContractCode
  , forall (t :: VMType) s. FrameState t s -> Int
pc           :: {-# UNPACK #-} !Int
  , forall (t :: VMType) s. FrameState t s -> [Expr 'EWord]
stack        :: [Expr EWord]
  , forall (t :: VMType) s. FrameState t s -> Memory s
memory       :: Memory s
  , forall (t :: VMType) s. FrameState t s -> Word64
memorySize   :: Word64
  , forall (t :: VMType) s. FrameState t s -> Expr 'Buf
calldata     :: Expr Buf
  , forall (t :: VMType) s. FrameState t s -> Expr 'EWord
callvalue    :: Expr EWord
  , forall (t :: VMType) s. FrameState t s -> Expr 'EAddr
caller       :: Expr EAddr
  , forall (t :: VMType) s. FrameState t s -> Gas t
gas          :: !(Gas t)
  , forall (t :: VMType) s. FrameState t s -> Expr 'Buf
returndata   :: Expr Buf
  , forall (t :: VMType) s. FrameState t s -> Bool
static       :: Bool
  }
  deriving ((forall x. FrameState t s -> Rep (FrameState t s) x)
-> (forall x. Rep (FrameState t s) x -> FrameState t s)
-> Generic (FrameState t s)
forall x. Rep (FrameState t s) x -> FrameState t s
forall x. FrameState t s -> Rep (FrameState t s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: VMType) s x. Rep (FrameState t s) x -> FrameState t s
forall (t :: VMType) s x. FrameState t s -> Rep (FrameState t s) x
$cfrom :: forall (t :: VMType) s x. FrameState t s -> Rep (FrameState t s) x
from :: forall x. FrameState t s -> Rep (FrameState t s) x
$cto :: forall (t :: VMType) s x. Rep (FrameState t s) x -> FrameState t s
to :: forall x. Rep (FrameState t s) x -> FrameState t s
Generic)

deriving instance Show (FrameState Symbolic s)
deriving instance Show (FrameState Concrete s)

data Memory s
  = ConcreteMemory (MutableMemory s)
  | SymbolicMemory !(Expr Buf)

instance Show (Memory s) where
  show :: Memory s -> String
show (ConcreteMemory MutableMemory s
_) = String
"<can't show mutable memory>"
  show (SymbolicMemory Expr 'Buf
m) = Expr 'Buf -> String
forall a. Show a => a -> String
show Expr 'Buf
m

type MutableMemory s = STVector s Word8

-- | The state that spans a whole transaction
data TxState = TxState
  { TxState -> W256
gasprice    :: W256
  , TxState -> Word64
gaslimit    :: Word64
  , TxState -> W256
priorityFee :: W256
  , TxState -> Expr 'EAddr
origin      :: Expr EAddr
  , TxState -> Expr 'EAddr
toAddr      :: Expr EAddr
  , TxState -> Expr 'EWord
value       :: Expr EWord
  , TxState -> SubState
substate    :: SubState
  , TxState -> Bool
isCreate    :: Bool
  , TxState -> Map (Expr 'EAddr) Contract
txReversion :: Map (Expr EAddr) Contract
  }
  deriving (Int -> TxState -> ShowS
[TxState] -> ShowS
TxState -> String
(Int -> TxState -> ShowS)
-> (TxState -> String) -> ([TxState] -> ShowS) -> Show TxState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TxState -> ShowS
showsPrec :: Int -> TxState -> ShowS
$cshow :: TxState -> String
show :: TxState -> String
$cshowList :: [TxState] -> ShowS
showList :: [TxState] -> ShowS
Show)

-- | Various environmental data
data Env = Env
  { Env -> Map (Expr 'EAddr) Contract
contracts      :: Map (Expr EAddr) Contract
  , Env -> W256
chainId        :: W256
  , Env -> Int
freshAddresses :: Int
  , Env -> Int
freshGasVals :: Int
  }
  deriving (Int -> Env -> ShowS
[Env] -> ShowS
Env -> String
(Int -> Env -> ShowS)
-> (Env -> String) -> ([Env] -> ShowS) -> Show Env
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Env -> ShowS
showsPrec :: Int -> Env -> ShowS
$cshow :: Env -> String
show :: Env -> String
$cshowList :: [Env] -> ShowS
showList :: [Env] -> ShowS
Show, (forall x. Env -> Rep Env x)
-> (forall x. Rep Env x -> Env) -> Generic Env
forall x. Rep Env x -> Env
forall x. Env -> Rep Env x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Env -> Rep Env x
from :: forall x. Env -> Rep Env x
$cto :: forall x. Rep Env x -> Env
to :: forall x. Rep Env x -> Env
Generic)

-- | Data about the block
data Block = Block
  { Block -> Expr 'EAddr
coinbase    :: Expr EAddr
  , Block -> Expr 'EWord
timestamp   :: Expr EWord
  , Block -> W256
number      :: W256
  , Block -> W256
prevRandao  :: W256
  , Block -> Word64
gaslimit    :: Word64
  , Block -> W256
baseFee     :: W256
  , Block -> W256
maxCodeSize :: W256
  , Block -> FeeSchedule Word64
schedule    :: FeeSchedule Word64
  } deriving (Int -> Block -> ShowS
[Block] -> ShowS
Block -> String
(Int -> Block -> ShowS)
-> (Block -> String) -> ([Block] -> ShowS) -> Show Block
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Block -> ShowS
showsPrec :: Int -> Block -> ShowS
$cshow :: Block -> String
show :: Block -> String
$cshowList :: [Block] -> ShowS
showList :: [Block] -> ShowS
Show, (forall x. Block -> Rep Block x)
-> (forall x. Rep Block x -> Block) -> Generic Block
forall x. Rep Block x -> Block
forall x. Block -> Rep Block x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Block -> Rep Block x
from :: forall x. Block -> Rep Block x
$cto :: forall x. Rep Block x -> Block
to :: forall x. Rep Block x -> Block
Generic)

-- | Full contract state
data Contract = Contract
  { Contract -> ContractCode
code        :: ContractCode
  , Contract -> Expr 'Storage
storage     :: Expr Storage
  , Contract -> Expr 'Storage
origStorage :: Expr Storage
  , Contract -> Expr 'EWord
balance     :: Expr EWord
  , Contract -> Maybe W64
nonce       :: Maybe W64
  , Contract -> Expr 'EWord
codehash    :: Expr EWord
  , Contract -> Vector Int
opIxMap     :: SV.Vector Int
  , Contract -> Vector (Int, Op)
codeOps     :: V.Vector (Int, Op)
  , Contract -> Bool
external    :: Bool
  }
  deriving (Int -> Contract -> ShowS
[Contract] -> ShowS
Contract -> String
(Int -> Contract -> ShowS)
-> (Contract -> String) -> ([Contract] -> ShowS) -> Show Contract
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Contract -> ShowS
showsPrec :: Int -> Contract -> ShowS
$cshow :: Contract -> String
show :: Contract -> String
$cshowList :: [Contract] -> ShowS
showList :: [Contract] -> ShowS
Show, Contract -> Contract -> Bool
(Contract -> Contract -> Bool)
-> (Contract -> Contract -> Bool) -> Eq Contract
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Contract -> Contract -> Bool
== :: Contract -> Contract -> Bool
$c/= :: Contract -> Contract -> Bool
/= :: Contract -> Contract -> Bool
Eq, Eq Contract
Eq Contract
-> (Contract -> Contract -> Ordering)
-> (Contract -> Contract -> Bool)
-> (Contract -> Contract -> Bool)
-> (Contract -> Contract -> Bool)
-> (Contract -> Contract -> Bool)
-> (Contract -> Contract -> Contract)
-> (Contract -> Contract -> Contract)
-> Ord Contract
Contract -> Contract -> Bool
Contract -> Contract -> Ordering
Contract -> Contract -> Contract
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Contract -> Contract -> Ordering
compare :: Contract -> Contract -> Ordering
$c< :: Contract -> Contract -> Bool
< :: Contract -> Contract -> Bool
$c<= :: Contract -> Contract -> Bool
<= :: Contract -> Contract -> Bool
$c> :: Contract -> Contract -> Bool
> :: Contract -> Contract -> Bool
$c>= :: Contract -> Contract -> Bool
>= :: Contract -> Contract -> Bool
$cmax :: Contract -> Contract -> Contract
max :: Contract -> Contract -> Contract
$cmin :: Contract -> Contract -> Contract
min :: Contract -> Contract -> Contract
Ord)

class VMOps (t :: VMType) where
  burn' :: Gas t -> EVM t s () -> EVM t s ()
  -- TODO: change to EvmWord t
  burnExp :: Expr EWord -> EVM t s () -> EVM t s ()
  burnSha3 :: Expr EWord -> EVM t s () -> EVM t s ()
  burnCalldatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
  burnCodecopy :: Expr EWord -> EVM t s () -> EVM t s ()
  burnExtcodecopy :: Expr EAddr -> Expr EWord -> EVM t s () -> EVM t s ()
  burnReturndatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
  burnLog :: Expr EWord -> Word8 -> EVM t s () -> EVM t s ()

  initialGas :: Gas t
  ensureGas :: Word64 -> EVM t s () -> EVM t s ()
  -- TODO: change to EvmWord t
  gasTryFrom :: Expr EWord -> Either () (Gas t)

  -- Gas cost of create, including hash cost if needed
  costOfCreate :: FeeSchedule Word64 -> Gas t -> Expr EWord -> Bool -> (Gas t, Gas t)

  costOfCall
    :: FeeSchedule Word64 -> Bool -> Expr EWord -> Gas t -> Gas t -> Expr EAddr
    -> (Word64 -> Word64 -> EVM t s ()) -> EVM t s ()

  reclaimRemainingGasAllowance :: VM t s -> EVM t s ()
  payRefunds :: EVM t s ()
  pushGas :: EVM t s ()
  enoughGas :: Word64 -> Gas t -> Bool
  subGas :: Gas t -> Word64 -> Gas t
  toGas :: Word64 -> Gas t

  whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a

  partial :: PartialExec -> EVM t s ()
  branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()

-- Bytecode Representations ------------------------------------------------------------------------


-- | A unique id for a given pc
type CodeLocation = (Expr EAddr, Int)

-- | The cache is data that can be persisted for efficiency:
-- any expensive query that is constant at least within a block.
data Cache = Cache
  { Cache -> Map Addr Contract
fetched :: Map Addr Contract
  , Cache -> Map (CodeLocation, Int) Bool
path    :: Map (CodeLocation, Int) Bool
  } deriving (Int -> Cache -> ShowS
[Cache] -> ShowS
Cache -> String
(Int -> Cache -> ShowS)
-> (Cache -> String) -> ([Cache] -> ShowS) -> Show Cache
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cache -> ShowS
showsPrec :: Int -> Cache -> ShowS
$cshow :: Cache -> String
show :: Cache -> String
$cshowList :: [Cache] -> ShowS
showList :: [Cache] -> ShowS
Show, (forall x. Cache -> Rep Cache x)
-> (forall x. Rep Cache x -> Cache) -> Generic Cache
forall x. Rep Cache x -> Cache
forall x. Cache -> Rep Cache x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Cache -> Rep Cache x
from :: forall x. Cache -> Rep Cache x
$cto :: forall x. Rep Cache x -> Cache
to :: forall x. Rep Cache x -> Cache
Generic)

instance Semigroup Cache where
  Cache
a <> :: Cache -> Cache -> Cache
<> Cache
b = Cache
    { $sel:fetched:Cache :: Map Addr Contract
fetched = (Contract -> Contract -> Contract)
-> Map Addr Contract -> Map Addr Contract -> Map Addr Contract
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Contract -> Contract -> Contract
unifyCachedContract Cache
a.fetched Cache
b.fetched
    , $sel:path:Cache :: Map (CodeLocation, Int) Bool
path = Map (CodeLocation, Int) Bool
-> Map (CodeLocation, Int) Bool -> Map (CodeLocation, Int) Bool
forall a. Monoid a => a -> a -> a
mappend Cache
a.path Cache
b.path
    }

instance Monoid Cache where
  mempty :: Cache
mempty = Cache { $sel:fetched:Cache :: Map Addr Contract
fetched = Map Addr Contract
forall a. Monoid a => a
mempty
                 , $sel:path:Cache :: Map (CodeLocation, Int) Bool
path = Map (CodeLocation, Int) Bool
forall a. Monoid a => a
mempty
                 }

-- only intended for use in Cache merges, where we expect
-- everything to be Concrete
unifyCachedContract :: Contract -> Contract -> Contract
unifyCachedContract :: Contract -> Contract -> Contract
unifyCachedContract Contract
a Contract
b = Contract
a { $sel:storage:Contract :: Expr 'Storage
storage = Expr 'Storage
merged }
  where merged :: Expr 'Storage
merged = case (Contract
a.storage, Contract
b.storage) of
                   (ConcreteStore Map W256 W256
sa, ConcreteStore Map W256 W256
sb) ->
                     Map W256 W256 -> Expr 'Storage
ConcreteStore (Map W256 W256 -> Map W256 W256 -> Map W256 W256
forall a. Monoid a => a -> a -> a
mappend Map W256 W256
sa Map W256 W256
sb)
                   (Expr 'Storage, Expr 'Storage)
_ -> Contract
a.storage


-- Bytecode Representations ------------------------------------------------------------------------


{- |
  A contract is either in creation (running its "constructor") or
  post-creation, and code in these two modes is treated differently
  by instructions like @EXTCODEHASH@, so we distinguish these two
  code types.

  The definition follows the structure of code output by solc. We need to use
  some heuristics here to deal with symbolic data regions that may be present
  in the bytecode since the fully abstract case is impractical:

  - initcode has concrete code, followed by an abstract data "section"
  - runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)

  hopefully we do not have to deal with dynamic immutable before we get a real data section...
-}
data ContractCode
  = UnknownCode (Expr EAddr)       -- ^ Fully abstract code, keyed on an address to give consistent results for e.g. extcodehash
  | InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation
  | RuntimeCode RuntimeCode        -- ^ "Instance" code, after contract creation
  deriving (Int -> ContractCode -> ShowS
[ContractCode] -> ShowS
ContractCode -> String
(Int -> ContractCode -> ShowS)
-> (ContractCode -> String)
-> ([ContractCode] -> ShowS)
-> Show ContractCode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ContractCode -> ShowS
showsPrec :: Int -> ContractCode -> ShowS
$cshow :: ContractCode -> String
show :: ContractCode -> String
$cshowList :: [ContractCode] -> ShowS
showList :: [ContractCode] -> ShowS
Show, ContractCode -> ContractCode -> Bool
(ContractCode -> ContractCode -> Bool)
-> (ContractCode -> ContractCode -> Bool) -> Eq ContractCode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ContractCode -> ContractCode -> Bool
== :: ContractCode -> ContractCode -> Bool
$c/= :: ContractCode -> ContractCode -> Bool
/= :: ContractCode -> ContractCode -> Bool
Eq, Eq ContractCode
Eq ContractCode
-> (ContractCode -> ContractCode -> Ordering)
-> (ContractCode -> ContractCode -> Bool)
-> (ContractCode -> ContractCode -> Bool)
-> (ContractCode -> ContractCode -> Bool)
-> (ContractCode -> ContractCode -> Bool)
-> (ContractCode -> ContractCode -> ContractCode)
-> (ContractCode -> ContractCode -> ContractCode)
-> Ord ContractCode
ContractCode -> ContractCode -> Bool
ContractCode -> ContractCode -> Ordering
ContractCode -> ContractCode -> ContractCode
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ContractCode -> ContractCode -> Ordering
compare :: ContractCode -> ContractCode -> Ordering
$c< :: ContractCode -> ContractCode -> Bool
< :: ContractCode -> ContractCode -> Bool
$c<= :: ContractCode -> ContractCode -> Bool
<= :: ContractCode -> ContractCode -> Bool
$c> :: ContractCode -> ContractCode -> Bool
> :: ContractCode -> ContractCode -> Bool
$c>= :: ContractCode -> ContractCode -> Bool
>= :: ContractCode -> ContractCode -> Bool
$cmax :: ContractCode -> ContractCode -> ContractCode
max :: ContractCode -> ContractCode -> ContractCode
$cmin :: ContractCode -> ContractCode -> ContractCode
min :: ContractCode -> ContractCode -> ContractCode
Ord)

-- | We have two variants here to optimize the fully concrete case.
-- ConcreteRuntimeCode just wraps a ByteString
-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).
data RuntimeCode
  = ConcreteRuntimeCode ByteString
  | SymbolicRuntimeCode (V.Vector (Expr Byte))
  deriving (Int -> RuntimeCode -> ShowS
[RuntimeCode] -> ShowS
RuntimeCode -> String
(Int -> RuntimeCode -> ShowS)
-> (RuntimeCode -> String)
-> ([RuntimeCode] -> ShowS)
-> Show RuntimeCode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuntimeCode -> ShowS
showsPrec :: Int -> RuntimeCode -> ShowS
$cshow :: RuntimeCode -> String
show :: RuntimeCode -> String
$cshowList :: [RuntimeCode] -> ShowS
showList :: [RuntimeCode] -> ShowS
Show, RuntimeCode -> RuntimeCode -> Bool
(RuntimeCode -> RuntimeCode -> Bool)
-> (RuntimeCode -> RuntimeCode -> Bool) -> Eq RuntimeCode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RuntimeCode -> RuntimeCode -> Bool
== :: RuntimeCode -> RuntimeCode -> Bool
$c/= :: RuntimeCode -> RuntimeCode -> Bool
/= :: RuntimeCode -> RuntimeCode -> Bool
Eq, Eq RuntimeCode
Eq RuntimeCode
-> (RuntimeCode -> RuntimeCode -> Ordering)
-> (RuntimeCode -> RuntimeCode -> Bool)
-> (RuntimeCode -> RuntimeCode -> Bool)
-> (RuntimeCode -> RuntimeCode -> Bool)
-> (RuntimeCode -> RuntimeCode -> Bool)
-> (RuntimeCode -> RuntimeCode -> RuntimeCode)
-> (RuntimeCode -> RuntimeCode -> RuntimeCode)
-> Ord RuntimeCode
RuntimeCode -> RuntimeCode -> Bool
RuntimeCode -> RuntimeCode -> Ordering
RuntimeCode -> RuntimeCode -> RuntimeCode
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RuntimeCode -> RuntimeCode -> Ordering
compare :: RuntimeCode -> RuntimeCode -> Ordering
$c< :: RuntimeCode -> RuntimeCode -> Bool
< :: RuntimeCode -> RuntimeCode -> Bool
$c<= :: RuntimeCode -> RuntimeCode -> Bool
<= :: RuntimeCode -> RuntimeCode -> Bool
$c> :: RuntimeCode -> RuntimeCode -> Bool
> :: RuntimeCode -> RuntimeCode -> Bool
$c>= :: RuntimeCode -> RuntimeCode -> Bool
>= :: RuntimeCode -> RuntimeCode -> Bool
$cmax :: RuntimeCode -> RuntimeCode -> RuntimeCode
max :: RuntimeCode -> RuntimeCode -> RuntimeCode
$cmin :: RuntimeCode -> RuntimeCode -> RuntimeCode
min :: RuntimeCode -> RuntimeCode -> RuntimeCode
Ord)

-- Execution Traces --------------------------------------------------------------------------------


data Trace = Trace
  { Trace -> Int
opIx      :: Int
  , Trace -> Contract
contract  :: Contract
  , Trace -> TraceData
tracedata :: TraceData
  }
  deriving (Trace -> Trace -> Bool
(Trace -> Trace -> Bool) -> (Trace -> Trace -> Bool) -> Eq Trace
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Trace -> Trace -> Bool
== :: Trace -> Trace -> Bool
$c/= :: Trace -> Trace -> Bool
/= :: Trace -> Trace -> Bool
Eq, Eq Trace
Eq Trace
-> (Trace -> Trace -> Ordering)
-> (Trace -> Trace -> Bool)
-> (Trace -> Trace -> Bool)
-> (Trace -> Trace -> Bool)
-> (Trace -> Trace -> Bool)
-> (Trace -> Trace -> Trace)
-> (Trace -> Trace -> Trace)
-> Ord Trace
Trace -> Trace -> Bool
Trace -> Trace -> Ordering
Trace -> Trace -> Trace
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Trace -> Trace -> Ordering
compare :: Trace -> Trace -> Ordering
$c< :: Trace -> Trace -> Bool
< :: Trace -> Trace -> Bool
$c<= :: Trace -> Trace -> Bool
<= :: Trace -> Trace -> Bool
$c> :: Trace -> Trace -> Bool
> :: Trace -> Trace -> Bool
$c>= :: Trace -> Trace -> Bool
>= :: Trace -> Trace -> Bool
$cmax :: Trace -> Trace -> Trace
max :: Trace -> Trace -> Trace
$cmin :: Trace -> Trace -> Trace
min :: Trace -> Trace -> Trace
Ord, Int -> Trace -> ShowS
[Trace] -> ShowS
Trace -> String
(Int -> Trace -> ShowS)
-> (Trace -> String) -> ([Trace] -> ShowS) -> Show Trace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Trace -> ShowS
showsPrec :: Int -> Trace -> ShowS
$cshow :: Trace -> String
show :: Trace -> String
$cshowList :: [Trace] -> ShowS
showList :: [Trace] -> ShowS
Show, (forall x. Trace -> Rep Trace x)
-> (forall x. Rep Trace x -> Trace) -> Generic Trace
forall x. Rep Trace x -> Trace
forall x. Trace -> Rep Trace x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Trace -> Rep Trace x
from :: forall x. Trace -> Rep Trace x
$cto :: forall x. Rep Trace x -> Trace
to :: forall x. Rep Trace x -> Trace
Generic)

data TraceData
  = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]
  | FrameTrace FrameContext
  | ErrorTrace EvmError
  | EntryTrace Text
  | ReturnTrace (Expr Buf) FrameContext
  deriving (TraceData -> TraceData -> Bool
(TraceData -> TraceData -> Bool)
-> (TraceData -> TraceData -> Bool) -> Eq TraceData
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TraceData -> TraceData -> Bool
== :: TraceData -> TraceData -> Bool
$c/= :: TraceData -> TraceData -> Bool
/= :: TraceData -> TraceData -> Bool
Eq, Eq TraceData
Eq TraceData
-> (TraceData -> TraceData -> Ordering)
-> (TraceData -> TraceData -> Bool)
-> (TraceData -> TraceData -> Bool)
-> (TraceData -> TraceData -> Bool)
-> (TraceData -> TraceData -> Bool)
-> (TraceData -> TraceData -> TraceData)
-> (TraceData -> TraceData -> TraceData)
-> Ord TraceData
TraceData -> TraceData -> Bool
TraceData -> TraceData -> Ordering
TraceData -> TraceData -> TraceData
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TraceData -> TraceData -> Ordering
compare :: TraceData -> TraceData -> Ordering
$c< :: TraceData -> TraceData -> Bool
< :: TraceData -> TraceData -> Bool
$c<= :: TraceData -> TraceData -> Bool
<= :: TraceData -> TraceData -> Bool
$c> :: TraceData -> TraceData -> Bool
> :: TraceData -> TraceData -> Bool
$c>= :: TraceData -> TraceData -> Bool
>= :: TraceData -> TraceData -> Bool
$cmax :: TraceData -> TraceData -> TraceData
max :: TraceData -> TraceData -> TraceData
$cmin :: TraceData -> TraceData -> TraceData
min :: TraceData -> TraceData -> TraceData
Ord, Int -> TraceData -> ShowS
[TraceData] -> ShowS
TraceData -> String
(Int -> TraceData -> ShowS)
-> (TraceData -> String)
-> ([TraceData] -> ShowS)
-> Show TraceData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TraceData -> ShowS
showsPrec :: Int -> TraceData -> ShowS
$cshow :: TraceData -> String
show :: TraceData -> String
$cshowList :: [TraceData] -> ShowS
showList :: [TraceData] -> ShowS
Show, (forall x. TraceData -> Rep TraceData x)
-> (forall x. Rep TraceData x -> TraceData) -> Generic TraceData
forall x. Rep TraceData x -> TraceData
forall x. TraceData -> Rep TraceData x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TraceData -> Rep TraceData x
from :: forall x. TraceData -> Rep TraceData x
$cto :: forall x. Rep TraceData x -> TraceData
to :: forall x. Rep TraceData x -> TraceData
Generic)

-- | Wrapper type containing vm traces and the context needed to pretty print them properly
data Traces = Traces
  { Traces -> Forest Trace
traces :: Forest Trace
  , Traces -> Map (Expr 'EAddr) Contract
contracts :: Map (Expr EAddr) Contract
  }
  deriving (Traces -> Traces -> Bool
(Traces -> Traces -> Bool)
-> (Traces -> Traces -> Bool) -> Eq Traces
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Traces -> Traces -> Bool
== :: Traces -> Traces -> Bool
$c/= :: Traces -> Traces -> Bool
/= :: Traces -> Traces -> Bool
Eq, Eq Traces
Eq Traces
-> (Traces -> Traces -> Ordering)
-> (Traces -> Traces -> Bool)
-> (Traces -> Traces -> Bool)
-> (Traces -> Traces -> Bool)
-> (Traces -> Traces -> Bool)
-> (Traces -> Traces -> Traces)
-> (Traces -> Traces -> Traces)
-> Ord Traces
Traces -> Traces -> Bool
Traces -> Traces -> Ordering
Traces -> Traces -> Traces
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Traces -> Traces -> Ordering
compare :: Traces -> Traces -> Ordering
$c< :: Traces -> Traces -> Bool
< :: Traces -> Traces -> Bool
$c<= :: Traces -> Traces -> Bool
<= :: Traces -> Traces -> Bool
$c> :: Traces -> Traces -> Bool
> :: Traces -> Traces -> Bool
$c>= :: Traces -> Traces -> Bool
>= :: Traces -> Traces -> Bool
$cmax :: Traces -> Traces -> Traces
max :: Traces -> Traces -> Traces
$cmin :: Traces -> Traces -> Traces
min :: Traces -> Traces -> Traces
Ord, Int -> Traces -> ShowS
[Traces] -> ShowS
Traces -> String
(Int -> Traces -> ShowS)
-> (Traces -> String) -> ([Traces] -> ShowS) -> Show Traces
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Traces -> ShowS
showsPrec :: Int -> Traces -> ShowS
$cshow :: Traces -> String
show :: Traces -> String
$cshowList :: [Traces] -> ShowS
showList :: [Traces] -> ShowS
Show, (forall x. Traces -> Rep Traces x)
-> (forall x. Rep Traces x -> Traces) -> Generic Traces
forall x. Rep Traces x -> Traces
forall x. Traces -> Rep Traces x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Traces -> Rep Traces x
from :: forall x. Traces -> Rep Traces x
$cto :: forall x. Rep Traces x -> Traces
to :: forall x. Rep Traces x -> Traces
Generic)

instance Semigroup Traces where
  (Traces Forest Trace
a Map (Expr 'EAddr) Contract
b) <> :: Traces -> Traces -> Traces
<> (Traces Forest Trace
c Map (Expr 'EAddr) Contract
d) = Forest Trace -> Map (Expr 'EAddr) Contract -> Traces
Traces (Forest Trace
a Forest Trace -> Forest Trace -> Forest Trace
forall a. Semigroup a => a -> a -> a
<> Forest Trace
c) (Map (Expr 'EAddr) Contract
b Map (Expr 'EAddr) Contract
-> Map (Expr 'EAddr) Contract -> Map (Expr 'EAddr) Contract
forall a. Semigroup a => a -> a -> a
<> Map (Expr 'EAddr) Contract
d)
instance Monoid Traces where
  mempty :: Traces
mempty = Forest Trace -> Map (Expr 'EAddr) Contract -> Traces
Traces Forest Trace
forall a. Monoid a => a
mempty Map (Expr 'EAddr) Contract
forall a. Monoid a => a
mempty


-- VM Initialization -------------------------------------------------------------------------------


-- | A specification for an initial VM state
data VMOpts (t :: VMType) = VMOpts
  { forall (t :: VMType). VMOpts t -> Contract
contract :: Contract
  , forall (t :: VMType). VMOpts t -> [(Expr 'EAddr, Contract)]
otherContracts :: [(Expr EAddr, Contract)]
  , forall (t :: VMType). VMOpts t -> (Expr 'Buf, [Prop])
calldata :: (Expr Buf, [Prop])
  , forall (t :: VMType). VMOpts t -> BaseState
baseState :: BaseState
  , forall (t :: VMType). VMOpts t -> Expr 'EWord
value :: Expr EWord
  , forall (t :: VMType). VMOpts t -> W256
priorityFee :: W256
  , forall (t :: VMType). VMOpts t -> Expr 'EAddr
address :: Expr EAddr
  , forall (t :: VMType). VMOpts t -> Expr 'EAddr
caller :: Expr EAddr
  , forall (t :: VMType). VMOpts t -> Expr 'EAddr
origin :: Expr EAddr
  , forall (t :: VMType). VMOpts t -> Gas t
gas :: Gas t
  , forall (t :: VMType). VMOpts t -> Word64
gaslimit :: Word64
  , forall (t :: VMType). VMOpts t -> W256
number :: W256
  , forall (t :: VMType). VMOpts t -> Expr 'EWord
timestamp :: Expr EWord
  , forall (t :: VMType). VMOpts t -> Expr 'EAddr
coinbase :: Expr EAddr
  , forall (t :: VMType). VMOpts t -> W256
prevRandao :: W256
  , forall (t :: VMType). VMOpts t -> W256
maxCodeSize :: W256
  , forall (t :: VMType). VMOpts t -> Word64
blockGaslimit :: Word64
  , forall (t :: VMType). VMOpts t -> W256
gasprice :: W256
  , forall (t :: VMType). VMOpts t -> W256
baseFee :: W256
  , forall (t :: VMType). VMOpts t -> FeeSchedule Word64
schedule :: FeeSchedule Word64
  , forall (t :: VMType). VMOpts t -> W256
chainId :: W256
  , forall (t :: VMType). VMOpts t -> Bool
create :: Bool
  , forall (t :: VMType). VMOpts t -> Map (Expr 'EAddr) [W256]
txAccessList :: Map (Expr EAddr) [W256]
  , forall (t :: VMType). VMOpts t -> Bool
allowFFI :: Bool
  }

deriving instance Show (VMOpts Symbolic)
deriving instance Show (VMOpts Concrete)


-- Opcodes -----------------------------------------------------------------------------------------


type Op = GenericOp (Expr EWord)

data GenericOp a
  = OpStop
  | OpAdd
  | OpMul
  | OpSub
  | OpDiv
  | OpSdiv
  | OpMod
  | OpSmod
  | OpAddmod
  | OpMulmod
  | OpExp
  | OpSignextend
  | OpLt
  | OpGt
  | OpSlt
  | OpSgt
  | OpEq
  | OpIszero
  | OpAnd
  | OpOr
  | OpXor
  | OpNot
  | OpByte
  | OpShl
  | OpShr
  | OpSar
  | OpSha3
  | OpAddress
  | OpBalance
  | OpOrigin
  | OpCaller
  | OpCallvalue
  | OpCalldataload
  | OpCalldatasize
  | OpCalldatacopy
  | OpCodesize
  | OpCodecopy
  | OpGasprice
  | OpExtcodesize
  | OpExtcodecopy
  | OpReturndatasize
  | OpReturndatacopy
  | OpExtcodehash
  | OpBlockhash
  | OpCoinbase
  | OpTimestamp
  | OpNumber
  | OpPrevRandao
  | OpGaslimit
  | OpChainid
  | OpSelfbalance
  | OpBaseFee
  | OpPop
  | OpMload
  | OpMstore
  | OpMstore8
  | OpSload
  | OpSstore
  | OpJump
  | OpJumpi
  | OpPc
  | OpMsize
  | OpGas
  | OpJumpdest
  | OpCreate
  | OpCall
  | OpStaticcall
  | OpCallcode
  | OpReturn
  | OpDelegatecall
  | OpCreate2
  | OpRevert
  | OpSelfdestruct
  | OpDup !Word8
  | OpSwap !Word8
  | OpLog !Word8
  | OpPush0
  | OpPush a
  | OpUnknown Word8
  deriving (Int -> GenericOp a -> ShowS
[GenericOp a] -> ShowS
GenericOp a -> String
(Int -> GenericOp a -> ShowS)
-> (GenericOp a -> String)
-> ([GenericOp a] -> ShowS)
-> Show (GenericOp a)
forall a. Show a => Int -> GenericOp a -> ShowS
forall a. Show a => [GenericOp a] -> ShowS
forall a. Show a => GenericOp a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> GenericOp a -> ShowS
showsPrec :: Int -> GenericOp a -> ShowS
$cshow :: forall a. Show a => GenericOp a -> String
show :: GenericOp a -> String
$cshowList :: forall a. Show a => [GenericOp a] -> ShowS
showList :: [GenericOp a] -> ShowS
Show, GenericOp a -> GenericOp a -> Bool
(GenericOp a -> GenericOp a -> Bool)
-> (GenericOp a -> GenericOp a -> Bool) -> Eq (GenericOp a)
forall a. Eq a => GenericOp a -> GenericOp a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => GenericOp a -> GenericOp a -> Bool
== :: GenericOp a -> GenericOp a -> Bool
$c/= :: forall a. Eq a => GenericOp a -> GenericOp a -> Bool
/= :: GenericOp a -> GenericOp a -> Bool
Eq, Eq (GenericOp a)
Eq (GenericOp a)
-> (GenericOp a -> GenericOp a -> Ordering)
-> (GenericOp a -> GenericOp a -> Bool)
-> (GenericOp a -> GenericOp a -> Bool)
-> (GenericOp a -> GenericOp a -> Bool)
-> (GenericOp a -> GenericOp a -> Bool)
-> (GenericOp a -> GenericOp a -> GenericOp a)
-> (GenericOp a -> GenericOp a -> GenericOp a)
-> Ord (GenericOp a)
GenericOp a -> GenericOp a -> Bool
GenericOp a -> GenericOp a -> Ordering
GenericOp a -> GenericOp a -> GenericOp a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (GenericOp a)
forall a. Ord a => GenericOp a -> GenericOp a -> Bool
forall a. Ord a => GenericOp a -> GenericOp a -> Ordering
forall a. Ord a => GenericOp a -> GenericOp a -> GenericOp a
$ccompare :: forall a. Ord a => GenericOp a -> GenericOp a -> Ordering
compare :: GenericOp a -> GenericOp a -> Ordering
$c< :: forall a. Ord a => GenericOp a -> GenericOp a -> Bool
< :: GenericOp a -> GenericOp a -> Bool
$c<= :: forall a. Ord a => GenericOp a -> GenericOp a -> Bool
<= :: GenericOp a -> GenericOp a -> Bool
$c> :: forall a. Ord a => GenericOp a -> GenericOp a -> Bool
> :: GenericOp a -> GenericOp a -> Bool
$c>= :: forall a. Ord a => GenericOp a -> GenericOp a -> Bool
>= :: GenericOp a -> GenericOp a -> Bool
$cmax :: forall a. Ord a => GenericOp a -> GenericOp a -> GenericOp a
max :: GenericOp a -> GenericOp a -> GenericOp a
$cmin :: forall a. Ord a => GenericOp a -> GenericOp a -> GenericOp a
min :: GenericOp a -> GenericOp a -> GenericOp a
Ord, (forall a b. (a -> b) -> GenericOp a -> GenericOp b)
-> (forall a b. a -> GenericOp b -> GenericOp a)
-> Functor GenericOp
forall a b. a -> GenericOp b -> GenericOp a
forall a b. (a -> b) -> GenericOp a -> GenericOp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GenericOp a -> GenericOp b
fmap :: forall a b. (a -> b) -> GenericOp a -> GenericOp b
$c<$ :: forall a b. a -> GenericOp b -> GenericOp a
<$ :: forall a b. a -> GenericOp b -> GenericOp a
Functor)


-- Function Selectors ------------------------------------------------------------------------------


-- | https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector
newtype FunctionSelector = FunctionSelector { FunctionSelector -> Word32
unFunctionSelector :: Word32 }
  deriving (Eq FunctionSelector
FunctionSelector
Eq FunctionSelector
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> FunctionSelector
-> (Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> Bool)
-> (FunctionSelector -> Maybe Int)
-> (FunctionSelector -> Int)
-> (FunctionSelector -> Bool)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int -> FunctionSelector)
-> (FunctionSelector -> Int)
-> Bits FunctionSelector
Int -> FunctionSelector
FunctionSelector -> Bool
FunctionSelector -> Int
FunctionSelector -> Maybe Int
FunctionSelector -> FunctionSelector
FunctionSelector -> Int -> Bool
FunctionSelector -> Int -> FunctionSelector
FunctionSelector -> FunctionSelector -> FunctionSelector
forall a.
Eq a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
$c.&. :: FunctionSelector -> FunctionSelector -> FunctionSelector
.&. :: FunctionSelector -> FunctionSelector -> FunctionSelector
$c.|. :: FunctionSelector -> FunctionSelector -> FunctionSelector
.|. :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cxor :: FunctionSelector -> FunctionSelector -> FunctionSelector
xor :: FunctionSelector -> FunctionSelector -> FunctionSelector
$ccomplement :: FunctionSelector -> FunctionSelector
complement :: FunctionSelector -> FunctionSelector
$cshift :: FunctionSelector -> Int -> FunctionSelector
shift :: FunctionSelector -> Int -> FunctionSelector
$crotate :: FunctionSelector -> Int -> FunctionSelector
rotate :: FunctionSelector -> Int -> FunctionSelector
$czeroBits :: FunctionSelector
zeroBits :: FunctionSelector
$cbit :: Int -> FunctionSelector
bit :: Int -> FunctionSelector
$csetBit :: FunctionSelector -> Int -> FunctionSelector
setBit :: FunctionSelector -> Int -> FunctionSelector
$cclearBit :: FunctionSelector -> Int -> FunctionSelector
clearBit :: FunctionSelector -> Int -> FunctionSelector
$ccomplementBit :: FunctionSelector -> Int -> FunctionSelector
complementBit :: FunctionSelector -> Int -> FunctionSelector
$ctestBit :: FunctionSelector -> Int -> Bool
testBit :: FunctionSelector -> Int -> Bool
$cbitSizeMaybe :: FunctionSelector -> Maybe Int
bitSizeMaybe :: FunctionSelector -> Maybe Int
$cbitSize :: FunctionSelector -> Int
bitSize :: FunctionSelector -> Int
$cisSigned :: FunctionSelector -> Bool
isSigned :: FunctionSelector -> Bool
$cshiftL :: FunctionSelector -> Int -> FunctionSelector
shiftL :: FunctionSelector -> Int -> FunctionSelector
$cunsafeShiftL :: FunctionSelector -> Int -> FunctionSelector
unsafeShiftL :: FunctionSelector -> Int -> FunctionSelector
$cshiftR :: FunctionSelector -> Int -> FunctionSelector
shiftR :: FunctionSelector -> Int -> FunctionSelector
$cunsafeShiftR :: FunctionSelector -> Int -> FunctionSelector
unsafeShiftR :: FunctionSelector -> Int -> FunctionSelector
$crotateL :: FunctionSelector -> Int -> FunctionSelector
rotateL :: FunctionSelector -> Int -> FunctionSelector
$crotateR :: FunctionSelector -> Int -> FunctionSelector
rotateR :: FunctionSelector -> Int -> FunctionSelector
$cpopCount :: FunctionSelector -> Int
popCount :: FunctionSelector -> Int
Bits, Integer -> FunctionSelector
FunctionSelector -> FunctionSelector
FunctionSelector -> FunctionSelector -> FunctionSelector
(FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector)
-> (Integer -> FunctionSelector)
-> Num FunctionSelector
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: FunctionSelector -> FunctionSelector -> FunctionSelector
+ :: FunctionSelector -> FunctionSelector -> FunctionSelector
$c- :: FunctionSelector -> FunctionSelector -> FunctionSelector
- :: FunctionSelector -> FunctionSelector -> FunctionSelector
$c* :: FunctionSelector -> FunctionSelector -> FunctionSelector
* :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cnegate :: FunctionSelector -> FunctionSelector
negate :: FunctionSelector -> FunctionSelector
$cabs :: FunctionSelector -> FunctionSelector
abs :: FunctionSelector -> FunctionSelector
$csignum :: FunctionSelector -> FunctionSelector
signum :: FunctionSelector -> FunctionSelector
$cfromInteger :: Integer -> FunctionSelector
fromInteger :: Integer -> FunctionSelector
Num, FunctionSelector -> FunctionSelector -> Bool
(FunctionSelector -> FunctionSelector -> Bool)
-> (FunctionSelector -> FunctionSelector -> Bool)
-> Eq FunctionSelector
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunctionSelector -> FunctionSelector -> Bool
== :: FunctionSelector -> FunctionSelector -> Bool
$c/= :: FunctionSelector -> FunctionSelector -> Bool
/= :: FunctionSelector -> FunctionSelector -> Bool
Eq, Eq FunctionSelector
Eq FunctionSelector
-> (FunctionSelector -> FunctionSelector -> Ordering)
-> (FunctionSelector -> FunctionSelector -> Bool)
-> (FunctionSelector -> FunctionSelector -> Bool)
-> (FunctionSelector -> FunctionSelector -> Bool)
-> (FunctionSelector -> FunctionSelector -> Bool)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> Ord FunctionSelector
FunctionSelector -> FunctionSelector -> Bool
FunctionSelector -> FunctionSelector -> Ordering
FunctionSelector -> FunctionSelector -> FunctionSelector
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FunctionSelector -> FunctionSelector -> Ordering
compare :: FunctionSelector -> FunctionSelector -> Ordering
$c< :: FunctionSelector -> FunctionSelector -> Bool
< :: FunctionSelector -> FunctionSelector -> Bool
$c<= :: FunctionSelector -> FunctionSelector -> Bool
<= :: FunctionSelector -> FunctionSelector -> Bool
$c> :: FunctionSelector -> FunctionSelector -> Bool
> :: FunctionSelector -> FunctionSelector -> Bool
$c>= :: FunctionSelector -> FunctionSelector -> Bool
>= :: FunctionSelector -> FunctionSelector -> Bool
$cmax :: FunctionSelector -> FunctionSelector -> FunctionSelector
max :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cmin :: FunctionSelector -> FunctionSelector -> FunctionSelector
min :: FunctionSelector -> FunctionSelector -> FunctionSelector
Ord, Num FunctionSelector
Ord FunctionSelector
Num FunctionSelector
-> Ord FunctionSelector
-> (FunctionSelector -> Rational)
-> Real FunctionSelector
FunctionSelector -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
$ctoRational :: FunctionSelector -> Rational
toRational :: FunctionSelector -> Rational
Real, Int -> FunctionSelector
FunctionSelector -> Int
FunctionSelector -> [FunctionSelector]
FunctionSelector -> FunctionSelector
FunctionSelector -> FunctionSelector -> [FunctionSelector]
FunctionSelector
-> FunctionSelector -> FunctionSelector -> [FunctionSelector]
(FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector)
-> (Int -> FunctionSelector)
-> (FunctionSelector -> Int)
-> (FunctionSelector -> [FunctionSelector])
-> (FunctionSelector -> FunctionSelector -> [FunctionSelector])
-> (FunctionSelector -> FunctionSelector -> [FunctionSelector])
-> (FunctionSelector
    -> FunctionSelector -> FunctionSelector -> [FunctionSelector])
-> Enum FunctionSelector
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: FunctionSelector -> FunctionSelector
succ :: FunctionSelector -> FunctionSelector
$cpred :: FunctionSelector -> FunctionSelector
pred :: FunctionSelector -> FunctionSelector
$ctoEnum :: Int -> FunctionSelector
toEnum :: Int -> FunctionSelector
$cfromEnum :: FunctionSelector -> Int
fromEnum :: FunctionSelector -> Int
$cenumFrom :: FunctionSelector -> [FunctionSelector]
enumFrom :: FunctionSelector -> [FunctionSelector]
$cenumFromThen :: FunctionSelector -> FunctionSelector -> [FunctionSelector]
enumFromThen :: FunctionSelector -> FunctionSelector -> [FunctionSelector]
$cenumFromTo :: FunctionSelector -> FunctionSelector -> [FunctionSelector]
enumFromTo :: FunctionSelector -> FunctionSelector -> [FunctionSelector]
$cenumFromThenTo :: FunctionSelector
-> FunctionSelector -> FunctionSelector -> [FunctionSelector]
enumFromThenTo :: FunctionSelector
-> FunctionSelector -> FunctionSelector -> [FunctionSelector]
Enum, Enum FunctionSelector
Real FunctionSelector
Real FunctionSelector
-> Enum FunctionSelector
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector -> FunctionSelector -> FunctionSelector)
-> (FunctionSelector
    -> FunctionSelector -> (FunctionSelector, FunctionSelector))
-> (FunctionSelector
    -> FunctionSelector -> (FunctionSelector, FunctionSelector))
-> (FunctionSelector -> Integer)
-> Integral FunctionSelector
FunctionSelector -> Integer
FunctionSelector
-> FunctionSelector -> (FunctionSelector, FunctionSelector)
FunctionSelector -> FunctionSelector -> FunctionSelector
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: FunctionSelector -> FunctionSelector -> FunctionSelector
quot :: FunctionSelector -> FunctionSelector -> FunctionSelector
$crem :: FunctionSelector -> FunctionSelector -> FunctionSelector
rem :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cdiv :: FunctionSelector -> FunctionSelector -> FunctionSelector
div :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cmod :: FunctionSelector -> FunctionSelector -> FunctionSelector
mod :: FunctionSelector -> FunctionSelector -> FunctionSelector
$cquotRem :: FunctionSelector
-> FunctionSelector -> (FunctionSelector, FunctionSelector)
quotRem :: FunctionSelector
-> FunctionSelector -> (FunctionSelector, FunctionSelector)
$cdivMod :: FunctionSelector
-> FunctionSelector -> (FunctionSelector, FunctionSelector)
divMod :: FunctionSelector
-> FunctionSelector -> (FunctionSelector, FunctionSelector)
$ctoInteger :: FunctionSelector -> Integer
toInteger :: FunctionSelector -> Integer
Integral)
instance Show FunctionSelector where show :: FunctionSelector -> String
show FunctionSelector
s = String
"0x" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> FunctionSelector -> ShowS
forall a. Integral a => a -> ShowS
showHex FunctionSelector
s String
""


-- ByteString wrapper ------------------------------------------------------------------------------


-- Newtype wrapper for ByteString to allow custom instances
newtype ByteStringS = ByteStringS ByteString deriving (ByteStringS -> ByteStringS -> Bool
(ByteStringS -> ByteStringS -> Bool)
-> (ByteStringS -> ByteStringS -> Bool) -> Eq ByteStringS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ByteStringS -> ByteStringS -> Bool
== :: ByteStringS -> ByteStringS -> Bool
$c/= :: ByteStringS -> ByteStringS -> Bool
/= :: ByteStringS -> ByteStringS -> Bool
Eq, (forall x. ByteStringS -> Rep ByteStringS x)
-> (forall x. Rep ByteStringS x -> ByteStringS)
-> Generic ByteStringS
forall x. Rep ByteStringS x -> ByteStringS
forall x. ByteStringS -> Rep ByteStringS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ByteStringS -> Rep ByteStringS x
from :: forall x. ByteStringS -> Rep ByteStringS x
$cto :: forall x. Rep ByteStringS x -> ByteStringS
to :: forall x. Rep ByteStringS x -> ByteStringS
Generic)

instance Show ByteStringS where
  show :: ByteStringS -> String
show (ByteStringS ByteString
x) = (String
"0x" ++) ShowS -> (ByteString -> String) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> String) -> (ByteString -> Text) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
fromBinary (ByteString -> String) -> ByteString -> String
forall a b. (a -> b) -> a -> b
$ ByteString
x
    where
      fromBinary :: ByteString -> Text
fromBinary =
        ByteString -> Text
T.decodeUtf8 (ByteString -> Text)
-> (ByteString -> ByteString) -> ByteString -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
toStrict (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (ByteString -> Builder) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Builder
byteStringHex

instance JSON.FromJSON ByteStringS where
  parseJSON :: Value -> Parser ByteStringS
parseJSON (JSON.String Text
x) = case Text -> Either Text ByteString
BS16.decodeBase16' Text
x of
                                Left Text
_ -> Parser ByteStringS
forall a. Parser a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                                Right ByteString
bs -> ByteStringS -> Parser ByteStringS
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> ByteStringS
ByteStringS ByteString
bs)
  parseJSON Value
_ = Parser ByteStringS
forall a. Parser a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance JSON.ToJSON ByteStringS where
  toJSON :: ByteStringS -> Value
toJSON (ByteStringS ByteString
x) = Text -> Value
JSON.String (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Word8 -> String) -> [Word8] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int -> Word8 -> String
forall a. (Show a, Integral a) => Int -> a -> String
paddedShowHex Int
2) ([Word8] -> String)
-> (ByteString -> [Word8]) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> [Word8]
BS.unpack (ByteString -> String) -> ByteString -> String
forall a b. (a -> b) -> a -> b
$ ByteString
x))


-- Word256 wrapper ---------------------------------------------------------------------------------


-- Newtype wrapper around Word256 to allow custom instances
newtype W256 = W256 Word256
  deriving
    ( Integer -> W256
W256 -> W256
W256 -> W256 -> W256
(W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256)
-> (W256 -> W256)
-> (W256 -> W256)
-> (Integer -> W256)
-> Num W256
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: W256 -> W256 -> W256
+ :: W256 -> W256 -> W256
$c- :: W256 -> W256 -> W256
- :: W256 -> W256 -> W256
$c* :: W256 -> W256 -> W256
* :: W256 -> W256 -> W256
$cnegate :: W256 -> W256
negate :: W256 -> W256
$cabs :: W256 -> W256
abs :: W256 -> W256
$csignum :: W256 -> W256
signum :: W256 -> W256
$cfromInteger :: Integer -> W256
fromInteger :: Integer -> W256
Num, Enum W256
Real W256
Real W256
-> Enum W256
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> (W256, W256))
-> (W256 -> W256 -> (W256, W256))
-> (W256 -> Integer)
-> Integral W256
W256 -> Integer
W256 -> W256 -> (W256, W256)
W256 -> W256 -> W256
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: W256 -> W256 -> W256
quot :: W256 -> W256 -> W256
$crem :: W256 -> W256 -> W256
rem :: W256 -> W256 -> W256
$cdiv :: W256 -> W256 -> W256
div :: W256 -> W256 -> W256
$cmod :: W256 -> W256 -> W256
mod :: W256 -> W256 -> W256
$cquotRem :: W256 -> W256 -> (W256, W256)
quotRem :: W256 -> W256 -> (W256, W256)
$cdivMod :: W256 -> W256 -> (W256, W256)
divMod :: W256 -> W256 -> (W256, W256)
$ctoInteger :: W256 -> Integer
toInteger :: W256 -> Integer
Integral, Num W256
Ord W256
Num W256 -> Ord W256 -> (W256 -> Rational) -> Real W256
W256 -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
$ctoRational :: W256 -> Rational
toRational :: W256 -> Rational
Real, Eq W256
Eq W256
-> (W256 -> W256 -> Ordering)
-> (W256 -> W256 -> Bool)
-> (W256 -> W256 -> Bool)
-> (W256 -> W256 -> Bool)
-> (W256 -> W256 -> Bool)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> Ord W256
W256 -> W256 -> Bool
W256 -> W256 -> Ordering
W256 -> W256 -> W256
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: W256 -> W256 -> Ordering
compare :: W256 -> W256 -> Ordering
$c< :: W256 -> W256 -> Bool
< :: W256 -> W256 -> Bool
$c<= :: W256 -> W256 -> Bool
<= :: W256 -> W256 -> Bool
$c> :: W256 -> W256 -> Bool
> :: W256 -> W256 -> Bool
$c>= :: W256 -> W256 -> Bool
>= :: W256 -> W256 -> Bool
$cmax :: W256 -> W256 -> W256
max :: W256 -> W256 -> W256
$cmin :: W256 -> W256 -> W256
min :: W256 -> W256 -> W256
Ord, Eq W256
W256
Eq W256
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256 -> W256)
-> (W256 -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> W256
-> (Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> Bool)
-> (W256 -> Maybe Int)
-> (W256 -> Int)
-> (W256 -> Bool)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int -> W256)
-> (W256 -> Int)
-> Bits W256
Int -> W256
W256 -> Bool
W256 -> Int
W256 -> Maybe Int
W256 -> W256
W256 -> Int -> Bool
W256 -> Int -> W256
W256 -> W256 -> W256
forall a.
Eq a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
$c.&. :: W256 -> W256 -> W256
.&. :: W256 -> W256 -> W256
$c.|. :: W256 -> W256 -> W256
.|. :: W256 -> W256 -> W256
$cxor :: W256 -> W256 -> W256
xor :: W256 -> W256 -> W256
$ccomplement :: W256 -> W256
complement :: W256 -> W256
$cshift :: W256 -> Int -> W256
shift :: W256 -> Int -> W256
$crotate :: W256 -> Int -> W256
rotate :: W256 -> Int -> W256
$czeroBits :: W256
zeroBits :: W256
$cbit :: Int -> W256
bit :: Int -> W256
$csetBit :: W256 -> Int -> W256
setBit :: W256 -> Int -> W256
$cclearBit :: W256 -> Int -> W256
clearBit :: W256 -> Int -> W256
$ccomplementBit :: W256 -> Int -> W256
complementBit :: W256 -> Int -> W256
$ctestBit :: W256 -> Int -> Bool
testBit :: W256 -> Int -> Bool
$cbitSizeMaybe :: W256 -> Maybe Int
bitSizeMaybe :: W256 -> Maybe Int
$cbitSize :: W256 -> Int
bitSize :: W256 -> Int
$cisSigned :: W256 -> Bool
isSigned :: W256 -> Bool
$cshiftL :: W256 -> Int -> W256
shiftL :: W256 -> Int -> W256
$cunsafeShiftL :: W256 -> Int -> W256
unsafeShiftL :: W256 -> Int -> W256
$cshiftR :: W256 -> Int -> W256
shiftR :: W256 -> Int -> W256
$cunsafeShiftR :: W256 -> Int -> W256
unsafeShiftR :: W256 -> Int -> W256
$crotateL :: W256 -> Int -> W256
rotateL :: W256 -> Int -> W256
$crotateR :: W256 -> Int -> W256
rotateR :: W256 -> Int -> W256
$cpopCount :: W256 -> Int
popCount :: W256 -> Int
Bits
    , (forall x. W256 -> Rep W256 x)
-> (forall x. Rep W256 x -> W256) -> Generic W256
forall x. Rep W256 x -> W256
forall x. W256 -> Rep W256 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. W256 -> Rep W256 x
from :: forall x. W256 -> Rep W256 x
$cto :: forall x. Rep W256 x -> W256
to :: forall x. Rep W256 x -> W256
Generic, Bits W256
Bits W256
-> (W256 -> Int)
-> (W256 -> Int)
-> (W256 -> Int)
-> FiniteBits W256
W256 -> Int
forall b.
Bits b -> (b -> Int) -> (b -> Int) -> (b -> Int) -> FiniteBits b
$cfiniteBitSize :: W256 -> Int
finiteBitSize :: W256 -> Int
$ccountLeadingZeros :: W256 -> Int
countLeadingZeros :: W256 -> Int
$ccountTrailingZeros :: W256 -> Int
countTrailingZeros :: W256 -> Int
FiniteBits, Int -> W256
W256 -> Int
W256 -> [W256]
W256 -> W256
W256 -> W256 -> [W256]
W256 -> W256 -> W256 -> [W256]
(W256 -> W256)
-> (W256 -> W256)
-> (Int -> W256)
-> (W256 -> Int)
-> (W256 -> [W256])
-> (W256 -> W256 -> [W256])
-> (W256 -> W256 -> [W256])
-> (W256 -> W256 -> W256 -> [W256])
-> Enum W256
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: W256 -> W256
succ :: W256 -> W256
$cpred :: W256 -> W256
pred :: W256 -> W256
$ctoEnum :: Int -> W256
toEnum :: Int -> W256
$cfromEnum :: W256 -> Int
fromEnum :: W256 -> Int
$cenumFrom :: W256 -> [W256]
enumFrom :: W256 -> [W256]
$cenumFromThen :: W256 -> W256 -> [W256]
enumFromThen :: W256 -> W256 -> [W256]
$cenumFromTo :: W256 -> W256 -> [W256]
enumFromTo :: W256 -> W256 -> [W256]
$cenumFromThenTo :: W256 -> W256 -> W256 -> [W256]
enumFromThenTo :: W256 -> W256 -> W256 -> [W256]
Enum, W256 -> W256 -> Bool
(W256 -> W256 -> Bool) -> (W256 -> W256 -> Bool) -> Eq W256
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: W256 -> W256 -> Bool
== :: W256 -> W256 -> Bool
$c/= :: W256 -> W256 -> Bool
/= :: W256 -> W256 -> Bool
Eq , W256
W256 -> W256 -> Bounded W256
forall a. a -> a -> Bounded a
$cminBound :: W256
minBound :: W256
$cmaxBound :: W256
maxBound :: W256
Bounded
    )

instance Read W256 where
  readsPrec :: Int -> ReadS W256
readsPrec Int
_ String
"0x" = [(W256
0, String
"")]
  readsPrec Int
n String
s = (Word256 -> W256) -> (Word256, String) -> (W256, String)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Word256 -> W256
W256 ((Word256, String) -> (W256, String))
-> [(Word256, String)] -> [(W256, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReadS Word256
forall a. Read a => Int -> ReadS a
readsPrec Int
n String
s

instance Show W256 where
  showsPrec :: Int -> W256 -> ShowS
showsPrec Int
_ W256
s = (String
"0x" ++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> ShowS
forall a. Integral a => a -> ShowS
showHex W256
s

instance JSON.ToJSON W256 where
  toJSON :: W256 -> Value
toJSON W256
x = Text -> Value
JSON.String  (Text -> Value) -> Text -> Value
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
pad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cutshow)
    where
      cutshow :: String
cutshow = Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
2 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ W256 -> String
forall a. Show a => a -> String
show W256
x
      pad :: String
pad = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
64 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String
cutshow)) Char
'0'

instance FromJSON W256 where
  parseJSON :: Value -> Parser W256
parseJSON Value
v = do
    String
s <- Text -> String
T.unpack (Text -> String) -> Parser Text -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Text
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case ReadS W256
forall a. Read a => ReadS a
reads String
s of
      [(W256
x, String
"")]  -> W256 -> Parser W256
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure W256
x
      [(W256, String)]
_          -> String -> Parser W256
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser W256) -> String -> Parser W256
forall a b. (a -> b) -> a -> b
$ String
"invalid hex word (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance FromJSONKey W256 where
  fromJSONKey :: FromJSONKeyFunction W256
fromJSONKey = (Text -> Parser W256) -> FromJSONKeyFunction W256
forall a. (Text -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyTextParser ((Text -> Parser W256) -> FromJSONKeyFunction W256)
-> (Text -> Parser W256) -> FromJSONKeyFunction W256
forall a b. (a -> b) -> a -> b
$ \Text
s ->
    case ReadS W256
forall a. Read a => ReadS a
reads (Text -> String
T.unpack Text
s) of
      [(W256
x, String
"")]  -> W256 -> Parser W256
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure W256
x
      [(W256, String)]
_          -> String -> Parser W256
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser W256) -> String -> Parser W256
forall a b. (a -> b) -> a -> b
$ String
"invalid word (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

wordField :: JSON.Object -> Key -> JSON.Parser W256
wordField :: Object -> Key -> Parser W256
wordField Object
x Key
f = ((W256 -> String -> W256
forall a. Read a => a -> String -> a
readNull W256
0) (String -> W256) -> (Text -> String) -> Text -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack)
                  (Text -> W256) -> Parser Text -> Parser W256
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Object
x Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
f)

instance ParseField W256
instance ParseFields W256
instance ParseRecord W256 where
  parseRecord :: Parser W256
parseRecord = (Only W256 -> W256) -> Parser (Only W256) -> Parser W256
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Only W256 -> W256
forall a. Only a -> a
getOnly Parser (Only W256)
forall a. ParseRecord a => Parser a
parseRecord


-- Word64 wrapper ----------------------------------------------------------------------------------


newtype W64 = W64 Data.Word.Word64
  deriving
    ( Integer -> W64
W64 -> W64
W64 -> W64 -> W64
(W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64)
-> (W64 -> W64)
-> (W64 -> W64)
-> (Integer -> W64)
-> Num W64
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: W64 -> W64 -> W64
+ :: W64 -> W64 -> W64
$c- :: W64 -> W64 -> W64
- :: W64 -> W64 -> W64
$c* :: W64 -> W64 -> W64
* :: W64 -> W64 -> W64
$cnegate :: W64 -> W64
negate :: W64 -> W64
$cabs :: W64 -> W64
abs :: W64 -> W64
$csignum :: W64 -> W64
signum :: W64 -> W64
$cfromInteger :: Integer -> W64
fromInteger :: Integer -> W64
Num, Enum W64
Real W64
Real W64
-> Enum W64
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> (W64, W64))
-> (W64 -> W64 -> (W64, W64))
-> (W64 -> Integer)
-> Integral W64
W64 -> Integer
W64 -> W64 -> (W64, W64)
W64 -> W64 -> W64
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: W64 -> W64 -> W64
quot :: W64 -> W64 -> W64
$crem :: W64 -> W64 -> W64
rem :: W64 -> W64 -> W64
$cdiv :: W64 -> W64 -> W64
div :: W64 -> W64 -> W64
$cmod :: W64 -> W64 -> W64
mod :: W64 -> W64 -> W64
$cquotRem :: W64 -> W64 -> (W64, W64)
quotRem :: W64 -> W64 -> (W64, W64)
$cdivMod :: W64 -> W64 -> (W64, W64)
divMod :: W64 -> W64 -> (W64, W64)
$ctoInteger :: W64 -> Integer
toInteger :: W64 -> Integer
Integral, Num W64
Ord W64
Num W64 -> Ord W64 -> (W64 -> Rational) -> Real W64
W64 -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
$ctoRational :: W64 -> Rational
toRational :: W64 -> Rational
Real, Eq W64
Eq W64
-> (W64 -> W64 -> Ordering)
-> (W64 -> W64 -> Bool)
-> (W64 -> W64 -> Bool)
-> (W64 -> W64 -> Bool)
-> (W64 -> W64 -> Bool)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> Ord W64
W64 -> W64 -> Bool
W64 -> W64 -> Ordering
W64 -> W64 -> W64
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: W64 -> W64 -> Ordering
compare :: W64 -> W64 -> Ordering
$c< :: W64 -> W64 -> Bool
< :: W64 -> W64 -> Bool
$c<= :: W64 -> W64 -> Bool
<= :: W64 -> W64 -> Bool
$c> :: W64 -> W64 -> Bool
> :: W64 -> W64 -> Bool
$c>= :: W64 -> W64 -> Bool
>= :: W64 -> W64 -> Bool
$cmax :: W64 -> W64 -> W64
max :: W64 -> W64 -> W64
$cmin :: W64 -> W64 -> W64
min :: W64 -> W64 -> W64
Ord, (forall x. W64 -> Rep W64 x)
-> (forall x. Rep W64 x -> W64) -> Generic W64
forall x. Rep W64 x -> W64
forall x. W64 -> Rep W64 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. W64 -> Rep W64 x
from :: forall x. W64 -> Rep W64 x
$cto :: forall x. Rep W64 x -> W64
to :: forall x. Rep W64 x -> W64
Generic
    , Eq W64
W64
Eq W64
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64 -> W64)
-> (W64 -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> W64
-> (Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> Bool)
-> (W64 -> Maybe Int)
-> (W64 -> Int)
-> (W64 -> Bool)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int -> W64)
-> (W64 -> Int)
-> Bits W64
Int -> W64
W64 -> Bool
W64 -> Int
W64 -> Maybe Int
W64 -> W64
W64 -> Int -> Bool
W64 -> Int -> W64
W64 -> W64 -> W64
forall a.
Eq a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
$c.&. :: W64 -> W64 -> W64
.&. :: W64 -> W64 -> W64
$c.|. :: W64 -> W64 -> W64
.|. :: W64 -> W64 -> W64
$cxor :: W64 -> W64 -> W64
xor :: W64 -> W64 -> W64
$ccomplement :: W64 -> W64
complement :: W64 -> W64
$cshift :: W64 -> Int -> W64
shift :: W64 -> Int -> W64
$crotate :: W64 -> Int -> W64
rotate :: W64 -> Int -> W64
$czeroBits :: W64
zeroBits :: W64
$cbit :: Int -> W64
bit :: Int -> W64
$csetBit :: W64 -> Int -> W64
setBit :: W64 -> Int -> W64
$cclearBit :: W64 -> Int -> W64
clearBit :: W64 -> Int -> W64
$ccomplementBit :: W64 -> Int -> W64
complementBit :: W64 -> Int -> W64
$ctestBit :: W64 -> Int -> Bool
testBit :: W64 -> Int -> Bool
$cbitSizeMaybe :: W64 -> Maybe Int
bitSizeMaybe :: W64 -> Maybe Int
$cbitSize :: W64 -> Int
bitSize :: W64 -> Int
$cisSigned :: W64 -> Bool
isSigned :: W64 -> Bool
$cshiftL :: W64 -> Int -> W64
shiftL :: W64 -> Int -> W64
$cunsafeShiftL :: W64 -> Int -> W64
unsafeShiftL :: W64 -> Int -> W64
$cshiftR :: W64 -> Int -> W64
shiftR :: W64 -> Int -> W64
$cunsafeShiftR :: W64 -> Int -> W64
unsafeShiftR :: W64 -> Int -> W64
$crotateL :: W64 -> Int -> W64
rotateL :: W64 -> Int -> W64
$crotateR :: W64 -> Int -> W64
rotateR :: W64 -> Int -> W64
$cpopCount :: W64 -> Int
popCount :: W64 -> Int
Bits , Bits W64
Bits W64
-> (W64 -> Int) -> (W64 -> Int) -> (W64 -> Int) -> FiniteBits W64
W64 -> Int
forall b.
Bits b -> (b -> Int) -> (b -> Int) -> (b -> Int) -> FiniteBits b
$cfiniteBitSize :: W64 -> Int
finiteBitSize :: W64 -> Int
$ccountLeadingZeros :: W64 -> Int
countLeadingZeros :: W64 -> Int
$ccountTrailingZeros :: W64 -> Int
countTrailingZeros :: W64 -> Int
FiniteBits, Int -> W64
W64 -> Int
W64 -> [W64]
W64 -> W64
W64 -> W64 -> [W64]
W64 -> W64 -> W64 -> [W64]
(W64 -> W64)
-> (W64 -> W64)
-> (Int -> W64)
-> (W64 -> Int)
-> (W64 -> [W64])
-> (W64 -> W64 -> [W64])
-> (W64 -> W64 -> [W64])
-> (W64 -> W64 -> W64 -> [W64])
-> Enum W64
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: W64 -> W64
succ :: W64 -> W64
$cpred :: W64 -> W64
pred :: W64 -> W64
$ctoEnum :: Int -> W64
toEnum :: Int -> W64
$cfromEnum :: W64 -> Int
fromEnum :: W64 -> Int
$cenumFrom :: W64 -> [W64]
enumFrom :: W64 -> [W64]
$cenumFromThen :: W64 -> W64 -> [W64]
enumFromThen :: W64 -> W64 -> [W64]
$cenumFromTo :: W64 -> W64 -> [W64]
enumFromTo :: W64 -> W64 -> [W64]
$cenumFromThenTo :: W64 -> W64 -> W64 -> [W64]
enumFromThenTo :: W64 -> W64 -> W64 -> [W64]
Enum, W64 -> W64 -> Bool
(W64 -> W64 -> Bool) -> (W64 -> W64 -> Bool) -> Eq W64
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: W64 -> W64 -> Bool
== :: W64 -> W64 -> Bool
$c/= :: W64 -> W64 -> Bool
/= :: W64 -> W64 -> Bool
Eq , W64
W64 -> W64 -> Bounded W64
forall a. a -> a -> Bounded a
$cminBound :: W64
minBound :: W64
$cmaxBound :: W64
maxBound :: W64
Bounded
    )

instance Read W64 where
  readsPrec :: Int -> ReadS W64
readsPrec Int
_ String
"0x" = [(W64
0, String
"")]
  readsPrec Int
n String
s = (Word64 -> W64) -> (Word64, String) -> (W64, String)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Word64 -> W64
W64 ((Word64, String) -> (W64, String))
-> [(Word64, String)] -> [(W64, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReadS Word64
forall a. Read a => Int -> ReadS a
readsPrec Int
n String
s

instance Show W64 where
  showsPrec :: Int -> W64 -> ShowS
showsPrec Int
_ W64
s = (String
"0x" ++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W64 -> ShowS
forall a. Integral a => a -> ShowS
showHex W64
s

instance JSON.ToJSON W64 where
  toJSON :: W64 -> Value
toJSON W64
x = Text -> Value
JSON.String  (Text -> Value) -> Text -> Value
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ W64 -> String
forall a. Show a => a -> String
show W64
x

instance FromJSON W64 where
  parseJSON :: Value -> Parser W64
parseJSON Value
v = do
    String
s <- Text -> String
T.unpack (Text -> String) -> Parser Text -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Text
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case ReadS W64
forall a. Read a => ReadS a
reads String
s of
      [(W64
x, String
"")]  -> W64 -> Parser W64
forall a. a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return W64
x
      [(W64, String)]
_          -> String -> Parser W64
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser W64) -> String -> Parser W64
forall a b. (a -> b) -> a -> b
$ String
"invalid hex word (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"


word64Field :: JSON.Object -> Key -> JSON.Parser Word64
word64Field :: Object -> Key -> Parser Word64
word64Field Object
x Key
f = ((Word64 -> String -> Word64
forall a. Read a => a -> String -> a
readNull Word64
0) (String -> Word64) -> (Text -> String) -> Text -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack)
                  (Text -> Word64) -> Parser Text -> Parser Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Object
x Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
f)


-- Addresses ---------------------------------------------------------------------------------------


newtype Addr = Addr { Addr -> Word160
addressWord160 :: Word160 }
  deriving
    ( Integer -> Addr
Addr -> Addr
Addr -> Addr -> Addr
(Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr)
-> (Addr -> Addr)
-> (Addr -> Addr)
-> (Integer -> Addr)
-> Num Addr
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Addr -> Addr -> Addr
+ :: Addr -> Addr -> Addr
$c- :: Addr -> Addr -> Addr
- :: Addr -> Addr -> Addr
$c* :: Addr -> Addr -> Addr
* :: Addr -> Addr -> Addr
$cnegate :: Addr -> Addr
negate :: Addr -> Addr
$cabs :: Addr -> Addr
abs :: Addr -> Addr
$csignum :: Addr -> Addr
signum :: Addr -> Addr
$cfromInteger :: Integer -> Addr
fromInteger :: Integer -> Addr
Num, Enum Addr
Real Addr
Real Addr
-> Enum Addr
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> (Addr, Addr))
-> (Addr -> Addr -> (Addr, Addr))
-> (Addr -> Integer)
-> Integral Addr
Addr -> Integer
Addr -> Addr -> (Addr, Addr)
Addr -> Addr -> Addr
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: Addr -> Addr -> Addr
quot :: Addr -> Addr -> Addr
$crem :: Addr -> Addr -> Addr
rem :: Addr -> Addr -> Addr
$cdiv :: Addr -> Addr -> Addr
div :: Addr -> Addr -> Addr
$cmod :: Addr -> Addr -> Addr
mod :: Addr -> Addr -> Addr
$cquotRem :: Addr -> Addr -> (Addr, Addr)
quotRem :: Addr -> Addr -> (Addr, Addr)
$cdivMod :: Addr -> Addr -> (Addr, Addr)
divMod :: Addr -> Addr -> (Addr, Addr)
$ctoInteger :: Addr -> Integer
toInteger :: Addr -> Integer
Integral, Num Addr
Ord Addr
Num Addr -> Ord Addr -> (Addr -> Rational) -> Real Addr
Addr -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
$ctoRational :: Addr -> Rational
toRational :: Addr -> Rational
Real, Eq Addr
Eq Addr
-> (Addr -> Addr -> Ordering)
-> (Addr -> Addr -> Bool)
-> (Addr -> Addr -> Bool)
-> (Addr -> Addr -> Bool)
-> (Addr -> Addr -> Bool)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> Ord Addr
Addr -> Addr -> Bool
Addr -> Addr -> Ordering
Addr -> Addr -> Addr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Addr -> Addr -> Ordering
compare :: Addr -> Addr -> Ordering
$c< :: Addr -> Addr -> Bool
< :: Addr -> Addr -> Bool
$c<= :: Addr -> Addr -> Bool
<= :: Addr -> Addr -> Bool
$c> :: Addr -> Addr -> Bool
> :: Addr -> Addr -> Bool
$c>= :: Addr -> Addr -> Bool
>= :: Addr -> Addr -> Bool
$cmax :: Addr -> Addr -> Addr
max :: Addr -> Addr -> Addr
$cmin :: Addr -> Addr -> Addr
min :: Addr -> Addr -> Addr
Ord, Int -> Addr
Addr -> Int
Addr -> [Addr]
Addr -> Addr
Addr -> Addr -> [Addr]
Addr -> Addr -> Addr -> [Addr]
(Addr -> Addr)
-> (Addr -> Addr)
-> (Int -> Addr)
-> (Addr -> Int)
-> (Addr -> [Addr])
-> (Addr -> Addr -> [Addr])
-> (Addr -> Addr -> [Addr])
-> (Addr -> Addr -> Addr -> [Addr])
-> Enum Addr
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Addr -> Addr
succ :: Addr -> Addr
$cpred :: Addr -> Addr
pred :: Addr -> Addr
$ctoEnum :: Int -> Addr
toEnum :: Int -> Addr
$cfromEnum :: Addr -> Int
fromEnum :: Addr -> Int
$cenumFrom :: Addr -> [Addr]
enumFrom :: Addr -> [Addr]
$cenumFromThen :: Addr -> Addr -> [Addr]
enumFromThen :: Addr -> Addr -> [Addr]
$cenumFromTo :: Addr -> Addr -> [Addr]
enumFromTo :: Addr -> Addr -> [Addr]
$cenumFromThenTo :: Addr -> Addr -> Addr -> [Addr]
enumFromThenTo :: Addr -> Addr -> Addr -> [Addr]
Enum
    , Addr -> Addr -> Bool
(Addr -> Addr -> Bool) -> (Addr -> Addr -> Bool) -> Eq Addr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Addr -> Addr -> Bool
== :: Addr -> Addr -> Bool
$c/= :: Addr -> Addr -> Bool
/= :: Addr -> Addr -> Bool
Eq, (forall x. Addr -> Rep Addr x)
-> (forall x. Rep Addr x -> Addr) -> Generic Addr
forall x. Rep Addr x -> Addr
forall x. Addr -> Rep Addr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Addr -> Rep Addr x
from :: forall x. Addr -> Rep Addr x
$cto :: forall x. Rep Addr x -> Addr
to :: forall x. Rep Addr x -> Addr
Generic, Eq Addr
Addr
Eq Addr
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr -> Addr)
-> (Addr -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> Addr
-> (Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Bool)
-> (Addr -> Maybe Int)
-> (Addr -> Int)
-> (Addr -> Bool)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int -> Addr)
-> (Addr -> Int)
-> Bits Addr
Int -> Addr
Addr -> Bool
Addr -> Int
Addr -> Maybe Int
Addr -> Addr
Addr -> Int -> Bool
Addr -> Int -> Addr
Addr -> Addr -> Addr
forall a.
Eq a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> a
-> (Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> Bool)
-> (a -> Maybe Int)
-> (a -> Int)
-> (a -> Bool)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int -> a)
-> (a -> Int)
-> Bits a
$c.&. :: Addr -> Addr -> Addr
.&. :: Addr -> Addr -> Addr
$c.|. :: Addr -> Addr -> Addr
.|. :: Addr -> Addr -> Addr
$cxor :: Addr -> Addr -> Addr
xor :: Addr -> Addr -> Addr
$ccomplement :: Addr -> Addr
complement :: Addr -> Addr
$cshift :: Addr -> Int -> Addr
shift :: Addr -> Int -> Addr
$crotate :: Addr -> Int -> Addr
rotate :: Addr -> Int -> Addr
$czeroBits :: Addr
zeroBits :: Addr
$cbit :: Int -> Addr
bit :: Int -> Addr
$csetBit :: Addr -> Int -> Addr
setBit :: Addr -> Int -> Addr
$cclearBit :: Addr -> Int -> Addr
clearBit :: Addr -> Int -> Addr
$ccomplementBit :: Addr -> Int -> Addr
complementBit :: Addr -> Int -> Addr
$ctestBit :: Addr -> Int -> Bool
testBit :: Addr -> Int -> Bool
$cbitSizeMaybe :: Addr -> Maybe Int
bitSizeMaybe :: Addr -> Maybe Int
$cbitSize :: Addr -> Int
bitSize :: Addr -> Int
$cisSigned :: Addr -> Bool
isSigned :: Addr -> Bool
$cshiftL :: Addr -> Int -> Addr
shiftL :: Addr -> Int -> Addr
$cunsafeShiftL :: Addr -> Int -> Addr
unsafeShiftL :: Addr -> Int -> Addr
$cshiftR :: Addr -> Int -> Addr
shiftR :: Addr -> Int -> Addr
$cunsafeShiftR :: Addr -> Int -> Addr
unsafeShiftR :: Addr -> Int -> Addr
$crotateL :: Addr -> Int -> Addr
rotateL :: Addr -> Int -> Addr
$crotateR :: Addr -> Int -> Addr
rotateR :: Addr -> Int -> Addr
$cpopCount :: Addr -> Int
popCount :: Addr -> Int
Bits, Bits Addr
Bits Addr
-> (Addr -> Int)
-> (Addr -> Int)
-> (Addr -> Int)
-> FiniteBits Addr
Addr -> Int
forall b.
Bits b -> (b -> Int) -> (b -> Int) -> (b -> Int) -> FiniteBits b
$cfiniteBitSize :: Addr -> Int
finiteBitSize :: Addr -> Int
$ccountLeadingZeros :: Addr -> Int
countLeadingZeros :: Addr -> Int
$ccountTrailingZeros :: Addr -> Int
countTrailingZeros :: Addr -> Int
FiniteBits
    )

instance Read Addr where
  readsPrec :: Int -> ReadS Addr
readsPrec Int
_ (Char
'0':Char
'x':String
s) = ReadS Addr
forall a. (Eq a, Num a) => ReadS a
readHex String
s
  readsPrec Int
_ String
s = ReadS Addr
forall a. (Eq a, Num a) => ReadS a
readHex String
s

instance Show Addr where
  showsPrec :: Int -> Addr -> ShowS
showsPrec Int
_ Addr
addr String
next =
    let hex :: String
hex = Addr -> ShowS
forall a. Integral a => a -> ShowS
showHex Addr
addr String
next
        str :: String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
40 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hex) Char
'0' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hex
    in String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
toChecksumAddress String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
40 String
str

-- https://eips.ethereum.org/EIPS/eip-55
toChecksumAddress :: String -> String
toChecksumAddress :: ShowS
toChecksumAddress String
addr = (Nibble -> Char -> Char) -> [Nibble] -> ShowS
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nibble -> Char -> Char
forall {a}. (Ord a, Num a) => a -> Char -> Char
transform [Nibble]
nibbles String
addr
  where
    nibbles :: [Nibble]
nibbles = ByteString -> [Nibble]
unpackNibbles (ByteString -> [Nibble])
-> (ByteString -> ByteString) -> ByteString -> [Nibble]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ByteString -> ByteString
BS.take Int
20 (ByteString -> [Nibble]) -> ByteString -> [Nibble]
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
keccakBytes (String -> ByteString
Char8.pack String
addr)
    transform :: a -> Char -> Char
transform a
nibble = if a
nibble a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
8 then Char -> Char
toUpper else Char -> Char
forall a. a -> a
id

instance JSON.ToJSON Addr where
  toJSON :: Addr -> Value
toJSON = Text -> Value
JSON.String (Text -> Value) -> (Addr -> Text) -> Addr -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Text) -> (Addr -> String) -> Addr -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> String
forall a. Show a => a -> String
show

instance FromJSON Addr where
  parseJSON :: Value -> Parser Addr
parseJSON Value
v = do
    String
s <- Text -> String
T.unpack (Text -> String) -> Parser Text -> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Text
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
    case ReadS Addr
forall a. Read a => ReadS a
reads String
s of
      [(Addr
x, String
"")] -> Addr -> Parser Addr
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Addr
x
      [(Addr, String)]
_         -> String -> Parser Addr
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser Addr) -> String -> Parser Addr
forall a b. (a -> b) -> a -> b
$ String
"invalid address (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance JSON.ToJSONKey Addr where
  toJSONKey :: ToJSONKeyFunction Addr
toJSONKey = (Addr -> Text) -> ToJSONKeyFunction Addr
forall a. (a -> Text) -> ToJSONKeyFunction a
JSON.toJSONKeyText (Addr -> Text
addrKey)
    where
      addrKey :: Addr -> Text
      addrKey :: Addr -> Text
addrKey Addr
addr = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
40 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hex) Char
'0' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hex
        where
          hex :: String
hex = Addr -> String
forall a. Show a => a -> String
show Addr
addr

instance FromJSONKey Addr where
  fromJSONKey :: FromJSONKeyFunction Addr
fromJSONKey = (Text -> Parser Addr) -> FromJSONKeyFunction Addr
forall a. (Text -> Parser a) -> FromJSONKeyFunction a
FromJSONKeyTextParser ((Text -> Parser Addr) -> FromJSONKeyFunction Addr)
-> (Text -> Parser Addr) -> FromJSONKeyFunction Addr
forall a b. (a -> b) -> a -> b
$ \Text
s ->
    case ReadS Addr
forall a. Read a => ReadS a
reads (Text -> String
T.unpack Text
s) of
      [(Addr
x, String
"")] -> Addr -> Parser Addr
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Addr
x
      [(Addr, String)]
_         -> String -> Parser Addr
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser Addr) -> String -> Parser Addr
forall a b. (a -> b) -> a -> b
$ String
"invalid word (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

addrField :: JSON.Object -> Key -> JSON.Parser Addr
addrField :: Object -> Key -> Parser Addr
addrField Object
x Key
f = (String -> Addr
forall a. Read a => String -> a
read (String -> Addr) -> (Text -> String) -> Text -> Addr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) (Text -> Addr) -> Parser Text -> Parser Addr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Object
x Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
f)

addrFieldMaybe :: JSON.Object -> Key -> JSON.Parser (Maybe Addr)
addrFieldMaybe :: Object -> Key -> Parser (Maybe Addr)
addrFieldMaybe Object
x Key
f = (String -> Maybe Addr
forall a. Read a => String -> Maybe a
Text.Read.readMaybe (String -> Maybe Addr) -> (Text -> String) -> Text -> Maybe Addr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) (Text -> Maybe Addr) -> Parser Text -> Parser (Maybe Addr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Object
x Object -> Key -> Parser Text
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
f)

instance ParseField Addr
instance ParseFields Addr
instance ParseRecord Addr where
  parseRecord :: Parser Addr
parseRecord = (Only Addr -> Addr) -> Parser (Only Addr) -> Parser Addr
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Only Addr -> Addr
forall a. Only a -> a
getOnly Parser (Only Addr)
forall a. ParseRecord a => Parser a
parseRecord


-- Nibbles -----------------------------------------------------------------------------------------


-- | A four bit value
newtype Nibble = Nibble Word8
  deriving (Integer -> Nibble
Nibble -> Nibble
Nibble -> Nibble -> Nibble
(Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble)
-> (Nibble -> Nibble)
-> (Nibble -> Nibble)
-> (Integer -> Nibble)
-> Num Nibble
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Nibble -> Nibble -> Nibble
+ :: Nibble -> Nibble -> Nibble
$c- :: Nibble -> Nibble -> Nibble
- :: Nibble -> Nibble -> Nibble
$c* :: Nibble -> Nibble -> Nibble
* :: Nibble -> Nibble -> Nibble
$cnegate :: Nibble -> Nibble
negate :: Nibble -> Nibble
$cabs :: Nibble -> Nibble
abs :: Nibble -> Nibble
$csignum :: Nibble -> Nibble
signum :: Nibble -> Nibble
$cfromInteger :: Integer -> Nibble
fromInteger :: Integer -> Nibble
Num, Enum Nibble
Real Nibble
Real Nibble
-> Enum Nibble
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> (Nibble, Nibble))
-> (Nibble -> Nibble -> (Nibble, Nibble))
-> (Nibble -> Integer)
-> Integral Nibble
Nibble -> Integer
Nibble -> Nibble -> (Nibble, Nibble)
Nibble -> Nibble -> Nibble
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: Nibble -> Nibble -> Nibble
quot :: Nibble -> Nibble -> Nibble
$crem :: Nibble -> Nibble -> Nibble
rem :: Nibble -> Nibble -> Nibble
$cdiv :: Nibble -> Nibble -> Nibble
div :: Nibble -> Nibble -> Nibble
$cmod :: Nibble -> Nibble -> Nibble
mod :: Nibble -> Nibble -> Nibble
$cquotRem :: Nibble -> Nibble -> (Nibble, Nibble)
quotRem :: Nibble -> Nibble -> (Nibble, Nibble)
$cdivMod :: Nibble -> Nibble -> (Nibble, Nibble)
divMod :: Nibble -> Nibble -> (Nibble, Nibble)
$ctoInteger :: Nibble -> Integer
toInteger :: Nibble -> Integer
Integral, Num Nibble
Ord Nibble
Num Nibble -> Ord Nibble -> (Nibble -> Rational) -> Real Nibble
Nibble -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
$ctoRational :: Nibble -> Rational
toRational :: Nibble -> Rational
Real, Eq Nibble
Eq Nibble
-> (Nibble -> Nibble -> Ordering)
-> (Nibble -> Nibble -> Bool)
-> (Nibble -> Nibble -> Bool)
-> (Nibble -> Nibble -> Bool)
-> (Nibble -> Nibble -> Bool)
-> (Nibble -> Nibble -> Nibble)
-> (Nibble -> Nibble -> Nibble)
-> Ord Nibble
Nibble -> Nibble -> Bool
Nibble -> Nibble -> Ordering
Nibble -> Nibble -> Nibble
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Nibble -> Nibble -> Ordering
compare :: Nibble -> Nibble -> Ordering
$c< :: Nibble -> Nibble -> Bool
< :: Nibble -> Nibble -> Bool
$c<= :: Nibble -> Nibble -> Bool
<= :: Nibble -> Nibble -> Bool
$c> :: Nibble -> Nibble -> Bool
> :: Nibble -> Nibble -> Bool
$c>= :: Nibble -> Nibble -> Bool
>= :: Nibble -> Nibble -> Bool
$cmax :: Nibble -> Nibble -> Nibble
max :: Nibble -> Nibble -> Nibble
$cmin :: Nibble -> Nibble -> Nibble
min :: Nibble -> Nibble -> Nibble
Ord, Int -> Nibble
Nibble -> Int
Nibble -> [Nibble]
Nibble -> Nibble
Nibble -> Nibble -> [Nibble]
Nibble -> Nibble -> Nibble -> [Nibble]
(Nibble -> Nibble)
-> (Nibble -> Nibble)
-> (Int -> Nibble)
-> (Nibble -> Int)
-> (Nibble -> [Nibble])
-> (Nibble -> Nibble -> [Nibble])
-> (Nibble -> Nibble -> [Nibble])
-> (Nibble -> Nibble -> Nibble -> [Nibble])
-> Enum Nibble
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Nibble -> Nibble
succ :: Nibble -> Nibble
$cpred :: Nibble -> Nibble
pred :: Nibble -> Nibble
$ctoEnum :: Int -> Nibble
toEnum :: Int -> Nibble
$cfromEnum :: Nibble -> Int
fromEnum :: Nibble -> Int
$cenumFrom :: Nibble -> [Nibble]
enumFrom :: Nibble -> [Nibble]
$cenumFromThen :: Nibble -> Nibble -> [Nibble]
enumFromThen :: Nibble -> Nibble -> [Nibble]
$cenumFromTo :: Nibble -> Nibble -> [Nibble]
enumFromTo :: Nibble -> Nibble -> [Nibble]
$cenumFromThenTo :: Nibble -> Nibble -> Nibble -> [Nibble]
enumFromThenTo :: Nibble -> Nibble -> Nibble -> [Nibble]
Enum, Nibble -> Nibble -> Bool
(Nibble -> Nibble -> Bool)
-> (Nibble -> Nibble -> Bool) -> Eq Nibble
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nibble -> Nibble -> Bool
== :: Nibble -> Nibble -> Bool
$c/= :: Nibble -> Nibble -> Bool
/= :: Nibble -> Nibble -> Bool
Eq, Nibble
Nibble -> Nibble -> Bounded Nibble
forall a. a -> a -> Bounded a
$cminBound :: Nibble
minBound :: Nibble
$cmaxBound :: Nibble
maxBound :: Nibble
Bounded, (forall x. Nibble -> Rep Nibble x)
-> (forall x. Rep Nibble x -> Nibble) -> Generic Nibble
forall x. Rep Nibble x -> Nibble
forall x. Nibble -> Rep Nibble x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Nibble -> Rep Nibble x
from :: forall x. Nibble -> Rep Nibble x
$cto :: forall x. Rep Nibble x -> Nibble
to :: forall x. Rep Nibble x -> Nibble
Generic)

instance Show Nibble where
  show :: Nibble -> String
show = (Char -> ShowS
forall a. a -> [a] -> [a]
:[]) (Char -> String) -> (Nibble -> Char) -> Nibble -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
intToDigit (Int -> Char) -> (Nibble -> Int) -> Nibble -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nibble -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral


-- Conversions -------------------------------------------------------------------------------------


toWord512 :: W256 -> Word512
toWord512 :: W256 -> Word512
toWord512 (W256 Word256
x) = HiWord Word512 -> LoWord Word512 -> Word512
forall w. DoubleWord w => HiWord w -> LoWord w -> w
fromHiAndLo HiWord Word512
Word256
0 LoWord Word512
Word256
x

fromWord512 :: Word512 -> W256
fromWord512 :: Word512 -> W256
fromWord512 Word512
x = Word256 -> W256
W256 (Word512 -> LoWord Word512
forall w. DoubleWord w => w -> LoWord w
loWord Word512
x)

maybeLitByte :: Expr Byte -> Maybe Word8
maybeLitByte :: Expr 'Byte -> Maybe Word8
maybeLitByte (LitByte Word8
x) = Word8 -> Maybe Word8
forall a. a -> Maybe a
Just Word8
x
maybeLitByte Expr 'Byte
_ = Maybe Word8
forall a. Maybe a
Nothing

maybeLitWord :: Expr EWord -> Maybe W256
maybeLitWord :: Expr 'EWord -> Maybe W256
maybeLitWord (Lit W256
w) = W256 -> Maybe W256
forall a. a -> Maybe a
Just W256
w
maybeLitWord (WAddr (LitAddr Addr
w)) = W256 -> Maybe W256
forall a. a -> Maybe a
Just (Addr -> W256
forall target source. From source target => source -> target
into Addr
w)
maybeLitWord Expr 'EWord
_ = Maybe W256
forall a. Maybe a
Nothing

maybeLitAddr :: Expr EAddr -> Maybe Addr
maybeLitAddr :: Expr 'EAddr -> Maybe Addr
maybeLitAddr (LitAddr Addr
a) = Addr -> Maybe Addr
forall a. a -> Maybe a
Just Addr
a
maybeLitAddr Expr 'EAddr
_ = Maybe Addr
forall a. Maybe a
Nothing

maybeConcreteStore :: Expr Storage -> Maybe (Map W256 W256)
maybeConcreteStore :: Expr 'Storage -> Maybe (Map W256 W256)
maybeConcreteStore (ConcreteStore Map W256 W256
s) = Map W256 W256 -> Maybe (Map W256 W256)
forall a. a -> Maybe a
Just Map W256 W256
s
maybeConcreteStore Expr 'Storage
_ = Maybe (Map W256 W256)
forall a. Maybe a
Nothing


word256 :: ByteString -> Word256
word256 :: ByteString -> Word256
word256 ByteString
xs | ByteString -> Int
BS.length ByteString
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 =
  -- optimize one byte pushes
  Word128 -> Word128 -> Word256
Word256 (Word64 -> Word64 -> Word128
Word128 Word64
0 Word64
0) (Word64 -> Word64 -> Word128
Word128 Word64
0 (Word8 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word8 -> Word64) -> Word8 -> Word64
forall a b. (a -> b) -> a -> b
$ HasCallStack => ByteString -> Word8
ByteString -> Word8
BS.head ByteString
xs))
word256 ByteString
xs = case Get Word256 -> ByteString -> Either String Word256
forall a. Get a -> ByteString -> Either String a
Cereal.runGet Get Word256
m (Int -> ByteString -> ByteString
padLeft Int
32 ByteString
xs) of
               Left String
_ -> String -> Word256
forall a. HasCallStack => String -> a
internalError String
"should not happen"
               Right Word256
x -> Word256
x
  where
    m :: Get Word256
m = do Word64
a <- Get Word64
Cereal.getWord64be
           Word64
b <- Get Word64
Cereal.getWord64be
           Word64
c <- Get Word64
Cereal.getWord64be
           Word64
d <- Get Word64
Cereal.getWord64be
           Word256 -> Get Word256
forall a. a -> Get a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word256 -> Get Word256) -> Word256 -> Get Word256
forall a b. (a -> b) -> a -> b
$ Word128 -> Word128 -> Word256
Word256 (Word64 -> Word64 -> Word128
Word128 Word64
a Word64
b) (Word64 -> Word64 -> Word128
Word128 Word64
c Word64
d)

word :: ByteString -> W256
word :: ByteString -> W256
word = Word256 -> W256
W256 (Word256 -> W256) -> (ByteString -> Word256) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Word256
word256

fromBE :: (Integral a) => ByteString -> a
fromBE :: forall a. Integral a => ByteString -> a
fromBE ByteString
xs = if ByteString
xs ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
forall a. Monoid a => a
mempty then a
0
  else a
256 a -> a -> a
forall a. Num a => a -> a -> a
* ByteString -> a
forall a. Integral a => ByteString -> a
fromBE (HasCallStack => ByteString -> ByteString
ByteString -> ByteString
BS.init ByteString
xs)
       a -> a -> a
forall a. Num a => a -> a -> a
+ (Word8 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word8 -> a) -> Word8 -> a
forall a b. (a -> b) -> a -> b
$ HasCallStack => ByteString -> Word8
ByteString -> Word8
BS.last ByteString
xs)

asBE :: (Integral a) => a -> ByteString
asBE :: forall a. Integral a => a -> ByteString
asBE a
0 = ByteString
forall a. Monoid a => a
mempty
asBE a
x = a -> ByteString
forall a. Integral a => a -> ByteString
asBE (a
x a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
256)
  ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [Word8] -> ByteString
BS.pack [a -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Word8) -> a -> Word8
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
256]

word256Bytes :: W256 -> ByteString
word256Bytes :: W256 -> ByteString
word256Bytes (W256 (Word256 (Word128 Word64
a Word64
b) (Word128 Word64
c Word64
d))) =
  Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
a ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
b ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
c ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
d

word160Bytes :: Addr -> ByteString
word160Bytes :: Addr -> ByteString
word160Bytes (Addr (Word160 Word32
a (Word128 Word64
b Word64
c))) =
  Word32 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word32
a ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
b ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word64 -> ByteString
forall a. Serialize a => a -> ByteString
Cereal.encode Word64
c

-- Get first and second Nibble from byte
hi, lo :: Word8 -> Nibble
hi :: Word8 -> Nibble
hi Word8
b = Word8 -> Nibble
Nibble (Word8 -> Nibble) -> Word8 -> Nibble
forall a b. (a -> b) -> a -> b
$ Word8
b Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
`shiftR` Int
4
lo :: Word8 -> Nibble
lo Word8
b = Word8 -> Nibble
Nibble (Word8 -> Nibble) -> Word8 -> Nibble
forall a b. (a -> b) -> a -> b
$ Word8
b Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.&. Word8
0x0f

toByte :: Nibble -> Nibble -> Word8
toByte :: Nibble -> Nibble -> Word8
toByte  (Nibble Word8
high) (Nibble Word8
low) = Word8
high Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
`shift` Int
4 Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. Word8
low

unpackNibbles :: ByteString -> [Nibble]
unpackNibbles :: ByteString -> [Nibble]
unpackNibbles ByteString
bs = ByteString -> [Word8]
BS.unpack ByteString
bs [Word8] -> (Word8 -> [Nibble]) -> [Nibble]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Word8 -> [Nibble]
unpackByte
  where unpackByte :: Word8 -> [Nibble]
unpackByte Word8
b = [Word8 -> Nibble
hi Word8
b, Word8 -> Nibble
lo Word8
b]

-- Well-defined for even length lists only (plz dependent types)
packNibbles :: [Nibble] -> ByteString
packNibbles :: [Nibble] -> ByteString
packNibbles [] = ByteString
forall a. Monoid a => a
mempty
packNibbles (Nibble
n1:Nibble
n2:[Nibble]
ns) = Word8 -> ByteString
BS.singleton (Nibble -> Nibble -> Word8
toByte Nibble
n1 Nibble
n2) ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [Nibble] -> ByteString
packNibbles [Nibble]
ns
packNibbles [Nibble]
_ = String -> ByteString
forall a. HasCallStack => String -> a
internalError String
"can't pack odd number of nibbles"

toWord64 :: W256 -> Maybe Word64
toWord64 :: W256 -> Maybe Word64
toWord64 W256
n =
  if W256
n W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> W256
forall target source. From source target => source -> target
into (Word64
forall a. Bounded a => a
maxBound :: Word64)
    then let (W256 (Word256 Word128
_ (Word128 Word64
_ Word64
n'))) = W256
n in Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
n'
    else Maybe Word64
forall a. Maybe a
Nothing

toInt :: W256 -> Maybe Int
toInt :: W256 -> Maybe Int
toInt W256
n =
  if W256
n W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int)
    then let (W256 (Word256 Word128
_ (Word128 Word64
_ Word64
n'))) = W256
n in Int -> Maybe Int
forall a. a -> Maybe a
Just (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n')
    else Maybe Int
forall a. Maybe a
Nothing

bssToBs :: ByteStringS -> ByteString
bssToBs :: ByteStringS -> ByteString
bssToBs (ByteStringS ByteString
bs) = ByteString
bs


-- Keccak hashing ----------------------------------------------------------------------------------


keccakBytes :: ByteString -> ByteString
keccakBytes :: ByteString -> ByteString
keccakBytes =
  (ByteString -> Digest Keccak_256
forall ba a.
(ByteArrayAccess ba, HashAlgorithm a) =>
ba -> Digest a
hash :: ByteString -> Digest Keccak_256)
    (ByteString -> Digest Keccak_256)
-> (Digest Keccak_256 -> ByteString) -> ByteString -> ByteString
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Digest Keccak_256 -> ByteString
forall bin bout.
(ByteArrayAccess bin, ByteArray bout) =>
bin -> bout
BA.convert

word32 :: [Word8] -> Word32
word32 :: [Word8] -> Word32
word32 [Word8]
xs = [Word32] -> Word32
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ Word8 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
x Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
`shiftL` (Int
8Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n)
                | (Int
n, Word8
x) <- [Int] -> [Word8] -> [(Int, Word8)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Word8] -> [Word8]
forall a. [a] -> [a]
reverse [Word8]
xs) ]

keccak :: Expr Buf -> Expr EWord
keccak :: Expr 'Buf -> Expr 'EWord
keccak (ConcreteBuf ByteString
bs) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
keccak' ByteString
bs
keccak Expr 'Buf
buf = Expr 'Buf -> Expr 'EWord
Keccak Expr 'Buf
buf

keccak' :: ByteString -> W256
keccak' :: ByteString -> W256
keccak' = ByteString -> ByteString
keccakBytes (ByteString -> ByteString)
-> (ByteString -> W256) -> ByteString -> W256
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString)
-> (ByteString -> W256) -> ByteString -> W256
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ByteString -> W256
word

abiKeccak :: ByteString -> FunctionSelector
abiKeccak :: ByteString -> FunctionSelector
abiKeccak =
  ByteString -> ByteString
keccakBytes
    (ByteString -> ByteString)
-> (ByteString -> FunctionSelector)
-> ByteString
-> FunctionSelector
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Int -> ByteString -> ByteString
BS.take Int
4
    (ByteString -> ByteString)
-> (ByteString -> FunctionSelector)
-> ByteString
-> FunctionSelector
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ByteString -> [Word8]
BS.unpack
    (ByteString -> [Word8])
-> ([Word8] -> FunctionSelector) -> ByteString -> FunctionSelector
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> [Word8] -> Word32
word32
    ([Word8] -> Word32)
-> (Word32 -> FunctionSelector) -> [Word8] -> FunctionSelector
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Word32 -> FunctionSelector
FunctionSelector


-- Utils -------------------------------------------------------------------------------------------

{- HLINT ignore internalError -}
internalError:: HasCallStack => [Char] -> a
internalError :: forall a. HasCallStack => String -> a
internalError String
m = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Internal Error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (CallStack -> String
prettyCallStack CallStack
HasCallStack => CallStack
callStack)

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM :: forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM a -> m [b]
f [a]
xs = ([[b]] -> [b]) -> m [[b]] -> m [b]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((a -> m [b]) -> [a] -> m [[b]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> m [b]
f [a]
xs)

regexMatches :: Text -> Text -> Bool
regexMatches :: Text -> Text -> Bool
regexMatches Text
regexSource =
  let
    compOpts :: CompOption
compOpts =
      CompOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
Regex.defaultCompOpt { lastStarGreedy :: Bool
Regex.lastStarGreedy = Bool
True }
    execOpts :: ExecOption
execOpts =
      ExecOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
Regex.defaultExecOpt { captureGroups :: Bool
Regex.captureGroups = Bool
False }
    regex :: Regex
regex = CompOption -> ExecOption -> String -> Regex
forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
Regex.makeRegexOpts CompOption
compOpts ExecOption
execOpts (Text -> String
T.unpack Text
regexSource)
  in
    Regex -> Seq Char -> Bool
forall regex source.
RegexLike regex source =>
regex -> source -> Bool
Regex.matchTest Regex
regex (Seq Char -> Bool) -> (Text -> Seq Char) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Seq Char
forall a. [a] -> Seq a
Seq.fromList (String -> Seq Char) -> (Text -> String) -> Text -> Seq Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack

readNull :: Read a => a -> String -> a
readNull :: forall a. Read a => a -> String -> a
readNull a
x = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x (Maybe a -> a) -> (String -> Maybe a) -> String -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe a
forall a. Read a => String -> Maybe a
Text.Read.readMaybe

padLeft :: Int -> ByteString -> ByteString
padLeft :: Int -> ByteString -> ByteString
padLeft Int
n ByteString
xs = Int -> Word8 -> ByteString
BS.replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- ByteString -> Int
BS.length ByteString
xs) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
xs

padLeft' :: Int -> V.Vector (Expr Byte) -> V.Vector (Expr Byte)
padLeft' :: Int -> Vector (Expr 'Byte) -> Vector (Expr 'Byte)
padLeft' Int
n Vector (Expr 'Byte)
xs = Int -> Expr 'Byte -> Vector (Expr 'Byte)
forall a. Int -> a -> Vector a
V.replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Vector (Expr 'Byte) -> Int
forall a. Vector a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Vector (Expr 'Byte)
xs) (Word8 -> Expr 'Byte
LitByte Word8
0) Vector (Expr 'Byte) -> Vector (Expr 'Byte) -> Vector (Expr 'Byte)
forall a. Semigroup a => a -> a -> a
<> Vector (Expr 'Byte)
xs

padRight :: Int -> ByteString -> ByteString
padRight :: Int -> ByteString -> ByteString
padRight Int
n ByteString
xs = ByteString
xs ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> Word8 -> ByteString
BS.replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- ByteString -> Int
BS.length ByteString
xs) Word8
0

padRight' :: Int -> String -> String
padRight' :: Int -> ShowS
padRight' Int
n String
xs = String
xs String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs) Char
'0'

-- We need this here instead of Format for cyclic import reasons...
formatString :: ByteString -> String
formatString :: ByteString -> String
formatString ByteString
bs =
  case ByteString -> Either UnicodeException Text
T.decodeUtf8' ((ByteString, ByteString) -> ByteString
forall a b. (a, b) -> a
fst ((Word8 -> Bool) -> ByteString -> (ByteString, ByteString)
BS.spanEnd (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0) ByteString
bs)) of
    Right Text
s -> String
"\"" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
s String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\""
    Left UnicodeException
_ -> String
"❮utf8 decode failed❯: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (ByteStringS -> String
forall a. Show a => a -> String
show (ByteStringS -> String) -> ByteStringS -> String
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteStringS
ByteStringS ByteString
bs)

-- |'paddedShowHex' displays a number in hexadecimal and pads the number
-- with 0 so that it has a minimum length of @w@.
paddedShowHex :: (Show a, Integral a) => Int -> a -> String
paddedShowHex :: forall a. (Show a, Integral a) => Int -> a -> String
paddedShowHex Int
w a
n = String
pad String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
    where
     str :: String
str = a -> ShowS
forall a. Integral a => a -> ShowS
showHex a
n String
""
     pad :: String
pad = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str) Char
'0'

untilFixpoint :: Eq a => (a -> a) -> a -> a
untilFixpoint :: forall a. Eq a => (a -> a) -> a -> a
untilFixpoint a -> a
f a
a = if a -> a
f a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
                    then a
a
                    else (a -> a) -> a -> a
forall a. Eq a => (a -> a) -> a -> a
untilFixpoint a -> a
f (a -> a
f a
a)

-- Optics ------------------------------------------------------------------------------------------


makeFieldLabelsNoPrefix ''VM
makeFieldLabelsNoPrefix ''FrameState
makeFieldLabelsNoPrefix ''TxState
makeFieldLabelsNoPrefix ''SubState
makeFieldLabelsNoPrefix ''Cache
makeFieldLabelsNoPrefix ''Trace
makeFieldLabelsNoPrefix ''VMOpts
makeFieldLabelsNoPrefix ''Frame
makeFieldLabelsNoPrefix ''FrameContext
makeFieldLabelsNoPrefix ''Contract
makeFieldLabelsNoPrefix ''Env
makeFieldLabelsNoPrefix ''Block
makeFieldLabelsNoPrefix ''RuntimeConfig