Implement BMC (bounded model checking) mode

[lucasmt]

This PR adds a --bmc-depth N option to kmir prove that enables bounded model checking by setting a bound on the number of iterations explored for each loop with a symbolic looping condition. It implements the is_loop and same_loop functions for identifying and comparing loop heads, which enable the BMC functionality present in pyk to be used with KMIR. Additionally, it includes unit tests of these functions and integration tests demonstrating that the implementation works in example Rust programs with loops.

Implementation Caveats

This initial implementation uses a simplified and somewhat overgeneralized definition of loop heads. Any branch, whether it is from a loop or not, is considered a loop head (note that this is the same behavior as the BMC implementation for the KEVM semantics). This is safe in most cases since a branching instruction that is not a loop is generally not revisited multiple times, but in some specific cases it might cause executions to be cut short unnecessarily: for example, if branching happens inside a function that is called multiple times in succession, the branches might be considered repetitions of the same loop head.

An alternative would be to identify loop heads by a static analysis of the program's control-flow graph built from the SMIR JSON. This would involve a depth-first search looking for back edges (edges that return to a previously-visited basic block), which would then be marked as loop heads. This would make the implementation more complex, and would either require breaking on every basic block terminator so pyk can check if it is a loop head (which would increase the size of the KCFG and potentially also bound loops with concrete looping conditions) or do additional analysis to identify which loop a branching node belongs to.