mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-16 11:22:33 +03:00
7e34c25e4d
"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n. "x %^ y" is the least k such that x+k is a multiple of y. For comparison, "x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n. "x % y" is the least k such that x-k is a multiple of y. The new syntax is much more suggestive of the relation to "/" and "%".
35 lines
899 B
Plaintext
35 lines
899 B
Plaintext
/*
|
|
* Copyright (c) 2014-2016 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
|
|
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 = [t1, t2, t3] == ~zero
|