From 885c813bd73bf09110e7e82b93aa40eddb9515ba Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Wed, 18 Sep 2024 10:09:28 -0300
Subject: [PATCH 1/3] Introducing the `LLVMPatternMatchingFailureEvent` class
 in ProofTrace.py

---
 pyk/src/pyk/kllvm/hints/prooftrace.py | 34 +++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py
index 2cc98e6f0ed..55d6f6caf6a 100644
--- a/pyk/src/pyk/kllvm/hints/prooftrace.py
+++ b/pyk/src/pyk/kllvm/hints/prooftrace.py
@@ -15,6 +15,7 @@
     llvm_side_condition_end_event,
     llvm_side_condition_event,
     llvm_step_event,
+    llvm_pattern_matching_failure_event,
     annotated_llvm_event,
     llvm_rewrite_trace_iterator,
     EventType,
@@ -167,6 +168,39 @@ def check_result(self) -> bool:
         """Return the boolean result of the evaluation of the side condition that corresponds to this event."""
         return self._side_condition_end_event.check_result
 
+@final
+class LLVMPatternMatchingFailureEvent(LLVMStepEvent):
+    """Represents an LLVM pattern matching failure event.
+
+    This event is used to indicate that the pattern matching failed during the rewriting process.
+
+    Attributes:
+        _pattern_matching_failure_event (llvm_pattern_matching_failure_event): The underlying pattern matching failure event.
+    """
+
+    _pattern_matching_failure_event: llvm_pattern_matching_failure_event
+
+    def __init__(self, pattern_matching_failure_event: llvm_pattern_matching_failure_event) -> None:
+        """Initialize a new instance of the LLVMPatternMatchingFailureEvent class.
+
+        Args:
+            pattern_matching_failure_event (llvm_pattern_matching_failure_event): The LLVM pattern matching failure event object.
+        """
+        self._pattern_matching_failure_event = pattern_matching_failure_event
+
+    def __repr__(self) -> str:
+        """Return a string representation of the object.
+
+        Returns:
+            A string representation of the LLVMPatternMatchingFailureEvent object using the AST printing method.
+        """
+        return self._pattern_matching_failure_event.__repr__()
+
+    @property
+    def function_name(self) -> str:
+        """Return the name of the function that failed to match the pattern."""
+        return self._pattern_matching_failure_event.function_name
+
 
 @final
 class LLVMFunctionEvent(LLVMStepEvent):

From c4c6cb62f8f90b6abe37522e49928227233ea7ec Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Wed, 18 Sep 2024 12:25:37 -0300
Subject: [PATCH 2/3] Adding the `LLVMPatternMatchingFailureEvent` case to
 `step_event` function of `LLVMArgument`

---
 pyk/src/pyk/kllvm/hints/prooftrace.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py
index 55d6f6caf6a..fabe1d2f64d 100644
--- a/pyk/src/pyk/kllvm/hints/prooftrace.py
+++ b/pyk/src/pyk/kllvm/hints/prooftrace.py
@@ -168,6 +168,7 @@ def check_result(self) -> bool:
         """Return the boolean result of the evaluation of the side condition that corresponds to this event."""
         return self._side_condition_end_event.check_result
 
+
 @final
 class LLVMPatternMatchingFailureEvent(LLVMStepEvent):
     """Represents an LLVM pattern matching failure event.
@@ -331,6 +332,8 @@ def step_event(self) -> LLVMStepEvent:
             return LLVMFunctionEvent(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_hook_event):
             return LLVMHookEvent(self._argument.step_event)
+        elif isinstance(self._argument.step_event, llvm_pattern_matching_failure_event):
+            return LLVMPatternMatchingFailureEvent(self._argument.step_event)
         else:
             raise AssertionError()
 

From 29781e330b2cfb9c602703632ad2a0bf6c4ae79b Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Wed, 18 Sep 2024 12:26:10 -0300
Subject: [PATCH 3/3] Adding the `assert` to verify that we're producing the
 `LLVMPatternMatchingFailureEvent` correctly

---
 pyk/src/tests/integration/kllvm/test_prooftrace.py | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py
index 0883ca54471..62fa039a55d 100644
--- a/pyk/src/tests/integration/kllvm/test_prooftrace.py
+++ b/pyk/src/tests/integration/kllvm/test_prooftrace.py
@@ -808,9 +808,14 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         # 12 initialization events
         assert len(pt.pre_trace) == 12
 
-        # 404 post-initial-configuration events
+        # 776 post-initial-configuration events
         assert len(pt.trace) == 776
 
+        # Assert that we have a pattern matching failure as the 135th event
+        assert pt.trace[135].is_step_event() and isinstance(
+            pt.trace[135].step_event, prooftrace.LLVMPatternMatchingFailureEvent
+        )
+
 
 class TestIMP5(ProofTraceTest):
     KOMPILE_DEFINITION = """