Using SBV to break the hash described in http://twistedoakstudios.com/blog/Post4706_breaking-a-toy-hash-function

gistfile1.hs

-- http://twistedoakstudios.com/blog/Post4706_breaking-a-toy-hash-function

import Data.List (findIndex)
import Control.Monad (guard)
import Data.Maybe (fromMaybe)
import Data.SBV.Bridge.Boolector
import Control.Monad.State
import Control.Applicative

codebook :: [Char]
codebook = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789`~!@#$%^&*()_+-=|[];',.{}:<>? "

encodeChar :: Char -> Word8
encodeChar c = fromIntegral $ fromMaybe (length codebook + 1) $ findIndex (== c) codebook

decodeChar :: Word8 -> Maybe Char
decodeChar x = do
    guard $ x' < length codebook
    return $ codebook !! x'
  where
    x' = fromIntegral x

type SChar = SWord8

-- | The hash function from the WC3 map
hash :: (Splittable a' a, Splittable a'' a', SignCast a'' h, Num h, SDivisible h) => [a] -> (h, h)
hash s = execState `flip` (0, 0) $ forM_ s $ \c -> do
    let c' = signCast . extend . extend $ c
    step c'
  where
    -- step :: SInt32 -> State (SInt32, SInt32) ()
    step c = replicateM_ 17 $ do
        (a, b) <- get
        let a' = a * (-6)   + b  + 0x74FA - c
            b' = b `sQuot` 3 + a' + 0x81BE - c
        put (a', b')

-- | Test against known solution, using 'hash' as a pure function
test1 :: Bool
test1 = (hash . map encodeChar $ "Procyon") == head targets

-- | Try to find a preimage of 7 characters
preimage7 :: (SInt32, SInt32) -> IO SatResult
preimage7 target = sat $ forSome (vars 7) $ \s1 s2 s3 s4 s5 s6 s7 ->
  let s = [s1, s2, s3, s4, s5, s6, s7] :: [SChar]
  in hash s .== target

vars :: Int -> [String]
vars k = [ 'c':show i | i <- [1..k] ]

targets :: (Num a) => [(a, a)]
targets = [(0x605D4A4F, 0x7EDDB1E5)]