Update dependency: deps/kevm_release (#954)

* deps/kevm_release: Set Version 1.0.788 * Sync Poetry files: kevm-pyk version 1.0.788 * flake.{nix,lock}: update Nix derivations * update expected output * Update schedule in loop invariant lemmas * Update expected output --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina <[email protected]> Co-authored-by: Andrei <[email protected]>
runtimeverification · Jan 30, 2025 · 97a1cad · 97a1cad
1 parent d896069
commit 97a1cad
Show file tree

Hide file tree

Showing 56 changed files with 279 additions and 279 deletions.
diff --git a/deps/kevm_release b/deps/kevm_release
@@ -1 +1 @@
-1.0.787
+1.0.788
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,7 +2,7 @@
   description = "Kontrol";
 
   inputs = {
-    kevm.url = "github:runtimeverification/evm-semantics/v1.0.787";
+    kevm.url = "github:runtimeverification/evm-semantics/v1.0.788";
     nixpkgs.follows = "kevm/nixpkgs";
     k-framework.follows = "kevm/k-framework";
     flake-utils.follows = "kevm/flake-utils";

diff --git a/poetry.lock b/poetry.lock
diff --git a/pyproject.toml b/pyproject.toml
@@ -12,7 +12,7 @@ authors = [
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.787", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.788", subdirectory = "kevm-pyk" }
 eth-utils = "^4.1.1"
 pycryptodome = "^3.20.0"
 pyevmasm = "^0.2.3"

diff --git a/src/tests/integration/test-data/lemmas.k b/src/tests/integration/test-data/lemmas.k
@@ -20,7 +20,7 @@ module SUM-TO-N-INVARIANT
       NORMAL
     </mode>
     <schedule>
-      SHANGHAI
+      CANCUN
     </schedule>
     <ethereum>
       <evm>

diff --git a/src/tests/integration/test-data/pausability-lemmas.k b/src/tests/integration/test-data/pausability-lemmas.k
@@ -124,7 +124,7 @@ module PAUSABILITY-LEMMAS [symbolic]
     rule [test-copy-memory-to-memory-summary]:
       <k> #execute ... </k>
       <useGas> false </useGas>
-      <schedule> SHANGHAI </schedule>
+      <schedule> CANCUN </schedule>
       <jumpDests> JUMPDESTS </jumpDests>
       // The program and program counter are symbolic, focusing on the part we will be executing (CP)
       <program> PROGRAM </program>

diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
@@ -39,7 +39,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -88,7 +88,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -267,7 +267,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
@@ -40,7 +40,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/...tegration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/...tegration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
@@ -130,7 +130,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -521,7 +521,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -930,7 +930,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1323,7 +1323,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1717,7 +1717,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/...est-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/...est-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
@@ -179,7 +179,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -570,7 +570,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -979,7 +979,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1372,7 +1372,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1766,7 +1766,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -2164,7 +2164,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -2564,7 +2564,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/...how/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected b/...how/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected
@@ -183,7 +183,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -576,7 +576,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -970,7 +970,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1381,7 +1381,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1779,7 +1779,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -2178,7 +2178,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -2578,7 +2578,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected
@@ -88,7 +88,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -266,7 +266,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/.../test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected b/.../test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected
@@ -157,7 +157,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -343,7 +343,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -533,7 +533,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -724,7 +724,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false

diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
@@ -73,7 +73,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -315,7 +315,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -559,7 +559,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -799,7 +799,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false
@@ -1042,7 +1042,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
                NORMAL
              </mode>
              <schedule>
-               SHANGHAI
+               CANCUN
              </schedule>
              <useGas>
                false