EVM.Fuzz

Documentation

tryCexFuzz :: [Prop] -> Integer -> Maybe SMTCex

filterCorrectKeccak :: [Prop] -> [Prop]

substituteEWord :: Map (Expr EWord) W256 -> Prop -> Prop

substituteBuf :: Map (Expr Buf) BufModel -> Prop -> Prop

substituteStores :: Map (Expr 'EAddr) (Map W256 W256) -> Prop -> Prop

data CollectVars

Constructors

CollectVars

Fields

• vars :: Set (Expr EWord)
• vals :: Set W256

Instances

Show CollectVars

Defined in EVM.Fuzz

Methods

showsPrec :: Int -> CollectVars -> ShowS

show :: CollectVars -> String

showList :: [CollectVars] -> ShowS

initVarsState :: CollectVars

findVarProp :: Prop -> State CollectVars Prop

extractVars :: [Prop] -> CollectVars

newtype CollectBufs

Constructors

CollectBufs

Fields

• bufs :: Set (Expr Buf)

Instances

Show CollectBufs

Defined in EVM.Fuzz

Methods

showsPrec :: Int -> CollectBufs -> ShowS

show :: CollectBufs -> String

showList :: [CollectBufs] -> ShowS

initBufsState :: CollectBufs

extractBufs :: [Prop] -> [Expr Buf]

findBufProp :: Prop -> State CollectBufs Prop

data CollectStorage

Constructors

CollectStorage

Fields

• addrs :: Set (Expr EAddr, Maybe W256)
• keys :: Set W256
• vals :: Set W256

Instances

Semigroup CollectStorage

Defined in EVM.Fuzz

Methods

(<>) :: CollectStorage -> CollectStorage -> CollectStorage

sconcat :: NonEmpty CollectStorage -> CollectStorage

stimes :: Integral b => b -> CollectStorage -> CollectStorage

Show CollectStorage

Defined in EVM.Fuzz

Methods

showsPrec :: Int -> CollectStorage -> ShowS

show :: CollectStorage -> String

showList :: [CollectStorage] -> ShowS

initStorageState :: CollectStorage

extractStorage :: [Prop] -> CollectStorage

findStoragePropComp :: Prop -> State CollectStorage Prop

findStoragePropInner :: Prop -> State CollectStorage Prop

getvals :: CollectVars -> Gen (Map (Expr EWord) W256)

getStores :: CollectStorage -> Gen (Map (Expr EAddr) (Map W256 W256))

getBufs :: [Expr Buf] -> Gen (Map (Expr Buf) BufModel)

getRndW256 :: Gen W256