Yes; see also the vellvm project, which develops proofs of a number of the equivalences LLVM uses: https://www.cis.upenn.edu/~stevez/vellvm/