I have re-written SHA1 so that is more idiomatically haskell and it is easy to see how it implements the specification. The only problem is I now have a space leak. I can see where the leak is but I'm less sure what to do about getting rid of it.
Here's the offending function:
pad :: [Word8] -> [Word8] pad xs = xs ++ [0x80] ++ ps ++ lb where l = length xs pl = (64-(l+9)) `mod` 64 ps = replicate pl 0x00 lb = i2osp 8 (8*l)
I would try something along the following lines (untested): \begin{spec} catWithLen xs f = xs ++ f (length xs) \end{spec} \begin{code} catWithLen :: [a] -> (Int -> [a]) -> [a] catWithLen xs f = h 0 xs where h k [] = f k h k (x : xs) = case succ k of -- forcing evaluation k' -> x : h k' xs \end{code} \begin{code} pad :: [Word8] -> [Word8] pad xs = catWithLen xs f where f l = 0x80 : ps lb where -- we know that |l = length xs| pl = (64-(l+9)) `mod` 64 ps = funPow pl (0x00 :) lb = i2osp 8 (8*l) \end{code} If you are lucky, then the replicate and the (++lb) in the original code might be fused by the compiler as an instance of foldr-build or something related --- check the optimised core code. In my variant I changed this to rely on efficient function powering instead: \begin{spec} funPow k f = foldr (.) id $ replicate k f \end{spec} \begin{code} funPow :: Int -> (a -> a) -> (a -> a) funPow n f = case compare n 0 of LT -> error ("funPow: negative argument: " ++ show n) EQ -> id GT -> pow n f where pow m g = if m > 1 then let (m',r) = divMod m 2 g' = g . g in if r == 0 then pow m' g' else pow m' g' . g else g \end{code} (You will probably also consider using Data.Bits for (`mod` 64), (8*), and (`divMod` 2). ) Wolfram