Optimize schedule.md

.github/workflows/test-pr.yml

@@ -110,7 +110,7 @@ jobs:
       - name: 'Build targets'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.haskell evm-semantics.kllvm evm-semantics.kllvm-runtime'
       - name: 'Test integration'
-        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration'
+        run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-integration PYTEST_ARGS+=-vv'
       - name: 'Test conformance'
         run: docker exec -u github-user kevm-ci-concrete-${{ github.sha }} /bin/bash -c 'make test-conformance'
       - name: 'Test llvm krun'

Makefile

@@ -136,7 +136,7 @@ KEEP_OUTPUTS  := false
 CHECK         := git --no-pager diff --no-index --ignore-all-space -R
 
 tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_MODE     = VMTESTS
-tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = DEFAULT
+tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = HOMESTEAD
 
 tests/%.run-interactive: tests/%
 	$(POETRY_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND)                          \

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/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json`:
 
 ```sh
-poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
+poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --schedule HOMESTEAD --mode VMTESTS
 ```
 
 To enable the debug symbols for the llvm backend, build using this command:

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.521"
+version = "1.0.522"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.521'
+VERSION: Final = '1.0.522'

kevm-pyk/src/kevm_pyk/cli.py

@@ -300,7 +300,6 @@ def kprove_legacy_args(self) -> ArgumentParser:
     @cached_property
     def evm_chain_args(self) -> ArgumentParser:
         schedules = (
-            'DEFAULT',
             'FRONTIER',
             'HOMESTEAD',
             'TANGERINE_WHISTLE',

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

@@ -83,7 +83,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
     syntax EthereumCommand ::= loadTx ( Account ) [klabel(loadTx)]
  // --------------------------------------------------------------
     rule <k> loadTx(_) => #end EVMC_OUT_OF_GAS ... </k>
-         <schedule> SCHED </schedule>
+         <scheduleTuple> SCHED </scheduleTuple>
          <txPending> ListItem(TXID:Int) ... </txPending>
          <message>
            <msgID>      TXID     </msgID>
@@ -101,8 +101,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
          ...
          </k>
          <schedule> SCHED </schedule>
+         <scheduleTuple> SCHEDT </scheduleTuple>
          <gasPrice> _ => #effectiveGasPrice(TXID) </gasPrice>
-         <callGas> _ => GLIMIT -Int G0(SCHED, CODE, true) </callGas>
+         <callGas> _ => GLIMIT -Int G0(SCHEDT, CODE, true) </callGas>
          <origin> _ => ACCTFROM </origin>
          <callDepth> _ => -1 </callDepth>
          <txPending> ListItem(TXID:Int) ... </txPending>
@@ -122,9 +123,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <nonce> NONCE </nonce>
            ...
          </account>
-         <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
+         <accessedAccounts> _ => #if Ghaswarmcoinbase(SCHEDT) #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
-      requires #hasValidInitCode(lengthBytes(CODE), SCHED)
+      requires #hasValidInitCode(lengthBytes(CODE), SCHEDT)
 
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
@@ -134,8 +135,9 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
          ...
          </k>
          <schedule> SCHED </schedule>
+         <scheduleTuple> SCHEDT </scheduleTuple>
          <gasPrice> _ => #effectiveGasPrice(TXID) </gasPrice>
-         <callGas> _ => GLIMIT -Int G0(SCHED, DATA, false) </callGas>
+         <callGas> _ => GLIMIT -Int G0(SCHEDT, DATA, false) </callGas>
          <origin> _ => ACCTFROM </origin>
          <callDepth> _ => -1 </callDepth>
          <txPending> ListItem(TXID:Int) ... </txPending>
@@ -155,7 +157,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <nonce> NONCE => NONCE +Int 1 </nonce>
            ...
          </account>
-         <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
+         <accessedAccounts> _ => #if Ghaswarmcoinbase(SCHEDT) #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires ACCTTO =/=K .Account
 
@@ -189,32 +191,32 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
                              | #loadAccessListAux ( Account , List ) [klabel(#loadAccessListAux)]
  // ---------------------------------------------------------------------------------------------
     rule <k> #loadAccessList ([ .JSONs ]) => .K ... </k>
-         <schedule> SCHED </schedule>
-      requires Ghasaccesslist << SCHED >>
+         <scheduleTuple> SCHED </scheduleTuple>
+      requires Ghasaccesslist(SCHED)
 
     rule <k> #loadAccessList ([ _ ]) => .K ... </k>
-         <schedule> SCHED </schedule>
-      requires notBool Ghasaccesslist << SCHED >>
+         <scheduleTuple> SCHED </scheduleTuple>
+      requires notBool Ghasaccesslist(SCHED)
 
     rule <k> #loadAccessList ([[ACCT, [STRG:JSONs]], REST])
           => #loadAccessListAux (#asAccount(ACCT), #parseAccessListStorageKeys([STRG]))
           ~> #loadAccessList ([REST])
          ...
          </k>
-         <schedule> SCHED </schedule>
-      requires Ghasaccesslist << SCHED >>
+         <scheduleTuple> SCHED </scheduleTuple>
+      requires Ghasaccesslist(SCHED)
 
     rule <k> #loadAccessListAux (ACCT, (ListItem(STRGK) STRGKS))
           => #accessStorage ACCT STRGK:Int
           ~> #loadAccessListAux (ACCT, STRGKS)
          ...
          </k>
-         <schedule> SCHED </schedule>
-         <callGas> GLIMIT => GLIMIT -Int Gaccessliststoragekey < SCHED > </callGas>
+         <scheduleTuple> SCHED </scheduleTuple>
+         <callGas> GLIMIT => GLIMIT -Int Gaccessliststoragekey(SCHED) </callGas>
 
     rule <k> #loadAccessListAux (ACCT, .List) => #accessAccounts ACCT ... </k>
-         <schedule> SCHED </schedule>
-         <callGas> GLIMIT => GLIMIT -Int Gaccesslistaddress < SCHED > </callGas>
+         <scheduleTuple> SCHED </scheduleTuple>
+         <callGas> GLIMIT => GLIMIT -Int Gaccesslistaddress(SCHED) </callGas>
 ```
 
 -   `exception` only clears from the `<k>` cell if there is an exception preceding it.