Fun with sbv.

sbv_fun.hs

-- Fun with sbv, a theorem prover to haskell.
-- In this file I:
--  - Implement a bit twiddling reverse function.
--  - Use SMT to prove the twiddling function correct.
--  - Implement and prove correct some simple bit conversion functions.
--  - Use the reverse function and sbv's SAT solver to find bytes that are palindromes.

import Data.SBV

-- Functions for reversing 8 bits.

-- Bit twiddling hack to reverse a byte.
-- https://graphics.stanford.edu/~seander/bithacks.html#ReverseByteWith64BitsDiv
rev :: SWord8 -> SWord8
rev x = conv64To8 $ (((conv8To64 x)  * (0x0202020202 :: SWord64) .&. (0x010884422010 :: SWord64)) `sMod` 1023)

-- Reverse a byte using a bit blasting hack.
-- Blast to little endian, then read back in as big endian.
rev' :: SWord8 -> SWord8
rev' = fromBitsBE . blastLE

-- Use rev several times to build a function that can reverse 64 bits.
rev64 :: SWord64 -> SWord64
rev64 x = let (a, b) = split x
              ((c, d), (e, f)) = (split a, split b)
              ((g, h), (i, j), (k, l), (m, n)) = (split c, split d, split e, split f)
              in
              ((rev n # rev m) # (rev l # rev k)) # ((rev j # rev i) # (rev h # rev g))

rev64' :: SWord64 -> SWord64
rev64' = fromBitsBE . blastLE

-- Properties of these function, to be proved later in main.

-- The bit blasting and bit twiddling hack return the same result.
revIsEquivalentToRev' :: SWord8 -> SBool
revIsEquivalentToRev' x = rev x .== rev' x

-- Reversing twice leaves the value unchanged.
revRevIsIdentity :: SWord8 -> SBool
revRevIsIdentity x = (rev . rev) x .== x

-- Reversing twice leaves the value unchanged.
rev64Rev64IsIdentity :: SWord64 -> SBool
rev64Rev64IsIdentity x = (rev64 . rev64) x .== x

-- The bit blasting and bit twiddling hack return the same result.
rev64IsEquivalentToRev64' :: SWord64 -> SBool
rev64IsEquivalentToRev64' x = rev64 x .== rev64' x

-- Functions for converting between different word lengths.

-- Embed 8 bits into 64 bits.
conv8To64 :: SWord8 -> SWord64
conv8To64 = extend . extend . extend

halveBits :: Splittable a c => a -> c
halveBits = snd . split

-- Truncate 64 bits to 8 bits.
conv64To8 :: SWord64 -> SWord8
conv64To8 = halveBits . halveBits . halveBits

-- Properties of these functions.

-- Converting from 8 to 64 back to 8 leaves value unchanged.
conv8To64To8IsIdentity :: SWord8 -> SBool
conv8To64To8IsIdentity n = (conv64To8 . conv8To64) n .== n

-- Converting from 64 to 8 to 64 will fail for some values.
-- Later this is used to find a counter example.
conv64To8To64FailsForSomeValues = do
  x <- exists_
  return $ (conv8To64 . conv64To8) x ./= x

-- Palindrome code. First the property, then code for
-- extracting a model of palindromes.

-- Predicate is true for bytes that are palindromes.
palindromeBytes :: SWord8 -> SBool
palindromeBytes n = rev n .== n

-- Use reverse function to find bytes that are palindromes.
findPalindromeBytes :: IO [Word8]
findPalindromeBytes = do
  palindromes <- allSat palindromeBytes
  return $ extractModels palindromes

-- Call the solver for each property and print the results.
main = do
  putStrLn "Proving (rev . rev) == id"
  revRes <- prove revRevIsIdentity
  print revRes
  putStrLn "Proving rev == rev'"
  revRes' <- prove revIsEquivalentToRev'
  print revRes'
  putStrLn "Proving (rev64 . rev64) == id"
  revRes'' <- prove rev64Rev64IsIdentity
  print revRes''
  putStrLn "Proving rev64 == rev64'"
  revRes''' <- prove rev64IsEquivalentToRev64'
  print revRes'''
  putStrLn "Proving (conv64To8 . conv8To64) == id"
  convRes <- prove conv8To64To8IsIdentity
  print convRes
  putStrLn "Proving that (conv8To64 . conv64To8) /= id"
  convCounterEx <- prove conv64To8To64FailsForSomeValues
  print convCounterEx
  putStrLn "Finding example where (conv8To64 . conv64To8) /= id"
  convCounterEx' <- sat conv64To8To64FailsForSomeValues
  print convCounterEx'
  putStrLn "Finding bytes that are palindromes"
  palindromes <- findPalindromeBytes
  print palindromes

Feels like magic.

λ: main
Proving (rev . rev) == id
Q.E.D.
Proving rev == rev'
Q.E.D.
Proving (rev64 . rev64) == id
Q.E.D.
Proving rev64 == rev64'
Q.E.D.
Proving (conv64To8 . conv8To64) == id
Q.E.D.
Proving that (conv8To64 . conv64To8) /= id
Q.E.D.
Finding example where (conv8To64 . conv64To8) /= id
Satisfiable. Model:
  s0 = 18446744073692774144 :: SWord64
Finding bytes that are palindromes
[0,36,24,60,129,153,66,195,165,102,231,90,189,126,219,255]