CSE: Include symbolic contracts corresponding to contract fields into accounts (#600)

* Draft implementation and test for `contract` field accounts inclusion

* Set Version: 0.1.301

* Set Version: 0.1.301

* Set Version: 0.1.302

* Use (simple) `#lookup` constraint for `contract` field in storage

* Minor formatting

* Set Version: 0.1.303

* Draft implementation refactoring

* Set Version: 0.1.306

* renaming contracts to avoid conflicts, removing unneeded constraints

* minor streamlining

* Set Version: 0.1.307

* Set Version: 0.1.308

* removing unused variable

* renaming re-assigned variable

* Make `_create_cse_accounts` apply recursively on `contract` field accounts

* Code quality improvement

* Set Version: 0.1.309

* Avoid adding new accs for constructors, add new CSE test for recursive storage building

* Enforce same symbolic storage variable name between constructor and functions

* tests with immutables

* stabilising tests

* Set Version: 0.1.309

* Update expected output, remove `Accounts` test

* Update `contracts.k` expected output to reflect removal of `Accounts`

* Set Version: 0.1.310

* Use default symbolic storage var name for constructor storage with CSE

* Documented `_create_cse_accounts`

* One other output update

* Set Version: 0.1.311

* Apply refactoring from review comments

* Apply refactoring from review comments, preserve `new_init_cterm`

* Add test for recursive storage generation in new accounts

* Update output to account for TGovernance

* correction

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 5 people

package/version

@@ -1 +1 @@
-0.1.310
+0.1.311

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. <[email protected]>",

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'

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
@@ -42,6 +42,7 @@
 
     from .deployment import DeploymentStateEntry
     from .options import ProveOptions
+    from .solc_to_k import StorageField
 
 _LOGGER: Final = logging.getLogger(__name__)
 
@@ -520,6 +521,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,
@@ -555,6 +557,7 @@ def _method_to_initialized_cfg(
 
 
 def _method_to_cfg(
+    foundry: Foundry,
     empty_config: KInner,
     contract: Contract,
     method: Contract.Method | Contract.Constructor,
@@ -581,9 +584,11 @@ def _method_to_cfg(
         program = contract_code
 
     init_cterm = _init_cterm(
+        foundry,
         empty_config,
         program=program,
         contract_code=bytesToken(contract_code),
+        storage_fields=contract.fields,
         method=method,
         use_gas=use_gas,
         deployment_state_entries=deployment_state_entries,
@@ -652,66 +657,76 @@ 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')),
-                ),
-                [],
-            )
+    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',
+        ]
+
+        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}
+
+        cells['ACCOUNTS_CELL'] = KEVM.accounts(
+            [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():
+            new_init_cterm = CTerm(set_cell(new_init_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.
+    # 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_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), [])
+        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:
@@ -773,9 +788,11 @@ def _init_account(address: int) -> None:
 
 
 def _init_cterm(
+    foundry: Foundry,
     empty_config: KInner,
     program: bytes,
     contract_code: KInner,
+    storage_fields: tuple[StorageField, ...],
     method: Contract.Method | Contract.Constructor,
     use_gas: bool,
     config_type: ConfigType,
@@ -827,6 +844,8 @@ def _init_cterm(
         'TRACEDATA_CELL': KApply('.List'),
     }
 
+    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)
         init_subst_test = {
@@ -844,13 +863,18 @@ 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] = [
-            Foundry.symbolic_account(Foundry.symbolic_contract_prefix(), contract_code),
-            KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap')),
-        ]
+        accounts: list[KInner] = []
+
+        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')))
 
         init_subst_accounts = {'ACCOUNTS_CELL': KEVM.accounts(accounts)}
         init_subst.update(init_subst_accounts)
@@ -881,6 +905,9 @@ def _init_cterm(
             mlEqualsFalse(KApply('_==Int_', [KVariable(contract_id, sort=KSort('Int')), Foundry.address_CHEATCODE()]))
         )
 
+    for constraint in storage_constraints:
+        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):
         init_cterm.add_constraint(
@@ -893,8 +920,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)
 
@@ -922,6 +949,75 @@ def _create_initial_account_list(
     return init_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] = []
+
+    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 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 full_contract_name.split('%')[-1] == contract_type:
+                    contract_account_code = bytesToken(bytes.fromhex(contract_obj.deployed_bytecode))
+                    contract_account_name = 'CONTRACT-' + field.label.upper()
+
+                    # TODO: handle the case where the field has a non-zero offset
+                    # maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 )
+                    contract_storage_lookup = KApply(
+                        '_&Int_',
+                        [
+                            intToken(1461501637330902918203684832716283019655932542975),
+                            KEVM.lookup(storage_map, 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
+                    new_account_constraints.append(
+                        mlEqualsFalse(
+                            KApply(
+                                '_==Int_',
+                                [
+                                    KVariable(contract_account_name + '_ID', sort=KSort('Int')),
+                                    Foundry.address_CHEATCODE(),
+                                ],
+                            )
+                        )
+                    )
+
+                    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(
     empty_config: KInner,
     program: KInner,

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
 

src/tests/integration/test-data/foundry-dependency-all

@@ -7,6 +7,8 @@ ArithmeticContract.add_sub_external(uint256,uint256,uint256)
 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)