Implement first past of KFlatModule conversion to Kore (#835)

This PR is to begin a refactoring needed for CSE, and also begin work on
implementing the skeleton of ModuleToKORE in pyk.

- A new routine is added to `konvert` for `kflatmodule_to_kore`, which
converts modules which contain only rules and imports to Kore.
- This routine is used for building up the dependencies and
circularities modules in initializing the `APRProver`, and then putting
them into the `add_module` endpoint directly.
- The code `KCFG.as_claim` is turned into a simpler `KCFG.as_rule`,
which uses existing routines instead of making a new one. This uses the
`cterm` modules `build_rule` functionality, which is adjusted to not
strip out information needed for making backend-compatible rules
(previously this routine was used for display purposes only).
- Old code for handling the dependencies/circularities modules in
`APRProver` is removed.

---------

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

Author: ehildenb

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.592'
-release = '0.1.592'
+version = '0.1.593'
+release = '0.1.593'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.592
+0.1.593

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.592"
+version = "0.1.593"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/cterm.py

@@ -13,10 +13,8 @@
     count_vars,
     flatten_label,
     free_vars,
-    minimize_rule,
     ml_pred_to_bool,
     push_down_rewrites,
-    remove_generated_cells,
     simplify_bool,
     split_config_and_constraints,
     split_config_from,
@@ -429,13 +427,13 @@ def build_rule(
     (init_config, init_constraint) = split_config_and_constraints(init_term)
     (final_config, final_constraint) = split_config_and_constraints(final_term)
 
-    rule_body = remove_generated_cells(push_down_rewrites(KRewrite(init_config, final_config)))
+    rule_body = push_down_rewrites(KRewrite(init_config, final_config))
     rule_requires = simplify_bool(ml_pred_to_bool(init_constraint))
     rule_ensures = simplify_bool(ml_pred_to_bool(final_constraint))
     att_dict = {} if priority is None else {'priority': str(priority)}
     rule_att = KAtt(atts=att_dict)
 
     rule = KRule(rule_body, requires=rule_requires, ensures=rule_ensures, att=rule_att)
     rule = rule.update_atts({'label': rule_id})
-    new_keep_vars = [v_subst[v].name if v in v_subst else v for v in keep_vars]
-    return (minimize_rule(rule, keep_vars=new_keep_vars), Subst(vremap_subst))
+
+    return (rule, Subst(vremap_subst))

src/pyk/kcfg/explore.py

@@ -18,10 +18,7 @@
     ml_pred_to_bool,
     push_down_rewrites,
 )
-from ..kast.outer import KRule
-from ..konvert import krule_to_kore
 from ..kore.rpc import AbortedResult, RewriteSuccess, SatResult, StopReason, UnknownResult, UnsatResult
-from ..kore.syntax import Import, Module
 from ..prelude import k
 from ..prelude.k import GENERATED_TOP_CELL
 from ..prelude.kbool import notBool
@@ -36,10 +33,8 @@
     from typing import Final
 
     from ..kast import KInner
-    from ..kast.outer import KClaim
     from ..kcfg.exploration import KCFGExploration
     from ..kore.rpc import KoreClient, LogEntry
-    from ..kore.syntax import Sentence
     from ..ktool.kprint import KPrint
     from .kcfg import NodeIdLike
     from .semantics import KCFGSemantics
@@ -525,22 +520,6 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]:
             case _:
                 raise AssertionError()
 
-    def add_dependencies_module(
-        self, old_module_name: str, new_module_name: str, dependencies: Iterable[KClaim], priority: int = 1
-    ) -> None:
-        kast_rules = [
-            KRule(body=c.body, requires=c.requires, ensures=c.ensures, att=c.att.update({'priority': priority}))
-            for c in dependencies
-        ]
-        kore_axioms: list[Sentence] = [
-            krule_to_kore(self.kprint.definition, self.kprint.kompiled_kore, r) for r in kast_rules
-        ]
-        sentences: list[Sentence] = [Import(module_name=old_module_name, attrs=())]
-        sentences = sentences + kore_axioms
-        m = Module(name=new_module_name, sentences=sentences)
-        _LOGGER.info(f'Adding dependencies module {self.id}: {new_module_name}')
-        self._kore_client.add_module(m)
-
 
 class ExtendResult(ABC):
     ...

src/pyk/konvert.py

@@ -7,6 +7,7 @@
 from .cterm import CTerm
 from .kast.inner import KApply, KLabel, KSequence, KSort, KToken, KVariable
 from .kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs
+from .kast.outer import KRule
 from .kore.prelude import BYTES as KORE_BYTES
 from .kore.prelude import DOTK, SORT_K
 from .kore.prelude import STRING as KORE_STRING
@@ -22,8 +23,10 @@
     EVar,
     Exists,
     Implies,
+    Import,
     MLPattern,
     MLQuant,
+    Module,
     Not,
     Rewrites,
     SortApp,
@@ -41,9 +44,9 @@
     from typing import Final
 
     from .kast import KInner
-    from .kast.outer import KDefinition, KRule
+    from .kast.outer import KDefinition, KFlatModule, KImport
     from .kore.kompiled import KompiledKore
-    from .kore.syntax import Pattern, Sort
+    from .kore.syntax import Pattern, Sentence, Sort
 
 _LOGGER: Final = logging.getLogger(__name__)
 
@@ -138,6 +141,20 @@ def krule_to_kore(kast_defn: KDefinition, kompiled_kore: KompiledKore, krule: KR
     return axiom
 
 
+def kflatmodule_to_kore(kast_defn: KDefinition, kompiled_kore: KompiledKore, kflatmodule: KFlatModule) -> Module:
+    kore_axioms: list[Sentence] = []
+    for sent in kflatmodule.sentences:
+        if type(sent) is not KRule:
+            raise ValueError(f'Cannot convert sentence to Kore: {sent}')
+        kore_axioms.append(krule_to_kore(kast_defn, kompiled_kore, sent))
+    imports: list[Sentence] = [_kimport_to_kore(kimport) for kimport in kflatmodule.imports]
+    return Module(name=kflatmodule.name, sentences=(imports + kore_axioms))
+
+
+def _kimport_to_kore(kimport: KImport) -> Import:
+    return Import(module_name=kimport.name, attrs=())
+
+
 def _ksort_to_kore(ksort: KSort) -> SortApp:
     return SortApp('Sort' + ksort.name)
 

src/pyk/proof/reachability.py

@@ -3,16 +3,18 @@
 import graphlib
 import json
 import logging
+import re
 from dataclasses import dataclass
 from typing import TYPE_CHECKING
 
 from pyk.kore.rpc import LogEntry
 
-from ..kast.inner import KInner, KRewrite, KSort, Subst
+from ..kast.inner import KInner, Subst
 from ..kast.manip import flatten_label, ml_pred_to_bool
-from ..kast.outer import KClaim
+from ..kast.outer import KFlatModule, KImport, KRule
 from ..kcfg import KCFG
 from ..kcfg.exploration import KCFGExploration
+from ..konvert import kflatmodule_to_kore
 from ..prelude.kbool import BOOL, TRUE
 from ..prelude.ml import mlAnd, mlEquals, mlTop
 from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single
@@ -24,11 +26,9 @@
     from pathlib import Path
     from typing import Any, Final, TypeVar
 
-    from ..cterm import CTerm
-    from ..kast.outer import KDefinition, KFlatModuleList
+    from ..kast.outer import KClaim, KDefinition, KFlatModuleList
     from ..kcfg import KCFGExplore
     from ..kcfg.kcfg import NodeIdLike
-    from ..ktool.kprint import KPrint
 
     T = TypeVar('T', bound='Proof')
 
@@ -206,17 +206,11 @@ def from_claim(
             **kwargs,
         )
 
-    def as_claim(self, kprint: KPrint) -> KClaim:
-        fr: CTerm = self.kcfg.node(self.init).cterm
-        to: CTerm = self.kcfg.node(self.target).cterm
-        fr_config_sorted = kprint.definition.sort_vars(fr.config, sort=KSort('GeneratedTopCell'))
-        to_config_sorted = kprint.definition.sort_vars(to.config, sort=KSort('GeneratedTopCell'))
-        kc = KClaim(
-            body=KRewrite(fr_config_sorted, to_config_sorted),
-            requires=ml_pred_to_bool(mlAnd(fr.constraints)),
-            ensures=ml_pred_to_bool(mlAnd(to.constraints)),
-        )
-        return kc
+    def as_rule(self, priority: int = 20) -> KRule:
+        _edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=())
+        _rule = _edge.to_rule('BASIC-BLOCK', priority=priority)
+        assert type(_rule) is KRule
+        return _rule
 
     @staticmethod
     def from_spec_modules(
@@ -644,6 +638,13 @@ def __init__(
         always_check_subsumption: bool = True,
         fast_check_subsumption: bool = False,
     ) -> None:
+        def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) -> None:
+            _module = KFlatModule(module_name, sentences, [KImport(import_name)])
+            _kore_module = kflatmodule_to_kore(
+                self.kcfg_explore.kprint.definition, self.kcfg_explore.kprint.kompiled_kore, _module
+            )
+            self.kcfg_explore._kore_client.add_module(_kore_module)
+
         super().__init__(kcfg_explore)
         self.proof = proof
         self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name
@@ -659,22 +660,14 @@ def __init__(
 
         apr_subproofs: list[APRProof] = [pf for pf in subproofs if isinstance(pf, APRProof)]
 
-        dependencies_as_claims: list[KClaim] = [d.as_claim(self.kcfg_explore.kprint) for d in apr_subproofs]
+        dependencies_as_rules: list[KRule] = [d.as_rule(priority=20) for d in apr_subproofs]
+        circularity_rule = proof.as_rule(priority=20)
 
-        self.dependencies_module_name = self.main_module_name + '-DEPENDS-MODULE'
-        self.kcfg_explore.add_dependencies_module(
-            self.main_module_name,
-            self.dependencies_module_name,
-            dependencies_as_claims,
-            priority=1,
-        )
-        self.circularities_module_name = self.main_module_name + '-CIRCULARITIES-MODULE'
-        self.kcfg_explore.add_dependencies_module(
-            self.main_module_name,
-            self.circularities_module_name,
-            dependencies_as_claims + ([proof.as_claim(self.kcfg_explore.kprint)] if proof.circularity else []),
-            priority=1,
-        )
+        module_name = re.sub(r'[%().:,]+', '-', self.proof.id.upper())
+        self.dependencies_module_name = module_name + '-DEPENDS-MODULE'
+        self.circularities_module_name = module_name + '-CIRCULARITIES-MODULE'
+        _inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules)
+        _inject_module(self.circularities_module_name, self.dependencies_module_name, [circularity_rule])
 
         self._checked_for_terminal = set()
         self._checked_for_subsumption = set()