From 43878bb4f5cf6c9e29cde14872455f3635f1f073 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 5 Jun 2024 19:52:10 +0700
Subject: [PATCH 01/35] Draft implementation and test for `contract` field
 accounts inclusion

---
 src/kontrol/prove.py                          | 88 +++++++++++++++++--
 .../foundry/test/ContractFieldTest.t.sol      | 35 ++++++++
 2 files changed, 117 insertions(+), 6 deletions(-)
 create mode 100644 src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index a47486ee4..554545241 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -30,7 +30,7 @@
 from .foundry import Foundry, foundry_to_xml
 from .hevm import Hevm
 from .options import ConfigType, TraceOptions
-from .solc_to_k import Contract, hex_string_to_int
+from .solc_to_k import Contract, StorageField, hex_string_to_int
 from .utils import parse_test_version_tuple
 
 if TYPE_CHECKING:
@@ -506,6 +506,7 @@ def _method_to_initialized_cfg(
 
     empty_config = foundry.kevm.definition.empty_config(GENERATED_TOP_CELL)
     kcfg, new_node_ids, init_node_id, target_node_id = _method_to_cfg(
+        foundry,
         empty_config,
         test.contract,
         test.method,
@@ -541,6 +542,7 @@ def _method_to_initialized_cfg(
 
 
 def _method_to_cfg(
+    foundry: Foundry,
     empty_config: KInner,
     contract: Contract,
     method: Contract.Method | Contract.Constructor,
@@ -567,6 +569,8 @@ def _method_to_cfg(
         program = contract_code
 
     init_cterm = _init_cterm(
+        foundry,
+        contract,
         empty_config,
         program=program,
         contract_code=contract_code,
@@ -759,6 +763,8 @@ def _init_account(address: int) -> None:
 
 
 def _init_cterm(
+    foundry: Foundry,
+    contract: Contract,
     empty_config: KInner,
     program: KInner,
     contract_code: KInner,
@@ -812,6 +818,8 @@ def _init_cterm(
         'TRACEDATA_CELL': KApply('.List'),
     }
 
+    storage_constraints = []
+
     if config_type == ConfigType.TEST_CONFIG or active_symbolik:
         init_account_list = _create_initial_account_list(contract_code, deployment_state_entries)
         init_subst_test = {
@@ -831,11 +839,21 @@ def _init_cterm(
     else:
         # Symbolic accounts of all relevant contracts
         # Status: Currently, only the executing contract
-        # TODO: Add all other accounts belonging to relevant contracts
-        accounts: list[KInner] = [
-            Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code),
-            KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')),
-        ]
+        # TODO: Add all other accounts belonging to relevant contracts``
+        accounts: list[KInner] = []
+
+        # TODO(palina): executed contract's storage
+        storage_map = KVariable(Foundry.symbolic_contract_prefix() + '_STORAGE', sort=KSort('Map'))
+        # TODO(palina): executed contract's name
+        contract_name = Foundry.symbolic_contract_prefix() + '_ID'
+        new_accounts, storage_constraints, storage_map = _create_cse_accounts(
+            foundry, contract.fields, contract_name, storage_map
+        )
+
+        accounts.extend(new_accounts)
+
+        accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), program, storage_map))
+        accounts.append(KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')))
 
         init_subst_accounts = {'ACCOUNTS_CELL': KEVM.accounts(accounts)}
         init_subst.update(init_subst_accounts)
@@ -864,6 +882,10 @@ def _init_cterm(
             mlEqualsFalse(KApply('_==Int_', [KVariable(contract_id, sort=KSort('Int')), Foundry.address_CHEATCODE()]))
         )
 
+    # TODO(palina): make sure these constraints are getting applied
+    for constraint in storage_constraints:
+        init_cterm.add_constraint(constraint)
+
     # The calling contract is assumed to be in the present accounts for non-tests
     if not (config_type == ConfigType.TEST_CONFIG or active_symbolik):
         init_cterm.add_constraint(
@@ -901,6 +923,60 @@ def _create_initial_account_list(
     return init_account_list
 
 
+def _create_cse_accounts(
+    foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_storage: KApply
+) -> tuple[list[KApply], list[KApply], KApply]:
+    # TODO: call this function recursively
+    new_accounts = []
+    new_account_constraints = []
+
+    for field in storage_fields:
+        if field.data_type.startswith('contract '):
+            contract_type = field.data_type.split(' ')[1]
+            for contract_name, contract_obj in foundry.contracts.items():
+                if contract_name.split('%')[-1] == contract_type:
+                    contract_code = KEVM.bin_runtime(KApply(f'contract_{contract_obj.name_with_path}'))
+                    contract_account_name = 'CONTRACT-' + field.label.upper()
+                    new_account = Foundry.symbolic_account(contract_account_name, contract_code)
+                    new_accounts.append(new_account)
+
+                    # TODO: handle the case where the field has a non-zero offset
+                    contract_storage = KApply(
+                        'Map:update',
+                        contract_storage,
+                        intToken(field.slot),
+                        KVariable(contract_account_name + '_ID'),
+                    )
+
+                    # New contract account is not the cheatcode contract
+                    new_account_constraints.append(
+                        mlEqualsFalse(
+                            KApply(
+                                '_==Int_',
+                                [
+                                    KVariable(contract_account_name + '_ID', sort=KSort('Int')),
+                                    Foundry.address_CHEATCODE(),
+                                ],
+                            )
+                        )
+                    )
+
+                    # New contract account is also not the symbolic contract account being executed
+                    new_account_constraints.append(
+                        mlEqualsFalse(
+                            KApply(
+                                '_==Int_',
+                                [
+                                    KVariable(contract_account_name + '_ID', sort=KSort('Int')),
+                                    KVariable(Foundry.symbolic_contract_prefix(), sort=KSort('Int')),
+                                ],
+                            )
+                        )
+                    )
+
+    return new_accounts, new_account_constraints, contract_storage
+
+
 def _final_cterm(
     empty_config: KInner,
     program: KInner,
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
new file mode 100644
index 000000000..7f53ecb6f
--- /dev/null
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+contract Token {
+    uint256 public totalSupply;
+    
+    constructor(uint256 _totalSupply) {
+        totalSupply = _totalSupply;
+    }
+}
+
+contract Escrow {
+    Token token;
+    uint256 tokenTotalSupply;
+
+    function getTokenTotalSupply() public {
+        uint256 tokenTS = token.totalSupply();
+        tokenTotalSupply = tokenTS + 15;
+    }
+}
+
+contract ContractFieldTest {
+    Escrow escrow; 
+
+    function setUp() public {
+        escrow = new Escrow();
+    }
+
+    /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
+       include `Token token` into the list of accounts in `getTokenTotalSupply`'s summary
+    */
+    function getEscrowToken() public {
+        escrow.getTokenTotalSupply();
+    }
+}
\ No newline at end of file

From 8010577f479f00788041e566f15d79f95b2d0d0d Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Wed, 5 Jun 2024 12:57:42 +0000
Subject: [PATCH 02/35] Set Version: 0.1.301

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 35c5ac5a5..350a67b2e 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.299
+0.1.301
diff --git a/pyproject.toml b/pyproject.toml
index 8fe2a7b2c..65c51db9c 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.299"
+version = "0.1.301"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 7289b1f05..4c7181e9f 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.299'
+VERSION: Final = '0.1.301'

From e3794f8165a19b254b5a9ef3ea3880a79362cd5e Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Wed, 5 Jun 2024 13:43:16 +0000
Subject: [PATCH 03/35] Set Version: 0.1.301

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 9f5aa14b4..350a67b2e 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.300
+0.1.301
diff --git a/pyproject.toml b/pyproject.toml
index aa34477a6..5a39e4e93 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.300"
+version = "0.1.301"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index ce4002296..4c7181e9f 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.300'
+VERSION: Final = '0.1.301'

From a78dbb672c11561139bc4007ef9347b99727694e Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Thu, 6 Jun 2024 07:06:40 +0000
Subject: [PATCH 04/35] Set Version: 0.1.302

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 350a67b2e..d8fcdfdd3 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.301
+0.1.302
diff --git a/pyproject.toml b/pyproject.toml
index 81c5037c8..8faab4a2f 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.301"
+version = "0.1.302"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 4c7181e9f..777e006ac 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.301'
+VERSION: Final = '0.1.302'

From 6092452b556a8ad4196fca4b08e38b3c8e8d0fbd Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Thu, 6 Jun 2024 18:31:31 +0700
Subject: [PATCH 05/35] Use (simple) `#lookup` constraint for `contract` field
 in storage

---
 src/kontrol/prove.py | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 481353930..1b8969d46 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -570,10 +570,10 @@ def _method_to_cfg(
 
     init_cterm = _init_cterm(
         foundry,
-        contract,
         empty_config,
         program=program,
         contract_code=bytesToken(contract_code),
+        storage_fields=contract.fields,
         use_gas=use_gas,
         deployment_state_entries=deployment_state_entries,
         calldata=calldata,
@@ -764,10 +764,10 @@ def _init_account(address: int) -> None:
 
 def _init_cterm(
     foundry: Foundry,
-    contract: Contract,
     empty_config: KInner,
     program: bytes,
     contract_code: KInner,
+    storage_fields: list[StorageField],
     use_gas: bool,
     config_type: ConfigType,
     active_symbolik: bool,
@@ -848,7 +848,7 @@ def _init_cterm(
         # TODO(palina): executed contract's name
         contract_name = Foundry.symbolic_contract_prefix() + '_ID'
         new_accounts, storage_constraints, storage_map = _create_cse_accounts(
-            foundry, contract.fields, contract_name, storage_map
+            foundry, storage_fields, contract_name, storage_map
         )
 
         accounts.extend(new_accounts)
@@ -942,11 +942,18 @@ def _create_cse_accounts(
                     new_accounts.append(new_account)
 
                     # TODO: handle the case where the field has a non-zero offset
-                    contract_storage = KApply(
-                        'Map:update',
-                        contract_storage,
-                        intToken(field.slot),
-                        KVariable(contract_account_name + '_ID'),
+                    # maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 )
+                    contract_storage_lookup = KApply(
+                        '_&Int_',
+                        [
+                            intToken(1461501637330902918203684832716283019655932542975),
+                            KEVM.lookup(contract_storage, intToken(field.slot)),
+                        ],
+                    )
+                    new_account_constraints.append(
+                        mlEqualsTrue(
+                            KApply('_==Int_', [contract_storage_lookup, KVariable(contract_account_name + '_ID')])
+                        )
                     )
 
                     # New contract account is not the cheatcode contract

From fcd95fa060f8c337cf2fea76a4b9544ec40e4c6f Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Thu, 6 Jun 2024 19:27:25 +0700
Subject: [PATCH 06/35] Minor formatting

---
 src/kontrol/prove.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 1b8969d46..38097c213 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -30,7 +30,7 @@
 from .foundry import Foundry, foundry_to_xml
 from .hevm import Hevm
 from .options import ConfigType, TraceOptions
-from .solc_to_k import Contract, StorageField, hex_string_to_int
+from .solc_to_k import Contract, hex_string_to_int
 from .utils import parse_test_version_tuple
 
 if TYPE_CHECKING:
@@ -42,6 +42,7 @@
 
     from .deployment import DeploymentStateEntry
     from .options import ProveOptions
+    from .solc_to_k import StorageField
 
 _LOGGER: Final = logging.getLogger(__name__)
 
@@ -767,7 +768,7 @@ def _init_cterm(
     empty_config: KInner,
     program: bytes,
     contract_code: KInner,
-    storage_fields: list[StorageField],
+    storage_fields: tuple[StorageField, ...],
     use_gas: bool,
     config_type: ConfigType,
     active_symbolik: bool,

From a336d157100782c1212fdcd76dcf29b7cbb7da8b Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Fri, 7 Jun 2024 08:11:30 +0000
Subject: [PATCH 07/35] Set Version: 0.1.303

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index d8fcdfdd3..2bfbb8b94 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.302
+0.1.303
diff --git a/pyproject.toml b/pyproject.toml
index 8faab4a2f..5a4e4d4c4 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.302"
+version = "0.1.303"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 777e006ac..eb73b01b7 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.302'
+VERSION: Final = '0.1.303'

From 47f126311a6fe116cde4348a27e236bcfc5e706d Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Fri, 7 Jun 2024 16:39:03 +0700
Subject: [PATCH 08/35] Draft implementation refactoring

---
 src/kontrol/prove.py                                | 13 ++++++-------
 .../integration/test-data/foundry-dependency-all    |  1 +
 .../test-data/foundry/test/ContractFieldTest.t.sol  |  5 +++--
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 5679ed56b..00b3b3a03 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -831,7 +831,7 @@ def _init_cterm(
         'TRACEDATA_CELL': KApply('.List'),
     }
 
-    storage_constraints = []
+    storage_constraints: list[KApply] = []
 
     if config_type == ConfigType.TEST_CONFIG or active_symbolik:
         init_account_list = _create_initial_account_list(contract_code, deployment_state_entries)
@@ -865,7 +865,7 @@ def _init_cterm(
 
         accounts.extend(new_accounts)
 
-        accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), program, storage_map))
+        accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code, storage_map))
         accounts.append(KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')))
 
         init_subst_accounts = {'ACCOUNTS_CELL': KEVM.accounts(accounts)}
@@ -895,9 +895,8 @@ def _init_cterm(
             mlEqualsFalse(KApply('_==Int_', [KVariable(contract_id, sort=KSort('Int')), Foundry.address_CHEATCODE()]))
         )
 
-    # TODO(palina): make sure these constraints are getting applied
     for constraint in storage_constraints:
-        init_cterm.add_constraint(constraint)
+        init_cterm = init_cterm.add_constraint(constraint)
 
     # The calling contract is assumed to be in the present accounts for non-tests
     if not (config_type == ConfigType.TEST_CONFIG or active_symbolik):
@@ -937,8 +936,8 @@ def _create_initial_account_list(
 
 
 def _create_cse_accounts(
-    foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_storage: KApply
-) -> tuple[list[KApply], list[KApply], KApply]:
+    foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_storage: KVariable
+) -> tuple[list[KApply], list[KApply], KVariable]:
     # TODO: call this function recursively
     new_accounts = []
     new_account_constraints = []
@@ -948,7 +947,7 @@ def _create_cse_accounts(
             contract_type = field.data_type.split(' ')[1]
             for contract_name, contract_obj in foundry.contracts.items():
                 if contract_name.split('%')[-1] == contract_type:
-                    contract_code = KEVM.bin_runtime(KApply(f'contract_{contract_obj.name_with_path}'))
+                    contract_code = bytesToken(bytes.fromhex(contract_obj.deployed_bytecode))
                     contract_account_name = 'CONTRACT-' + field.label.upper()
                     new_account = Foundry.symbolic_account(contract_account_name, contract_code)
                     new_accounts.append(new_account)
diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
index 5880aa6c5..a9720140c 100644
--- a/src/tests/integration/test-data/foundry-dependency-all
+++ b/src/tests/integration/test-data/foundry-dependency-all
@@ -7,6 +7,7 @@ ArithmeticContract.add_sub_external(uint256,uint256,uint256)
 CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
+ContractFieldTest.testEscrowToken()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index 7f53ecb6f..3e00aba5d 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -1,5 +1,6 @@
 // SPDX-License-Identifier: UNLICENSED
 pragma solidity =0.8.13;
+import {Test} from "forge-std/Test.sol";
 
 contract Token {
     uint256 public totalSupply;
@@ -19,7 +20,7 @@ contract Escrow {
     }
 }
 
-contract ContractFieldTest {
+contract ContractFieldTest is Test {
     Escrow escrow; 
 
     function setUp() public {
@@ -29,7 +30,7 @@ contract ContractFieldTest {
     /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
        include `Token token` into the list of accounts in `getTokenTotalSupply`'s summary
     */
-    function getEscrowToken() public {
+    function testEscrowToken() public {
         escrow.getTokenTotalSupply();
     }
 }
\ No newline at end of file

From 8bae8cfb3aa5b2391a22672686dbc058f601bb7a Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Sat, 8 Jun 2024 08:59:14 +0000
Subject: [PATCH 09/35] Set Version: 0.1.306

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 75ed58cc7..8ae56a816 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.305
+0.1.306
diff --git a/pyproject.toml b/pyproject.toml
index 1a2ca778a..0f74ae7e8 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.305"
+version = "0.1.306"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 01dd5cbd0..917ddfd85 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.305'
+VERSION: Final = '0.1.306'

From b8aa43c21847e7f823d2ee9e8a819213ee358706 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Sat, 8 Jun 2024 14:44:45 +0100
Subject: [PATCH 10/35] renaming contracts to avoid conflicts, removing
 unneeded constraints

---
 src/kontrol/prove.py                          | 16 +++----------
 .../foundry/test/ContractFieldTest.t.sol      | 23 +++++++++++--------
 2 files changed, 16 insertions(+), 23 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index f65c3f3f0..5a4f73f84 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -945,6 +945,9 @@ def _create_cse_accounts(
         if field.data_type.startswith('contract '):
             contract_type = field.data_type.split(' ')[1]
             for contract_name, contract_obj in foundry.contracts.items():
+                suffix = contract_name.split('%')[-1]
+                # TODO: this is not enough, it is possible that the same contract comes with
+                # src% and test%, in which case we don't know automatically which one to choose
                 if contract_name.split('%')[-1] == contract_type:
                     contract_code = bytesToken(bytes.fromhex(contract_obj.deployed_bytecode))
                     contract_account_name = 'CONTRACT-' + field.label.upper()
@@ -979,19 +982,6 @@ def _create_cse_accounts(
                         )
                     )
 
-                    # New contract account is also not the symbolic contract account being executed
-                    new_account_constraints.append(
-                        mlEqualsFalse(
-                            KApply(
-                                '_==Int_',
-                                [
-                                    KVariable(contract_account_name + '_ID', sort=KSort('Int')),
-                                    KVariable(Foundry.symbolic_contract_prefix(), sort=KSort('Int')),
-                                ],
-                            )
-                        )
-                    )
-
     return new_accounts, new_account_constraints, contract_storage
 
 
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index 3e00aba5d..4ac438040 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -2,35 +2,38 @@
 pragma solidity =0.8.13;
 import {Test} from "forge-std/Test.sol";
 
-contract Token {
+contract TestToken {
     uint256 public totalSupply;
-    
+
     constructor(uint256 _totalSupply) {
         totalSupply = _totalSupply;
     }
 }
 
 contract Escrow {
-    Token token;
+    TestToken token;
     uint256 tokenTotalSupply;
 
-    function getTokenTotalSupply() public {
-        uint256 tokenTS = token.totalSupply();
-        tokenTotalSupply = tokenTS + 15;
+    constructor(uint256 _totalSupply) {
+        token = new TestToken(_totalSupply);
+    }
+
+    function getTokenTotalSupply() public returns (uint256) {
+        return token.totalSupply() + 15;
     }
 }
 
 contract ContractFieldTest is Test {
-    Escrow escrow; 
+    Escrow escrow;
 
     function setUp() public {
-        escrow = new Escrow();
+        escrow = new Escrow(12330);
     }
 
     /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
-       include `Token token` into the list of accounts in `getTokenTotalSupply`'s summary
+       include `TestToken token` into the list of accounts in `getTokenTotalSupply`'s summary
     */
     function testEscrowToken() public {
-        escrow.getTokenTotalSupply();
+        assert(escrow.getTokenTotalSupply() == 12345);
     }
 }
\ No newline at end of file

From 1c5795d3b4bcea3db607cd724abd8632e758f515 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Mon, 10 Jun 2024 10:34:30 +0100
Subject: [PATCH 11/35] minor streamlining

---
 .../integration/test-data/foundry/test/ContractFieldTest.t.sol   | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index 4ac438040..b42d5b1a1 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -12,7 +12,6 @@ contract TestToken {
 
 contract Escrow {
     TestToken token;
-    uint256 tokenTotalSupply;
 
     constructor(uint256 _totalSupply) {
         token = new TestToken(_totalSupply);

From 90e9e635af1dfb7cc2cec81255210aa0d2de7892 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Tue, 11 Jun 2024 07:25:15 +0000
Subject: [PATCH 12/35] Set Version: 0.1.307

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 8ae56a816..0acdb21eb 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.306
+0.1.307
diff --git a/pyproject.toml b/pyproject.toml
index 0f74ae7e8..f8c393b4a 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.306"
+version = "0.1.307"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 917ddfd85..98e5505e6 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.306'
+VERSION: Final = '0.1.307'

From 4941ea1696246c314584dd6c3df42f9705daf4d5 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Tue, 11 Jun 2024 08:00:57 +0000
Subject: [PATCH 13/35] Set Version: 0.1.308

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 0acdb21eb..217f5022a 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.307
+0.1.308
diff --git a/pyproject.toml b/pyproject.toml
index f8c393b4a..c7170608a 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.307"
+version = "0.1.308"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 98e5505e6..515a8a132 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.307'
+VERSION: Final = '0.1.308'

From be0c2a385e5b3a4a9952b6ad0aa3d905a7698535 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 11 Jun 2024 09:21:48 +0100
Subject: [PATCH 14/35] removing unused variable

---
 src/kontrol/prove.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index e95452228..ea597320f 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -954,7 +954,6 @@ def _create_cse_accounts(
         if field.data_type.startswith('contract '):
             contract_type = field.data_type.split(' ')[1]
             for contract_name, contract_obj in foundry.contracts.items():
-                suffix = contract_name.split('%')[-1]
                 # TODO: this is not enough, it is possible that the same contract comes with
                 # src% and test%, in which case we don't know automatically which one to choose
                 if contract_name.split('%')[-1] == contract_type:

From a736864eaa376f8f6f0d4ed2d5c574f39e04776f Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 11 Jun 2024 09:23:00 +0100
Subject: [PATCH 15/35] renaming re-assigned variable

---
 src/kontrol/prove.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index ea597320f..c6cb0b7e7 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -914,8 +914,8 @@ def _init_cterm(
         )
 
     if isinstance(method, Contract.Constructor) and len(arg_constraints) > 0:
-        for constraint in arg_constraints:
-            init_cterm = init_cterm.add_constraint(mlEqualsTrue(constraint))
+        for arg_constraint in arg_constraints:
+            init_cterm = init_cterm.add_constraint(mlEqualsTrue(arg_constraint))
 
     init_cterm = KEVM.add_invariant(init_cterm)
 

From 7e71976078c51c5563c860d779938b4603eb231e Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Tue, 11 Jun 2024 16:13:12 +0700
Subject: [PATCH 16/35] Make `_create_cse_accounts` apply recursively on
 `contract` field accounts

---
 src/kontrol/prove.py | 41 ++++++++++++++++++-----------------------
 1 file changed, 18 insertions(+), 23 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index c6cb0b7e7..6fd23a119 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -853,21 +853,10 @@ def _init_cterm(
         init_subst.update(init_subst_test)
     else:
         # Symbolic accounts of all relevant contracts
-        # Status: Currently, only the executing contract
-        # TODO: Add all other accounts belonging to relevant contracts``
-        accounts: list[KInner] = []
-
-        # TODO(palina): executed contract's storage
-        storage_map = KVariable(Foundry.symbolic_contract_prefix() + '_STORAGE', sort=KSort('Map'))
-        # TODO(palina): executed contract's name
-        contract_name = Foundry.symbolic_contract_prefix() + '_ID'
-        new_accounts, storage_constraints, storage_map = _create_cse_accounts(
-            foundry, storage_fields, contract_name, storage_map
+        accounts, storage_constraints = _create_cse_accounts(
+            foundry, storage_fields, Foundry.symbolic_contract_prefix(), contract_code
         )
 
-        accounts.extend(new_accounts)
-
-        accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code, storage_map))
         accounts.append(KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')))
 
         init_subst_accounts = {'ACCOUNTS_CELL': KEVM.accounts(accounts)}
@@ -944,23 +933,23 @@ def _create_initial_account_list(
 
 
 def _create_cse_accounts(
-    foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_storage: KVariable
-) -> tuple[list[KApply], list[KApply], KVariable]:
-    # TODO: call this function recursively
+    foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_code: KInner
+) -> tuple[list[KApply], list[KApply]]:
     new_accounts = []
     new_account_constraints = []
 
+    storage_map = KVariable(contract_name + '_STORAGE', sort=KSort('Map'))
+    new_accounts.append(Foundry.symbolic_account(contract_name, contract_code, storage_map))
+
     for field in storage_fields:
         if field.data_type.startswith('contract '):
             contract_type = field.data_type.split(' ')[1]
-            for contract_name, contract_obj in foundry.contracts.items():
+            for full_contract_name, contract_obj in foundry.contracts.items():
                 # TODO: this is not enough, it is possible that the same contract comes with
                 # src% and test%, in which case we don't know automatically which one to choose
-                if contract_name.split('%')[-1] == contract_type:
-                    contract_code = bytesToken(bytes.fromhex(contract_obj.deployed_bytecode))
+                if full_contract_name.split('%')[-1] == contract_type:
+                    contract_account_code = bytesToken(bytes.fromhex(contract_obj.deployed_bytecode))
                     contract_account_name = 'CONTRACT-' + field.label.upper()
-                    new_account = Foundry.symbolic_account(contract_account_name, contract_code)
-                    new_accounts.append(new_account)
 
                     # TODO: handle the case where the field has a non-zero offset
                     # maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 )
@@ -968,7 +957,7 @@ def _create_cse_accounts(
                         '_&Int_',
                         [
                             intToken(1461501637330902918203684832716283019655932542975),
-                            KEVM.lookup(contract_storage, intToken(field.slot)),
+                            KEVM.lookup(storage_map, intToken(field.slot)),
                         ],
                     )
                     new_account_constraints.append(
@@ -990,7 +979,13 @@ def _create_cse_accounts(
                         )
                     )
 
-    return new_accounts, new_account_constraints, contract_storage
+                    contract_accounts, contract_constraints = _create_cse_accounts(
+                        foundry, contract_obj.fields, contract_account_name, contract_account_code
+                    )
+                    new_accounts.extend(contract_accounts)
+                    new_account_constraints.extend(contract_constraints)
+
+    return new_accounts, new_account_constraints
 
 
 def _final_cterm(

From b1509f76cca018c2de0cbda9f9937efef3a9b533 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Tue, 11 Jun 2024 16:27:19 +0700
Subject: [PATCH 17/35] Code quality improvement

---
 src/kontrol/prove.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 6fd23a119..604fb7f84 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -852,6 +852,7 @@ def _init_cterm(
         }
         init_subst.update(init_subst_test)
     else:
+        accounts: list[KInner] = []
         # Symbolic accounts of all relevant contracts
         accounts, storage_constraints = _create_cse_accounts(
             foundry, storage_fields, Foundry.symbolic_contract_prefix(), contract_code
@@ -934,9 +935,9 @@ def _create_initial_account_list(
 
 def _create_cse_accounts(
     foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_code: KInner
-) -> tuple[list[KApply], list[KApply]]:
-    new_accounts = []
-    new_account_constraints = []
+) -> tuple[list[KInner], list[KApply]]:
+    new_accounts: list[KInner] = []
+    new_account_constraints: list[KApply] = []
 
     storage_map = KVariable(contract_name + '_STORAGE', sort=KSort('Map'))
     new_accounts.append(Foundry.symbolic_account(contract_name, contract_code, storage_map))

From a085c81a324c49b2439ad2491da7933bcae19cb9 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Tue, 11 Jun 2024 09:27:34 +0000
Subject: [PATCH 18/35] Set Version: 0.1.309

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 217f5022a..626c1b0cf 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.308
+0.1.309
diff --git a/pyproject.toml b/pyproject.toml
index c7170608a..e33dc2016 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.308"
+version = "0.1.309"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 515a8a132..8a2f1cf8d 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.308'
+VERSION: Final = '0.1.309'

From c5c452c39d9a34f262e843165c0d3a9fd3949037 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Tue, 11 Jun 2024 17:30:45 +0700
Subject: [PATCH 19/35] Avoid adding new accs for constructors, add new CSE
 test for recursive storage building

---
 src/kontrol/prove.py                          |  13 +-
 .../test-data/foundry-dependency-all          |   1 +
 .../test-data/foundry/src/cse/Accounts.sol    |  34 +++
 .../test-data/show/contracts.k.expected       | 202 ++++++++++++++++++
 .../test-data/show/foundry.k.expected         |  54 ++++-
 5 files changed, 297 insertions(+), 7 deletions(-)
 create mode 100644 src/tests/integration/test-data/foundry/src/cse/Accounts.sol

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 604fb7f84..f3fbc5564 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -853,10 +853,15 @@ def _init_cterm(
         init_subst.update(init_subst_test)
     else:
         accounts: list[KInner] = []
-        # Symbolic accounts of all relevant contracts
-        accounts, storage_constraints = _create_cse_accounts(
-            foundry, storage_fields, Foundry.symbolic_contract_prefix(), contract_code
-        )
+
+        if isinstance(method, Contract.Constructor):
+            # Symbolic account for the contract being executed
+            accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code))
+        else:
+            # Symbolic accounts of all relevant contracts
+            accounts, storage_constraints = _create_cse_accounts(
+                foundry, storage_fields, Foundry.symbolic_contract_prefix(), contract_code
+            )
 
         accounts.append(KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')))
 
diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
index a9720140c..c6ecf9343 100644
--- a/src/tests/integration/test-data/foundry-dependency-all
+++ b/src/tests/integration/test-data/foundry-dependency-all
@@ -8,6 +8,7 @@ CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
 ContractFieldTest.testEscrowToken()
+CompositionalAccounts.getEscrowToken()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)
diff --git a/src/tests/integration/test-data/foundry/src/cse/Accounts.sol b/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
new file mode 100644
index 000000000..a36409ede
--- /dev/null
+++ b/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+import {Test} from "forge-std/Test.sol";
+
+contract CompositionalToken {
+    uint256 public totalSupply;
+
+    constructor(uint256 _totalSupply) {
+        totalSupply = _totalSupply;
+    }
+}
+
+contract CompositionalEscrow {
+    CompositionalToken cseToken;
+
+    constructor(uint256 _totalSupply) {
+        cseToken = new CompositionalToken(_totalSupply);
+    }
+
+    function getTokenTotalSupply() public returns (uint256) {
+        return cseToken.totalSupply() + 15;
+    }
+}
+
+contract CompositionalAccounts {
+    CompositionalEscrow cseEscrow;
+
+    /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
+       include `CompositionalEscrow escrow`and `CompositionalToken token` into the list of accounts in `getEscrowToken`'s summary
+    */
+    function getEscrowToken() public {
+        assert(cseEscrow.getTokenTotalSupply() == 12345);
+    }
+}
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index ff068b97c..f39630875 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -227,6 +227,63 @@ module S2KtestZModAccountParamsTest-CONTRACT
     rule  ( selector ( "test_getNonce_unknownSymbolic(address)" ) => 3941547284 )
       
 
+endmodule
+
+module S2KsrcZModcseZModCompositionalAccounts-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KsrcZModcseZModCompositionalAccountsContract
+    
+    syntax S2KsrcZModcseZModCompositionalAccountsContract ::= "S2KsrcZModcseZModCompositionalAccounts" [symbol(""), klabel(contract_src%cse%CompositionalAccounts)]
+    
+    syntax Bytes ::= S2KsrcZModcseZModCompositionalAccountsContract "." S2KsrcZModcseZModCompositionalAccountsMethod [function, symbol(""), klabel(method_src%cse%CompositionalAccounts)]
+    
+    syntax S2KsrcZModcseZModCompositionalAccountsMethod ::= "S2KgetEscrowToken" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalAccounts_S2KgetEscrowToken_)]
+    
+    rule  ( S2KsrcZModcseZModCompositionalAccounts . S2KgetEscrowToken ( ) => #abiCallData ( "getEscrowToken" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "getEscrowToken()" ) => 1851159305 )
+      
+
+endmodule
+
+module S2KsrcZModcseZModCompositionalEscrow-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KsrcZModcseZModCompositionalEscrowContract
+    
+    syntax S2KsrcZModcseZModCompositionalEscrowContract ::= "S2KsrcZModcseZModCompositionalEscrow" [symbol(""), klabel(contract_src%cse%CompositionalEscrow)]
+    
+    syntax Bytes ::= S2KsrcZModcseZModCompositionalEscrowContract "." S2KsrcZModcseZModCompositionalEscrowMethod [function, symbol(""), klabel(method_src%cse%CompositionalEscrow)]
+    
+    syntax S2KsrcZModcseZModCompositionalEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalEscrow_S2KgetTokenTotalSupply_)]
+    
+    rule  ( S2KsrcZModcseZModCompositionalEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
+      
+
+endmodule
+
+module S2KsrcZModcseZModCompositionalToken-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KsrcZModcseZModCompositionalTokenContract
+    
+    syntax S2KsrcZModcseZModCompositionalTokenContract ::= "S2KsrcZModcseZModCompositionalToken" [symbol(""), klabel(contract_src%cse%CompositionalToken)]
+    
+    syntax Bytes ::= S2KsrcZModcseZModCompositionalTokenContract "." S2KsrcZModcseZModCompositionalTokenMethod [function, symbol(""), klabel(method_src%cse%CompositionalToken)]
+    
+    syntax S2KsrcZModcseZModCompositionalTokenMethod ::= "S2KtotalSupply" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalToken_S2KtotalSupply_)]
+    
+    rule  ( S2KsrcZModcseZModCompositionalToken . S2KtotalSupply ( ) => #abiCallData ( "totalSupply" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "totalSupply()" ) => 404098525 )
+      
+
 endmodule
 
 module S2KtestZModAddrTest-CONTRACT
@@ -2851,6 +2908,151 @@ module S2KtestZModContractBTest-CONTRACT
     rule  ( selector ( "testNumberIs42()" ) => 795542700 )
       
 
+endmodule
+
+module S2KtestZModContractFieldTest-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KtestZModContractFieldTestContract
+    
+    syntax S2KtestZModContractFieldTestContract ::= "S2KtestZModContractFieldTest" [symbol(""), klabel(contract_test%ContractFieldTest)]
+    
+    syntax Bytes ::= S2KtestZModContractFieldTestContract "." S2KtestZModContractFieldTestMethod [function, symbol(""), klabel(method_test%ContractFieldTest)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KISZUndTEST_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KexcludeArtifacts_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KexcludeContracts_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KexcludeSenders_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2Kfailed" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2Kfailed_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KsetUp" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KsetUp_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtargetArtifactSelectors_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtargetArtifacts_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtargetContracts" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtargetContracts_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtargetSelectors_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtargetSenders" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtargetSenders_)]
+    
+    syntax S2KtestZModContractFieldTestMethod ::= "S2KtestEscrowToken" "(" ")" [symbol(""), klabel(method_test%ContractFieldTest_S2KtestEscrowToken_)]
+    
+    rule  ( S2KtestZModContractFieldTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KsetUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModContractFieldTest . S2KtestEscrowToken ( ) => #abiCallData ( "testEscrowToken" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+      
+    
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+      
+    
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+      
+    
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+      
+    
+    rule  ( selector ( "failed()" ) => 3124842406 )
+      
+    
+    rule  ( selector ( "setUp()" ) => 177362148 )
+      
+    
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+      
+    
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+      
+    
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+      
+    
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+      
+    
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+      
+    
+    rule  ( selector ( "testEscrowToken()" ) => 892426400 )
+      
+
+endmodule
+
+module S2KtestZModEscrow-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KtestZModEscrowContract
+    
+    syntax S2KtestZModEscrowContract ::= "S2KtestZModEscrow" [symbol(""), klabel(contract_test%Escrow)]
+    
+    syntax Bytes ::= S2KtestZModEscrowContract "." S2KtestZModEscrowMethod [function, symbol(""), klabel(method_test%Escrow)]
+    
+    syntax S2KtestZModEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%Escrow_S2KgetTokenTotalSupply_)]
+    
+    rule  ( S2KtestZModEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
+      
+
+endmodule
+
+module S2KtestZModTestToken-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KtestZModTestTokenContract
+    
+    syntax S2KtestZModTestTokenContract ::= "S2KtestZModTestToken" [symbol(""), klabel(contract_test%TestToken)]
+    
+    syntax Bytes ::= S2KtestZModTestTokenContract "." S2KtestZModTestTokenMethod [function, symbol(""), klabel(method_test%TestToken)]
+    
+    syntax S2KtestZModTestTokenMethod ::= "S2KtotalSupply" "(" ")" [symbol(""), klabel(method_test%TestToken_S2KtotalSupply_)]
+    
+    rule  ( S2KtestZModTestToken . S2KtotalSupply ( ) => #abiCallData ( "totalSupply" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "totalSupply()" ) => 404098525 )
+      
+
 endmodule
 
 module S2KtestZModCounter-CONTRACT
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 2383f33aa..5b61734a2 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -8,6 +8,9 @@ module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION
     imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
     imports public S2KtestZModAccountParamsTest-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalAccounts-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalEscrow-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalToken-VERIFICATION
     imports public S2KtestZModAddrTest-VERIFICATION
     imports public S2KtestZModAllowChangesTest-VERIFICATION
     imports public S2KtestZModValueStore-VERIFICATION
@@ -36,6 +39,9 @@ module FOUNDRY-MAIN
     imports public S2KtestZModImportedContract-VERIFICATION
     imports public S2KtestZModContractTest-VERIFICATION
     imports public S2KtestZModContractBTest-VERIFICATION
+    imports public S2KtestZModContractFieldTest-VERIFICATION
+    imports public S2KtestZModEscrow-VERIFICATION
+    imports public S2KtestZModTestToken-VERIFICATION
     imports public S2KtestZModCounter-VERIFICATION
     imports public S2KtestZModCounterTest-VERIFICATION
     imports public S2KsrcZModDeploymentState-VERIFICATION
@@ -137,9 +143,9 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole2-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
-    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
-    
-    
+    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION    
+
+
 
 endmodule
 
@@ -162,6 +168,27 @@ module S2KtestZModAccountParamsTest-VERIFICATION
     
     
 
+endmodule
+
+module S2KsrcZModcseZModCompositionalAccounts-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalAccounts-CONTRACT
+    
+    
+
+endmodule
+
+module S2KsrcZModcseZModCompositionalEscrow-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalEscrow-CONTRACT
+    
+    
+
+endmodule
+
+module S2KsrcZModcseZModCompositionalToken-VERIFICATION
+    imports public S2KsrcZModcseZModCompositionalToken-CONTRACT
+    
+    
+
 endmodule
 
 module S2KtestZModAddrTest-VERIFICATION
@@ -360,6 +387,27 @@ module S2KtestZModContractBTest-VERIFICATION
     
     
 
+endmodule
+
+module S2KtestZModContractFieldTest-VERIFICATION
+    imports public S2KtestZModContractFieldTest-CONTRACT
+    
+    
+
+endmodule
+
+module S2KtestZModEscrow-VERIFICATION
+    imports public S2KtestZModEscrow-CONTRACT
+    
+    
+
+endmodule
+
+module S2KtestZModTestToken-VERIFICATION
+    imports public S2KtestZModTestToken-CONTRACT
+    
+    
+
 endmodule
 
 module S2KtestZModCounter-VERIFICATION

From 3c0b3ce9fb54fba6cbeb0ed1bf5640c02ea36ae0 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Tue, 11 Jun 2024 17:54:27 +0700
Subject: [PATCH 20/35] Enforce same symbolic storage variable name between
 constructor and functions

---
 src/kontrol/prove.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index f3fbc5564..3c13893be 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -856,7 +856,8 @@ def _init_cterm(
 
         if isinstance(method, Contract.Constructor):
             # Symbolic account for the contract being executed
-            accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code))
+            storage_map = KVariable(Foundry.symbolic_contract_prefix() + '_STORAGE_ID', sort=KSort('Map'))
+            accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code, storage_map))
         else:
             # Symbolic accounts of all relevant contracts
             accounts, storage_constraints = _create_cse_accounts(

From a46b3ec0b253d5fe41beded36f3cd9f0892c1015 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 11 Jun 2024 22:32:32 +0100
Subject: [PATCH 21/35] tests with immutables

---
 src/kontrol/prove.py                          | 137 ++++++++++--------
 .../foundry/test/ContractFieldTest.t.sol      |  29 ++--
 .../test-data/symbolic-bytes-lemmas.k         |  24 +++
 3 files changed, 118 insertions(+), 72 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 3c13893be..f601b6eb8 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -11,7 +11,7 @@
 from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, run_prover
 from pathos.pools import ProcessPool  # type: ignore
 from pyk.cterm import CTerm, CTermSymbolic
-from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
+from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst
 from pyk.kast.manip import flatten_label, set_cell
 from pyk.kcfg import KCFG, KCFGExplore
 from pyk.kore.rpc import KoreClient, TransportType, kore_server
@@ -656,66 +656,81 @@ def _method_to_cfg(
 
 
 def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigType) -> CTerm:
-    new_accounts_cell = node.cterm.cell('ACCOUNTS_CELL')
-    number_cell = node.cterm.cell('NUMBER_CELL')
-    timestamp_cell = node.cterm.cell('TIMESTAMP_CELL')
-    basefee_cell = node.cterm.cell('BASEFEE_CELL')
-    chainid_cell = node.cterm.cell('CHAINID_CELL')
-    coinbase_cell = node.cterm.cell('COINBASE_CELL')
-    prevcaller_cell = node.cterm.cell('PREVCALLER_CELL')
-    prevorigin_cell = node.cterm.cell('PREVORIGIN_CELL')
-    newcaller_cell = node.cterm.cell('NEWCALLER_CELL')
-    neworigin_cell = node.cterm.cell('NEWORIGIN_CELL')
-    active_cell = node.cterm.cell('ACTIVE_CELL')
-    depth_cell = node.cterm.cell('DEPTH_CELL')
-    singlecall_cell = node.cterm.cell('SINGLECALL_CELL')
-    gas_cell = node.cterm.cell('GAS_CELL')
-    callgas_cell = node.cterm.cell('CALLGAS_CELL')
-
-    all_accounts = flatten_label('_AccountCellMap_', new_accounts_cell)
-
-    new_accounts = [CTerm(account, []) for account in all_accounts if (type(account) is KApply and account.is_cell)]
-    non_cell_accounts = [account for account in all_accounts if not (type(account) is KApply and account.is_cell)]
-
-    new_accounts_map = {account.cell('ACCTID_CELL'): account for account in new_accounts}
-
-    if config_type == ConfigType.SUMMARY_CONFIG:
-        for account_id, account in new_accounts_map.items():
-            acct_id_cell = account.cell('ACCTID_CELL')
-            if type(acct_id_cell) is KVariable:
-                acct_id = acct_id_cell.name
-            elif type(acct_id_cell) is KToken:
-                acct_id = acct_id_cell.token
-            else:
-                raise RuntimeError(
-                    f'Failed to abstract storage. acctId cell is neither variable nor token: {acct_id_cell}'
-                )
-            new_accounts_map[account_id] = CTerm(
-                set_cell(
-                    account.config,
-                    'STORAGE_CELL',
-                    KVariable(f'STORAGE_{acct_id}', sort=KSort('Map')),
-                ),
-                [],
-            )
-
-    new_accounts_cell = KEVM.accounts([account.config for account in new_accounts_map.values()] + non_cell_accounts)
-
-    new_init_cterm = CTerm(set_cell(cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NUMBER_CELL', number_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'TIMESTAMP_CELL', timestamp_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'BASEFEE_CELL', basefee_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CHAINID_CELL', chainid_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'COINBASE_CELL', coinbase_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVCALLER_CELL', prevcaller_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVORIGIN_CELL', prevorigin_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWCALLER_CELL', newcaller_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWORIGIN_CELL', neworigin_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACTIVE_CELL', active_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'DEPTH_CELL', depth_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'SINGLECALL_CELL', singlecall_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'GAS_CELL', gas_cell), [])
-    new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CALLGAS_CELL', callgas_cell), [])
+    if config_type == ConfigType.TEST_CONFIG:
+        new_accounts_cell = node.cterm.cell('ACCOUNTS_CELL')
+        number_cell = node.cterm.cell('NUMBER_CELL')
+        timestamp_cell = node.cterm.cell('TIMESTAMP_CELL')
+        basefee_cell = node.cterm.cell('BASEFEE_CELL')
+        chainid_cell = node.cterm.cell('CHAINID_CELL')
+        coinbase_cell = node.cterm.cell('COINBASE_CELL')
+        prevcaller_cell = node.cterm.cell('PREVCALLER_CELL')
+        prevorigin_cell = node.cterm.cell('PREVORIGIN_CELL')
+        newcaller_cell = node.cterm.cell('NEWCALLER_CELL')
+        neworigin_cell = node.cterm.cell('NEWORIGIN_CELL')
+        active_cell = node.cterm.cell('ACTIVE_CELL')
+        depth_cell = node.cterm.cell('DEPTH_CELL')
+        singlecall_cell = node.cterm.cell('SINGLECALL_CELL')
+        gas_cell = node.cterm.cell('GAS_CELL')
+        callgas_cell = node.cterm.cell('CALLGAS_CELL')
+
+        all_accounts = flatten_label('_AccountCellMap_', new_accounts_cell)
+
+        new_accounts = [CTerm(account, []) for account in all_accounts if (type(account) is KApply and account.is_cell)]
+        non_cell_accounts = [account for account in all_accounts if not (type(account) is KApply and account.is_cell)]
+
+        new_accounts_map = {account.cell('ACCTID_CELL'): account for account in new_accounts}
+
+        new_accounts_cell = KEVM.accounts([account.config for account in new_accounts_map.values()] + non_cell_accounts)
+
+        new_init_cterm = CTerm(set_cell(cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NUMBER_CELL', number_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'TIMESTAMP_CELL', timestamp_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'BASEFEE_CELL', basefee_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CHAINID_CELL', chainid_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'COINBASE_CELL', coinbase_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVCALLER_CELL', prevcaller_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVORIGIN_CELL', prevorigin_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWCALLER_CELL', newcaller_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWORIGIN_CELL', neworigin_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACTIVE_CELL', active_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'DEPTH_CELL', depth_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'SINGLECALL_CELL', singlecall_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'GAS_CELL', gas_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CALLGAS_CELL', callgas_cell), [])
+    # config_type == ConfigType.SUMMARY_CONFIG
+    # This means that a function is being run in isolation, that is, that the `node` we are
+    # taking information from has come from a constructor and not a setUp function.
+    # In this case, the <output> cell of the constructor execution becomes the program cell
+    # of the function execution and the constraints from the constructor are propagated.
+    else:
+        new_program_cell = node.cterm.cell('OUTPUT_CELL')
+        accounts_cell = cterm.cell('ACCOUNTS_CELL')
+        contract_id = cterm.cell('ID_CELL')
+
+        all_accounts = flatten_label('_AccountCellMap_', accounts_cell)
+        # TODO: Understand why there are two possible KInner representations or accounts,
+        # one directly with `<acccount>` and the other with `AccountCellMapItem`.
+        cell_accounts = [
+            CTerm(account, []) for account in all_accounts if (type(account) is KApply and account.is_cell)
+        ] + [
+            CTerm(account.args[1], [])
+            for account in all_accounts
+            if (type(account) is KApply and account.label.name == 'AccountCellMapItem')
+        ]
+        other_accounts = [
+            account
+            for account in all_accounts
+            if not (type(account) is KApply and (account.is_cell or account.label.name == 'AccountCellMapItem'))
+        ]
+        cell_accounts_map = {account.cell('ACCTID_CELL'): account for account in cell_accounts}
+        # Set the code of the active contract to the one produced by the constructor
+        contract_account = cell_accounts_map[contract_id]
+        contract_account = CTerm(set_cell(contract_account.config, 'CODE_CELL', new_program_cell), [])
+        cell_accounts_map[contract_id] = contract_account
+        new_accounts_cell = KEVM.accounts([account.config for account in cell_accounts_map.values()] + other_accounts)
+
+        new_init_cterm = CTerm(set_cell(cterm.config, 'PROGRAM_CELL', new_program_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
 
     # Adding constraints from the initial cterm and initial node
     for constraint in cterm.constraints + node.cterm.constraints:
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index b42d5b1a1..f84195b9f 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -2,31 +2,38 @@
 pragma solidity =0.8.13;
 import {Test} from "forge-std/Test.sol";
 
-contract TestToken {
-    uint256 public totalSupply;
+contract TToken {
+    uint128 public immutable baseSupply = 32;
+    uint128 public immutable additionalSupply;
 
-    constructor(uint256 _totalSupply) {
-        totalSupply = _totalSupply;
+    constructor(uint128 _additionalSupply) {
+        additionalSupply = _additionalSupply;
+    }
+
+    function totalSupply() public returns (uint256) {
+      return uint256(baseSupply) + uint256(additionalSupply);
     }
 }
 
-contract Escrow {
-    TestToken token;
+contract TEscrow {
+    TToken token;
 
-    constructor(uint256 _totalSupply) {
-        token = new TestToken(_totalSupply);
+    constructor(address _token) {
+        token = TToken(_token);
     }
 
     function getTokenTotalSupply() public returns (uint256) {
-        return token.totalSupply() + 15;
+        return token.totalSupply() + 23;
     }
 }
 
 contract ContractFieldTest is Test {
-    Escrow escrow;
+    TToken token;
+    TEscrow escrow;
 
     function setUp() public {
-        escrow = new Escrow(12330);
+        token = new TToken(12300);
+        escrow = new TEscrow(address(token));
     }
 
     /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
diff --git a/src/tests/integration/test-data/symbolic-bytes-lemmas.k b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
index 4a39293d9..63cb27802 100644
--- a/src/tests/integration/test-data/symbolic-bytes-lemmas.k
+++ b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
@@ -22,4 +22,28 @@ module SYMBOLIC-BYTES-LEMMAS
       requires lengthBytes(A) <=Int I
       [simplification, preserves-definedness]
 
+    rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B1:Bytes +Bytes B2:Bytes #Equals B } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B:Bytes #Equals #buf( N, X:Int ) +Bytes B2:Bytes } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
+    rule { #buf( N, X:Int ) +Bytes B2:Bytes #Equals B } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
 endmodule
\ No newline at end of file

From 69132aa2e896f8289f0293009a20bac81765b1c4 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 11 Jun 2024 23:45:15 +0100
Subject: [PATCH 22/35] stabilising tests

---
 src/tests/integration/test-data/cse-lemmas.k     | 16 +++++++++++++++-
 .../foundry/test/ContractFieldTest.t.sol         | 13 ++++++-------
 .../test-data/symbolic-bytes-lemmas.k            |  2 +-
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/src/tests/integration/test-data/cse-lemmas.k b/src/tests/integration/test-data/cse-lemmas.k
index 582e052da..86e34442a 100644
--- a/src/tests/integration/test-data/cse-lemmas.k
+++ b/src/tests/integration/test-data/cse-lemmas.k
@@ -31,7 +31,7 @@ module CSE-LEMMAS
       [simplification]
 
     // Function selector does not match
-    rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } => #Bottom
+    rule { B:Bytes #Equals B1:Bytes +Bytes _:Bytes } => #Bottom
       requires #range(B, 0, 4) =/=K #range (B1, 0, 4)
       [simplification(60), concrete(B, B1)]
 
@@ -40,6 +40,20 @@ module CSE-LEMMAS
       requires 4 <=Int lengthBytes(B) andBool #range(B, 0, 4) ==K B1
       [simplification(60), concrete(B, B1)]
 
+    // Bitwise inequalities
+    rule [bitwise-and-maxUInt-lt-l]:
+      A <Int X &Int Y => false
+      requires 0 <=Int X andBool 0 <=Int Y
+       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+       andBool X +Int 1 <=Int A
+       [concrete(X), simplification, preserves-definedness]
+
+    rule [bitwise-and-maxUInt-le-r]:
+      X &Int Y <=Int A => true
+      requires 0 <=Int X andBool 0 <=Int Y
+       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+       andBool X +Int 1 <=Int A
+       [concrete(X), simplification, preserves-definedness]
 
 endmodule
 
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index f84195b9f..685a30a3a 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -3,15 +3,14 @@ pragma solidity =0.8.13;
 import {Test} from "forge-std/Test.sol";
 
 contract TToken {
-    uint128 public immutable baseSupply = 32;
-    uint128 public immutable additionalSupply;
+    uint128 private totalSupply;
 
-    constructor(uint128 _additionalSupply) {
-        additionalSupply = _additionalSupply;
+    constructor(uint128 _totalSupply) {
+        totalSupply = _totalSupply;
     }
 
-    function totalSupply() public returns (uint256) {
-      return uint256(baseSupply) + uint256(additionalSupply);
+    function getTotalSupply() public returns (uint256) {
+      return 32 + uint256(totalSupply);
     }
 }
 
@@ -23,7 +22,7 @@ contract TEscrow {
     }
 
     function getTokenTotalSupply() public returns (uint256) {
-        return token.totalSupply() + 23;
+        return token.getTotalSupply() + 13;
     }
 }
 
diff --git a/src/tests/integration/test-data/symbolic-bytes-lemmas.k b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
index 63cb27802..9ee1dfd90 100644
--- a/src/tests/integration/test-data/symbolic-bytes-lemmas.k
+++ b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
@@ -13,7 +13,7 @@ module SYMBOLIC-BYTES-LEMMAS
       [simplification(40)]
 
     rule [bytes-concat-lookup-left]:
-        (A:Bytes +Bytes B:Bytes) [I] => A [I]
+        (A:Bytes +Bytes _:Bytes) [I] => A [I]
       requires 0 <=Int I andBool I <Int lengthBytes(A)
       [simplification, preserves-definedness]
 

From df4e23c94a9b00d95aff0aa1df3efa904e44f497 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Tue, 11 Jun 2024 23:05:04 +0000
Subject: [PATCH 23/35] Set Version: 0.1.309

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 217f5022a..626c1b0cf 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.308
+0.1.309
diff --git a/pyproject.toml b/pyproject.toml
index b00c261f3..acb0ee8c0 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.308"
+version = "0.1.309"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 515a8a132..8a2f1cf8d 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.308'
+VERSION: Final = '0.1.309'

From 610d6e9fe781210e2af0b182995c95d08e841589 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 12:57:03 +0700
Subject: [PATCH 24/35] Update expected output, remove `Accounts` test

---
 .../test-data/foundry-dependency-all          |   1 -
 .../test-data/foundry/src/cse/Accounts.sol    |  34 --
 .../AddConst.applyOp(uint256).cse.expected    |  18 +-
 ...ctFieldTest.testEscrowToken().cse.expected | 309 ++++++++++++++++++
 ...ImportedContract.add(uint256).cse.expected |  22 +-
 .../ImportedContract.count().cse.expected     |   6 +-
 .../show/ImportedContract.init.cse.expected   |   2 +-
 ...ImportedContract.set(uint256).cse.expected |  18 +-
 .../test-data/show/contracts.k.expected       |  26 +-
 .../test-data/show/foundry.k.expected         |  14 +-
 10 files changed, 362 insertions(+), 88 deletions(-)
 delete mode 100644 src/tests/integration/test-data/foundry/src/cse/Accounts.sol
 create mode 100644 src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected

diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
index c6ecf9343..a9720140c 100644
--- a/src/tests/integration/test-data/foundry-dependency-all
+++ b/src/tests/integration/test-data/foundry-dependency-all
@@ -8,7 +8,6 @@ CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
 ContractFieldTest.testEscrowToken()
-CompositionalAccounts.getEscrowToken()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)
diff --git a/src/tests/integration/test-data/foundry/src/cse/Accounts.sol b/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
deleted file mode 100644
index a36409ede..000000000
--- a/src/tests/integration/test-data/foundry/src/cse/Accounts.sol
+++ /dev/null
@@ -1,34 +0,0 @@
-// SPDX-License-Identifier: UNLICENSED
-pragma solidity =0.8.13;
-import {Test} from "forge-std/Test.sol";
-
-contract CompositionalToken {
-    uint256 public totalSupply;
-
-    constructor(uint256 _totalSupply) {
-        totalSupply = _totalSupply;
-    }
-}
-
-contract CompositionalEscrow {
-    CompositionalToken cseToken;
-
-    constructor(uint256 _totalSupply) {
-        cseToken = new CompositionalToken(_totalSupply);
-    }
-
-    function getTokenTotalSupply() public returns (uint256) {
-        return cseToken.totalSupply() + 15;
-    }
-}
-
-contract CompositionalAccounts {
-    CompositionalEscrow cseEscrow;
-
-    /* Calling `getTokenTotalSupply` will summarize `totalSupply` and
-       include `CompositionalEscrow escrow`and `CompositionalToken token` into the list of accounts in `getEscrowToken`'s summary
-    */
-    function getEscrowToken() public {
-        assert(cseEscrow.getTokenTotalSupply() == 12345);
-    }
-}
\ No newline at end of file
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
index 953b2b42c..703d0b69d 100644
--- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
 ┃  │
 ┃  ├─ 8
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -29,7 +29,7 @@
 ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
-┗━━┓ constraint: ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+┗━━┓ constraint: ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
    │
    ├─ 9
    │   k: #execute ~> CONTINUATION:K
@@ -76,7 +76,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                   ( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                  </output>
                  <statusCode>
                    ( _STATUSCODE => EVMC_SUCCESS )
@@ -98,7 +98,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      ( .WordStack => ( selector ( "applyOp(uint256)" ) : .WordStack ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) )
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -138,7 +138,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -247,7 +247,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) )
+       andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-8-TO-6)]
     
@@ -288,7 +288,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( CONTRACT_STORAGE:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -331,7 +331,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -440,7 +440,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( ( maxUInt256 -Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) <Int VV0_x_114b9705:Int
+       andBool ( ( maxUInt256 -Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
                ))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-9-TO-7)]
 
diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
new file mode 100644
index 000000000..a9e417af4
--- /dev/null
+++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
@@ -0,0 +1,309 @@
+
+┌─ 1 (root, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: 0
+│   statusCode: STATUSCODE:StatusCode
+│
+│  (2219 steps)
+├─ 14 (terminal)
+│   k: #halt ~> CONTINUATION:K
+│   pc: 194
+│   callDepth: 0
+│   statusCode: EVMC_SUCCESS
+│
+┊  constraint: true
+┊  subst: OMITTED SUBST
+└─ 11 (leaf, target, terminal)
+    k: #halt ~> CONTINUATION:K
+    pc: PC_CELL_5d410f2a:Int
+    callDepth: CALLDEPTH_CELL_5d410f2a:Int
+    statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
+
+module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
+    
+    
+    rule [BASIC-BLOCK-1-TO-14]: <foundry>
+           <kevm>
+             <k>
+               ( #execute => #halt )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <touchedAccounts>
+                   ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     ( b"\n\x92T\xe4" => b"51X\xa0" )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( selector ( "testEscrowToken()" ) : .WordStack ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0009" )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     .List
+                   </log>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
+                   </accessedStorage>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       ( 645326474426547203313410069153905908525362434349 => 263400868551549723330807389252719309078400616203 )
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( .Map => ( 0 |-> 491460923342184218035706888008750043977755113263 ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       ( 0 => 1 )
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( ( 11 |-> 1 )
+                       ( 7 |-> 1 ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account> => ( <account>
+                     <acctID>
+                       491460923342184218035706888008750043977755113263
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( 0 |-> 12300 )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                     ...
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     <storage>
+                       ( ( 11 |-> 1 )
+                       ( ( 27 |-> 491460923342184218035706888008750043977755113263 )
+                       ( ( 28 |-> 263400868551549723330807389252719309078400616203 )
+                       ( 7 |-> 1 ) ) ) )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       3
+                     </nonce>
+                     ...
+                   </account> ) ) ) )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int TIMESTAMP_CELL:Int
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( TIMESTAMP_CELL:Int <Int pow256
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+               ))))))))))))
+      [priority(20), label(BASIC-BLOCK-1-TO-14)]
+
+endmodule
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
index 12a63c233..34e532a29 100644
--- a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+┣━━┓ constraint: ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( CONTRACT_STORAGE:Map , 0 )
 ┃  │
 ┃  ├─ 13
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -30,7 +30,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┣━━┓ constraints:
-┃  ┃     #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+┃  ┃     #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
 ┃  ┃     ( notBool STATIC_CELL:Bool )
 ┃  │
 ┃  ├─ 16
@@ -55,7 +55,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┗━━┓ constraints:
-   ┃     #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+   ┃     #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
    ┃     STATIC_CELL:Bool
    │
    ├─ 17
@@ -122,7 +122,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                      CALLVALUE_79cb2bc6:Int
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) : ( VV0_x_114b9705:Int : ( 147 : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( #lookup ( CONTRACT_STORAGE:Map , 0 ) : ( VV0_x_114b9705:Int : ( 147 : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -165,7 +165,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -276,7 +276,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( ( maxUInt256 -Int VV0_x_114b9705:Int ) <Int #lookup ( CONTRACT_STORAGE:Map , 0 )
                ))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-13-TO-7)]
     
@@ -363,7 +363,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( STORAGE_CONTRACT_ID:Map => STORAGE_CONTRACT_ID:Map [ 0 <- ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) +Int VV0_x_114b9705:Int ) ] )
+                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- ( #lookup ( CONTRACT_STORAGE:Map , 0 ) +Int VV0_x_114b9705:Int ) ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -475,7 +475,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
                )))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-16-TO-10)]
     
@@ -513,7 +513,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                      CALLVALUE_79cb2bc6:Int
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 0 : ( ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) +Int VV0_x_114b9705:Int ) : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) )
+                     ( .WordStack => ( 0 : ( ( #lookup ( CONTRACT_STORAGE:Map , 0 ) +Int VV0_x_114b9705:Int ) : ( VV0_x_114b9705:Int : ( 106 : ( selector ( "add(uint256)" ) : .WordStack ) ) ) ) ) )
                    </wordStack>
                    <localMem>
                      ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -559,7 +559,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -671,7 +671,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
                )))))))))))))))))))))))))))
       [priority(20), label(BASIC-BLOCK-17-TO-11)]
 
diff --git a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
index 9b2f99e2d..8cc5321cb 100644
--- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
@@ -44,7 +44,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => #buf ( 32 , #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) )
+                   ( _OUTPUT_CELL => #buf ( 32 , #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
                  </output>
                  <statusCode>
                    ( _STATUSCODE => EVMC_SUCCESS )
@@ -66,7 +66,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
                      ( .WordStack => ( 73 : ( selector ( "count()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) )
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , #lookup ( CONTRACT_STORAGE:Map , 0 ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -106,7 +106,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
index 74c99048d..92a7e19af 100644
--- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
@@ -109,7 +109,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- 5 ] )
+                       ( CONTRACT_STORAGE_ID:Map => CONTRACT_STORAGE_ID:Map [ 0 <- 5 ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
index 5921a35c8..c7beff05c 100644
--- a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 ┃
 ┃ (branch)
-┣━━┓ constraint: #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <Int 3
+┣━━┓ constraint: #lookup ( CONTRACT_STORAGE:Map , 0 ) <Int 3
 ┃  │
 ┃  ├─ 13
 ┃  │   k: #execute ~> CONTINUATION:K
@@ -30,7 +30,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┣━━┓ constraints:
-┃  ┃     3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+┃  ┃     3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
 ┃  ┃     ( notBool STATIC_CELL:Bool )
 ┃  │
 ┃  ├─ 16
@@ -55,7 +55,7 @@
 ┃      statusCode: STATUSCODE_FINAL:StatusCode
 ┃
 ┗━━┓ constraints:
-   ┃     3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+   ┃     3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
    ┃     STATIC_CELL:Bool
    │
    ├─ 17
@@ -165,7 +165,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -271,7 +271,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) <Int 3
+       andBool ( #lookup ( CONTRACT_STORAGE:Map , 0 ) <Int 3
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
@@ -361,7 +361,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( STORAGE_CONTRACT_ID:Map => STORAGE_CONTRACT_ID:Map [ 0 <- VV0_x_114b9705:Int ] )
+                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- VV0_x_114b9705:Int ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -468,7 +468,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( 3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( 3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
@@ -555,7 +555,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       STORAGE_CONTRACT_ID:Map
+                       CONTRACT_STORAGE:Map
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
@@ -662,7 +662,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0
        andBool ( ( notBool <acctID>
           CONTRACT_ID:Int
         </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
-       andBool ( 3 <=Int #lookup ( STORAGE_CONTRACT_ID:Map , 0 )
+       andBool ( 3 <=Int #lookup ( CONTRACT_STORAGE:Map , 0 )
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index f39630875..24256b486 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -3017,18 +3017,18 @@ module S2KtestZModContractFieldTest-CONTRACT
 
 endmodule
 
-module S2KtestZModEscrow-CONTRACT
+module S2KtestZModTEscrow-CONTRACT
     imports public FOUNDRY
     
-    syntax Contract ::= S2KtestZModEscrowContract
+    syntax Contract ::= S2KtestZModTEscrowContract
     
-    syntax S2KtestZModEscrowContract ::= "S2KtestZModEscrow" [symbol(""), klabel(contract_test%Escrow)]
+    syntax S2KtestZModTEscrowContract ::= "S2KtestZModTEscrow" [symbol(""), klabel(contract_test%TEscrow)]
     
-    syntax Bytes ::= S2KtestZModEscrowContract "." S2KtestZModEscrowMethod [function, symbol(""), klabel(method_test%Escrow)]
+    syntax Bytes ::= S2KtestZModTEscrowContract "." S2KtestZModTEscrowMethod [function, symbol(""), klabel(method_test%TEscrow)]
     
-    syntax S2KtestZModEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%Escrow_S2KgetTokenTotalSupply_)]
+    syntax S2KtestZModTEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%TEscrow_S2KgetTokenTotalSupply_)]
     
-    rule  ( S2KtestZModEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
+    rule  ( S2KtestZModTEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
       
     
     rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
@@ -3036,21 +3036,21 @@ module S2KtestZModEscrow-CONTRACT
 
 endmodule
 
-module S2KtestZModTestToken-CONTRACT
+module S2KtestZModTToken-CONTRACT
     imports public FOUNDRY
     
-    syntax Contract ::= S2KtestZModTestTokenContract
+    syntax Contract ::= S2KtestZModTTokenContract
     
-    syntax S2KtestZModTestTokenContract ::= "S2KtestZModTestToken" [symbol(""), klabel(contract_test%TestToken)]
+    syntax S2KtestZModTTokenContract ::= "S2KtestZModTToken" [symbol(""), klabel(contract_test%TToken)]
     
-    syntax Bytes ::= S2KtestZModTestTokenContract "." S2KtestZModTestTokenMethod [function, symbol(""), klabel(method_test%TestToken)]
+    syntax Bytes ::= S2KtestZModTTokenContract "." S2KtestZModTTokenMethod [function, symbol(""), klabel(method_test%TToken)]
     
-    syntax S2KtestZModTestTokenMethod ::= "S2KtotalSupply" "(" ")" [symbol(""), klabel(method_test%TestToken_S2KtotalSupply_)]
+    syntax S2KtestZModTTokenMethod ::= "S2KgetTotalSupply" "(" ")" [symbol(""), klabel(method_test%TToken_S2KgetTotalSupply_)]
     
-    rule  ( S2KtestZModTestToken . S2KtotalSupply ( ) => #abiCallData ( "totalSupply" , .TypedArgs ) )
+    rule  ( S2KtestZModTToken . S2KgetTotalSupply ( ) => #abiCallData ( "getTotalSupply" , .TypedArgs ) )
       
     
-    rule  ( selector ( "totalSupply()" ) => 404098525 )
+    rule  ( selector ( "getTotalSupply()" ) => 3303283490 )
       
 
 endmodule
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 5b61734a2..ec930ba13 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -40,8 +40,8 @@ module FOUNDRY-MAIN
     imports public S2KtestZModContractTest-VERIFICATION
     imports public S2KtestZModContractBTest-VERIFICATION
     imports public S2KtestZModContractFieldTest-VERIFICATION
-    imports public S2KtestZModEscrow-VERIFICATION
-    imports public S2KtestZModTestToken-VERIFICATION
+    imports public S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTToken-VERIFICATION
     imports public S2KtestZModCounter-VERIFICATION
     imports public S2KtestZModCounterTest-VERIFICATION
     imports public S2KsrcZModDeploymentState-VERIFICATION
@@ -143,7 +143,7 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole2-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
-    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION    
+    imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
 
 
 
@@ -396,15 +396,15 @@ module S2KtestZModContractFieldTest-VERIFICATION
 
 endmodule
 
-module S2KtestZModEscrow-VERIFICATION
-    imports public S2KtestZModEscrow-CONTRACT
+module S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTEscrow-CONTRACT
     
     
 
 endmodule
 
-module S2KtestZModTestToken-VERIFICATION
-    imports public S2KtestZModTestToken-CONTRACT
+module S2KtestZModTToken-VERIFICATION
+    imports public S2KtestZModTToken-CONTRACT
     
     
 

From 112a3fb2a733e3ec177ddb84615bc73e9e36a95c Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 13:07:25 +0700
Subject: [PATCH 25/35] Update `contracts.k` expected output to reflect removal
 of `Accounts`

---
 .../test-data/show/contracts.k.expected       | 57 -------------------
 .../test-data/show/foundry.k.expected         | 24 --------
 2 files changed, 81 deletions(-)

diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index 24256b486..8d7af1bf0 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -227,63 +227,6 @@ module S2KtestZModAccountParamsTest-CONTRACT
     rule  ( selector ( "test_getNonce_unknownSymbolic(address)" ) => 3941547284 )
       
 
-endmodule
-
-module S2KsrcZModcseZModCompositionalAccounts-CONTRACT
-    imports public FOUNDRY
-    
-    syntax Contract ::= S2KsrcZModcseZModCompositionalAccountsContract
-    
-    syntax S2KsrcZModcseZModCompositionalAccountsContract ::= "S2KsrcZModcseZModCompositionalAccounts" [symbol(""), klabel(contract_src%cse%CompositionalAccounts)]
-    
-    syntax Bytes ::= S2KsrcZModcseZModCompositionalAccountsContract "." S2KsrcZModcseZModCompositionalAccountsMethod [function, symbol(""), klabel(method_src%cse%CompositionalAccounts)]
-    
-    syntax S2KsrcZModcseZModCompositionalAccountsMethod ::= "S2KgetEscrowToken" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalAccounts_S2KgetEscrowToken_)]
-    
-    rule  ( S2KsrcZModcseZModCompositionalAccounts . S2KgetEscrowToken ( ) => #abiCallData ( "getEscrowToken" , .TypedArgs ) )
-      
-    
-    rule  ( selector ( "getEscrowToken()" ) => 1851159305 )
-      
-
-endmodule
-
-module S2KsrcZModcseZModCompositionalEscrow-CONTRACT
-    imports public FOUNDRY
-    
-    syntax Contract ::= S2KsrcZModcseZModCompositionalEscrowContract
-    
-    syntax S2KsrcZModcseZModCompositionalEscrowContract ::= "S2KsrcZModcseZModCompositionalEscrow" [symbol(""), klabel(contract_src%cse%CompositionalEscrow)]
-    
-    syntax Bytes ::= S2KsrcZModcseZModCompositionalEscrowContract "." S2KsrcZModcseZModCompositionalEscrowMethod [function, symbol(""), klabel(method_src%cse%CompositionalEscrow)]
-    
-    syntax S2KsrcZModcseZModCompositionalEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalEscrow_S2KgetTokenTotalSupply_)]
-    
-    rule  ( S2KsrcZModcseZModCompositionalEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) )
-      
-    
-    rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
-      
-
-endmodule
-
-module S2KsrcZModcseZModCompositionalToken-CONTRACT
-    imports public FOUNDRY
-    
-    syntax Contract ::= S2KsrcZModcseZModCompositionalTokenContract
-    
-    syntax S2KsrcZModcseZModCompositionalTokenContract ::= "S2KsrcZModcseZModCompositionalToken" [symbol(""), klabel(contract_src%cse%CompositionalToken)]
-    
-    syntax Bytes ::= S2KsrcZModcseZModCompositionalTokenContract "." S2KsrcZModcseZModCompositionalTokenMethod [function, symbol(""), klabel(method_src%cse%CompositionalToken)]
-    
-    syntax S2KsrcZModcseZModCompositionalTokenMethod ::= "S2KtotalSupply" "(" ")" [symbol(""), klabel(method_src%cse%CompositionalToken_S2KtotalSupply_)]
-    
-    rule  ( S2KsrcZModcseZModCompositionalToken . S2KtotalSupply ( ) => #abiCallData ( "totalSupply" , .TypedArgs ) )
-      
-    
-    rule  ( selector ( "totalSupply()" ) => 404098525 )
-      
-
 endmodule
 
 module S2KtestZModAddrTest-CONTRACT
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index ec930ba13..5fdcf5181 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -8,9 +8,6 @@ module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION
     imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
     imports public S2KtestZModAccountParamsTest-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalAccounts-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalEscrow-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalToken-VERIFICATION
     imports public S2KtestZModAddrTest-VERIFICATION
     imports public S2KtestZModAllowChangesTest-VERIFICATION
     imports public S2KtestZModValueStore-VERIFICATION
@@ -168,27 +165,6 @@ module S2KtestZModAccountParamsTest-VERIFICATION
     
     
 
-endmodule
-
-module S2KsrcZModcseZModCompositionalAccounts-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalAccounts-CONTRACT
-    
-    
-
-endmodule
-
-module S2KsrcZModcseZModCompositionalEscrow-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalEscrow-CONTRACT
-    
-    
-
-endmodule
-
-module S2KsrcZModcseZModCompositionalToken-VERIFICATION
-    imports public S2KsrcZModcseZModCompositionalToken-CONTRACT
-    
-    
-
 endmodule
 
 module S2KtestZModAddrTest-VERIFICATION

From a630375abbceb255327d202be04c3127b5119ecf Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Wed, 12 Jun 2024 06:53:27 +0000
Subject: [PATCH 26/35] Set Version: 0.1.310

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 626c1b0cf..7933c2399 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.309
+0.1.310
diff --git a/pyproject.toml b/pyproject.toml
index 1ccfac127..1605e824e 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.309"
+version = "0.1.310"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 8a2f1cf8d..0f37b9ce0 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.309'
+VERSION: Final = '0.1.310'

From b3e9746c26e2a4542c651fa8684871f5e8c0dc33 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 14:11:25 +0700
Subject: [PATCH 27/35] Use default symbolic storage var name for constructor
 storage with CSE

---
 src/kontrol/prove.py                                          | 3 +--
 .../test-data/show/ImportedContract.init.cse.expected         | 2 +-
 src/tests/integration/test-data/show/foundry.k.expected       | 4 ++--
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index cfb31e84a..c12480475 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -872,8 +872,7 @@ def _init_cterm(
 
         if isinstance(method, Contract.Constructor):
             # Symbolic account for the contract being executed
-            storage_map = KVariable(Foundry.symbolic_contract_prefix() + '_STORAGE_ID', sort=KSort('Map'))
-            accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code, storage_map))
+            accounts.append(Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code))
         else:
             # Symbolic accounts of all relevant contracts
             accounts, storage_constraints = _create_cse_accounts(
diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
index 92a7e19af..74c99048d 100644
--- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
@@ -109,7 +109,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0
                        CONTRACT_BAL:Int
                      </balance>
                      <storage>
-                       ( CONTRACT_STORAGE_ID:Map => CONTRACT_STORAGE_ID:Map [ 0 <- 5 ] )
+                       ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- 5 ] )
                      </storage>
                      <nonce>
                        CONTRACT_NONCE:Int
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 5fdcf5181..f4f9de4e5 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -141,8 +141,8 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole2-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
-
-
+    
+    
 
 endmodule
 

From 86d5bf2051092d6c5360ca65f5d83a1e090b7f3c Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 14:17:12 +0700
Subject: [PATCH 28/35] Documented `_create_cse_accounts`

---
 src/kontrol/prove.py | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index c12480475..ab0600b33 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -957,6 +957,19 @@ def _create_initial_account_list(
 def _create_cse_accounts(
     foundry: Foundry, storage_fields: tuple[StorageField, ...], contract_name: str, contract_code: KInner
 ) -> tuple[list[KInner], list[KApply]]:
+    """
+    Recursively generates a list of new accounts corresponding to `contract` fields, each having <code> and <storage> cell (partially) set up.
+    Args:
+        foundry (Foundry): The Foundry object containing the information about contracts in the project.
+        storage_fields (tuple[StorageField, ...]): A tuple of StorageField objects representing the contract's storage fields.
+        contract_name (str): The name of the contract being executed to be used in the account-related symbolic variables.
+        contract_code (KInner): The KInner object representing the contract's runtime bytecode.
+    Returns:
+        tuple[list[KInner], list[KApply]]:
+            - A list of accounts to be included in the initial configuration.
+            - A list of constraints on symbolic account IDs.
+    """
+
     new_accounts: list[KInner] = []
     new_account_constraints: list[KApply] = []
 

From ef0acc3f61f2139cdae3b898f088c70f32486181 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 15:31:42 +0700
Subject: [PATCH 29/35] One other output update

---
 .../show/ContractFieldTest.testEscrowToken().cse.expected | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
index a9e417af4..6ebeed102 100644
--- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
+++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
@@ -6,7 +6,7 @@
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (2219 steps)
-├─ 14 (terminal)
+├─ 8 (terminal)
 │   k: #halt ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
@@ -14,7 +14,7 @@
 │
 ┊  constraint: true
 ┊  subst: OMITTED SUBST
-└─ 11 (leaf, target, terminal)
+└─ 7 (leaf, target, terminal)
     k: #halt ~> CONTINUATION:K
     pc: PC_CELL_5d410f2a:Int
     callDepth: CALLDEPTH_CELL_5d410f2a:Int
@@ -26,7 +26,7 @@
 module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
     
     
-    rule [BASIC-BLOCK-1-TO-14]: <foundry>
+    rule [BASIC-BLOCK-1-TO-8]: <foundry>
            <kevm>
              <k>
                ( #execute => #halt )
@@ -304,6 +304,6 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                ))))))))))))
-      [priority(20), label(BASIC-BLOCK-1-TO-14)]
+      [priority(20), label(BASIC-BLOCK-1-TO-8)]
 
 endmodule
\ No newline at end of file

From c8ad9346e9fd8151e892d0afa17efeeb3aa4075f Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Wed, 12 Jun 2024 08:32:21 +0000
Subject: [PATCH 30/35] Set Version: 0.1.311

---
 package/version         | 2 +-
 pyproject.toml          | 2 +-
 src/kontrol/__init__.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/package/version b/package/version
index 7933c2399..1ae2cbabd 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.310
+0.1.311
diff --git a/pyproject.toml b/pyproject.toml
index 16d70071e..3f92cae27 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.310"
+version = "0.1.311"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 0f37b9ce0..de6948f4a 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.310'
+VERSION: Final = '0.1.311'

From 78f2894be3cb601b58b7547a2b0ae5cd57bdc925 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 17:37:19 +0700
Subject: [PATCH 31/35] Apply refactoring from review comments

---
 src/kontrol/prove.py | 59 ++++++++++++++------------------------------
 1 file changed, 19 insertions(+), 40 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index ab0600b33..eef542e5b 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -658,46 +658,25 @@ def _method_to_cfg(
 
 def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigType) -> CTerm:
     if config_type == ConfigType.TEST_CONFIG:
-        new_accounts_cell = node.cterm.cell('ACCOUNTS_CELL')
-        number_cell = node.cterm.cell('NUMBER_CELL')
-        timestamp_cell = node.cterm.cell('TIMESTAMP_CELL')
-        basefee_cell = node.cterm.cell('BASEFEE_CELL')
-        chainid_cell = node.cterm.cell('CHAINID_CELL')
-        coinbase_cell = node.cterm.cell('COINBASE_CELL')
-        prevcaller_cell = node.cterm.cell('PREVCALLER_CELL')
-        prevorigin_cell = node.cterm.cell('PREVORIGIN_CELL')
-        newcaller_cell = node.cterm.cell('NEWCALLER_CELL')
-        neworigin_cell = node.cterm.cell('NEWORIGIN_CELL')
-        active_cell = node.cterm.cell('ACTIVE_CELL')
-        depth_cell = node.cterm.cell('DEPTH_CELL')
-        singlecall_cell = node.cterm.cell('SINGLECALL_CELL')
-        gas_cell = node.cterm.cell('GAS_CELL')
-        callgas_cell = node.cterm.cell('CALLGAS_CELL')
-
-        all_accounts = flatten_label('_AccountCellMap_', new_accounts_cell)
+        cell_names = [
+            'ACCOUNTS_CELL', 'NUMBER_CELL', 'TIMESTAMP_CELL', 'BASEFEE_CELL', 
+            'CHAINID_CELL', 'COINBASE_CELL', 'PREVCALLER_CELL', 'PREVORIGIN_CELL',
+            'NEWCALLER_CELL', 'NEWORIGIN_CELL', 'ACTIVE_CELL', 'DEPTH_CELL', 
+            'SINGLECALL_CELL', 'GAS_CELL', 'CALLGAS_CELL'
+        ]
+        
+        cells = {name: node.cterm.cell(name) for name in cell_names}
+        all_accounts = flatten_label('_AccountCellMap_', cells['ACCOUNTS_CELL'])
 
         new_accounts = [CTerm(account, []) for account in all_accounts if (type(account) is KApply and account.is_cell)]
         non_cell_accounts = [account for account in all_accounts if not (type(account) is KApply and account.is_cell)]
 
         new_accounts_map = {account.cell('ACCTID_CELL'): account for account in new_accounts}
 
-        new_accounts_cell = KEVM.accounts([account.config for account in new_accounts_map.values()] + non_cell_accounts)
-
-        new_init_cterm = CTerm(set_cell(cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NUMBER_CELL', number_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'TIMESTAMP_CELL', timestamp_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'BASEFEE_CELL', basefee_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CHAINID_CELL', chainid_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'COINBASE_CELL', coinbase_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVCALLER_CELL', prevcaller_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'PREVORIGIN_CELL', prevorigin_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWCALLER_CELL', newcaller_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'NEWORIGIN_CELL', neworigin_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACTIVE_CELL', active_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'DEPTH_CELL', depth_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'SINGLECALL_CELL', singlecall_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'GAS_CELL', gas_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CALLGAS_CELL', callgas_cell), [])
+        cells['ACCOUNTS_CELL'] = KEVM.accounts([account.config for account in new_accounts_map.values()] + non_cell_accounts)
+
+        for cell_name, cell_value in cells.items():
+            cterm = CTerm(set_cell(cterm.config, cell_name, cell_value), [])
     # config_type == ConfigType.SUMMARY_CONFIG
     # This means that a function is being run in isolation, that is, that the `node` we are
     # taking information from has come from a constructor and not a setUp function.
@@ -730,17 +709,17 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigTy
         cell_accounts_map[contract_id] = contract_account
         new_accounts_cell = KEVM.accounts([account.config for account in cell_accounts_map.values()] + other_accounts)
 
-        new_init_cterm = CTerm(set_cell(cterm.config, 'PROGRAM_CELL', new_program_cell), [])
-        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
+        cterm = CTerm(set_cell(cterm.config, 'PROGRAM_CELL', new_program_cell), [])
+        cterm = CTerm(set_cell(cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
 
     # Adding constraints from the initial cterm and initial node
     for constraint in cterm.constraints + node.cterm.constraints:
-        new_init_cterm = new_init_cterm.add_constraint(constraint)
-    new_init_cterm = KEVM.add_invariant(new_init_cterm)
+        cterm = cterm.add_constraint(constraint)
+    cterm = KEVM.add_invariant(cterm)
 
-    new_init_cterm = new_init_cterm.remove_useless_constraints()
+    cterm = cterm.remove_useless_constraints()
 
-    return new_init_cterm
+    return cterm
 
 
 def deployment_state_to_account_cells(deployment_state_entries: Iterable[DeploymentStateEntry]) -> list[KApply]:

From 16cd4e54e0685a4501ce44d113cf5745dd813e60 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 18:29:16 +0700
Subject: [PATCH 32/35] Apply refactoring from review comments, preserve
 `new_init_cterm`

---
 src/kontrol/prove.py | 39 +++++++++++++++++++++++++++------------
 1 file changed, 27 insertions(+), 12 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index eef542e5b..046cba8c6 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -659,12 +659,23 @@ def _method_to_cfg(
 def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigType) -> CTerm:
     if config_type == ConfigType.TEST_CONFIG:
         cell_names = [
-            'ACCOUNTS_CELL', 'NUMBER_CELL', 'TIMESTAMP_CELL', 'BASEFEE_CELL', 
-            'CHAINID_CELL', 'COINBASE_CELL', 'PREVCALLER_CELL', 'PREVORIGIN_CELL',
-            'NEWCALLER_CELL', 'NEWORIGIN_CELL', 'ACTIVE_CELL', 'DEPTH_CELL', 
-            'SINGLECALL_CELL', 'GAS_CELL', 'CALLGAS_CELL'
+            'ACCOUNTS_CELL',
+            'NUMBER_CELL',
+            'TIMESTAMP_CELL',
+            'BASEFEE_CELL',
+            'CHAINID_CELL',
+            'COINBASE_CELL',
+            'PREVCALLER_CELL',
+            'PREVORIGIN_CELL',
+            'NEWCALLER_CELL',
+            'NEWORIGIN_CELL',
+            'ACTIVE_CELL',
+            'DEPTH_CELL',
+            'SINGLECALL_CELL',
+            'GAS_CELL',
+            'CALLGAS_CELL',
         ]
-        
+
         cells = {name: node.cterm.cell(name) for name in cell_names}
         all_accounts = flatten_label('_AccountCellMap_', cells['ACCOUNTS_CELL'])
 
@@ -673,10 +684,14 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigTy
 
         new_accounts_map = {account.cell('ACCTID_CELL'): account for account in new_accounts}
 
-        cells['ACCOUNTS_CELL'] = KEVM.accounts([account.config for account in new_accounts_map.values()] + non_cell_accounts)
+        cells['ACCOUNTS_CELL'] = KEVM.accounts(
+            [account.config for account in new_accounts_map.values()] + non_cell_accounts
+        )
 
         for cell_name, cell_value in cells.items():
             cterm = CTerm(set_cell(cterm.config, cell_name, cell_value), [])
+
+        new_init_cterm = cterm
     # config_type == ConfigType.SUMMARY_CONFIG
     # This means that a function is being run in isolation, that is, that the `node` we are
     # taking information from has come from a constructor and not a setUp function.
@@ -709,17 +724,17 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigTy
         cell_accounts_map[contract_id] = contract_account
         new_accounts_cell = KEVM.accounts([account.config for account in cell_accounts_map.values()] + other_accounts)
 
-        cterm = CTerm(set_cell(cterm.config, 'PROGRAM_CELL', new_program_cell), [])
-        cterm = CTerm(set_cell(cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
+        new_init_cterm = CTerm(set_cell(cterm.config, 'PROGRAM_CELL', new_program_cell), [])
+        new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'ACCOUNTS_CELL', new_accounts_cell), [])
 
     # Adding constraints from the initial cterm and initial node
     for constraint in cterm.constraints + node.cterm.constraints:
-        cterm = cterm.add_constraint(constraint)
-    cterm = KEVM.add_invariant(cterm)
+        new_init_cterm = new_init_cterm.add_constraint(constraint)
+    new_init_cterm = KEVM.add_invariant(new_init_cterm)
 
-    cterm = cterm.remove_useless_constraints()
+    new_init_cterm = new_init_cterm.remove_useless_constraints()
 
-    return cterm
+    return new_init_cterm
 
 
 def deployment_state_to_account_cells(deployment_state_entries: Iterable[DeploymentStateEntry]) -> list[KApply]:

From 78d538dc4f003f146c0ef3288b9b87ef391df486 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 18:35:49 +0700
Subject: [PATCH 33/35] Add test for recursive storage generation in new
 accounts

---
 .../test-data/foundry-dependency-all          |   1 +
 .../foundry/test/ContractFieldTest.t.sol      |  12 +
 ...e.getEscrowTokenTotalSupply().cse.expected | 843 ++++++++++++++++++
 3 files changed, 856 insertions(+)
 create mode 100644 src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected

diff --git a/src/tests/integration/test-data/foundry-dependency-all b/src/tests/integration/test-data/foundry-dependency-all
index a9720140c..5ec64edc3 100644
--- a/src/tests/integration/test-data/foundry-dependency-all
+++ b/src/tests/integration/test-data/foundry-dependency-all
@@ -8,6 +8,7 @@ CSETest.test_add_const(uint256,uint256)
 CSETest.test_identity(uint256,uint256)
 ConstructorTest.test_contract_call()
 ContractFieldTest.testEscrowToken()
+TGovernance.getEscrowTokenTotalSupply()
 Identity.applyOp(uint256)
 Identity.identity(uint256)
 ImportedContract.set(uint256)
diff --git a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
index 685a30a3a..f5ebfa692 100644
--- a/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol
@@ -26,6 +26,18 @@ contract TEscrow {
     }
 }
 
+contract TGovernance {
+    TEscrow escrow;
+
+    constructor(address _escrow) {
+        escrow = TEscrow(_escrow);
+    }
+
+    function getEscrowTokenTotalSupply() public returns (uint256) {
+        return escrow.getTokenTotalSupply();
+    }
+}
+
 contract ContractFieldTest is Test {
     TToken token;
     TEscrow escrow;
diff --git a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
new file mode 100644
index 000000000..a4a6eab5b
--- /dev/null
+++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
@@ -0,0 +1,843 @@
+
+┌─ 1 (root, split, init)
+│   k: #execute ~> CONTINUATION:K
+│   pc: 0
+│   callDepth: CALLDEPTH_CELL:Int
+│   statusCode: STATUSCODE:StatusCode
+┃
+┃ (branch)
+┣━━┓ constraint: 1024 <=Int CALLDEPTH_CELL:Int
+┃  │
+┃  ├─ 13
+┃  │   k: #execute ~> CONTINUATION:K
+┃  │   pc: 0
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: STATUSCODE:StatusCode
+┃  │
+┃  │  (376 steps)
+┃  ├─ 7 (terminal)
+┃  │   k: #halt ~> CONTINUATION:K
+┃  │   pc: 153
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: EVMC_REVERT
+┃  │
+┃  ┊  constraint: OMITTED CONSTRAINT
+┃  ┊  subst: OMITTED SUBST
+┃  └─ 2 (leaf, target, terminal)
+┃      k: #halt ~> CONTINUATION:K
+┃      pc: PC_CELL_5d410f2a:Int
+┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
+┃      statusCode: STATUSCODE_FINAL:StatusCode
+┃
+┣━━┓ constraints:
+┃  ┃     CALLDEPTH_CELL:Int <Int 1024
+┃  ┃     CALLDEPTH_CELL:Int <Int 1023
+┃  │
+┃  ├─ 16
+┃  │   k: #execute ~> CONTINUATION:K
+┃  │   pc: 0
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: STATUSCODE:StatusCode
+┃  │
+┃  │  (638 steps)
+┃  ├─ 10 (terminal)
+┃  │   k: #halt ~> CONTINUATION:K
+┃  │   pc: 68
+┃  │   callDepth: CALLDEPTH_CELL:Int
+┃  │   statusCode: EVMC_SUCCESS
+┃  │
+┃  ┊  constraint: OMITTED CONSTRAINT
+┃  ┊  subst: OMITTED SUBST
+┃  └─ 2 (leaf, target, terminal)
+┃      k: #halt ~> CONTINUATION:K
+┃      pc: PC_CELL_5d410f2a:Int
+┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
+┃      statusCode: STATUSCODE_FINAL:StatusCode
+┃
+┗━━┓ constraints:
+   ┃     CALLDEPTH_CELL:Int <Int 1024
+   ┃     1023 <=Int CALLDEPTH_CELL:Int
+   │
+   ├─ 17
+   │   k: #execute ~> CONTINUATION:K
+   │   pc: 0
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: STATUSCODE:StatusCode
+   │
+   │  (389 steps)
+   ├─ 11 (terminal)
+   │   k: #halt ~> CONTINUATION:K
+   │   pc: 153
+   │   callDepth: CALLDEPTH_CELL:Int
+   │   statusCode: EVMC_REVERT
+   │
+   ┊  constraint: OMITTED CONSTRAINT
+   ┊  subst: OMITTED SUBST
+   └─ 2 (leaf, target, terminal)
+       k: #halt ~> CONTINUATION:K
+       pc: PC_CELL_5d410f2a:Int
+       callDepth: CALLDEPTH_CELL_5d410f2a:Int
+       statusCode: STATUSCODE_FINAL:StatusCode
+
+
+
+
+module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0
+    
+    
+    rule [BASIC-BLOCK-13-TO-7]: <foundry>
+           <kevm>
+             <k>
+               ( #execute => #halt )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   ( _OUTPUT_CELL => b"" )
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_REVERT )
+                 </statusCode>
+                 <callState>
+                   <id>
+                     CONTRACT_ID:Int
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"z\xdb@\x8d"
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( 1 : ( 132 : ( selector ( "getTokenTotalSupply()" ) : ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) : ( 0 : ( 51 : ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) ) ) ) ) ) ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00W\xdf\x84K\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <callDepth>
+                     CALLDEPTH_CELL:Int
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( ACCESSEDACCOUNTS_CELL:Set => ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
+                   </accessedAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-TOKEN_BAL:Int
+                     </balance>
+                     <nonce>
+                       CONTRACT-TOKEN_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-ESCROW_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT-ESCROW_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT-ESCROW_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       CONTRACT_ID:Int
+                     </acctID>
+                     <balance>
+                       CONTRACT_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ACCOUNTS_REST:AccountCellMap ) ) )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( 0 <=Int CONTRACT_ID:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int CONTRACT_BAL:Int
+       andBool ( 0 <=Int CONTRACT_NONCE:Int
+       andBool ( 0 <=Int TIMESTAMP_CELL:Int
+       andBool ( 1024 <=Int CALLDEPTH_CELL:Int
+       andBool ( 0 <=Int CONTRACT-TOKEN_BAL:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_BAL:Int
+       andBool ( 0 <=Int CONTRACT-TOKEN_NONCE:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_NONCE:Int
+       andBool ( CONTRACT_NONCE:Int <Int maxUInt64
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CONTRACT-TOKEN_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT-ESCROW_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( CONTRACT_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( CONTRACT_BAL:Int <Int pow256
+       andBool ( TIMESTAMP_CELL:Int <Int pow256
+       andBool ( CONTRACT-TOKEN_BAL:Int <Int pow256
+       andBool ( CONTRACT-ESCROW_BAL:Int <Int pow256
+       andBool ( ( notBool <acctID>
+          CONTRACT_ID:Int
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( _CONTRACT-ESCROW_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( _CONTRACT-TOKEN_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=K ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) <= 9 ) )
+               )))))))))))))))))))))))))))))))))))))))))
+       ensures ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+      [priority(20), label(BASIC-BLOCK-13-TO-7)]
+    
+    rule [BASIC-BLOCK-16-TO-10]: <foundry>
+           <kevm>
+             <k>
+               ( #execute => #halt )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   ( _OUTPUT_CELL => #buf ( 32 , ( ( maxUInt128 &Int #lookup ( CONTRACT-TOKEN_STORAGE:Map , 0 ) ) +Int 45 ) ) )
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
+                 <touchedAccounts>
+                   ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( CONTRACT_ID:Int ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) ) )
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     CONTRACT_ID:Int
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"z\xdb@\x8d"
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( maxUInt128 &Int #lookup ( CONTRACT-TOKEN_STORAGE:Map , 0 ) ) +Int 45 ) ) +Bytes #buf ( 32 , ( ( maxUInt128 &Int #lookup ( CONTRACT-TOKEN_STORAGE:Map , 0 ) ) +Int 45 ) ) )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <callDepth>
+                     CALLDEPTH_CELL:Int
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( ACCESSEDACCOUNTS_CELL:Set => ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) |Set SetItem ( CONTRACT_ID:Int ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
+                   </accessedAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-TOKEN_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT-TOKEN_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT-TOKEN_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-ESCROW_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT-ESCROW_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT-ESCROW_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       CONTRACT_ID:Int
+                     </acctID>
+                     <balance>
+                       CONTRACT_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ACCOUNTS_REST:AccountCellMap ) ) )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( 0 <=Int CONTRACT_ID:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int CONTRACT_BAL:Int
+       andBool ( 0 <=Int CONTRACT_NONCE:Int
+       andBool ( 0 <=Int TIMESTAMP_CELL:Int
+       andBool ( CALLDEPTH_CELL:Int <Int 1023
+       andBool ( CALLDEPTH_CELL:Int <Int 1024
+       andBool ( 0 <=Int CONTRACT-TOKEN_BAL:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_BAL:Int
+       andBool ( 0 <=Int CONTRACT-TOKEN_NONCE:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_NONCE:Int
+       andBool ( CONTRACT_NONCE:Int <Int maxUInt64
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CONTRACT-TOKEN_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT-ESCROW_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( CONTRACT_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( CONTRACT_BAL:Int <Int pow256
+       andBool ( TIMESTAMP_CELL:Int <Int pow256
+       andBool ( CONTRACT-TOKEN_BAL:Int <Int pow256
+       andBool ( CONTRACT-ESCROW_BAL:Int <Int pow256
+       andBool ( ( notBool <acctID>
+          CONTRACT_ID:Int
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( _CONTRACT-ESCROW_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( _CONTRACT-TOKEN_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=K ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) <= 9 ) )
+               ))))))))))))))))))))))))))))))))))))))))))
+       ensures ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+      [priority(20), label(BASIC-BLOCK-16-TO-10)]
+    
+    rule [BASIC-BLOCK-17-TO-11]: <foundry>
+           <kevm>
+             <k>
+               ( #execute => #halt )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   ( _OUTPUT_CELL => b"" )
+                 </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_REVERT )
+                 </statusCode>
+                 <touchedAccounts>
+                   ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( CONTRACT_ID:Int ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
+                 </touchedAccounts>
+                 <callState>
+                   <id>
+                     CONTRACT_ID:Int
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"z\xdb@\x8d"
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( .WordStack => ( 1 : ( 132 : ( selector ( "getTokenTotalSupply()" ) : ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) : ( 0 : ( 51 : ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) ) ) ) ) ) ) )
+                   </wordStack>
+                   <localMem>
+                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00W\xdf\x84K\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                   </localMem>
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
+                   <callDepth>
+                     CALLDEPTH_CELL:Int
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <refund>
+                     0
+                   </refund>
+                   <accessedAccounts>
+                     ( ACCESSEDACCOUNTS_CELL:Set => ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) )
+                   </accessedAccounts>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   <timestamp>
+                     TIMESTAMP_CELL:Int
+                   </timestamp>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-TOKEN_BAL:Int
+                     </balance>
+                     <nonce>
+                       CONTRACT-TOKEN_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+                     </acctID>
+                     <balance>
+                       CONTRACT-ESCROW_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT-ESCROW_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT-ESCROW_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ( <account>
+                     <acctID>
+                       CONTRACT_ID:Int
+                     </acctID>
+                     <balance>
+                       CONTRACT_BAL:Int
+                     </balance>
+                     <storage>
+                       CONTRACT_STORAGE:Map
+                     </storage>
+                     <nonce>
+                       CONTRACT_NONCE:Int
+                     </nonce>
+                     ...
+                   </account>
+                   ACCOUNTS_REST:AccountCellMap ) ) )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               ...
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+             <mockCalls>
+               .MockCallCellMap
+             </mockCalls>
+           </cheatcodes>
+           <KEVMTracing>
+             <activeTracing>
+               false
+             </activeTracing>
+             <traceStorage>
+               false
+             </traceStorage>
+             <traceWordStack>
+               false
+             </traceWordStack>
+             <traceMemory>
+               false
+             </traceMemory>
+             <recordedTrace>
+               false
+             </recordedTrace>
+             <traceData>
+               .List
+             </traceData>
+           </KEVMTracing>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( 0 <=Int CONTRACT_ID:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int CONTRACT_BAL:Int
+       andBool ( 0 <=Int CONTRACT_NONCE:Int
+       andBool ( 0 <=Int TIMESTAMP_CELL:Int
+       andBool ( CALLDEPTH_CELL:Int <Int 1024
+       andBool ( 1023 <=Int CALLDEPTH_CELL:Int
+       andBool ( 0 <=Int CONTRACT-TOKEN_BAL:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_BAL:Int
+       andBool ( 0 <=Int CONTRACT-TOKEN_NONCE:Int
+       andBool ( 0 <=Int CONTRACT-ESCROW_NONCE:Int
+       andBool ( CONTRACT_NONCE:Int <Int maxUInt64
+       andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CONTRACT-TOKEN_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT-ESCROW_NONCE:Int <Int maxUInt64
+       andBool ( CONTRACT_ID:Int =/=Int 645326474426547203313410069153905908525362434349
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( CONTRACT_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( CONTRACT_BAL:Int <Int pow256
+       andBool ( TIMESTAMP_CELL:Int <Int pow256
+       andBool ( CONTRACT-TOKEN_BAL:Int <Int pow256
+       andBool ( CONTRACT-ESCROW_BAL:Int <Int pow256
+       andBool ( ( notBool <acctID>
+          CONTRACT_ID:Int
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( _CONTRACT-ESCROW_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( _CONTRACT-TOKEN_ID ==Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
+       andBool ( ( notBool #range ( 0 < CONTRACT_ID:Int <= 9 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( CONTRACT_ID:Int =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+       andBool ( 645326474426547203313410069153905908525362434349 =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( notBool <acctID>
+          ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+        </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+       andBool ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=K ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) <= 9 ) )
+       andBool ( ( notBool #range ( 0 < ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) <= 9 ) )
+               ))))))))))))))))))))))))))))))))))))))))))
+       ensures ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) =/=Int ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) )
+      [priority(20), label(BASIC-BLOCK-17-TO-11)]
+
+endmodule
\ No newline at end of file

From e82ab0c62bc6a6e0dbe4220f0af0cd7d20c8b936 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Wed, 12 Jun 2024 19:40:10 +0700
Subject: [PATCH 34/35] Update output to account for TGovernance

---
 .../test-data/show/contracts.k.expected       | 19 +++++++++++++++++++
 .../test-data/show/foundry.k.expected         |  8 ++++++++
 2 files changed, 27 insertions(+)

diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index 8d7af1bf0..e2748c1d7 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -2977,6 +2977,25 @@ module S2KtestZModTEscrow-CONTRACT
     rule  ( selector ( "getTokenTotalSupply()" ) => 1474266187 )
       
 
+endmodule
+
+module S2KtestZModTGovernance-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KtestZModTGovernanceContract
+    
+    syntax S2KtestZModTGovernanceContract ::= "S2KtestZModTGovernance" [symbol(""), klabel(contract_test%TGovernance)]
+    
+    syntax Bytes ::= S2KtestZModTGovernanceContract "." S2KtestZModTGovernanceMethod [function, symbol(""), klabel(method_test%TGovernance)]
+    
+    syntax S2KtestZModTGovernanceMethod ::= "S2KgetEscrowTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%TGovernance_S2KgetEscrowTokenTotalSupply_)]
+    
+    rule  ( S2KtestZModTGovernance . S2KgetEscrowTokenTotalSupply ( ) => #abiCallData ( "getEscrowTokenTotalSupply" , .TypedArgs ) )
+      
+    
+    rule  ( selector ( "getEscrowTokenTotalSupply()" ) => 2061189261 )
+      
+
 endmodule
 
 module S2KtestZModTToken-CONTRACT
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index f4f9de4e5..203552e96 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -38,6 +38,7 @@ module FOUNDRY-MAIN
     imports public S2KtestZModContractBTest-VERIFICATION
     imports public S2KtestZModContractFieldTest-VERIFICATION
     imports public S2KtestZModTEscrow-VERIFICATION
+    imports public S2KtestZModTGovernance-VERIFICATION
     imports public S2KtestZModTToken-VERIFICATION
     imports public S2KtestZModCounter-VERIFICATION
     imports public S2KtestZModCounterTest-VERIFICATION
@@ -377,6 +378,13 @@ module S2KtestZModTEscrow-VERIFICATION
     
     
 
+endmodule
+
+module S2KtestZModTGovernance-VERIFICATION
+    imports public S2KtestZModTGovernance-CONTRACT
+    
+    
+
 endmodule
 
 module S2KtestZModTToken-VERIFICATION

From 40e0f37e31cf6a993d3b4aa28b1d2f23ba6b9f82 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 12 Jun 2024 15:34:39 +0100
Subject: [PATCH 35/35] correction

---
 src/kontrol/prove.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 046cba8c6..c11e5e0cf 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -688,10 +688,11 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, config_type: ConfigTy
             [account.config for account in new_accounts_map.values()] + non_cell_accounts
         )
 
+        new_init_cterm = CTerm(cterm.config, [])
+
         for cell_name, cell_value in cells.items():
-            cterm = CTerm(set_cell(cterm.config, cell_name, cell_value), [])
+            new_init_cterm = CTerm(set_cell(new_init_cterm.config, cell_name, cell_value), [])
 
-        new_init_cterm = cterm
     # config_type == ConfigType.SUMMARY_CONFIG
     # This means that a function is being run in isolation, that is, that the `node` we are
     # taking information from has come from a constructor and not a setUp function.