Simplify returning of proof results (#114)

* Use Proof class to simplify returning of proof results * Set Version: 0.1.31 * Don't index by unhashable FoundryTest type * Fix test * Set Version: 0.1.33 * Fix test * Apply suggestions * Set Version: 0.1.34 * Set Version: 0.1.34 * Set Version: 0.1.35 * Set Version: 0.1.36 * Set Version: 0.1.37 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Oct 25, 2023 · e4f1d6e · e4f1d6e
1 parent cf5e56b
commit e4f1d6e
Show file tree

Hide file tree

Showing 6 changed files with 51 additions and 63 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.36
+0.1.37
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.36"
+version = "0.1.37"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git 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.36'
+VERSION: Final = '0.1.37'
diff --git 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
@@ -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
@@ -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))