diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 91c917cb23..40c7d6c01c 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.327" +version = "1.0.328" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d27ad28287..90c6120254 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/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' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 3df8f0ec30..1252f265f1 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -1,11 +1,10 @@ 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 @@ -13,32 +12,22 @@ 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,25 +248,31 @@ 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, @@ -283,65 +280,17 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: 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) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 7ad3f39259..889ad40578 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/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 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 diff --git a/package/version b/package/version index 6698d2ca16..6300eb8079 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.327 +1.0.328