Wording should be fixed to avoid calling these "cryptographic"

[TomMD]

Checksums aren't generally called hashes and these ones certainly aren't cryptographic. We should change the wording to reflect this fact.

An easy proof that alder32 is not cryptographic is in the simplicity of discovering a collision which, by definition, is computationally infeasible against a cryptographic hash. For example:

% cat adler.cry
import Cryptol::Extras

MOD_ADLER : [32]
MOD_ADLER = 65521

adler32 : {n} (fin n, n >= 0) => [n][8] -> [32]
adler32 dat = ((ys ! 0).1 << 16) || (ys ! 0).0
 where
 ys = [(1,0)] # [ (domod (a + pad d), domod (b + a)) | (a,b) <- ys | d <- dat ]
 domod x = x % MOD_ADLER
 pad x = zero # x
% cryptol adler.cry
Main> :sat \x y -> adler32 (x : [2][8]) == adler32 (y : [3][8])
(\x y -> adler32 (x : [2][8]) == adler32 (y : [3][8]))
  [0x7f, 0x10] [0x0e, 0x62, 0x1f] = True