fix: proof separate files (#1995)

* use new proof system

* Set Version: 1.0.249

* Change to proof_data_exists function in kevm prove

* Fix proof reading in _method_to_apr_proof and add test for proof resumption

* Fix formatting and typing

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Noah Watson <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.248"
+version = "1.0.249"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__main__.py

@@ -309,7 +309,11 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                 else:
                     proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory)
             else:
-                if save_directory is not None and not reinit and APRProof.proof_exists(claim.label, save_directory):
+                if (
+                    save_directory is not None
+                    and not reinit
+                    and APRProof.proof_data_exists(claim.label, save_directory)
+                ):
                     proof_problem = APRProof.read_proof_data(save_directory, claim.label)
 
                 else:

kevm-pyk/src/kevm_pyk/foundry.py

@@ -674,7 +674,7 @@ def foundry_list(foundry_root: Path) -> list[str]:
     for method in sorted(all_methods):
         contract_name, test_name = method.split('.')
         proof_digest = foundry.proof_digest(contract_name, test_name)
-        if APRProof.proof_exists(proof_digest, apr_proofs_dir):
+        if APRProof.proof_data_exists(proof_digest, apr_proofs_dir):
             apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
             lines.extend(apr_proof.summary.lines)
             lines.append('')
@@ -898,16 +898,9 @@ def _method_to_apr_proof(
     method_name = method.name
     test = f'{contract_name}.{method_name}'
     proof_digest = foundry.proof_digest(contract_name, method_name)
-    if Proof.proof_exists(proof_digest, save_directory) and not reinit:
-        proof_path = save_directory / f'{hash_str(proof_digest)}.json'
-        proof_dict = json.loads(proof_path.read_text())
-        match proof_dict['type']:
-            case 'APRProof':
-                apr_proof = APRProof.from_dict(proof_dict, proof_dir=save_directory)
-            case 'APRBMCProof':
-                apr_proof = APRBMCProof.from_dict(proof_dict, proof_dir=save_directory)
-            case unsupported_type:
-                raise ValueError(f'Unsupported proof type {unsupported_type}')
+    if Proof.proof_data_exists(proof_digest, save_directory) and not reinit:
+        apr_proof = Proof.read_proof_data(proof_dir=save_directory, id=proof_digest)
+        assert isinstance(apr_proof, APRProof)
     else:
         _LOGGER.info(f'Initializing KCFG for test: {test}')
 

kevm-pyk/src/tests/integration/test_foundry_prove.py

@@ -244,3 +244,27 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update:
         expected_file.write_text(actual_text)
     else:
         assert actual_text == expected_text
+
+
+def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) -> None:
+    test_id = 'AssumeTest.test_assume_false'
+    prove_res = foundry_prove(
+        foundry_root,
+        tests=[test_id],
+        smt_timeout=125,
+        smt_retry_limit=4,
+        auto_abstract_gas=True,
+        max_iterations=4,
+        reinit=True,
+    )
+    assert_pass(test_id, prove_res)
+    prove_res = foundry_prove(
+        foundry_root,
+        tests=[test_id],
+        smt_timeout=125,
+        smt_retry_limit=4,
+        auto_abstract_gas=True,
+        max_iterations=6,
+        reinit=False,
+    )
+    assert_fail(test_id, prove_res)

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.248) unstable; urgency=medium
+kevm (1.0.249) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.248
+1.0.249