Fetch: Refactor how we use RPC info and Fetcher

Author: blishko

cli/cli.hs

@@ -25,6 +25,7 @@ import Data.Text.IO qualified as T
 import Data.Version (showVersion)
 import Data.Word (Word64)
 import GHC.Conc (getNumProcessors)
+import GitHash
 import Numeric.Natural (Natural)
 import Optics.Core ((&), set)
 import Witch (unsafeInto)
@@ -43,7 +44,6 @@ import EVM.ABI (Sig(..))
 import EVM.Dapp (dappInfo, DappInfo, emptyDapp)
 import EVM.Expr qualified as Expr
 import EVM.Concrete qualified as Concrete
-import GitHash
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format (hexByteString, strip0x, formatExpr)
@@ -405,12 +405,11 @@ equivalence eqOpts cOpts = do
   when (isNothing bytecodeB) $ liftIO $ do
     putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
     exitFailure
-  let veriOpts = VeriOpts { iterConf = IterConfig {
+  let veriOpts = defaultVeriOpts { iterConf = IterConfig {
                             maxIter = parseMaxIters cOpts.maxIterations
                             , askSmtIters = cOpts.askSmtIterations
                             , loopHeuristic = cOpts.loopDetectionHeuristic
                             }
-                          , rpcInfo = mempty
                           }
   calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
   solver <- liftIO $ getSolver cOpts.solver
@@ -520,7 +519,7 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = do
                               , askSmtIters = cOpts.askSmtIterations
                               , loopHeuristic = cOpts.loopDetectionHeuristic
                               }
-                            , rpcInfo = mempty {Fetch.blockNumURL = blockUrlInfo}
+                            , rpcInfo = Fetch.RpcInfo blockUrlInfo
                             }
     let fetcher = Fetch.oracle solvers (Just sess) veriOpts.rpcInfo
     (expr, res) <- verify solvers fetcher veriOpts preState (checkAssertions errCodes)
@@ -576,7 +575,7 @@ launchExec cFileOpts execOpts cExecOpts cOpts = do
   let
     block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
     blockUrlInfo = (,) block <$> cExecOpts.rpc
-    rpcDat :: Fetch.RpcInfo = mempty { Fetch.blockNumURL = blockUrlInfo }
+    rpcDat :: Fetch.RpcInfo = Fetch.RpcInfo blockUrlInfo
 
   -- TODO: we shouldn't need solvers to execute this code
   withSolvers Z3 0 1 Nothing $ \solvers -> do
@@ -841,7 +840,7 @@ unitTestOptions testOpts cOpts solvers buildOutput = do
           (Just block, Just url) -> Just (Fetch.BlockNumber block, url)
           (Nothing, Just url) -> Just (Fetch.Latest, url)
           _ -> Nothing
-      rpcDat = Fetch.mkRpcInfo blockUrlInfo
+      rpcDat = Fetch.RpcInfo blockUrlInfo
   sess <- Fetch.mkSession cOpts.cacheDir testOpts.number
   params <- paramsFromRpc rpcDat sess
   let testn = params.number

src/EVM/Fetch.hs

@@ -8,8 +8,9 @@ module EVM.Fetch
   , RpcInfo (..)
   , RpcQuery (..)
   , EVM.Fetch.zero
+  , noRpc
+  , noRpcFetcher
   , BlockNumber (..)
-  , mkRpcInfo
   , mkSession
   , mkSessionWithoutCache
   , Session (..)
@@ -46,7 +47,6 @@ import Data.Bifunctor (first)
 import Control.Exception (try, SomeException)
 
 import Control.Monad.Trans.Maybe
-import Control.Applicative (Alternative(..))
 import Data.Aeson hiding (Error)
 import Data.Aeson.Optics
 import Data.ByteString qualified as BS
@@ -137,18 +137,11 @@ instance ToJSON RPCContract
 
 instance FromJSON RPCContract
 
-data RpcInfo = RpcInfo
-  { blockNumURL  :: Maybe (BlockNumber, Text) -- ^ (block number, RPC url)
-  }
+newtype RpcInfo = RpcInfo { blockNumURL  :: Maybe (BlockNumber, Text)} -- ^ (block number, RPC url)
   deriving (Show)
-instance Semigroup RpcInfo where
-  RpcInfo a1 <> RpcInfo b1 =
-    RpcInfo (a1 <|> b1)
-instance Monoid RpcInfo where
-  mempty = RpcInfo Nothing
 
-mkRpcInfo :: Maybe (BlockNumber, Text) -> RpcInfo
-mkRpcInfo blockNumURL = RpcInfo blockNumURL
+noRpc :: RpcInfo
+noRpc = RpcInfo Nothing
 
 rpc :: String -> [Value] -> Value
 rpc method args = object
@@ -422,7 +415,10 @@ zero :: Natural -> Maybe Natural -> Fetcher t m s
 zero smtjobs smttimeout q = do
   sess <- mkSessionWithoutCache
   withSolvers Z3 smtjobs 1 smttimeout $ \s ->
-    oracle s (Just sess) mempty q
+    oracle s (Just sess) noRpc q
+
+noRpcFetcher :: forall t m s . App m => SolverGroup -> Fetcher t m s
+noRpcFetcher sg = oracle sg Nothing noRpc
 
 -- SMT solving + RPC data fetching + reading from environment
 oracle :: forall t m s . App m => SolverGroup -> Maybe Session -> RpcInfo -> Fetcher t m s

src/EVM/SymExec.hs

@@ -105,12 +105,9 @@ data VeriOpts = VeriOpts
 defaultVeriOpts :: VeriOpts
 defaultVeriOpts = VeriOpts
   { iterConf = defaultIterConf
-  , rpcInfo = mempty
+  , rpcInfo = Fetch.noRpc
   }
 
-rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
-rpcVeriOpts info = defaultVeriOpts { rpcInfo  = mempty { Fetch.blockNumURL = Just info }}
-
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
 extractCex (Cex c) = Just c
 extractCex _ = Nothing
@@ -840,7 +837,7 @@ equivalenceCheck solvers sess bytecodeA bytecodeB opts calldata create = do
       conf <- readConfig
       let bytecode = if BS.null bs then BS.pack [0] else bs
       prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create
-      expr <- interpret (Fetch.oracle solvers sess mempty) opts.iterConf prestate runExpr
+      expr <- interpret (Fetch.oracle solvers sess Fetch.noRpc) opts.iterConf prestate runExpr
       let simpl = if conf.simp then Expr.simplify expr else expr
       pure $ flattenExpr simpl
     oneQedOrNoQed :: EqIssues -> EqIssues

test/EVM/Test/BlockchainTests.hs

@@ -109,7 +109,7 @@ prepareTests = do
 
     runTest :: App m => EVM.Fetch.Session -> (String, Case) -> m TestTree
     runTest session (name, x) = do
-      let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.oracle s (Just session) mempty q
+      let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.oracle s (Just session) EVM.Fetch.noRpc q
       exec <- toIO $ runVMTest fetcher x
       pure $ testCase' name exec
     testCase' :: String -> Assertion -> TestTree

test/EVM/Test/FuzzSymExec.hs

@@ -13,6 +13,7 @@ concretely through Expr.simplify, then check that against evmtool's output.
 module EVM.Test.FuzzSymExec where
 
 import Control.Monad (when)
+import Control.Monad.IO.Unlift
 import Control.Monad.ST (ST, stToIO)
 import Control.Monad.State.Strict (StateT(..))
 import Control.Monad.Reader (ReaderT)
@@ -29,6 +30,7 @@ import Data.Word (Word8, Word64)
 import GHC.Generics (Generic)
 import GHC.IO.Exception (ExitCode(ExitSuccess))
 import Numeric (showHex)
+import Optics.Core hiding (pre)
 import System.Directory (removeDirectoryRecursive)
 import System.FilePath ((</>))
 import System.IO.Temp (getCanonicalTemporaryDirectory, createTempDirectory)
@@ -42,8 +44,6 @@ import Test.Tasty.HUnit (assertEqual, testCase)
 import Test.Tasty.QuickCheck hiding (Failure, Success)
 import Witch (into, unsafeInto)
 
-import Optics.Core hiding (pre)
-
 import EVM (makeVm, initialContract, symbolify)
 import EVM.Assembler (assemble)
 import EVM.Expr qualified as Expr
@@ -60,7 +60,6 @@ import EVM.Traversals (mapExpr)
 import EVM.Transaction qualified
 import EVM.Types hiding (Env)
 import EVM.Effects
-import Control.Monad.IO.Unlift
 import EVM.Tracing (interpretWithTrace, VMTraceStep(..), VMTraceStepResult(..))
 
 data EVMToolTrace =
@@ -283,7 +282,7 @@ getHEVMRet
   => OpContract -> ByteString -> Int -> m (Either (EvmError, [VMTraceStep]) (Expr 'End, [VMTraceStep], VMTraceStepResult))
 getHEVMRet contr txData gaslimitExec = do
   let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec
-  runCodeWithTrace mempty evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
+  runCodeWithTrace Fetch.noRpc evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
 
 getEVMToolRet :: FilePath -> OpContract -> ByteString -> Int -> IO (Maybe EVMToolResult)
 getEVMToolRet evmDir contr txData gaslimitExec = do

test/EVM/Test/Utils.hs

@@ -24,7 +24,7 @@ import EVM.Effects
 import Data.Maybe (fromMaybe)
 import EVM.Types (internalError)
 import System.Environment (lookupEnv)
-import EVM.Fetch (RpcInfo)
+import EVM.Fetch (RpcInfo, noRpc)
 import EVM.Fetch qualified as Fetch
 
 -- Returns tuple of (No cex, No warnings)
@@ -47,7 +47,7 @@ runForgeTestCustom testFile match timeout maxIter ffiAllowed rpcinfo = do
 runForgeTest
   :: (MonadMask m, App m)
   => FilePath -> Text -> m (Bool, Bool)
-runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True mempty
+runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True noRpc
 
 testOpts :: forall m . App m => SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> m (UnitTestOptions RealWorld)
 testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do

test/rpc.hs

@@ -82,15 +82,12 @@ tests = testGroup "rpc"
     -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code
     , test "weth-conc" $ do
         let
-          blockNum = 16198552
           wad = 0x999999999999999999
           calldata' = ConcreteBuf $ abiMethod "transfer(address,uint256)" (AbiTuple (V.fromList [AbiAddress (Addr 0xdead), AbiUInt 256 wad]))
-          rpcDat = Just (BlockNumber blockNum, testRpc)
-          rpcInfo :: RpcInfo = mempty { blockNumURL = rpcDat }
         sess <- mkSessionWithoutCache
-        vm <- weth9VM sess blockNum (calldata', [])
+        vm <- weth9VM sess testBlockNumber (calldata', [])
         postVm <- withSolvers Z3 1 1 Nothing $ \solvers ->
-          Stepper.interpret (oracle solvers (Just sess) rpcInfo) vm Stepper.runFully
+          Stepper.interpret (oracle solvers (Just sess) testRpcInfo) vm Stepper.runFully
         let
           wethStore = (fromJust $ Map.lookup (LitAddr 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2) postVm.env.contracts).storage
           wethStore' = case wethStore of
@@ -109,36 +106,34 @@ tests = testGroup "rpc"
     , test "weth-sym" $ do
         calldata' <- symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata")
         let
-          blockNum = 16198552
           postc _ (Failure _ _ (Revert _)) = PBool False
           postc _ _ = PBool True
         sess <- mkSession Nothing Nothing
-        vm <- weth9VM sess blockNum calldata'
+        vm <- weth9VM sess testBlockNumber calldata'
         (_, [Cex (_, model)]) <- withSolvers Z3 1 1 Nothing $ \s ->
-          let rpcInfo ::RpcInfo =  mempty { blockNumURL = Just (BlockNumber blockNum, testRpc) }
-          in verify s (oracle s (Just sess) rpcInfo) (rpcVeriOpts (fromJust rpcInfo.blockNumURL)) (symbolify vm) postc
+          verify s (oracle s (Just sess) testRpcInfo) (defaultVeriOpts {rpcInfo = testRpcInfo}) (symbolify vm) postc
         liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
     ]
   ]
 
 -- call into WETH9 from 0xf04a... (a large holder)
-weth9VM :: App m => Session -> W256 -> (Expr Buf, [Prop]) -> m (VM Concrete RealWorld)
+weth9VM :: App m => Session -> BlockNumber -> (Expr Buf, [Prop]) -> m (VM Concrete RealWorld)
 weth9VM sess blockNum calldata' = do
   let
     caller' = LitAddr 0xf04a5cc80b1e94c69b48f5ee68a08cd2f09a7c3e
     weth9 = Addr 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2
     callvalue' = Lit 0
   vmFromRpc sess blockNum calldata' callvalue' caller' weth9
 
-vmFromRpc :: App m => Session -> W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> m (VM Concrete RealWorld)
+vmFromRpc :: App m => Session -> BlockNumber -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> m (VM Concrete RealWorld)
 vmFromRpc sess blockNum calldata callvalue caller address = do
   conf <- readConfig
-  ctrct <- liftIO $ fetchContractWithSession conf sess (BlockNumber blockNum) testRpc address >>= \case
+  ctrct <- liftIO $ fetchContractWithSession conf sess blockNum testRpc address >>= \case
         Nothing -> internalError $ "contract not found: " <> show address
         Just contract' -> pure contract'
 
   liftIO $ addFetchCache sess address ctrct
-  blk <- liftIO $ fetchBlockWithSession conf sess (BlockNumber blockNum) testRpc >>= \case
+  blk <- liftIO $ fetchBlockWithSession conf sess blockNum testRpc >>= \case
     Nothing -> internalError "could not fetch block"
     Just b -> pure b
 
@@ -174,6 +169,8 @@ vmFromRpc sess blockNum calldata callvalue caller address = do
 testRpc :: Text
 testRpc = "https://eth-mainnet.alchemyapi.io/v2/vpeKFsEF6PHifHzdtcwXSDbhV3ym5Ro4"
 
+testBlockNumber :: BlockNumber
+testBlockNumber = BlockNumber 16198552
+
 testRpcInfo :: RpcInfo
-testRpcInfo = let rpcDat = Just (BlockNumber 16198552, testRpc)
-  in mempty { blockNumURL = rpcDat }
+testRpcInfo = RpcInfo $ Just (testBlockNumber, testRpc)

test/test.hs

@@ -1891,7 +1891,7 @@ tests = testGroup "hevm"
           let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), [])
           initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True
           let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased }
-          expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing mempty) iterConf initVM runExpr
+          expr <- Expr.simplify <$> interpret (Fetch.noRpcFetcher s) iterConf initVM runExpr
           assertBoolM "unexptected partial execution" (not $ Expr.containsNode isPartial expr)
     , test "mixed-concrete-symbolic-args" $ do
         Just c <- solcRuntime "C"
@@ -1982,7 +1982,7 @@ tests = testGroup "hevm"
         withDefaultSolver $ \s -> do
           vm <- liftIO $ stToIO $ loadSymVM runtimecode (Lit 0) initCode False
           let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased }
-          expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing mempty) iterConf vm runExpr
+          expr <- Expr.simplify <$> interpret (Fetch.noRpcFetcher s) iterConf vm runExpr
           case expr of
             Partial _ _ (JumpIntoSymbolicCode _ _ _) -> assertBoolM "" True
             _ -> assertBoolM "did not encounter expected partial node" False
@@ -2022,7 +2022,7 @@ tests = testGroup "hevm"
               , ("test/contracts/fail/symbolicFail.sol",      "prove_symb_fail_allrev_selector.*", (False, False))
               , ("test/contracts/fail/symbolicFail.sol",      "prove_symb_fail_somerev_selector.*", (False, True))]
         forM_ cases $ \(testFile, match, expected) -> do
-          actual <- runForgeTestCustom testFile match Nothing Nothing False mempty
+          actual <- runForgeTestCustom testFile match Nothing Nothing False Fetch.noRpc
           putStrLnM $ "Test result for " <> testFile <> " match: " <> T.unpack match <> ": " <> show actual
           assertEqualM "Must match" expected actual
     , test "Trivial-Fail" $ do
@@ -2055,14 +2055,14 @@ tests = testGroup "hevm"
         runForgeTest testFile "prove_trivial" >>= assertEqualM "prove_trivial" (False, False)
         runForgeTest testFile "prove_trivial_dstest" >>= assertEqualM "prove_trivial_dstest" (False, False)
         runForgeTest testFile "prove_add" >>= assertEqualM "prove_add" (False, True)
-        runForgeTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False mempty
+        runForgeTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Fetch.noRpc
           >>= assertEqualM "prove_smtTimeout" (True, False)
         runForgeTest testFile "prove_multi" >>= assertEqualM "prove_multi" (False, True)
         runForgeTest testFile "prove_distributivity" >>= assertEqualM "prove_distributivity" (False, True)
     , test "Loop-Tests" $ do
         let testFile = "test/contracts/pass/loops.sol"
-        runForgeTestCustom testFile "prove_loop" Nothing (Just 10) False mempty  >>= assertEqualM "test result" (True, False)
-        runForgeTestCustom testFile "prove_loop" Nothing (Just 100) False mempty >>= assertEqualM "test result" (False, False)
+        runForgeTestCustom testFile "prove_loop" Nothing (Just 10) False Fetch.noRpc  >>= assertEqualM "test result" (True, False)
+        runForgeTestCustom testFile "prove_loop" Nothing (Just 100) False Fetch.noRpc >>= assertEqualM "test result" (False, False)
     , test "Cheat-Codes-Pass" $ do
         let testFile = "test/contracts/pass/cheatCodes.sol"
         runForgeTest testFile ".*" >>= assertEqualM "test result" (True, False)
@@ -4218,7 +4218,7 @@ tests = testGroup "hevm"
                     <&> set (#state % #callvalue) (Lit 0)
                     <&> over (#env % #contracts)
                        (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a))))
-            verify s (Fetch.oracle s Nothing mempty) defaultVeriOpts vm (checkAssertions defaultPanicCodes)
+            verify s (Fetch.noRpcFetcher s) defaultVeriOpts vm (checkAssertions defaultPanicCodes)
 
           let storeCex = cex.store
               testCex = case (Map.lookup cAddr storeCex, Map.lookup aAddr storeCex) of
@@ -4294,7 +4294,7 @@ tests = testGroup "hevm"
           let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"
           calldata <- mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []
           vm <- liftIO $ stToIO $ abstractVM calldata yulsafeDistributivity Nothing False
-          (_, [Qed]) <-  withDefaultSolver $ \s -> verify s (Fetch.oracle s Nothing mempty) defaultVeriOpts vm (checkAssertions defaultPanicCodes)
+          (_, [Qed]) <-  withDefaultSolver $ \s -> verify s (Fetch.noRpcFetcher s) defaultVeriOpts vm (checkAssertions defaultPanicCodes)
           putStrLnM "Proven"
         ,
         test "safemath-distributivity-sol" $ do