Simplify returning of proof results

package/version

@@ -1 +1 @@
-0.1.32
+0.1.33

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.32"
+version = "0.1.33"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.32'
+VERSION: Final = '0.1.33'

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
@@ -197,16 +198,18 @@ def exec_prove(
         run_constructor=run_constructor,
     )
     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)

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
@@ -63,7 +57,7 @@ def foundry_prove(
     auto_abstract_gas: bool = False,
     port: int | None = None,
     run_constructor: bool = False,
-) -> dict[tuple[str, int], tuple[bool, list[str] | None]]:
+) -> list[Proof]:
     if workers <= 0:
         raise ValueError(f'Must have at least one worker, found: --workers {workers}')
     if max_iterations is not None and max_iterations < 0:
@@ -107,7 +101,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(
             test_suite,
             foundry,
@@ -133,14 +127,14 @@ def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[boo
     if 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}')
 
@@ -233,8 +227,8 @@ def _run_cfg_group(
     auto_abstract_gas: bool,
     port: int | None,
     run_constructor: bool = False,
-) -> 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:
         llvm_definition_dir = foundry.llvm_library if use_booster else None
         start_server = port is None
 
@@ -259,7 +253,7 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]:
                 run_constructor=run_constructor,
             )
 
-            passed = kevm_prove(
+            kevm_prove(
                 foundry.kevm,
                 proof,
                 kcfg_explore,
@@ -269,22 +263,17 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]:
                 break_on_jumpi=break_on_jumpi,
                 break_on_calls=break_on_calls,
             )
-            failure_log = None
-            if not passed:
-                failure_log = print_failure_info(proof, kcfg_explore, counterexample_info)
-            return passed, failure_log
+            return proof
 
-    _apr_proofs: list[tuple[bool, list[str] | None]]
+    apr_proofs: list[Proof]
     if workers > 1:
         with ProcessPool(ncpus=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
 
 

src/tests/integration/test_foundry_prove.py

@@ -22,6 +22,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
 
@@ -327,23 +328,21 @@ def test_foundry_remove_node(
     assert_pass(test, 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, prove_res: list[Proof]) -> None:
+    proof = single([proof for proof in prove_res if proof.id.split(':')[0] == test])
+    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, prove_res: list[Proof]) -> None:
+    proof = single([proof for proof in prove_res if proof.id.split(':')[0] == test])
+    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:
@@ -386,20 +385,20 @@ def test_foundry_resume_proof(
         port=server.port,
         bug_report=bug_report,
     )
-    id = id_for_test(test, prove_res)
 
-    proof = foundry.get_apr_proof(f'{test}:{id}')
+    proof = foundry.get_apr_proof(f'{single(prove_res).id}')
     assert proof.pending
 
     prove_res = foundry_prove(
         foundry_root,
-        tests=[(test, id)],
+        tests=[(test, None)],
         auto_abstract_gas=True,
-        max_iterations=6,
+        max_iterations=10,
         reinit=False,
         port=server.port,
         bug_report=bug_report,
     )
+
     assert_fail(test, prove_res)