Comment by zodiac

Does this require having a Rocq semantics of LLVM IR? Which one do you use?