Enable using proof heirarchy from depends clauses

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.327'
+VERSION: Final = '1.0.328'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -1,44 +1,33 @@
 from __future__ import annotations
 
 import contextlib
-import graphlib
 import json
 import logging
-import os
 import sys
+import tempfile
 import time
 from argparse import ArgumentParser
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pathos.pools import ProcessPool  # type: ignore
 from pyk.cli.utils import file_path
-from pyk.cterm import CTerm
 from pyk.kast.outer import KApply, KRewrite, KSort, KToken
-from pyk.kcfg import KCFG
 from pyk.kore.tools import PrintOutput, kore_print
 from pyk.ktool.kompile import LLVMKompileType
 from pyk.ktool.krun import KRunOutput
 from pyk.prelude.ml import is_top, mlOr
-from pyk.proof import APRProof
-from pyk.proof.equality import EqualityProof
+from pyk.proof import APRProof, ProofStatus
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
-from pyk.utils import single
+from pyk.utils import single, unique
 
 from . import VERSION, config, kdist
 from .cli import KEVMCLIArgs, node_id_like
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
-from .utils import (
-    claim_dependency_dict,
-    ensure_ksequence_on_k_cell,
-    get_apr_proof_for_spec,
-    kevm_prove,
-    legacy_explore,
-    print_failure_info,
-)
+from .utils import get_apr_proof_for_spec, kevm_prove, legacy_explore, print_failure_info
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -47,7 +36,6 @@
 
     from pyk.kast.outer import KClaim
     from pyk.kcfg.kcfg import NodeIdLike
-    from pyk.proof.proof import Proof
     from pyk.utils import BugReport
 
     T = TypeVar('T')
@@ -238,6 +226,9 @@ def exec_prove(
     if smt_retry_limit is None:
         smt_retry_limit = 10
 
+    if save_directory is None:
+        save_directory = Path(tempfile.TemporaryDirectory().name)
+
     kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report)
 
     include_dirs = [Path(include) for include in includes]
@@ -257,91 +248,49 @@ def is_functional(claim: KClaim) -> bool:
     llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None
 
     _LOGGER.info(f'Extracting claims from file: {spec_file}')
-    all_claims = kevm.get_claims(
-        spec_file,
-        spec_module_name=spec_module,
-        include_dirs=include_dirs,
-        md_selector=md_selector,
-        claim_labels=None,
-        exclude_claim_labels=exclude_claim_labels,
+    spec_modules = kevm.get_claim_modules(
+        spec_file, spec_module_name=spec_module, include_dirs=include_dirs, md_selector=md_selector
     )
-    if all_claims is None:
-        raise ValueError(f'No claims found in file: {spec_file}')
-    all_claims_by_label: dict[str, KClaim] = {c.label: c for c in all_claims}
-    spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper()
-    claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name)
-
-    def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
+    proofs = APRProof.from_spec_modules(
+        kevm.definition, spec_modules, spec_labels=claim_labels, logs={}, proof_dir=save_directory
+    )
+    proofs = list(unique(proofs))
+
+    def _init_and_run_proof(proof_id: str) -> tuple[bool, list[str] | None]:
+        proof = APRProof.read_proof_data(save_directory, proof_id)
+        if proof.passed:
+            _LOGGER.info(f'Proof already passed, skipping: {proof.id}')
+            return True, None
+        if proof.failed:
+            _LOGGER.info(f'Proof already failed, skipping: {proof.id}')
+            return False, None
+        while proof.subproofs_status == ProofStatus.PENDING:
+            pending_subproofs = [subproof.id for subproof in proof.subproofs if subproof.status == ProofStatus.PENDING]
+            _LOGGER.info(f'Waiting for subproofs to complete {proof.id}: {pending_subproofs}')
+            time.sleep(10)
+            proof = APRProof.read_proof_data(save_directory, proof_id)
         with legacy_explore(
             kevm,
             kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas),
-            id=claim.label,
+            id=proof.id,
             llvm_definition_dir=llvm_definition_dir,
             bug_report=bug_report,
             kore_rpc_command=kore_rpc_command,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             trace_rewrites=trace_rewrites,
         ) as kcfg_explore:
-            proof_problem: Proof
-            if is_functional(claim):
-                if (
-                    save_directory is not None
-                    and not reinit
-                    and EqualityProof.proof_exists(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_data_exists(claim.label, save_directory)
-                ):
-                    proof_problem = APRProof.read_proof_data(save_directory, claim.label)
-
-                else:
-                    _LOGGER.info(f'Converting claim to KCFG: {claim.label}')
-                    kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim)
-
-                    new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm)
-                    new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm)
-
-                    _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}')
-                    new_init = kcfg_explore.cterm_assume_defined(new_init)
-
-                    if simplify_init:
-                        _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
-                        new_init, _ = kcfg_explore.cterm_simplify(new_init)
-                        new_target, _ = kcfg_explore.cterm_simplify(new_target)
-                        if CTerm._is_bottom(new_init.kast):
-                            raise ValueError(
-                                'Simplifying initial node led to #Bottom, are you sure your LHS is defined?'
-                            )
-                        if CTerm._is_top(new_target.kast):
-                            raise ValueError(
-                                'Simplifying target node led to #Bottom, are you sure your RHS is defined?'
-                            )
-
-                    kcfg.replace_node(init_node_id, new_init)
-                    kcfg.replace_node(target_node_id, new_target)
-
-                    proof_problem = APRProof(
-                        claim.label,
-                        kcfg,
-                        [],
-                        init_node_id,
-                        target_node_id,
-                        {},
-                        proof_dir=save_directory,
-                        subproof_ids=claims_graph[claim.label],
-                    )
-
             start_time = time.time()
+            if len(proof.kcfg.successors(proof.init)) == 0:
+                new_init_cterm, _ = kcfg_explore.cterm_simplify(proof.kcfg.node(proof.init).cterm)
+                new_init_cterm = kcfg_explore.cterm_assume_defined(new_init_cterm)
+                new_target_cterm, _ = kcfg_explore.cterm_simplify(proof.kcfg.node(proof.target).cterm)
+                proof.kcfg.replace_node(proof.init, new_init_cterm)
+                proof.kcfg.replace_node(proof.target, new_target_cterm)
+                proof.write_proof_data()
             passed = kevm_prove(
                 kevm,
-                proof_problem,
+                proof,
                 kcfg_explore,
                 max_depth=max_depth,
                 max_iterations=max_iterations,
@@ -351,36 +300,21 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                 fail_fast=fail_fast,
             )
             end_time = time.time()
-            _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')
-            failure_log = None
-            if not passed:
-                failure_log = print_failure_info(proof_problem, kcfg_explore)
-
+            _LOGGER.info(f'Proof timing {proof.id}: {end_time - start_time}s')
+            failure_log = None if not passed else print_failure_info(proof, kcfg_explore)
             return passed, failure_log
 
-    topological_sorter = graphlib.TopologicalSorter(claims_graph)
-    topological_sorter.prepare()
     with wrap_process_pool(workers=workers) as process_pool:
-        selected_results: list[tuple[bool, list[str] | None]] = []
-        selected_claims = []
-        while topological_sorter.is_active():
-            ready = topological_sorter.get_ready()
-            _LOGGER.info(f'Discharging proof obligations: {ready}')
-            curr_claim_list = [all_claims_by_label[label] for label in ready]
-            results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list)
-            for label in ready:
-                topological_sorter.done(label)
-            selected_results.extend(results)
-            selected_claims.extend(curr_claim_list)
+        results = process_pool.map(_init_and_run_proof, [proof.id for proof in proofs])
 
     failed = 0
-    for claim, r in zip(selected_claims, selected_results, strict=True):
+    for proof, r in zip(proofs, results, strict=True):
         passed, failure_log = r
         if passed:
-            print(f'PROOF PASSED: {claim.label}')
+            print(f'PROOF PASSED: {proof.id}')
         else:
             failed += 1
-            print(f'PROOF FAILED: {claim.label}')
+            print(f'PROOF FAILED: {proof.id}')
             if failure_info and failure_log is not None:
                 for line in failure_log:
                     print(line)

kevm-pyk/src/kevm_pyk/utils.py

@@ -5,18 +5,15 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KInner, KRewrite, KVariable, Subst
 from pyk.kast.manip import (
     abstract_term_safely,
     bottom_up,
     free_vars,
     is_anon_var,
-    set_cell,
     split_config_and_constraints,
     split_config_from,
 )
-from pyk.kast.outer import KSequence
 from pyk.kcfg import KCFGExplore
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, kore_server
 from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver
@@ -27,7 +24,8 @@
     from collections.abc import Callable, Collection, Iterable, Iterator
     from typing import Final, TypeVar
 
-    from pyk.kast.outer import KClaim, KDefinition
+    from pyk.cterm import CTerm
+    from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFG
     from pyk.kcfg.semantics import KCFGSemantics
     from pyk.ktool.kprint import KPrint
@@ -41,24 +39,6 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-def claim_dependency_dict(claims: Iterable[KClaim], spec_module_name: str | None = None) -> dict[str, list[str]]:
-    claims_by_label = {claim.label: claim for claim in claims}
-    graph: dict[str, list[str]] = {}
-    for claim in claims:
-        graph[claim.label] = []
-        for dependency in claim.dependencies:
-            if dependency not in claims_by_label:
-                if spec_module_name is None:
-                    raise ValueError(f'Could not find dependency and no spec_module provided: {dependency}')
-                else:
-                    spec_dependency = f'{spec_module_name}.{dependency}'
-                    if spec_dependency not in claims_by_label:
-                        raise ValueError(f'Could not find dependency: {dependency} or {spec_dependency}')
-                    dependency = spec_dependency
-            graph[claim.label].append(dependency)
-    return graph
-
-
 def get_apr_proof_for_spec(
     kprove: KProve,
     spec_file: Path,
@@ -295,14 +275,6 @@ def abstract_cell_vars(cterm: KInner, keep_vars: Collection[KVariable] = ()) ->
     return Subst(subst)(config)
 
 
-def ensure_ksequence_on_k_cell(cterm: CTerm) -> CTerm:
-    k_cell = cterm.cell('K_CELL')
-    if type(k_cell) is not KSequence:
-        _LOGGER.info('Introducing artificial KSequence on <k> cell.')
-        return CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence([k_cell])))
-    return cterm
-
-
 def constraints_for(vars: list[str], constraints: Iterable[KInner]) -> Iterable[KInner]:
     accounts_constraints = []
     constraints_changed = True

package/version

@@ -1 +1 @@
-1.0.327
+1.0.328