Been doing this at work for the past couple weeks. Extremely powerful to be able to have an agent open a PR with some experiments showing it makes some function faster using SIMD or CUDA, and just confidently merge it because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation.

▲

mattr03 2 hours ago | parent | next [-]

How do you gain confidence that your theorem actually applies to your code?

	▲	sestep 2 hours ago \| parent [-]
		My Rocq setup directly reads my actual code. And I fuzz my semantic models against the real machine.

▲

hedgehog 2 hours ago | parent | prev [-]

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.