Thread Haskell-backend logging and booster-only-simplify flags

src/kontrol/cli.py

@@ -7,7 +7,7 @@
 
 from kevm_pyk.cli import KEVMCLIArgs, node_id_like
 from kevm_pyk.utils import arg_pair_of
-from pyk.cli.utils import dir_path, file_path
+from pyk.cli.utils import dir_path, file_path, list_of
 from pyk.utils import ensure_dir_path
 
 from .options import (
@@ -228,6 +228,28 @@ def rpc_args(self) -> ArgumentParser:
                 'Format is <file>:<module name>.'
             ),
         )
+        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.',
+        )
+        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.',
+        )
         return args
 
 

src/kontrol/display.py

@@ -159,6 +159,9 @@ def foundry_show(
             id=test_id,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
+            haskell_log_entries=options.haskell_log_entries,
+            haskell_log_dir=options.haskell_log_dir,
+            booster_only_simplify=options.booster_only_simplify,
             start_server=start_server,
             port=options.port,
             extra_module=foundry.load_lemmas(options.lemmas),

src/kontrol/foundry.py

@@ -1203,6 +1203,9 @@ def foundry_simplify_node(
         smt_tactic=options.smt_tactic,
         log_succ_rewrites=options.log_succ_rewrites,
         log_fail_rewrites=options.log_fail_rewrites,
+        haskell_log_entries=options.haskell_log_entries,
+        haskell_log_dir=options.haskell_log_dir,
+        booster_only_simplify=options.booster_only_simplify,
         start_server=start_server,
         port=options.port,
         extra_module=foundry.load_lemmas(options.lemmas),
@@ -1292,6 +1295,9 @@ def foundry_step_node(
         smt_tactic=options.smt_tactic,
         log_succ_rewrites=options.log_succ_rewrites,
         log_fail_rewrites=options.log_fail_rewrites,
+        haskell_log_entries=options.haskell_log_entries,
+        haskell_log_dir=options.haskell_log_dir,
+        booster_only_simplify=options.booster_only_simplify,
         start_server=start_server,
         port=options.port,
         extra_module=foundry.load_lemmas(options.lemmas),
@@ -1327,6 +1333,9 @@ def foundry_section_edge(
         smt_tactic=options.smt_tactic,
         log_succ_rewrites=options.log_succ_rewrites,
         log_fail_rewrites=options.log_fail_rewrites,
+        haskell_log_entries=options.haskell_log_entries,
+        haskell_log_dir=options.haskell_log_dir,
+        booster_only_simplify=options.booster_only_simplify,
         start_server=start_server,
         port=options.port,
         extra_module=foundry.load_lemmas(options.lemmas),
@@ -1374,6 +1383,9 @@ def foundry_get_model(
         smt_tactic=options.smt_tactic,
         log_succ_rewrites=options.log_succ_rewrites,
         log_fail_rewrites=options.log_fail_rewrites,
+        haskell_log_entries=options.haskell_log_entries,
+        haskell_log_dir=options.haskell_log_dir,
+        booster_only_simplify=options.booster_only_simplify,
         start_server=start_server,
         port=options.port,
         extra_module=foundry.load_lemmas(options.lemmas),

src/kontrol/options.py

@@ -18,6 +18,7 @@
 from kevm_pyk.utils import arg_pair_of
 from pyk.cli.args import BugReportOptions, KompileOptions, LoggingOptions, Options, ParallelOptions, SMTOptions
 from pyk.cli.utils import dir_path, file_path
+from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES
 from pyk.utils import ensure_dir_path
 
 from .utils import parse_test_version_tuple
@@ -64,6 +65,9 @@ class RpcOptions(Options):
     use_booster: bool
     port: int | None
     lemmas: str | None
+    haskell_log_entries: list[str]
+    haskell_log_dir: Path | None
+    booster_only_simplify: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -74,6 +78,9 @@ def default() -> dict[str, Any]:
             'use_booster': True,
             'port': None,
             'lemmas': None,
+            'haskell_log_entries': list(HASKELL_LOGGING_ENTRIES),
+            'haskell_log_dir': None,
+            'booster_only_simplify': False,
         }
 
     @staticmethod

src/kontrol/prove.py

@@ -375,6 +375,9 @@ def create_kcfg_explore() -> KCFGExplore:
                     foundry.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,
+                    haskell_log_dir=options.haskell_log_dir,
                 )
                 return KCFGExplore(
                     cterm_symbolic,

src/tests/conftest.py

@@ -1,13 +1,12 @@
 from __future__ import annotations
 
+from pathlib import Path
 from typing import TYPE_CHECKING
 
 import pytest
 from pyk.cli.utils import dir_path
 
 if TYPE_CHECKING:
-    from pathlib import Path
-
     from pytest import FixtureRequest, Parser
 
 
@@ -29,6 +28,12 @@ def pytest_addoption(parser: Parser) -> None:
         action='store_true',
         help='Use sequential, single-threaded proof loop.',
     )
+    parser.addoption(
+        '--haskell-log-dir',
+        type=Path,
+        default=None,
+        help='Capture per-request Haskell-backend log bundles (one <request-id>.jsonl per RPC) under this directory for proof tests.',
+    )
 
 
 @pytest.fixture(scope='session')
@@ -44,3 +49,11 @@ def update_expected_output(request: FixtureRequest) -> bool:
 @pytest.fixture(scope='session')
 def force_sequential(request: FixtureRequest) -> bool:
     return request.config.getoption('--force-sequential')
+
+
+@pytest.fixture(scope='session')
+def haskell_log_dir(request: FixtureRequest) -> Path | None:
+    d: Path | None = request.config.getoption('--haskell-log-dir')
+    if d is not None:
+        d.mkdir(parents=True, exist_ok=True)
+    return d

src/tests/integration/test_foundry_prove.py

@@ -89,6 +89,7 @@ def test_foundry_prove(
     bug_report: BugReport | None,
     server: KoreServer,
     force_sequential: bool,
+    haskell_log_dir: Path | None,
 ) -> None:
     if test_id in SKIPPED_PROVE_TESTS or (update_expected_output and not test_id in SHOW_TESTS):
         pytest.skip()
@@ -107,6 +108,7 @@ def test_foundry_prove(
                 'usegas': test_id in GAS_TESTS,
                 'port': server.port,
                 'force_sequential': force_sequential,
+                'haskell_log_dir': haskell_log_dir,
             }
         ),
     )

src/tests/unit/test_toml_args.py

@@ -5,8 +5,15 @@
 from typing import TYPE_CHECKING
 
 from pyk.cli.pyk import parse_toml_args
+from pyk.cterm.symbolic import HASKELL_LOGGING_ENTRIES
 
-from kontrol.cli import _create_argument_parser, get_argument_type_setter, get_option_string_destination
+from kontrol.cli import (
+    _create_argument_parser,
+    generate_options,
+    get_argument_type_setter,
+    get_option_string_destination,
+)
+from kontrol.options import ProveOptions
 
 from .utils import TEST_DATA_DIR
 
@@ -101,3 +108,36 @@ def test_toml_profiles() -> None:
     assert args_dict['workers'] == 5
     assert 'smt_timeout' in args_dict
     assert args_dict['smt_timeout'] == 1000
+
+
+def _prove_options(cmd_args: list[str]) -> ProveOptions:
+    parser = _create_argument_parser()
+    args = parser.parse_args(['prove', *cmd_args])
+    stripped_args = {
+        key: val for (key, val) in vars(args).items() if val is not None and not (isinstance(val, Iterable) and not val)
+    }
+    options = generate_options(stripped_args)
+    assert isinstance(options, ProveOptions)
+    return options
+
+
+def test_haskell_logging_options() -> None:
+    options = _prove_options(
+        [
+            '--haskell-log-dir',
+            '/tmp/hlog',
+            '--haskell-log-entries',
+            'Abort,Simplify,Rewrite',
+            '--booster-only-simplify',
+        ]
+    )
+    assert options.haskell_log_dir == Path('/tmp/hlog')
+    assert options.haskell_log_entries == ['Abort', 'Simplify', 'Rewrite']
+    assert options.booster_only_simplify is True
+
+
+def test_haskell_logging_option_defaults() -> None:
+    options = _prove_options([])
+    assert options.haskell_log_dir is None
+    assert options.haskell_log_entries == list(HASKELL_LOGGING_ENTRIES)
+    assert options.booster_only_simplify is False