FNV.cry

/*
  Copyright (c) 2014-2018, Galois Inc.
  www.cryptol.net
 */

module Primitive::Keyless::Hash::FNV where

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

pad : {msgLen} (fin msgLen) => [msgLen] -> [msgLen /^ 8][8]
pad msg = split (msg # (zero:[msgLen %^ 8]))

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

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

fnv1a_offset_basis : [64]
fnv1a_offset_basis = 14695981039346656037

fnv1a_prime : [64]
fnv1a_prime = 1099511628211

t1 = fnv1a [] == 0xcbf29ce484222325
t2 = fnv1a (join "a") == 0xaf63dc4c8601ec8c
t3 = fnv1a (join "foobar") == 0x85944171f73967e8

property testsPass = and [t1, t2, t3]