Merge pull request #639 from ethereum/gas-fixes

Gas fixes

Author: msooseth

src/EVM/SMT.hs

@@ -9,7 +9,7 @@ module EVM.SMT where
 import Prelude hiding (LT, GT)
 
 import Control.Monad
-import Data.Containers.ListUtils (nubOrd)
+import Data.Containers.ListUtils (nubOrd, nubInt)
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.List qualified as List
@@ -28,6 +28,7 @@ import Data.Text.Lazy (Text)
 import Data.Text qualified as TS
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.Builder
+import Data.Text.Read (decimal)
 import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
 import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
 import Numeric (readHex, readBin)
@@ -232,6 +233,7 @@ assertPropsNoSimp psPreConc = do
   <> smt2Line ""
   <> keccakAssertions'
   <> readAssumes'
+  <> gasOrder
   <> smt2Line ""
   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
   <> SMT2 smt mempty mempty
@@ -256,6 +258,7 @@ assertPropsNoSimp psPreConc = do
     allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals <> [abstrVars abst]
     frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals
     blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals
+    gasOrder = enforceGasOrder psPreConc
 
     abstrVars :: AbstState -> [Builder]
     abstrVars (AbstState b _) = map ((\v->fromString ("abst_" ++ show v)) . snd) (Map.toList b)
@@ -321,7 +324,7 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
     go = \case
       TxValue -> [(fromString "txvalue", [])]
       v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]
-      Gas {} -> internalError "TODO: GAS"
+      Gas freshVar -> [(fromString ("gas_" <> show freshVar), [])]
       _ -> []
 
 referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
@@ -438,6 +441,22 @@ declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cex
     declare n = "(declare-fun " <> n <> " () Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
+enforceGasOrder :: [Prop] -> SMT2
+enforceGasOrder ps = SMT2 (["; gas ordering"] <> order indices) mempty mempty
+  where
+    order :: [Int] -> [Builder]
+    order n = consecutivePairs n >>= \(x, y)->
+      -- The GAS instruction itself costs gas, so it's strictly decreasing
+      ["(assert (bvugt gas_" <> (fromString . show $ x) <> " gas_" <> (fromString . show $ y) <> "))"]
+    consecutivePairs :: [Int] -> [(Int, Int)]
+    consecutivePairs [] = []
+    consecutivePairs l = zip l (tail l)
+    indices :: [Int] = nubInt $ concatMap (foldProp go mempty) ps
+    go :: Expr a -> [Int]
+    go e = case e of
+      Gas freshVar -> [freshVar]
+      _ -> []
+
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
 declareFrameContext names = do
   decls <- concatMapM declare names
@@ -850,6 +869,7 @@ exprToSMT = \case
     encPrev <- exprToSMT prev
     pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
   SLoad idx store -> op2 "select" store idx
+  Gas freshVar -> pure $ fromLazyText $ "gas_"  <> (T.pack $ show freshVar)
 
   a -> internalError $ "TODO: implement: " <> show a
   where
@@ -1022,6 +1042,11 @@ parseEAddr name
   | Just a <- TS.stripPrefix "symaddr_" name = SymAddr a
   | otherwise = internalError $ "cannot parse: " <> show name
 
+textToInt :: TS.Text -> Int
+textToInt text = case decimal text of
+  Right (value, _) -> value
+  Left _ -> internalError $ "cannot parse '" <> (TS.unpack text) <> "' into an Int"
+
 parseBlockCtx :: TS.Text -> Expr EWord
 parseBlockCtx "origin" = Origin
 parseBlockCtx "coinbase" = Coinbase
@@ -1031,12 +1056,14 @@ parseBlockCtx "prevrandao" = PrevRandao
 parseBlockCtx "gaslimit" = GasLimit
 parseBlockCtx "chainid" = ChainId
 parseBlockCtx "basefee" = BaseFee
-parseBlockCtx t = internalError $ "cannot parse " <> (TS.unpack t) <> " into an Expr"
+parseBlockCtx gas | TS.isPrefixOf (TS.pack "gas_") gas = Gas (textToInt $ TS.drop 4 gas)
+parseBlockCtx val = internalError $ "cannot parse '" <> (TS.unpack val) <> "' into an Expr"
 
 parseTxCtx :: TS.Text -> Expr EWord
 parseTxCtx name
   | name == "txvalue" = TxValue
   | Just a <- TS.stripPrefix "balance_" name = Balance (parseEAddr a)
+  | Just a <- TS.stripPrefix "gas_" name = Gas (textToInt a)
   | otherwise = internalError $ "cannot parse " <> (TS.unpack name) <> " into an Expr"
 
 getAddrs :: (TS.Text -> Expr EAddr) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EAddr) Addr)

src/EVM/Types.hs

@@ -286,7 +286,7 @@ data Expr (a :: EType) where
 
   Balance        :: Expr EAddr -> Expr EWord
 
-  Gas            :: Int                -- frame idx
+  Gas            :: Int                -- fresh gas variable
                  -> Expr EWord
 
   -- code

test/test.hs

@@ -1168,8 +1168,21 @@ tests = testGroup "hevm"
              |]
          (_, [Cex _]) <- withSolvers Bitwuzla 1 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
          putStrLnM "expected counterexample found"
-      ,
-     test "enum-conversion-fail" $ do
+     , test "gas-decrease-monotone" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(uint8 a) external {
+                uint a = gasleft();
+                uint b = gasleft();
+                assert(a > b);
+              }
+             }
+            |]
+        let sig = (Just (Sig "fun(uint8)" [AbiUIntType 8]))
+        (_, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        putStrLnM "expected Qed found"
+     , test "enum-conversion-fail" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {