Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constantinople #267

Merged
merged 11 commits into from
Oct 31, 2018
Merged

Constantinople #267

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
9ba2625
tests/ethereum-tests: update to latest develop
Aug 28, 2018
2ec9d4a
data: add >>Word, >>sWord, and <<Word
Aug 28, 2018
2597726
evm: add EIP 145: bitwise shift instructions
Aug 28, 2018
301d60b
driver, evm-node, evm, tests/interactive: add EIP 1283: dirty SSTORE …
Sep 14, 2018
61bbdc2
data: add #newAddr variant for CREATE2
Sep 14, 2018
f007ad3
evm: add EIP 1014: Skinny CREATE2
Sep 14, 2018
3e9fa1b
driver: add new discardKey
Sep 14, 2018
460c9f8
data, evm: add EIP 1234: block reward adjustment for constantinople
Sep 14, 2018
bdf9ee2
Makefile: filter bad tests
Oct 11, 2018
61fc3b9
evm: add EIP 1052: EXTCODEHASH opcode
Oct 11, 2018
7bbfeca
tests/proofs: update proofs submodule
Oct 30, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 9 additions & 7 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 15 additions & 1 deletion data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -320,11 +324,18 @@ Bitwise logical operators are lifted from the integer versions.
| Int "|Word" Int [function]
| Int "&Word" Int [function]
| Int "xorWord" Int [function]
| Int "<<Word" Int [function]
| Int ">>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 <<Word W1 => chop( W0 <<Int W1 ) requires W1 <Int 256
rule W0 <<Word W1 => 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).
Expand Down Expand Up @@ -543,13 +554,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))

Expand Down
3 changes: 2 additions & 1 deletion driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <k> run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... </k> requires KEY in #discardKeys
```
Expand Down Expand Up @@ -475,6 +475,7 @@ The individual fields of the accounts are dealt with here.
<account>
<acctID> ACCT </acctID>
<storage> _ => STORAGE </storage>
<origStorage> _ => STORAGE </origStorage>
...
</account>
```
Expand Down
2 changes: 2 additions & 0 deletions evm-node.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ Because the same account may be loaded more than once, implementations of this i
<balance> #getBalance(ACCT) </balance>
<code> #if #isCodeEmpty(ACCT) #then .WordStack #else #unloaded #fi </code>
<storage> .Map </storage>
<origStorage> .Map </origStorage>
<nonce> #getNonce(ACCT) </nonce>
</account>
)
Expand All @@ -74,6 +75,7 @@ Because the same account may be loaded more than once, implementations of this i
<account>
<acctID> ACCT </acctID>
<storage> STORAGE => STORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] </storage>
<origStorage> ORIGSTORAGE => ORIGSTORAGE [ INDEX <- #getStorageData(ACCT, INDEX) ] </origStorage>
...
</account>
requires notBool INDEX in_keys(STORAGE)
Expand Down
Loading