Skip to content

Commit

Permalink
Bump the ethereum-tests submodule (#2506)
Browse files Browse the repository at this point in the history 
* bump ethereum-tests to v13.3

* add suport for Cancun schedule

* compatibility with v13

* update failing.llvm list

* typos

* Set Version: 1.0.623

* test-integration: update expected output

* update k claims

* tweak run rule

* Set Version: 1.0.624

* Set Version: 1.0.625

* Set Version: 1.0.626

* Set Version: 1.0.627

* Set Version: 1.0.628

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@anvacaru
anvacaru and devops authored Jul 3, 2024
1 parent e990cd6 commit 1984739
Show file tree
Hide file tree
Showing 111 changed files with 4,046 additions and 42 deletions.
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.627"
version = "1.0.628"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '1.0.627'
VERSION: Final = '1.0.628'
1 change: 1 addition & 0 deletions kevm-pyk/src/kevm_pyk/cli.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -897,6 +897,7 @@ def evm_chain_args(self) -> ArgumentParser:
'LONDON',
'MERGE',
'SHANGHAI',
'CANCUN',
)
modes = ('NORMAL', 'VMTESTS')

Expand Down
78 changes: 53 additions & 25 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -272,13 +272,16 @@ 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") SetItem("withdrawals") )
rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("network") SetItem("genesisRLP") )
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
requires KEY in #loadKeys
rule <k> run _TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, .JSONs ] , ( REST2 => KEY : VAL , REST2 ) } ... </k>
rule <k> run TESTID : { "blocks" : [ { .JSONs }, .JSONs ] , REST } => run TESTID : { REST } ... </k>
rule <k> run _TESTID : { "blocks" : [ { KEY : VAL , REST1 => REST1 }, _ ] , ( REST2 => KEY : VAL , REST2 ) } ... </k>
rule <k> run TESTID : { "blocks" : [ { .JSONs }, _ ] , REST } => run TESTID : { REST } ... </k>
rule <k> run _TESTID : { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
rule <k> run TESTID : { "rlp_decoded" : { .JSONs } , REST } => run TESTID : { REST } ... </k>
```

- `#execKeys` are all the JSON nodes which should be considered for execution (between loading and checking).
Expand Down Expand Up @@ -322,7 +325,8 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule #postKeys => ( SetItem("post") SetItem("postState") SetItem("postStateHash") )
rule #allPostKeys => ( #postKeys SetItem("expect") SetItem("export") SetItem("expet") )
rule #checkKeys => ( #allPostKeys SetItem("logs") SetItem("out") SetItem("gas")
SetItem("blockHeader") SetItem("transactions") SetItem("uncleHeaders") SetItem("genesisBlockHeader")
SetItem("blockHeader") SetItem("transactions") SetItem("uncleHeaders")
SetItem("genesisBlockHeader") SetItem("withdrawals") SetItem("blocknumber")
)
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => run TESTID : { REST } ~> check TESTID : { "post" : VAL } ... </k> requires KEY in #allPostKeys
Expand All @@ -334,7 +338,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
```k
syntax Set ::= "#discardKeys" [function]
// ----------------------------------------
rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") SetItem("sealEngine") SetItem("transactionSequence") SetItem("chainname") )
rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") SetItem("sealEngine") SetItem("transactionSequence") SetItem("chainname") SetItem("expectException"))
rule <k> run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... </k> requires KEY in #discardKeys
```
Expand Down Expand Up @@ -387,6 +391,10 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> check TESTID : { "post" : (POST:String) } => check "blockHeader" : { "stateRoot" : #parseWord(POST) } ~> failure TESTID ... </k>
rule <k> check TESTID : { "post" : { POST } } => check "account" : { POST } ~> failure TESTID ... </k>
// Temp rule to skip Beacon Roots contract checks.
// To be removed after EIP-4788
rule <k> check "account" : { 339909022928299415537769066420252604268194818 : _ } => .K ... </k>
rule <k> check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ... </k>
requires REST =/=K .JSONs
Expand Down Expand Up @@ -472,25 +480,30 @@ Here we check the other post-conditions associated with an EVM test.
SetItem("mixHash") SetItem("nonce") SetItem("number") SetItem("parentHash")
SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas") SetItem("withdrawalsRoot")
SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot")
)
rule <k> check "blockHeader" : { "bloom" : VALUE } => .K ... </k> <logsBloom> VALUE </logsBloom>
rule <k> check "blockHeader" : { "coinbase" : VALUE } => .K ... </k> <coinbase> VALUE </coinbase>
rule <k> check "blockHeader" : { "difficulty" : VALUE } => .K ... </k> <difficulty> VALUE </difficulty>
rule <k> check "blockHeader" : { "extraData" : VALUE } => .K ... </k> <extraData> VALUE </extraData>
rule <k> check "blockHeader" : { "gasLimit" : VALUE } => .K ... </k> <gasLimit> VALUE </gasLimit>
rule <k> check "blockHeader" : { "gasUsed" : VALUE } => .K ... </k> <gasUsed> VALUE </gasUsed>
rule <k> check "blockHeader" : { "mixHash" : VALUE } => .K ... </k> <mixHash> VALUE </mixHash>
rule <k> check "blockHeader" : { "nonce" : VALUE } => .K ... </k> <blockNonce> VALUE </blockNonce>
rule <k> check "blockHeader" : { "number" : VALUE } => .K ... </k> <number> VALUE </number>
rule <k> check "blockHeader" : { "parentHash" : VALUE } => .K ... </k> <previousHash> VALUE </previousHash>
rule <k> check "blockHeader" : { "receiptTrie" : VALUE } => .K ... </k> <receiptsRoot> VALUE </receiptsRoot>
rule <k> check "blockHeader" : { "stateRoot" : VALUE } => .K ... </k> <stateRoot> VALUE </stateRoot>
rule <k> check "blockHeader" : { "timestamp" : VALUE } => .K ... </k> <timestamp> VALUE </timestamp>
rule <k> check "blockHeader" : { "transactionsTrie" : VALUE } => .K ... </k> <transactionsRoot> VALUE </transactionsRoot>
rule <k> check "blockHeader" : { "uncleHash" : VALUE } => .K ... </k> <ommersHash> VALUE </ommersHash>
rule <k> check "blockHeader" : { "baseFeePerGas" : VALUE } => .K ... </k> <baseFee> VALUE </baseFee>
rule <k> check "blockHeader" : { "withdrawalsRoot" : VALUE } => .K ... </k> <withdrawalsRoot> VALUE </withdrawalsRoot>
rule <k> check "blockHeader" : { "bloom" : VALUE } => .K ... </k> <logsBloom> VALUE </logsBloom>
rule <k> check "blockHeader" : { "coinbase" : VALUE } => .K ... </k> <coinbase> VALUE </coinbase>
rule <k> check "blockHeader" : { "difficulty" : VALUE } => .K ... </k> <difficulty> VALUE </difficulty>
rule <k> check "blockHeader" : { "extraData" : VALUE } => .K ... </k> <extraData> VALUE </extraData>
rule <k> check "blockHeader" : { "gasLimit" : VALUE } => .K ... </k> <gasLimit> VALUE </gasLimit>
rule <k> check "blockHeader" : { "gasUsed" : VALUE } => .K ... </k> <gasUsed> VALUE </gasUsed>
rule <k> check "blockHeader" : { "mixHash" : VALUE } => .K ... </k> <mixHash> VALUE </mixHash>
rule <k> check "blockHeader" : { "nonce" : VALUE } => .K ... </k> <blockNonce> VALUE </blockNonce>
rule <k> check "blockHeader" : { "number" : VALUE } => .K ... </k> <number> VALUE </number>
rule <k> check "blockHeader" : { "parentHash" : VALUE } => .K ... </k> <previousHash> VALUE </previousHash>
rule <k> check "blockHeader" : { "receiptTrie" : VALUE } => .K ... </k> <receiptsRoot> VALUE </receiptsRoot>
rule <k> check "blockHeader" : { "stateRoot" : VALUE } => .K ... </k> <stateRoot> VALUE </stateRoot>
rule <k> check "blockHeader" : { "timestamp" : VALUE } => .K ... </k> <timestamp> VALUE </timestamp>
rule <k> check "blockHeader" : { "transactionsTrie" : VALUE } => .K ... </k> <transactionsRoot> VALUE </transactionsRoot>
rule <k> check "blockHeader" : { "uncleHash" : VALUE } => .K ... </k> <ommersHash> VALUE </ommersHash>
rule <k> check "blockHeader" : { "baseFeePerGas" : VALUE } => .K ... </k> <baseFee> VALUE </baseFee>
rule <k> check "blockHeader" : { "withdrawalsRoot" : VALUE } => .K ... </k> <withdrawalsRoot> VALUE </withdrawalsRoot>
rule <k> check "blockHeader" : { "blobGasUsed" : VALUE } => .K ... </k> <blobGasUsed> VALUE </blobGasUsed>
rule <k> check "blockHeader" : { "excessBlobGas" : VALUE } => .K ... </k> <excessBlobGas> VALUE </excessBlobGas>
rule <k> check "blockHeader" : { "parentBeaconBlockRoot": VALUE } => .K ... </k> <beaconRoot> VALUE </beaconRoot>
rule <k> check "blockHeader" : { "hash": HASH:Bytes } => .K ...</k>
<previousHash> HP </previousHash>
Expand All @@ -510,9 +523,13 @@ Here we check the other post-conditions associated with an EVM test.
<blockNonce> HN </blockNonce>
<baseFee> HF </baseFee>
<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)
<blobGasUsed> UB </blobGasUsed>
<excessBlobGas> EB </excessBlobGas>
<beaconRoot> BR </beaconRoot>
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)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
// ------------------------------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -585,6 +602,17 @@ TODO: case with nonzero ommers.
rule <k> check "ommerHeaders" : [ .JSONs ] => .K ... </k> <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
```

```k
rule <k> check TESTID : {"withdrawals" : WITHDRAWALS } => check "withdrawals" : WITHDRAWALS ~> failure TESTID ... </k>
// ----------------------------------------------------------------------------------------------------------------------
```

```k
rule <k> check TESTID : { "blocknumber": BN } => check "blocknumber" : BN ~> failure TESTID ... </k>
// ----------------------------------------------------------------------------------------------------
rule <k> check "blocknumber" : (VALUE:String => #parseWord(VALUE)) ... </k>
rule <k> check "blocknumber" : BN => .K ... </k> <number> BN </number>
```
```k
endmodule
```
4 changes: 4 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,9 @@ In the comments next to each cell, we've marked which component of the YellowPap
<blockNonce> 0 </blockNonce> // I_Hn
<baseFee> 0 </baseFee>
<withdrawalsRoot> 0 </withdrawalsRoot>
<blobGasUsed> 0 </blobGasUsed>
<excessBlobGas> 0 </excessBlobGas>
<beaconRoot> 0 </beaconRoot>
<ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
</block>
Expand Down Expand Up @@ -1746,6 +1749,7 @@ Precompiled Contracts
rule #precompiledAccountsUB(LONDON) => #precompiledAccountsUB(BERLIN)
rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON)
rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE)
rule #precompiledAccountsUB(CANCUN) => #precompiledAccountsUB(SHANGHAI)
syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total]
Expand Down
12 changes: 12 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -372,5 +372,17 @@ A `ScheduleConst` is a constant determined by the fee schedule.
orBool SCHEDFLAG ==K Ghaspushzero
orBool SCHEDFLAG ==K Ghaswarmcoinbase
)
```

### Cancun Schedule

```k
syntax Schedule ::= "CANCUN" [symbol(CANCUN_EVM), smtlib(schedule_CANCUN)]
// --------------------------------------------------------------------------
rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI >
rule SCHEDFLAG << CANCUN >> => SCHEDFLAG << SHANGHAI >>
```
```k
endmodule
```
31 changes: 24 additions & 7 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,16 @@ Address/Hash Helpers
- `#blockHeaderHash` computes the hash of a block header given all the block data.

```k
syntax Int ::= #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int ) [function, symbol(blockHeaderHash) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBytes) ]
| #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int ) [function, symbol(blockHeaderHashBaseFee) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBaseFeeBytes) ]
| #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int ) [function, symbol(blockHeaderHashWithdrawals) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, symbol(#blockHashHeaderWithdrawalsBytes)]
// -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
syntax Int ::= #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int ) [function, symbol(blockHeaderHash) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(blockHashHeaderBytes) ]
| #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int ) [function, symbol(blockHeaderHashBaseFee) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(blockHashHeaderBaseFeeBytes) ]
| #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int ) [function, symbol(blockHeaderHashWithdrawals) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(blockHashHeaderWithdrawalsBytes)]
| #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Int , Int ) [function, symbol(blockHeaderHashBlobBeacon) ]
| #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, symbol(blockHashHeaderBlobBeacon) ]
// -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
rule #blockHeaderHash(HP:Bytes, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)
=> #parseHexWord( Keccak256( #rlpEncode( [ HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN ] ) ) )
Expand Down Expand Up @@ -113,6 +116,20 @@ Address/Hash Helpers
)
)
)
rule #blockHeaderHash(HP:Bytes, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WF, UB, EB, BR)
=> #parseHexWord( Keccak256( #rlpEncode( [ HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WF, UB, EB, BR] ) ) )
rule #blockHeaderHash(HP:Int, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WF, UB, EB, BR)
=> #parseHexWord( Keccak256( #rlpEncode( [ #wordBytes(HP), #wordBytes(HO), #addrBytes(HC)
, #wordBytes(HR), #wordBytes(HT), #wordBytes(HE)
, HB, HD, HI, HL, HG, HS, HX
, #wordBytes(HM), #padToWidth(8, #asByteStack(HN))
, HF , #wordBytes(WF) , UB , EB , #wordBytes(BR)
]
)
)
)
```

- `#hashTxData` returns the Keccak-256 message hash `HT` to be signed.
Expand Down
Loading

0 comments on commit 1984739

Please sign in to comment.