Simplify and compact kompilation for Haskell vs Booster (#2144)

* kevm-pyk/kompile: use haskell_binary when kompiling Booster too

* kevm-pyk/{kompile,__main__}: remove KompileTarget.HASKELL_BOOSTER

* tests/integration/test_prove: simplify given that we always kompile with booster

* Set Version: 1.0.359

* kevm-pyk/cli: update documentation

* fix haskell-booster references

* Set Version: 1.0.372

* Set Version: 1.0.376

* Set Version: 1.0.377

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>
Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>

VERIFICATION.md

@@ -18,12 +18,12 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile-spec sum-to-n-spec.k --target haskell-booster --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile-spec sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
 ```
 
 In this example, the arguments used are:
 
-  - `--target haskell-booster`: specify which symbolic backend to use for reasoning.
+  - `--target haskell`: specify which symbolic backend to use for reasoning.
   - `--syntax-module VERIFICATION`: explicitly state the syntax module.
   - `--main-module VERIFICATION`: explicitly state the main module.
   - `--definition sum-to-n-spec/haskell`: the path where the kompiled definition is stored.

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.376"
+version = "1.0.377"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.376'
+VERSION: Final = '1.0.377'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -110,12 +110,10 @@ def exec_kompile_spec(
     **kwargs: Any,
 ) -> None:
     if target is None:
-        target = KompileTarget.HASKELL_BOOSTER
+        target = KompileTarget.HASKELL
 
-    if target not in [KompileTarget.HASKELL, KompileTarget.HASKELL_BOOSTER, KompileTarget.MAUDE]:
-        raise ValueError(
-            f'Can only call kevm kompile-spec with --target [haskell,haskell-booster,maude], got: {target.value}'
-        )
+    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()
 
@@ -683,7 +681,7 @@ def parse(s: str) -> list[T]:
         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|haskell-booster|maude]')
+    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-pyk/src/kevm_pyk/cli.py

@@ -170,7 +170,7 @@ def rpc_args(self) -> ArgumentParser:
             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",
+            help='Use the booster RPC server instead of kore-rpc.',
         )
         args.add_argument(
             '--port',

kevm-pyk/src/kevm_pyk/kompile.py

@@ -28,15 +28,14 @@
 class KompileTarget(Enum):
     LLVM = 'llvm'
     HASKELL = 'haskell'
-    HASKELL_BOOSTER = 'haskell-booster'
     MAUDE = 'maude'
 
     @property
     def md_selector(self) -> str:
         match self:
             case self.LLVM:
                 return 'k & ! symbolic'
-            case self.HASKELL | self.HASKELL_BOOSTER | self.MAUDE:
+            case self.HASKELL | self.MAUDE:
                 return 'k & ! concrete'
             case _:
                 raise AssertionError()
@@ -140,13 +139,6 @@ def run_kompile(
                 )
                 return kompile(output_dir=output_dir, debug=debug, verbose=verbose)
 
-            case KompileTarget.HASKELL:
-                kompile = HaskellKompile(
-                    base_args=base_args,
-                    haskell_binary=haskell_binary,
-                )
-                return kompile(output_dir=output_dir, debug=debug, verbose=verbose)
-
             case KompileTarget.MAUDE:
                 kompile_maude = MaudeKompile(
                     base_args=base_args,
@@ -170,7 +162,7 @@ def _kompile_haskell() -> None:
 
                 return output_dir
 
-            case KompileTarget.HASKELL_BOOSTER:
+            case KompileTarget.HASKELL:
                 base_args_llvm = KompileArgs(
                     main_file=main_file,
                     main_module=main_module,
@@ -184,7 +176,7 @@ def _kompile_haskell() -> None:
                 kompile_llvm = LLVMKompile(
                     base_args=base_args_llvm, ccopts=ccopts, opt_level=optimization, llvm_kompile_type=LLVMKompileType.C
                 )
-                kompile_haskell = HaskellKompile(base_args=base_args)
+                kompile_haskell = HaskellKompile(base_args=base_args, haskell_binary=haskell_binary)
 
                 def _kompile_llvm() -> None:
                     kompile_llvm(output_dir=llvm_library, debug=debug, verbose=verbose)

kevm-pyk/src/tests/integration/test_prove.py

@@ -112,15 +112,11 @@ def exclude_list(exclude_file: Path) -> list[Path]:
 class Target(NamedTuple):
     main_file: Path
     main_module_name: str
-    use_booster: bool
 
     def __call__(self, output_dir: Path) -> Path:
-        definition_subdir = 'kompiled' if not self.use_booster else 'kompiled-booster'
-        definition_dir = output_dir / definition_subdir
-        target = KompileTarget.HASKELL if not self.use_booster else KompileTarget.HASKELL_BOOSTER
         return kevm_kompile(
-            output_dir=definition_dir,
-            target=target,
+            output_dir=output_dir / 'kompiled',
+            target=KompileTarget.HASKELL,
             main_file=self.main_file,
             main_module=self.main_module_name,
             syntax_module=self.main_module_name,
@@ -129,12 +125,12 @@ def __call__(self, output_dir: Path) -> Path:
 
 
 @pytest.fixture(scope='module')
-def kompiled_target_for(tmp_path_factory: TempPathFactory) -> Callable[[Path, bool], Path]:
+def kompiled_target_for(tmp_path_factory: TempPathFactory) -> Callable[[Path], Path]:
     cache_dir = tmp_path_factory.mktemp('target')
     cache: dict[Target, Path] = {}
 
-    def kompile(spec_file: Path, use_booster: bool) -> Path:
-        target = _target_for_spec(spec_file, use_booster=use_booster)
+    def kompile(spec_file: Path) -> Path:
+        target = _target_for_spec(spec_file)
 
         if target not in cache:
             output_dir = cache_dir / f'{target.main_file.stem}-{len(cache)}'
@@ -146,13 +142,13 @@ def kompile(spec_file: Path, use_booster: bool) -> Path:
     return kompile
 
 
-def _target_for_spec(spec_file: Path, use_booster: bool) -> Target:
+def _target_for_spec(spec_file: Path) -> Target:
     spec_file = spec_file.resolve()
     spec_id = str(spec_file.relative_to(SPEC_DIR))
     spec_root = SPEC_DIR / spec_file.relative_to(SPEC_DIR).parents[-2]
     main_file = spec_root / KOMPILE_MAIN_FILE.get(spec_id, 'verification.k')
     main_module_name = KOMPILE_MAIN_MODULE.get(spec_id, 'VERIFICATION')
-    return Target(main_file, main_module_name, use_booster)
+    return Target(main_file, main_module_name)
 
 
 # ---------
@@ -185,7 +181,7 @@ def leaf_number(proof: APRProof) -> int:
 )
 def test_pyk_prove(
     spec_file: Path,
-    kompiled_target_for: Callable[[Path, bool], Path],
+    kompiled_target_for: Callable[[Path], Path],
     tmp_path: Path,
     caplog: LogCaptureFixture,
     use_booster: bool,
@@ -203,7 +199,7 @@ def test_pyk_prove(
 
     # When
     try:
-        definition_dir = kompiled_target_for(spec_file, use_booster)
+        definition_dir = kompiled_target_for(spec_file)
         exec_prove(
             spec_file=spec_file,
             definition_dir=definition_dir,
@@ -250,7 +246,7 @@ def test_pyk_prove(
 )
 def test_kprove_prove(
     spec_file: Path,
-    kompiled_target_for: Callable[[Path, bool], Path],
+    kompiled_target_for: Callable[[Path], Path],
     tmp_path: Path,
     caplog: LogCaptureFixture,
     bug_report: BugReport | None,
@@ -274,7 +270,7 @@ def test_kprove_prove(
 
     # When
     try:
-        definition_dir = kompiled_target_for(spec_file, False)
+        definition_dir = kompiled_target_for(spec_file)
         kevm = KEVM(definition_dir, use_directory=use_directory)
         actual = kevm.prove(spec_file=spec_file, include_dirs=list(config.INCLUDE_DIRS), **args)
     except BaseException:

package/test-package.sh

@@ -35,7 +35,7 @@ kevm kompile-spec tests/specs/benchmarks/verification.k             \
     --output-definition tests/specs/benchmarks/verification/haskell \
     --main-module VERIFICATION                                      \
     --syntax-module VERIFICATION                                    \
-    --target haskell-booster                                        \
+    --target haskell                                                \
     --verbose
 
 kevm prove tests/specs/benchmarks/structarg00-spec.k         \

package/version

@@ -1 +1 @@
-1.0.376
+1.0.377