Claim dependencies included as subproofs (#4411)

This PR fixes some small issues in claim dependency process.

- Claim dependencies were not included as subproofs, which meant they
weren't being re-used appropriately when needed, in
`APRProof.from_claim(...)`. Fixing this enables using
`APRProof.from_claim(...)` directly downstream instead of manually
creating the KCFG and proof objects. Note that we have to do some
translation of the claim dependencies because by default they would come
in with unqualified names, which is fixed by adjusting the claim
attributes directly.
- Common predicates between multiple branches were showing up in
side-conditions on branching results of exploration, and now they are
factored out and reported separately.
- Some adjustments to `KCFG.to_rule(s)` and `ARPProof.as_rule(s)` which
allow better naming/labelling of the generated rules, so it's easier to
tell where they came from.

---------

Co-authored-by: Tamás Tóth <[email protected]>

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)