diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index a606d0224..be47693cc 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -191,17 +191,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/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 4e30aa2c4..2520fd3f2 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, @@ -1065,9 +1130,18 @@ 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.startswith('enum'): - enum_name = field.data_type.split(' ')[1] + if field.data_type.name.startswith('enum'): + enum_name = field.data_type.name.split(' ')[1] if enum_name not in foundry.enums: _LOGGER.warning( f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.' @@ -1083,7 +1157,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( @@ -1107,7 +1181,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 @@ -1120,11 +1194,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 @@ -1205,6 +1279,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 8fb56daba..d5546d1f5 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -48,7 +48,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', [], @@ -337,7 +337,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 @@ -1082,8 +1082,105 @@ 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[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() + 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, contract_obj 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')]), + ], + ), + ) + ) + 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 + + 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]: @@ -1149,10 +1246,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: @@ -1404,6 +1501,114 @@ 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) -> list[KInner]: + + constraints: list[KInner] = [] +# 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 +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', [ +# 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() + return [] + +@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 _contract_name_from_bytecode( bytecode: bytes, contracts: dict[str, tuple[str, list[tuple[int, int]], list[tuple[int, int]]]] @@ -1434,15 +1639,9 @@ 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) + 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 new file mode 100644 index 000000000..6df6fcf8e --- /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 { + 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; + MappingContract c; + + constructor() public { + c = new MappingContract(); + } + +// function my_internal() internal { } + + function test_mapping(address a) public { + val = c.smallint(); +// val2 = c.get_mapping_val2(a); +// my_internal(); + assert(val < 256); + } + +}