Add rules for new Prague schedule (#2747)

* fix typos in Makefile

* define Prague schedule

* update execution-spec-tests/failing.llvm

* set Prague as the default schedule for testing

* update expected output

* keep cancun as default schedule for now

* update golden files

Author: anvacaru

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

kevm-pyk/src/kevm_pyk/cli.py

@@ -967,6 +967,7 @@ def evm_chain_args(self) -> ArgumentParser:
             'MERGE',
             'SHANGHAI',
             'CANCUN',
+            'PRAGUE',
         )
         modes = ('NORMAL', 'VMTESTS')
 

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)

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]

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
 ```

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

@@ -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" : { "currentBaseFee"       : (BF:Int)     } => .K ... </k> <baseFee>       _ => BF     </baseFee>
+    rule <k> load "env" : { "currentRandom"        : (RANDAO:Int) } => .K ... </k> <mixHash>       _ => RANDAO </mixHash>
+    rule <k> load "env" : { "currentExcessBlobGas" : (BGAS:Int)   } => .K ... </k> <excessBlobGas> _ => BGAS   </excessBlobGas>
 
     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.

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,

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,

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