Shanghai Schedule Update (#1907)

* add SHANGHAI schedule * EIP-3561: warm coinbase * EIP-3855: PUSHZERO instruction * EIP-3860: initcode limit and metering * EIP-4895: withdrawals * fix eips * Set Version: 1.0.210 * cleanup * update expected files for interactive tests * Set Version: 1.0.211 * Set Version: 1.0.211 * update schedule in python test * Set Version: 1.0.215 * update accesslist_proto.bin.expected * update configuration for tests * add PUSHZERO optimization * Set Version: 1.0.218 * Set Version: 1.0.219 * Set Version: 1.0.220 * fix test expected output * Set Version: 1.0.221 * Set Version: 1.0.228 * update expected files for gst_to_kore * update schedule in kevm pyk * update log3_MaxTopic.parse-expected * Set Version: 1.0.229 * fix schedule in Makefile * Set Version: 1.0.237 * Set Version: 1.0.238 * Set Version: 1.0.239 * Set Version: 1.0.240 * Set Version: 1.0.242 * update expected output for foundry-prove * Set Version: 1.0.243 * Set Version: 1.0.249 * Set Version: 1.0.251 * set default schedule to shanghai in tests/specs/examples * Set Version: 1.0.252 * set default schedule for foundry * Set Version: 1.0.253 * Foundry/forge+solc nix fixes (#2008) * Fix solc version * cleanup * Set Version: 1.0.251 * switch to patched version of solc.nix * switched back to github:hellwolf/solc.nix * Set Version: 1.0.252 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> * Set Version: 1.0.253 * Set Version: 1.0.257 * update expected output of foundry-tests * update-expected output in kevm-pyk * Set Version: 1.0.259 * Set Version: 1.0.261 * Set Version: 1.0.286 * Set Version: 1.0.290 * Update test-pr.yml Increase timeout of tests * Revert "set default schedule to shanghai in tests/specs/examples" This reverts commit 341173e. * Update test-pr.yml Return timeouts to original. * Update test-pr.yml * review suggestions * Set Version: 1.0.291 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Freeman <[email protected]>
runtimeverification · Sep 13, 2023 · 4fad7d9 · 4fad7d9
1 parent 86adf32
commit 4fad7d9
Show file tree

Hide file tree

Showing 148 changed files with 432 additions and 154 deletions.
diff --git a/Makefile b/Makefile
@@ -312,7 +312,7 @@ TEST_SYMBOLIC_BACKEND := haskell
 CHECK := git --no-pager diff --no-index --ignore-all-space -R
 
 KEVM_MODE     := NORMAL
-KEVM_SCHEDULE := MERGE
+KEVM_SCHEDULE := SHANGHAI
 KEVM_CHAINID  := 1
 
 KPROVE_MODULE  = VERIFICATION

diff --git a/README.md b/README.md
@@ -253,7 +253,7 @@ make build-llvm KEVM_OPTS=--enable-llvm-debug
 To debug a conformance test, add the `--debugger` flag to the command:
 
 ```sh
-kevm run tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --target llvm --mode NORMAL --schedule MERGE --chainid 1 --debugger
+kevm run tests/ethereum-tests/BlockchainTests/GeneralStateTests/stExample/add11.json --target llvm --mode NORMAL --schedule SHANGHAI --chainid 1 --debugger
 ```
 
 ### Keeping in mind while developing

diff --git a/include/kframework/asm.md b/include/kframework/asm.md
@@ -117,6 +117,7 @@ Operator `#revOps` can be used to reverse a program.
     rule #asmOpCode( MSIZE          ) =>  89
     rule #asmOpCode( GAS            ) =>  90
     rule #asmOpCode( JUMPDEST       ) =>  91
+    rule #asmOpCode( PUSHZERO       ) =>  95
     rule #asmOpCode( PUSH(1)        ) =>  96
     rule #asmOpCode( PUSH(2)        ) =>  97
     rule #asmOpCode( PUSH(3)        ) =>  98

diff --git a/include/kframework/driver.md b/include/kframework/driver.md
@@ -64,8 +64,6 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 -   `loadTx(_)` loads the next transaction to be executed into the current state.
 -   `finishTx` is a place-holder for performing necessary cleanup after a transaction.
 
-**TODO**: `loadTx(_) => loadTx_`
-
 ```k
     syntax EthereumCommand ::= "startTx"
  // ------------------------------------
@@ -84,6 +82,17 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 
     syntax EthereumCommand ::= loadTx ( Account )
  // ---------------------------------------------
+    rule <k> loadTx(_) => #end EVMC_OUT_OF_GAS ... </k>
+         <schedule> SCHED </schedule>
+         <txPending> ListItem(TXID:Int) ... </txPending>
+         <message>
+           <msgID>      TXID     </msgID>
+           <to>         .Account </to>
+           <data>       CODE     </data>
+           ...
+         </message>
+       requires notBool #hasValidInitCode(lengthBytes(CODE), SCHED)
+
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccounts(SCHED)
           ~> #loadAccessList(TA)
@@ -113,8 +122,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <nonce> NONCE </nonce>
            ...
          </account>
-         <accessedAccounts> _ => .Set </accessedAccounts>
+         <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
+      requires #hasValidInitCode(lengthBytes(CODE), SCHED)
 
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM ACCTTO #precompiledAccounts(SCHED)
@@ -145,7 +155,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <nonce> NONCE => NONCE +Int 1 </nonce>
            ...
          </account>
-         <accessedAccounts> _ => .Set </accessedAccounts>
+         <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires ACCTTO =/=K .Account
 
@@ -261,7 +271,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
 ```k
     syntax Set ::= "#loadKeys" [function]
  // -------------------------------------
-    rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("network") SetItem("genesisRLP") )
+    rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("network") SetItem("genesisRLP") SetItem("withdrawals") )
 
     rule <k> run  TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
       requires KEY in #loadKeys
@@ -459,7 +469,7 @@ Here we check the other post-conditions associated with an EVM test.
       requires KEY in ( SetItem("coinbase") SetItem("difficulty") SetItem("gasLimit") SetItem("gasUsed")
                         SetItem("mixHash") SetItem("nonce") SetItem("number") SetItem("parentHash")
                         SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
-                        SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas")
+                        SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas") SetItem("withdrawalsRoot")
                       )
 
     rule <k> check "blockHeader" : { "bloom"            : VALUE } => . ... </k> <logsBloom>        VALUE </logsBloom>
@@ -478,6 +488,7 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "blockHeader" : { "transactionsTrie" : VALUE } => . ... </k> <transactionsRoot> VALUE </transactionsRoot>
     rule <k> check "blockHeader" : { "uncleHash"        : VALUE } => . ... </k> <ommersHash>       VALUE </ommersHash>
     rule <k> check "blockHeader" : { "baseFeePerGas"    : VALUE } => . ... </k> <baseFee>          VALUE </baseFee>
+    rule <k> check "blockHeader" : { "withdrawalsRoot"  : VALUE } => . ... </k> <withdrawalsRoot>  VALUE </withdrawalsRoot>
 
     rule <k> check "blockHeader" : { "hash": HASH:Bytes } => . ...</k>
          <previousHash>     HP </previousHash>
@@ -496,8 +507,10 @@ Here we check the other post-conditions associated with an EVM test.
          <mixHash>          HM </mixHash>
          <blockNonce>       HN </blockNonce>
          <baseFee>          HF </baseFee>
-      requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)     ==Int #asWord(HASH)
-        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF) ==Int #asWord(HASH)
+         <withdrawalsRoot>  WR </withdrawalsRoot>
+      requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)         ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF)     ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR) ==Int #asWord(HASH)
 
     rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
  // ------------------------------------------------------------------------------------------------------------------------

diff --git a/include/kframework/evm.md b/include/kframework/evm.md
@@ -108,6 +108,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
               <mixHash>          0      </mixHash>          // I_Hm
               <blockNonce>       0      </blockNonce>       // I_Hn
               <baseFee>          0      </baseFee>
+              <withdrawalsRoot>  0      </withdrawalsRoot>
 
               <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
             </block>
@@ -357,7 +358,7 @@ The `#next [_]` operator initiates execution by:
 
     syntax Int ::= #stackNeeded ( OpCode ) [function]
  // -------------------------------------------------
-    rule #stackNeeded(PUSH(_))          => 0
+    rule #stackNeeded(_POP:PushOp)      => 0
     rule #stackNeeded(_IOP:InvalidOp)   => 0
     rule #stackNeeded(_NOP:NullStackOp) => 0
     rule #stackNeeded(_UOP:UnStackOp)   => 1
@@ -845,8 +846,11 @@ Some operators don't calculate anything, they just push the stack around a bit.
     rule <k> DUP(N)  WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS)                      ... </k>
     rule <k> SWAP(N) (W0 : WS)    => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... </k>
 
-    syntax PushOp ::= PUSH ( Int )
+    syntax PushOp ::= "PUSHZERO"
+                    | PUSH ( Int )
  // ------------------------------
+    rule <k> PUSHZERO => 0 ~> #push ... </k>
+
     rule <k> PUSH(N) => #asWord(#range(PGM, PCOUNT +Int 1, N)) ~> #push ... </k>
          <pc> PCOUNT </pc>
          <program> PGM </program>
@@ -1457,6 +1461,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 -   `#create____` transfers the endowment to the new account and triggers the execution of the initialization code.
 -   `#codeDeposit_` checks the result of initialization code and whether the code deposit can be paid, indicating an error if not.
 -   `#isValidCode_` checks if the code returned by the execution of the initialization code begins with a reserved byte. [EIP-3541]
+-   `#hasValidInitCode` checks the length of the transaction data in a create transaction. [EIP-3860]
 
 ```k
     syntax InternalOp ::= "#create"   Int Int Int Bytes
@@ -1497,6 +1502,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
            ...
          </account>
 
+    syntax Bool ::= #hasValidInitCode ( Int , Schedule ) [function]
+ // ---------------------------------------------------------------
+    rule #hasValidInitCode(INITCODELEN, SCHED) => notBool Ghasmaxinitcodesize << SCHED >> orBool INITCODELEN <=Int maxInitCodeSize < SCHED >
+
     syntax Bool ::= #isValidCode ( Bytes , Schedule ) [function]
  // ------------------------------------------------------------
     rule #isValidCode( OUT ,  SCHED) => Ghasrejectedfirstbyte << SCHED >> impliesBool OUT[0] =/=Int 239 requires lengthBytes(OUT) >Int 0
@@ -1562,7 +1571,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
 ```k
     syntax TernStackOp ::= "CREATE"
  // -------------------------------
-    rule [create]:
+    rule [create-valid]:
          <k> CREATE VALUE MEMSTART MEMWIDTH
           => #accessAccounts #newAddr(ACCT, NONCE)
           ~> #checkCall ACCT VALUE
@@ -1577,14 +1586,19 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
            <nonce> NONCE </nonce>
            ...
          </account>
+         <schedule> SCHED </schedule>
+      requires #hasValidInitCode(MEMWIDTH, SCHED)
+
+    rule [create-invalid]:
+         <k> CREATE _ _ _ => #end EVMC_OUT_OF_GAS ... </k> [owise]
 ```
 
 `CREATE2` will attempt to `#create` the account, but with the new scheme for choosing the account address.
 
 ```k
     syntax QuadStackOp ::= "CREATE2"
  // --------------------------------
-    rule [create2]:
+    rule [create2-valid]:
          <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
           => #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
           ~> #checkCall ACCT VALUE
@@ -1594,6 +1608,11 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
          </k>
          <id> ACCT </id>
          <localMem> LM </localMem>
+         <schedule> SCHED </schedule>
+      requires #hasValidInitCode( MEMWIDTH /Int 2, SCHED)
+
+    rule [create2-invalid]:
+         <k> CREATE2 _ _ _ _ => #end EVMC_OUT_OF_GAS ... </k> [owise]
 ```
 
 `SELFDESTRUCT` marks the current account for deletion and transfers funds out of the current account.
@@ -1657,6 +1676,7 @@ Precompiled Contracts
     rule #precompiledAccounts(BERLIN)            => #precompiledAccounts(ISTANBUL)
     rule #precompiledAccounts(LONDON)            => #precompiledAccounts(BERLIN)
     rule #precompiledAccounts(MERGE)             => #precompiledAccounts(LONDON)
+    rule #precompiledAccounts(SHANGHAI)          => #precompiledAccounts(MERGE)
 ```
 
 -   `ECREC` performs ECDSA public key recovery.
@@ -2014,14 +2034,14 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
            ...
          </account>
 
-    rule <k> #gasExec(SCHED, CREATE _ _ _)
-          => Gcreate < SCHED > ~> #deductGas
+    rule <k> #gasExec(SCHED, CREATE _ _ WIDTH)
+          => Gcreate < SCHED > +Int Cinitcode(SCHED, WIDTH) ~> #deductGas
           ~> #allocateCreateGas ~> 0
          ...
          </k>
 
     rule <k> #gasExec(SCHED, CREATE2 _ _ WIDTH _)
-          => Gcreate < SCHED > +Int Gsha3word < SCHED > *Int (WIDTH up/Int 32) ~> #deductGas
+          => Gcreate < SCHED > +Int Gsha3word < SCHED > *Int (WIDTH up/Int 32) +Int Cinitcode(SCHED, WIDTH) ~> #deductGas
           ~> #allocateCreateGas ~> 0
          ...
          </k>
@@ -2056,6 +2076,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
     rule <k> #gasExec(SCHED, BASEFEE)        => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, POP _)          => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, PC)             => Gbase < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, PUSHZERO)       => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, MSIZE)          => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, GAS)            => Gbase < SCHED > ... </k>
     rule <k> #gasExec(SCHED, CHAINID)        => Gbase < SCHED > ... </k>
@@ -2260,6 +2281,7 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  89,     _ ) => MSIZE
     rule #dasmOpCode(  90,     _ ) => GAS
     rule #dasmOpCode(  91,     _ ) => JUMPDEST
+    rule #dasmOpCode(  95, SCHED ) => PUSHZERO requires Ghaspushzero << SCHED >>
     rule #dasmOpCode(  96,     _ ) => PUSH(1)
     rule #dasmOpCode(  97,     _ ) => PUSH(2)
     rule #dasmOpCode(  98,     _ ) => PUSH(3)

diff --git a/include/kframework/gas.md b/include/kframework/gas.md
@@ -118,6 +118,7 @@ module GAS-FEES
                  | Cextcodehash   ( Schedule )                           [function, total, smtlib(gas_Cextcodehash)  ]
                  | Cbalance       ( Schedule )                           [function, total, smtlib(gas_Cbalance)      ]
                  | Cmodexp        ( Schedule , Bytes , Int , Int , Int ) [function, total, smtlib(gas_Cmodexp)       ]
+                 | Cinitcode      ( Schedule , Int )                     [function, total, smtlib(gas_Cinitcode)     ]
  // ------------------------------------------------------------------------------------------------------------------
     rule [Cgascap]:
          Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA)
@@ -202,6 +203,9 @@ module GAS-FEES
       requires Ghasaccesslist << SCHED >>
       [concrete]
 
+    rule [Cinitcode.new]: Cinitcode(SCHED, INITCODELEN) => Ginitcodewordcost < SCHED > *Int ( INITCODELEN up/Int 32 ) requires         Ghasmaxinitcodesize << SCHED >> [concrete]
+    rule [Cinitcode.old]: Cinitcode(SCHED, _)           => 0                                                          requires notBool Ghasmaxinitcodesize << SCHED >> [concrete]
+
     syntax Bool ::= #accountEmpty ( AccountCode , Int , Int ) [function, total, klabel(accountEmpty), symbol]
  // ---------------------------------------------------------------------------------------------------------
     rule #accountEmpty(CODE, NONCE, BAL) => CODE ==K .Bytes andBool NONCE ==Int 0 andBool BAL ==Int 0
@@ -212,14 +216,11 @@ module GAS-FEES
     rule [allBut64th.pos]: #allBut64th(N) => N -Int (N /Int 64) requires 0 <=Int N
     rule [allBut64th.neg]: #allBut64th(N) => 0                  requires N  <Int 0
 
-    syntax Int ::= G0 ( Schedule , Bytes , Bool )           [function]
+    syntax Int ::= G0 ( Schedule , Bytes , Bool )           [function, klabel(G0base)]
                  | G0 ( Schedule , Bytes , Int , Int, Int ) [function, klabel(G0data)]
-                 | G0 ( Schedule , Bool )                   [function, klabel(G0base)]
  // ----------------------------------------------------------------------------------
-    rule G0(SCHED, WS, B) => G0(SCHED, WS, 0, lengthBytes(WS), 0) +Int G0(SCHED, B)
-
-    rule G0(SCHED, true)  => Gtxcreate    < SCHED >
-    rule G0(SCHED, false) => Gtransaction < SCHED >
+    rule G0(SCHED, WS, false) => G0(SCHED, WS, 0, lengthBytes(WS), 0) +Int Gtransaction < SCHED >
+    rule G0(SCHED, WS, true)  => G0(SCHED, WS, 0, lengthBytes(WS), 0) +Int Gtxcreate < SCHED > +Int Cinitcode(SCHED, lengthBytes(WS))
 
     rule G0(    _,  _, I, I, R) => R
     rule G0(SCHED, WS, I, J, R) => G0(SCHED, WS, I +Int 1, J, R +Int #if WS[I] ==Int 0 #then Gtxdatazero < SCHED > #else Gtxdatanonzero < SCHED > #fi) [owise]

diff --git a/include/kframework/optimizations.md b/include/kframework/optimizations.md
@@ -22,6 +22,37 @@ module EVM-OPTIMIZATIONS [kore]
     imports EVM-OPTIMIZATIONS-LEMMAS
     imports INT-SIMPLIFICATION
 
+rule <kevm>
+       <k>
+         ( #next[ PUSHZERO ] => . ) ...
+       </k>
+       <schedule>
+         SCHED
+       </schedule>
+       <ethereum>
+         <evm>
+           <callState>
+             <wordStack>
+               ( WS => 0 : WS )
+             </wordStack>
+             <pc>
+               ( PCOUNT => ( PCOUNT +Int 1 ) )
+             </pc>
+             <gas>
+               ( GAVAIL => ( GAVAIL -Gas Gbase < SCHED > ) )
+             </gas>
+             ...
+           </callState>
+           ...
+         </evm>
+         ...
+       </ethereum>
+       ...
+     </kevm>
+  requires ( Gbase < SCHED > <=Gas GAVAIL )
+   andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 )
+    [priority(40)]
+
 rule <kevm>
        <k>
          ( #next[ PUSH(N) ] => . ) ...