From 6dafb519fd459961e41a69c4052f9e8d4045ec45 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 9 Jul 2024 17:30:07 -0500 Subject: [PATCH 01/10] Add test, add more advanced storage types system --- src/kontrol/prove.py | 12 +- src/kontrol/solc_to_k.py | 115 ++++++++++++++++-- .../test-data/foundry/test/Mapping.t.sol | 39 ++++++ 3 files changed, 151 insertions(+), 15 deletions(-) create mode 100644 src/tests/integration/test-data/foundry/test/Mapping.t.sol diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 25ff12670..bd13d30b5 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1062,8 +1062,8 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: for field in storage_fields: field_name = contract_name + '_' + field.label.upper() - if field.data_type.startswith('enum'): - enum_name = field.data_type.split(' ')[1] + if field.data_type.name.startswith('enum'): + enum_name = field.data_type.name.split(' ')[1] enum_max = foundry.enums[enum_name] new_account_constraints.append( mlEqualsTrue( @@ -1074,7 +1074,7 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: ) ) # Processing of strings - if field.data_type == 'string': + if field.data_type.name == 'string': string_contents = KVariable(field_name + '_S_CONTENTS', sort=KSort('Bytes')) string_length = KVariable(field_name + '_S_LENGTH', sort=KSort('Int')) string_structure = KEVM.as_word( @@ -1098,7 +1098,7 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: new_account_constraints.append(mlEqualsTrue(string_length_lb)) new_account_constraints.append(mlEqualsTrue(string_length_ub)) # Processing of addresses - if field.data_type == 'address': + if field.data_type.name == 'address': if field.slot in singly_occupied_slots: # The offset must equal zero assert field.offset == 0 @@ -1111,11 +1111,11 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: new_account_constraints.append(mlEqualsTrue(address_range_lb)) new_account_constraints.append(mlEqualsTrue(address_range_ub)) # Processing of contracts - if field.data_type.startswith('contract '): + if field.data_type.name.startswith('contract '): if field.linked_interface: contract_type = field.linked_interface else: - contract_type = field.data_type.split(' ')[1] + contract_type = field.data_type.name.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 diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 4d6219912..e28bef4e6 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -18,6 +18,8 @@ from pyk.prelude.kint import eqInt, intToken, ltInt from pyk.prelude.string import stringToken from pyk.utils import hash_str, run_process, single +from pyk.prelude.ml import mlEqualsTrue +from pyk.prelude.k import K_ITEM, GENERATED_TOP_CELL if TYPE_CHECKING: from collections.abc import Iterable @@ -337,7 +339,7 @@ def parse_devdoc(tag: str, devdoc: dict | None) -> dict: class StorageField(NamedTuple): label: str - data_type: str + data_type: StorageFieldType slot: int offset: int linked_interface: str | None @@ -1378,6 +1380,108 @@ def _find_function_calls(node: dict) -> None: _find_function_calls(node) return function_calls +@dataclass +class StorageFieldType: + name: str + pred: KInner | None + + def compute_preds(self, base_pred: KInner) -> None: + self.pred = base_pred + + def preds(self) -> list[tuple[KInner, str]]: + assert self.pred is not None + return [(self.pred, self.name)] + + def pred_vars(self) -> list[KInner]: + return [] + + def compute_constraints(self, storage_map: KInner) -> list[KInner]: + + constraints: list[KInner] = [] + for pred, pred_type in self.preds(): + assert isinstance(pred, KApply) + constraint = _range_predicate(term=KEVM.lookup(storage_map, pred.args[1]), type_label=pred_type) + if constraint is not None: + constraint = mlEqualsTrue(constraint) + for pred_var in self.pred_vars(): + constraint = KLabel('#Forall', K_ITEM, GENERATED_TOP_CELL)(pred_var, constraint) + constraints.append(constraint) + return constraints + +@dataclass +class StorageFieldArrayType(StorageFieldType): + base_type: StorageFieldType + + +@dataclass +class StorageFieldMappingType(StorageFieldType): + key_type: StorageFieldType + val_type: StorageFieldType + pred_var: tuple[KInner, ...] = () + + def pred_vars(self) -> list[KInner]: + return list(self.pred_var) + self.val_type.pred_vars() + + def compute_preds(self, base_pred: KInner) -> None: + variable = KVariable('V_' + hash_str(base_pred)[0:8]) + self.pred_var = (variable,) + self.pred = base_pred + self.val_type.compute_preds( + KApply('buf', [intToken(32), + KApply('keccak(_)_SERIALIZATION_Int_Bytes', [ + KEVM.bytes_append( + variable, + base_pred, + ) + ]) + ]) + ) + + def preds(self) -> list[tuple[KInner, str]]: + assert self.pred is not None + return [(self.pred, self.name)] + self.val_type.preds() + +@dataclass +class StorageFieldStructType(StorageFieldType): + members: tuple[StorageField, ...] + + +def build_storage_field_type(dct: dict, types_dct: dict, interface_annotations: dict) -> StorageFieldType: + if 'key' in dct: + # Mapping + return StorageFieldMappingType( + name=dct['label'], + key_type=build_storage_field_type(types_dct[dct['key']], types_dct, interface_annotations), + val_type=build_storage_field_type(types_dct[dct['value']], types_dct, interface_annotations), + pred=None, + ) + elif 'members' in dct: + # Struct + return StorageFieldStructType( + name=dct['label'], + members=tuple(storage_field_from_dict(member, types_dct, interface_annotations) for member in dct['members']), + pred=None, + ) + elif 'base' in dct: + # Array + return StorageFieldArrayType( + name=dct['label'], + base_type=build_storage_field_type(types_dct[dct['base']], types_dct, interface_annotations), + pred=None, + ) + else: + # Other + return StorageFieldType(name=dct['label'], pred=None) + + +def storage_field_from_dict(dct: dict, types_dct: dict, interface_annotations: dict) -> StorageField: + label= dct['label'] + slot = int(dct['slot']) + offset = int(dct['offset']) + data_type = build_storage_field_type(types_dct[dct['type']], types_dct, interface_annotations) + linked_interface = interface_annotations.get(dct['label'], None) + return StorageField(label, data_type, slot, offset, linked_interface) + def process_storage_layout(storage_layout: dict, interface_annotations: dict) -> tuple[StorageField, ...]: storage = storage_layout.get('storage', []) @@ -1386,14 +1490,7 @@ def process_storage_layout(storage_layout: dict, interface_annotations: dict) -> fields_list: list[StorageField] = [] for field in storage: try: - type_info = types.get(field['type'], {}) - storage_field = StorageField( - label=field['label'], - data_type=type_info.get('label', field['type']), - slot=int(field['slot']), - offset=int(field['offset']), - linked_interface=interface_annotations.get(field['label'], None), - ) + storage_field = storage_field_from_dict(field, types, interface_annotations) fields_list.append(storage_field) except (KeyError, ValueError) as e: _LOGGER.error(f'Error processing field {field}: {e}') diff --git a/src/tests/integration/test-data/foundry/test/Mapping.t.sol b/src/tests/integration/test-data/foundry/test/Mapping.t.sol new file mode 100644 index 000000000..d9844e869 --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/Mapping.t.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +contract MappingContract { + mapping(address => mapping(address => uint256)) public balances; + mapping(address => uint256) public single_map; + + function get_mapping_val(address a) public returns (uint256) { + return balances[a][a]; + } + + function get_mapping_val2(address a) public returns (uint256) { + return single_map[a]; + } +} + +contract MappingTest is Test { + uint256 val; + uint256 val2; + MappingContract c; + + constructor() public { + c = new MappingContract(); + } + + function my_internal() internal { } + + function test_mapping(address a) public { + val = c.get_mapping_val(a); + val2 = c.get_mapping_val2(a); + my_internal(); + assert(val < 256); + assert(val2 < 256); + } + +} From e7bd8eac61780f7bb630a7a81ecfb06802eb8129 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Jul 2024 22:31:33 +0000 Subject: [PATCH 02/10] Set Version: 0.1.348 --- 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 4b816fda1..737844ba1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.347 +0.1.348 diff --git a/pyproject.toml b/pyproject.toml index eba2b5321..ebe1dc520 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.347" +version = "0.1.348" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 00b5d622d..130d29d96 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.347' +VERSION: Final = '0.1.348' From e06c75c5ae35cbffaeb64da170d1f3aad06f880c Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 11 Jul 2024 09:47:18 +0000 Subject: [PATCH 03/10] Set Version: 0.1.349 --- 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 737844ba1..11ca9de75 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.348 +0.1.349 diff --git a/pyproject.toml b/pyproject.toml index a26b294e5..89fc01d60 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.348" +version = "0.1.349" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 130d29d96..055f482b2 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.348' +VERSION: Final = '0.1.349' From 3f2700400eb5153f0b2b05cbdb2d46fe0e1a2d16 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 11 Jul 2024 19:57:39 +0000 Subject: [PATCH 04/10] Set Version: 0.1.350 --- 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 11ca9de75..5e7980b7d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.349 +0.1.350 diff --git a/pyproject.toml b/pyproject.toml index 194116570..402f1657e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.349" +version = "0.1.350" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 055f482b2..35d8c0d91 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.349' +VERSION: Final = '0.1.350' From 0f12f214a4b776bce23ac8e057fda92e18a182df Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 12 Jul 2024 18:33:27 +0000 Subject: [PATCH 05/10] Set Version: 0.1.351 --- 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 5e7980b7d..8013983ed 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.350 +0.1.351 diff --git a/pyproject.toml b/pyproject.toml index 402f1657e..47370e8d4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.350" +version = "0.1.351" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 35d8c0d91..6386b0519 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.350' +VERSION: Final = '0.1.351' From f378be0466f25a381ac56dbd033b8a39a4463d60 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 12 Jul 2024 13:57:32 -0500 Subject: [PATCH 06/10] Fix constraint generation --- src/kontrol/prove.py | 9 +++++++++ src/kontrol/solc_to_k.py | 3 ++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 378fdb88c..e440e09a1 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1064,6 +1064,15 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: ] for field in storage_fields: + + for constraint in field.data_type.compute_constraints(storage_map): + new_account_constraints.append(constraint) + print(constraint) +# print(field.data_type.slot_vars()) + +# if isinstance(field.data_type, StorageFieldMappingType): +# ... + field_name = contract_name + '_' + field.label.upper() if field.data_type.name.startswith('enum'): enum_name = field.data_type.name.split(' ')[1] diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 7998256a9..05a8836c5 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -1428,7 +1428,7 @@ def compute_preds(self, base_pred: KInner) -> None: self.pred = base_pred self.val_type.compute_preds( KApply('buf', [intToken(32), - KApply('keccak(_)_SERIALIZATION_Int_Bytes', [ + KApply('keccak', [ KEVM.bytes_append( variable, base_pred, @@ -1492,6 +1492,7 @@ def process_storage_layout(storage_layout: dict, interface_annotations: dict) -> try: storage_field = storage_field_from_dict(field, types, interface_annotations) fields_list.append(storage_field) + storage_field.data_type.compute_preds(KApply('buf', [intToken(32), intToken(storage_field.slot)])) except (KeyError, ValueError) as e: _LOGGER.error(f'Error processing field {field}: {e}') From 8743729d3c3c3932242e6525a88286bf8dcb419a Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 15 Jul 2024 18:59:01 +0000 Subject: [PATCH 07/10] Set Version: 0.1.353 --- 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 485cda699..7fe8a155c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.352 +0.1.353 diff --git a/pyproject.toml b/pyproject.toml index 886abc9e3..ceaba1d2d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.352" +version = "0.1.353" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index c9bdb6d7b..544fe2418 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.352' +VERSION: Final = '0.1.353' From 7ad2625ece83b09980d4a6de4ee1d40b48fec4bb Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 17 Jul 2024 17:53:24 -0500 Subject: [PATCH 08/10] Add KontrolAPRProver --- src/kontrol/prove.py | 67 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 9c95704f9..2e5456a98 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -12,7 +12,9 @@ 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.outer import KProduction, KFlatModule, KImport, KTerminal, KNonTerminal from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst +from pyk.konvert import kflatmodule_to_kore from pyk.kast.manip import flatten_label, set_cell from pyk.kcfg import KCFG, KCFGExplore from pyk.kore.rpc import KoreClient, TransportType, kore_server @@ -25,7 +27,7 @@ from pyk.prelude.string import stringToken from pyk.proof import ProofStatus from pyk.proof.proof import Proof -from pyk.proof.reachability import APRFailureInfo, APRProof +from pyk.proof.reachability import APRFailureInfo, APRProof, APRProver from pyk.utils import run_process_2, unique from .foundry import Foundry, foundry_to_xml @@ -36,6 +38,8 @@ from .utils import console, parse_test_version_tuple if TYPE_CHECKING: + from pyk.kast.outer import KSentence +# from pyk.kast.outer import KRule from collections.abc import Iterable from typing import Final, TypeGuard @@ -294,6 +298,55 @@ def __exit__(self, *args: Any) -> None: ... def port(self) -> int: return self._port +class KontrolAPRProver(APRProver): + accounts: list[str] + + def __init__( + self, + kcfg_explore: KCFGExplore, + accounts: list[str], + execute_depth: int | None = None, + cut_point_rules: Iterable[str] = (), + terminal_rules: Iterable[str] = (), + counterexample_info: bool = False, + always_check_subsumption: bool = True, + fast_check_subsumption: bool = False, + direct_subproof_rules: bool = False, + ) -> None: + + self.accounts = accounts + super().__init__(kcfg_explore, execute_depth, cut_point_rules, terminal_rules, counterexample_info, always_check_subsumption, fast_check_subsumption, direct_subproof_rules) + + def init_proof(self, proof: APRProof) -> None: + def _inject_module(module_name: str, import_name: str, sentences: list[KSentence]) -> None: + _module = KFlatModule(module_name, sentences, [KImport(import_name)]) + print(_module) + _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, _module) + self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) + + subproofs: list[Proof] = ( + [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids] + if proof.proof_dir is not None + else [] + ) + dependencies_as_rules: list[KSentence] = [ + rule + for subproof in subproofs + if isinstance(subproof, APRProof) + for rule in subproof.as_rules(priority=20, direct_rule=self.direct_subproof_rules) + ] + storage_invariants: list[KSentence] = [ + KProduction(KSort('Bool'), [KTerminal(f'{account}_storage_invariant'), KTerminal('('), KNonTerminal(KSort('Map')), KTerminal(')')]) for account in self.accounts + ] + circularity_rule = proof.as_rule(priority=20) + + _inject_module(proof.dependencies_module_name, self.main_module_name, dependencies_as_rules + storage_invariants) + _inject_module(proof.circularities_module_name, proof.dependencies_module_name, [circularity_rule]) + + for node_id in [proof.init, proof.target]: + if self.kcfg_explore.kcfg_semantics.is_terminal(proof.kcfg.node(node_id).cterm): + proof.add_terminal(node_id) + def _run_cfg_group( tests: list[FoundryTest], @@ -363,6 +416,7 @@ def create_kcfg_explore() -> KCFGExplore: id=test.id, ) + if proof is None: # With CSE, top-level proof should be a summary if it's not a test or setUp function if ( @@ -407,9 +461,20 @@ def create_kcfg_explore() -> KCFGExplore: cut_point_rules.extend( rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules ) + + def create_apr_prover() -> APRProver: + return KontrolAPRProver( + create_kcfg_explore(), + accounts=['abc', 'def', 'ghi'], + execute_depth=options.max_depth, + terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), + cut_point_rules=cut_point_rules, + counterexample_info=options.counterexample_info, + ) run_prover( proof, create_kcfg_explore=create_kcfg_explore, + create_apr_prover=create_apr_prover, max_depth=options.max_depth, max_iterations=options.max_iterations, cut_point_rules=cut_point_rules, From 14feebca7ca5e82aab61bb3879e3404bb2e7b640 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 22 Jul 2024 16:45:35 -0500 Subject: [PATCH 09/10] Generate invariant productions and add them to side conditions when generating symbolic storage --- src/kontrol/kompile.py | 4 +- src/kontrol/prove.py | 5 +++ src/kontrol/solc_to_k.py | 89 +++++++++++++++++++++++++++++++++++++--- 3 files changed, 92 insertions(+), 6 deletions(-) diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index c356975ee..70b108c65 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -97,6 +97,7 @@ def foundry_kompile( contracts=foundry.contracts.values(), requires=['foundry.md'], enums=foundry.enums, + foundry=foundry, ) contract_main_definition = _foundry_to_main_def( @@ -164,9 +165,10 @@ def _foundry_to_contract_def( contracts: Iterable[Contract], requires: Iterable[str], enums: dict[str, int], + foundry: Foundry, ) -> KDefinition: modules = [ - contract_to_main_module(contract, empty_config, imports=['FOUNDRY'], enums=enums) for contract in contracts + contract_to_main_module(contract, empty_config, imports=['FOUNDRY'], enums=enums, contracts=foundry.contracts) for contract in contracts ] # First module is chosen as main module arbitrarily, since the contract definition is just a set of # contract modules. diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 21f08ca47..6780c8d19 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1234,6 +1234,11 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: ) ) + new_account_constraints.append(mlEqualsTrue(KApply( + f's2k_invariant_{field_name}', [storage_map] + ))) + + contract_accounts, contract_constraints = _create_cse_accounts( foundry, contract_obj.fields, field_name, contract_account_code ) diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 028b31801..05f706e9d 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -50,7 +50,7 @@ def solc_to_k(options: SolcToKOptions) -> str: imports = list(options.imports) requires = list(options.requires) - contract_module = contract_to_main_module(contract, empty_config, enums={}, imports=['EDSL'] + imports) + contract_module = contract_to_main_module(contract, empty_config, enums={}, imports=['EDSL'] + imports, contracts={}) _main_module = KFlatModule( options.main_module if options.main_module else 'MAIN', [], @@ -1068,8 +1068,87 @@ def method_sentences(self, enums: dict[str, int]) -> list[KSentence]: res.extend(method.selector_alias_rule for method in self.methods) return res if len(res) > 1 else [] - def sentences(self, enums: dict[str, int]) -> list[KSentence]: - return [self.subsort, self.production] + self.method_sentences(enums) + def storage_productions(self, contracts: dict[str, Contract]) -> list[KSentence]: + + def get_contract(type_name: str) -> Contract: + for full_contract_name, contract_obj in contracts.items(): + if full_contract_name.split('%')[-1] == type_name: + return contract_obj + raise ValueError(f'Contract {type_name} not found.') + + def gen_accounts_list(contract: Contract, contract_name: str) -> list[str]: + accounts_list: list[str] = [] + for field in contract.fields: + if field.data_type.name.startswith('contract '): + field_name = f'C_{contract_name}_{field.label}'.upper() + accounts_list.append(field_name) + contract_type = field.data_type.name.split(' ')[1] + contract = get_contract(contract_type) + accounts_list += gen_accounts_list(contract=contract, contract_name=field_name) + return accounts_list + + storage_prods: list[KSentence] = [] + for account_label in gen_accounts_list(self, self._name): + storage_prods.append( + KProduction( + KSort('Bool'), + items=[ + KTerminal(f's2k_invariant_{account_label}'), + KTerminal('('), + KNonTerminal(KSort('Map')), + KTerminal(')'), + ], + att=KAtt(entries=[Atts.SYMBOL(f's2k_invariant_{account_label}'), Atts.FUNCTION(None)]), + ) + ) + + storage_prods.append( + KProduction( + KSort('Bool'), + items=[ + KTerminal(f's2k_entry_invariant_{account_label}'), + KTerminal('('), + KNonTerminal(KSort('Int')), + KTerminal(','), + KNonTerminal(KSort('Int')), + KTerminal(')'), + ], + att=KAtt(entries=[Atts.SYMBOL(f's2k_entry_invariant_{account_label}'), Atts.FUNCTION(None)]), + ) + ) + + storage_prods.append(KRule(KRewrite(KApply(f's2k_invariant_{account_label}', [KApply('.Map')]), TRUE))) + + storage_prods.append( + KRule( + KRewrite( + KApply( + f's2k_invariant_{account_label}', + [KApply('_Map_', [KApply('_|->_', [KVariable('K'), KVariable('V')]), KVariable('M')])], + ), + KApply( + '_andBool_', + [ + KApply(f's2k_entry_invariant_{account_label}', [KVariable('K'), KVariable('V')]), + KApply(f's2k_invariant_{account_label}', [KVariable('M')]), + ], + ), + ), + requires=KApply( + 'notBool_', + [ + KApply('_in_keys(_)_MAP_Bool_KItem_Map', [KVariable('K'), KVariable('M')]), + ], + ), + ) + ) + + return storage_prods + + def sentences(self, enums: dict[str, int], contracts: dict[str, Contract]) -> list[KSentence]: + sents: list[KSentence] = [self.subsort, self.production] + self.method_sentences(enums) + sents += self.storage_productions(contracts) + return sents @property def method_by_name(self) -> dict[str, Contract.Method]: @@ -1135,10 +1214,10 @@ def solc_compile(contract_file: Path) -> dict[str, Any]: def contract_to_main_module( - contract: Contract, empty_config: KInner, enums: dict[str, int], imports: Iterable[str] = () + contract: Contract, empty_config: KInner, enums: dict[str, int], contracts: dict[str, Contract], imports: Iterable[str] = () ) -> KFlatModule: module_name = Contract.contract_to_module_name(contract.name_with_path) - return KFlatModule(module_name, contract.sentences(enums), [KImport(i) for i in list(imports)]) + return KFlatModule(module_name, contract.sentences(enums, contracts), [KImport(i) for i in list(imports)]) def contract_to_verification_module(contract: Contract, empty_config: KInner, imports: Iterable[str]) -> KFlatModule: From d5f2048e93ef752124945f924df9dcf299872705 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 30 Jul 2024 11:23:59 -0500 Subject: [PATCH 10/10] Test adding lemmas for simple types --- src/kontrol/__main__.py | 22 ++--- src/kontrol/solc_to_k.py | 84 ++++++++++++------- .../test-data/foundry/test/Mapping.t.sol | 32 +++---- 3 files changed, 80 insertions(+), 58 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index dec41412d..865add14f 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -189,17 +189,17 @@ def exec_build(options: BuildOptions) -> None: building_message = f'[{_rv_blue()}]:hammer: [bold]Building [{_rv_yellow()}]Kontrol[/{_rv_yellow()}] project[/bold] :hammer:[/{_rv_blue()}]' else: building_message = f'[{_rv_blue()}]:hammer: [bold]Building [{_rv_yellow()}]Kontrol[/{_rv_yellow()}] project[/bold] :hammer: \n Add `--verbose` to `kontrol build` for more details![/{_rv_blue()}]' - try: - console.print(building_message) - foundry_kompile( - options=options, - foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), - ) - console.print( - ':white_heavy_check_mark: [bold green]Success![/bold green] [bold]Kontrol project built[/bold] :muscle:' - ) - except Exception as e: - console.print(f'[bold red]An error occurred while building your Kontrol project:[/bold red] [black]{e}[/black]') +# try: + console.print(building_message) + foundry_kompile( + options=options, + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), + ) + console.print( + ':white_heavy_check_mark: [bold green]Success![/bold green] [bold]Kontrol project built[/bold] :muscle:' + ) +# except Exception as e: +# console.print(f'[bold red]An error occurred while building your Kontrol project:[/bold red] [black]{e}[/black]') def exec_prove(options: ProveOptions) -> None: diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 05f706e9d..429866076 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -17,8 +17,6 @@ from pyk.prelude.kbool import TRUE, andBool from pyk.prelude.kint import eqInt, intToken, ltInt from pyk.prelude.string import stringToken -from pyk.prelude.ml import mlEqualsTrue -from pyk.prelude.k import K_ITEM, GENERATED_TOP_CELL from pyk.utils import hash_str, run_process_2, single if TYPE_CHECKING: @@ -1076,19 +1074,19 @@ def get_contract(type_name: str) -> Contract: return contract_obj raise ValueError(f'Contract {type_name} not found.') - def gen_accounts_list(contract: Contract, contract_name: str) -> list[str]: - accounts_list: list[str] = [] + def gen_accounts_list(contract: Contract, contract_name: str) -> list[tuple[str, Contract]]: + accounts_list: list[tuple[str, Contract]] = [] for field in contract.fields: if field.data_type.name.startswith('contract '): field_name = f'C_{contract_name}_{field.label}'.upper() - accounts_list.append(field_name) contract_type = field.data_type.name.split(' ')[1] contract = get_contract(contract_type) + accounts_list.append((field_name, contract)) accounts_list += gen_accounts_list(contract=contract, contract_name=field_name) return accounts_list storage_prods: list[KSentence] = [] - for account_label in gen_accounts_list(self, self._name): + for account_label, contract_obj in gen_accounts_list(self, self._name): storage_prods.append( KProduction( KSort('Bool'), @@ -1142,6 +1140,24 @@ def gen_accounts_list(contract: Contract, contract_name: str) -> list[str]: ), ) ) + print(account_label) + print(contract_obj.fields) + for field in contract_obj.fields: + for key, type_name in field.data_type.preds(): + print(key) + rp = _range_predicate(term=KVariable('V'), type_label=type_name) + +# print(KRule(KRewrite(lhs=KApply( +# f's2k_entry_invariant_{account_label}' , [key, KVariable('V')]) , rhs=_range_predicate(term=KVariable('V'), type_label=type_name) +# ))) + +# if rp is not None: +# storage_prods.append(KRule(KRewrite(lhs=KApply( +# f's2k_entry_invariant_{account_label}' , [key, KVariable('V')]) , rhs=rp +# ))) +# field.data_type.compute_constraints() + print('---') + return storage_prods @@ -1484,17 +1500,21 @@ def preds(self) -> list[tuple[KInner, str]]: def pred_vars(self) -> list[KInner]: return [] - def compute_constraints(self, storage_map: KInner) -> list[KInner]: + def compute_constraints(self) -> list[KInner]: constraints: list[KInner] = [] - for pred, pred_type in self.preds(): - assert isinstance(pred, KApply) - constraint = _range_predicate(term=KEVM.lookup(storage_map, pred.args[1]), type_label=pred_type) - if constraint is not None: - constraint = mlEqualsTrue(constraint) - for pred_var in self.pred_vars(): - constraint = KLabel('#Forall', K_ITEM, GENERATED_TOP_CELL)(pred_var, constraint) - constraints.append(constraint) +# for pred, pred_type in self.preds(): +# constraints.append( +# KRule(KRewrite(lhs=)) +# ) +# print(pred, pred_type) +# assert isinstance(pred, KApply) +# constraint = _range_predicate(term=KEVM.lookup(storage_map, pred.args[1]), type_label=pred_type) +# if constraint is not None: +# constraint = mlEqualsTrue(constraint) +# for pred_var in self.pred_vars(): +# constraint = KLabel('#Forall', K_ITEM, GENERATED_TOP_CELL)(pred_var, constraint) +# constraints.append(constraint) return constraints @dataclass @@ -1512,23 +1532,25 @@ def pred_vars(self) -> list[KInner]: return list(self.pred_var) + self.val_type.pred_vars() def compute_preds(self, base_pred: KInner) -> None: - variable = KVariable('V_' + hash_str(base_pred)[0:8]) - self.pred_var = (variable,) - self.pred = base_pred - self.val_type.compute_preds( - KApply('buf', [intToken(32), - KApply('keccak', [ - KEVM.bytes_append( - variable, - base_pred, - ) - ]) - ]) - ) + ... +# variable = KVariable('V_' + hash_str(base_pred)[0:8]) +# self.pred_var = (variable,) +# self.pred = base_pred +# self.val_type.compute_preds( +# KApply('buf', [intToken(32), +# KApply('keccak', [ +# KEVM.bytes_append( +# variable, +# base_pred, +# ) +# ]) +# ]) +# ) def preds(self) -> list[tuple[KInner, str]]: - assert self.pred is not None - return [(self.pred, self.name)] + self.val_type.preds() +# assert self.pred is not None +# return [(self.pred, self.name)] + self.val_type.preds() + return [] @dataclass class StorageFieldStructType(StorageFieldType): @@ -1581,7 +1603,7 @@ def process_storage_layout(storage_layout: dict, interface_annotations: dict) -> try: storage_field = storage_field_from_dict(field, types, interface_annotations) fields_list.append(storage_field) - storage_field.data_type.compute_preds(KApply('buf', [intToken(32), intToken(storage_field.slot)])) + storage_field.data_type.compute_preds(intToken(storage_field.slot)) except (KeyError, ValueError) as e: _LOGGER.error(f'Error processing field {field}: {e}') diff --git a/src/tests/integration/test-data/foundry/test/Mapping.t.sol b/src/tests/integration/test-data/foundry/test/Mapping.t.sol index d9844e869..6df6fcf8e 100644 --- a/src/tests/integration/test-data/foundry/test/Mapping.t.sol +++ b/src/tests/integration/test-data/foundry/test/Mapping.t.sol @@ -5,35 +5,35 @@ import "forge-std/Test.sol"; import "kontrol-cheatcodes/KontrolCheats.sol"; contract MappingContract { - mapping(address => mapping(address => uint256)) public balances; - mapping(address => uint256) public single_map; - - function get_mapping_val(address a) public returns (uint256) { - return balances[a][a]; - } - - function get_mapping_val2(address a) public returns (uint256) { - return single_map[a]; - } + uint8 public smallint; +// mapping(address => mapping(address => uint256)) public balances; +// mapping(address => uint256) public single_map; + +// function get_mapping_val(address a) public returns (uint256) { +// return balances[a][a]; +// } +// +// function get_mapping_val2(address a) public returns (uint256) { +// return single_map[a]; +// } } contract MappingTest is Test { uint256 val; - uint256 val2; +// uint256 val2; MappingContract c; constructor() public { c = new MappingContract(); } - function my_internal() internal { } +// function my_internal() internal { } function test_mapping(address a) public { - val = c.get_mapping_val(a); - val2 = c.get_mapping_val2(a); - my_internal(); + val = c.smallint(); +// val2 = c.get_mapping_val2(a); +// my_internal(); assert(val < 256); - assert(val2 < 256); } }