I'm curious about your workflow (or the one in the blog post), I have been doing some experiments proving things about existing binaries and it's been extremely slow progress.

▲

sestep 2 hours ago | parent [-]

Yeah it took a bit to decide which abstraction level to target but I ended up choosing LLVM IR (planning to try PTX soon). It's been pretty successful so far for SIMD stuff, although proving theorems about concurrent programs seems a lot slower so far.

▲

zodiac 2 hours ago | parent [-]

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.