diff --git a/Makefile b/Makefile index 44499278d9..57a7e11756 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 57c10fb60a..36a250d182 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -967,6 +967,7 @@ def evm_chain_args(self) -> ArgumentParser: 'MERGE', 'SHANGHAI', 'CANCUN', + 'PRAGUE', ) modes = ('NORMAL', 'VMTESTS') diff --git a/kevm-pyk/src/kevm_pyk/interpreter.py b/kevm-pyk/src/kevm_pyk/interpreter.py index 3b4171377e..ccd101895d 100644 --- a/kevm-pyk/src/kevm_pyk/interpreter.py +++ b/kevm-pyk/src/kevm_pyk/interpreter.py @@ -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) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 6732b424a3..b2fd55a98f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2003,6 +2003,7 @@ Precompiled Contracts rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON) rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE) rule #precompiledAccountsUB(CANCUN) => 10 + rule #precompiledAccountsUB(PRAGUE) => #precompiledAccountsUB(CANCUN) syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index ad0480d09d..b1d01a4b14 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -415,6 +415,18 @@ A `ScheduleConst` is a constant determined by the fee schedule. orBool SCHEDFLAG ==K Ghasblobhash ) ``` + +### Prague Schedule + +```k + syntax Schedule ::= "PRAGUE" [symbol(PRAGUE_EVM), smtlib(schedule_PRAGUE)] + // -------------------------------------------------------------------------- + rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN > + + rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> + +``` + ```k endmodule ``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index dd1ddec6be..590505e22c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -137,17 +137,19 @@ Here we load the environmental information. ```k rule load "env" : { KEY : ((VAL:String) => #parseWord(VAL)) } ... - 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 load "env" : { KEY : ((VAL:String) => #parseHexWord(VAL)) } ... requires KEY in (SetItem("currentCoinbase") SetItem("previousHash")) // ---------------------------------------------------------------------- - rule load "env" : { "currentCoinbase" : (CB:Int) } => .K ... _ => CB - rule load "env" : { "currentDifficulty" : (DIFF:Int) } => .K ... _ => DIFF - rule load "env" : { "currentGasLimit" : (GLIMIT:Int) } => .K ... _ => GLIMIT - rule load "env" : { "currentNumber" : (NUM:Int) } => .K ... _ => NUM - rule load "env" : { "previousHash" : (HASH:Int) } => .K ... _ => HASH - rule load "env" : { "currentTimestamp" : (TS:Int) } => .K ... _ => TS - rule load "env" : { "currentBaseFee" : (BF:Int) } => .K ... _ => BF + rule load "env" : { "currentCoinbase" : (CB:Int) } => .K ... _ => CB + rule load "env" : { "currentDifficulty" : (DIFF:Int) } => .K ... _ => DIFF + rule load "env" : { "currentGasLimit" : (GLIMIT:Int) } => .K ... _ => GLIMIT + rule load "env" : { "currentNumber" : (NUM:Int) } => .K ... _ => NUM + rule load "env" : { "previousHash" : (HASH:Int) } => .K ... _ => HASH + rule load "env" : { "currentTimestamp" : (TS:Int) } => .K ... _ => TS + rule load "env" : { "currentBaseFee" : (BF:Int) } => .K ... _ => BF + rule load "env" : { "currentRandom" : (RANDAO:Int) } => .K ... _ => RANDAO + rule load "env" : { "currentExcessBlobGas" : (BGAS:Int) } => .K ... _ => BGAS syntax KItem ::= "loadCallState" JSON // ------------------------------------- @@ -188,6 +190,7 @@ The `"network"` key allows setting the fee schedule inside the test. rule #asScheduleString("Shanghai") => SHANGHAI rule #asScheduleString("Cancun") => CANCUN rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN + rule #asScheduleString("Prague") => PRAGUE ``` - `#parseJSONs2List` parse a JSON object with string values into a list of value. diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/kevm-pyk/src/tests/integration/test_conformance.py index 664b81f24d..40fbf8fdd2 100644 --- a/kevm-pyk/src/tests/integration/test_conformance.py +++ b/kevm-pyk/src/tests/integration/test_conformance.py @@ -89,7 +89,7 @@ def test_rest_vm(test_file: Path, save_failing: bool) -> None: def test_bchain(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, @@ -109,7 +109,7 @@ def test_bchain(test_file: Path, save_failing: bool) -> None: def test_rest_bchain(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, diff --git a/kevm-pyk/src/tests/integration/test_execution_spec_tests.py b/kevm-pyk/src/tests/integration/test_execution_spec_tests.py index 6b4ca8fabd..80db5cb50b 100644 --- a/kevm-pyk/src/tests/integration/test_execution_spec_tests.py +++ b/kevm-pyk/src/tests/integration/test_execution_spec_tests.py @@ -41,7 +41,7 @@ def chain_id_always_one(_file: str) -> int: def test_bchain(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, @@ -64,7 +64,7 @@ def test_bchain(test_file: Path, save_failing: bool) -> None: def test_bchain_engine(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, @@ -87,7 +87,7 @@ def test_bchain_engine(test_file: Path, save_failing: bool) -> None: def test_state(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, @@ -110,7 +110,7 @@ def test_state(test_file: Path, save_failing: bool) -> None: def test_transaction(test_file: Path, save_failing: bool) -> None: _test( test_file, - schedule='CANCUN', + schedule='PRAGUE', mode='NORMAL', usegas=True, save_failing=save_failing, diff --git a/kevm-pyk/src/tests/integration/test_run.py b/kevm-pyk/src/tests/integration/test_run.py index d76d2c223e..1f9b4a8e24 100644 --- a/kevm-pyk/src/tests/integration/test_run.py +++ b/kevm-pyk/src/tests/integration/test_run.py @@ -31,7 +31,7 @@ def test_run(gst_file: Path, update_expected_output: bool) -> None: gst_data = json.load(f) # When - pattern = interpret(gst_data, 'CANCUN', 'NORMAL', 1, True, check=False) + pattern = interpret(gst_data, 'PRAGUE', 'NORMAL', 1, True, check=False) actual = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY) # Then