Prove that Edward Kmett's lsb implementation is correct

LSB.hs

module LSB(main) where

import Data.Word
import Data.Array.Unboxed
import Data.Bits
import Data.SBV

-- Kmett's implementation of finding the least significant bit set in a 64 bit word
-- Adapted from the original implementation at:
--    http://github.com/ekmett/algebra/blob/master/Numeric/Coalgebra/Geometric.hs#L72
lsbIndex :: SWord64 -> SWord8
lsbIndex n = select ix 0 (shiftR ((n .&. (-n)) * 0x07EDD5E59A4E28C2) 58)
  where
    ix = [ 63,  0, 58,  1, 59, 47, 53,  2
         , 60, 39, 48, 27, 54, 33, 42,  3
         , 61, 51, 37, 40, 49, 18, 28, 20
         , 55, 30, 34, 11, 43, 14, 22,  4
         , 62, 57, 46, 52, 38, 26, 32, 41
         , 50, 36, 17, 19, 29, 10, 13, 21
         , 56, 45, 25, 31, 35, 16,  9, 12
         , 44, 24, 15,  8, 23,  7,  6,  5
         ]

-- Obvious "reference implementation", simply walk through the bits. The only trick here
-- is the use of the counter value hitting 65 to stop the recursion.
lsbIndexRef :: SWord64 -> SWord8
lsbIndexRef n = go n 0
  where go n i = ite (i .== 65 ||| n .== 0 ||| lsb n)
                     i
                     (go (n `shiftR` 1) (i+1))

-- Correctness theorem
main :: IO ()
main = print =<< prove thm
  where thm :: SWord64 -> SBool
        thm x = x .== 0 ||| (lsbIndex x .== lsbIndexRef x)