Skip to content

Commit f653697

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 769d7ed + f5deb06 commit f653697

File tree

14 files changed

+67
-58
lines changed

14 files changed

+67
-58
lines changed

‎kevm-pyk/src/kevm_pyk/__main__.py‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -603,7 +603,9 @@ def exec_run(options: RunOptions) -> None:
603603
json_read = {options.gst_name: json_read[options.gst_name]}
604604
kore_pattern_list = [
605605
(name, kore)
606-
for (name, kore) in iterate_gst(json_read, options.schedule, options.mode, options.chainid, options.usegas)
606+
for (name, kore) in iterate_gst(
607+
json_read, options.mode, options.chainid, options.usegas, schedule=options.schedule
608+
)
607609
]
608610
except json.JSONDecodeError:
609611
pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation'))
@@ -645,7 +647,9 @@ def exec_kast(options: KastOptions) -> None:
645647
json_read = {options.gst_name: json_read[options.gst_name]}
646648
kore_pattern_list = [
647649
(name, kore)
648-
for (name, kore) in iterate_gst(json_read, options.schedule, options.mode, options.chainid, options.usegas)
650+
for (name, kore) in iterate_gst(
651+
json_read, options.mode, options.chainid, options.usegas, schedule=options.schedule
652+
)
649653
]
650654
except json.JSONDecodeError:
651655
pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation'))

‎kevm-pyk/src/kevm_pyk/config.py‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,3 +20,5 @@
2020

2121

2222
NIX_LIBS: Final = os.getenv('NIX_LIBS')
23+
24+
DEFAULT_SCHEDULE: Final[str] = 'PRAGUE'

‎kevm-pyk/src/kevm_pyk/gst_to_kore.py‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
from typing import TYPE_CHECKING
88

99
from pyk.cli.utils import file_path
10+
from pyk.konvert import munge
1011
from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer
1112
from pyk.kore.syntax import App, SortApp
1213

@@ -28,6 +29,27 @@
2829
SORT_MODE: Final = SortApp('SortMode')
2930
SORT_ETHEREUM_SIMULATION: Final = SortApp('SortEthereumSimulation')
3031

32+
33+
SCHEDULE_MAPPING: Final[dict[str, str]] = {
34+
'Frontier': 'FRONTIER',
35+
'Homestead': 'HOMESTEAD',
36+
'EIP150': 'TANGERINE_WHISTLE',
37+
'EIP158': 'SPURIOUS_DRAGON',
38+
'Byzantium': 'BYZANTIUM',
39+
'Constantinople': 'CONSTANTINOPLE',
40+
'ConstantinopleFix': 'PETERSBURG',
41+
'Istanbul': 'ISTANBUL',
42+
'Berlin': 'BERLIN',
43+
'London': 'LONDON',
44+
'Merge': 'MERGE',
45+
'Paris': 'MERGE',
46+
'Shanghai': 'SHANGHAI',
47+
'Cancun': 'CANCUN',
48+
'ShanghaiToCancunAtTime15k': 'CANCUN',
49+
'Prague': 'PRAGUE',
50+
'CancunToPragueAtTime15k': 'PRAGUE',
51+
}
52+
3153
_GST_DISCARD_KEYS: Final = frozenset(
3254
[
3355
'//',
@@ -39,14 +61,14 @@
3961
'lastblockhash',
4062
'hasBigInt',
4163
'config',
64+
'network',
4265
]
4366
)
4467
_GST_LOAD_KEYS: Final = frozenset(
4568
[
4669
'env',
4770
'pre',
4871
'rlp',
49-
'network',
5072
'genesisRLP',
5173
]
5274
)
@@ -113,7 +135,7 @@ def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: s
113135

114136

115137
def _schedule_to_kore(schedule: str) -> App:
116-
return App(f"Lbl{schedule}'Unds'EVM")
138+
return App(f"Lbl{munge(schedule)}'Unds'EVM")
117139

118140

119141
def _mode_to_kore(mode: str) -> App:

‎kevm-pyk/src/kevm_pyk/interpreter.py‎

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@
55
from pyk.kdist import kdist
66
from pyk.ktool.krun import llvm_interpret
77

8-
from .gst_to_kore import filter_gst_keys, gst_to_kore
8+
from .config import DEFAULT_SCHEDULE
9+
from .gst_to_kore import SCHEDULE_MAPPING, filter_gst_keys, gst_to_kore
910

1011
if TYPE_CHECKING:
1112
from collections.abc import Iterator
@@ -15,14 +16,30 @@
1516

1617

1718
def iterate_gst(
18-
gst_data: dict, schedule: str, mode: str, chainid: int, usegas: bool, skipped_keys: frozenset[str] = frozenset()
19+
gst_data: dict,
20+
mode: str,
21+
chainid: int,
22+
usegas: bool,
23+
skipped_keys: frozenset[str] = frozenset(),
24+
schedule: str | None = None,
1925
) -> Iterator[tuple[str, App]]:
2026
"""Yield (test_name, kore_pattern) for each test in GST data after filtering discarded keys."""
2127
for test_name, test in gst_data.items():
2228
if test_name in skipped_keys:
2329
continue
30+
test_schedule = _resolve_schedule(test, schedule)
2431
gst_filtered = {test_name: filter_gst_keys(test)}
25-
yield test_name, gst_to_kore(gst_filtered, schedule, mode, chainid, usegas)
32+
yield test_name, gst_to_kore(gst_filtered, test_schedule, mode, chainid, usegas)
33+
34+
35+
def _resolve_schedule(test: dict, fallback: str | None) -> str:
36+
"""Return schedule from test's network field, falling back to provided schedule or DEFAULT_SCHEDULE."""
37+
network = test.get('network')
38+
if network is not None:
39+
if network not in SCHEDULE_MAPPING:
40+
raise ValueError(f'Unknown network {network}.')
41+
return SCHEDULE_MAPPING[network]
42+
return fallback or DEFAULT_SCHEDULE
2643

2744

2845
def interpret(init_kore: Any, *, check: bool = True) -> Pattern:

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -419,7 +419,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
419419
```k
420420
syntax Set ::= "#loadKeys" [function]
421421
// -------------------------------------
422-
rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("network") SetItem("genesisRLP") )
422+
rule #loadKeys => ( SetItem("env") SetItem("pre") SetItem("rlp") SetItem("genesisRLP") )
423423
424424
rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => load KEY : VAL ~> run TESTID : { REST } ... </k>
425425
requires KEY in #loadKeys

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md‎

Lines changed: 0 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -172,33 +172,6 @@ Here we load the environmental information.
172172
rule <k> loadCallState { .JSONs } => .K ... </k>
173173
```
174174

175-
The `"network"` key allows setting the fee schedule inside the test.
176-
177-
```k
178-
rule <k> load "network" : SCHEDSTRING => .K ... </k>
179-
<schedule> _ => #asScheduleString(SCHEDSTRING) </schedule>
180-
181-
syntax Schedule ::= #asScheduleString ( String ) [symbol(#asScheduleString), function]
182-
// --------------------------------------------------------------------------------------
183-
rule #asScheduleString("Frontier") => FRONTIER
184-
rule #asScheduleString("Homestead") => HOMESTEAD
185-
rule #asScheduleString("EIP150") => TANGERINE_WHISTLE
186-
rule #asScheduleString("EIP158") => SPURIOUS_DRAGON
187-
rule #asScheduleString("Byzantium") => BYZANTIUM
188-
rule #asScheduleString("Constantinople") => CONSTANTINOPLE
189-
rule #asScheduleString("ConstantinopleFix") => PETERSBURG
190-
rule #asScheduleString("Istanbul") => ISTANBUL
191-
rule #asScheduleString("Berlin") => BERLIN
192-
rule #asScheduleString("London") => LONDON
193-
rule #asScheduleString("Merge") => MERGE
194-
rule #asScheduleString("Paris") => MERGE
195-
rule #asScheduleString("Shanghai") => SHANGHAI
196-
rule #asScheduleString("Cancun") => CANCUN
197-
rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN
198-
rule #asScheduleString("Prague") => PRAGUE
199-
rule #asScheduleString("CancunToPragueAtTime15k") => PRAGUE
200-
```
201-
202175
- `#parseJSONs2List` parse a JSON object with string values into a list of value.
203176
```k
204177
syntax List ::= "#parseJSONs2List" "(" JSONs ")" [function]

‎kevm-pyk/src/tests/integration/test_conformance.py‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,6 @@ def compute_chain_id(gst_file: str) -> int:
4444
def test_vm(test_file: Path, save_failing: bool) -> None:
4545
_test(
4646
test_file,
47-
schedule='DEFAULT',
4847
mode='VMTESTS',
4948
usegas=True,
5049
save_failing=save_failing,
@@ -64,7 +63,6 @@ def test_vm(test_file: Path, save_failing: bool) -> None:
6463
def test_rest_vm(test_file: Path, save_failing: bool) -> None:
6564
_test(
6665
test_file,
67-
schedule='DEFAULT',
6866
mode='VMTESTS',
6967
usegas=True,
7068
save_failing=save_failing,
@@ -89,7 +87,6 @@ def test_rest_vm(test_file: Path, save_failing: bool) -> None:
8987
def test_bchain(test_file: Path, save_failing: bool) -> None:
9088
_test(
9189
test_file,
92-
schedule='PRAGUE',
9390
mode='NORMAL',
9491
usegas=True,
9592
save_failing=save_failing,
@@ -109,7 +106,6 @@ def test_bchain(test_file: Path, save_failing: bool) -> None:
109106
def test_rest_bchain(test_file: Path, save_failing: bool) -> None:
110107
_test(
111108
test_file,
112-
schedule='PRAGUE',
113109
mode='NORMAL',
114110
usegas=True,
115111
save_failing=save_failing,

‎kevm-pyk/src/tests/integration/test_execution_spec_tests.py‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,6 @@ def chain_id_always_one(_file: str) -> int:
4141
def test_bchain(test_file: Path, save_failing: bool) -> None:
4242
_test(
4343
test_file,
44-
schedule='PRAGUE',
4544
mode='NORMAL',
4645
usegas=True,
4746
save_failing=save_failing,
@@ -64,7 +63,6 @@ def test_bchain(test_file: Path, save_failing: bool) -> None:
6463
def test_engine_bchain(test_file: Path, save_failing: bool) -> None:
6564
_test(
6665
test_file,
67-
schedule='PRAGUE',
6866
mode='NORMAL',
6967
usegas=True,
7068
save_failing=save_failing,
@@ -87,7 +85,6 @@ def test_engine_bchain(test_file: Path, save_failing: bool) -> None:
8785
def test_state(test_file: Path, save_failing: bool) -> None:
8886
_test(
8987
test_file,
90-
schedule='PRAGUE',
9188
mode='NORMAL',
9289
usegas=True,
9390
save_failing=save_failing,
@@ -110,7 +107,6 @@ def test_state(test_file: Path, save_failing: bool) -> None:
110107
def test_transaction(test_file: Path, save_failing: bool) -> None:
111108
_test(
112109
test_file,
113-
schedule='PRAGUE',
114110
mode='NORMAL',
115111
usegas=True,
116112
save_failing=save_failing,

‎kevm-pyk/src/tests/integration/test_run.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ def test_run(gst_file: Path, update_expected_output: bool) -> None:
3232

3333
actual = ''
3434
# When
35-
for _, init_kore in iterate_gst(gst_data, 'PRAGUE', 'NORMAL', 1, True):
35+
for _, init_kore in iterate_gst(gst_data, 'NORMAL', 1, True):
3636
pattern = interpret(init_kore, check=False)
3737
actual += kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY)
3838

‎kevm-pyk/src/tests/unit/test_gst_to_kore.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ def test_gst_to_kore(gst_path: str, expected_path: str, update_expected_output:
3838
expected_file = REPO_ROOT / expected_path
3939

4040
# When
41-
actuals = [kore for _, kore in iterate_gst(gst_data, 'CANCUN', 'NORMAL', 1, True)]
41+
actuals = [kore for _, kore in iterate_gst(gst_data, 'NORMAL', 1, True)]
4242

4343
# Then
4444
if update_expected_output:

0 commit comments

Comments
 (0)