Implement parser from Binary kore to https://github.com/runtimeverification/proof-generation/pull/48
We can do this in one of these in one of two ways:
a. Implement a direct parser
b. Implement a conversion from Pyk's Kore data structures to our datastructures.
We need a python parser for the LLVM's binary proof hint file. The proof hint will be parsed into a
Task
such as in https://github.com/runtimeverification/proof-generation/blob/main/ml/rewrite/tasks.py#L350.Note that we cannot use Pyk's Kore data-structures for representing Kore, but must instead use this: https://github.com/runtimeverification/proof-generation/blob/main/ml/kore/ast.py