kevm prove + test harness: Haskell-backend logging flags, per-claim filtering, booster-only-simplify

.gitignore

@@ -29,3 +29,6 @@
 # Kept in-repo for discoverability; the summarised report is committed under
 # docs/experiment-logs/ instead.  See CLAUDE.md "Comparing haskell-backend builds".
 /perf-runs/
+
+# Per-spec backend log bundles written by the test harness --haskell-logging default.
+*.analysis/

kevm-pyk/src/kevm_pyk/__main__.py

@@ -18,6 +18,7 @@
 from pathos.pools import ProcessPool  # type: ignore
 from pyk.cli.pyk import parse_toml_args
 from pyk.cterm import CTermSymbolic
+from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES
 from pyk.kast.outer import KApply, KRewrite, KSort, KToken
 from pyk.kcfg import KCFG
 from pyk.kcfg.explore import KCFGExplore
@@ -318,7 +319,9 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]:
             interim_simplification=options.interim_simplification,
             no_post_exec_simplify=(not options.post_exec_simplify),
             port=options.port,
-            haskell_threads=options.max_frontier_parallel,
+            haskell_log_entries=options.haskell_log_entries,
+            haskell_log_dir=options.haskell_log_dir,
+            booster_only_simplify=options.booster_only_simplify,
         ) as kcfg_explore:
 
             def create_kcfg_explore() -> KCFGExplore:
@@ -336,6 +339,9 @@ def create_kcfg_explore() -> KCFGExplore:
                     kevm.definition,
                     log_succ_rewrites=options.log_succ_rewrites,
                     log_fail_rewrites=options.log_fail_rewrites,
+                    booster_only_simplify=options.booster_only_simplify,
+                    haskell_log_entries=options.haskell_log_entries or HASKELL_LOGGING_ENTRIES,
+                    haskell_log_dir=options.haskell_log_dir,
                 )
                 return KCFGExplore(
                     cterm_symbolic,

kevm-pyk/src/kevm_pyk/cli.py

@@ -185,6 +185,13 @@ def _create_argument_parser() -> ArgumentParser:
         action='store_true',
         help='Reinitialize CFGs even if they already exist.',
     )
+    prove_args.add_argument(
+        '--booster-only-simplify',
+        dest='booster_only_simplify',
+        default=None,
+        action='store_true',
+        help='Skip the Kore simplification pass after Booster; assume_defined still uses Kore for #Ceil evaluation.',
+    )
     prove_args.add_argument(
         '--max-frontier-parallel',
         type=int,
@@ -353,6 +360,8 @@ class RPCOptions(Options):
     interim_simplification: int | None
     port: int | None
     use_booster_dev: bool
+    haskell_log_entries: list[str]
+    haskell_log_dir: Path | None
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -366,6 +375,8 @@ def default() -> dict[str, Any]:
             'interim_simplification': None,
             'port': None,
             'use_booster_dev': False,
+            'haskell_log_entries': [],
+            'haskell_log_dir': None,
         }
 
     @staticmethod
@@ -599,12 +610,14 @@ class ProveOptions(
     KProveOptions,
 ):
     reinit: bool
+    booster_only_simplify: bool
     max_frontier_parallel: int
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'reinit': False,
+            'booster_only_simplify': False,
             'max_frontier_parallel': 1,
         }
 
@@ -1089,6 +1102,18 @@ def rpc_args(self) -> ArgumentParser:
             type=int,
             help='Use existing RPC server on named port.',
         )
+        args.add_argument(
+            '--haskell-log-entries',
+            dest='haskell_log_entries',
+            type=list_of(str, delim=','),
+            help='Comma-separated Haskell-backend log entries to capture per request (e.g. Abort,Simplify,Rewrite); defaults to the curated pyk set when omitted.',
+        )
+        args.add_argument(
+            '--haskell-log-dir',
+            dest='haskell_log_dir',
+            type=Path,
+            help='Capture per-request Haskell-backend log bundles, one <request-id>.jsonl file per RPC, under this directory.',
+        )
         return args
 
     @cached_property

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -769,7 +769,6 @@ def _init_and_run_proof(proof: APRProof) -> tuple[bool, list[str]]:
                 interim_simplification=25,
                 no_post_exec_simplify=False,
                 port=None,
-                haskell_threads=8,
             ) as kcfg_explore:
 
                 def create_kcfg_explore() -> KCFGExplore:

kevm-pyk/src/kevm_pyk/utils.py

@@ -319,7 +319,9 @@ def initialize_apr_proof(cterm_symbolic: CTermSymbolic, proof: APRProof) -> None
     target_cterm = proof.kcfg.node(proof.target).cterm
 
     _LOGGER.info(f'Computing definedness constraint for initial node: {proof.id}')
-    init_cterm = cterm_symbolic.assume_defined(init_cterm)
+    # Pin booster_only_simplify=False regardless of the run-wide setting: the #Ceil
+    # definedness constraint must be discharged by Kore, which Booster-only mode skips.
+    init_cterm = cterm_symbolic.assume_defined(init_cterm, booster_only_simplify=False)
 
     _LOGGER.info(f'Simplifying initial and target node: {proof.id}')
     init_cterm, _ = cterm_symbolic.simplify(init_cterm)
@@ -349,15 +351,16 @@ def legacy_explore(
     bug_report: BugReport | None = None,
     haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
     haskell_log_entries: Iterable[str] = (),
-    haskell_threads: int | None = None,
     log_axioms_file: Path | None = None,
+    haskell_log_dir: Path | None = None,
     log_succ_rewrites: bool = True,
     log_fail_rewrites: bool = True,
     start_server: bool = True,
     fallback_on: Iterable[FallbackReason] | None = None,
     interim_simplification: int | None = None,
     no_post_exec_simplify: bool = False,
     extra_module: KFlatModule | None = None,
+    booster_only_simplify: bool = False,
 ) -> Iterator[KCFGExplore]:
     with cterm_symbolic(
         definition=kprint.definition,
@@ -371,13 +374,16 @@ def legacy_explore(
         smt_tactic=smt_tactic,
         bug_report=bug_report,
         haskell_log_format=haskell_log_format,
+        haskell_log_entries=haskell_log_entries,
         log_axioms_file=log_axioms_file,
+        haskell_log_dir=haskell_log_dir,
         log_succ_rewrites=log_succ_rewrites,
         log_fail_rewrites=log_fail_rewrites,
         start_server=start_server,
         fallback_on=fallback_on,
         interim_simplification=interim_simplification,
         no_post_exec_simplify=no_post_exec_simplify,
+        booster_only_simplify=booster_only_simplify,
     ) as csymbolic:
         if extra_module:
             csymbolic.add_module(extra_module, name_as_id=True)

kevm-pyk/src/tests/conftest.py

@@ -5,10 +5,19 @@
 
 import pytest
 
+from .utils import DEFAULT_HASKELL_LOG_ENTRIES
+
 if TYPE_CHECKING:
     from pytest import FixtureRequest, Parser
 
 
+def _csv_option(raw: str | None) -> list[str] | None:
+    """Parse a comma-separated option value into a trimmed list, or None if unset."""
+    if raw is None:
+        return None
+    return [item.strip() for item in raw.split(',') if item.strip()]
+
+
 def pytest_addoption(parser: Parser) -> None:
     parser.addoption(
         '--save-failing',
@@ -40,6 +49,12 @@ def pytest_addoption(parser: Parser) -> None:
         type=str,
         help='Run only this specific specification (skip others)',
     )
+    parser.addoption(
+        '--claim-labels',
+        default=None,
+        type=str,
+        help='Comma-separated claim labels to prove within a spec (e.g. foo-claim,bar-claim); proves all claims if omitted',
+    )
     parser.addoption(
         '--kompiled-targets-dir',
         type=Path,
@@ -51,6 +66,38 @@ def pytest_addoption(parser: Parser) -> None:
         action='store_true',
         help='Use sequential, single-threaded proof loop.',
     )
+    parser.addoption(
+        '--booster-log-dir',
+        type=Path,
+        default=None,
+        help='Capture per-request Haskell backend log bundles under this directory, one per-spec subdirectory of <request-id>.jsonl files. Implies --haskell-logging.',
+    )
+    parser.addoption(
+        '--haskell-logging',
+        action='store_true',
+        default=False,
+        help=(
+            'Enable JSON logging of the default Haskell-backend entries '
+            f'({",".join(DEFAULT_HASKELL_LOG_ENTRIES)}) for all proof tests. '
+            'Use with --booster-log-dir to persist logs.'
+        ),
+    )
+    parser.addoption(
+        '--booster-log-levels',
+        default=None,
+        type=str,
+        help=(
+            'Comma-separated Haskell-backend log entries to enable, overriding the default set '
+            f'used by --haskell-logging ({",".join(DEFAULT_HASKELL_LOG_ENTRIES)}). '
+            'Valid entries are defined by the backend; see its --log-level help.'
+        ),
+    )
+    parser.addoption(
+        '--booster-only-simplify',
+        action='store_true',
+        default=False,
+        help='Skip the Kore simplification pass after Booster for all simplify/execute/implies calls.',
+    )
 
 
 @pytest.fixture
@@ -83,6 +130,41 @@ def spec_name(request: FixtureRequest) -> str | None:
     return request.config.getoption('--spec-name')
 
 
+@pytest.fixture(scope='session')
+def claim_labels(request: FixtureRequest) -> list[str] | None:
+    return _csv_option(request.config.getoption('--claim-labels'))
+
+
 @pytest.fixture(scope='session')
 def kompiled_targets_dir(request: FixtureRequest) -> Path | None:
     return request.config.getoption('--kompiled-targets-dir')
+
+
+@pytest.fixture(scope='session')
+def booster_log_dir(request: FixtureRequest) -> Path | None:
+    d: Path | None = request.config.getoption('--booster-log-dir')
+    if d is not None:
+        d.mkdir(parents=True, exist_ok=True)
+    return d
+
+
+@pytest.fixture(scope='session')
+def haskell_logging(request: FixtureRequest, booster_log_dir: Path | None) -> bool:
+    return bool(request.config.getoption('--haskell-logging')) or booster_log_dir is not None
+
+
+@pytest.fixture(scope='session')
+def booster_log_levels(request: FixtureRequest) -> list[str] | None:
+    """
+    Return explicit log entries for the Haskell backend, or None to use the default.
+
+    When None is returned and haskell_logging is True, the harness falls back to
+    DEFAULT_HASKELL_LOG_ENTRIES. Set via --booster-log-levels on the command line:
+        pytest ... --booster-log-levels Abort,Rewrite,SMT
+    """
+    return _csv_option(request.config.getoption('--booster-log-levels'))
+
+
+@pytest.fixture(scope='session')
+def booster_only_simplify(request: FixtureRequest) -> bool:
+    return request.config.getoption('--booster-only-simplify')