Enable booster backend

package/version

@@ -1 +1 @@
-0.1.35
+0.1.36

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.35"
+version = "0.1.36"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/komet/kdist/plugin.py

@@ -6,7 +6,7 @@
 
 from pyk.kbuild.utils import k_version
 from pyk.kdist.api import Target
-from pyk.ktool.kompile import kompile
+from pyk.ktool.kompile import LLVMKompileType, kompile
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Mapping
@@ -56,6 +56,17 @@ def deps(self) -> tuple[str]:
             'warnings_to_errors': True,
         },
     ),
+    'llvm-library': KompileTarget(
+        lambda src_dir: {
+            'backend': 'llvm',
+            'llvm_kompile_type': LLVMKompileType.C,
+            'main_file': src_dir / 'soroban-semantics/kasmer.md',
+            'syntax_module': 'KASMER-SYNTAX',
+            'include_dirs': [src_dir],
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
     'haskell': KompileTarget(
         lambda src_dir: {
             'backend': 'haskell',

src/komet/proof.py

@@ -8,7 +8,7 @@
 from pyk.kcfg.semantics import DefaultSemantics
 from pyk.proof import APRProof, APRProver
 
-from .utils import symbolic_definition
+from .utils import library_definition, symbolic_definition
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -23,6 +23,7 @@ def _explore_context(id: str, bug_report: BugReport | None) -> Iterator[KCFGExpl
     with cterm_symbolic(
         definition=symbolic_definition.kdefinition,
         definition_dir=symbolic_definition.path,
+        llvm_definition_dir=library_definition.path,
         id=id if bug_report else None,
         bug_report=bug_report,
     ) as cts:

src/komet/utils.py

@@ -64,4 +64,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any)
 
 
 concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm'))
+library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library'))
 symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell'))