Fixing incorrect passing proof reporting (#2024)

* Fixing incorrect passing proof reporting * Set Version: 1.0.264 * simplifications * one import fewer * Set Version: 1.0.265 * Set Version: 1.0.266 * Set Version: 1.0.267 * Set Version: 1.0.268 * Set Version: 1.0.269 * Set Version: 1.0.270 * Set Version: 1.0.271 * Set Version: 1.0.272 * Set Version: 1.0.273 * Set Version: 1.0.274 * correcting the resume_proof test * formatting --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]>
runtimeverification · Aug 23, 2023 · 1df6371 · 1df6371
1 parent 506821c
commit 1df6371
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 17 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.273"
+version = "1.0.274"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -21,7 +21,6 @@
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, kore_server
 from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver
 from pyk.proof.equality import EqualityProof, EqualityProver
-from pyk.proof.proof import ProofStatus
 from pyk.utils import single
 
 if TYPE_CHECKING:
@@ -125,38 +124,30 @@ def kevm_prove(
                 cut_point_rules=cut_point_rules,
             )
             assert isinstance(proof, APRProof)
-            failure_nodes = proof.failing
-            if len(failure_nodes) == 0:
+            if proof.passed:
                 _LOGGER.info(f'Proof passed: {proof.id}')
                 return True
             else:
                 _LOGGER.error(f'Proof failed: {proof.id}')
                 return False
         elif type(prover) is EqualityProver:
             prover.advance_proof()
-            if prover.proof.status == ProofStatus.PASSED:
+            if prover.proof.passed:
                 _LOGGER.info(f'Proof passed: {prover.proof.id}')
                 return True
-            if prover.proof.status == ProofStatus.FAILED:
+            elif prover.proof.failed:
                 _LOGGER.error(f'Proof failed: {prover.proof.id}')
                 if type(proof) is EqualityProof:
                     _LOGGER.info(proof.pretty(kprove))
                 return False
-            if prover.proof.status == ProofStatus.PENDING:
+            else:
                 _LOGGER.info(f'Proof pending: {prover.proof.id}')
                 return False
         return False
 
     except Exception as e:
         _LOGGER.error(f'Proof crashed: {proof.id}\n{e}', exc_info=True)
         return False
-    failure_nodes = proof.pending + proof.failing
-    if len(failure_nodes) == 0:
-        _LOGGER.info(f'Proof passed: {proof.id}')
-        return True
-    else:
-        _LOGGER.error(f'Proof failed: {proof.id}')
-        return False
 
 
 def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> list[str]:

diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py
@@ -328,7 +328,9 @@ 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) -> None:
+    foundry = Foundry(foundry_root)
     test_id = 'AssumeTest.test_assume_false(uint256,uint256)'
+
     prove_res = foundry_prove(
         foundry_root,
         tests=[test_id],
@@ -338,7 +340,10 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool)
         max_iterations=4,
         reinit=True,
     )
-    assert_pass(test_id, prove_res)
+
+    proof = foundry.get_apr_proof(test_id)
+    assert proof.pending
+
     prove_res = foundry_prove(
         foundry_root,
         tests=[test_id],

diff --git a/package/debian/changelog b/package/debian/changelog
@@ -1,4 +1,4 @@
-kevm (1.0.273) unstable; urgency=medium
+kevm (1.0.274) unstable; urgency=medium
 
   * Initial Release.
 

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.273
+1.0.274