diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 929119965..65aca5123 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -10,6 +10,7 @@ from kevm_pyk.cli import node_id_like from kevm_pyk.utils import arg_pair_of from pyk.cli.utils import file_path +from pyk.proof.reachability import APRProof from pyk.proof.tui import APRProofViewer from . import VERSION @@ -203,16 +204,18 @@ def exec_prove( tests=tests, ) failed = 0 - for pid, r in results.items(): - passed, failure_log = r - if passed: - print(f'PROOF PASSED: {pid}') + for proof in results: + if proof.passed: + print(f'PROOF PASSED: {proof.id}') else: failed += 1 - print(f'PROOF FAILED: {pid}') + print(f'PROOF FAILED: {proof.id}') + failure_log = None + if isinstance(proof, APRProof): + failure_log = proof.failure_info if failure_info and failure_log is not None: - failure_log += Foundry.help_info() - for line in failure_log: + log = failure_log.print() + Foundry.help_info() + for line in log: print(line) sys.exit(failed) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 6de58d587..e00a161e0 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -5,13 +5,7 @@ from typing import TYPE_CHECKING, NamedTuple from kevm_pyk.kevm import KEVM, KEVMSemantics -from kevm_pyk.utils import ( - KDefinition__expand_macros, - abstract_cell_vars, - kevm_prove, - legacy_explore, - print_failure_info, -) +from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, kevm_prove, legacy_explore from pathos.pools import ProcessPool # type: ignore from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence, KVariable, Subst @@ -46,7 +40,7 @@ def foundry_prove( foundry_root: Path, options: ProveOptions, tests: Iterable[tuple[str, int | None]] = (), -) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: +) -> list[Proof]: if options.workers <= 0: raise ValueError(f'Must have at least one worker, found: --workers {options.workers}') if options.max_iterations is not None and options.max_iterations < 0: @@ -89,7 +83,7 @@ def foundry_prove( for test in constructor_tests: test.method.update_digest(foundry.digest_file) - def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: + def run_prover(test_suite: list[FoundryTest]) -> list[Proof]: return _run_cfg_group( tests=test_suite, foundry=foundry, @@ -99,14 +93,14 @@ def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[boo if options.run_constructor: _LOGGER.info(f'Running initialization code for contracts in parallel: {constructor_names}') results = run_prover(constructor_tests) - failed = [init_cfg for init_cfg, passed in results.items() if not passed] + failed = [proof for proof in results if not proof.passed] if failed: raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}') _LOGGER.info(f'Running setup functions in parallel: {setup_method_names}') results = run_prover(setup_method_tests) - failed = [setup_cfg for setup_cfg, passed in results.items() if not passed] + failed = [proof for proof in results if not proof.passed] if failed: raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}') @@ -182,10 +176,9 @@ def _run_cfg_group( tests: list[FoundryTest], foundry: Foundry, options: ProveOptions, -) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: - def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: +) -> list[Proof]: + def init_and_run_proof(test: FoundryTest) -> Proof: start_server = options.port is None - with legacy_explore( foundry.kevm, kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), @@ -207,7 +200,7 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: run_constructor=options.run_constructor, ) - passed = kevm_prove( + kevm_prove( foundry.kevm, proof, kcfg_explore, @@ -217,22 +210,17 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: break_on_jumpi=options.break_on_jumpi, break_on_calls=options.break_on_calls, ) - failure_log = None - if not passed: - failure_log = print_failure_info(proof, kcfg_explore, options.counterexample_info) - return passed, failure_log + return proof - _apr_proofs: list[tuple[bool, list[str] | None]] + apr_proofs: list[Proof] if options.workers > 1: with ProcessPool(ncpus=options.workers) as process_pool: - _apr_proofs = process_pool.map(init_and_run_proof, tests) + apr_proofs = process_pool.map(init_and_run_proof, tests) else: - _apr_proofs = [] + apr_proofs = [] for test in tests: - _apr_proofs.append(init_and_run_proof(test)) + apr_proofs.append(init_and_run_proof(test)) - unparsed_tests = [test.unparsed for test in tests] - apr_proofs = dict(zip(unparsed_tests, _apr_proofs, strict=True)) return apr_proofs diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 4f755dc9b..6dd326c1b 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -23,6 +23,7 @@ from typing import Final from pyk.kore.rpc import KoreServer + from pyk.proof.proof import Proof from pyk.utils import BugReport from pytest import TempPathFactory @@ -138,7 +139,7 @@ def test_foundry_prove( ) # Then - assert_pass(test_id, prove_res) + assert_pass(test_id, single(prove_res)) if test_id not in SHOW_TESTS or use_booster: return @@ -185,7 +186,7 @@ def test_foundry_fail( ) # Then - assert_fail(test_id, prove_res) + assert_fail(test_id, single(prove_res)) if test_id not in SHOW_TESTS or use_booster: return @@ -229,7 +230,7 @@ def test_foundry_bmc(test_id: str, foundry_root: Path, bug_report: BugReport | N ) # Then - assert_pass(test_id, prove_res) + assert_pass(test_id, single(prove_res)) def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, server: KoreServer) -> None: @@ -264,7 +265,7 @@ def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, s bug_report=bug_report, ), ) - assert_pass(test, prove_res) + assert_pass(test, single(prove_res)) def check_pending(foundry_root: Path, test: str, pending: list[int]) -> None: @@ -327,7 +328,7 @@ def test_foundry_remove_node( bug_report=bug_report, ), ) - assert_pass(test, prove_res) + assert_pass(test, single(prove_res)) foundry_remove_node( foundry_root=foundry_root, @@ -347,26 +348,22 @@ def test_foundry_remove_node( bug_report=bug_report, ), ) - assert_pass(test, prove_res) + assert_pass(test, single(prove_res)) -def assert_pass(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> None: - id = id_for_test(test, prove_res) - passed, log = prove_res[(test, id)] - if not passed: - assert log - pytest.fail('\n'.join(log)) +def assert_pass(test: str, proof: Proof) -> None: + if not proof.passed: + if isinstance(proof, APRProof): + assert proof.failure_info + pytest.fail('\n'.join(proof.failure_info.print())) + else: + pytest.fail() -def assert_fail(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> None: - id = id_for_test(test, prove_res) - passed, log = prove_res[test, id] - assert not passed - assert log - - -def id_for_test(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> int: - return single(_id for _test, _id in prove_res.keys() if _test == test and _id is not None) +def assert_fail(test: str, proof: Proof) -> None: + assert not proof.passed + if isinstance(proof, APRProof): + assert proof.failure_info def assert_or_update_show_output(show_res: str, expected_file: Path, *, update: bool) -> None: @@ -397,7 +394,6 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update: def test_foundry_resume_proof( foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None, server: KoreServer ) -> None: - foundry = Foundry(foundry_root) test = 'AssumeTest.test_assume_false(uint256,uint256)' prove_res = foundry_prove( @@ -411,23 +407,24 @@ def test_foundry_resume_proof( bug_report=bug_report, ), ) - id = id_for_test(test, prove_res) - proof = foundry.get_apr_proof(f'{test}:{id}') + proof = single(prove_res) + assert isinstance(proof, APRProof) assert proof.pending prove_res = foundry_prove( foundry_root, - tests=[(test, id)], + tests=[(test, None)], options=ProveOptions( auto_abstract_gas=True, - max_iterations=6, + max_iterations=10, reinit=False, port=server.port, bug_report=bug_report, ), ) - assert_fail(test, prove_res) + + assert_fail(test, single(prove_res)) ALL_INIT_CODE_TESTS: Final = ('InitCodeTest.test_init()', 'InitCodeTest.testFail_init()') @@ -449,4 +446,4 @@ def test_foundry_init_code(test: str, foundry_root: Path, bug_report: BugReport ) # Then - assert_pass(test, prove_res) + assert_pass(test, single(prove_res))