From 08e5377e83f4460ecf05f1ed4a70d288eaf0d2ed Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Tue, 9 Jul 2024 18:41:36 -0500 Subject: [PATCH] Add option to use sequential proof loop (#2518) * Add option to use sequential proof loop * Set Version: 1.0.634 * Set Version: 1.0.635 * Set Version: 1.0.636 * Add --force-sequential to pytest fixtures --------- Co-authored-by: devops --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 1 + kevm-pyk/src/kevm_pyk/cli.py | 9 +++++++++ kevm-pyk/src/kevm_pyk/utils.py | 19 ++++++++++++------- kevm-pyk/src/tests/conftest.py | 11 +++++++++++ kevm-pyk/src/tests/integration/test_prove.py | 8 ++++++++ package/version | 2 +- 8 files changed, 44 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 4fc7906fb8..6064e4d877 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.635" +version = "1.0.636" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d49067a2f1..6284b18225 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.635' +VERSION: Final = '1.0.636' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 425c086055..09d5d764e0 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -354,6 +354,7 @@ def create_kcfg_explore() -> KCFGExplore: fast_check_subsumption=options.fast_check_subsumption, direct_subproof_rules=options.direct_subproof_rules, max_frontier_parallel=options.max_frontier_parallel, + force_sequential=options.force_sequential, ) end_time = time.time() _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s') diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index c379e203bc..d3efd6d905 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -337,6 +337,7 @@ class ExploreOptions(Options): auto_abstract_gas: bool counterexample_info: bool fail_fast: bool + force_sequential: bool @staticmethod def default() -> dict[str, Any]: @@ -353,6 +354,7 @@ def default() -> dict[str, Any]: 'auto_abstract_gas': False, 'counterexample_info': True, 'fail_fast': True, + 'force_sequential': False, } @staticmethod @@ -1113,6 +1115,13 @@ def explore_args(self) -> ArgumentParser: action='store_true', help='Stop execution on other branches if a failing node is detected (default).', ) + args.add_argument( + '--force-sequential', + dest='force_sequential', + default=None, + action='store_true', + help='Use sequential, single-threaded proof loop.', + ) args.add_argument( '--no-fail-fast', dest='fail_fast', diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 60253e40f7..ea24433d5a 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -108,6 +108,7 @@ def run_prover( fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, max_frontier_parallel: int = 1, + force_sequential: bool = False, ) -> bool: prover: APRProver | ImpliesProver try: @@ -125,13 +126,17 @@ def create_prover() -> APRProver: direct_subproof_rules=direct_subproof_rules, ) - parallel_advance_proof( - proof=proof, - create_prover=create_prover, - max_iterations=max_iterations, - fail_fast=fail_fast, - max_workers=max_frontier_parallel, - ) + if force_sequential: + prover = create_prover() + prover.advance_proof(proof=proof, max_iterations=max_iterations, fail_fast=fail_fast) + else: + parallel_advance_proof( + proof=proof, + create_prover=create_prover, + max_iterations=max_iterations, + fail_fast=fail_fast, + max_workers=max_frontier_parallel, + ) elif type(proof) is EqualityProof: prover = ImpliesProver(proof, kcfg_explore=create_kcfg_explore()) diff --git a/kevm-pyk/src/tests/conftest.py b/kevm-pyk/src/tests/conftest.py index 86921835d6..bf9a6856f0 100644 --- a/kevm-pyk/src/tests/conftest.py +++ b/kevm-pyk/src/tests/conftest.py @@ -39,6 +39,12 @@ def pytest_addoption(parser: Parser) -> None: type=Path, help='Use pre-kompiled definitions for proof tests', ) + parser.addoption( + '--force-sequential', + default=False, + action='store_true', + help='Use sequential, single-threaded proof loop.', + ) @pytest.fixture @@ -56,6 +62,11 @@ def use_booster_dev(request: FixtureRequest) -> bool: return request.config.getoption('--use-booster-dev') +@pytest.fixture(scope='session') +def force_sequential(request: FixtureRequest) -> bool: + return request.config.getoption('--force-sequential') + + @pytest.fixture(scope='session') def spec_name(request: FixtureRequest) -> str | None: return request.config.getoption('--spec-name') diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 9d263ee0d8..f9490e4cfa 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -181,6 +181,7 @@ def _test_prove( tmp_path: Path, caplog: LogCaptureFixture, no_use_booster: bool, + force_sequential: bool, use_booster_dev: bool, bug_report: BugReport | None, spec_name: str | None, @@ -216,6 +217,7 @@ def _test_prove( 'save_directory': use_directory, 'md_selector': 'foo', # TODO Ignored flag, this is to avoid KeyError 'use_booster': not no_use_booster, + 'force_sequential': force_sequential, 'use_booster_dev': use_booster_dev, 'bug_report': bug_report, 'break_on_calls': break_on_calls, @@ -318,6 +320,7 @@ def test_prove_rules( tmp_path: Path, caplog: LogCaptureFixture, no_use_booster: bool, + force_sequential: bool, use_booster_dev: bool, bug_report: BugReport | None, spec_name: str | None, @@ -328,6 +331,7 @@ def test_prove_rules( tmp_path, caplog, no_use_booster, + force_sequential, use_booster_dev, bug_report=bug_report, spec_name=spec_name, @@ -345,6 +349,7 @@ def test_prove_functional( tmp_path: Path, caplog: LogCaptureFixture, no_use_booster: bool, + force_sequential: bool, use_booster_dev: bool, bug_report: BugReport | None, spec_name: str | None, @@ -355,6 +360,7 @@ def test_prove_functional( tmp_path, caplog, no_use_booster, + force_sequential, use_booster_dev, bug_report=bug_report, spec_name=spec_name, @@ -366,6 +372,7 @@ def test_prove_dss( kompiled_target_for: Callable[[Path], Path], tmp_path: Path, caplog: LogCaptureFixture, + force_sequential: bool, bug_report: BugReport | None, ) -> None: spec_file = REPO_ROOT / 'tests/specs/mcd/vat-spec.k' @@ -375,6 +382,7 @@ def test_prove_dss( tmp_path, caplog, False, + force_sequential, False, bug_report=bug_report, spec_name=None, diff --git a/package/version b/package/version index c2d2c07617..8895d5daf4 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.635 +1.0.636