Abstract gas v3

cli/cli.hs

@@ -41,7 +41,8 @@ import EVM.Solvers
 import EVM.Stepper qualified
 import EVM.SymExec
 import EVM.Transaction qualified
-import EVM.Types hiding (word, Env)
+import EVM.Types hiding (word, Env, Symbolic)
+import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
 
@@ -405,7 +406,7 @@ launchExec cmd = do
         internalError "no EVM result"
 
 -- | Creates a (concrete) VM from command line options
-vmFromCommand :: Command Options.Unwrapped -> IO (VM RealWorld)
+vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld)
 vmFromCommand cmd = do
   (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of
     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
@@ -490,14 +491,13 @@ vmFromCommand cmd = do
           , baseState      = EmptyBase
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
-          , symbolic       = False
           }
         word f def = fromMaybe def (f cmd)
         word64 f def = fromMaybe def (f cmd)
         addr f def = maybe def LitAddr (f cmd)
         bytes f def = maybe def decipher (f cmd)
 
-symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM RealWorld)
+symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
 symvmFromCommand cmd calldata = do
   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of
     Nothing -> pure (SymAddr "miner",0,0,0)
@@ -555,7 +555,7 @@ symvmFromCommand cmd calldata = do
       , address        = address
       , caller         = caller
       , origin         = origin
-      , gas            = word64 (.gas) 0xffffffffffffffff
+      , gas            = ()
       , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
       , baseFee        = baseFee
       , priorityFee    = word (.priorityFee) 0
@@ -572,7 +572,6 @@ symvmFromCommand cmd calldata = do
       , baseState      = maybe AbstractBase parseInitialStorage (cmd.initialStorage)
       , txAccessList   = mempty
       , allowFFI       = False
-      , symbolic       = True
       }
     word f def = fromMaybe def (f cmd)
     word64 f def = fromMaybe def (f cmd)

hevm.cabal

@@ -59,6 +59,8 @@ common shared
     -Wno-orphans
     -Wno-ambiguous-fields
     -optc-Wno-ignored-attributes
+    -fspecialize-aggressively
+    -fexpose-all-unfoldings
   default-language: GHC2021
   default-extensions:
     DuplicateRecordFields