Merge branch 'master' into pi2/robertorosmaninho/eip-4844-blobhash-op…

…code
runtimeverification · Jan 23, 2025 · a0d834b · a0d834b
2 parents f18175d + 61b8f9e
commit a0d834b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -809,16 +809,17 @@ These are just used by the other operators for shuffling local execution state a
            <acctID> ACCT  </acctID>
            <code>   CODE  </code>
            <nonce>  NONCE </nonce>
+           <storage> STORAGE </storage>
            ...
          </account>
-      requires CODE =/=K .Bytes orBool NONCE =/=Int 0
+      requires CODE =/=K .Bytes orBool NONCE =/=Int 0 orBool STORAGE =/=K .Map
 
     rule <k> #newExistingAccount ACCT => .K ... </k>
          <account>
            <acctID>      ACCT      </acctID>
            <code>        CODE      </code>
            <nonce>       0         </nonce>
-           <storage>     _ => .Map </storage>
+           <storage>     .Map   </storage>
            <origStorage> _ => .Map </origStorage>
            ...
          </account>

diff --git a/tests/failing.llvm b/tests/failing.llvm
@@ -133,14 +133,11 @@ BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/zero_amou
 BlockchainTests/GeneralStateTests/stBadOpcode/opc49DiffPlaces.json,*
 BlockchainTests/GeneralStateTests/stBadOpcode/opc4ADiffPlaces.json,*
 BlockchainTests/GeneralStateTests/stBadOpcode/undefinedOpcodeFirstByte.json,*
-BlockchainTests/GeneralStateTests/stCreate2/create2collisionStorageParis.json,*
-BlockchainTests/GeneralStateTests/stCreate2/RevertInCreateInInitCreate2Paris.json,*
 BlockchainTests/GeneralStateTests/stEIP1559/lowFeeCap.json,*
 BlockchainTests/GeneralStateTests/stEIP1559/lowGasLimit.json,lowGasLimit_d0g0v0_Cancun
 BlockchainTests/GeneralStateTests/stEIP1559/lowGasPriceOldTypes.json,*
 BlockchainTests/GeneralStateTests/stEIP1559/tipTooHigh.json,*
 BlockchainTests/GeneralStateTests/stEIP1559/transactionIntinsicBug_Paris.json,*
-BlockchainTests/GeneralStateTests/stExtCodeHash/dynamicAccountOverwriteEmpty_Paris.json,*
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/idPrecomps.json,idPrecomps_d9g0v0_Cancun
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d117g0v0_Cancun
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d12g0v0_Cancun
@@ -164,6 +161,4 @@ BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.j
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d63g0v0_Cancun
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d81g0v0_Cancun
 BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d99g0v0_Cancun
-BlockchainTests/GeneralStateTests/stRevertTest/RevertInCreateInInit_Paris.json,*
 BlockchainTests/GeneralStateTests/stSpecialTest/failed_tx_xcf416c53_Paris.json,*
-BlockchainTests/GeneralStateTests/stSStoreTest/InitCollisionParis.json,*