Merge branch 'main' into propogate-constraints

.github/workflows/build.yml

@@ -23,7 +23,7 @@ jobs:
  runs-on: ${{ matrix.os }}
  steps:
  - uses: actions/checkout@v3
- - uses: cachix/install-nix-action@v20
+ - uses: cachix/install-nix-action@v21
  with:
  nix_path: nixpkgs=channel:nixos-unstable
  extra_nix_config: |

.github/workflows/check-dependencies.yml

@@ -13,7 +13,7 @@ jobs:
  runs-on: ubuntu-latest
  steps:
  - uses: actions/checkout@v3
- - uses: cachix/install-nix-action@v19
+ - uses: cachix/install-nix-action@v21
  with:
  nix_path: nixpkgs=channel:nixos-unstable
  extra_nix_config: |

.github/workflows/publish-docs.yml

@@ -12,7 +12,7 @@ jobs:
  with:
  submodules: recursive
 
- - uses: cachix/install-nix-action@v18
+ - uses: cachix/install-nix-action@v21
 
  - name: build docs
  run: nix-shell --pure --command "cd doc && mdbook build"

.github/workflows/release.yml

@@ -29,7 +29,7 @@ jobs:
  runs-on: ubuntu-latest
  steps:
  - uses: actions/checkout@v3
- - uses: cachix/install-nix-action@v18
+ - uses: cachix/install-nix-action@v21
  with:
  nix_path: nixpkgs=channel:nixos-unstable
  extra_nix_config: |

CHANGELOG.md

@@ -12,6 +12,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - hevm now gracefully handles missing `out` directories
 - Constraints are correctly propogated to the final output expression during symbolic execution
 
+## Changed
+
+- HEVM is now fully compliant with the Shanghai hard fork
+
 ## [0.51.0] - 2023-04-27
 
 ## Added

flake.nix

@@ -16,7 +16,7 @@
  flake = false;
  };
  ethereum-tests = {
- url = "github:ethereum/tests/v11.2";
+ url = "github:ethereum/tests/v12.2";
  flake = false;
  };
  };

src/EVM.hs

@@ -98,7 +98,7 @@ makeVm o =
  let txaccessList = o.txAccessList
  txorigin = o.origin
  txtoAddr = o.address
- initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList)
+ initialAccessedAddrs = fromList $ [txorigin, txtoAddr, o.coinbase] ++ [1..9] ++ (Map.keys txaccessList)
  initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)
  touched = if o.create then [txorigin] else [txorigin, txtoAddr]
  in
@@ -238,6 +238,12 @@ exec1 = do
 
  case getOp(?op) of
 
+ OpPush0 -> do
+ limitStack 1 $
+ burn g_base $ do
+ next
+ pushSym (Lit 0)
+
  OpPush n' -> do
  let n = fromIntegral n'
  !xs = case vm.state.code of
@@ -621,9 +627,9 @@ exec1 = do
  refund (g_sreset + g_access_list_storage_key)
  else do
  when (original /= 0) $
- if new' == 0
- then refund (g_sreset + g_access_list_storage_key)
- else unRefund (g_sreset + g_access_list_storage_key)
+ if current' == 0
+ then unRefund (g_sreset + g_access_list_storage_key)
+ else when (new' == 0) $ refund (g_sreset + g_access_list_storage_key)
  when (original == new') $
  if original == 0
  then refund (g_sset - g_sload)
@@ -695,14 +701,11 @@ exec1 = do
  availableGas <- use (#state % #gas)
  let
  newAddr = createAddress self this.nonce
- (cost, gas') = costOfCreate fees availableGas 0
+ (cost, gas') = costOfCreate fees availableGas xSize False
  _ <- accessAccountForGas newAddr
- burn (cost - gas') $ do
- -- unfortunately we have to apply some (pretty hacky)
- -- heuristics here to parse the unstructured buffer read
- -- from memory into a code and data section
+ burn cost $ do
  let initCode = readMemory xOffset' xSize' vm
- create self this (num gas') xValue xs newAddr initCode
+ create self this xSize (num gas') xValue xs newAddr initCode
  _ -> underrun
 
  OpCall ->
@@ -794,9 +797,10 @@ exec1 = do
  \initCode -> do
  let
  newAddr = create2Address self xSalt initCode
- (cost, gas') = costOfCreate fees availableGas xSize
+ (cost, gas') = costOfCreate fees availableGas xSize True
  _ <- accessAccountForGas newAddr
- burn (cost - gas') $ create self this gas' xValue xs newAddr (ConcreteBuf initCode)
+ burn cost $
+ create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode)
  _ -> underrun
 
  OpStaticcall ->
@@ -1254,7 +1258,6 @@ finalize = do
 
  let
  sumRefunds = sum (snd <$> tx.substate.refunds)
- blockReward = num (block.schedule.r_block)
  gasUsed = tx.gaslimit - gasRemaining
  cappedRefund = min (quot gasUsed 5) (num sumRefunds)
  originPay = (num $ gasRemaining + cappedRefund) * tx.gasprice
@@ -1266,14 +1269,6 @@ finalize = do
  (Map.adjust (over #balance (+ minerPay)) block.coinbase)
  touchAccount block.coinbase
 
- -- pay out the block reward, recreating the miner if necessary
- preuse (#env % #contracts % ix block.coinbase) >>= \case
- Nothing -> modifying (#env % #contracts)
- (Map.insert block.coinbase (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))
- Just _ -> noop
- modifying (#env % #contracts)
- (Map.adjust (over #balance (+ blockReward)) block.coinbase)
-
  -- perform state trie clearing (EIP 161), of selfdestructs
  -- and touched accounts. addresses are cleared if they have
  -- a) selfdestructed, or
@@ -1627,8 +1622,8 @@ collision c' = case c' of
 
 create :: (?op :: Word8)
  => Addr -> Contract
- -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()
-create self this xGas' xValue xs newAddr initCode = do
+ -> W256 -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM ()
+create self this xSize xGas' xValue xs newAddr initCode = do
  vm0 <- get
  let xGas = num xGas'
  if this.nonce == num (maxBound :: Word64)
@@ -1643,6 +1638,11 @@ create self this xGas' xValue xs newAddr initCode = do
  assign (#state % #returndata) mempty
  pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance
  next
+ else if xSize > vm0.block.maxCodeSize * 2
+ then do
+ assign (#state % #stack) (Lit 0 : xs)
+ assign (#state % #returndata) mempty
+ vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize
  else if length vm0.frames >= 1024
  then do
  assign (#state % #stack) (Lit 0 : xs)
@@ -1662,7 +1662,6 @@ create self this xGas' xValue xs newAddr initCode = do
  -- unfortunately we have to apply some (pretty hacky)
  -- heuristics here to parse the unstructured buffer read
  -- from memory into a code and data section
- -- TODO: comment explaining whats going on here
  let contract' = do
  prefixLen <- Expr.concPrefix initCode
  prefix <- Expr.toList $ Expr.take (num prefixLen) initCode
@@ -2207,12 +2206,12 @@ costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas target =
 -- Gas cost of create, including hash cost if needed
 costOfCreate
  :: FeeSchedule Word64
- -> Word64 -> W256 -> (Word64, Word64)
-costOfCreate (FeeSchedule {..}) availableGas hashSize =
- (createCost + initGas, initGas)
+ -> Word64 -> W256 -> Bool -> (Word64, Word64)
+costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)
  where
- createCost = g_create + hashCost
- hashCost = g_sha3word * ceilDiv (num hashSize) 32
+ byteCost = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword
+ createCost = g_create + codeCost
+ codeCost = byteCost * (ceilDiv (num size) 32)
  initGas = allButOne64th (availableGas - createCost)
 
 concreteModexpGasFee :: ByteString -> Word64

src/EVM/Assembler.hs

@@ -106,4 +106,5 @@ assemble os = V.fromList $ concatMap go os
  else error $ "Internal Error: invalid argument to OpLog: " <> show n
  -- we just always assemble OpPush into PUSH32
  OpPush wrd -> (LitByte 0x7f) : [Expr.indexWord (Lit i) wrd | i <- [0..31]]
+ OpPush0 -> [LitByte 0x5f]
  OpUnknown o -> [LitByte o]

src/EVM/FeeSchedule.hs

@@ -35,6 +35,7 @@ data FeeSchedule n = FeeSchedule
  , g_logtopic :: n
  , g_sha3 :: n
  , g_sha3word :: n
+ , g_initcodeword :: n
  , g_copy :: n
  , g_blockhash :: n
  , g_extcodehash :: n
@@ -110,6 +111,7 @@ homestead = FeeSchedule
  , g_logtopic = 375
  , g_sha3 = 30
  , g_sha3word = 6
+ , g_initcodeword = 2
  , g_copy = 3
  , g_blockhash = 20
  , g_extcodehash = 400
@@ -173,8 +175,8 @@ istanbul = eip1108 . eip1884 . eip2028 . eip2200 $ metropolis
  -- <https:/ethereum/EIPs/blob/master/EIPS/eip-2929.md>
 eip2929 :: EIP n
 eip2929 fees = fees
- { g_sload = 100 
- , g_sreset = 5000 - 2100 
+ { g_sload = 100
+ , g_sreset = 5000 - 2100
  , g_call = 2600
  , g_balance = 2600
  , g_extcode = 2600

src/EVM/Format.hs

@@ -385,6 +385,7 @@ prettyError = \case
  StateChangeWhileStatic -> "State change while static"
  CallDepthLimitReached -> "Call depth limit reached"
  MaxCodeSizeExceeded a b -> "Max code size exceeded: max: " <> show a <> " actual: " <> show b
+ MaxInitCodeSizeExceeded a b -> "Max init code size exceeded: max: " <> show a <> " actual: " <> show b
  InvalidFormat -> "Invalid Format"
  PrecompileFailure -> "Precompile failure"
  ReturnDataOutOfBounds -> "Return data out of bounds"

src/EVM/Op.hs

@@ -86,6 +86,7 @@ intToOpName a =
  0x5a -> "GAS"
  0x5b -> "JUMPDEST"
  --
+ 0x5f -> "PUSH0"
  0x60 -> "PUSH1"
  0x61 -> "PUSH2"
  0x62 -> "PUSH3"
@@ -250,6 +251,7 @@ opString (i, o) = let showPc x | x < 0x10 = '0' : showHex x ""
  OpDup x -> "DUP" ++ show x
  OpSwap x -> "SWAP" ++ show x
  OpLog x -> "LOG" ++ show x
+ OpPush0 -> "PUSH0"
  OpPush x -> case x of
  Lit x' -> "PUSH 0x" ++ (showHex x' "")
  _ -> "PUSH " ++ show x
@@ -332,6 +334,7 @@ getOp x = case x of
  0x59 -> OpMsize
  0x5a -> OpGas
  0x5b -> OpJumpdest
+ 0x5f -> OpPush0
  0xf0 -> OpCreate
  0xf1 -> OpCall
  0xf2 -> OpCallcode

src/EVM/Transaction.hs

@@ -2,7 +2,7 @@ module EVM.Transaction where
 
 import Prelude hiding (Word)
 
-import EVM (initialContract)
+import EVM (initialContract, ceilDiv)
 import EVM.FeeSchedule
 import EVM.RLP
 import EVM.Types
@@ -185,10 +185,11 @@ txGasCost fs tx =
  zeroBytes = BS.count 0 calldata
  nonZeroBytes = BS.length calldata - zeroBytes
  baseCost = fs.g_transaction
- + (if isNothing tx.toAddr then fs.g_txcreate else 0)
+ + (if isNothing tx.toAddr then fs.g_txcreate + initcodeCost else 0)
  + (accessListPrice fs tx.accessList )
  zeroCost = fs.g_txdatazero
  nonZeroCost = fs.g_txdatanonzero
+ initcodeCost = fs.g_initcodeword * num (ceilDiv (BS.length calldata) 32)
  in baseCost + zeroCost * (fromIntegral zeroBytes) + nonZeroCost * (fromIntegral nonZeroBytes)
 
 instance FromJSON AccessListEntry where

src/EVM/Types.hs

@@ -502,6 +502,7 @@ data EvmError
  | InvalidMemoryAccess
  | CallDepthLimitReached
  | MaxCodeSizeExceeded W256 W256
+ | MaxInitCodeSizeExceeded W256 W256
  | InvalidFormat
  | PrecompileFailure
  | ReturnDataOutOfBounds
@@ -931,6 +932,7 @@ data GenericOp a
  | OpDup !Word8
  | OpSwap !Word8
  | OpLog !Word8
+ | OpPush0
  | OpPush a
  | OpUnknown Word8
  deriving (Show, Eq, Functor)