Enable SimpleSub type inference mode for kompile and kprove (#2421)

* Add type_inference_mode parameter to kevm_kompile

* Set type_inference_mode default to CHECKED for a CI run

* Set Version: 1.0.549

* Set Version: 1.0.552

* Change back to SIMPLESUB mode for merge

---------

Co-authored-by: devops <[email protected]>

Author: Scott-Guest

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/kompile.py

@@ -8,6 +8,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.kdist import kdist
+from pyk.ktool import TypeInferenceMode
 from pyk.ktool.kompile import HaskellKompile, KompileArgs, LLVMKompile, LLVMKompileType, MaudeKompile
 from pyk.utils import run_process
 
@@ -61,6 +62,7 @@ def kevm_kompile(
     debug_build: bool = False,
     debug: bool = False,
     verbose: bool = False,
+    type_inference_mode: str | TypeInferenceMode | None = None,
 ) -> Path:
     if plugin_dir is None:
         plugin_dir = kdist.get('evm-semantics.plugin')
@@ -83,6 +85,7 @@ def kevm_kompile(
         debug_build=debug_build,
         debug=debug,
         verbose=verbose,
+        type_inference_mode=type_inference_mode,
     )
 
 
@@ -104,10 +107,14 @@ def run_kompile(
     debug_build: bool = False,
     debug: bool = False,
     verbose: bool = False,
+    type_inference_mode: str | TypeInferenceMode | None = None,
 ) -> Path:
     if llvm_library is None:
         llvm_library = output_dir / 'llvm-library'
 
+    if type_inference_mode is None:
+        type_inference_mode = TypeInferenceMode.SIMPLESUB
+
     include_dirs = [Path(include) for include in includes]
     include_dirs += config.INCLUDE_DIRS
 
@@ -136,7 +143,9 @@ def run_kompile(
                     llvm_kompile_type=llvm_kompile_type,
                     enable_llvm_debug=enable_llvm_debug,
                 )
-                return kompile(output_dir=output_dir, debug=debug, verbose=verbose)
+                return kompile(
+                    output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                )
 
             case KompileTarget.MAUDE:
                 kompile_maude = MaudeKompile(
@@ -147,10 +156,14 @@ def run_kompile(
                 maude_dir = output_dir / 'kompiled-maude'
 
                 def _kompile_maude() -> None:
-                    kompile_maude(output_dir=maude_dir, debug=debug, verbose=verbose)
+                    kompile_maude(
+                        output_dir=maude_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                    )
 
                 def _kompile_haskell() -> None:
-                    kompile_haskell(output_dir=output_dir, debug=debug, verbose=verbose)
+                    kompile_haskell(
+                        output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                    )
 
                 with concurrent.futures.ThreadPoolExecutor(max_workers=2) as executor:
                     futures = [
@@ -178,10 +191,14 @@ def _kompile_haskell() -> None:
                 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)
+                    kompile_llvm(
+                        output_dir=llvm_library, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                    )
 
                 def _kompile_haskell() -> None:
-                    kompile_haskell(output_dir=output_dir, debug=debug, verbose=verbose)
+                    kompile_haskell(
+                        output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                    )
 
                 with concurrent.futures.ThreadPoolExecutor(max_workers=2) as executor:
                     futures = [

kevm-pyk/src/kevm_pyk/utils.py

@@ -22,6 +22,7 @@
 from pyk.kast.outer import KSequence
 from pyk.kcfg import KCFGExplore
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server
+from pyk.ktool import TypeInferenceMode
 from pyk.proof import APRProof, APRProver
 from pyk.proof.implies import EqualityProof, ImpliesProver
 from pyk.proof.proof import parallel_advance_proof
@@ -87,6 +88,7 @@ def get_apr_proof_for_spec(
             md_selector=md_selector,
             claim_labels=claim_labels,
             exclude_claim_labels=exclude_claim_labels,
+            type_inference_mode=TypeInferenceMode.SIMPLESUB,
         )
     )
 

package/version

@@ -1 +1 @@
-1.0.551
+1.0.552