jkff / digest Goto Github PK

% 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