Change to new proof read/write functions

runtimeverification · Jul 28, 2023 · 58b049b · 58b049b
1 parent decca7b
commit 58b049b
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 20 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -298,12 +298,12 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                     and not reinit
                     and EqualityProof.proof_exists(claim.label, save_directory)
                 ):
-                    proof_problem = EqualityProof.read_proof(claim.label, save_directory)
+                    proof_problem = EqualityProof.read_proof_data(save_directory, claim.label)
                 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):
-                    proof_problem = APRProof.read_proof(claim.label, save_directory)
+                    proof_problem = APRProof.read_proof_data(save_directory, claim.label)
 
                 else:
                     _LOGGER.info(f'Converting claim to KCFG: {claim.label}')
@@ -418,10 +418,10 @@ def exec_prune_proof(
         )
     )
 
-    apr_proof = APRProof.read_proof(claim.label, save_directory)
+    apr_proof = APRProof.read_proof_data(save_directory, claim.label)
     node_ids = apr_proof.kcfg.prune(node)
     _LOGGER.info(f'Pruned nodes: {node_ids}')
-    apr_proof.write_proof()
+    apr_proof.write_proof_data()
 
 
 def exec_show_kcfg(
@@ -661,7 +661,7 @@ def exec_foundry_view_kcfg(foundry_root: Path, test: str, **kwargs: Any) -> None
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
 
-    proof = APRProof.read_proof(proof_digest, proofs_dir)
+    proof = APRProof.read_proof_data(proofs_dir, proof_digest)
 
     def _short_info(cterm: CTerm) -> Iterable[str]:
         return foundry.short_info_for_contract(contract_name, cterm)

diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py
@@ -601,7 +601,7 @@ def foundry_show(
 
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    proof = Proof.read_proof(proof_digest, proofs_dir)
+    proof = Proof.read_proof_data(proofs_dir, proof_digest)
     assert isinstance(proof, APRProof)
 
     def _short_info(cterm: CTerm) -> Iterable[str]:
@@ -648,7 +648,7 @@ def foundry_to_dot(foundry_root: Path, test: str) -> None:
     dump_dir = proofs_dir / 'dump'
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    proof = APRProof.read_proof(proof_digest, proofs_dir)
+    proof = APRProof.read_proof_data(proofs_dir, proof_digest)
 
     node_printer = foundry_node_printer(foundry, contract_name, proof)
     proof_show = APRProofShow(foundry.kevm, node_printer=node_printer)
@@ -669,7 +669,7 @@ def foundry_list(foundry_root: Path) -> list[str]:
         contract_name, test_name = method.split('.')
         proof_digest = foundry.proof_digest(contract_name, test_name)
         if APRProof.proof_exists(proof_digest, apr_proofs_dir):
-            apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+            apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
             lines.extend(apr_proof.summary.lines)
             lines.append('')
     if len(lines) > 0:
@@ -683,10 +683,10 @@ def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike) -> None
     apr_proofs_dir = foundry.out / 'apr_proofs'
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+    apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
     node_ids = apr_proof.kcfg.prune(node, [apr_proof.init, apr_proof.target])
     _LOGGER.info(f'Pruned nodes: {node_ids}')
-    apr_proof.write_proof()
+    apr_proof.write_proof_data()
 
 
 def foundry_simplify_node(
@@ -706,7 +706,7 @@ def foundry_simplify_node(
     apr_proofs_dir = foundry.out / 'apr_proofs'
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+    apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
     cterm = apr_proof.kcfg.node(node).cterm
     with KCFGExplore(
         foundry.kevm,
@@ -720,7 +720,7 @@ def foundry_simplify_node(
         new_term, _ = kcfg_explore.cterm_simplify(cterm)
     if replace:
         apr_proof.kcfg.replace_node(node, CTerm.from_kast(new_term))
-        apr_proof.write_proof()
+        apr_proof.write_proof_data()
     res_term = minimize_term(new_term) if minimize else new_term
     return foundry.kevm.pretty_print(res_term, unalias=False, sort_collections=sort_collections)
 
@@ -747,7 +747,7 @@ def foundry_step_node(
     apr_proofs_dir = foundry.out / 'apr_proofs'
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+    apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
     with KCFGExplore(
         foundry.kevm,
         kcfg_semantics=KEVMSemantics(),
@@ -759,7 +759,7 @@ def foundry_step_node(
     ) as kcfg_explore:
         for _i in range(repeat):
             node = kcfg_explore.step(apr_proof.kcfg, node, apr_proof.logs, depth=depth)
-            apr_proof.write_proof()
+            apr_proof.write_proof_data()
 
 
 def foundry_section_edge(
@@ -778,7 +778,7 @@ def foundry_section_edge(
     apr_proofs_dir = foundry.out / 'apr_proofs'
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+    apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest)
     source_id, target_id = edge
     with KCFGExplore(
         foundry.kevm,
@@ -792,7 +792,7 @@ def foundry_section_edge(
         kcfg, _ = kcfg_explore.section_edge(
             apr_proof.kcfg, source_id=source_id, target_id=target_id, logs=apr_proof.logs, sections=sections
         )
-    apr_proof.write_proof()
+    apr_proof.write_proof_data()
 
 
 def foundry_get_model(
@@ -808,7 +808,7 @@ def foundry_get_model(
 
     contract_name, test_name = test.split('.')
     proof_digest = foundry.proof_digest(contract_name, test_name)
-    proof = Proof.read_proof(proof_digest, proofs_dir)
+    proof = Proof.read_proof_data(proofs_dir, proof_digest)
     assert isinstance(proof, APRProof)
 
     if not nodes:
@@ -939,7 +939,7 @@ def _method_to_apr_proof(
         else:
             apr_proof = APRProof(proof_digest, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory)
 
-    apr_proof.write_proof()
+    apr_proof.write_proof_data()
     return apr_proof
 
 
@@ -967,7 +967,7 @@ def _method_to_cfg(
 
 
 def get_final_accounts_cell(proof_digest: str, proof_dir: Path) -> tuple[KInner, Iterable[KInner]]:
-    apr_proof = APRProof.read_proof(proof_digest, proof_dir)
+    apr_proof = APRProof.read_proof_data(proof_dir, proof_digest)
     target = apr_proof.kcfg.node(apr_proof.target)
     cterm = single(apr_proof.kcfg.covers(target_id=target.id)).source.cterm
     acct_cell = cterm.cell('ACCOUNTS_CELL')

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -63,7 +63,7 @@ def get_apr_proof_for_spec(  # noqa: N802
         )
     )
 
-    apr_proof = APRProof.read_proof(claim.label, save_directory)
+    apr_proof = APRProof.read_proof_data(save_directory, claim.label)
     return apr_proof