From d10dd05577031194976268fadbe112b4ed8ccd3a Mon Sep 17 00:00:00 2001
From: Noah Watson <107630091+nwatson22@users.noreply.github.com>
Date: Mon, 22 Jul 2024 13:02:05 -0500
Subject: [PATCH] Fix crash with failure info with custom multiplicity cells
 (#4531)

This crash was found by @lucasmt. When there is a structural match
failure in failure info computation we were assuming the cells in the
antecedent were always present in the consequent, but this is not
necessarily true in the case where we have optional cells, e.g.
`type="Map"`. This avoids the crash by simply indicating the missing
cell is missing from the consequent. There is still confusing behavior
when, e.g. there are multiple copies of the same cell.
---
 pyk/src/pyk/cterm/symbolic.py                 | 22 ++++---
 .../tests/integration/proof/test_mini_kevm.py | 63 +++++++++++++++++++
 2 files changed, 76 insertions(+), 9 deletions(-)

diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py
index f169295c0b2..bdefcb59f58 100644
--- a/pyk/src/pyk/cterm/symbolic.py
+++ b/pyk/src/pyk/cterm/symbolic.py
@@ -8,7 +8,7 @@
 from pyk.utils import not_none
 
 from ..cterm import CSubst, CTerm
-from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst
+from ..kast.inner import KApply, KLabel, KRewrite, KToken, KVariable, Subst
 from ..kast.manip import flatten_label, is_spurious_constraint, sort_ac_collections
 from ..kast.pretty import PrettyPrinter
 from ..konvert import kast_to_kore, kore_to_kast
@@ -259,14 +259,18 @@ def implies(
                     curr_cell_match = Subst({})
                     for cell in antecedent.cells:
                         antecedent_cell = sort_ac_collections(antecedent.cell(cell))
-                        consequent_cell = sort_ac_collections(consequent.cell(cell))
-                        cell_match = consequent_cell.match(antecedent_cell)
-                        if cell_match is not None:
-                            _curr_cell_match = curr_cell_match.union(cell_match)
-                            if _curr_cell_match is not None:
-                                curr_cell_match = _curr_cell_match
-                                continue
-                        failing_cells.append((cell, KRewrite(antecedent_cell, consequent_cell)))
+
+                        if cell not in consequent.cells:
+                            failing_cells.append((cell, KRewrite(antecedent_cell, KToken('.K', sort='KItem'))))
+                        else:
+                            consequent_cell = sort_ac_collections(consequent.cell(cell))
+                            cell_match = consequent_cell.match(antecedent_cell)
+                            if cell_match is not None:
+                                _curr_cell_match = curr_cell_match.union(cell_match)
+                                if _curr_cell_match is not None:
+                                    curr_cell_match = _curr_cell_match
+                                    continue
+                            failing_cells.append((cell, KRewrite(antecedent_cell, consequent_cell)))
                 else:
                     consequent_constraints = list(
                         filter(
diff --git a/pyk/src/tests/integration/proof/test_mini_kevm.py b/pyk/src/tests/integration/proof/test_mini_kevm.py
index 4e38dfee0f2..af651edc19c 100644
--- a/pyk/src/tests/integration/proof/test_mini_kevm.py
+++ b/pyk/src/tests/integration/proof/test_mini_kevm.py
@@ -6,7 +6,10 @@
 
 import pytest
 
+from pyk.cterm import CTerm
+from pyk.kast.inner import KApply, KVariable
 from pyk.kcfg.show import KCFGShow
+from pyk.prelude.kint import intToken
 from pyk.proof import APRProof, APRProver, ProofStatus
 from pyk.proof.show import APRProofNodePrinter
 from pyk.testing import KCFGExploreTest, KProveTest
@@ -100,3 +103,63 @@ def test_all_path_reachability_prove(
 
             assert proof.status == proof_status
             assert leaf_number(proof) == expected_leaf_number
+
+    def test_implication_failure_reason_cell_mismatch(
+        self,
+        kcfg_explore: KCFGExplore,
+        kprove: KProve,
+    ) -> None:
+
+        expected = (
+            'Matching failed.\n'
+            'The following cells failed matching individually (antecedent #Implies consequent):\n'
+            'ACCTID_CELL: 0 #Implies .K\n'
+            'STORAGE_CELL: .Map #Implies .K\n'
+            'ORIGSTORAGE_CELL: .Map #Implies .K'
+        )
+
+        antecedent_term = CTerm(
+            KApply(
+                '<generatedTop>',
+                [
+                    KApply('<k>', [intToken(0)]),
+                    KApply('<id>', [intToken(0)]),
+                    KApply(
+                        '<accounts>',
+                        [
+                            KApply(
+                                '<account>',
+                                [
+                                    KApply('<acctID>', [intToken(0)]),
+                                    KApply('<storage>', [KApply('.Map')]),
+                                    KApply('<origStorage>', [KApply('.Map')]),
+                                ],
+                            )
+                        ],
+                    ),
+                    KVariable('GENERATED_COUNTER_CELL'),
+                ],
+            ),
+        )
+
+        consequent_term = CTerm(
+            KApply(
+                '<generatedTop>',
+                [
+                    KApply('<k>', [intToken(0)]),
+                    KApply('<id>', [intToken(0)]),
+                    KApply(
+                        '<accounts>',
+                        [
+                            KApply('.AccountCellMap'),
+                        ],
+                    ),
+                    KVariable('GENERATED_COUNTER_CELL'),
+                ],
+            ),
+        )
+
+        passed, actual = kcfg_explore.implication_failure_reason(antecedent_term, consequent_term)
+
+        assert not passed
+        assert actual == expected