Having a go at implementing 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 =
@@ -1900,6 +1908,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,12 +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
+import Debug.Trace (traceM)
 
 -- | Abstract representation of an RPC fetch request
 data RpcQuery a where
@@ -184,16 +184,6 @@ 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
@@ -218,6 +208,7 @@ oracle solvers info q = do
          continue <$> getSolution solvers symAddr pathconds
 
     PleaseFetchContract addr base continue -> do
+      traceM $ "Fetching contract " <> show addr <> "base: " <> show base <> " from " <> show info
       contract <- case info of
         Nothing -> let
           c = case base of
@@ -229,15 +220,24 @@ oracle solvers info q = do
         Just x -> pure $ continue x
         Nothing -> internalError $ "oracle error: " ++ show q
 
-    PleaseFetchSlot addr slot continue ->
+    PleaseFetchSlot addr slot continue -> do
+      traceM $ "Fetching slot " <> show slot <> " from " <> show info
       case info of
         Nothing -> pure (continue 0)
-        Just (n, url) ->
+        Just (n, url) -> do
+         traceM $ "Fetching slot " <> show slot <> " from " <> show url <> " at addr " <> show addr <> " at block " <> show n
          liftIO $ fetchSlotFrom n url addr slot >>= \case
            Just x  -> pure (continue x)
            Nothing ->
              internalError $ "oracle error: " ++ show q
 
+    PleaseFetchBlock url blockNo continue -> do
+      traceM $ "Fetching block " <> show blockNo <> " from " <> show url
+      liftIO $ fetchBlockFrom (EVM.Fetch.BlockNumber blockNo) (pack url) >>= \case
+        Just block  -> do
+          pure (continue block)
+        Nothing -> internalError $ "oracle error: " ++ show q
+
     PleaseReadEnv variable continue -> do
       value <- liftIO $ lookupEnv variable
       pure . continue $ fromMaybe "" value

src/EVM/Types.hs

@@ -593,6 +593,7 @@ deriving instance Show (Effect t s)
 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
+  PleaseFetchBlock    :: String -> W256 -> (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
@@ -609,11 +610,15 @@ data BranchCondition = Case Bool | Unknown
 instance Show (Query t s) where
   showsPrec _ = \case
     PleaseFetchContract addr base _ ->
-      (("<EVM.Query: fetch contract " ++ show addr ++ show base ++ ">") ++)
+      (("<EVM.Query: fetch from contract " ++ show addr ++ show base ++ ">") ++)
     PleaseFetchSlot addr slot _ ->
       (("<EVM.Query: fetch slot "
         ++ show slot ++ " for "
         ++ show addr ++ ">") ++)
+    PleaseFetchBlock url block _ ->
+      (("<EVM.Query: fetch from url "
+        ++ show url ++ " block "
+        ++ show block ++ ">") ++)
     PleaseAskSMT condition constraints _ ->
       (("<EVM.Query: ask SMT about "
         ++ show condition ++ " in context "

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