From 71adb1a61d30b875263d40053c956f0c5768d55d Mon Sep 17 00:00:00 2001 From: Palina Tolmach Date: Thu, 13 Jun 2024 00:40:25 +0700 Subject: [PATCH] CSE: Include symbolic contracts corresponding to `contract` fields into accounts (#600) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 Co-authored-by: Petar Maksimović Co-authored-by: Petar Maksimovic Co-authored-by: rv-jenkins --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/prove.py | 234 +++-- src/tests/integration/test-data/cse-lemmas.k | 16 +- .../test-data/foundry-dependency-all | 2 + .../foundry/test/ContractFieldTest.t.sol | 56 ++ .../AddConst.applyOp(uint256).cse.expected | 18 +- ...ctFieldTest.testEscrowToken().cse.expected | 309 +++++++ ...ImportedContract.add(uint256).cse.expected | 22 +- .../ImportedContract.count().cse.expected | 6 +- ...ImportedContract.set(uint256).cse.expected | 18 +- ...e.getEscrowTokenTotalSupply().cse.expected | 843 ++++++++++++++++++ .../test-data/show/contracts.k.expected | 164 ++++ .../test-data/show/foundry.k.expected | 32 + .../test-data/symbolic-bytes-lemmas.k | 26 +- 16 files changed, 1646 insertions(+), 106 deletions(-) create mode 100644 src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol create mode 100644 src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected create mode 100644 src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected 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. ", 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' diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index b12ac84e1..c11e5e0cf 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 @@ -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 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 `` 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 and 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, 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 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-dependency-all b/src/tests/integration/test-data/foundry-dependency-all index 5880aa6c5..5ec64edc3 100644 --- a/src/tests/integration/test-data/foundry-dependency-all +++ b/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) 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..f5ebfa692 --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/ContractFieldTest.t.sol @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; +import {Test} from "forge-std/Test.sol"; + +contract TToken { + uint128 private totalSupply; + + constructor(uint128 _totalSupply) { + totalSupply = _totalSupply; + } + + function getTotalSupply() public returns (uint256) { + return 32 + uint256(totalSupply); + } +} + +contract TEscrow { + TToken token; + + constructor(address _token) { + token = TToken(_token); + } + + function getTokenTotalSupply() public returns (uint256) { + return token.getTotalSupply() + 13; + } +} + +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; + + function setUp() public { + token = new TToken(12300); + escrow = new TEscrow(address(token)); + } + + /* Calling `getTokenTotalSupply` will summarize `totalSupply` and + include `TestToken token` into the list of accounts in `getTokenTotalSupply`'s summary + */ + function testEscrowToken() public { + assert(escrow.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 ) ) CONTINUATION:K @@ -76,7 +76,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 - ( _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 ) ) ) ) ( _STATUSCODE => EVMC_SUCCESS ) @@ -98,7 +98,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 ( .WordStack => ( selector ( "applyOp(uint256)" ) : .WordStack ) ) - ( 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 ) ) ) ) 0 @@ -138,7 +138,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 CONTRACT_BAL:Int - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map 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 - ( .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 ) ) ) ) ) ) ) ) ) ( 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 - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map 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 ) ) CONTINUATION:K +│ pc: 0 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ +│ (2219 steps) +├─ 8 (terminal) +│ k: #halt ~> CONTINUATION:K +│ pc: 194 +│ callDepth: 0 +│ statusCode: EVMC_SUCCESS +│ +┊ constraint: true +┊ subst: OMITTED SUBST +└─ 7 (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-8]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + .List + + + .List + + + ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) ) + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + ( b"\n\x92T\xe4" => b"51X\xa0" ) + + + 0 + + + ( .WordStack => ( selector ( "testEscrowToken()" ) : .WordStack ) ) + + + ( 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" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) ) + + + .Map + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + ( + + ( 645326474426547203313410069153905908525362434349 => 263400868551549723330807389252719309078400616203 ) + + + 0 + + + ( .Map => ( 0 |-> 491460923342184218035706888008750043977755113263 ) ) + + + .Map + + + ( 0 => 1 ) + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( ( 11 |-> 1 ) + ( 7 |-> 1 ) ) + + + .Map + + + 1 + + ... + => ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + ( 0 |-> 12300 ) + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( ( 11 |-> 1 ) + ( ( 27 |-> 491460923342184218035706888008750043977755113263 ) + ( ( 28 |-> 263400868551549723330807389252719309078400616203 ) + ( 7 |-> 1 ) ) ) ) + + + .Map + + + 3 + + ... + ) ) ) ) + + ... + + + ... + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + .MockCallCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + 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 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 - ( .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 ) ) ) ) ) ) ) ) ( 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 - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map 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 ) - ( 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 ) ] ) 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 - ( .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 ) ) ) ) ) ) ( 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 - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map 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 - ( _OUTPUT_CELL => #buf ( 32 , #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) ) ) + ( _OUTPUT_CELL => #buf ( 32 , #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) ( _STATUSCODE => EVMC_SUCCESS ) @@ -66,7 +66,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 ( .WordStack => ( 73 : ( selector ( "count()" ) : .WordStack ) ) ) - ( 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 ) ) ) 0 @@ -106,7 +106,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 CONTRACT_BAL:Int - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map 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 ) 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 - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map CONTRACT_NONCE:Int @@ -271,7 +271,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 andBool ( ( notBool CONTRACT_ID:Int in_keys ( ACCOUNTS_REST:AccountCellMap ) ) - andBool ( #lookup ( STORAGE_CONTRACT_ID:Map , 0 ) - ( STORAGE_CONTRACT_ID:Map => STORAGE_CONTRACT_ID:Map [ 0 <- VV0_x_114b9705:Int ] ) + ( CONTRACT_STORAGE:Map => CONTRACT_STORAGE:Map [ 0 <- VV0_x_114b9705:Int ] ) CONTRACT_NONCE:Int @@ -468,7 +468,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 andBool ( ( notBool CONTRACT_ID:Int 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 - STORAGE_CONTRACT_ID:Map + CONTRACT_STORAGE:Map CONTRACT_NONCE:Int @@ -662,7 +662,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 andBool ( ( notBool CONTRACT_ID:Int 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/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 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 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]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + ( _OUTPUT_CELL => b"" ) + + + ( _STATUSCODE => EVMC_REVERT ) + + + + CONTRACT_ID:Int + + + CALLER_ID:Int + + + b"z\xdb@\x8d" + + + 0 + + + ( .WordStack => ( 1 : ( 132 : ( selector ( "getTokenTotalSupply()" ) : ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) : ( 0 : ( 51 : ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) ) ) ) ) ) ) ) + + + ( 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" ) + + + 0 + + + 0 + + + CALLDEPTH_CELL:Int + + ... + + + + 0 + + + ( ACCESSEDACCOUNTS_CELL:Set => ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) ) + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + + + CONTRACT-TOKEN_BAL:Int + + + CONTRACT-TOKEN_NONCE:Int + + ... + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + + + CONTRACT-ESCROW_BAL:Int + + + CONTRACT-ESCROW_STORAGE:Map + + + CONTRACT-ESCROW_NONCE:Int + + ... + + ( + + CONTRACT_ID:Int + + + CONTRACT_BAL:Int + + + CONTRACT_STORAGE:Map + + + CONTRACT_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) ) ) + + ... + + + ... + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + .MockCallCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + 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 + CONTRACT_ID:Int + 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 + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( ( notBool + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + 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]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + ( _OUTPUT_CELL => #buf ( 32 , ( ( maxUInt128 &Int #lookup ( CONTRACT-TOKEN_STORAGE:Map , 0 ) ) +Int 45 ) ) ) + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + ( 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 ) ) ) ) + + + + CONTRACT_ID:Int + + + CALLER_ID:Int + + + b"z\xdb@\x8d" + + + 0 + + + ( .WordStack => ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) ) + + + ( 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 ) ) ) + + + 0 + + + 0 + + + CALLDEPTH_CELL:Int + + ... + + + + 0 + + + ( 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 ) ) ) ) + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + + + CONTRACT-TOKEN_BAL:Int + + + CONTRACT-TOKEN_STORAGE:Map + + + CONTRACT-TOKEN_NONCE:Int + + ... + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + + + CONTRACT-ESCROW_BAL:Int + + + CONTRACT-ESCROW_STORAGE:Map + + + CONTRACT-ESCROW_NONCE:Int + + ... + + ( + + CONTRACT_ID:Int + + + CONTRACT_BAL:Int + + + CONTRACT_STORAGE:Map + + + CONTRACT_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) ) ) + + ... + + + ... + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + .MockCallCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + 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 + CONTRACT_ID:Int + 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 + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( ( notBool + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + 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]: + + + ( #execute => #halt ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + ( _OUTPUT_CELL => b"" ) + + + ( _STATUSCODE => EVMC_REVERT ) + + + ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( CONTRACT_ID:Int ) |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) ) + + + + CONTRACT_ID:Int + + + CALLER_ID:Int + + + b"z\xdb@\x8d" + + + 0 + + + ( .WordStack => ( 1 : ( 132 : ( selector ( "getTokenTotalSupply()" ) : ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) : ( 0 : ( 51 : ( selector ( "getEscrowTokenTotalSupply()" ) : .WordStack ) ) ) ) ) ) ) ) + + + ( 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" ) + + + 0 + + + 0 + + + CALLDEPTH_CELL:Int + + ... + + + + 0 + + + ( ACCESSEDACCOUNTS_CELL:Set => ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) ) ) + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + + + CONTRACT-TOKEN_BAL:Int + + + CONTRACT-TOKEN_NONCE:Int + + ... + + ( + + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + + + CONTRACT-ESCROW_BAL:Int + + + CONTRACT-ESCROW_STORAGE:Map + + + CONTRACT-ESCROW_NONCE:Int + + ... + + ( + + CONTRACT_ID:Int + + + CONTRACT_BAL:Int + + + CONTRACT_STORAGE:Map + + + CONTRACT_NONCE:Int + + ... + + ACCOUNTS_REST:AccountCellMap ) ) ) + + ... + + + ... + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .Set + + + .Set + + + + .MockCallCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + 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 + CONTRACT_ID:Int + 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 + ( maxUInt160 &Int #lookup ( CONTRACT_STORAGE:Map , 0 ) ) + in_keys ( ACCOUNTS_REST:AccountCellMap ) ) + andBool ( ( notBool + ( maxUInt160 &Int #lookup ( CONTRACT-ESCROW_STORAGE:Map , 0 ) ) + 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 diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index ff068b97c..e2748c1d7 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -2851,6 +2851,170 @@ 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 S2KtestZModTEscrow-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KtestZModTEscrowContract + + syntax S2KtestZModTEscrowContract ::= "S2KtestZModTEscrow" [symbol(""), klabel(contract_test%TEscrow)] + + syntax Bytes ::= S2KtestZModTEscrowContract "." S2KtestZModTEscrowMethod [function, symbol(""), klabel(method_test%TEscrow)] + + syntax S2KtestZModTEscrowMethod ::= "S2KgetTokenTotalSupply" "(" ")" [symbol(""), klabel(method_test%TEscrow_S2KgetTokenTotalSupply_)] + + rule ( S2KtestZModTEscrow . S2KgetTokenTotalSupply ( ) => #abiCallData ( "getTokenTotalSupply" , .TypedArgs ) ) + + + 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 + imports public FOUNDRY + + syntax Contract ::= S2KtestZModTTokenContract + + syntax S2KtestZModTTokenContract ::= "S2KtestZModTToken" [symbol(""), klabel(contract_test%TToken)] + + syntax Bytes ::= S2KtestZModTTokenContract "." S2KtestZModTTokenMethod [function, symbol(""), klabel(method_test%TToken)] + + syntax S2KtestZModTTokenMethod ::= "S2KgetTotalSupply" "(" ")" [symbol(""), klabel(method_test%TToken_S2KgetTotalSupply_)] + + rule ( S2KtestZModTToken . S2KgetTotalSupply ( ) => #abiCallData ( "getTotalSupply" , .TypedArgs ) ) + + + rule ( selector ( "getTotalSupply()" ) => 3303283490 ) + + 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..203552e96 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -36,6 +36,10 @@ module FOUNDRY-MAIN imports public S2KtestZModImportedContract-VERIFICATION imports public S2KtestZModContractTest-VERIFICATION 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 imports public S2KsrcZModDeploymentState-VERIFICATION @@ -360,6 +364,34 @@ module S2KtestZModContractBTest-VERIFICATION +endmodule + +module S2KtestZModContractFieldTest-VERIFICATION + imports public S2KtestZModContractFieldTest-CONTRACT + + + +endmodule + +module S2KtestZModTEscrow-VERIFICATION + imports public S2KtestZModTEscrow-CONTRACT + + + +endmodule + +module S2KtestZModTGovernance-VERIFICATION + imports public S2KtestZModTGovernance-CONTRACT + + + +endmodule + +module S2KtestZModTToken-VERIFICATION + imports public S2KtestZModTToken-CONTRACT + + + endmodule module S2KtestZModCounter-VERIFICATION diff --git a/src/tests/integration/test-data/symbolic-bytes-lemmas.k b/src/tests/integration/test-data/symbolic-bytes-lemmas.k index 4a39293d9..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 + { #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