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

…meverification/haskell-backend

pyk/src/pyk/kcfg/explore.py

@@ -15,8 +15,8 @@
 )
 from ..kast.pretty import PrettyPrinter
 from ..kore.rpc import LogRewrite, RewriteSuccess
-from ..prelude.ml import is_top
-from ..utils import not_none, shorten_hashes, single
+from ..prelude.ml import is_top, mlAnd
+from ..utils import not_none, shorten_hashes, single, unique
 from .kcfg import KCFG, Abstract, Branch, NDBranch, Step, Stuck, Vacuous
 from .semantics import DefaultSemantics
 
@@ -262,7 +262,20 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]:
         # Branch
         assert len(next_states) > 1
         if all(branch_constraint for _, branch_constraint in next_states):
-            branches = [not_none(rule_predicate) for _, rule_predicate in next_states]
+            branch_preds = [flatten_label('#And', not_none(rule_predicate)) for _, rule_predicate in next_states]
+            common_preds = list(
+                unique(
+                    pred
+                    for branch_pred in branch_preds
+                    for pred in branch_pred
+                    if all(pred in bp for bp in branch_preds)
+                )
+            )
+            branches = [mlAnd(pred for pred in branch_pred if pred not in common_preds) for branch_pred in branch_preds]
+            if common_preds:
+                log(
+                    f'Common predicates found in branches: {[self.pretty_print(ml_pred_to_bool(cp)) for cp in common_preds]}'
+                )
             constraint_strs = [self.pretty_print(ml_pred_to_bool(bc)) for bc in branches]
             log(f'{len(branches)} branches: {node_id} -> {constraint_strs}')
             return Branch(branches)

pyk/src/pyk/kcfg/kcfg.py

@@ -605,8 +605,9 @@ def to_json(self) -> str:
     def from_json(s: str, optimize_memory: bool = True) -> KCFG:
         return KCFG.from_dict(json.loads(s), optimize_memory=optimize_memory)
 
-    def to_rules(self, priority: int = 20) -> list[KRuleLike]:
-        return [e.to_rule('BASIC-BLOCK', priority=priority) for e in self.edges()]
+    def to_rules(self, priority: int = 20, id: str | None = None) -> list[KRuleLike]:
+        id = '' if id is None else f'{id}-'
+        return [e.to_rule(f'{id}BASIC-BLOCK', priority=priority) for e in self.edges()]
 
     def to_module(
         self,

pyk/src/pyk/proof/reachability.py

@@ -10,6 +10,7 @@
 from pyk.kore.rpc import LogEntry
 
 from ..cterm.cterm import remove_useless_constraints
+from ..kast.att import AttEntry, Atts
 from ..kast.inner import KInner, Subst
 from ..kast.manip import flatten_label, free_vars, ml_pred_to_bool
 from ..kast.outer import KFlatModule, KImport, KRule
@@ -378,12 +379,21 @@ def from_claim(
             proof_dir=proof_dir,
             circularity=claim.is_circularity,
             admitted=claim.is_trusted,
+            subproof_ids=claim.dependencies,
             **kwargs,
         )
 
+    def as_rules(self, priority: int = 20) -> list[KRule]:
+        _rules = []
+        for _edge in self.kcfg.edges():
+            _rule = _edge.to_rule(f'APRPROOF-{self.id.upper()}-BASIC-BLOCK', priority=priority)
+            assert type(_rule) is KRule
+            _rules.append(_rule)
+        return _rules
+
     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)
+        _rule = _edge.to_rule(f'APRPROOF-{self.id.upper()}-BASIC-BLOCK', priority=priority)
         assert type(_rule) is KRule
         return _rule
 
@@ -448,12 +458,14 @@ def from_spec_modules(
                 else:
                     _LOGGER.info(f'Building APRProof for claim: {claim_label}')
                     claim = claims_by_label[claim_label]
+                    if len(claims_graph[claim_label]) > 0:
+                        claim_att = claim.att.update([AttEntry(Atts.DEPENDS, ','.join(claims_graph[claim_label]))])
+                        claim = claim.let_att(claim_att)
                     apr_proof = APRProof.from_claim(
                         defn,
                         claim,
                         logs=logs,
                         proof_dir=proof_dir,
-                        subproof_ids=claims_graph[claim_label],
                     )
                     apr_proof.write_proof_data()
                 apr_proofs.append(apr_proof)
@@ -709,7 +721,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike
 
         dependencies_as_rules: list[KRuleLike] = []
         for apr_subproof in [pf for pf in subproofs if isinstance(pf, APRProof)]:
-            dependencies_as_rules.extend(apr_subproof.kcfg.to_rules(priority=20))
+            dependencies_as_rules.extend(apr_subproof.as_rules(priority=20))
             if apr_subproof.admitted and len(apr_subproof.kcfg.predecessors(apr_subproof.target)) == 0:
                 dependencies_as_rules.append(apr_subproof.as_rule(priority=20))
         circularity_rule = proof.as_rule(priority=20)

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

@@ -203,13 +203,7 @@ def _run_proof(
         max_iterations: int | None,
     ) -> tuple[ProofStatus, list[str]]:
 
-        proof = APRProof.from_claim(
-            kprove.definition,
-            claim,
-            subproof_ids=[],
-            logs={},
-            proof_dir=proof_dir,
-        )
+        proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
         init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm)
         proof.kcfg.let_node(proof.init, cterm=init_cterm)
         kcfg_explore.simplify(proof.kcfg, {})

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

@@ -79,13 +79,7 @@ def test_all_path_reachability_prove(
                     Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}']
                 )
             )
-            proof = APRProof.from_claim(
-                kprove.definition,
-                claim,
-                subproof_ids=[],
-                logs={},
-                proof_dir=proof_dir,
-            )
+            proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
 
             new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm)
             proof.kcfg.let_node(proof.init, cterm=new_init_cterm)