Merge branch 'master' into abstraction-cheatcodes

runtimeverification · Jan 14, 2025 · 7be55d6 · 7be55d6
2 parents ab23771 + f1dec7c
commit 7be55d6
Show file tree

Hide file tree

Showing 44 changed files with 1,199 additions and 216 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.191
+7.1.196
diff --git a/deps/kevm_release b/deps/kevm_release
@@ -1 +1 @@
-1.0.765
+1.0.770
diff --git a/deps/z3 b/deps/z3
@@ -1 +1 @@
-4.13.0
+4.13.4
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.765";
+    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.765", 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/lemmas.k b/src/tests/integration/test-data/lemmas.k
@@ -32,7 +32,7 @@ module SUM-TO-N-INVARIANT
             JUMPDESTS
           </jumpDests>
           <wordStack>
-              (S => (S +Int ((N *Int (N +Int 1)) /Int 2)))
+              (S => (S +Int ((N *Int (N +Int 1)) divInt 2)))
             : 0 
             : (N => 0)
             : 459 
@@ -55,7 +55,7 @@ module SUM-TO-N-INVARIANT
   </kevm>
 
   requires 0 <Int N
-   andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) /Int 2))
+   andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) divInt 2))
    andBool #rangeUInt(256, N)
    andBool #rangeUInt(256, S)
    andBool GAS_AMT >=Int N *Int 178

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