diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 11f9d06bd3..97ba724e17 100644 --- 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.248" +version = "1.0.249" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 5089157557..30be74c755 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/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: diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py index 68f63e8a1f..c5c3b56f97 100644 --- a/kevm-pyk/src/kevm_pyk/foundry.py +++ b/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}') diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index 33a6bdd77e..441a80c764 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/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) diff --git a/package/debian/changelog b/package/debian/changelog index d29d9243bf..2fef431de3 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.248) unstable; urgency=medium +kevm (1.0.249) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e94c454622..fb8d264788 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.248 +1.0.249