Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/llvm-backend

.github/workflows/release.yml

@@ -84,9 +84,9 @@ jobs:
           packages: jq
           script: |
             export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH"
-            kup publish k-framework-binary .#k --keep-days 180
-            kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180
-
+            kup publish --verbose k-framework-binary .#k --keep-days 180
+            kup publish --verbose k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180
+      
   ubuntu-noble:
     name: 'K Ubuntu Noble Package'
     runs-on: [self-hosted, linux, normal]

k-distribution/include/kframework/builtin/domains.md

@@ -1241,9 +1241,13 @@ You can:
                > left:
                  Int "*Int" Int                 [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)]
                /* FIXME: translate /Int and %Int into smtlib */
-               /* /Int and %Int implement t-division, which rounds towards 0 */
-               | Int "/Int" Int                 [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)]
-               | Int "%Int" Int                 [function, symbol(_%Int_), left, smt-hook(mod), hook(INT.tmod)]
+               /* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */
+               | Int "/Int" Int                 [function, symbol(_/Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))),
+                                                 hook(INT.tdiv)]
+               | Int "%Int" Int                 [function, symbol(_%Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))),
+                                                 hook(INT.tmod)]
                /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */
                | Int "divInt" Int               [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)]
                | Int "modInt" Int               [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)]

pyk/regression-new/kprove-haskell/sum-spec.k.out

@@ -31,7 +31,9 @@ Subproofs: 0
 │     #And { true #Equals N:Int >=Int 0 }
 ┃
 ┃ (branch)
-┣━━┓ constraint: N:Int >Int 0
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     N:Int >Int 0
 ┃  │
 ┃  ├─ 3
 ┃  │     <generatedTop>
@@ -92,8 +94,11 @@ Subproofs: 0
 ┃  │     #And { true #Equals N:Int >=Int 0 }
 ┃  │     #And { true #Equals N:Int +Int -1 >=Int 0 }
 ┃  │
-┃  ┊  constraint: OMITTED CONSTRAINT
-┃  ┊  subst: OMITTED SUBST
+┃  ┊  constraint:
+┃  ┊      S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2
+┃  ┊  subst:
+┃  ┊      ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int
+┃  ┊      ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int
 ┃  └─ 2 (leaf, target)
 ┃        <generatedTop>
 ┃          <k>
@@ -112,7 +117,9 @@ Subproofs: 0
 ┃        #And { true #Equals N:Int >=Int 0 }
 ┃        #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
 ┃
-┗━━┓ constraint: N:Int ==Int 0
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     N:Int ==Int 0
    │
    ├─ 4
    │     <generatedTop>
@@ -151,8 +158,11 @@ Subproofs: 0
    │     </generatedTop>
    │     #And { N:Int #Equals 0 }
    │
-   ┊  constraint: OMITTED CONSTRAINT
-   ┊  subst: OMITTED SUBST
+   ┊  constraint:
+   ┊      S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2
+   ┊  subst:
+   ┊      C <- COUNTER_CELL_af8c44a5:Int
+   ┊      GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int
    └─ 2 (leaf, target)
          <generatedTop>
            <k>

pyk/regression-new/kprove-haskell/test-spec.k.out

@@ -48,7 +48,8 @@ Subproofs: 0
 │     </generatedTop>
 │
 ┊  constraint: true
-┊  subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
+┊  subst:
+┊      GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
 └─ 2 (leaf, target)
       <generatedTop>
         <k>

pyk/src/pyk/__main__.py

@@ -282,7 +282,7 @@ def explore_context() -> Iterator[KCFGExplore]:
         if options.show_kcfg and type(proof) is APRProof:
             node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
             show = APRProofShow(kprove, node_printer=node_printer)
-            print('\n'.join(show.show(proof)))
+            print('\n'.join(show.show(proof, minimize=False)))
     sys.exit(len([p.id for p in proofs if not p.passed]))
 
 

pyk/src/pyk/cterm/cterm.py

@@ -38,7 +38,7 @@ class CTerm:
 
     Contains the data:
     - `config`: the _configuration_ (structural component of the state, potentially containing free variabls)
-    - `constraints`: conditiions which limit/constraint the free variables from the `config`
+    - `constraints`: conditions which limit/constraint the free variables from the `config`
     """
 
     config: KInner  # TODO Optional?
@@ -253,6 +253,25 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm:
         return CTerm(self.config, new_constraints)
 
 
+def cterm_match(cterm1: CTerm, cterm2: CTerm) -> CSubst | None:
+    """Find a substitution which can instantiate `cterm1` to `cterm2`.
+
+    Args:
+        cterm1: `CTerm` to instantiate to `cterm2`.
+        cterm2: `CTerm` to instantiate `cterm1` to.
+
+    Returns:
+        A `CSubst` which can instantiate `cterm1` to `cterm2`, or `None` if no such `CSubst` exists.
+    """
+    # todo: delete this function and use cterm1.match_with_constraint(cterm2) directly after closing #4496
+    subst = cterm1.config.match(cterm2.config)
+    if subst is None:
+        return None
+    source_constraints = [subst(c) for c in cterm1.constraints]
+    constraints = [c for c in cterm2.constraints if c not in source_constraints]
+    return CSubst(subst, constraints)
+
+
 def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:
     """Return a generalized state over the two input states.
 
@@ -333,8 +352,13 @@ def add_constraint(self, constraint: KInner) -> CSubst:
 
     def apply(self, cterm: CTerm) -> CTerm:
         """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints)."""
-        _kast = self.subst(cterm.kast)
-        return CTerm(_kast, [self.constraint])
+        config = self.subst(cterm.config)
+        constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints)
+        return CTerm(config, constraints)
+
+    def __call__(self, cterm: CTerm) -> CTerm:
+        """Overload for `CSubst.apply`."""
+        return self.apply(cterm)
 
 
 def cterm_build_claim(

pyk/src/pyk/kast/manip.py

@@ -215,48 +215,39 @@ def extract_rhs(term: KInner) -> KInner:
 
 
 def extract_subst(term: KInner) -> tuple[Subst, KInner]:
-    def _subst_for_terms(term1: KInner, term2: KInner) -> Subst | None:
-        if type(term1) is KVariable and type(term2) not in {KToken, KVariable}:
-            return Subst({term1.name: term2})
-        if type(term2) is KVariable and type(term1) not in {KToken, KVariable}:
-            return Subst({term2.name: term1})
-        return None
-
-    def _extract_subst(conjunct: KInner) -> Subst | None:
-        if type(conjunct) is KApply:
-            if conjunct.label.name == '#Equals':
-                subst = _subst_for_terms(conjunct.args[0], conjunct.args[1])
-
-                if subst is not None:
-                    return subst
-
-                if (
-                    conjunct.args[0] == TRUE
-                    and type(conjunct.args[1]) is KApply
-                    and conjunct.args[1].label.name in {'_==K_', '_==Int_'}
-                ):
-                    subst = _subst_for_terms(conjunct.args[1].args[0], conjunct.args[1].args[1])
-
-                    if subst is not None:
-                        return subst
+    subst = {}
+    rem_conjuncts: list[KInner] = []
 
+    def _extract_subst(term: KInner, term2: KInner) -> tuple[str, KInner] | None:
+        if (
+            (isinstance(term, KVariable) and term.name not in subst)
+            and not (isinstance(term2, KVariable) and term2.name in subst)
+            and term.name not in free_vars(term2)
+        ):
+            return (term.name, term2)
+        if (
+            (isinstance(term2, KVariable) and term2.name not in subst)
+            and not (isinstance(term, KVariable) and term.name in subst)
+            and term2.name not in free_vars(term)
+        ):
+            return (term2.name, term)
+        if term == TRUE and isinstance(term2, KApply) and term2.label.name in {'_==K_', '_==Int_'}:
+            return _extract_subst(term2.args[0], term2.args[1])
+        if term2 == TRUE and isinstance(term, KApply) and term.label.name in {'_==K_', '_==Int_'}:
+            return _extract_subst(term.args[0], term.args[1])
         return None
 
-    conjuncts = flatten_label('#And', term)
-    subst = Subst()
-    rem_conjuncts: list[KInner] = []
-
-    for conjunct in conjuncts:
-        new_subst = _extract_subst(conjunct)
-        if new_subst is None:
-            rem_conjuncts.append(conjunct)
+    for conjunct in flatten_label('#And', term):
+        if isinstance(conjunct, KApply) and conjunct.label.name == '#Equals':
+            if _conjunct_subst := _extract_subst(conjunct.args[0], conjunct.args[1]):
+                name, value = _conjunct_subst
+                subst[name] = value
+            else:
+                rem_conjuncts.append(conjunct)
         else:
-            new_subst = subst.union(new_subst)
-            if new_subst is None:
-                raise ValueError('Conflicting substitutions')  # TODO handle this case
-            subst = new_subst
+            rem_conjuncts.append(conjunct)
 
-    return subst, mlAnd(rem_conjuncts)
+    return Subst(subst), mlAnd(rem_conjuncts)
 
 
 def count_vars(term: KInner) -> Counter[str]:

pyk/src/pyk/kcfg/kcfg.py

@@ -9,6 +9,8 @@
 from threading import RLock
 from typing import TYPE_CHECKING, Final, List, Union, cast, final
 
+from pyk.cterm.cterm import cterm_match
+
 from ..cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule
 from ..kast import EMPTY_ATT
 from ..kast.inner import KApply
@@ -1040,6 +1042,16 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike,
         self.add_successor(split)
         return split
 
+    def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None:
+        """Create a split without crafting a CSubst."""
+        source = self.node(source_id)
+        targets = [self.node(nid) for nid in target_ids]
+        try:
+            csubsts = [not_none(cterm_match(source.cterm, target.cterm)) for target in targets]
+        except ValueError:
+            return None
+        return self.create_split(source.id, zip(target_ids, csubsts, strict=True))
+
     def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]:
         source_id = self._resolve(source_id) if source_id is not None else None
         target_id = self._resolve(target_id) if target_id is not None else None

pyk/src/pyk/kcfg/show.py

@@ -27,6 +27,7 @@
     from pathlib import Path
     from typing import Final
 
+    from ..cterm import CSubst
     from ..kast import KInner
     from ..kast.outer import KFlatModule, KSentence
     from ..ktool.kprint import KPrint
@@ -126,6 +127,34 @@ def pretty_segments(self, kcfg: KCFG, minimize: bool = True) -> Iterable[tuple[s
         processed_nodes: list[KCFG.Node] = []
         ret_lines: list[tuple[str, list[str]]] = []
 
+        def _multi_line_print(
+            label: str, lines: list[str], default: str = 'None', indent: int = 4, max_width: int | None = None
+        ) -> list[str]:
+            ret_lines = []
+            if len(lines) == 0:
+                ret_lines.append(f'{label}: {default}')
+            else:
+                ret_lines.append(f'{label}:')
+                ret_lines.extend([f'{indent * " "}{line}' for line in lines])
+            if max_width is not None:
+                ret_lines = [
+                    ret_line if len(ret_line) <= max_width else ret_line[0:max_width] + '...' for ret_line in ret_lines
+                ]
+            return ret_lines
+
+        def _print_csubst(
+            csubst: CSubst, subst_first: bool = False, indent: int = 4, max_width: int | None = None
+        ) -> list[str]:
+            _constraint_strs = [
+                self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints
+            ]
+            constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width)
+            _subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in csubst.subst.minimize().items()]
+            subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width)
+            if subst_first:
+                return subst_strs + constraint_strs
+            return constraint_strs + subst_strs
+
         def _print_node(node: KCFG.Node) -> list[str]:
             return self.node_short_info(kcfg, node)
 
@@ -143,46 +172,12 @@ def _print_merged_edge(merged_edge: KCFG.MergedEdge) -> list[str]:
             return [res] if len(res) < 78 else ['(merged edge)']
 
         def _print_cover(cover: KCFG.Cover) -> Iterable[str]:
-            subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in cover.csubst.subst.items()]
-            subst_str = ''
-            if len(subst_strs) == 0:
-                subst_str = '.Subst'
-            if len(subst_strs) == 1:
-                subst_str = subst_strs[0]
-            if len(subst_strs) > 1 and minimize:
-                subst_str = 'OMITTED SUBST'
-            if len(subst_strs) > 1 and not minimize:
-                subst_str = '{\n    ' + '\n    '.join(subst_strs) + '\n}'
-            constraint_str = self.kprint.pretty_print(ml_pred_to_bool(cover.csubst.constraint, unsafe=True))
-            if len(constraint_str) > 78:
-                constraint_str = 'OMITTED CONSTRAINT'
-            return [
-                f'constraint: {constraint_str}',
-                f'subst: {subst_str}',
-            ]
+            max_width = None if not minimize else 78
+            return _print_csubst(cover.csubst, subst_first=False, indent=4, max_width=max_width)
 
         def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]:
-            csubst = split.splits[target_id]
-            ret_split_lines: list[str] = []
-            substs = csubst.subst.minimize().items()
-            constraints = [ml_pred_to_bool(c, unsafe=True) for c in csubst.constraints]
-            if len(constraints) == 1:
-                first_line, *rest_lines = self.kprint.pretty_print(constraints[0]).split('\n')
-                ret_split_lines.append(f'constraint: {first_line}')
-                ret_split_lines.extend(f'              {line}' for line in rest_lines)
-            elif len(constraints) > 1:
-                ret_split_lines.append('constraints:')
-                for constraint in constraints:
-                    first_line, *rest_lines = self.kprint.pretty_print(constraint).split('\n')
-                    ret_split_lines.append(f'    {first_line}')
-                    ret_split_lines.extend(f'      {line}' for line in rest_lines)
-            if len(substs) == 1:
-                vname, term = list(substs)[0]
-                ret_split_lines.append(f'subst: {vname} <- {self.kprint.pretty_print(term)}')
-            elif len(substs) > 1:
-                ret_split_lines.append('substs:')
-                ret_split_lines.extend(f'    {vname} <- {self.kprint.pretty_print(term)}' for vname, term in substs)
-            return ret_split_lines
+            max_width = None if not minimize else 78
+            return _print_csubst(split.splits[target_id], subst_first=True, indent=4, max_width=max_width)
 
         def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG.Node]) -> None:
             processed = curr_node in processed_nodes

pyk/src/pyk/prelude/ml.py

@@ -5,7 +5,7 @@
 from pyk.utils import single
 
 from ..kast.inner import KApply, KLabel, build_assoc, flatten_label
-from .k import GENERATED_TOP_CELL, K_ITEM
+from .k import GENERATED_TOP_CELL, K_ITEM, K
 from .kbool import BOOL, FALSE, TRUE
 
 if TYPE_CHECKING:
@@ -55,7 +55,7 @@ def is_bottom(term: KInner, *, weak: bool = False) -> bool:
 def mlEquals(  # noqa: N802
     term1: KInner,
     term2: KInner,
-    arg_sort: str | KSort = GENERATED_TOP_CELL,
+    arg_sort: str | KSort = K,
     sort: str | KSort = GENERATED_TOP_CELL,
 ) -> KApply:
     return KLabel('#Equals', arg_sort, sort)(term1, term2)

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

@@ -12,7 +12,7 @@
 from pyk.kast.manip import minimize_term, sort_ac_collections
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.kcfg.show import KCFGShow
-from pyk.prelude.kbool import FALSE, andBool, orBool
+from pyk.prelude.kbool import BOOL, FALSE, andBool, orBool
 from pyk.prelude.kint import intToken
 from pyk.prelude.ml import mlAnd, mlBottom, mlEquals, mlEqualsFalse, mlEqualsTrue, mlTop
 from pyk.proof import APRProver, ProofStatus
@@ -700,7 +700,7 @@ def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
         'failing-if',
         0,
         1,
-        (mlEquals(KVariable('_B', 'Bool'), FALSE),),
+        (mlEquals(KVariable('_B', 'Bool'), FALSE, arg_sort=BOOL),),
         False,
     ),
     (