Update dependency: deps/kevm_release (#928)

* deps/kevm_release: Set Version 1.0.769 * Sync Poetry files: kevm-pyk version 1.0.769 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.770 * Sync Poetry files: kevm-pyk version 1.0.770 * flake.{nix,lock}: update Nix derivations * integrate CREATEDACCOUNTS_CELL in the Kontrol initial state; update expected output * Sync Poetry files: kevm-pyk version 1.0.770 * update expected output for CSE and end to end --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei <[email protected]>
runtimeverification · Jan 14, 2025 · f1dec7c · f1dec7c
1 parent 3603b67
commit f1dec7c
Show file tree

Hide file tree

Showing 41 changed files with 975 additions and 81 deletions.
diff --git a/deps/kevm_release b/deps/kevm_release
@@ -1 +1 @@
-1.0.768
+1.0.770
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.768";
+    kevm.url = "github:runtimeverification/evm-semantics/v1.0.770";
     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.768", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.770", subdirectory = "kevm-pyk" }
 eth-utils = "^4.1.1"
 pycryptodome = "^3.20.0"
 pyevmasm = "^0.2.3"

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -1064,6 +1064,7 @@ def _init_cterm(
             'ACCESSEDSTORAGE_CELL': map_empty(),
             'INTERIMSTATES_CELL': list_empty(),
             'TOUCHEDACCOUNTS_CELL': set_empty(),
+            'CREATEDACCOUNTS_CELL': set_empty(),
             'STATIC_CELL': FALSE,
             'ACCOUNTS_CELL': KEVM.accounts(init_account_list),
         }

diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
@@ -107,6 +107,9 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>

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
@@ -108,6 +108,9 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                    ...
                  </substate>
                  <origin>

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
@@ -261,6 +261,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                      <accessedStorage>
                        .Map
                      </accessedStorage>
+                     <createdAccounts>
+                       .Set
+                     </createdAccounts>
                    </substate> } ) => .List )
                  </interimStates>
                  <touchedAccounts>
@@ -315,6 +318,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -643,6 +649,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                      <accessedStorage>
                        .Map
                      </accessedStorage>
+                     <createdAccounts>
+                       .Set
+                     </createdAccounts>
                    </substate> } ) )
                  </interimStates>
                  <touchedAccounts>
@@ -697,6 +706,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -1049,6 +1061,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                      <accessedStorage>
                        .Map
                      </accessedStorage>
+                     <createdAccounts>
+                       .Set
+                     </createdAccounts>
                    </substate> } ) => .List )
                  </interimStates>
                  <touchedAccounts>
@@ -1103,6 +1118,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -1436,6 +1454,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                      <accessedStorage>
                        .Map
                      </accessedStorage>
+                     <createdAccounts>
+                       .Set
+                     </createdAccounts>
                    </substate> } ) => .List )
                  </interimStates>
                  <touchedAccounts>
@@ -1490,6 +1511,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -1824,6 +1848,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                      <accessedStorage>
                        .Map
                      </accessedStorage>
+                     <createdAccounts>
+                       .Set
+                     </createdAccounts>
                    </substate> } ) => .List )
                  </interimStates>
                  <touchedAccounts>
@@ -1878,6 +1905,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   <createdAccounts>
+                     .Set
+                   </createdAccounts>
                  </substate>
                  <origin>
                    ORIGIN_ID:Int