Specification Requests

Is anyone up to the task (however small) of specifying FNV in cryptol?

http://en.wikipedia.org/wiki/Fowler_Noll_Vo_hash

If so, thanks!

TOD: Late. Testing: Minimal. Code:

fnv1a : {n} (fin n) => [n] -> [64]
fnv1a ws = fnv1a' (pad ws)

pad : {msgLen,chunks,padding}
     ( fin msgLen
     , chunks     == (msgLen+7) / 8
     , padding    == (8 - msgLen % 8) % 8
     )
     => [msgLen] -> [chunks][8]
pad msg = split (msg # (zero:[padding]))

fnv1a' : {chunks} (fin chunks) => [chunks][8] -> [64]
fnv1a' msg = Ss ! 0
  where
   Ss = [fnv1a_offset_basis] #
           [ block s m
           | s <- Ss
           | m <- msg
           ]

block : {padding} ( padding == 64 - 8) => [64] -> [8] -> [64]
block state val = (state ^ ((zero : [padding]) # val)) * fnv1a_prime

fnv1a_offset_basis : [64]
fnv1a_offset_basis = 14695981039346656037

fnv1a_prime : [64]
fnv1a_prime = 1099511628211