Inject ccopts directly into kevm_kompile and fix some tests

Makefile

@@ -59,7 +59,7 @@ test-prove-kprove: tests/specs/opcodes/evm-optimizations-spec.md poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_kprove_prove"
 
 # to generate optimizations.md, run: ./optimizer/optimize.sh &> output
-tests/specs/opcodes/evm-optimizations-spec.md:
+tests/specs/opcodes/evm-optimizations-spec.md: kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
 	cat kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md | sed 's/^rule/claim/' | sed 's/EVM-OPTIMIZATIONS/EVM-OPTIMIZATIONS-SPEC/' | grep -v 'priority(40)' > $@
 
 
@@ -108,7 +108,7 @@ tests/specs/%.prove: tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$*))/$
 		--definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(TEST_SYMBOLIC_BACKEND)
 
 tests/specs/%/timestamp: tests/specs/$$(firstword $$(subst /, ,$$*))/$$(KPROVE_FILE).$$(KPROVE_EXT)
-	$(POETRY_RUN) kevm-pyk kompile                                                                             \
+	$(POETRY_RUN) kevm-pyk kompile-spec                                                                         \
 		$<                                                                                                      \
 		--target $(word 3, $(subst /, , $*))                                                                    \
 		--output-definition tests/specs/$(firstword $(subst /, ,$*))/$(KPROVE_FILE)/$(word 3, $(subst /, , $*)) \

README.md

@@ -207,7 +207,7 @@ Finally, you can build the semantics.
 poetry -C kevm-pyk run kevm-dist --verbose build -j4
 ```
 
-You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone}`, e.g.:
+You can build specific targets using options `evm-semantics.{llvm,haskell,haskell-standalone,plugin}`, e.g.:
 
 ```sh
 poetry -C kevm-pyk run kevm-dist build -j2 evm-semantics.llvm evm-semantics.haskell

VERIFICATION.md

@@ -18,13 +18,12 @@ It has two modules:
 The first step is kompiling the `.k` file with the below command.
 
 ```sh
-kevm kompile sum-to-n-spec.k --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
+kevm kompile-spec sum-to-n-spec.k --target haskell-booster --syntax-module VERIFICATION --main-module VERIFICATION --definition sum-to-n-spec/haskell
 ```
 
 In this example, the arguments used are:
 
-  - `—-pyk`: a flag that enables the pyk library.
-  - `—-backend haskell`: used to kompile the definition with the Haskell backend, enabling the symbolic execution ([more about it here]).
+  - `--target haskell-booster`: 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.
@@ -61,7 +60,7 @@ These rules are then used in the claims. As an example, the `#binRuntime(ERC20)`
 Following this, we can compile the Markdown file with:
 
 ```sh
-kevm kompile erc20-spec.md --target haskell --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
+kevm kompile-spec erc20-spec.md --syntax-module VERIFICATION --main-module VERIFICATION --definition erc20-spec/haskell
 ```
 
 Next, run the prover with:
@@ -101,7 +100,7 @@ A running example:
 
 ```sh
 mkdir kcfgs
-kevm kompile --target haskell tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
+kevm kompile-spec tests/specs/benchmarks/verification.k --definition tests/specs/benchmarks/verification/haskell --main-module VERIFICATION --syntax-module VERIFICATION
 kevm prove tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell --verbose --save-directory kcfgs
 kevm view-kcfg --verbose kcfgs tests/specs/benchmarks/address00-spec.k --definition tests/specs/benchmarks/verification/haskell
 ```

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.355"
+version = "1.0.356"
 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.355'
+VERSION: Final = '1.0.356'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -33,7 +33,7 @@
 from .cli import KEVMCLIArgs, node_id_like
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
-from .kompile import KompileTarget, kevm_kompile
+from .kompile import KompileTarget, kevm_kompile, lib_ccopts
 from .utils import (
     claim_dependency_dict,
     ensure_ksequence_on_k_cell,
@@ -87,7 +87,7 @@ def exec_version(**kwargs: Any) -> None:
     print(f'KEVM Version: {VERSION}')
 
 
-def exec_kompile(
+def exec_kompile_spec(
     output_dir: Path | None,
     main_file: Path,
     emit_json: bool,
@@ -109,7 +109,12 @@ def exec_kompile(
     **kwargs: Any,
 ) -> None:
     if target is None:
-        target = KompileTarget.LLVM
+        target = KompileTarget.HASKELL_BOOSTER
+
+    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}'
+        )
 
     output_dir = output_dir or Path()
 
@@ -123,6 +128,8 @@ def exec_kompile(
     if debug_build:
         optimization = 0
 
+    ccopts = list(ccopts) + lib_ccopts(kdist.get('evm-semantics.plugin'), debug_build=debug_build)
+
     kevm_kompile(
         target,
         output_dir=output_dir,
@@ -671,17 +678,17 @@ def parse(s: str) -> list[T]:
 
     command_parser.add_parser('version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args])
 
-    kevm_kompile_args = command_parser.add_parser(
-        'kompile',
+    kevm_kompile_spec_args = command_parser.add_parser(
+        'kompile-spec',
         help='Kompile KEVM specification.',
         parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args],
     )
-    kevm_kompile_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
-    kevm_kompile_args.add_argument('--target', type=KompileTarget, help='[llvm|haskell|haskell-booster]')
-    kevm_kompile_args.add_argument(
+    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(
         '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.'
     )
-    kevm_kompile_args.add_argument(
+    kevm_kompile_spec_args.add_argument(
         '--debug-build', dest='debug_build', default=False, help='Enable debug symbols in LLVM builds.'
     )
 

kevm-pyk/src/kevm_pyk/kdist/plugin.py

@@ -6,8 +6,8 @@
 from pyk.kbuild.utils import sync_files
 from pyk.utils import run_process
 
-from .. import config
-from ..kompile import KompileTarget, kevm_kompile
+from .. import config, kdist
+from ..kompile import KompileTarget, kevm_kompile, lib_ccopts
 from .api import Target
 
 if TYPE_CHECKING:
@@ -27,12 +27,15 @@ def __init__(self, kompile_args: Mapping[str, Any], *, deps: Iterable[str] | Non
     def build(self, output_dir: Path, deps: dict[str, Path], args: dict[str, Any]) -> None:
         verbose = args.get('verbose', False)
         enable_llvm_debug = args.get('enable_llvm_debug', False)
+        debug_build = args.get('debug_build', False)
+        ccopts = args.get('ccopts', [])
 
+        ccopts = ccopts + lib_ccopts(kdist.get('evm-semantics.plugin'), debug_build=debug_build)
         kevm_kompile(
             output_dir=output_dir,
             enable_llvm_debug=enable_llvm_debug,
             verbose=verbose,
-            plugin_dir=deps.get('evm-semantics.plugin'),
+            ccopts=ccopts,
             **self._kompile_args,
         )
 

kevm-pyk/src/kevm_pyk/kompile.py

@@ -45,8 +45,8 @@ def md_selector(self) -> str:
 def kevm_kompile(
     target: KompileTarget,
     output_dir: Path,
-    *,
     main_file: Path,
+    *,
     main_module: str | None,
     syntax_module: str | None,
     includes: Iterable[str] = (),
@@ -57,17 +57,13 @@ def kevm_kompile(
     llvm_kompile_type: LLVMKompileType | None = None,
     enable_llvm_debug: bool = False,
     llvm_library: Path | None = None,
-    plugin_dir: Path | None = None,
     debug_build: bool = False,
     debug: bool = False,
     verbose: bool = False,
 ) -> Path:
     if llvm_library is None:
         llvm_library = output_dir / 'llvm-library'
 
-    if target in [KompileTarget.LLVM, KompileTarget.HASKELL_BOOSTER] and not plugin_dir:
-        raise ValueError(f'Parameter plugin_dir is required for target: {target.value}')
-
     include_dirs = [Path(include) for include in includes]
     include_dirs += config.INCLUDE_DIRS
 
@@ -89,8 +85,6 @@ def kevm_kompile(
     try:
         match target:
             case KompileTarget.LLVM:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 kompile = LLVMKompile(
                     base_args=base_args,
                     ccopts=ccopts,
@@ -129,9 +123,8 @@ def _kompile_haskell() -> None:
                     [future.result() for future in futures]
 
                 return output_dir
+
             case KompileTarget.HASKELL_BOOSTER:
-                assert plugin_dir
-                ccopts = list(ccopts) + _lib_ccopts(plugin_dir, kernel, debug_build=debug_build)
                 base_args_llvm = KompileArgs(
                     main_file=main_file,
                     main_module=main_module,
@@ -173,7 +166,9 @@ def _kompile_haskell() -> None:
         raise
 
 
-def _lib_ccopts(plugin_dir: Path, kernel: str, debug_build: bool = False) -> list[str]:
+def lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]:
+    kernel = sys.platform
+
     ccopts = ['-std=c++17']
 
     if debug_build:

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md

@@ -7,7 +7,7 @@ These optimizations work on the LLVM and Haskell backend and are generated by th
 requires "evm.md"
 requires "lemmas/int-simplification.k"
 
-module EVM-OPTIMIZATIONS-LEMMAS [kore, symbolic]
+module EVM-OPTIMIZATIONS-LEMMAS [kore]
     imports EVM
 
     rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]

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

@@ -12,7 +12,7 @@
 from kevm_pyk import config, kdist
 from kevm_pyk.__main__ import exec_prove
 from kevm_pyk.kevm import KEVM
-from kevm_pyk.kompile import KompileTarget, kevm_kompile
+from kevm_pyk.kompile import KompileTarget, kevm_kompile, lib_ccopts
 
 from ..utils import REPO_ROOT
 
@@ -117,16 +117,16 @@ class Target(NamedTuple):
     def __call__(self, output_dir: Path) -> Path:
         definition_subdir = 'kompiled' if not self.use_booster else 'kompiled-booster'
         definition_dir = output_dir / definition_subdir
-        plugin_dir = kdist.get('evm-semantics.plugin') if self.use_booster else None
         target = KompileTarget.HASKELL if not self.use_booster else KompileTarget.HASKELL_BOOSTER
+        ccopts = lib_ccopts(kdist.get('evm-semantics.plugin')) if self.use_booster else []
         return kevm_kompile(
             output_dir=definition_dir,
             target=target,
             main_file=self.main_file,
             main_module=self.main_module_name,
             syntax_module=self.main_module_name,
             includes=[],
-            plugin_dir=plugin_dir,
+            ccopts=ccopts,
             debug=True,
         )
 

package/test-package.sh

@@ -30,3 +30,16 @@ if ! ${APPLE_SILICON:-false}; then
         || git --no-pager diff --no-index --ignore-all-space -R tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
     rm -rf tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.llvm-out
 fi
+
+kevm kompile-spec tests/specs/benchmarks/verification.k             \
+    --output-definition tests/specs/benchmarks/verification/haskell \
+    --main-module VERIFICATION                                      \
+    --syntax-module VERIFICATION                                    \
+    --target haskell-booster                                        \
+    --verbose
+
+kevm prove tests/specs/benchmarks/structarg00-spec.k         \
+    --definition tests/specs/benchmarks/verification/haskell \
+    --save-directory proofs                                  \
+    --verbose                                                \
+    --use-booster

package/version

@@ -1 +1 @@
-1.0.355
+1.0.356

tests/specs/examples/sum-to-n-foundry-spec.k

@@ -4,6 +4,7 @@ requires "gas.md"
 module VERIFICATION
     imports LEMMAS
     imports INFINITE-GAS
+    imports EVM
 
     rule N xorInt maxUInt256 => maxUInt256 -Int N
     requires #rangeUInt(256, N)

tests/specs/functional/infinite-gas-spec.k

@@ -4,6 +4,7 @@ requires "lemmas/lemmas.k"
 module VERIFICATION
     imports INFINITE-GAS
     imports LEMMAS
+    imports EVM
 endmodule
 
 module INFINITE-GAS-SPEC