Optimize _<_> schedule operator (#1)

See runtimeverification#2335
Pi-Squared-Inc · Jun 25, 2024 · d2cdd9e · d2cdd9e
1 parent 8ed2042
commit d2cdd9e
Show file tree

Hide file tree

Showing 13 changed files with 1,067 additions and 241 deletions.
diff --git a/Makefile b/Makefile
@@ -135,7 +135,7 @@ KEEP_OUTPUTS  := false
 CHECK         := git --no-pager diff --no-index --ignore-all-space -R
 
 tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_MODE     = VMTESTS
-tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = DEFAULT
+tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = HOMESTEAD
 
 tests/%.run-interactive: tests/%
 	$(POETRY_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND)                          \

diff --git a/README.md b/README.md
@@ -287,7 +287,7 @@ You can call `kevm-pyk --help` to get a quick summary of how to use the script.
 Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`:
 
 ```sh
-poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
+poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json --schedule HOMESTEAD --mode VMTESTS
 ```
 
 To enable the debug symbols for the llvm backend, build using this command:

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -884,7 +884,6 @@ def kprove_legacy_args(self) -> ArgumentParser:
     @cached_property
     def evm_chain_args(self) -> ArgumentParser:
         schedules = (
-            'DEFAULT',
             'FRONTIER',
             'HOMESTEAD',
             'TANGERINE_WHISTLE',

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1718,8 +1718,7 @@ Precompiled Contracts
 
     syntax Int ::= #precompiledAccountsUB ( Schedule ) [klabel(#precompiledAccountsUB), function, total]
  // ----------------------------------------------------------------------------------------------------
-    rule #precompiledAccountsUB(DEFAULT)           => 4
-    rule #precompiledAccountsUB(FRONTIER)          => #precompiledAccountsUB(DEFAULT)
+    rule #precompiledAccountsUB(FRONTIER)          => 4
     rule #precompiledAccountsUB(HOMESTEAD)         => #precompiledAccountsUB(FRONTIER)
     rule #precompiledAccountsUB(TANGERINE_WHISTLE) => #precompiledAccountsUB(HOMESTEAD)
     rule #precompiledAccountsUB(SPURIOUS_DRAGON)   => #precompiledAccountsUB(TANGERINE_WHISTLE)