From 5084dc9028d30a3d7ae1ebb1265e9e8b905ee5fc Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 23 Sep 2024 22:08:37 +0800 Subject: [PATCH 1/2] Assume an `address` field is not `vm` --- src/kontrol/prove.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 261ca9ddd..caefa977d 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1216,6 +1216,19 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: address_range_ub = ltInt(field_variable, intToken(1461501637330902918203684832716283019655932542976)) new_account_constraints.append(mlEqualsTrue(address_range_lb)) new_account_constraints.append(mlEqualsTrue(address_range_ub)) + # Address is not the cheatcode contract address + new_account_constraints.append( + mlEqualsFalse( + KApply( + '_==Int_', + [ + field_variable, + Foundry.address_CHEATCODE(), + ], + ) + ) + ) + # TODO(palina): assume it's not a precompiled address # Processing of contracts if field.data_type.startswith('contract '): if field.linked_interface: From 2397468d2a50d9439117e3ae50ab6653c2dda5c4 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Thu, 26 Sep 2024 22:17:26 +0800 Subject: [PATCH 2/2] Add percompile constraints --- src/kontrol/prove.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index caefa977d..4a1bb8d23 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1044,7 +1044,7 @@ def _init_cterm( else: # Symbolic accounts of all relevant contracts accounts, storage_constraints = _create_cse_accounts( - foundry, storage_fields, contract_account_name, contract_code + foundry, storage_fields, contract_account_name, contract_code, schedule ) accounts.append(KVariable('ACCOUNTS_REST', sort=KSort('AccountCellMap'))) @@ -1135,6 +1135,7 @@ def _create_cse_accounts( storage_fields: tuple[StorageField, ...], contract_name: str, contract_code: KInner, + schedule: KApply, ) -> tuple[list[KInner], list[KApply]]: """ Recursively generates a list of new accounts corresponding to `contract` fields, each having and cell (partially) set up. @@ -1228,7 +1229,18 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: ) ) ) - # TODO(palina): assume it's not a precompiled address + # Address is not a precompiled contract address + # _account_constraints.append( + # mlEqualsFalse(KEVM.is_precompiled_account(acct_id.args[0], cterm.cell('SCHEDULE_CELL'))) + # ) + new_account_constraints.append( + mlEqualsFalse( + KEVM.is_precompiled_account( + field_variable, + schedule, + ) + ) + ) # Processing of contracts if field.data_type.startswith('contract '): if field.linked_interface: