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 <[email protected]>

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. <[email protected]>",

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'

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')

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',

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())

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')

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,

package/version

@@ -1 +1 @@
-1.0.635
+1.0.636