| ▲ | zodiac 2 hours ago | |
Does this require having a Rocq semantics of LLVM IR? Which one do you use? | ||
| ▲ | sestep an hour ago | parent [-] | |
No existing semantics are enough for my goals, so I'm building my own based on Vellvm, and proving "equivalence" theorems to it and other related work that specify what quirks/discrepancies/idiosyncrasies they have with respect to each other. | ||