Adding inline documentation to prooftrace.py (#4407)

This is a simple PR that documents the prooftrace bindings classes and
methods using docstrings.
It also adds `__init__.py` to `pyk.kllvm.hints` so it gets recognized by
`Sphinx` and hopefully published in
https://runtimeverification.github.io/pyk/index.html

pyk/src/pyk/kllvm/hints/prooftrace.py

@@ -25,21 +25,43 @@
 
 
 class LLVMStepEvent(ABC):
-    pass
+    """
+    Abstract base class representing an LLVM step event.
+    """
 
 
 class LLVMRewriteEvent(LLVMStepEvent):
+    """
+    Represents LLVM rewrite event.
+    """
+
     @property
     @abstractmethod
-    def rule_ordinal(self) -> int: ...
+    def rule_ordinal(self) -> int:
+        """Returns the axiom ordinal number of the rewrite rule. The rule ordinal represents the `nth` axiom in the kore definition."""
+        ...
 
     @property
     @abstractmethod
-    def substitution(self) -> dict[str, Pattern]: ...
+    def substitution(self) -> dict[str, Pattern]:
+        """Returns the substitution dictionary used to perform the rewrite represented by this event."""
+        ...
 
 
 @final
 class LLVMRuleEvent(LLVMRewriteEvent):
+    """
+    Represents an LLVM rule event.
+
+    Attributes:
+        _rule_event (llvm_rule_event): The underlying LLVM rule event.
+
+    Methods:
+        __init__(self, rule_event: llvm_rule_event) -> None: Initializes a new instance of the LLVMRuleEvent class.
+
+        __repr__(self) -> str: Returns a string representation of the LLVMRuleEvent object using the AST printing method.
+    """
+
     _rule_event: llvm_rule_event
 
     def __init__(self, rule_event: llvm_rule_event) -> None:
@@ -50,15 +72,29 @@ def __repr__(self) -> str:
 
     @property
     def rule_ordinal(self) -> int:
+        """Returns the axiom ordinal number of the rule event."""
         return self._rule_event.rule_ordinal
 
     @property
     def substitution(self) -> dict[str, Pattern]:
+        """Returns the substitution dictionary used to perform the rewrite represented by this rule event."""
         return {k: v[0] for k, v in self._rule_event.substitution.items()}
 
 
 @final
 class LLVMSideConditionEventEnter(LLVMRewriteEvent):
+    """
+    Represents an event that enters a side condition in LLVM rewriting. This event is used to check the side condition of a rule. Mostly used in ensures/requires clauses.
+
+    Attributes:
+        _side_condition_event (llvm_side_condition_event): The underlying side condition event.
+
+    Methods:
+        __init__(self, side_condition_event: llvm_side_condition_event) -> None: Initializes a new instance of the LLVMSideConditionEventEnter class.
+
+        __repr__(self) -> str: Returns a string representation of the LLVMSideConditionEventEnter object using the AST printing method.
+    """
+
     _side_condition_event: llvm_side_condition_event
 
     def __init__(self, side_condition_event: llvm_side_condition_event) -> None:
@@ -69,15 +105,29 @@ def __repr__(self) -> str:
 
     @property
     def rule_ordinal(self) -> int:
+        """Returns the axiom ordinal number associated with the side condition event."""
         return self._side_condition_event.rule_ordinal
 
     @property
     def substitution(self) -> dict[str, Pattern]:
+        """Returns the substitution dictionary used to perform the rewrite represented by this side condition event."""
         return {k: v[0] for k, v in self._side_condition_event.substitution.items()}
 
 
 @final
 class LLVMSideConditionEventExit(LLVMStepEvent):
+    """
+    Represents an LLVM side condition event indicating the exit of a side condition. This event contains the result of the side condition evaluation.
+
+    Attributes:
+        _side_condition_end_event (llvm_side_condition_end_event): The underlying side condition end event.
+
+    Methods:
+        __init__(side_condition_end_event: llvm_side_condition_end_event) -> None: Initializes the LLVMSideConditionEventExit instance.
+
+        __repr__(self) -> str: Returns a string representation of the LLVMSideConditionEventExit instance using the AST printing method.
+    """
+
     _side_condition_end_event: llvm_side_condition_end_event
 
     def __init__(self, side_condition_end_event: llvm_side_condition_end_event) -> None:
@@ -88,15 +138,29 @@ def __repr__(self) -> str:
 
     @property
     def rule_ordinal(self) -> int:
+        """Returns the axiom ordinal number associated with the side condition event."""
         return self._side_condition_end_event.rule_ordinal
 
     @property
     def check_result(self) -> bool:
+        """Returns 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 LLVMFunctionEvent(LLVMStepEvent):
+    """
+    Represents an LLVM function event in a proof trace.
+
+    Attributes:
+        _function_event (llvm_function_event): The underlying LLVM function event object.
+
+    Methods:
+        __init__(self, function_event: llvm_function_event) -> None: Initializes a new instance of the LLVMFunctionEvent class.
+
+        __repr__(self) -> str: Returns a string representation of the LLVMFunctionEvent object using the AST printing method.
+    """
+
     _function_event: llvm_function_event
 
     def __init__(self, function_event: llvm_function_event) -> None:
@@ -107,19 +171,34 @@ def __repr__(self) -> str:
 
     @property
     def name(self) -> str:
+        """Returns the name of the LLVM function as a KORE Symbol Name."""
         return self._function_event.name
 
     @property
     def relative_position(self) -> str:
+        """Returns the relative position of the LLVM function event in the proof trace. Ex.: (0:0:0:0)"""
         return self._function_event.relative_position
 
     @property
     def args(self) -> list[LLVMArgument]:
+        """Returns a list of LLVMArgument objects representing the arguments of the LLVM function."""
         return [LLVMArgument(arg) for arg in self._function_event.args]
 
 
 @final
 class LLVMHookEvent(LLVMStepEvent):
+    """
+    Represents a hook event in LLVM execution.
+
+    Attributes:
+        _hook_event (llvm_hook_event): The underlying hook event object.
+
+    Methods:
+        __init__(hook_event: llvm_hook_event): Initializes a new instance of the LLVMHookEvent class.
+
+        __repr__() -> str: Returns a string representation of the LLVMHookEvent object using the AST printing method.
+    """
+
     _hook_event: llvm_hook_event
 
     def __init__(self, hook_event: llvm_hook_event) -> None:
@@ -130,23 +209,39 @@ def __repr__(self) -> str:
 
     @property
     def name(self) -> str:
+        """Returns the attribute name of the hook event. Ex.: "INT.add" """
         return self._hook_event.name
 
     @property
     def relative_position(self) -> str:
+        """Returns the relative position of the hook event in the proof trace. Ex.: (0:0:0:0)"""
         return self._hook_event.relative_position
 
     @property
     def args(self) -> list[LLVMArgument]:
+        """Returns a list of LLVMArgument objects representing the arguments of the hook event."""
         return [LLVMArgument(arg) for arg in self._hook_event.args]
 
     @property
     def result(self) -> Pattern:
+        """Returns the result pattern of the hook event evaluation."""
         return self._hook_event.result
 
 
 @final
 class LLVMArgument:
+    """
+    Represents an LLVM argument.
+
+    Attributes:
+        _argument (Argument): The underlying Argument object. An argument is a wrapper object containing either a step event or a KORE pattern.
+
+    Methods:
+        __init__(self, argument: Argument) -> None: Initializes the LLVMArgument object.
+
+        __repr__(self) -> str: Returns a string representation of the LLVMArgument object using the AST printing method.
+    """
+
     _argument: Argument
 
     def __init__(self, argument: Argument) -> None:
@@ -157,6 +252,7 @@ def __repr__(self) -> str:
 
     @property
     def step_event(self) -> LLVMStepEvent:
+        """Returns the LLVMStepEvent associated with the argument if any."""
         if isinstance(self._argument.step_event, llvm_rule_event):
             return LLVMRuleEvent(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_side_condition_event):
@@ -172,18 +268,37 @@ def step_event(self) -> LLVMStepEvent:
 
     @property
     def kore_pattern(self) -> Pattern:
+        """Returns the KORE Pattern associated with the argument if any."""
         assert isinstance(self._argument.kore_pattern, Pattern)
         return self._argument.kore_pattern
 
     def is_kore_pattern(self) -> bool:
+        """Checks if the argument is a KORE Pattern."""
         return self._argument.is_kore_pattern()
 
     def is_step_event(self) -> bool:
+        """Checks if the argument is a step event."""
         return self._argument.is_step_event()
 
 
 @final
 class LLVMRewriteTrace:
+    """
+    Represents an LLVM rewrite trace.
+
+    Attributes:
+        _rewrite_trace (llvm_rewrite_trace): The underlying LLVM rewrite trace object.
+
+    Methods:
+        __init__(self, rewrite_trace: llvm_rewrite_trace) -> None: Initializes a new instance of the LLVMRewriteTrace class.
+        __repr__(self) -> str: Returns a string representation of the LLVMRewriteTrace object using the AST printing method.
+        version(self) -> int: Returns the version of the HINTS formart.
+        pre_trace(self) -> list[LLVMArgument]: Returns the pre-trace events as a list of LLVMArgument objects.
+        initial_config(self) -> LLVMArgument: Returns the initial configuration as an LLVMArgument object.
+        trace(self) -> list[LLVMArgument]: Returns the trace events as a list of LLVMArgument objects.
+        parse(trace: bytes, header: kore_header) -> LLVMRewriteTrace: Parses the given proof hints byte string using the given kore_header object to create an LLVMRewriteTrace object.
+    """
+
     _rewrite_trace: llvm_rewrite_trace
 
     def __init__(self, rewrite_trace: llvm_rewrite_trace) -> None: