[DRAFT] Implement createSelectFork

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   and continue running, whenever possible
 - STATICCALL abstraction is now performed in case of symbolic arguments
 - Better error messages for JSON parsing
+- Added support for createSelectFork(string,uint256)
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM.hs

@@ -67,6 +67,7 @@ import Witch (into, tryFrom, unsafeInto, tryInto)
 import Crypto.Hash (Digest, SHA256, RIPEMD160)
 import Crypto.Hash qualified as Crypto
 import Crypto.Number.ModArithmetic (expFast)
+import Debug.Trace (traceM)
 
 blankState :: VMOps t => ST s (FrameState t s)
 blankState = do
@@ -1407,6 +1408,13 @@ query q = assign #result $ Just $ HandleEffect (Query q)
 choose :: Choose s -> EVM Symbolic s ()
 choose c = assign #result $ Just $ HandleEffect (Choose c)
 
+fetchBlockFrom :: VMOps t => String -> W256 -> (Block -> EVM t s ()) -> EVM t s ()
+fetchBlockFrom url blockNo continue = do
+      assign (#result) . Just . HandleEffect . Query $
+        PleaseFetchBlock url blockNo $ \c -> do
+          assign #result Nothing
+          continue c
+
 -- | Construct RPC Query and halt execution until resolved
 fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
 fetchAccount addr continue =
@@ -1424,8 +1432,10 @@ fetchAccount addr continue =
             continue c
           Nothing -> do
             base <- use (#config % #baseState)
+            block <- use (#block % #number)
+            let rpcInfo = Just FinRpcInfo {block=block, url="a"}
             assign (#result) . Just . HandleEffect . Query $
-              PleaseFetchContract a base $ \c -> do
+              PleaseFetchContract rpcInfo a base $ \c -> do
                 assign (#cache % #fetched % at a) (Just c)
                 assign (#env % #contracts % at addr) (Just c)
                 assign #result Nothing
@@ -1900,6 +1910,25 @@ cheatActions = Map.fromList
                 vmError (NonexistentFork forkId')
         _ -> vmError (BadCheatCode "selectFork(uint256) parameter decoding failed" sig)
 
+  , action "createSelectFork(string,uint256)" $
+      \sig input -> case decodeBuf [AbiStringType, AbiUIntType 256] input of
+        CAbi [AbiString url, AbiUInt 256 blockNo] -> do
+          let blockNo' = fromIntegral blockNo
+          fetchBlockFrom (BS8.unpack url) blockNo' $ \block -> do
+            traceM $ "here, continuing with block:" <> show  block
+            vm <- get
+            let forks = vm.forks Seq.|> ForkState vm.env block vm.cache (BS8.unpack url)
+            let forkId = length $ forks
+            modify' $ \vm' -> vm'
+              { env = vm.env
+              , block = block
+              , forks =  forks
+              , currentFork = forkId
+              }
+            -- modify' $ \vm' -> vm' { env = vm.env, block = block }
+            frameReturn $ AbiUInt 256 (fromIntegral forkId)
+        _ -> vmError (BadCheatCode "createSelectFork(string,uint256) parameter decoding failed" sig)
+
   , action "activeFork()" $
       \_ _ -> do
         vm <- get

src/EVM/Fetch.hs

@@ -23,28 +23,12 @@ import Data.Vector qualified as RegularVector
 import Network.Wreq
 import Network.Wreq.Session (Session)
 import Network.Wreq.Session qualified as Session
-import Numeric.Natural (Natural)
 import System.Environment (lookupEnv, getEnvironment)
 import System.Process
 import Control.Monad.IO.Class
 import Control.Monad (when)
 import EVM.Effects
-
--- | Abstract representation of an RPC fetch request
-data RpcQuery a where
-  QueryCode    :: Addr         -> RpcQuery BS.ByteString
-  QueryBlock   ::                 RpcQuery Block
-  QueryBalance :: Addr         -> RpcQuery W256
-  QueryNonce   :: Addr         -> RpcQuery W64
-  QuerySlot    :: Addr -> W256 -> RpcQuery W256
-  QueryChainId ::                 RpcQuery W256
-
-data BlockNumber = Latest | BlockNumber W256
-  deriving (Show, Eq)
-
-deriving instance Show (RpcQuery a)
-
-type RpcInfo = Maybe (BlockNumber, Text)
+import Debug.Trace (traceM)
 
 rpc :: String -> [Value] -> Value
 rpc method args = object
@@ -54,28 +38,28 @@ rpc method args = object
   , "params"  .= args
   ]
 
-class ToRPC a where
-  toRPC :: a -> Value
+-- class ToRPC a where
+--   toRPC :: a -> Value
 
-instance ToRPC Addr where
-  toRPC = String . pack . show
+-- instance ToRPC Addr where
+--   toRPC = String . pack . show
 
-instance ToRPC W256 where
-  toRPC = String . pack . show
+-- instance ToRPC W256 where
+--   toRPC = String . pack . show
 
-instance ToRPC Bool where
-  toRPC = Bool
+-- instance ToRPC Bool where
+--   toRPC = Bool
 
-instance ToRPC BlockNumber where
-  toRPC Latest          = String "latest"
-  toRPC (EVM.Fetch.BlockNumber n) = String . pack $ show n
+-- instance ToRPC BlockInt where
+--   toRPC Latest          = String "latest"
+--   toRPC (EVM.Fetch.BlockInt n) = String . pack $ show n
 
 readText :: Read a => Text -> a
 readText = read . unpack
 
 fetchQuery
   :: Show a
-  => BlockNumber
+  => BlockInt
   -> (Value -> IO (Maybe Value))
   -> RpcQuery a
   -> IO (Maybe a)
@@ -137,8 +121,7 @@ fetchWithSession url sess x = do
   r <- asValue =<< Session.post sess (unpack url) x
   pure (r ^? (lensVL responseBody) % key "result")
 
-fetchContractWithSession
-  :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
+fetchContractWithSession :: BlockInt -> Text -> Addr -> Session -> IO (Maybe Contract)
 fetchContractWithSession n url addr sess = runMaybeT $ do
   let
     fetch :: Show a => RpcQuery a -> IO (Maybe a)
@@ -154,27 +137,25 @@ fetchContractWithSession n url addr sess = runMaybeT $ do
       & set #balance  (Lit balance)
       & set #external True
 
-fetchSlotWithSession
-  :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
+fetchSlotWithSession :: BlockInt -> Text -> Session -> Addr -> W256 -> IO (Maybe W256)
 fetchSlotWithSession n url sess addr slot =
   fetchQuery n (fetchWithSession url sess) (QuerySlot addr slot)
 
-fetchBlockWithSession
-  :: BlockNumber -> Text -> Session -> IO (Maybe Block)
+fetchBlockWithSession :: BlockInt -> Text -> Session -> IO (Maybe Block)
 fetchBlockWithSession n url sess =
   fetchQuery n (fetchWithSession url sess) QueryBlock
 
-fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
+fetchBlockFrom :: BlockInt -> Text -> IO (Maybe Block)
 fetchBlockFrom n url = do
   sess <- Session.newAPISession
   fetchBlockWithSession n url sess
 
-fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
+fetchContractFrom :: BlockInt -> Text -> Addr -> IO (Maybe Contract)
 fetchContractFrom n url addr = do
   sess <- Session.newAPISession
   fetchContractWithSession n url addr sess
 
-fetchSlotFrom :: BlockNumber -> Text -> Addr -> W256 -> IO (Maybe W256)
+fetchSlotFrom :: BlockInt -> Text -> Addr -> W256 -> IO (Maybe W256)
 fetchSlotFrom n url addr slot = do
   sess <- Session.newAPISession
   fetchSlotWithSession n url sess addr slot
@@ -184,19 +165,9 @@ fetchChainIdFrom url = do
   sess <- Session.newAPISession
   fetchQuery Latest (fetchWithSession url sess) QueryChainId
 
-http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
-http smtjobs smttimeout n url q =
-  withSolvers Z3 smtjobs 1 smttimeout $ \s ->
-    oracle s (Just (n, url)) q
-
-zero :: Natural -> Maybe Natural -> Fetcher t m s
-zero smtjobs smttimeout q =
-  withSolvers Z3 smtjobs 1 smttimeout $ \s ->
-    oracle s Nothing q
-
 -- smtsolving + (http or zero)
-oracle :: SolverGroup -> RpcInfo -> Fetcher t m s
-oracle solvers info q = do
+oracle :: SolverGroup -> Fetcher t m s
+oracle solvers q = do
   case q of
     PleaseDoFFI vals envs continue -> case vals of
        cmd : args -> do
@@ -217,26 +188,34 @@ oracle solvers info q = do
          let pathconds = foldl' PAnd (PBool True) pathconditions
          continue <$> getSolution solvers symAddr pathconds
 
-    PleaseFetchContract addr base continue -> do
-      contract <- case info of
+    PleaseFetchContract rpcInfo addr base continue -> do
+      contract <- case rpcInfo of
         Nothing -> let
           c = case base of
             AbstractBase -> unknownContract (LitAddr addr)
             EmptyBase -> emptyContract
           in pure $ Just c
-        Just (n, url) -> liftIO $ fetchContractFrom n url addr
+        Just rpcDat -> liftIO $ fetchContractFrom rpcDat.blockNo rpcDat.url addr
       case contract of
         Just x -> pure $ continue x
         Nothing -> internalError $ "oracle error: " ++ show q
 
-    PleaseFetchSlot addr slot continue ->
-      case info of
+    PleaseFetchSlot rpcInfo addr slot continue -> do
+      case rpcInfo of
         Nothing -> pure (continue 0)
-        Just (n, url) ->
-         liftIO $ fetchSlotFrom n url addr slot >>= \case
+        Just rpcDat -> do
+         liftIO $ fetchSlotFrom rpcDat.blockNo rpcDat.url addr slot >>= \case
            Just x  -> pure (continue x)
-           Nothing ->
-             internalError $ "oracle error: " ++ show q
+           Nothing -> internalError $ "oracle error: " ++ show q
+
+    PleaseFetchBlock rpcInfo continue -> do
+      -- traceM $ "Fetching block " <> show rpcInfo.blockNo <> " from " <> show rpcInfo.url
+      case rpcInfo of
+        Nothing -> internalError "PleaseFetchBlock: no rpcInfo"
+        Just rpcDat -> do
+          liftIO $ fetchBlockFrom rpcDat.blockNo rpcDat.url >>= \case
+            Just block  -> pure (continue block)
+            Nothing -> internalError $ "oracle error: " ++ show q
 
     PleaseReadEnv variable continue -> do
       value <- liftIO $ lookupEnv variable

src/EVM/SymExec.hs

@@ -94,7 +94,7 @@ data VeriOpts = VeriOpts
   , maxIter :: Maybe Integer
   , askSmtIters :: Integer
   , loopHeuristic :: LoopHeuristic
-  , rpcInfo :: Fetch.RpcInfo
+  , rpcInfo :: RpcInfo
   }
   deriving (Eq, Show)
 
@@ -107,7 +107,7 @@ defaultVeriOpts = VeriOpts
   , rpcInfo = Nothing
   }
 
-rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
+rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts
 rpcVeriOpts info = defaultVeriOpts { rpcInfo = Just info }
 
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
@@ -963,7 +963,7 @@ prettyCalldata cex buf sig types = headErr errSig (T.splitOn "(" sig) <> "(" <>
           ConcreteBuf c -> T.pack (bsToHex c)
           _ -> err
       SAbi _ -> err
-    headErr e l = fromMaybe e $ listToMaybe l 
+    headErr e l = fromMaybe e $ listToMaybe l
     err = internalError $ "unable to produce a concrete model for calldata: " <> show buf
     errSig = internalError $ "unable to split sig: " <> show sig
 

src/EVM/Types.hs

@@ -591,8 +591,9 @@ 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
+  PleaseFetchContract :: RpcInfo -> Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
+  PleaseFetchSlot     :: RpcInfo -> Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
+  PleaseFetchBlock    :: RpcInfo -> (Block -> EVM t s ()) -> Query t s
   PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseGetSol        :: Expr EWord -> [Prop] -> (Maybe W256 -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseDoFFI         :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s
@@ -608,12 +609,16 @@ data BranchCondition = Case Bool | Unknown
 
 instance Show (Query t s) where
   showsPrec _ = \case
-    PleaseFetchContract addr base _ ->
-      (("<EVM.Query: fetch contract " ++ show addr ++ show base ++ ">") ++)
-    PleaseFetchSlot addr slot _ ->
+    PleaseFetchContract _ addr base _ ->
+      (("<EVM.Query: fetch from contract " ++ show addr ++ show base ++ ">") ++)
+    PleaseFetchSlot _ addr slot _ ->
       (("<EVM.Query: fetch slot "
         ++ show slot ++ " for "
         ++ show addr ++ ">") ++)
+    PleaseFetchBlock rpcInfo _ ->
+      (("<EVM.Query: fetch from url "
+        ++ (T.unpack rpcInfo.url) ++ " block "
+        ++ show rpcInfo.block ++ ">") ++)
     PleaseAskSMT condition constraints _ ->
       (("<EVM.Query: ask SMT about "
         ++ show condition ++ " in context "
@@ -1435,6 +1440,23 @@ untilFixpoint f a = if f a == a
                     then a
                     else untilFixpoint f (f a)
 
+data BlockInt = Latest | BlockInt W256
+  deriving (Show, Eq)
+
+deriving instance Show (RpcQuery a)
+
+type RpcInfo = Maybe FinRpcInfo
+data FinRpcInfo = FinRpcInfo {block :: W256, url :: Text}
+
+-- | Abstract representation of an RPC fetch request
+data RpcQuery a where
+  QueryCode    :: Addr         -> RpcQuery BS.ByteString
+  QueryBlock   ::                 RpcQuery Block
+  QueryBalance :: Addr         -> RpcQuery W256
+  QueryNonce   :: Addr         -> RpcQuery W64
+  QuerySlot    :: Addr -> W256 -> RpcQuery W256
+  QueryChainId ::                 RpcQuery W256
+
 -- Optics ------------------------------------------------------------------------------------------
 
 

test/EVM/Test/BlockchainTests.hs

@@ -37,10 +37,12 @@ import System.Process (readProcessWithExitCode)
 import GHC.IO.Exception (ExitCode(ExitSuccess))
 import Witch (into, unsafeInto)
 import Witherable (Filterable, catMaybes)
+import EVM.Solvers (withSolvers, Solver(..))
 
 import Test.Tasty
 import Test.Tasty.ExpectedFailure
 import Test.Tasty.HUnit
+import qualified EVM.Fetch as EVM
 
 data Which = Pre | Post
 
@@ -175,11 +177,15 @@ ciProblematicTests = Map.fromList
   , ("loopExp_d9g0v0_Cancun", ignoreTest)
   ]
 
+zeroFetcher :: EVM.Fetch.Fetcher t m s
+zeroFetcher q = withSolvers Z3 0 1 (Just 0) $ \s ->
+    EVM.oracle s Nothing q
+
 runVMTest :: App m => Case -> m ()
 runVMTest x = do
   -- traceVsGeth fname name x
   vm0 <- liftIO $ vmForCase x
-  result <- EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) vm0 EVM.Stepper.runFully
+  result <- EVM.Stepper.interpret zeroFetcher vm0 EVM.Stepper.runFully
   writeTrace result
   maybeReason <- checkExpectation x result
   liftIO $ forM_ maybeReason assertFailure
@@ -189,7 +195,7 @@ runVMTest x = do
 traceVMTest :: App m => Case -> m [VMTrace]
 traceVMTest x = do
   vm0 <- liftIO $ vmForCase x
-  (_, (_, ts)) <- runStateT (interpretWithTrace (EVM.Fetch.zero 0 (Just 0)) EVM.Stepper.runFully) (vm0, [])
+  (_, (_, ts)) <- runStateT (interpretWithTrace zeroFetcher EVM.Stepper.runFully) (vm0, [])
   pure ts
 
 -- | given a path to a test file, a test case from within that file, and a trace from geth from running that test, compare the traces and show where we differ