# HG changeset patch # User wenzelm # Date 1267973489 -3600 # Node ID f1456d045151406ef0da6f085493b398acb34cfa # Parent 6cec06ef67a79f86a493966c8176dff787c37446 Digesting strings according to SHA-1. diff -r 6cec06ef67a7 -r f1456d045151 src/Pure/General/sha1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/sha1.ML Sun Mar 07 15:51:29 2010 +0100 @@ -0,0 +1,129 @@ +(* Title: Pure/General/sha1.ML + Author: Makarius + +Digesting strings according to SHA-1 (see RFC 3174) -- relatively slow +version in pure ML. +*) + +signature SHA1 = +sig + val digest: string -> string +end; + +structure SHA1: SHA1 = +struct + +(* 32bit words *) + +infix 4 << >>; +infix 3 andb; +infix 2 orb xorb; + +val op << = Word32.<<; +val op >> = Word32.>>; +val op andb = Word32.andb; +val op orb = Word32.orb; +val op xorb = Word32.xorb; +val notb = Word32.notb; + +fun rotate k w = w << k orb w >> (0w32 - k); + + +(* hexadecimal words *) + +fun hex_digit (text, w: Word32.word) = + let + val d = Word32.toInt (w andb 0wxf); + val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10); + in (dig ^ text, w >> 0w4) end; + +fun hex_word w = #1 (funpow 8 hex_digit ("", w)); + + +(* padding *) + +fun pack_bytes 0 n = "" + | pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256); + +fun padded_text str = + let + val len = size str; + val padding = chr 128 ^ replicate_string (~ (len + 9) mod 64) (chr 0) ^ pack_bytes 8 (len * 8); + fun byte i = Char.ord (String.sub (if i < len then (str, i) else (padding, (i - len)))); + fun word i = + Word32.fromInt (byte (4 * i)) << 0w24 orb + Word32.fromInt (byte (4 * i + 1)) << 0w16 orb + Word32.fromInt (byte (4 * i + 2)) << 0w8 orb + Word32.fromInt (byte (4 * i + 3)); + in ((len + size padding) div 4, word) end; + + +(* digest *) + +fun digest_word (i, w, {a, b, c, d, e}) = + let + val {f, k} = + if i < 20 then + {f = (b andb c) orb (notb b andb d), + k = 0wx5A827999} + else if i < 40 then + {f = b xorb c xorb d, + k = 0wx6ED9EBA1} + else if i < 60 then + {f = (b andb c) orb (b andb d) orb (c andb d), + k = 0wx8F1BBCDC} + else + {f = b xorb c xorb d, + k = 0wxCA62C1D6}; + val op + = Word32.+; + in + {a = rotate 0w5 a + f + e + w + k, + b = a, + c = rotate 0w30 b, + d = c, + e = d} + end; + +fun digest str = + let + val (text_len, text) = padded_text str; + + (*hash result -- 5 words*) + val hash_array : Word32.word Array.array = + Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0]; + fun hash i = Array.sub (hash_array, i); + fun add_hash x i = Array.update (hash_array, i, hash i + x); + + (*current chunk -- 80 words*) + val chunk_array = Array.array (80, 0w0: Word32.word); + fun chunk i = Array.sub (chunk_array, i); + fun init_chunk pos = + Array.modifyi (fn (i, _) => + if i < 16 then text (pos + i) + else rotate 0w1 (chunk (i - 3) xorb chunk (i - 8) xorb chunk (i - 14) xorb chunk (i - 16))) + chunk_array; + + fun digest_chunks pos = + if pos < text_len then + let + val _ = init_chunk pos; + val {a, b, c, d, e} = Array.foldli digest_word + {a = hash 0, + b = hash 1, + c = hash 2, + d = hash 3, + e = hash 4} + chunk_array; + val _ = add_hash a 0; + val _ = add_hash b 1; + val _ = add_hash c 2; + val _ = add_hash d 3; + val _ = add_hash e 4; + in digest_chunks (pos + 16) end + else (); + val _ = digest_chunks 0; + + val hex = hex_word o hash; + in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end; + +end; diff -r 6cec06ef67a7 -r f1456d045151 src/Pure/General/sha1_polyml.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/sha1_polyml.ML Sun Mar 07 15:51:29 2010 +0100 @@ -0,0 +1,29 @@ +(* Title: Pure/General/sha1_polyml.ML + Author: Sascha Boehme, TU Muenchen + +Digesting strings according to SHA-1 (see RFC 3174) -- based on an +external implementation in C with a fallback to an internal +implementation. +*) + +structure SHA1: SHA1 = +struct + +fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10); + +fun hex_string arr i = + let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr) + in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end + +fun digest_external str = + let + val digest = CInterface.alloc 20 CInterface.Cchar; + val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer") + (CInterface.STRING, CInterface.INT, CInterface.POINTER) + CInterface.POINTER (str, size str, CInterface.address digest); + in fold (suffix o hex_string digest) (0 upto 19) "" end; + +fun digest str = digest_external str + handle CInterface.Foreign _ => SHA1.digest str; + +end; diff -r 6cec06ef67a7 -r f1456d045151 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sun Mar 07 15:49:49 2010 +0100 +++ b/src/Pure/IsaMakefile Sun Mar 07 15:51:29 2010 +0100 @@ -57,8 +57,9 @@ General/markup.ML General/name_space.ML General/ord_list.ML \ General/output.ML General/path.ML General/position.ML \ General/pretty.ML General/print_mode.ML General/properties.ML \ - General/queue.ML General/same.ML General/scan.ML General/secure.ML \ - General/seq.ML General/source.ML General/stack.ML General/symbol.ML \ + General/queue.ML General/same.ML General/scan.ML General/sha1.ML \ + General/sha1_polyml.ML General/secure.ML General/seq.ML \ + General/source.ML General/stack.ML General/symbol.ML \ General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \ General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ diff -r 6cec06ef67a7 -r f1456d045151 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Mar 07 15:49:49 2010 +0100 +++ b/src/Pure/ROOT.ML Sun Mar 07 15:51:29 2010 +0100 @@ -52,6 +52,11 @@ use "General/xml.ML"; use "General/yxml.ML"; +use "General/sha1.ML"; +if String.isPrefix "polyml" ml_system +then use "General/sha1_polyml.ML" +else (); + (* concurrency within the ML runtime *)