From 9ba2625e59db206565382fd8d774a6022671d7a7 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 28 Aug 2018 10:15:59 -0500 Subject: [PATCH 01/11] tests/ethereum-tests: update to latest develop --- tests/ethereum-tests | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/ethereum-tests b/tests/ethereum-tests index 23306818ca..0c76bf7d18 160000 --- a/tests/ethereum-tests +++ b/tests/ethereum-tests @@ -1 +1 @@ -Subproject commit 23306818ca1452596c584c78c58e0ac91fa73150 +Subproject commit 0c76bf7d18e63bb65e4b8ffdd20e602e97e1c83b From 2ec9d4a510cde95e9b8e54fb6a57fce8fc1e616d Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 28 Aug 2018 11:44:37 -0500 Subject: [PATCH 02/11] data: add >>Word, >>sWord, and <>Word" Int [function] + | Int ">>sWord" Int [function] // ------------------------------------------- rule ~Word W => chop( W xorInt (pow256 -Int 1) ) rule W0 |Word W1 => chop( W0 |Int W1 ) rule W0 &Word W1 => chop( W0 &Int W1 ) rule W0 xorWord W1 => chop( W0 xorInt W1 ) + rule W0 < chop( W0 < 0 requires W1 >=Int 256 + rule W0 >>Word W1 => chop( W0 >>Int W1 ) + rule W0 >>sWord W1 => chop( (abs(W0) *Int sgn(W0)) >>Int W1 ) ``` - `bit` gets bit $N$ (0 being MSB). From 259772615dc2c842dc10b0e3c188d5a4d3e30b49 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 28 Aug 2018 11:45:03 -0500 Subject: [PATCH 03/11] evm: add EIP 145: bitwise shift instructions --- evm.md | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/evm.md b/evm.md index 2dc4e03c45..aaba2655c9 100644 --- a/evm.md +++ b/evm.md @@ -478,6 +478,9 @@ The `#next` operator executes a single step by: rule #changesState(XOR, _) => false rule #changesState(NOT, _) => false rule #changesState(BYTE, _) => false + rule #changesState(SHL, _) => false + rule #changesState(SHR, _) => false + rule #changesState(SAR, _) => false rule #changesState(SHA3, _) => false rule #changesState(ADDRESS, _) => false rule #changesState(BALANCE, _) => false @@ -1023,6 +1026,12 @@ NOTE: We have to call the opcode `OR` by `EVMOR` instead, because K has trouble rule BYTE INDEX W => byte(INDEX, W) ~> #push ... rule SIGNEXTEND W0 W1 => signextend(W0, W1) ~> #push ... + syntax BinStackOp ::= "SHL" | "SHR" | "SAR" + // ------------------------------------------- + rule SHL W0 W1 => W1 < #push ... + rule SHR W0 W1 => W1 >>Word W0 ~> #push ... + rule SAR W0 W1 => W1 >>sWord W0 ~> #push ... + syntax BinStackOp ::= "AND" | "EVMOR" | "XOR" // --------------------------------------------- rule AND W0 W1 => W0 &Word W1 ~> #push ... @@ -1901,6 +1910,9 @@ Grumble grumble, K sucks at `owise`. rule #memory(EVMOR _ _, MU) => MU rule #memory(XOR _ _, MU) => MU rule #memory(BYTE _ _, MU) => MU + rule #memory(SHL _ _, MU) => MU + rule #memory(SHR _ _, MU) => MU + rule #memory(SAR _ _, MU) => MU rule #memory(ISZERO _, MU) => MU rule #memory(LT _ _, MU) => MU @@ -2041,6 +2053,9 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, EVMOR _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, XOR _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, BYTE _ _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, SHL _ _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, SHR _ _) => Gverylow < SCHED > ... + rule #gasExec(SCHED, SAR _ _) => Gverylow < SCHED > ... rule #gasExec(SCHED, CALLDATALOAD _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MLOAD _) => Gverylow < SCHED > ... rule #gasExec(SCHED, MSTORE _ _) => Gverylow < SCHED > ... @@ -2196,8 +2211,8 @@ A `ScheduleFlag` is a boolean determined by the fee schedule; applying a `Schedu // ---------------------------------------------------------- syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas" - | "Ghasrevert" | "Ghasreturndata" | "Ghasstaticcall" - // ----------------------------------------------------------------------------------------- + | "Ghasrevert" | "Ghasreturndata" | "Ghasstaticcall" | "Ghasshift" + // ------------------------------------------------------------------------------------------------------------ ``` ### Schedule Constants @@ -2279,6 +2294,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Ghasrevert << DEFAULT >> => false rule Ghasreturndata << DEFAULT >> => false rule Ghasstaticcall << DEFAULT >> => false + rule Ghasshift << DEFAULT >> => false ``` ```c++ @@ -2472,11 +2488,11 @@ static const EVMSchedule ByzantiumSchedule = [] ```k syntax Schedule ::= "CONSTANTINOPLE" [klabel(CONSTANTINOPLE_EVM), symbol] // ------------------------------------------------------------------------- - rule Gblockhash < CONSTANTINOPLE > => 800 rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > - requires SCHEDCONST =/=K Gblockhash + rule Ghasshift << CONSTANTINOPLE >> => true rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> + requires notBool ( SCHEDFLAG ==K Ghasshift ) ``` ```c++ @@ -2556,6 +2572,9 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 24, _ ) => XOR rule #dasmOpCode( 25, _ ) => NOT rule #dasmOpCode( 26, _ ) => BYTE + rule #dasmOpCode( 27, SCHED ) => SHL requires Ghasshift << SCHED >> + rule #dasmOpCode( 28, SCHED ) => SHR requires Ghasshift << SCHED >> + rule #dasmOpCode( 29, SCHED ) => SAR requires Ghasshift << SCHED >> rule #dasmOpCode( 32, _ ) => SHA3 rule #dasmOpCode( 48, _ ) => ADDRESS rule #dasmOpCode( 49, _ ) => BALANCE From 301d60b8130cf65540e98adb86cbe23e5e78a91b Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 14 Sep 2018 14:08:09 -0500 Subject: [PATCH 04/11] driver, evm-node, evm, tests/interactive: add EIP 1283: dirty SSTORE gas costs --- driver.md | 1 + evm-node.md | 2 + evm.md | 101 +++++++++++++----- .../interactive/gas-analysis/sumTo10.evm.out | 3 + 4 files changed, 80 insertions(+), 27 deletions(-) diff --git a/driver.md b/driver.md index 0103a7c39f..3222b22033 100644 --- a/driver.md +++ b/driver.md @@ -475,6 +475,7 @@ The individual fields of the accounts are dealt with here. ACCT _ => STORAGE + _ => STORAGE ... ``` diff --git a/evm-node.md b/evm-node.md index 18e2c61466..031af0e485 100644 --- a/evm-node.md +++ b/evm-node.md @@ -52,6 +52,7 @@ Because the same account may be loaded more than once, implementations of this i #getBalance(ACCT) #if #isCodeEmpty(ACCT) #then .WordStack #else #unloaded #fi .Map + .Map #getNonce(ACCT) ) @@ -74,6 +75,7 @@ Because the same account may be loaded more than once, implementations of this i ACCT STORAGE => STORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] + ORIGSTORAGE => ORIGSTORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] ... requires notBool INDEX in_keys(STORAGE) diff --git a/evm.md b/evm.md index aaba2655c9..816aad7c1c 100644 --- a/evm.md +++ b/evm.md @@ -118,11 +118,12 @@ In the comments next to each cell, we've marked which component of the YellowPap .Set - 0 - 0 - .WordStack:AccountCode - .Map - 0 + 0 + 0 + .WordStack:AccountCode + .Map + .Map + 0 @@ -684,15 +685,29 @@ This is a right cons-list of `SubstateLogEntry` (which contains the account ID a After executing a transaction, it's necessary to have the effect of the substate log recorded. +- `#finalizeStorage` updates the origStorage cell with the new values of storage. - `#finalizeTx` makes the substate log actually have an effect on the state. - `#deleteAccounts` deletes the accounts specified by the self destruct list. ```k + syntax InternalOp ::= #finalizeStorage ( Set ) + // ---------------------------------------------- + rule #finalizeStorage((SetItem(ACCT) => .Set) _) ... + + ACCT + STORAGE + _ => STORAGE + ... + + + rule #finalizeStorage(.Set) => . + syntax InternalOp ::= #finalizeTx ( Bool ) | #deleteAccounts ( List ) // ---------------------------------------------- - rule #finalizeTx(true) => . ... + rule #finalizeTx(true) => #finalizeStorage(ACCTS) ... .Set + ACCTS rule (.K => #newAccount MINER) ~> #finalizeTx(_)... MINER @@ -840,10 +855,11 @@ These are just used by the other operators for shuffling local execution state a rule #newAccount ACCT => . ... - ACCT - .WordStack - 0 - _ => .Map + ACCT + .WordStack + 0 + _ => .Map + _ => .Map ... @@ -1311,28 +1327,29 @@ These rules reach into the network state and load/store from account storage: syntax BinStackOp ::= "SSTORE" // ------------------------------ - rule SSTORE INDEX VALUE => . ... + rule SSTORE INDEX NEW => . ... ACCT ACCT - ... (INDEX |-> (OLD => VALUE)) ... + ... (INDEX |-> (CURR => NEW)) ... + ORIGSTORAGE ... - R => #if OLD =/=Int 0 andBool VALUE ==Int 0 - #then R +Word Rsstoreclear < SCHED > - #else R - #fi - + R => R +Int Rsstore(SCHED, NEW, CURR, #lookup(ORIGSTORAGE, INDEX)) SCHED - rule SSTORE INDEX VALUE => . ... + rule SSTORE INDEX NEW => . ... ACCT ACCT - STORAGE => STORAGE [ INDEX <- VALUE ] + STORAGE => STORAGE [ INDEX <- NEW ] + ORIGSTORAGE ... + R => R +Int Rsstore(SCHED, NEW, 0, #lookup(ORIGSTORAGE, INDEX)) + SCHED requires notBool (INDEX in_keys(STORAGE)) + ``` ### Call Operations @@ -1968,11 +1985,12 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). ```k syntax InternalOp ::= #gasExec ( Schedule , OpCode ) // ---------------------------------------------------- - rule #gasExec(SCHED, SSTORE INDEX VALUE) => Csstore(SCHED, VALUE, #lookup(STORAGE, INDEX)) ... + rule #gasExec(SCHED, SSTORE INDEX VALUE) => Csstore(SCHED, VALUE, #lookup(STORAGE, INDEX), #lookup(ORIGSTORAGE, INDEX)) ... ACCT ACCT STORAGE + ORIGSTORAGE ... @@ -2120,7 +2138,8 @@ There are several helpers for calculating gas (most of them also specified in th => Gselfdestruct < SCHED > +Int Cnew(SCHED, BAL, ISEMPTY andBool Gselfdestructnewaccount << SCHED >>) ... syntax Int ::= Cgascap ( Schedule , Int , Int , Int ) [function] - | Csstore ( Schedule , Int , Int ) [function] + | Csstore ( Schedule , Int , Int , Int ) [function] + | Rsstore ( Schedule , Int , Int , Int ) [function] | Cextra ( Schedule , Int , Bool ) [function] | Cnew ( Schedule , Int , Bool ) [function] | Cxfer ( Schedule , Int ) [function] @@ -2128,8 +2147,33 @@ There are several helpers for calculating gas (most of them also specified in th rule Cgascap(SCHED, GCAP, GAVAIL, GEXTRA) => #if GAVAIL > #then GCAP #else minInt(#allBut64th(GAVAIL -Int GEXTRA), GCAP) #fi - rule Csstore(SCHED, VALUE, OLD) - => #if VALUE =/=Int 0 andBool OLD ==Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi + rule Csstore(SCHED, NEW, CURR, ORIG) + => #if CURR ==Int NEW orBool ORIG =/=Int CURR #then Gsload < SCHED > #else #if ORIG ==Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi #fi + requires Ghasdirtysstore << SCHED >> + rule Csstore(SCHED, NEW, CURR, ORIG) + => #if CURR ==Int 0 andBool NEW =/=Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi + requires notBool Ghasdirtysstore << SCHED >> + + rule Rsstore(SCHED, NEW, CURR, ORIG) + => #if CURR =/=Int NEW andBool ORIG ==Int CURR andBool NEW ==Int 0 #then + Rsstoreclear < SCHED > + #else + #if CURR =/=Int NEW andBool ORIG =/=Int CURR andBool ORIG =/=Int 0 #then + #if CURR ==Int 0 #then 0 -Int Rsstoreclear < SCHED > #else #if NEW ==Int 0 #then Rsstoreclear < SCHED > #else 0 #fi #fi + #else + 0 + #fi +Int + #if CURR =/=Int NEW andBool ORIG ==Int NEW #then + #if ORIG ==Int 0 #then Gsstoreset < SCHED > #else Gsstorereset < SCHED > #fi -Int Gsload < SCHED > + #else + 0 + #fi + #fi + requires Ghasdirtysstore << SCHED >> + + rule Rsstore(SCHED, NEW, CURR, ORIG) + => #if CURR =/=Int 0 andBool NEW ==Int 0 #then Rsstoreclear < SCHED > #else 0 #fi + requires notBool Ghasdirtysstore << SCHED >> rule Cextra(SCHED, VALUE, ISEMPTY) => Gcall < SCHED > +Int Cnew(SCHED, VALUE, ISEMPTY) +Int Cxfer(SCHED, VALUE) @@ -2212,7 +2256,8 @@ A `ScheduleFlag` is a boolean determined by the fee schedule; applying a `Schedu syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas" | "Ghasrevert" | "Ghasreturndata" | "Ghasstaticcall" | "Ghasshift" - // ------------------------------------------------------------------------------------------------------------ + | "Ghasdirtysstore" + // ----------------------------------------- ``` ### Schedule Constants @@ -2295,6 +2340,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Ghasreturndata << DEFAULT >> => false rule Ghasstaticcall << DEFAULT >> => false rule Ghasshift << DEFAULT >> => false + rule Ghasdirtysstore << DEFAULT >> => false ``` ```c++ @@ -2490,9 +2536,10 @@ static const EVMSchedule ByzantiumSchedule = [] // ------------------------------------------------------------------------- rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > - rule Ghasshift << CONSTANTINOPLE >> => true - rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> - requires notBool ( SCHEDFLAG ==K Ghasshift ) + rule Ghasshift << CONSTANTINOPLE >> => true + rule Ghasdirtysstore << CONSTANTINOPLE >> => true + rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> + requires notBool ( SCHEDFLAG ==K Ghasshift orBool SCHEDFLAG ==K Ghasdirtysstore ) ``` ```c++ diff --git a/tests/interactive/gas-analysis/sumTo10.evm.out b/tests/interactive/gas-analysis/sumTo10.evm.out index 002543b6fc..7147e91b9d 100644 --- a/tests/interactive/gas-analysis/sumTo10.evm.out +++ b/tests/interactive/gas-analysis/sumTo10.evm.out @@ -262,6 +262,9 @@ 0 |-> 10 + + .Map + 1 From 61bbdc2dfd8965e1781c755491f8f52e06e897e5 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 14 Sep 2018 14:10:22 -0500 Subject: [PATCH 05/11] data: add #newAddr variant for CREATE2 --- data.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/data.md b/data.md index b1ff7f3f2b..4a1c4c3179 100644 --- a/data.md +++ b/data.md @@ -550,13 +550,16 @@ Addresses ```k syntax Int ::= #newAddr ( Int , Int ) [function] - // ------------------------------------------------ + | #newAddr ( Int , Int , WordStack ) [function, klabel(#newAddrCreate2)] + // ------------------------------------------------------------------------------------- rule #newAddr(ACCT, NONCE) => #addr(#parseHexWord(Keccak256(#rlpEncodeLength(#rlpEncodeBytes(ACCT, 20) +String #rlpEncodeWord(NONCE), 192)))) + rule #newAddr(ACCT, SALT, INITCODE) => #addr(#parseHexWord(Keccak256("\xff" +String #unparseByteStack(#padToWidth(20, #asByteStack(ACCT))) +String #unparseByteStack(#padToWidth(32, #asByteStack(SALT))) +String #unparseByteStack(#parseHexBytes(Keccak256(#unparseByteStack(INITCODE))))))) syntax Account ::= #sender ( Int , Int , Int , Account , Int , String , Int , WordStack , WordStack ) [function] | #sender ( String , Int , String , String ) [function, klabel(#senderAux)] | #sender ( String ) [function, klabel(#senderAux2)] // ------------------------------------------------------------------------------------------------------------------------------------- + rule #sender(TN, TP, TG, TT, TV, DATA, TW, TR, TS) => #sender(#unparseByteStack(#parseHexBytes(Keccak256(#rlpEncodeLength(#rlpEncodeWordStack(TN : TP : TG : .WordStack) +String #rlpEncodeAccount(TT) +String #rlpEncodeWord(TV) +String #rlpEncodeString(DATA), 192)))), TW, #unparseByteStack(TR), #unparseByteStack(TS)) From f007ad348a7d2fdb19d37071734be894cc1260c9 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 14 Sep 2018 14:11:10 -0500 Subject: [PATCH 06/11] evm: add EIP 1014: Skinny CREATE2 --- evm.md | 37 +++++++++++++++++++++++++++++++------ 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/evm.md b/evm.md index 816aad7c1c..ac5ce4dccc 100644 --- a/evm.md +++ b/evm.md @@ -451,6 +451,7 @@ The `#next` operator executes a single step by: rule #changesState(SSTORE, _) => true rule #changesState(CALL, _ : _ : VALUE : _) => VALUE =/=Int 0 rule #changesState(CREATE, _) => true + rule #changesState(CREATE2, _) => true rule #changesState(SELFDESTRUCT, _) => true rule #changesState(DUP(_), _) => false @@ -1695,6 +1696,25 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state- ``` +`CREATE2` will attempt to `#create` the account, but with the new scheme for choosing the account address. +Note that we cannot execute #loadAccount during the #load phase earlier because gas will not yet +have been paid, and it may be to expensive to compute the hash of the init code. + +```k + syntax QuadStackOp ::= "CREATE2" + // -------------------------------- + rule CREATE2 VALUE MEMSTART MEMWIDTH SALT + => #loadAccount #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) + ~> #checkCreate ACCT VALUE + ~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) #allBut64th(GAVAIL) VALUE #range(LM, MEMSTART, MEMWIDTH) + ~> #codeDeposit #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) + ... + + ACCT + GAVAIL => GAVAIL /Int 64 + LM +``` + `SELFDESTRUCT` marks the current account for deletion and transfers funds out of the current account. Self destructing to yourself, unlike a regular transfer, destroys the balance in the account, irreparably losing it. @@ -1892,9 +1912,10 @@ In the YellowPaper, each opcode is defined to consume zero gas unless specified rule #memory ( CALLDATACOPY START _ WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) rule #memory ( RETURNDATACOPY START _ WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) - rule #memory ( CREATE _ START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) - rule #memory ( RETURN START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) - rule #memory ( REVERT START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) + rule #memory ( CREATE _ START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) + rule #memory ( CREATE2 _ START WIDTH _ , MU ) => #memoryUsageUpdate(MU, START, WIDTH) + rule #memory ( RETURN START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) + rule #memory ( REVERT START WIDTH , MU ) => #memoryUsageUpdate(MU, START, WIDTH) rule #memory ( COP:CallOp _ _ _ ARGSTART ARGWIDTH RETSTART RETWIDTH , MU ) => #memoryUsageUpdate(#memoryUsageUpdate(MU, ARGSTART, ARGWIDTH), RETSTART, RETWIDTH) rule #memory ( CSOP:CallSixOp _ _ ARGSTART ARGWIDTH RETSTART RETWIDTH , MU ) => #memoryUsageUpdate(#memoryUsageUpdate(MU, ARGSTART, ARGWIDTH), RETSTART, RETWIDTH) @@ -2027,6 +2048,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, CREATE _ _ _) => Gcreate < SCHED > ... + rule #gasExec(SCHED, CREATE2 _ _ WIDTH _) => Gcreate < SCHED > +Int Gsha3word < SCHED > *Int (WIDTH up/Int 32) ... rule #gasExec(SCHED, SHA3 _ WIDTH) => Gsha3 < SCHED > +Int (Gsha3word < SCHED > *Int (WIDTH up/Int 32)) ... @@ -2256,8 +2278,8 @@ A `ScheduleFlag` is a boolean determined by the fee schedule; applying a `Schedu syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas" | "Ghasrevert" | "Ghasreturndata" | "Ghasstaticcall" | "Ghasshift" - | "Ghasdirtysstore" - // ----------------------------------------- + | "Ghasdirtysstore" | "Ghascreate2" + // ----------------------------------------------------------------- ``` ### Schedule Constants @@ -2341,6 +2363,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Ghasstaticcall << DEFAULT >> => false rule Ghasshift << DEFAULT >> => false rule Ghasdirtysstore << DEFAULT >> => false + rule Ghascreate2 << DEFAULT >> => false ``` ```c++ @@ -2538,8 +2561,9 @@ static const EVMSchedule ByzantiumSchedule = [] rule Ghasshift << CONSTANTINOPLE >> => true rule Ghasdirtysstore << CONSTANTINOPLE >> => true + rule Ghascreate2 << CONSTANTINOPLE >> => true rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> - requires notBool ( SCHEDFLAG ==K Ghasshift orBool SCHEDFLAG ==K Ghasdirtysstore ) + requires notBool ( SCHEDFLAG ==K Ghasshift orBool SCHEDFLAG ==K Ghasdirtysstore orBool SCHEDFLAG ==K Ghascreate2 ) ``` ```c++ @@ -2661,6 +2685,7 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 242, _ ) => CALLCODE rule #dasmOpCode( 243, _ ) => RETURN rule #dasmOpCode( 244, SCHED ) => DELEGATECALL requires SCHED =/=K FRONTIER + rule #dasmOpCode( 245, SCHED ) => CREATE2 requires Ghascreate2 << SCHED >> rule #dasmOpCode( 250, SCHED ) => STATICCALL requires Ghasstaticcall << SCHED >> rule #dasmOpCode( 253, SCHED ) => REVERT requires Ghasrevert << SCHED >> rule #dasmOpCode( 254, _ ) => INVALID From 3e9fa1bfb31cb1e2f06db254eeed8070a215435d Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 14 Sep 2018 14:43:57 -0500 Subject: [PATCH 07/11] driver: add new discardKey --- driver.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/driver.md b/driver.md index 3222b22033..7006809712 100644 --- a/driver.md +++ b/driver.md @@ -336,7 +336,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` ```{.k .standalone} syntax Set ::= "#discardKeys" [function] // ---------------------------------------- - rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") ) + rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") SetItem("sealEngine") ) rule run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... requires KEY in #discardKeys ``` From 460c9f828c96550abe2dc967d90481ec5d5cb1e1 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 14 Sep 2018 14:43:26 -0500 Subject: [PATCH 08/11] data, evm: add EIP 1234: block reward adjustment for constantinople --- data.md | 4 ++++ evm.md | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/data.md b/data.md index 4a1c4c3179..d5dc423f2e 100644 --- a/data.md +++ b/data.md @@ -91,6 +91,10 @@ These can be used for pattern-matching on the LHS of rules as well (`macro` attr rule maxUInt160 => 1461501637330902918203684832716283019655932542975 [macro] /* 2^160 - 1 */ rule minUInt256 => 0 [macro] rule maxUInt256 => 115792089237316195423570985008687907853269984665640564039457584007913129639935 [macro] /* 2^256 - 1 */ + + syntax Int ::= "eth" + // -------------------- + rule eth => 1000000000000000000 [macro] ``` - Range of types diff --git a/evm.md b/evm.md index ac5ce4dccc..d249d00a28 100644 --- a/evm.md +++ b/evm.md @@ -2529,7 +2529,7 @@ static const EVMSchedule EIP158Schedule = [] ```k syntax Schedule ::= "BYZANTIUM" [klabel(BYZANTIUM_EVM), symbol] // --------------------------------------------------------------- - rule Rb < BYZANTIUM > => 3 *Int (10 ^Int 18) + rule Rb < BYZANTIUM > => 3 *Int eth rule SCHEDCONST < BYZANTIUM > => SCHEDCONST < EIP158 > requires notBool ( SCHEDCONST ==K Rb ) @@ -2557,7 +2557,9 @@ static const EVMSchedule ByzantiumSchedule = [] ```k syntax Schedule ::= "CONSTANTINOPLE" [klabel(CONSTANTINOPLE_EVM), symbol] // ------------------------------------------------------------------------- + rule Rb < CONSTANTINOPLE > => 2 *Int eth rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > + requires notBool ( SCHEDCONST ==K Rb ) rule Ghasshift << CONSTANTINOPLE >> => true rule Ghasdirtysstore << CONSTANTINOPLE >> => true From bdf9ee25c973e3310401136f03faaa752592cdad Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 11 Oct 2018 09:13:56 -0500 Subject: [PATCH 09/11] Makefile: filter bad tests --- Makefile | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 0c2d172154..736ddf6be6 100644 --- a/Makefile +++ b/Makefile @@ -288,13 +288,15 @@ slow_bchain_tests=$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTe $(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Call50000*.json) \ $(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Return50000*.json) \ $(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Call1MB1024Calldepth_d1g0v0.json) \ - tests/ethereum-tests/BlockchainTests/GeneralStateTests/stRandom/randomStatetest177_d0g0v0.json \ - tests/ethereum-tests/BlockchainTests/GeneralStateTests/stSpecialTest/JUMPDEST_Attack_d0g0v0.json \ - tests/ethereum-tests/BlockchainTests/GeneralStateTests/stSpecialTest/JUMPDEST_AttackwithJump_d0g0v0.json -quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(bchain_tests)) - -test-all-bchain: $(bchain_tests:=.test) -test-slow-bchain: $(bchain_tests:=.test) + tests/ethereum-tests/BlockchainTests/GeneralStateTests/stCreateTest/CREATE_ContractRETURNBigOffset_d2g0v0.json \ + tests/ethereum-tests/BlockchainTests/GeneralStateTests/stCreateTest/CREATE_ContractRETURNBigOffset_d1g0v0.json +bad_bchain_tests= tests/ethereum-tests/BlockchainTests/GeneralStateTests/stCreate2/RevertOpcodeInCreateReturns_d0g0v0.json \ + tests/ethereum-tests/BlockchainTests/GeneralStateTests/stCreate2/RevertInCreateInInit_d0g0v0.json +all_bchain_tests=$(filter-out $(bad_bchain_tests), $(bchain_tests)) +quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(all_bchain_tests)) + +test-all-bchain: $(all_bchain_tests:=.test) +test-slow-bchain: $(slow_bchain_tests:=.test) test-bchain: $(quick_bchain_tests:=.test) tests/ethereum-tests/BlockchainTests/%.test: tests/ethereum-tests/BlockchainTests/% build-ocaml From 61fc3b97ae81394f1e4c9966c9efd5e4011081ac Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 11 Oct 2018 10:06:38 -0500 Subject: [PATCH 10/11] evm: add EIP 1052: EXTCODEHASH opcode --- evm.md | 33 +++++++++++++++++++++++++++++---- 1 file changed, 29 insertions(+), 4 deletions(-) diff --git a/evm.md b/evm.md index d249d00a28..392a739c76 100644 --- a/evm.md +++ b/evm.md @@ -499,6 +499,7 @@ The `#next` operator executes a single step by: rule #changesState(EXTCODECOPY, _) => false rule #changesState(RETURNDATASIZE, _) => false rule #changesState(RETURNDATACOPY, _) => false + rule #changesState(EXTCODEHASH, _) => false rule #changesState(BLOCKHASH, _) => false rule #changesState(COINBASE, _) => false rule #changesState(TIMESTAMP, _) => false @@ -630,7 +631,8 @@ The `CallOp` opcodes all interperet their second argument as an address. // -------------------------------------------------- rule #addr?(BALANCE) => true rule #addr?(SELFDESTRUCT) => true - rule #addr?(OP) => false requires (OP =/=K BALANCE) andBool (OP =/=K SELFDESTRUCT) + rule #addr?(EXTCODEHASH) => true + rule #addr?(OP) => false requires (OP =/=K BALANCE) andBool (OP =/=K SELFDESTRUCT) andBool (OP =/=K EXTCODEHASH) syntax Bool ::= "#code?" "(" OpCode ")" [function] // -------------------------------------------------- @@ -1282,6 +1284,24 @@ For now, I assume that they instantiate an empty account and use the empty data. rule EXTCODESIZE ACCT => 0 ~> #push ... ACCTS requires notBool ACCT in ACCTS + + syntax UnStackOp ::= "EXTCODEHASH" + // ---------------------------------- +``` + +```{.k .standalone} + rule EXTCODEHASH ACCT => keccak(CODE) ~> #push ... + + ACCT + CODE + ... + +``` + +```k + rule EXTCODEHASH ACCT => 0 ~> #push ... + ACCTS + requires notBool ACCT in ACCTS ``` TODO: What should happen in the case that the account doesn't exist with `EXTCODECOPY`? @@ -1985,6 +2005,7 @@ Grumble grumble, K sucks at `owise`. rule #memory(SELFDESTRUCT _, MU) => MU rule #memory(CALLDATALOAD _, MU) => MU rule #memory(EXTCODESIZE _, MU) => MU + rule #memory(EXTCODEHASH _, MU) => MU rule #memory(BALANCE _, MU) => MU rule #memory(BLOCKHASH _, MU) => MU @@ -2122,6 +2143,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, EXTCODESIZE _) => Gextcodesize < SCHED > ... rule #gasExec(SCHED, BALANCE _) => Gbalance < SCHED > ... + rule #gasExec(SCHED, EXTCODEHASH _) => Gbalance < SCHED > ... rule #gasExec(SCHED, BLOCKHASH _) => Gblockhash < SCHED > ... // Precompiled @@ -2278,8 +2300,8 @@ A `ScheduleFlag` is a boolean determined by the fee schedule; applying a `Schedu syntax ScheduleFlag ::= "Gselfdestructnewaccount" | "Gstaticcalldepth" | "Gemptyisnonexistent" | "Gzerovaluenewaccountgas" | "Ghasrevert" | "Ghasreturndata" | "Ghasstaticcall" | "Ghasshift" - | "Ghasdirtysstore" | "Ghascreate2" - // ----------------------------------------------------------------- + | "Ghasdirtysstore" | "Ghascreate2" | "Ghasextcodehash" + // ------------------------------------------------------------------------------------------ ``` ### Schedule Constants @@ -2364,6 +2386,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Ghasshift << DEFAULT >> => false rule Ghasdirtysstore << DEFAULT >> => false rule Ghascreate2 << DEFAULT >> => false + rule Ghasextcodehash << DEFAULT >> => false ``` ```c++ @@ -2564,8 +2587,9 @@ static const EVMSchedule ByzantiumSchedule = [] rule Ghasshift << CONSTANTINOPLE >> => true rule Ghasdirtysstore << CONSTANTINOPLE >> => true rule Ghascreate2 << CONSTANTINOPLE >> => true + rule Ghasextcodehash << CONSTANTINOPLE >> => true rule SCHEDFLAG << CONSTANTINOPLE >> => SCHEDFLAG << BYZANTIUM >> - requires notBool ( SCHEDFLAG ==K Ghasshift orBool SCHEDFLAG ==K Ghasdirtysstore orBool SCHEDFLAG ==K Ghascreate2 ) + requires notBool ( SCHEDFLAG ==K Ghasshift orBool SCHEDFLAG ==K Ghasdirtysstore orBool SCHEDFLAG ==K Ghascreate2 orBool SCHEDFLAG ==K Ghasextcodehash ) ``` ```c++ @@ -2664,6 +2688,7 @@ After interpreting the strings representing programs as a `WordStack`, it should rule #dasmOpCode( 60, _ ) => EXTCODECOPY rule #dasmOpCode( 61, SCHED ) => RETURNDATASIZE requires Ghasreturndata << SCHED >> rule #dasmOpCode( 62, SCHED ) => RETURNDATACOPY requires Ghasreturndata << SCHED >> + rule #dasmOpCode( 63, SCHED ) => EXTCODEHASH requires Ghasextcodehash << SCHED >> rule #dasmOpCode( 64, _ ) => BLOCKHASH rule #dasmOpCode( 65, _ ) => COINBASE rule #dasmOpCode( 66, _ ) => TIMESTAMP From 7bbfeca06904ce60015b81cf2e312709b44cbb5c Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 30 Oct 2018 11:49:19 -0500 Subject: [PATCH 11/11] tests/proofs: update proofs submodule --- tests/proofs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/proofs b/tests/proofs index b79b336f45..7a0d88a94d 160000 --- a/tests/proofs +++ b/tests/proofs @@ -1 +1 @@ -Subproject commit b79b336f45a5814c0d8f10b47d84a99fd1fe1e14 +Subproject commit 7a0d88a94d32a805a5a2de9efe96da6aacdf1525