hevm-0.44.1: Ethereum virtual machine evaluator

Safe HaskellNone
LanguageHaskell2010

EVM.Types

Synopsis

Documentation

data Word512 Source #

Constructors

Word512 !Word256 !Word256 
Instances
Bounded Word512 Source # 
Instance details

Defined in EVM.Types

Enum Word512 Source # 
Instance details

Defined in EVM.Types

Eq Word512 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Word512 -> Word512 -> Bool #

(/=) :: Word512 -> Word512 -> Bool #

Integral Word512 Source # 
Instance details

Defined in EVM.Types

Data Word512 Source # 
Instance details

Defined in EVM.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Word512 -> c Word512 #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Word512 #

toConstr :: Word512 -> Constr #

dataTypeOf :: Word512 -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Word512) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Word512) #

gmapT :: (forall b. Data b => b -> b) -> Word512 -> Word512 #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Word512 -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Word512 -> r #

gmapQ :: (forall d. Data d => d -> u) -> Word512 -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Word512 -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Word512 -> m Word512 #

Num Word512 Source # 
Instance details

Defined in EVM.Types

Ord Word512 Source # 
Instance details

Defined in EVM.Types

Read Word512 Source # 
Instance details

Defined in EVM.Types

Real Word512 Source # 
Instance details

Defined in EVM.Types

Show Word512 Source # 
Instance details

Defined in EVM.Types

Ix Word512 Source # 
Instance details

Defined in EVM.Types

Generic Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Word512 :: Type -> Type #

Methods

from :: Word512 -> Rep Word512 x #

to :: Rep Word512 x -> Word512 #

Hashable Word512 Source # 
Instance details

Defined in EVM.Types

Methods

hashWithSalt :: Int -> Word512 -> Int #

hash :: Word512 -> Int #

Bits Word512 Source # 
Instance details

Defined in EVM.Types

FiniteBits Word512 Source # 
Instance details

Defined in EVM.Types

BinaryWord Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type UnsignedWord Word512 :: Type #

type SignedWord Word512 :: Type #

DoubleWord Word512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type LoWord Word512 :: Type #

type HiWord Word512 :: Type #

type Rep Word512 Source # 
Instance details

Defined in EVM.Types

type SignedWord Word512 Source # 
Instance details

Defined in EVM.Types

type UnsignedWord Word512 Source # 
Instance details

Defined in EVM.Types

type HiWord Word512 Source # 
Instance details

Defined in EVM.Types

type LoWord Word512 Source # 
Instance details

Defined in EVM.Types

data Int512 Source #

Constructors

Int512 !Int256 !Word256 
Instances
Bounded Int512 Source # 
Instance details

Defined in EVM.Types

Enum Int512 Source # 
Instance details

Defined in EVM.Types

Eq Int512 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Int512 -> Int512 -> Bool #

(/=) :: Int512 -> Int512 -> Bool #

Integral Int512 Source # 
Instance details

Defined in EVM.Types

Data Int512 Source # 
Instance details

Defined in EVM.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Int512 -> c Int512 #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Int512 #

toConstr :: Int512 -> Constr #

dataTypeOf :: Int512 -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Int512) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Int512) #

gmapT :: (forall b. Data b => b -> b) -> Int512 -> Int512 #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Int512 -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Int512 -> r #

gmapQ :: (forall d. Data d => d -> u) -> Int512 -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Int512 -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Int512 -> m Int512 #

Num Int512 Source # 
Instance details

Defined in EVM.Types

Ord Int512 Source # 
Instance details

Defined in EVM.Types

Read Int512 Source # 
Instance details

Defined in EVM.Types

Real Int512 Source # 
Instance details

Defined in EVM.Types

Show Int512 Source # 
Instance details

Defined in EVM.Types

Ix Int512 Source # 
Instance details

Defined in EVM.Types

Generic Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Int512 :: Type -> Type #

Methods

from :: Int512 -> Rep Int512 x #

to :: Rep Int512 x -> Int512 #

Hashable Int512 Source # 
Instance details

Defined in EVM.Types

Methods

hashWithSalt :: Int -> Int512 -> Int #

hash :: Int512 -> Int #

Bits Int512 Source # 
Instance details

Defined in EVM.Types

FiniteBits Int512 Source # 
Instance details

Defined in EVM.Types

BinaryWord Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type UnsignedWord Int512 :: Type #

type SignedWord Int512 :: Type #

DoubleWord Int512 Source # 
Instance details

Defined in EVM.Types

Associated Types

type LoWord Int512 :: Type #

type HiWord Int512 :: Type #

type Rep Int512 Source # 
Instance details

Defined in EVM.Types

type SignedWord Int512 Source # 
Instance details

Defined in EVM.Types

type UnsignedWord Int512 Source # 
Instance details

Defined in EVM.Types

type HiWord Int512 Source # 
Instance details

Defined in EVM.Types

type LoWord Int512 Source # 
Instance details

Defined in EVM.Types

data Buffer Source #

Instances
Show Buffer Source #

Operations over buffers (concrete or symbolic)

A buffer is a list of bytes. For concrete execution, this is simply ByteString. In symbolic settings, it is a list of symbolic bitvectors of size 8.

Instance details

Defined in EVM.Types

Semigroup Buffer Source # 
Instance details

Defined in EVM.Types

Monoid Buffer Source # 
Instance details

Defined in EVM.Types

EqSymbolic Buffer Source # 
Instance details

Defined in EVM.Types

SDisplay Buffer Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Buffer -> SExpr Text Source #

newtype W256 Source #

Constructors

W256 Word256 
Instances
Bounded W256 Source # 
Instance details

Defined in EVM.Types

Enum W256 Source # 
Instance details

Defined in EVM.Types

Methods

succ :: W256 -> W256 #

pred :: W256 -> W256 #

toEnum :: Int -> W256 #

fromEnum :: W256 -> Int #

enumFrom :: W256 -> [W256] #

enumFromThen :: W256 -> W256 -> [W256] #

enumFromTo :: W256 -> W256 -> [W256] #

enumFromThenTo :: W256 -> W256 -> W256 -> [W256] #

Eq W256 Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: W256 -> W256 -> Bool #

(/=) :: W256 -> W256 -> Bool #

Integral W256 Source # 
Instance details

Defined in EVM.Types

Methods

quot :: W256 -> W256 -> W256 #

rem :: W256 -> W256 -> W256 #

div :: W256 -> W256 -> W256 #

mod :: W256 -> W256 -> W256 #

quotRem :: W256 -> W256 -> (W256, W256) #

divMod :: W256 -> W256 -> (W256, W256) #

toInteger :: W256 -> Integer #

Num W256 Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: W256 -> W256 -> W256 #

(-) :: W256 -> W256 -> W256 #

(*) :: W256 -> W256 -> W256 #

negate :: W256 -> W256 #

abs :: W256 -> W256 #

signum :: W256 -> W256 #

fromInteger :: Integer -> W256 #

Ord W256 Source # 
Instance details

Defined in EVM.Types

Methods

compare :: W256 -> W256 -> Ordering #

(<) :: W256 -> W256 -> Bool #

(<=) :: W256 -> W256 -> Bool #

(>) :: W256 -> W256 -> Bool #

(>=) :: W256 -> W256 -> Bool #

max :: W256 -> W256 -> W256 #

min :: W256 -> W256 -> W256 #

Read W256 Source # 
Instance details

Defined in EVM.Types

Real W256 Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: W256 -> Rational #

Show W256 Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> W256 -> ShowS #

show :: W256 -> String #

showList :: [W256] -> ShowS #

Generic W256 Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep W256 :: Type -> Type #

Methods

from :: W256 -> Rep W256 x #

to :: Rep W256 x -> W256 #

ToJSON W256 Source # 
Instance details

Defined in EVM.Types

FromJSON W256 Source # 
Instance details

Defined in EVM.Types

FromJSONKey W256 Source # 
Instance details

Defined in EVM.Types

Bits W256 Source # 
Instance details

Defined in EVM.Types

FiniteBits W256 Source # 
Instance details

Defined in EVM.Types

ParseField W256 Source # 
Instance details

Defined in EVM.Types

ParseFields W256 Source # 
Instance details

Defined in EVM.Types

ParseRecord W256 Source # 
Instance details

Defined in EVM.Types

ToSizzleBV W256 Source # 
Instance details

Defined in EVM.Types

ToRPC W256 Source # 
Instance details

Defined in EVM.Fetch

Methods

toRPC :: W256 -> Value Source #

SDisplay W256 Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: W256 -> SExpr Text Source #

type Rep W256 Source # 
Instance details

Defined in EVM.Types

type Rep W256 = D1 (MetaData "W256" "EVM.Types" "hevm-0.44.1-inplace" True) (C1 (MetaCons "W256" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word256)))

data Word Source #

Constructors

C Whiff W256 
Instances
Bounded Word Source # 
Instance details

Defined in EVM.Types

Enum Word Source # 
Instance details

Defined in EVM.Types

Methods

succ :: Word -> Word #

pred :: Word -> Word #

toEnum :: Int -> Word #

fromEnum :: Word -> Int #

enumFrom :: Word -> [Word] #

enumFromThen :: Word -> Word -> [Word] #

enumFromTo :: Word -> Word -> [Word] #

enumFromThenTo :: Word -> Word -> Word -> [Word] #

Eq Word Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Word -> Word -> Bool #

(/=) :: Word -> Word -> Bool #

Integral Word Source # 
Instance details

Defined in EVM.Types

Methods

quot :: Word -> Word -> Word #

rem :: Word -> Word -> Word #

div :: Word -> Word -> Word #

mod :: Word -> Word -> Word #

quotRem :: Word -> Word -> (Word, Word) #

divMod :: Word -> Word -> (Word, Word) #

toInteger :: Word -> Integer #

Num Word Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: Word -> Word -> Word #

(-) :: Word -> Word -> Word #

(*) :: Word -> Word -> Word #

negate :: Word -> Word #

abs :: Word -> Word #

signum :: Word -> Word #

fromInteger :: Integer -> Word #

Ord Word Source # 
Instance details

Defined in EVM.Types

Methods

compare :: Word -> Word -> Ordering #

(<) :: Word -> Word -> Bool #

(<=) :: Word -> Word -> Bool #

(>) :: Word -> Word -> Bool #

(>=) :: Word -> Word -> Bool #

max :: Word -> Word -> Word #

min :: Word -> Word -> Word #

Read Word Source # 
Instance details

Defined in EVM.Types

Real Word Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: Word -> Rational #

Show Word Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Word -> ShowS #

show :: Word -> String #

showList :: [Word] -> ShowS #

ToJSON Word Source # 
Instance details

Defined in EVM.Types

Bits Word Source # 
Instance details

Defined in EVM.Types

FiniteBits Word Source # 
Instance details

Defined in EVM.Types

SDisplay Word Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Word -> SExpr Text Source #

data SymWord Source #

Symbolic words of 256 bits, possibly annotated with additional "insightful" information

Constructors

S Whiff (SWord 256) 
Instances
Bounded SymWord Source # 
Instance details

Defined in EVM.Types

Enum SymWord Source # 
Instance details

Defined in EVM.Types

Eq SymWord Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: SymWord -> SymWord -> Bool #

(/=) :: SymWord -> SymWord -> Bool #

Num SymWord Source # 
Instance details

Defined in EVM.Types

Show SymWord Source # 
Instance details

Defined in EVM.Types

Bits SymWord Source # 
Instance details

Defined in EVM.Types

EqSymbolic SymWord Source #

Custom instances for SymWord, many of which have direct analogues for concrete words defined in Concrete.hs

Instance details

Defined in EVM.Types

SDivisible SymWord Source # 
Instance details

Defined in EVM.Types

SDisplay SymWord Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: SymWord -> SExpr Text Source #

iteWhiff :: Whiff -> SBool -> SWord 256 -> SWord 256 -> SymWord Source #

Instead of supporting a Mergeable instance directly, we use one which carries the Whiff around:

data Whiff Source #

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 do optimizations on the AST instead of letting the SMT solver do all the heavy lifting.

Instances
Show Whiff Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Whiff -> ShowS #

show :: Whiff -> String #

showList :: [Whiff] -> ShowS #

newtype Addr Source #

Constructors

Addr 
Instances
Enum Addr Source # 
Instance details

Defined in EVM.Types

Methods

succ :: Addr -> Addr #

pred :: Addr -> Addr #

toEnum :: Int -> Addr #

fromEnum :: Addr -> Int #

enumFrom :: Addr -> [Addr] #

enumFromThen :: Addr -> Addr -> [Addr] #

enumFromTo :: Addr -> Addr -> [Addr] #

enumFromThenTo :: Addr -> Addr -> Addr -> [Addr] #

Eq Addr Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Addr -> Addr -> Bool #

(/=) :: Addr -> Addr -> Bool #

Integral Addr Source # 
Instance details

Defined in EVM.Types

Methods

quot :: Addr -> Addr -> Addr #

rem :: Addr -> Addr -> Addr #

div :: Addr -> Addr -> Addr #

mod :: Addr -> Addr -> Addr #

quotRem :: Addr -> Addr -> (Addr, Addr) #

divMod :: Addr -> Addr -> (Addr, Addr) #

toInteger :: Addr -> Integer #

Num Addr Source # 
Instance details

Defined in EVM.Types

Methods

(+) :: Addr -> Addr -> Addr #

(-) :: Addr -> Addr -> Addr #

(*) :: Addr -> Addr -> Addr #

negate :: Addr -> Addr #

abs :: Addr -> Addr #

signum :: Addr -> Addr #

fromInteger :: Integer -> Addr #

Ord Addr Source # 
Instance details

Defined in EVM.Types

Methods

compare :: Addr -> Addr -> Ordering #

(<) :: Addr -> Addr -> Bool #

(<=) :: Addr -> Addr -> Bool #

(>) :: Addr -> Addr -> Bool #

(>=) :: Addr -> Addr -> Bool #

max :: Addr -> Addr -> Addr #

min :: Addr -> Addr -> Addr #

Read Addr Source # 
Instance details

Defined in EVM.Types

Real Addr Source # 
Instance details

Defined in EVM.Types

Methods

toRational :: Addr -> Rational #

Show Addr Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> Addr -> ShowS #

show :: Addr -> String #

showList :: [Addr] -> ShowS #

Generic Addr Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Addr :: Type -> Type #

Methods

from :: Addr -> Rep Addr x #

to :: Rep Addr x -> Addr #

FromJSON Addr Source # 
Instance details

Defined in EVM.Types

FromJSONKey Addr Source # 
Instance details

Defined in EVM.Types

Bits Addr Source # 
Instance details

Defined in EVM.Types

ParseField Addr Source # 
Instance details

Defined in EVM.Types

ParseFields Addr Source # 
Instance details

Defined in EVM.Types

ParseRecord Addr Source # 
Instance details

Defined in EVM.Types

ToSizzleBV Addr Source # 
Instance details

Defined in EVM.Types

ToRPC Addr Source # 
Instance details

Defined in EVM.Fetch

Methods

toRPC :: Addr -> Value Source #

SDisplay Addr Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Addr -> SExpr Text Source #

type Rep Addr Source # 
Instance details

Defined in EVM.Types

type Rep Addr = D1 (MetaData "Addr" "EVM.Types" "hevm-0.44.1-inplace" True) (C1 (MetaCons "Addr" PrefixI True) (S1 (MetaSel (Just "addressWord160") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word160)))

newtype SAddr Source #

Constructors

SAddr 

Fields

Instances
Num SAddr Source # 
Instance details

Defined in EVM.Types

Show SAddr Source # 
Instance details

Defined in EVM.Types

Methods

showsPrec :: Int -> SAddr -> ShowS #

show :: SAddr -> String #

showList :: [SAddr] -> ShowS #

type family FromSizzle (t :: Type) :: Type where ... Source #

Capture the correspondence between sized and fixed-sized BVs (This is blatant copypasta of FromSized from sbv, which just happens to be defined up to 64 bits)

Equations

FromSizzle (WordN 256) = W256 
FromSizzle (WordN 160) = Addr 

class FromSizzleBV a where Source #

Conversion from a sized BV to a fixed-sized bit-vector.

Minimal complete definition

Nothing

Methods

fromSizzle :: a -> FromSizzle a Source #

Convert a sized bit-vector to the corresponding fixed-sized bit-vector, for instance 'SWord 16' to SWord16. See also toSized.

fromSizzle :: (Num (FromSizzle a), Integral a) => a -> FromSizzle a Source #

Convert a sized bit-vector to the corresponding fixed-sized bit-vector, for instance 'SWord 16' to SWord16. See also toSized.

Instances
FromSizzleBV (WordN 160) Source # 
Instance details

Defined in EVM.Types

Methods

fromSizzle :: WordN 160 -> FromSizzle (WordN 160) Source #

FromSizzleBV (WordN 256) Source # 
Instance details

Defined in EVM.Types

Methods

fromSizzle :: WordN 256 -> FromSizzle (WordN 256) Source #

type family ToSizzle (t :: Type) :: Type where ... Source #

convert between (WordN 256) and Word256

Equations

ToSizzle W256 = WordN 256 
ToSizzle Addr = WordN 160 

class ToSizzleBV a where Source #

Conversion from a fixed-sized BV to a sized bit-vector.

Minimal complete definition

Nothing

Methods

toSizzle :: a -> ToSizzle a Source #

Convert a fixed-sized bit-vector to the corresponding sized bit-vector,

toSizzle :: (Num (ToSizzle a), Integral a) => a -> ToSizzle a Source #

Convert a fixed-sized bit-vector to the corresponding sized bit-vector,

Instances
ToSizzleBV Addr Source # 
Instance details

Defined in EVM.Types

ToSizzleBV W256 Source # 
Instance details

Defined in EVM.Types

readNull :: Read a => a -> String -> a Source #

num :: (Integral a, Num b) => a -> b Source #

truncpad :: Int -> [SWord 8] -> [SWord 8] Source #

Right padding / truncating

padLeft' :: Num a => Int -> [a] -> [a] Source #

byteAt :: (Bits a, Bits b, Integral a, Num b) => a -> Int -> b Source #

newtype Nibble Source #

Constructors

Nibble Word8 
Instances
Bounded Nibble Source # 
Instance details

Defined in EVM.Types

Enum Nibble Source # 
Instance details

Defined in EVM.Types

Eq Nibble Source # 
Instance details

Defined in EVM.Types

Methods

(==) :: Nibble -> Nibble -> Bool #

(/=) :: Nibble -> Nibble -> Bool #

Integral Nibble Source # 
Instance details

Defined in EVM.Types

Num Nibble Source # 
Instance details

Defined in EVM.Types

Ord Nibble Source # 
Instance details

Defined in EVM.Types

Real Nibble Source # 
Instance details

Defined in EVM.Types

Show Nibble Source # 
Instance details

Defined in EVM.Types

Generic Nibble Source # 
Instance details

Defined in EVM.Types

Associated Types

type Rep Nibble :: Type -> Type #

Methods

from :: Nibble -> Rep Nibble x #

to :: Rep Nibble x -> Nibble #

Bits Nibble Source # 
Instance details

Defined in EVM.Types

FiniteBits Nibble Source # 
Instance details

Defined in EVM.Types

type Rep Nibble Source # 
Instance details

Defined in EVM.Types

type Rep Nibble = D1 (MetaData "Nibble" "EVM.Types" "hevm-0.44.1-inplace" True) (C1 (MetaCons "Nibble" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Word8)))

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] Source #