Skip to content

Add support for state tests #2746

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

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Add support for state tests #2746

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
82b2ddd
add support for state-tests format
anvacaru Apr 22, 2025
e5677e0
update execution-sepc-tests/failing.llvm
anvacaru Apr 22, 2025
832d4c5
more tweaks; save wip
anvacaru Apr 23, 2025
ae0c8d3
remove debug statement
anvacaru Apr 23, 2025
be9b1bd
fix typos
anvacaru Apr 23, 2025
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
8 changes: 4 additions & 4 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,14 +59,14 @@ test-fixtures: poetry download-json-fixtures
$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_execution_spec_tests.py"

fixtures-failing-list: poetry download-json-fixtures
cat /dev/null > tests/ethereum-sepc-tests/failing.llvm
cat /dev/null > tests/execution-spec-tests/failing.llvm
- $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_execution_spec_tests.py --save-failing --maxfail=10000"
LC_ALL=en_US.UTF-8 sort -f -d -o tests/execution-spec-tests/failing.llvm tests/execution-spec-tests/failing.llvm
if [ "$(shell uname)" = "Darwin" ]; then \
sed -i '' '1{/^[[:space:]]*$$/d;}' tests/ethereum-sepc-tests/failing.llvm ;\
echo >> tests/ethereum-sepc-tests/failing.llvm ;\
sed -i '' '1{/^[[:space:]]*$$/d;}' tests/execution-spec-tests/failing.llvm ;\
echo >> tests/execution-spec-tests/failing.llvm ;\
else \
sed -i '1{/^[[:space:]]*$$/d;}' tests/ethereum-sepc-tests/failing.llvm ;\
sed -i '1{/^[[:space:]]*$$/d;}' tests/execution-spec-tests/failing.llvm ;\
fi

test-vm: poetry
Expand Down
3 changes: 0 additions & 3 deletions kevm-pyk/src/kevm_pyk/interpreter.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,5 @@

def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, *, check: bool = True) -> Pattern:
"""Interpret the given GST data using the LLVM backend."""
if 'config' in gst_data.keys():
schedule = gst_data['config']['network'].upper()
chainid = int(gst_data['config']['network'], 16)
init_kore = gst_to_kore(filter_gst_keys(gst_data), schedule, mode, chainid, usegas)
return llvm_interpret(kdist.get('evm-semantics.llvm'), init_kore, check=check)
47 changes: 41 additions & 6 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,13 +85,24 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
<chainID> B </chainID>
<gas> _ => 0 </gas>
<message>
<msgID> TXID </msgID>
<sigV> TW </sigV>
<sigR> TR </sigR>
<sigS> TS </sigS>
<msgID> TXID </msgID>
<sigV> TW </sigV>
<sigR> TR </sigR>
<sigS> TS </sigS>
<sender> .Account </sender>
...
</message>

rule <k> startTx => loadTx( ACCTFROM ) ... </k>
<txPending> ListItem(TXID:Int) ... </txPending>
<gas> _ => 0 </gas>
<message>
<msgID> TXID </msgID>
<sender> ACCTFROM </sender>
...
</message>
requires notBool ACCTFROM ==K .Account

syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
// --------------------------------------------------------------
rule <k> loadTx(_) => startTx ... </k>
Expand Down Expand Up @@ -225,6 +236,14 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
syntax EthereumCommand ::= #loadAccessList ( JSON ) [symbol(#loadAccessList)]
| #loadAccessListAux ( Account , List ) [symbol(#loadAccessListAux)]
// ---------------------------------------------------------------------------------------------
rule <k> #loadAccessList ( [ { "address" : ACCT:String , "storageKeys" : [STRG] }, REST ] )
=> #loadAccessListAux (#parseAddr(ACCT), #parseAccessListStorageKeys([STRG]))
~> #loadAccessList ([REST])
...
</k>
<schedule> SCHED </schedule>
requires Ghasaccesslist << SCHED >>

rule <k> #loadAccessList ([ .JSONs ]) => .K ... </k>
<schedule> SCHED </schedule>
requires Ghasaccesslist << SCHED >>
Expand Down Expand Up @@ -315,7 +334,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("transaction"))

rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
requires KEY in #loadKeys
Expand Down Expand Up @@ -352,6 +371,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> process TESTID : { KEY : VAL , REST } => process TESTID : { REST } ~> check TESTID : {KEY : VAL} ... </k> requires KEY in #checkKeys
rule <k> process _TESTID : { .JSONs } => #startBlock ~> startTx ... </k>

rule <k> run _TESTID : { .JSONs } => #startBlock ~> startTx ... </k>
rule <k> run _TESTID : { "exec" : (EXEC:JSON) } => loadCallState EXEC ~> start ~> flush ... </k>

rule <k> load "exec" : J => loadCallState J ... </k>
Expand Down Expand Up @@ -413,6 +433,13 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
rule <k> loadTransaction _ { "maxFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
rule <k> loadTransaction _ { "maxFeePerBlobGas" : (V:Bytes => #asWord(V)), _ } ... </k>

// for state-tests

rule <k> loadTransaction _ { KEY : ((VAL:String) => #parseWord(VAL)), _ } ... </k>
requires KEY in (SetItem("nonce") SetItem("gasPrice") SetItem("gasLimit") SetItem("to") SetItem("value") SetItem("sender") SetItem("maxPriorityFeePerGas") SetItem("maxFeePerGas") SetItem("maxFeePerBlobGas"))
rule <k> loadTransaction _ { KEY : ((VAL:String) => #parseByteStack(VAL)), _ } ... </k>
requires KEY in (SetItem("data"))
```

### Checking State
Expand All @@ -437,7 +464,15 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
requires KEY in (SetItem("callcreates")) andBool notBool sortedJSONs(JS)

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>
rule <k> check TESTID : { "post" : {(SCHEDULE_STR:String) : [ POST ] } }
=> check TESTID : { "post" : POST } ~> failure TESTID ... </k>
<schedule> SCHEDULE </schedule>
requires #asScheduleString(SCHEDULE_STR) ==K SCHEDULE

rule <k> check _TESTID : { "post" : { (KEY : _VALUE, REST => REST) } } ... </k> requires KEY in (SetItem("hash") SetItem("logs") SetItem("txbytes") SetItem("indexes"))
rule <k> check _TESTID : { "post" : { "state" : { STATE } } } => check "account" : { STATE } ... </k>

rule <k> check TESTID : { "post" : { POST } } => check "account" : { POST } ~> failure TESTID ... </k> [owise]

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
1 change: 1 addition & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,6 +171,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
<txType> .TxType </txType> // T_x
<txMaxBlobFee> 0 </txMaxBlobFee>
<txVersionedHashes> .List </txVersionedHashes>
<sender> .Account </sender>
</message>
</messages>

Expand Down
10 changes: 10 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,16 @@ module JSON-EXT
// ----------------------
```

- inKeys - returns true if a key is present in a JSON object.

```k
syntax Bool ::= inKeys ( String , JSONs ) [symbol(in_keys_json), function]
// --------------------------------------------------------------------------
rule inKeys(_KEY, .JSONs) => false
rule inKeys(KEY, (KEY : _, _REST)) => true
rule inKeys(KEY, (KEY' : _, REST)) => inKeys(KEY, REST) requires KEY =/=String KEY'
```

```k
endmodule
```
Expand Down
7 changes: 4 additions & 3 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,9 +253,10 @@ These parsers can interpret hex-encoded strings as `Int`s, `Bytes`s, and `Map`s.
syntax List ::= #parseAccessListStorageKeys ( JSONs ) [symbol(#parseAccessListStorageKeys), function]
| #parseAccessListStorageKeys ( JSONs , List ) [symbol(#parseAccessListStorageKeysAux), function]
// --------------------------------------------------------------------------------------------------------------
rule #parseAccessListStorageKeys( J ) => #parseAccessListStorageKeys(J, .List)
rule #parseAccessListStorageKeys([S:Bytes, REST ], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT )
rule #parseAccessListStorageKeys([ .JSONs ], RESULT:List) => RESULT
rule #parseAccessListStorageKeys( J ) => #parseAccessListStorageKeys(J, .List)
rule #parseAccessListStorageKeys([S:String, REST ], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#parseHexWord(S)) RESULT )
rule #parseAccessListStorageKeys([S:Bytes, REST ], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT )
rule #parseAccessListStorageKeys([ .JSONs ], RESULT:List) => RESULT
```

Unparsing
Expand Down
43 changes: 35 additions & 8 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,17 +137,19 @@ Here we load the environmental information.

```k
rule <k> load "env" : { KEY : ((VAL:String) => #parseWord(VAL)) } ... </k>
requires KEY in (SetItem("currentTimestamp") SetItem("currentGasLimit") SetItem("currentNumber") SetItem("currentDifficulty") SetItem("currentBaseFee"))
requires KEY in (SetItem("currentTimestamp") SetItem("currentGasLimit") SetItem("currentNumber") SetItem("currentDifficulty") SetItem("currentBaseFee") SetItem("currentRandom") SetItem("currentExcessBlobGas"))
rule <k> load "env" : { KEY : ((VAL:String) => #parseHexWord(VAL)) } ... </k>
requires KEY in (SetItem("currentCoinbase") SetItem("previousHash"))
// ----------------------------------------------------------------------
rule <k> load "env" : { "currentCoinbase" : (CB:Int) } => .K ... </k> <coinbase> _ => CB </coinbase>
rule <k> load "env" : { "currentDifficulty" : (DIFF:Int) } => .K ... </k> <difficulty> _ => DIFF </difficulty>
rule <k> load "env" : { "currentGasLimit" : (GLIMIT:Int) } => .K ... </k> <gasLimit> _ => GLIMIT </gasLimit>
rule <k> load "env" : { "currentNumber" : (NUM:Int) } => .K ... </k> <number> _ => NUM </number>
rule <k> load "env" : { "previousHash" : (HASH:Int) } => .K ... </k> <previousHash> _ => HASH </previousHash>
rule <k> load "env" : { "currentTimestamp" : (TS:Int) } => .K ... </k> <timestamp> _ => TS </timestamp>
rule <k> load "env" : { "currentBaseFee" : (BF:Int) } => .K ... </k> <baseFee> _ => BF </baseFee>
rule <k> load "env" : { "currentCoinbase" : (CB:Int) } => .K ... </k> <coinbase> _ => CB </coinbase>
rule <k> load "env" : { "currentDifficulty" : (DIFF:Int) } => .K ... </k> <difficulty> _ => DIFF </difficulty>
rule <k> load "env" : { "currentGasLimit" : (GLIMIT:Int) } => .K ... </k> <gasLimit> _ => GLIMIT </gasLimit>
rule <k> load "env" : { "currentNumber" : (NUM:Int) } => .K ... </k> <number> _ => NUM </number>
rule <k> load "env" : { "previousHash" : (HASH:Int) } => .K ... </k> <previousHash> _ => HASH </previousHash>
rule <k> load "env" : { "currentTimestamp" : (TS:Int) } => .K ... </k> <timestamp> _ => TS </timestamp>
rule <k> load "env" : { "currentRandom" : (RANDAO:Int) } => .K ... </k> <mixHash> _ => RANDAO </mixHash>
rule <k> load "env" : { "currentBaseFee" : (BF:Int) } => .K ... </k> <baseFee> _ => BF </baseFee>
rule <k> load "env" : { "currentExcessBlobGas" : (BGAS:Int) } => .K ... </k> <excessBlobGas> _ => BGAS </excessBlobGas>

syntax KItem ::= "loadCallState" JSON
// -------------------------------------
Expand Down Expand Up @@ -195,6 +197,7 @@ The `"network"` key allows setting the fee schedule inside the test.
syntax List ::= "#parseJSONs2List" "(" JSONs ")" [function]
// ----------------------------------------------------------
rule #parseJSONs2List ( .JSONs ) => .List
rule #parseJSONs2List ( (VAL:String), REST ) => ListItem(#parseByteStack(VAL)) #parseJSONs2List ( REST )
rule #parseJSONs2List ( (VAL:Bytes) , REST ) => ListItem(VAL) #parseJSONs2List ( REST )
```

Expand Down Expand Up @@ -375,6 +378,14 @@ The `"rlp"` key loads the block information.
</k>
requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob)

rule <k> load "transaction" : { TXDATA } => mkTX !ID:Int ~> loadTransaction !ID { "type": #dasmTxPrefix(Blob), TXDATA } ... </k>
requires inKeys("blobVersionedHashes", TXDATA)
rule <k> load "transaction" : { TXDATA } => mkTX !ID:Int ~> loadTransaction !ID { "type": #dasmTxPrefix(AccessList), TXDATA } ... </k>
requires inKeys("accessLists", TXDATA)
andBool notBool inKeys("blobVersionedHashes", TXDATA)
rule <k> load "transaction" : { TXDATA } => mkTX !ID:Int ~> loadTransaction !ID { "type": #dasmTxPrefix(Legacy), TXDATA } ... </k>
[owise]

syntax EthereumCommand ::= "loadTransaction" Int JSON
// -----------------------------------------------------
rule <k> loadTransaction _ { .JSONs } => .K ... </k>
Expand Down Expand Up @@ -427,6 +438,22 @@ The `"rlp"` key loads the block information.

rule <k> loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... </k>
<message> <msgID> TXID </msgID> <txVersionedHashes> _ => #parseJSONs2List(TVH) </txVersionedHashes> ... </message>

rule <k> loadTransaction TXID { "sender" : TS:Int , REST => REST } ... </k>
<message> <msgID> TXID </msgID> <sender> _ => TS </sender> ... </message>

rule <k> loadTransaction _TXID { "accessLists" : [ .JSONs ], REST => REST } ... </k>

rule <k> loadTransaction TXID { "accessLists" : [ [ TA:JSONs ] , TAS ], REST }
=> loadTransaction TXID { "accessList" : [ TA ]}
~> loadTransaction TXID { "accessLists" : [ TAS ], REST } ... </k>

rule <k> loadTransaction _TXID {( KEY : [VAL, .JSONs] => KEY : VAL), _REST } ... </k>
requires KEY in (SetItem("gasLimit") SetItem("value") SetItem("data"))

rule <k> loadTransaction _TXID {KEY : _VAL, REST => REST } ... </k>
requires KEY in (SetItem("secretKey"))

```

### Getting State
Expand Down
22 changes: 22 additions & 0 deletions kevm-pyk/src/tests/unit/test_kevm.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
from pyk.prelude.utils import token

from kevm_pyk.kevm import KEVM, KEVMSemantics, compute_jumpdests
from tests.utils import read_gst_schedule_and_chainid

TEST_DATA: Final = [
('single-ktoken', token(0), KToken('0x0', 'Int')),
Expand Down Expand Up @@ -215,3 +216,24 @@ def test_is_mergeable(test_id: str, input: list[CTerm], expected: KInner, raise_
return
# Then
assert result == expected


GST_TEST_DATA = [
('base_0', {'config': {'network': 'Cancun', 'chainid': '0x01'}}, ('CANCUN', 1)),
('base_1', {'post': {'Shanghai': {}}, 'config': {'chainid': '0x02'}}, ('SHANGHAI', 2)),
('missing_network', {'config': {'chainid': '0x00'}}, (None, 0)),
('missing_chainid', {'config': {'network': 'Berlin'}}, ('BERLIN', None)),
('empty', {}, (None, None)),
]


@pytest.mark.parametrize(
'test_id,input,expected',
GST_TEST_DATA,
ids=[test_id for test_id, *_ in GST_TEST_DATA],
)
def test_gst_schedule_and_chainid(test_id: str, input: dict, expected: tuple[str | None, int | None]) -> None:
# When
result = read_gst_schedule_and_chainid(input)
# Then
assert result == expected
37 changes: 36 additions & 1 deletion kevm-pyk/src/tests/utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,17 @@ def _test(
_LOGGER.info(f'Running test: {gst_file} - {test_name}')
if test_name in skipped_gst_tests:
continue
chain_id = compute_chain_id(gst_file_relative_path)
# for execution_spec_tests, we look for chainid and schedule in the test file
# TODO: using this approach we end up calling _schedule_to_kore of a possibly unimplemented schedule
# which would result in `llvm_interpret` throwing a RuntimeError like:
# No tag found for symbol LbIPRAGUE 'Unds 'EVM{}. Maybe attempted to evaluate a symbol with no rules
gst_schedule, gst_chain_id = read_gst_schedule_and_chainid(test)
if gst_schedule is not None:
schedule = gst_schedule

# for the legacy test suite, we need to use the compute_chain_id func
chain_id = gst_chain_id if gst_chain_id is not None else compute_chain_id(gst_file_relative_path)

res = interpret({test_name: test}, schedule, mode, chain_id, usegas, check=False)

try:
Expand All @@ -110,3 +120,28 @@ def _test(
for test_name in sorted(failing_tests):
writer.writerow([gst_file_relative_path, test_name])
raise AssertionError(f'Found failing tests in GST file {gst_file_relative_path}: {failing_tests}')


def read_gst_schedule_and_chainid(test: dict) -> tuple[str | None, int | None]:
schedule = None
chainid = None

# for blockchain_tests, json fixtures have `"config": { "network": "Cancun", "chainid": "0x01",...`
config = test.get('config')
if config:
network = config.get('network')
if network:
schedule = network.upper()

chainid_str = config.get('chainid')
if chainid_str:
chainid = int(chainid_str, 16)

# for state_tests, json fixtures have `"post": { "Berlin": [{ "hash": ...`
if not schedule and 'post' in test:
post = test['post']
if post and len(post) == 1:
schedule = next(iter(post)).upper()

return (schedule, chainid)

Loading
Loading