Merge pull request #692 from ethereum/symbolic-block-number

msooseth · web-flow · commit 6c2869bd06f5 · 2025-04-08T06:53:43.000-07:00
Symbolic block number is now allowed in library mode
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -85,6 +85,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Add `--arrays-exp` to cvc5 options.
 - We now use Options.Applicative and a rather different way of parsing CLI options.
   This should give us much better control over the CLI options and their parsing.
+- block.number can now be symbolic. This only affects library use of hevm
 - Removed `--smtoutput` since it was never used
 - We now build with -DCMAKE_POLICY_VERSION_MINIMUM=3.5 libff, as cmake deprecated 3.5
 
diff --git a/cli/cli.hs b/cli/cli.hs
@@ -576,7 +576,7 @@ launchExec cFileOpts execOpts cExecOpts cOpts = do
 vmFromCommand :: CommonOptions -> CommonExecOptions -> CommonFileOptions -> ExecOptions -> IO (VM Concrete RealWorld)
 vmFromCommand cOpts cExecOpts cFileOpts execOpts= do
   (miner,ts,baseFee,blockNum,prevRan) <- case cExecOpts.rpc of
-    Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
+    Nothing -> pure (LitAddr 0,Lit 0,0,Lit 0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
       Nothing -> do
         putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
@@ -665,7 +665,7 @@ vmFromCommand cOpts cExecOpts cFileOpts execOpts= do
           , priorityFee    = word (.priorityFee) 0
           , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
           , coinbase       = addr (.coinbase) miner
-          , number         = word (.number) blockNum
+          , number         = maybe blockNum Lit cExecOpts.number
           , timestamp      = Lit $ word (.timestamp) ts
           , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff
           , gasprice       = word (.gasprice) 0
@@ -688,7 +688,7 @@ vmFromCommand cOpts cExecOpts cFileOpts execOpts= do
 symvmFromCommand :: CommonExecOptions -> SymbolicOptions -> CommonFileOptions -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
 symvmFromCommand cExecOpts sOpts cFileOpts calldata = do
   (miner,blockNum,baseFee,prevRan) <- case cExecOpts.rpc of
-    Nothing -> pure (SymAddr "miner",0,0,0)
+    Nothing -> pure (SymAddr "miner",Lit 0,0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
       Nothing -> do
         putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
@@ -765,7 +765,7 @@ symvmFromCommand cExecOpts sOpts cFileOpts calldata = do
       , baseFee        = baseFee
       , priorityFee    = word (.priorityFee) 0
       , coinbase       = eaddr (.coinbase) miner
-      , number         = word (.number) blockNum
+      , number         = maybe blockNum Lit cExecOpts.number
       , timestamp      = ts
       , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff
       , gasprice       = word (.gasprice) 0
diff --git a/doc/src/limitations-and-workarounds.md b/doc/src/limitations-and-workarounds.md
@@ -105,3 +105,13 @@ WARNING: hevm was only able to partially explore the call prefix 0x[...] due to
 
 For these cases, we suggest concretizing the call that creates the contract,
 such that the bytecode created and later jumped to, is not symbolic.
+
+## Setting block number
+
+The [roll(uint256)
+cheatcode](https://book.getfoundry.sh/cheatcodes/roll?highlight=roll#roll) can
+be used to set the block number in the current EVM state. However, it does not
+alter the block number that the RPC calls use. For that, one must use the
+`--number` command line option. Hence, it is not possible to dynamically change
+what block number the RPC calls fetch from, other than by restarting the hevm
+process with a different block number.
diff --git a/src/EVM.hs b/src/EVM.hs
@@ -581,13 +581,21 @@ exec1 conf = do
               underrun
 
         OpBlockhash -> do
-          -- We adopt the fake block hash scheme of the VMTests,
-          -- so that blockhash(i) is the hash of i as decimal ASCII.
           stackOp1 g_blockhash $ \case
-            Lit i -> if i + 256 < vm.block.number || i >= vm.block.number
-                     then Lit 0
-                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit
+            Lit i -> case vm.block.number of
+              Lit vmBlockNumber ->
+                if i + 256 < vmBlockNumber || i >= vmBlockNumber
+                -- blockhash is 0 if block is too old or too new as per EVM spec
+                then Lit 0
+                -- We adopt the fake block hash scheme of the VMTests,
+                -- so that blockhash(i) is the hash of i as decimal ASCII.
+                else fakeBlockHash i
+              -- For symbolic block numbers, we don't know if it's too old or too new,
+              -- so we return fake block hash
+              _ -> fakeBlockHash i
             i -> BlockHash i
+            where
+              fakeBlockHash i = (into i :: Integer) & show & Char8.pack & keccak' & Lit
 
         OpCoinbase ->
           limitStack 1 . burn g_base $
@@ -599,7 +607,7 @@ exec1 conf = do
 
         OpNumber ->
           limitStack 1 . burn g_base $
-            next >> push vm.block.number
+            next >> pushSym vm.block.number
 
         OpPrevRandao -> do
           limitStack 1 . burn g_base $
@@ -1802,8 +1810,8 @@ cheatActions = Map.fromList
 
   , action "roll(uint256)" $
       \sig input -> case decodeStaticArgs 0 1 input of
-        [x] -> forceConcrete x "cannot roll to a symbolic block number" $ \block -> do
-          assign (#block % #number) block
+        [x] -> do
+          assign (#block % #number) x
           doStop
         _ -> vmError (BadCheatCode "roll(uint256) parameter decoding failed" sig)
 
diff --git a/src/EVM/Exec.hs b/src/EVM/Exec.hs
@@ -27,7 +27,7 @@ vmForEthrunCreation creationCode =
     , caller = LitAddr ethrunAddress
     , origin = LitAddr ethrunAddress
     , coinbase = LitAddr 0
-    , number = 0
+    , number = Lit 0
     , timestamp = Lit 0
     , blockGaslimit = 0
     , gasprice = 0
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
@@ -115,7 +115,7 @@ parseBlock :: (AsValue s, Show s) => s -> Maybe Block
 parseBlock j = do
   coinbase   <- LitAddr . readText <$> j ^? key "miner" % _String
   timestamp  <- Lit . readText <$> j ^? key "timestamp" % _String
-  number     <- readText <$> j ^? key "number" % _String
+  number     <- Lit . readText <$> j ^? key "number" % _String
   gasLimit   <- readText <$> j ^? key "gasLimit" % _String
   let
    baseFee = readText <$> j ^? key "baseFeePerGas" % _String
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
@@ -257,7 +257,7 @@ loadSymVM x callvalue cd create =
     , caller = SymAddr "caller"
     , origin = SymAddr "origin"
     , coinbase = SymAddr "coinbase"
-    , number = 0
+    , number = Lit 0
     , timestamp = Lit 0
     , blockGaslimit = 0
     , gasprice = 0
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
@@ -826,7 +826,7 @@ data Env = Env
 data Block = Block
   { coinbase    :: Expr EAddr
   , timestamp   :: Expr EWord
-  , number      :: W256
+  , number      :: Expr EWord
   , prevRandao  :: W256
   , gaslimit    :: Word64
   , baseFee     :: W256
@@ -1004,7 +1004,7 @@ data VMOpts (t :: VMType) = VMOpts
   , origin :: Expr EAddr
   , gas :: Gas t
   , gaslimit :: Word64
-  , number :: W256
+  , number :: Expr EWord
   , timestamp :: Expr EWord
   , coinbase :: Expr EAddr
   , prevRandao :: W256
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
@@ -418,7 +418,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = do
            , gas = toGas testParams.gasCreate
            , gaslimit = testParams.gasCreate
            , coinbase = testParams.coinbase
-           , number = testParams.number
+           , number = Lit testParams.number
            , timestamp = Lit testParams.timestamp
            , blockGaslimit = testParams.gaslimit
            , gasprice = testParams.gasprice
@@ -444,7 +444,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = do
 paramsFromRpc :: Fetch.RpcInfo -> IO TestVMParams
 paramsFromRpc rpcinfo = do
   (miner,ts,blockNum,ran,limit,base) <- case rpcinfo of
-    Nothing -> pure (SymAddr "miner", Lit 0, 0, 0, 0, 0)
+    Nothing -> pure (SymAddr "miner", Lit 0, Lit 0, 0, 0, 0)
     Just (block, url) -> Fetch.fetchBlockFrom block url >>= \case
       Nothing -> internalError "Could not fetch block"
       Just Block{..} -> pure ( coinbase
@@ -467,7 +467,7 @@ paramsFromRpc rpcinfo = do
     , priorityFee = 0
     , balanceCreate = defaultBalanceForTestContract
     , coinbase = miner
-    , number = blockNum
+    , number = forceLit blockNum
     , timestamp = ts'
     , gaslimit = limit
     , gasprice = 0
diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs
@@ -444,7 +444,7 @@ fromBlockchainCase' block tx preState postState =
        , baseFee        = block.baseFee
        , priorityFee    = priorityFee tx block.baseFee
        , gaslimit       = tx.gasLimit
-       , number         = block.number
+       , number         = Lit block.number
        , timestamp      = Lit block.timestamp
        , coinbase       = LitAddr block.coinbase
        , prevRandao     = block.mixHash
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
@@ -144,7 +144,7 @@ instance JSON.FromJSON EVMToolTraceOutput
 data EVMToolEnv = EVMToolEnv
   { coinbase    :: Addr
   , timestamp   :: Expr EWord
-  , number      :: W256
+  , number      :: Expr EWord
   , gasLimit    :: Data.Word.Word64
   , baseFee     :: W256
   , maxCodeSize :: W256
@@ -158,7 +158,7 @@ data EVMToolEnv = EVMToolEnv
 instance JSON.ToJSON EVMToolEnv where
   toJSON b = JSON.object [ ("currentCoinBase"  , (JSON.toJSON b.coinbase))
                          , ("currentGasLimit"  , (JSON.toJSON ("0x" ++ showHex (into @Integer b.gasLimit) "")))
-                         , ("currentNumber"    , (JSON.toJSON b.number))
+                         , ("currentNumber"    , (JSON.toJSON number))
                          , ("currentTimestamp" , (JSON.toJSON tstamp))
                          , ("currentBaseFee"   , (JSON.toJSON b.baseFee))
                          , ("blockHashes"      , (JSON.toJSON b.blockHashes))
@@ -171,11 +171,15 @@ instance JSON.ToJSON EVMToolEnv where
                 tstamp = case (b.timestamp) of
                               Lit a -> a
                               _ -> internalError "Timestamp needs to be a Lit"
+                number :: W256
+                number = case (b.number) of
+                              Lit a -> a
+                              _ -> internalError "Timestamp needs to be a Lit"
 
 emptyEvmToolEnv :: EVMToolEnv
 emptyEvmToolEnv = EVMToolEnv { coinbase = 0
                              , timestamp = Lit 0
-                             , number     = 0
+                             , number     = Lit 0
                              , gasLimit   = 0xffffffffffffffff
                              , baseFee    = 0
                              , maxCodeSize= 0xffffffff
@@ -287,7 +291,7 @@ evmSetup contr txData gaslimitExec = (txn, evmEnv, contrAlloc, fromAddress, toAd
       }
     evmEnv = EVMToolEnv { coinbase      = 0xff
                         , timestamp     = Lit 0x3e8
-                        , number        = 0x0
+                        , number        = Lit 0
                         , gasLimit      = unsafeInto gaslimitExec
                         , baseFee       = 0x0
                         , maxCodeSize   = 0xfffff
diff --git a/test/rpc.hs b/test/rpc.hs
@@ -11,7 +11,7 @@ import Data.Text (Text)
 import Data.Vector qualified as V
 
 import Optics.Core
-import EVM (makeVm, symbolify)
+import EVM (makeVm, symbolify, forceLit)
 import EVM.ABI
 import EVM.Fetch
 import EVM.SMT
@@ -42,28 +42,28 @@ tests = testGroup "rpc"
         let block = BlockNumber 15537392
         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case
                       Nothing -> internalError "Could not fetch block"
-                      Just Block{..} -> return ( coinbase
+                      Just Block{..} -> pure ( coinbase
                                                    , number
                                                    , baseFee
                                                    , prevRandao
                                                    )
 
         assertEqual "coinbase" (LitAddr 0xea674fdde714fd979de3edf0f56aa9716b898ec8) cb
-        assertEqual "number" (BlockNumber numb) block
+        assertEqual "number" (BlockNumber (forceLit numb)) block
         assertEqual "basefee" 38572377838 basefee
         assertEqual "prevRan" 11049842297455506 prevRan
     , testCase "post-merge-block" $ do
         let block = BlockNumber 16184420
         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case
                       Nothing -> internalError "Could not fetch block"
-                      Just Block{..} -> return ( coinbase
+                      Just Block{..} -> pure ( coinbase
                                                    , number
                                                    , baseFee
                                                    , prevRandao
                                                    )
 
         assertEqual "coinbase" (LitAddr 0x690b9a9e9aa1c9db991c7721a92d351db4fac990) cb
-        assertEqual "number" (BlockNumber numb) block
+        assertEqual "number" (BlockNumber (forceLit numb)) block
         assertEqual "basefee" 22163046690 basefee
         assertEqual "prevRan" 0x2267531ab030ed32fd5f2ef51f81427332d0becbd74fe7f4cd5684ddf4b287e0 prevRan
     ]
@@ -125,7 +125,7 @@ vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> I
 vmFromRpc blockNum calldata callvalue caller address = do
   ctrct <- fetchContractFrom (BlockNumber blockNum) testRpc address >>= \case
         Nothing -> internalError $ "contract not found: " <> show address
-        Just contract' -> return contract'
+        Just contract' -> pure contract'
 
   blk <- fetchBlockFrom (BlockNumber blockNum) testRpc >>= \case
     Nothing -> internalError "could not fetch block"
diff --git a/test/test.hs b/test/test.hs
@@ -2232,6 +2232,20 @@ tests = testGroup "hevm"
             |]
         (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
         putStrLnM "Require works as expected"
+     , test "symbolic-block-number" $ do
+       Just c <- solcRuntime "C" [i|
+           interface Vm {
+               function roll(uint) external;
+           }
+           contract C {
+             function myfun(uint x, uint y) public {
+               Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+               vm.roll(x);
+               assert(block.number == y);
+             }
+           } |]
+       (e, [Cex _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+       assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial e)
      , test "symbolic-to-concrete-multi" $ do
         Just c <- solcRuntime "MyContract"
             [i|
