diff --git a/flake.lock b/flake.lock index 7b62b32196..8643333d5f 100644 --- a/flake.lock +++ b/flake.lock @@ -529,16 +529,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1710160021, - "narHash": "sha256-gBJknRgcc7NP7b5wAsu2S/YlF/XpRxSEmV7OAE133bM=", + "lastModified": 1709926220, + "narHash": "sha256-8f4tkKi2p/Oj7gpOZ09sozYbk3766URN4b/Qj61MD5c=", "owner": "runtimeverification", "repo": "pyk", - "rev": "e243908892fa1d959743cd24dd9ff4a7b9efad00", + "rev": "89d0c0270836df0420918bceec463aaf0986f436", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.694", + "ref": "noah/default-options", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index e8e7b7e9ff..da251c972c 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/pyk/v0.1.694"; + pyk.url = "github:runtimeverification/pyk/noah/default-options"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; blockchain-k-plugin = { diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 32018bec9e..98023a16ab 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.694" +version = "0.1.692" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.694" -resolved_reference = "e243908892fa1d959743cd24dd9ff4a7b9efad00" +reference = "noah/default-options" +resolved_reference = "89d0c0270836df0420918bceec463aaf0986f436" [[package]] name = "pyperclip" @@ -1116,4 +1116,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "4c3c1e6022582589cd65a2a2d807ce6e33b388fd16c6af0d334bca0164f97cb9" +content-hash = "a0691f5001072ff9b3bd87d11d453206d425029f5c535fb89b0e43a4e0952566" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index dd0e13071b..91ec1a4689 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.492" +version = "1.0.493" description = "" authors = [ "Runtime Verification, Inc. ", @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.694" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 176f3a8fa4..f40b3d75c4 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.492' +VERSION: Final = '1.0.493' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 4944e8e588..1f6e54e80c 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -8,13 +8,22 @@ import sys import tempfile import time -from argparse import ArgumentParser from dataclasses import dataclass from functools import cached_property from pathlib import Path from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore +from pyk.cli.args import ( + BugReportOptions, + KompileOptions, + LoggingOptions, + ParallelOptions, + SaveDirOptions, + SMTOptions, + SpecOptions, +) +from pyk.cli.cli import CLI, Command from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken @@ -24,14 +33,23 @@ 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.implies import EqualityProof +from pyk.proof.reachability import APRProof from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer from pyk.utils import FrozenDict, hash_str, single from . import VERSION, config -from .cli import KEVMCLIArgs, node_id_like +from .cli import ( + EVMChainOptions, + ExploreOptions, + KEVMDisplayOptions, + KOptions, + KProveLegacyOptions, + KProveOptions, + RPCOptions, + TargetOptions, +) 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 @@ -46,16 +64,14 @@ ) if TYPE_CHECKING: - from argparse import Namespace + from argparse import ArgumentParser from collections.abc import Callable, Iterable, Iterator from typing import Any, Final, TypeVar from pyk.kast.outer import KClaim from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem - from pyk.kore.rpc import FallbackReason from pyk.proof.proof import Proof - from pyk.utils import BugReport T = TypeVar('T') @@ -72,128 +88,205 @@ def _ignore_arg(args: dict[str, Any], arg: str, cli_option: str) -> None: def main() -> None: sys.setrecursionlimit(15000000) - parser = _create_argument_parser() - args = parser.parse_args() - logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) - - executor_name = 'exec_' + args.command.lower().replace('-', '_') - if executor_name not in globals(): - raise AssertionError(f'Unimplemented command: {args.command}') - - execute = globals()[executor_name] - execute(**vars(args)) - - -# Command implementation - - -def exec_version(**kwargs: Any) -> None: - print(f'KEVM Version: {VERSION}') - - -def exec_kompile_spec( - output_dir: Path | None, - main_file: Path, - emit_json: bool, - includes: list[str], - main_module: str | None, - syntax_module: str | None, - target: KompileTarget | None = None, - read_only: bool = False, - ccopts: Iterable[str] = (), - o0: bool = False, - o1: bool = False, - o2: bool = False, - o3: bool = False, - enable_llvm_debug: bool = False, - llvm_library: bool = False, - debug_build: bool = False, - debug: bool = False, - verbose: bool = False, - **kwargs: Any, -) -> None: - if target is None: - target = KompileTarget.HASKELL - - if target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: - raise ValueError(f'Can only call kevm kompile-spec with --target [haskell,maude], got: {target.value}') - - output_dir = output_dir or Path() - - optimization = 0 - if o1: - optimization = 1 - if o2: - optimization = 2 - if o3: - optimization = 3 - if debug_build: - optimization = 0 - kevm_kompile( - target, - output_dir=output_dir, - main_file=main_file, - main_module=main_module, - syntax_module=syntax_module, - includes=includes, - emit_json=emit_json, - read_only=read_only, - ccopts=ccopts, - optimization=optimization, - enable_llvm_debug=enable_llvm_debug, - llvm_kompile_type=LLVMKompileType.C if llvm_library else LLVMKompileType.MAIN, - debug_build=debug_build, - debug=debug, - verbose=verbose, + kevm_cli = CLI( + ( + KastCommand, + KompileSpecCommand, + ProveLegacyCommand, + ProveCommand, + PruneCommand, + RunCommand, + ShowKCFGCommand, + VersionCommand, + ViewKCFGCommand, + ) ) + command = kevm_cli.get_command() + assert isinstance(command, LoggingOptions) + logging.basicConfig(level=_loglevel(command), format=_LOG_FORMAT) + command.exec() + + +class KompileSpecCommand(Command, KOptions, KompileOptions, LoggingOptions): + main_file: Path + target: KompileTarget + output_dir: Path + debug_build: bool + + @staticmethod + def name() -> str: + return 'kompile-spec' + + @staticmethod + def help_str() -> str: + return 'Kompile KEVM specification.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'debug_build': False, + 'output_dir': Path(), + 'target': KompileTarget.HASKELL, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('main_file', type=file_path, help='Path to file with main module.') + parser.add_argument('--target', type=KompileTarget, help='[haskell|maude]') + parser.add_argument( + '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' + ) + parser.add_argument('--debug-build', dest='debug_build', help='Enable debug symbols in LLVM builds.') + def exec(self) -> None: + if self.target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: + raise ValueError(f'Can only call kevm kompile-spec with --target [haskell,maude], got: {self.target.value}') -def exec_prove_legacy( - spec_file: Path, - definition_dir: Path | None = None, - includes: Iterable[str] = (), - bug_report_legacy: bool = False, - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - debug: bool = False, - debugger: bool = False, - max_depth: int | None = None, - max_counterexamples: int | None = None, - branching_allowed: int | None = None, - haskell_backend_args: Iterable[str] = (), - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') - - if definition_dir is None: - definition_dir = kdist.get('evm-semantics.haskell') - - kevm = KEVM(definition_dir, use_directory=save_directory) - - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - - final_state = kevm.prove_legacy( - spec_file=spec_file, - includes=include_dirs, - bug_report=bug_report_legacy, - spec_module=spec_module, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, - debug=debug, - debugger=debugger, - max_depth=max_depth, - max_counterexamples=max_counterexamples, - branching_allowed=branching_allowed, - haskell_backend_args=haskell_backend_args, - ) - final_kast = mlOr([state.kast for state in final_state]) - print(kevm.pretty_print(final_kast)) - if not is_top(final_kast): - raise SystemExit(1) + optimization = 0 + if self.o1: + optimization = 1 + if self.o2: + optimization = 2 + if self.o3: + optimization = 3 + if self.debug_build: + optimization = 0 + + kevm_kompile( + self.target, + output_dir=self.output_dir, + main_file=self.main_file, + main_module=self.main_module, + syntax_module=self.syntax_module, + includes=self.includes, + emit_json=self.emit_json, + read_only=self.read_only, + ccopts=self.ccopts, + optimization=optimization, + enable_llvm_debug=self.enable_llvm_debug, + llvm_kompile_type=LLVMKompileType.C if self.llvm_library else LLVMKompileType.MAIN, + debug_build=self.debug_build, + debug=self.debug, + verbose=self.verbose, + ) + + +class ShowKCFGCommand(Command, KOptions, SpecOptions, KEVMDisplayOptions, LoggingOptions): + nodes: list[NodeIdLike] + node_deltas: list[tuple[NodeIdLike, NodeIdLike]] + failure_info: bool + to_module: bool + pending: bool + failing: bool + counterexample_info: bool + + @staticmethod + def name() -> str: + return 'show-kcfg' + + @staticmethod + def help_str() -> str: + return 'Print the CFG for a given proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'failure_info': False, + 'to_module': False, + 'pending': False, + 'failing': False, + 'counterexample_info': False, + 'nodes': [], + 'node_deltas': [], + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--node', + type=node_id_like, + dest='nodes', + action='append', + help='List of nodes to display as well.', + ) + parser.add_argument( + '--node-delta', + type=arg_pair_of(node_id_like, node_id_like), + dest='node_deltas', + action='append', + help='List of nodes to display delta for.', + ) + parser.add_argument( + '--failure-information', + dest='failure_info', + action='store_true', + help='Show failure summary for cfg', + ) + parser.add_argument( + '--no-failure-information', + dest='failure_info', + action='store_false', + help='Do not show failure summary for cfg', + ) + parser.add_argument('--to-module', dest='to_module', action='store_true', help='Output edges as a K module.') + parser.add_argument('--pending', dest='pending', action='store_true', help='Also display pending nodes') + parser.add_argument('--failing', dest='failing', action='store_true', help='Also display failing nodes') + parser.add_argument( + '--counterexample-information', + dest='counterexample_info', + action='store_true', + help="Show models for failing nodes. Should be called with the '--failure-information' flag", + ) + + def exec(self) -> None: + if self.definition_dir is None: + raise ValueError('Must pass --definition to show-kcfg!') + + kevm = KEVM(self.definition_dir) + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + proof = get_apr_proof_for_spec( + kevm, + self.spec_file, + save_directory=self.save_directory, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=self.md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) + + nodes = [] + if self.pending: + nodes = list(self.nodes) + [node.id for node in proof.pending] + if self.failing: + nodes = list(self.nodes) + [node.id for node in proof.failing] + + node_printer = kevm_node_printer(kevm, proof) + proof_show = APRProofShow(kevm, node_printer=node_printer) + + res_lines = proof_show.show( + proof, + nodes=nodes, + node_deltas=self.node_deltas, + to_module=self.to_module, + minimize=self.minimize, + sort_collections=self.sort_collections, + ) + + if self.failure_info: + with legacy_explore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: + res_lines += print_failure_info(proof, kcfg_explore) + + print('\n'.join(res_lines)) + + +def node_id_like(s: str) -> NodeIdLike: + try: + return int(s) + except ValueError: + return s class ZeroProcessPool: @@ -201,15 +294,6 @@ def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: return [f(x) for x in xs] -@contextlib.contextmanager -def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: - if workers <= 1: - yield ZeroProcessPool() - else: - with ProcessPool(ncpus=workers) as pp: - yield pp - - class JSONEncoder(json.JSONEncoder): def default(self, obj: Any) -> Any: if isinstance(obj, FrozenDict): @@ -273,668 +357,588 @@ def get_or_load_claim_job(claim_label: str) -> KClaimJob: return frozenset({get_or_load_claim_job(claim.label) for claim in claims}) -def exec_prove( - spec_file: Path, - includes: Iterable[str], - definition_dir: Path | None = None, - bug_report: BugReport | None = None, - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - reinit: bool = False, - max_depth: int = 1000, - max_iterations: int | None = None, - workers: int = 1, - break_every_step: bool = False, - break_on_jumpi: bool = False, - break_on_calls: bool = False, - break_on_storage: bool = False, - break_on_basic_blocks: bool = False, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - trace_rewrites: bool = False, - failure_info: bool = True, - auto_abstract_gas: bool = False, - fail_fast: bool = False, - always_check_subsumption: bool = True, - fast_check_subsumption: bool = False, - fallback_on: Iterable[FallbackReason] | None = None, - interim_simplification: int | None = None, - post_exec_simplify: bool = True, - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') - md_selector = 'k' - - if save_directory is None: - save_directory = Path(tempfile.mkdtemp()) - - digest_file = save_directory / 'digest' - - if definition_dir is None: - definition_dir = kdist.get('evm-semantics.haskell') - - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) - - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - - if kore_rpc_command is None: - kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) - elif isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - def is_functional(claim: KClaim) -> bool: - claim_lhs = claim.body - if type(claim_lhs) is KRewrite: - claim_lhs = claim_lhs.lhs - return not (type(claim_lhs) is KApply and claim_lhs.label.name == '') - - 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=claim_labels, - exclude_claim_labels=exclude_claim_labels, - ) - if all_claims is None: - raise ValueError(f'No claims found in file: {spec_file}') - spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() - all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) - all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} - claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) - - def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: - claim = claim_job.claim - up_to_date = claim_job.up_to_date(digest_file) - if up_to_date: - _LOGGER.info(f'Claim is up to date: {claim.label}') - else: - _LOGGER.info(f'Claim reinitialized because it is out of date: {claim.label}') - claim_job.update_digest(digest_file) - with legacy_explore( - kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), - id=claim.label, - 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, - fallback_on=fallback_on, - interim_simplification=interim_simplification, - no_post_exec_simplify=(not post_exec_simplify), - ) as kcfg_explore: - proof_problem: Proof - if is_functional(claim): - if not reinit and up_to_date 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 not reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): - proof_problem = APRProof.read_proof_data(save_directory, claim.label) +@contextlib.contextmanager +def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: + if workers <= 1: + yield ZeroProcessPool() + else: + with ProcessPool(ncpus=workers) as pp: + yield pp - 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_symbolic.assume_defined(new_init) - - _LOGGER.info(f'Simplifying initial and target node: {claim.label}') - new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init) - new_target, _ = kcfg_explore.cterm_symbolic.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], - admitted=claim.is_trusted, - ) - - if proof_problem.admitted: - proof_problem.write_proof_data() - _LOGGER.info(f'Skipping execution of proof because it is marked as admitted: {proof_problem.id}') - return True, None - - start_time = time.time() - passed = run_prover( - proof_problem, - kcfg_explore, - max_depth=max_depth, - max_iterations=max_iterations, - cut_point_rules=KEVMSemantics.cut_point_rules( - break_on_jumpi, break_on_calls, break_on_storage, break_on_basic_blocks - ), - terminal_rules=KEVMSemantics.terminal_rules(break_every_step), - fail_fast=fail_fast, - always_check_subsumption=always_check_subsumption, - fast_check_subsumption=fast_check_subsumption, - ) - 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) - - 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_claim_jobs_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) - - failed = 0 - for job, r in zip(selected_claims, selected_results, strict=True): - passed, failure_log = r - if passed: - print(f'PROOF PASSED: {job.claim.label}') - else: - failed += 1 - print(f'PROOF FAILED: {job.claim.label}') - if failure_info and failure_log is not None: - for line in failure_log: - print(line) - - if failed: - sys.exit(failed) - - -def exec_prune( - definition_dir: Path, - spec_file: Path, - node: NodeIdLike, - includes: Iterable[str] = (), - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') - md_selector = 'k' - - if save_directory is None: - raise ValueError('Must pass --save-directory to prune!') - - kevm = KEVM(definition_dir, use_directory=save_directory) - - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - - _LOGGER.info(f'Extracting claims from file: {spec_file}') - claim = single( - kevm.get_claims( - spec_file, - spec_module_name=spec_module, - include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + +class ProveCommand( + Command, + KOptions, + ParallelOptions, + KProveOptions, + BugReportOptions, + SMTOptions, + ExploreOptions, + SpecOptions, + RPCOptions, + LoggingOptions, +): + reinit: bool + + @staticmethod + def name() -> str: + return 'prove' + + @staticmethod + def help_str() -> str: + return 'Run KEVM proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'reinit': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--reinit', + dest='reinit', + action='store_true', + help='Reinitialize CFGs even if they already exist.', ) - ) - apr_proof = APRProof.read_proof_data(save_directory, claim.label) - node_ids = apr_proof.prune(node) - _LOGGER.info(f'Pruned nodes: {node_ids}') - apr_proof.write_proof_data() - - -def exec_section_edge( - definition_dir: Path, - spec_file: Path, - edge: tuple[str, str], - sections: int = 2, - includes: Iterable[str] = (), - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - trace_rewrites: bool = False, - bug_report: BugReport | None = None, - use_booster: bool = False, - **kwargs: Any, -) -> None: - md_selector = 'k' - - if save_directory is None: - raise ValueError('Must pass --save-directory to section-edge!') - - if kore_rpc_command is None: - kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) - elif isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - kevm = KEVM(definition_dir, use_directory=save_directory) - llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None - - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - - claim = single( - kevm.get_claims( - spec_file, - spec_module_name=spec_module, + def exec(self) -> None: + md_selector = 'k' + + save_directory = self.save_directory if self.save_directory is not None else Path(tempfile.mkdtemp()) + digest_file = save_directory / 'digest' + + definition_dir = self.definition_dir if self.definition_dir is not None else kdist.get('evm-semantics.haskell') + + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=self.bug_report) + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + kore_rpc_command: Iterable[str] + if self.kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if self.use_booster else ('kore-rpc',) + elif isinstance(self.kore_rpc_command, str): + kore_rpc_command = self.kore_rpc_command.split() + + def is_functional(claim: KClaim) -> bool: + claim_lhs = claim.body + if type(claim_lhs) is KRewrite: + claim_lhs = claim_lhs.lhs + return not (type(claim_lhs) is KApply and claim_lhs.label.name == '') + + llvm_definition_dir = definition_dir / 'llvm-library' if self.use_booster else None + + _LOGGER.info(f'Extracting claims from file: {self.spec_file}') + all_claims = kevm.get_claims( + self.spec_file, + spec_module_name=self.spec_module, include_dirs=include_dirs, md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, ) - ) - - proof = APRProof.read_proof_data(save_directory, claim.label) - source_id, target_id = edge - with legacy_explore( - kevm, - kcfg_semantics=KEVMSemantics(), - id=proof.id, - bug_report=bug_report, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - llvm_definition_dir=llvm_definition_dir, - ) as kcfg_explore: - kcfg, _ = kcfg_explore.section_edge( - proof.kcfg, source_id=int(source_id), target_id=int(target_id), logs=proof.logs, sections=sections + if all_claims is None: + raise ValueError(f'No claims found in file: {self.spec_file}') + spec_module_name = ( + self.spec_module if self.spec_module is not None else os.path.splitext(self.spec_file.name)[0].upper() ) - proof.write_proof_data() - - -def exec_show_kcfg( - definition_dir: Path, - spec_file: Path, - save_directory: Path | None = None, - includes: Iterable[str] = (), - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - spec_module: str | None = None, - md_selector: str | None = None, - nodes: Iterable[NodeIdLike] = (), - node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), - to_module: bool = False, - minimize: bool = True, - failure_info: bool = False, - sort_collections: bool = False, - pending: bool = False, - failing: bool = False, - **kwargs: Any, -) -> None: - kevm = KEVM(definition_dir) - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - proof = get_apr_proof_for_spec( - kevm, - spec_file, - save_directory=save_directory, - spec_module_name=spec_module, - include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, - ) + all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) + all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} + claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) + + def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: + claim = claim_job.claim + up_to_date = claim_job.up_to_date(digest_file) + if up_to_date: + _LOGGER.info(f'Claim is up to date: {claim.label}') + else: + _LOGGER.info(f'Claim reinitialized because it is out of date: {claim.label}') + claim_job.update_digest(digest_file) + with legacy_explore( + kevm, + kcfg_semantics=KEVMSemantics(auto_abstract_gas=self.auto_abstract_gas), + id=claim.label, + llvm_definition_dir=llvm_definition_dir, + bug_report=self.bug_report, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + trace_rewrites=self.trace_rewrites, + fallback_on=self.fallback_on, + interim_simplification=self.interim_simplification, + no_post_exec_simplify=(not self.post_exec_simplify), + ) as kcfg_explore: + proof_problem: Proof + if is_functional(claim): + if not self.reinit and up_to_date 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 not self.reinit and up_to_date 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_symbolic.assume_defined(new_init) + + _LOGGER.info(f'Simplifying initial and target node: {claim.label}') + new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init) + new_target, _ = kcfg_explore.cterm_symbolic.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], + admitted=claim.is_trusted, + ) + + if proof_problem.admitted: + proof_problem.write_proof_data() + _LOGGER.info(f'Skipping execution of proof because it is marked as admitted: {proof_problem.id}') + return True, None + + start_time = time.time() + passed = run_prover( + proof_problem, + kcfg_explore, + max_depth=self.max_depth, + max_iterations=self.max_iterations, + cut_point_rules=KEVMSemantics.cut_point_rules( + self.break_on_jumpi, + self.break_on_calls, + self.break_on_storage, + self.break_on_basic_blocks, + ), + terminal_rules=KEVMSemantics.terminal_rules(self.break_every_step), + fail_fast=self.fail_fast, + always_check_subsumption=self.always_check_subsumption, + fast_check_subsumption=self.fast_check_subsumption, + ) + 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) + + return passed, failure_log + + topological_sorter = graphlib.TopologicalSorter(claims_graph) + topological_sorter.prepare() + with wrap_process_pool(workers=self.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_claim_jobs_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) + + failed = 0 + for job, r in zip(selected_claims, selected_results, strict=True): + passed, failure_log = r + if passed: + print(f'PROOF PASSED: {job.claim.label}') + else: + failed += 1 + print(f'PROOF FAILED: {job.claim.label}') + if self.failure_info and failure_log is not None: + for line in failure_log: + print(line) - if pending: - nodes = list(nodes) + [node.id for node in proof.pending] - if failing: - nodes = list(nodes) + [node.id for node in proof.failing] - - node_printer = kevm_node_printer(kevm, proof) - proof_show = APRProofShow(kevm, node_printer=node_printer) - - res_lines = proof_show.show( - proof, - nodes=nodes, - node_deltas=node_deltas, - to_module=to_module, - minimize=minimize, - sort_collections=sort_collections, - ) + if failed: + sys.exit(failed) - if failure_info: - with legacy_explore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: - res_lines += print_failure_info(proof, kcfg_explore) - - print('\n'.join(res_lines)) - - -def exec_view_kcfg( - definition_dir: Path, - spec_file: Path, - save_directory: Path | None = None, - includes: Iterable[str] = (), - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - spec_module: str | None = None, - md_selector: str | None = None, - **kwargs: Any, -) -> None: - kevm = KEVM(definition_dir) - include_dirs = [Path(include) for include in includes] - include_dirs += config.INCLUDE_DIRS - proof = get_apr_proof_for_spec( - kevm, - spec_file, - save_directory=save_directory, - spec_module_name=spec_module, - include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, - ) - node_printer = kevm_node_printer(kevm, proof) +class VersionCommand(Command, LoggingOptions): + @staticmethod + def name() -> str: + return 'version' - def custom_view(element: KCFGElem) -> list[str]: - if type(element) is KCFG.Edge: - return list(element.rules) - if type(element) is KCFG.NDBranch: - return list(element.rules) - return [] + @staticmethod + def help_str() -> str: + return 'Print KEVM version and exit.' - proof_view = APRProofViewer(proof, kevm, node_printer=node_printer, custom_view=custom_view) + def exec(self) -> None: + print(f'KEVM Version: {VERSION}') - proof_view.run() +class PruneCommand(Command, KOptions, SpecOptions, LoggingOptions): + node: NodeIdLike -def exec_run( - input_file: Path, - expand_macros: bool, - depth: int | None, - output: KRunOutput, - schedule: str, - mode: str, - chainid: int, - usegas: bool, - target: str | None = None, - save_directory: Path | None = None, - debugger: bool = False, - **kwargs: Any, -) -> None: - if target is None: - target = 'llvm' + @staticmethod + def name() -> str: + return 'prune-proof' - target_fqn = f'evm-semantics.{target}' + @staticmethod + def help_str() -> str: + return 'Remove a node and its successors from the proof state.' - _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - try: - json_read = json.loads(input_file.read_text()) - kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas) - except json.JSONDecodeError: - pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation')) - kast_pgm = kevm.parse_token(pgm_token) - kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation')) - kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas) - - kevm.run( - kore_pattern, - depth=depth, - term=True, - expand_macros=expand_macros, - output=output, - check=True, - debugger=debugger, - ) + def exec(self) -> None: + md_selector = 'k' + if self.save_directory is None: + raise ValueError('Must pass --save-directory to prune-proof!') -def exec_kast( - input_file: Path, - output: PrintOutput, - schedule: str, - mode: str, - chainid: int, - usegas: bool, - target: str | None = None, - save_directory: Path | None = None, - **kwargs: Any, -) -> None: - if target is None: - target = 'llvm' + if self.definition_dir is None: + raise ValueError('Must pass --definition to prune-proof!') - target_fqn = f'evm-semantics.{target}' + kevm = KEVM(self.definition_dir, use_directory=self.save_directory) - _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS - try: - json_read = json.loads(input_file.read_text()) - kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas) - except json.JSONDecodeError: - pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation')) - kast_pgm = kevm.parse_token(pgm_token) - kore_pgm = kevm.kast_to_kore(kast_pgm) - kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas) + _LOGGER.info(f'Extracting claims from file: {self.spec_file}') + claim = single( + kevm.get_claims( + self.spec_file, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) + ) - output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=output) - print(output_text) + apr_proof = APRProof.read_proof_data(self.save_directory, claim.label) + node_ids = apr_proof.prune(self.node) + print(f'Pruned nodes: {node_ids}') + apr_proof.write_proof_data() + + +class ProveLegacyCommand(Command, KOptions, SpecOptions, KProveLegacyOptions, LoggingOptions): + bug_report_legacy: bool + + @staticmethod + def name() -> str: + return 'prove-legacy' + + @staticmethod + def help_str() -> str: + return 'Run KEVM proof using the legacy kprove binary.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report_legacy': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('--bug-report-legacy', action='store_true', help='Generate a legacy bug report.') + + def exec(self) -> None: + definition_dir = self.definition_dir + if definition_dir is None: + definition_dir = kdist.get('evm-semantics.haskell') + + kevm = KEVM(definition_dir, use_directory=self.save_directory) + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + final_state = kevm.prove_legacy( + spec_file=self.spec_file, + includes=include_dirs, + bug_report=self.bug_report_legacy, + spec_module=self.spec_module, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + debug=self.debug, + debugger=self.debugger, + max_depth=self.max_depth, + max_counterexamples=self.max_counterexamples, + branching_allowed=self.branching_allowed, + haskell_backend_args=self.haskell_backend_args, + ) + final_kast = mlOr([state.kast for state in final_state]) + print(kevm.pretty_print(final_kast)) + if not is_top(final_kast): + raise SystemExit(1) -# Helpers +class ViewKCFGCommand(Command, KOptions, SpecOptions, LoggingOptions): + @staticmethod + def name() -> str: + return 'view-kcfg' + @staticmethod + def help_str() -> str: + return 'Explore a given proof in the KCFG visualizer.' -def _create_argument_parser() -> ArgumentParser: - def list_of(elem_type: Callable[[str], T], delim: str = ';') -> Callable[[str], list[T]]: - def parse(s: str) -> list[T]: - return [elem_type(elem) for elem in s.split(delim)] + def exec(self) -> None: + if self.definition_dir is None: + raise ValueError('Must pass --definition to view-kcfg!') - return parse + kevm = KEVM(self.definition_dir) + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + proof = get_apr_proof_for_spec( + kevm, + self.spec_file, + save_directory=self.save_directory, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=self.md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) - kevm_cli_args = KEVMCLIArgs() - parser = ArgumentParser(prog='kevm-pyk') + node_printer = kevm_node_printer(kevm, proof) + + def custom_view(element: KCFGElem) -> list[str]: + if type(element) is KCFG.Edge: + return list(element.rules) + if type(element) is KCFG.NDBranch: + return list(element.rules) + return [] + + proof_view = APRProofViewer(proof, kevm, node_printer=node_printer, custom_view=custom_view) + + proof_view.run() + + +class RunCommand(Command, KOptions, TargetOptions, EVMChainOptions, SaveDirOptions, LoggingOptions): + input_file: Path + output: KRunOutput + expand_macros: bool + debugger: bool + + @staticmethod + def name() -> str: + return 'run' + + @staticmethod + def help_str() -> str: + return 'Run KEVM test/simulation.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': KRunOutput.PRETTY, + 'expand_macros': True, + 'debugger': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + type=KRunOutput, + choices=list(KRunOutput), + ) + parser.add_argument( + '--expand-macros', + dest='expand_macros', + action='store_true', + help='Expand macros on the input term before execution.', + ) + parser.add_argument( + '--no-expand-macros', + dest='expand_macros', + action='store_false', + help='Do not expand macros on the input term before execution.', + ) + parser.add_argument( + '--debugger', + dest='debugger', + action='store_true', + help='Run GDB debugger for execution.', + ) - command_parser = parser.add_subparsers(dest='command', required=True) + def exec(self) -> None: + target_fqn = f'evm-semantics.{self.target}' - command_parser.add_parser('version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args]) + kevm = KEVM(kdist.get(target_fqn), use_directory=self.save_directory) - kevm_kompile_spec_args = command_parser.add_parser( - 'kompile-spec', - help='Kompile KEVM specification.', - parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args], - ) - kevm_kompile_spec_args.add_argument('main_file', type=file_path, help='Path to file with main module.') - kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|maude]') - kevm_kompile_spec_args.add_argument( - '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' - ) - kevm_kompile_spec_args.add_argument( - '--debug-build', dest='debug_build', default=False, help='Enable debug symbols in LLVM builds.' - ) + try: + json_read = json.loads(self.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, self.schedule, self.mode, self.chainid, self.usegas) + except json.JSONDecodeError: + pgm_token = KToken(self.input_file.read_text(), KSort('EthereumSimulation')) + kast_pgm = kevm.parse_token(pgm_token) + kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation')) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, self.schedule, self.mode, self.chainid, self.usegas + ) - prove_args = command_parser.add_parser( - 'prove', - help='Run KEVM proof.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.parallel_args, - kevm_cli_args.k_args, - kevm_cli_args.kprove_args, - kevm_cli_args.rpc_args, - kevm_cli_args.bug_report_args, - kevm_cli_args.smt_args, - kevm_cli_args.explore_args, - kevm_cli_args.spec_args, - ], - ) - prove_args.add_argument( - '--reinit', - dest='reinit', - default=False, - action='store_true', - help='Reinitialize CFGs even if they already exist.', - ) + kevm.run( + kore_pattern, + depth=self.depth, + term=True, + expand_macros=self.expand_macros, + output=self.output, + check=True, + debugger=self.debugger, + ) - prune_args = command_parser.add_parser( - 'prune', - help='Remove a node and its successors from the proof state.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - ], - ) - prune_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - - section_edge_args = command_parser.add_parser( - 'section-edge', - help='Break an edge into sections.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - ], - ) - section_edge_args.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') - section_edge_args.add_argument( - '--sections', type=int, default=2, help='Number of sections to make from edge (>= 2).' - ) - section_edge_args.add_argument( - '--use-booster', - dest='use_booster', - default=False, - action='store_true', - help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", - ) - prove_legacy_args = command_parser.add_parser( - 'prove-legacy', - help='Run KEVM proof using the legacy kprove binary.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - kevm_cli_args.kprove_legacy_args, - ], - ) - prove_legacy_args.add_argument( - '--bug-report-legacy', default=False, action='store_true', help='Generate a legacy bug report.' - ) +class KastCommand(Command, TargetOptions, EVMChainOptions, SaveDirOptions, LoggingOptions): + input_file: Path + output: PrintOutput - command_parser.add_parser( - 'view-kcfg', - help='Explore a given proof in the KCFG visualizer.', - parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args], - ) + @staticmethod + def name() -> str: + return 'kast' - command_parser.add_parser( - 'show-kcfg', - help='Print the CFG for a given proof.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.kcfg_show_args, - kevm_cli_args.spec_args, - kevm_cli_args.display_args, - ], - ) + @staticmethod + def help_str() -> str: + return 'Run KEVM program.' - run_args = command_parser.add_parser( - 'run', - help='Run KEVM test/simulation.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.target_args, - kevm_cli_args.evm_chain_args, - kevm_cli_args.k_args, - ], - ) - run_args.add_argument('input_file', type=file_path, help='Path to input file.') - run_args.add_argument( - '--output', - default=KRunOutput.PRETTY, - type=KRunOutput, - choices=list(KRunOutput), - ) - run_args.add_argument( - '--expand-macros', - dest='expand_macros', - default=True, - action='store_true', - help='Expand macros on the input term before execution.', - ) - run_args.add_argument( - '--no-expand-macros', - dest='expand_macros', - action='store_false', - help='Do not expand macros on the input term before execution.', - ) - run_args.add_argument( - '--debugger', - dest='debugger', - action='store_true', - help='Run GDB debugger for execution.', - ) + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': PrintOutput.KORE, + } - kast_args = command_parser.add_parser( - 'kast', - help='Run KEVM program.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.target_args, - kevm_cli_args.evm_chain_args, - kevm_cli_args.k_args, - ], - ) - kast_args.add_argument('input_file', type=file_path, help='Path to input file.') - kast_args.add_argument( - '--output', - default=PrintOutput.KORE, - type=PrintOutput, - choices=list(PrintOutput), - ) + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + type=PrintOutput, + choices=list(PrintOutput), + ) + + def exec(self) -> None: + target_fqn = f'evm-semantics.{self.target}' + + kevm = KEVM(kdist.get(target_fqn), use_directory=self.save_directory) + + try: + json_read = json.loads(self.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, self.schedule, self.mode, self.chainid, self.usegas) + except json.JSONDecodeError: + pgm_token = KToken(self.input_file.read_text(), KSort('EthereumSimulation')) + kast_pgm = kevm.parse_token(pgm_token) + kore_pgm = kevm.kast_to_kore(kast_pgm) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, self.schedule, self.mode, self.chainid, self.usegas + ) + + output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=self.output) + print(output_text) + + +class SectionEdgeCommand(Command, LoggingOptions, KOptions, SpecOptions, RPCOptions, BugReportOptions, SMTOptions): + edge: tuple[str, str] + sections: int + use_booster: bool + + @staticmethod + def name() -> str: + return 'section-edge' + + @staticmethod + def help_str() -> str: + return 'Break an edge into sections.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'sections': 2, + 'use-booster': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') + parser.add_argument('--sections', type=int, help='Number of sections to make from edge (>= 2).') + parser.add_argument( + '--use-booster', + dest='use_booster', + action='store_true', + help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", + ) + + def exec(self) -> None: + md_selector = 'k' + + if self.save_directory is None: + raise ValueError('Must pass --save-directory to section-edge!') - return parser + kore_rpc_command: Iterable[str] + if self.kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if self.use_booster else ('kore-rpc',) + elif isinstance(self.kore_rpc_command, str): + kore_rpc_command = self.kore_rpc_command.split() + + if self.definition_dir is None: + raise ValueError('Must pass --definition to section-edge!') + + kevm = KEVM(self.definition_dir, use_directory=self.save_directory) + llvm_definition_dir = self.definition_dir / 'llvm-library' if self.use_booster else None + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + claim = single( + kevm.get_claims( + self.spec_file, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) + ) + + proof = APRProof.read_proof_data(self.save_directory, claim.label) + source_id, target_id = self.edge + with legacy_explore( + kevm, + kcfg_semantics=KEVMSemantics(), + id=proof.id, + bug_report=self.bug_report, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + trace_rewrites=self.trace_rewrites, + llvm_definition_dir=llvm_definition_dir, + ) as kcfg_explore: + kcfg, _ = kcfg_explore.section_edge( + proof.kcfg, source_id=int(source_id), target_id=int(target_id), logs=proof.logs, sections=self.sections + ) + proof.write_proof_data() + + +# Helpers -def _loglevel(args: Namespace) -> int: +def _loglevel(args: LoggingOptions) -> int: if args.debug: return logging.DEBUG diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index c5e4ac5fba..454302bb05 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -1,22 +1,21 @@ from __future__ import annotations +import logging from argparse import ArgumentParser from functools import cached_property -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, Any -from pyk.cli.args import KCLIArgs +from pyk.cli.args import DisplayOptions, KDefinitionOptions, Options from pyk.kore.rpc import FallbackReason -from .utils import arg_pair_of - if TYPE_CHECKING: from collections.abc import Callable - from typing import TypeVar - - from pyk.kcfg.kcfg import NodeIdLike + from typing import Final, TypeVar T = TypeVar('T') +_LOGGER: Final = logging.getLogger(__name__) + def list_of(elem_type: Callable[[str], T], delim: str = ';') -> Callable[[str], list[T]]: def parse(s: str) -> list[T]: @@ -25,323 +24,405 @@ def parse(s: str) -> list[T]: return parse -def node_id_like(s: str) -> NodeIdLike: - try: - return int(s) - except ValueError: - return s +class KEVMDisplayOptions(DisplayOptions): + sort_collections: bool + @staticmethod + def default() -> dict[str, Any]: + return {'sort_collections': False} -class KEVMCLIArgs(KCLIArgs): - @cached_property - def target_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) - return args + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--sort-collections', + dest='sort_collections', + action='store_true', + help='Sort collections before outputting term.', + ) - @cached_property - def k_args(self) -> ArgumentParser: - args = super().definition_args - args.add_argument('--depth', default=None, type=int, help='Maximum depth to execute to.') - return args - @cached_property - def kprove_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( +class KOptions(KDefinitionOptions): + depth: int | None + + @staticmethod + def default() -> dict[str, Any]: + return {'depth': None} + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('--depth', type=int, help='Maximum depth to execute to.') + + +class KProveOptions(Options): + debug_equations: list[str] + always_check_subsumption: bool + fast_check_subsumption: bool + + @staticmethod + def default() -> dict[str, Any]: + return {'always_check_subsumption': True, 'fast_check_subsumption': False, 'debug_equations': []} + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--debug-equations', type=list_of(str, delim=','), - default=[], help='Comma-separate list of equations to debug.', ) - args.add_argument( + parser.add_argument( '--always-check-subsumption', - dest='always-check_subsumption', - default=True, + dest='always_check_subsumption', action='store_true', help='Check subsumption even on non-terminal nodes.', ) - args.add_argument( + parser.add_argument( '--no-always-check-subsumption', - dest='always-check_subsumption', + dest='always_check_subsumption', action='store_false', help='Do not check subsumption on non-terminal nodes.', ) - args.add_argument( + parser.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', - default=False, action='store_true', help='Use fast-check on k-cell to determine subsumption.', ) - return args - @cached_property - def kprove_legacy_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--bug-report', - default=False, - action='store_true', - help='Generate a haskell-backend bug report for the execution.', - ) - args.add_argument( - '--debugger', - dest='debugger', - default=False, - action='store_true', - help='Launch proof in an interactive debugger.', - ) - args.add_argument( - '--max-depth', - dest='max_depth', - default=None, - type=int, - help='The maximum number of computational steps to prove.', - ) - args.add_argument( - '--max-counterexamples', - type=int, - dest='max_counterexamples', - default=None, - help='Maximum number of counterexamples reported before a forcible stop.', - ) - args.add_argument( - '--branching-allowed', - type=int, - dest='branching_allowed', - default=None, - help='Number of branching events allowed before a forcible stop.', - ) - args.add_argument( - '--haskell-backend-arg', - dest='haskell_backend_args', - default=[], - action='append', - help='Arguments passed to the Haskell backend execution engine.', - ) - return args - @cached_property - def evm_chain_args(self) -> ArgumentParser: - schedules = ( - 'DEFAULT', - 'FRONTIER', - 'HOMESTEAD', - 'TANGERINE_WHISTLE', - 'SPURIOUS_DRAGON', - 'BYZANTIUM', - 'CONSTANTINOPLE', - 'PETERSBURG', - 'ISTANBUL', - 'BERLIN', - 'LONDON', - 'MERGE', - 'SHANGHAI', - ) - modes = ('NORMAL', 'VMTESTS') +class RPCOptions(Options): + trace_rewrites: bool + kore_rpc_command: str | None + use_booster: bool + fallback_on: list[FallbackReason] | None + post_exec_simplify: bool + interim_simplification: int | None + port: int | None + maude_port: int | None - args = ArgumentParser(add_help=False) - args.add_argument( - '--schedule', - choices=schedules, - default='SHANGHAI', - help=f"schedule to use for execution [{'|'.join(schedules)}]", - ) - args.add_argument('--chainid', type=int, default=1, help='chain ID to use for execution') - args.add_argument( - '--mode', - choices=modes, - default='NORMAL', - help="execution mode to use [{'|'.join(modes)}]", - ) - args.add_argument( - '--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations' - ) - return args + @staticmethod + def default() -> dict[str, Any]: + return { + 'trace_rewrites': False, + 'use_booster': False, + 'post_exec_simplify': True, + 'kore_rpc_command': None, + 'interim_simplification': None, + 'port': None, + 'maude_port': None, + 'fallback_on': None, + } - @cached_property - def display_args(self) -> ArgumentParser: - args = super().display_args - args.add_argument( - '--sort-collections', - dest='sort_collections', - default=False, - action='store_true', - help='Sort collections before outputting term.', - ) - return args - - @cached_property - def rpc_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--trace-rewrites', dest='trace_rewrites', - default=False, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) - args.add_argument( + parser.add_argument( '--kore-rpc-command', dest='kore_rpc_command', type=str, - default=None, help='Custom command to start RPC server', ) - args.add_argument( + parser.add_argument( '--use-booster', dest='use_booster', - default=False, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) - args.add_argument( + parser.add_argument( '--fallback-on', dest='fallback_on', type=list_of(FallbackReason, delim=','), help='Comma-separated reasons to fallback from booster to kore, only usable with --use-booster. Options [Branching,Aborted,Stuck].', ) - args.add_argument( + parser.add_argument( '--post-exec-simplify', dest='post_exec_simplify', - default=True, action='store_true', help='Always simplify states with kore backend after booster execution, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--no-post-exec-simplify', dest='post_exec_simplify', action='store_false', help='Do not simplify states with kore backend after booster execution, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--interim-simplification', dest='interim_simplification', type=int, help='Max number of steps to execute before applying simplifier to term in booster backend, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--port', dest='port', type=int, - default=None, help='Use existing RPC server on named port', ) - args.add_argument( + parser.add_argument( '--maude-port', dest='maude_port', type=int, - default=None, help='Use existing Maude RPC server on named port', ) - return args - @cached_property - def explore_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + +class ExploreOptions(Options): + break_every_step: bool + break_on_jumpi: bool + break_on_calls: bool + break_on_storage: bool + break_on_basic_blocks: bool + max_depth: int + max_iterations: int | None + failure_info: bool + auto_abstract_gas: bool + counterexample_info: bool + fail_fast: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'break_every_step': False, + 'break_on_jumpi': False, + 'break_on_calls': False, + 'break_on_storage': False, + 'break_on_basic_blocks': False, + 'max_depth': 1000, + 'failure_info': True, + 'counterexample_info': True, + 'fail_fast': True, + 'max_iterations': None, + 'auto_abstract_gas': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--break-every-step', dest='break_every_step', - default=False, action='store_true', help='Store a node for every EVM opcode step (expensive).', ) - args.add_argument( + parser.add_argument( '--break-on-jumpi', dest='break_on_jumpi', - default=False, action='store_true', help='Store a node for every EVM jump opcode.', ) - args.add_argument( + parser.add_argument( '--break-on-calls', dest='break_on_calls', - default=False, action='store_true', help='Store a node for every EVM call made.', ) - args.add_argument( + parser.add_argument( '--no-break-on-calls', dest='break_on_calls', - default=True, action='store_false', help='Do not store a node for every EVM call made.', ) - args.add_argument( + parser.add_argument( '--break-on-storage', dest='break_on_storage', - default=False, action='store_true', help='Store a node for every EVM SSTORE/SLOAD made.', ) - args.add_argument( + parser.add_argument( '--break-on-basic-blocks', dest='break_on_basic_blocks', - default=False, action='store_true', help='Store a node for every EVM basic block (implies --break-on-calls).', ) - args.add_argument( + parser.add_argument( '--max-depth', dest='max_depth', - default=1000, type=int, help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.', ) - args.add_argument( + parser.add_argument( '--max-iterations', dest='max_iterations', - default=None, type=int, help='Number of times to expand the next pending node in the CFG.', ) - args.add_argument( + parser.add_argument( '--failure-information', dest='failure_info', - default=True, action='store_true', help='Show failure summary for all failing tests', ) - args.add_argument( + parser.add_argument( '--no-failure-information', dest='failure_info', action='store_false', help='Do not show failure summary for failing tests', ) - args.add_argument( + parser.add_argument( '--auto-abstract-gas', dest='auto_abstract_gas', action='store_true', help='Automatically extract gas cell when infinite gas is enabled', ) - args.add_argument( + parser.add_argument( '--counterexample-information', dest='counterexample_info', - default=True, action='store_true', help='Show models for failing nodes.', ) - args.add_argument( + parser.add_argument( '--no-counterexample-information', dest='counterexample_info', action='store_false', help='Do not show models for failing nodes.', ) - args.add_argument( + parser.add_argument( '--fail-fast', dest='fail_fast', - default=True, action='store_true', help='Stop execution on other branches if a failing node is detected.', ) - args.add_argument( + parser.add_argument( '--no-fail-fast', dest='fail_fast', action='store_false', help='Continue execution on other branches if a failing node is detected.', ) - return args + + +class KProveLegacyOptions(Options): + bug_report: bool + debugger: bool + max_depth: int | None + max_counterexamples: int | None + branching_allowed: int | None + haskell_backend_args: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report': False, + 'debugger': False, + 'max_depth': None, + 'max_counterexamples': None, + 'branching_allowed': None, + 'haskell_backend_args': [], + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--bug-report', + action='store_true', + help='Generate a haskell-backend bug report for the execution.', + ) + parser.add_argument( + '--debugger', + dest='debugger', + action='store_true', + help='Launch proof in an interactive debugger.', + ) + parser.add_argument( + '--max-depth', + dest='max_depth', + type=int, + help='The maximum number of computational steps to prove.', + ) + parser.add_argument( + '--max-counterexamples', + type=int, + dest='max_counterexamples', + help='Maximum number of counterexamples reported before a forcible stop.', + ) + parser.add_argument( + '--branching-allowed', + type=int, + dest='branching_allowed', + help='Number of branching events allowed before a forcible stop.', + ) + parser.add_argument( + '--haskell-backend-arg', + dest='haskell_backend_args', + action='append', + help='Arguments passed to the Haskell backend execution engine.', + ) + + +class TargetOptions(Options): + target: str + + @staticmethod + def default() -> dict[str, Any]: + return { + 'target': 'llvm', + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) + + +class EVMChainOptions(Options): + schedule: str + chainid: int + mode: str + usegas: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'schedule': 'SHANGHAI', + 'chainid': 1, + 'mode': 'NORMAL', + 'usegas': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + schedules = ( + 'DEFAULT', + 'FRONTIER', + 'HOMESTEAD', + 'TANGERINE_WHISTLE', + 'SPURIOUS_DRAGON', + 'BYZANTIUM', + 'CONSTANTINOPLE', + 'PETERSBURG', + 'ISTANBUL', + 'BERLIN', + 'LONDON', + 'MERGE', + 'SHANGHAI', + ) + modes = ('NORMAL', 'VMTESTS') + + parser.add_argument( + '--schedule', + choices=schedules, + help=f"schedule to use for execution [{'|'.join(schedules)}]", + ) + parser.add_argument('--chainid', type=int, help='chain ID to use for execution') + parser.add_argument( + '--mode', + choices=modes, + help="execution mode to use [{'|'.join(modes)}]", + ) + parser.add_argument('--no-gas', action='store_false', dest='usegas', help='omit gas cost computations') + + +class KEVMCLIArgs: + requires: list[str] + imports: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'requires': [], + 'imports': [], + } @cached_property def k_gen_args(self) -> ArgumentParser: @@ -349,65 +430,13 @@ def k_gen_args(self) -> ArgumentParser: args.add_argument( '--require', dest='requires', - default=[], action='append', help='Extra K requires to include in generated output.', ) args.add_argument( '--module-import', dest='imports', - default=[], action='append', help='Extra modules to import into generated main module.', ) return args - - @cached_property - def kcfg_show_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--node', - type=node_id_like, - dest='nodes', - default=[], - action='append', - help='List of nodes to display as well.', - ) - args.add_argument( - '--node-delta', - type=arg_pair_of(node_id_like, node_id_like), - dest='node_deltas', - default=[], - action='append', - help='List of nodes to display delta for.', - ) - args.add_argument( - '--failure-information', - dest='failure_info', - default=False, - action='store_true', - help='Show failure summary for cfg', - ) - args.add_argument( - '--no-failure-information', - dest='failure_info', - action='store_false', - help='Do not show failure summary for cfg', - ) - args.add_argument( - '--to-module', dest='to_module', default=False, action='store_true', help='Output edges as a K module.' - ) - args.add_argument( - '--pending', dest='pending', default=False, action='store_true', help='Also display pending nodes' - ) - args.add_argument( - '--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes' - ) - args.add_argument( - '--counterexample-information', - dest='counterexample_info', - default=False, - action='store_true', - help="Show models for failing nodes. Should be called with the '--failure-information' flag", - ) - return args diff --git a/kevm-pyk/src/kevm_pyk/gst_to_kore.py b/kevm-pyk/src/kevm_pyk/gst_to_kore.py index fa7f92447c..95c1a6fd9b 100644 --- a/kevm-pyk/src/kevm_pyk/gst_to_kore.py +++ b/kevm-pyk/src/kevm_pyk/gst_to_kore.py @@ -10,7 +10,7 @@ from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer from pyk.kore.syntax import App, SortApp -from .cli import KEVMCLIArgs +from .cli import EVMChainOptions if TYPE_CHECKING: from argparse import Namespace @@ -67,10 +67,10 @@ def _exec_gst_to_kore(input_file: Path, schedule: str, mode: str, chainid: int, def _parse_args() -> Namespace: - kevm_cli_args = KEVMCLIArgs() + EVMChainOptions.all_args() parser = ArgumentParser( description='Convert a GeneralStateTest to Kore for compsumption by KEVM', - parents=[kevm_cli_args.evm_chain_args], + parents=[EVMChainOptions.all_args()], ) parser.add_argument('input_file', type=file_path, help='path to GST') return parser.parse_args() diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index fc10d65ba6..3d77af61c4 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -9,7 +9,7 @@ from pyk.proof.reachability import APRProof from kevm_pyk import config -from kevm_pyk.__main__ import exec_prove +from kevm_pyk.__main__ import ProveCommand from kevm_pyk.kevm import KEVM from kevm_pyk.kompile import KompileTarget, kevm_kompile @@ -222,18 +222,21 @@ def test_pyk_prove( definition_dir = kompiled_target_for(spec_file) name = str(spec_file.relative_to(SPEC_DIR)) break_on_calls = name in TEST_PARAMS and TEST_PARAMS[name].break_on_calls - exec_prove( - spec_file=spec_file, - definition_dir=definition_dir, - includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], - save_directory=use_directory, - smt_timeout=300, - smt_retry_limit=10, - md_selector='foo', # TODO Ignored flag, this is to avoid KeyError - use_booster=use_booster, - bug_report=bug_report, - break_on_calls=break_on_calls, + + options = ProveCommand( + { + 'spec_file': spec_file, + 'definition_dir': definition_dir, + 'includes': [str(include_dir) for include_dir in config.INCLUDE_DIRS], + 'save_directory': use_directory, + 'md_selector': 'foo', + 'use_booster': use_booster, + 'bug_report': bug_report, + 'break_on_calls': break_on_calls, + } ) + + options.exec() if name in TEST_PARAMS: params = TEST_PARAMS[name] if params.leaf_number is not None and params.main_claim_id is not None: diff --git a/package/version b/package/version index b9c0a675e9..cdf6f00a1c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.492 +1.0.493