Construct an appropriate `is_mergable` heuristic for merging nodes and composable verification.

Currently, we have implemented a language-agnostic merge_node (K#4425). However, applying it to practical scenarios and solving problems like Kontrol#448 still requires addressing the following challenges:

1. From the verification user’s perspective, what are the understandable benefits of merged nodes? For example, loop-invariant generation or support for composable verification at the function level?
2. From a requirements/theoretical perspective, what kind of nodes are mergable or are reasonable to be merged?
3. From a technical perspective, how to distinguish them by a simple specification.
4. Theoretical reliability analysis: Can these specifications theoretically meet our requirements?
5. Implementation reliability analysis: Can our implementation achieve the theoretical results?

Some answers to the above issues:

1. According to the current, users are easy to check the unexpected result of the auto-merged function spec. However, they cannot specify concrete behavior of that function. They can only specify the function under different status.

Here are some small steps/tasks that I plan to complete next:

• https://github.com/runtimeverification/evm-semantics/pull/2627; https://github.com/runtimeverification/evm-semantics/pull/2626
• #824
• Determine how to use logical specifications to describe it.
• Implement this specification in KEVM.
• Check the result in Kontrol. #829
• Provide more node-merging examples/case, e.g., LIDO ...