Basic defunctionalization for building rules in K (#4610)

Currently, when we are converting a summarized K definition to a module,
we have only used it for then feeding that module into the Haskell
backend, which does not have the restriction that the generated rules
cannot have functions on the LHS of them. Now Pi2 wants to also feed
those rules into the LLVM backend, so it's needed that we can
defunctionalize the LHS of those rules.

This PR achieves that by threading through the needed options to
`cterm_build_rule` to defunctionalize the LHS of generated rules. In
particular:

- Some bugs in the imports of
#4607 are fixed. Imports
are made relative, and a circular import path is broken.
- A routine `defunctionalize(KDefinition, KInner) -> tuple[Kinner,
list[KInner]]` is added to `kast.manip`, which replaces functions in the
supplied term with variables and returns also a list of constraints
binding those variables to their original terms.
- A unit test-harness, and many tests, are added of the
`defunctionalize` routine.
- An integration test of `cterm_build_rule` defunctionalization is added
over the `simple_proofs.k` test harness.
- The "functions" `.Map`, `.Set`, `.List`, and `.RangeMap` are added to
the list of "not actually functions, more like constructors" for
considering when deciding if something is a function or a constructor.
This is exercised by the added test because `.Map` shows up, but is not
defunctionalized.
- `KCFG.edge.to_rule`, `cterm_build_rule`, and `build_rule` now take an
optional `KDefinition`, and if it's supplied, will defunctionalize the
LHS of generated rules that it makes.
- The routine in `kast.manip` named `minimize_rule` is renamed to
`minimize_rule_like`, to reflect better its type.
- `KCFG.edge.to_rule` now takes an optional `minimize: bool` parameter,
which if supplied will run the `minimize_rule_like` routine over the
generated rule.

---------

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

pyk/src/pyk/__main__.py

@@ -22,7 +22,7 @@
 from .kast.inner import KInner
 from .kast.manip import (
     flatten_label,
-    minimize_rule,
+    minimize_rule_like,
     minimize_term,
     propagate_up_constraints,
     remove_source_map,
@@ -394,7 +394,7 @@ def exec_coverage(options: CoverageOptions) -> None:
     definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json'))
     pretty_printer = PrettyPrinter(definition)
     for rid in options.coverage_file:
-        rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
+        rule = minimize_rule_like(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
         options.output_file.write('\n\n')
         options.output_file.write('Rule: ' + rid.strip())
         options.output_file.write('\nUnparsed:\n')

pyk/src/pyk/cterm/cterm.py

@@ -367,6 +367,7 @@ def cterm_build_rule(
     final_cterm: CTerm,
     priority: int | None = None,
     keep_vars: Iterable[str] = (),
+    defunc_with: KDefinition | None = None,
 ) -> tuple[KRule, Subst]:
     """Return a `KRule` between the supplied initial and final states.
 
@@ -375,6 +376,8 @@ def cterm_build_rule(
         init_cterm: State to put on LHS of the rule (constraints interpreted as `requires` clause).
         final_cterm: State to put on RHS of the rule (constraints interpreted as `ensures` clause).
         keep_vars: Variables to leave in the side-conditions even if not bound in the configuration.
+        priority: Priority index to use for generated rules.
+        defunc_with (optional): KDefinition to be able to defunctionalize LHS appropriately.
 
     Returns:
         A tuple ``(rule, var_map)`` where
@@ -386,4 +389,13 @@ def cterm_build_rule(
     """
     init_config, *init_constraints = init_cterm
     final_config, *final_constraints = final_cterm
-    return build_rule(rule_id, init_config, final_config, init_constraints, final_constraints, priority, keep_vars)
+    return build_rule(
+        rule_id,
+        init_config,
+        final_config,
+        init_constraints,
+        final_constraints,
+        priority,
+        keep_vars,
+        defunc_with=defunc_with,
+    )

pyk/src/pyk/kast/manip.py

@@ -6,7 +6,7 @@
 
 from ..prelude.k import DOTS, GENERATED_TOP_CELL
 from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
-from ..prelude.ml import is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlOr, mlTop
+from ..prelude.ml import is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlOr, mlTop
 from ..utils import find_common_items, hash_str, unique
 from .att import EMPTY_ATT, Atts, KAtt, WithKAtt
 from .inner import (
@@ -543,7 +543,7 @@ def minimize_term(
     return term
 
 
-def minimize_rule(rule: RL, keep_vars: Iterable[str] = ()) -> RL:
+def minimize_rule_like(rule: RL, keep_vars: Iterable[str] = ()) -> RL:
     """Minimize a K rule or claim for pretty-printing.
 
     - Variables only used once will be removed.
@@ -756,6 +756,7 @@ def build_rule(
     final_constraints: Iterable[KInner] = (),
     priority: int | None = None,
     keep_vars: Iterable[str] = (),
+    defunc_with: KDefinition | None = None,
 ) -> tuple[KRule, Subst]:
     """Return a `KRule` between the supplied initial and final states.
 
@@ -765,7 +766,9 @@ def build_rule(
         final_config: State to put on RHS of the rule.
         init_constraints: Constraints to use as `requires` clause.
         final_constraints: Constraints to use as `ensures` clause.
+        priority: Priority index to assign to generated rules.
         keep_vars: Variables to leave in the side-conditions even if not bound in the configuration.
+        defunc_with: KDefinition for filtering out function symbols on LHS of rules.
 
     Returns:
         A tuple ``(rule, var_map)`` where
@@ -778,6 +781,9 @@ def build_rule(
     init_constraints = [normalize_ml_pred(c) for c in init_constraints]
     final_constraints = [normalize_ml_pred(c) for c in final_constraints]
     final_constraints = [c for c in final_constraints if c not in init_constraints]
+    if defunc_with is not None:
+        init_config, new_constraints = defunctionalize(defunc_with, init_config)
+        init_constraints = init_constraints + new_constraints
     init_term = mlAnd([init_config] + init_constraints)
     final_term = mlAnd([final_config] + final_constraints)
 
@@ -854,3 +860,30 @@ def _no_cell_rewrite_to_dots(_term: KInner) -> KInner:
     subst = Subst({cell_name: _no_cell_rewrite_to_dots(cell_contents) for cell_name, cell_contents in _subst.items()})
 
     return subst(config)
+
+
+def defunctionalize(defn: KDefinition, kinner: KInner) -> tuple[KInner, list[KInner]]:
+    """Turn non-constructor arguments into side-conditions so that a term is only constructor-like.
+
+    Args:
+        defn: The definition to pull function label information from.
+        kinner: The term to defunctionalize.
+
+    Returns:
+        A tuple of the defunctionalized term and the list of constraints generated.
+    """
+    function_symbols = [prod.klabel for prod in defn.functions if prod.klabel is not None]
+    constraints: list[KInner] = []
+
+    def _defunctionalize(_kinner: KInner) -> KInner:
+        if type(_kinner) is KApply and _kinner.label in function_symbols:
+            sort = defn.sort(_kinner)
+            assert sort is not None
+            new_var = abstract_term_safely(_kinner, base_name='F', sort=sort)
+            var_constraint = mlEquals(new_var, _kinner, arg_sort=sort)
+            constraints.append(var_constraint)
+            return new_var
+        return _kinner
+
+    new_kinner = top_down(_defunctionalize, kinner)
+    return (new_kinner, list(unique(constraints)))

pyk/src/pyk/kast/outer.py

@@ -864,6 +864,10 @@ def is_not_actually_function(label: str) -> bool:
                 '_List_',
                 '_Map_',
                 '_RangeMap_',
+                '.Set',
+                '.List',
+                '.Map',
+                '.RangeMap',
                 'SetItem',
                 'ListItem',
                 '_|->_',

pyk/src/pyk/kcfg/exploration.py

@@ -3,6 +3,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.kcfg.kcfg import KCFG, NodeAttr
+from pyk.kcfg.minimize import KCFGMinimizer
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
@@ -109,4 +110,4 @@ def to_dict(self) -> dict[str, Any]:
 
     # Minimizing the KCFG
     def minimize_kcfg(self) -> None:
-        self.kcfg.minimize()
+        KCFGMinimizer(self.kcfg).minimize()

pyk/src/pyk/kcfg/kcfg.py

@@ -18,13 +18,13 @@
     extract_rhs,
     flatten_label,
     inline_cell_maps,
+    minimize_rule_like,
     rename_generated_vars,
     sort_ac_collections,
 )
 from ..kast.outer import KFlatModule
 from ..prelude.kbool import andBool
 from ..utils import ensure_dir_path, not_none
-from .minimize import KCFGMinimizer
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping, MutableMapping
@@ -218,7 +218,14 @@ def to_dict(self) -> dict[str, Any]:
         def from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) -> KCFG.Edge:
             return KCFG.Edge(nodes[dct['source']], nodes[dct['target']], dct['depth'], tuple(dct['rules']))
 
-        def to_rule(self, label: str, claim: bool = False, priority: int | None = None) -> KRuleLike:
+        def to_rule(
+            self,
+            label: str,
+            claim: bool = False,
+            priority: int | None = None,
+            defunc_with: KDefinition | None = None,
+            minimize: bool = False,
+        ) -> KRuleLike:
             def is_ceil_condition(kast: KInner) -> bool:
                 return type(kast) is KApply and kast.label.name == '#Ceil'
 
@@ -234,7 +241,11 @@ def _simplify_config(config: KInner) -> KInner:
             if claim:
                 rule, _ = cterm_build_claim(sentence_id, init_cterm, target_cterm)
             else:
-                rule, _ = cterm_build_rule(sentence_id, init_cterm, target_cterm, priority=priority)
+                rule, _ = cterm_build_rule(
+                    sentence_id, init_cterm, target_cterm, priority=priority, defunc_with=defunc_with
+                )
+            if minimize:
+                rule = minimize_rule_like(rule)
             return rule
 
         def replace_source(self, node: KCFG.Node) -> KCFG.Edge:
@@ -1234,9 +1245,6 @@ def write_cfg_data(self) -> None:
         self._deleted_nodes.clear()
         self._created_nodes.clear()
 
-    def minimize(self) -> None:
-        KCFGMinimizer(self).minimize()
-
     @staticmethod
     def read_cfg_data(cfg_dir: Path) -> KCFG:
         store = KCFGStore(cfg_dir)

pyk/src/pyk/kcfg/minimize.py

@@ -3,13 +3,13 @@
 from functools import reduce
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm
-from pyk.utils import not_none, single
+from ..cterm import CTerm
+from ..utils import not_none, single
 
 if TYPE_CHECKING:
     from collections.abc import Callable
 
-    from pyk.kcfg.kcfg import KCFG, NodeIdLike
+    from .kcfg import KCFG, NodeIdLike
 
 
 class KCFGMinimizer:

pyk/src/pyk/kcfg/show.py

@@ -9,7 +9,7 @@
 from ..kast.manip import (
     flatten_label,
     inline_cell_maps,
-    minimize_rule,
+    minimize_rule_like,
     minimize_term,
     ml_pred_to_bool,
     push_down_rewrites,
@@ -316,7 +316,7 @@ def _process_sentence(sent: KSentence) -> KSentence:
                 sent = sent.let(body=KCFGShow.hide_cells(sent.body, omit_cells))
                 if parseable_output:
                     sent = sent.let(body=remove_generated_cells(sent.body))
-                    sent = minimize_rule(sent)
+                    sent = minimize_rule_like(sent)
             return sent
 
         module = cfg.to_module(module_name)

pyk/src/tests/integration/cterm/test_simple.py

@@ -4,11 +4,9 @@
 
 import pytest
 
-from pyk.cterm import CTerm
+from pyk.cterm import CTerm, cterm_build_rule
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable
-from pyk.prelude.kint import leInt
 from pyk.prelude.ml import mlEqualsTrue, mlTop
-from pyk.prelude.utils import token
 from pyk.testing import CTermSymbolicTest, KPrintTest
 
 from ..utils import K_FILES
@@ -18,7 +16,6 @@
     from typing import Final, Union
 
     from pyk.cterm import CTermSymbolic
-    from pyk.kast.inner import KInner
     from pyk.ktool.kprint import KPrint
 
     STATE = Union[tuple[str, str], tuple[str, str, str]]
@@ -38,9 +35,13 @@
 
 SIMPLIFY_TEST_DATA: Final = (('bytes-return', ('mybytes', '.Map'), (r'b"\x00\x90\xa0\n\xa1\xf1a" ~> .K', '.Map')),)
 
-
-def le_int(n: int, var: str) -> KInner:
-    return mlEqualsTrue(leInt(token(n), KVariable(var)))
+BUILD_RULE_TEST_DATA: Final = (
+    (
+        'functional-lhs',
+        (('mybytes', '.Map'), (r'mybytes ~> .K', '.Map')),
+        ('( F_e096a1bd:KItem => mybytes )', '.Map', 'F_e096a1bd:KItem ==K mybytes', 'true'),
+    ),
+)
 
 
 class TestSimpleProof(CTermSymbolicTest, KPrintTest):
@@ -130,3 +131,36 @@ def test_simplify(
         # Then
         assert actual_k == expected_k
         assert actual_state == expected_state
+
+    @pytest.mark.parametrize(
+        'test_id,pre,expected_post',
+        BUILD_RULE_TEST_DATA,
+        ids=[test_id for test_id, *_ in BUILD_RULE_TEST_DATA],
+    )
+    def test_cterm_build_rule(
+        self,
+        cterm_symbolic: CTermSymbolic,
+        kprint: KPrint,
+        test_id: str,
+        pre: tuple[tuple[str, str, str | None], tuple[str, str, str | None]],
+        expected_post: tuple[str, str, str | None, str | None],
+    ) -> None:
+        # Given
+        lhs, rhs = pre
+        expected_k, expected_state, expected_requires, expected_ensures = expected_post
+
+        # When
+        config_lhs = self.config(kprint, *lhs)
+        config_rhs = self.config(kprint, *rhs)
+        rule, _ = cterm_build_rule(test_id, config_lhs, config_rhs, defunc_with=kprint.definition)
+        rule_body_cterm = CTerm.from_kast(rule.body)
+        rule_k = kprint.pretty_print(rule_body_cterm.cell('K_CELL'))
+        rule_state = kprint.pretty_print(rule_body_cterm.cell('STATE_CELL'))
+        rule_requires = kprint.pretty_print(rule.requires)
+        rule_ensures = kprint.pretty_print(rule.ensures)
+
+        # Then
+        assert rule_k == expected_k
+        assert rule_state == expected_state
+        assert rule_requires == expected_requires
+        assert rule_ensures == expected_ensures

pyk/src/tests/integration/proof/test_refute_node.py

@@ -11,6 +11,7 @@
 from pyk.kast.manip import free_vars
 from pyk.kast.outer import KClaim
 from pyk.kcfg import KCFG
+from pyk.kcfg.minimize import KCFGMinimizer
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.prelude.kint import gtInt, intToken, leInt
 from pyk.prelude.ml import is_top, mlEqualsTrue
@@ -372,7 +373,7 @@ def test_apr_proof_refute_node_multiple_constraints(
         prover.advance_proof(proof, max_iterations=4)
         # After the minimization, nodes 7-10 created by the advancement of the proof
         # will have multiple constraints in their immediately preceding splits
-        proof.kcfg.minimize()
+        KCFGMinimizer(proof.kcfg).minimize()
 
         # Then
         for i in [7, 8, 9, 10]: