From a04a2444a5b6f0549a9fe567e2e229ff559aa503 Mon Sep 17 00:00:00 2001 From: Dylan McNamee Date: Mon, 21 Apr 2014 13:50:00 -0700 Subject: [PATCH] Note: NIST 180-4 has an inconsistency in section 4.1.1 - the prose says 0<=t<=80, but the formula says 0<=t<=79. Later, they refer to 80 elements, so we're going with the formula's specification --- examples/SHA1.cry | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/SHA1.cry b/examples/SHA1.cry index bb27ed1c..4838e179 100644 --- a/examples/SHA1.cry +++ b/examples/SHA1.cry @@ -3,7 +3,7 @@ * Distributed under the terms of the BSD3 license (see LICENSE file) */ -// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-1.htm +// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-4.htm sha1 msg = sha1' pmsg where @@ -42,7 +42,7 @@ f (t, x, y, z) = if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z) | (20 <= t) && (t <= 39) then x ^ y ^ z | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z) - | (60 <= t) && (t <= 80) then x ^ y ^ z + | (60 <= t) && (t <= 79) then x ^ y ^ z else error "f: t out of range" Ks : [80][32]