src/Pure/General/sha1.ML
author wenzelm
Thu, 15 Jun 2023 14:28:17 +0200
changeset 78158 8b5a2e4b16d4
parent 77896 a9626bcb0c3b
child 78716 97dfba4405e3
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/sha1.ML
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
     3
    Author:     Sascha Boehme, TU Muenchen
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     4
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
     5
Digesting strings according to SHA-1 (see RFC 3174).
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     6
*)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     7
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     8
signature SHA1 =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
     9
sig
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
    10
  eqtype digest
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
    11
  val rep: digest -> string
57638
ed58e740a699 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents: 41954
diff changeset
    12
  val fake: string -> digest
62702
e29f47e04180 tuned signature;
wenzelm
parents: 62666
diff changeset
    13
  val digest: string -> digest
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    14
  val test_samples: unit -> unit
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    15
end;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    16
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    17
structure SHA1: SHA1 =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    18
struct
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    19
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    20
(** internal implementation in ML -- relatively slow **)
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    21
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    22
local
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    23
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    24
(* 32bit words *)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    25
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    26
infix 4 << >>;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    27
infix 3 andb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    28
infix 2 orb xorb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    29
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    30
val op << = Word32.<<;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    31
val op >> = Word32.>>;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    32
val op andb = Word32.andb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    33
val op orb = Word32.orb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    34
val op xorb = Word32.xorb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    35
val notb = Word32.notb;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    36
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    37
fun rotate k w = w << k orb w >> (0w32 - k);
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    38
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    39
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    40
(* hexadecimal words *)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    41
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    42
fun hex_digit (text, w: Word32.word) =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    43
  let
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    44
    val d = Word32.toInt (w andb 0wxf);
64275
ac2abc987cf9 accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents: 62819
diff changeset
    45
    val dig = if d < 10 then chr (Char.ord #"0" + d) else chr (Char.ord #"a" + d - 10);
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    46
  in (dig ^ text, w >> 0w4) end;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    47
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    48
fun hex_word w = #1 (funpow 8 hex_digit ("", w));
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    49
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    50
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    51
(* padding *)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    52
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    53
fun pack_bytes 0 _ = ""
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    54
  | pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256);
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    55
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    56
fun padded_text str =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    57
  let
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    58
    val len = size str;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    59
    val padding = chr 128 ^ replicate_string (~ (len + 9) mod 64) (chr 0) ^ pack_bytes 8 (len * 8);
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    60
    fun byte i = Char.ord (String.sub (if i < len then (str, i) else (padding, (i - len))));
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    61
    fun word i =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    62
      Word32.fromInt (byte (4 * i)) << 0w24 orb
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    63
      Word32.fromInt (byte (4 * i + 1)) << 0w16 orb
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    64
      Word32.fromInt (byte (4 * i + 2)) << 0w8 orb
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    65
      Word32.fromInt (byte (4 * i + 3));
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    66
  in ((len + size padding) div 4, word) end;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    67
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    68
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    69
(* digest_string_internal *)
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    70
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    71
fun digest_word (i, w, {a, b, c, d, e}) =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    72
  let
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    73
    val {f, k} =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    74
      if i < 20 then
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    75
        {f = (b andb c) orb (notb b andb d),
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    76
         k = 0wx5A827999}
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    77
      else if i < 40 then
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    78
        {f = b xorb c xorb d,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    79
         k = 0wx6ED9EBA1}
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    80
      else if i < 60 then
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    81
        {f = (b andb c) orb (b andb d) orb (c andb d),
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    82
         k = 0wx8F1BBCDC}
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    83
      else
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    84
        {f = b xorb c xorb d,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    85
         k = 0wxCA62C1D6};
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    86
    val op + = Word32.+;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    87
  in
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    88
    {a = rotate 0w5 a + f + e + w + k,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    89
     b = a,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    90
     c = rotate 0w30 b,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    91
     d = c,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    92
     e = d}
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    93
  end;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    94
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    95
in
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    96
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
    97
fun digest_string_internal str =
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    98
  let
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
    99
    val (text_len, text) = padded_text str;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   100
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   101
    (*hash result -- 5 words*)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   102
    val hash_array : Word32.word Array.array =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   103
      Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
77888
wenzelm
parents: 72661
diff changeset
   104
    val hash = Array.nth hash_array;
77896
a9626bcb0c3b tuned signature;
wenzelm
parents: 77888
diff changeset
   105
    fun add_hash x i = Array.upd hash_array i (hash i + x);
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   106
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   107
    (*current chunk -- 80 words*)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   108
    val chunk_array = Array.array (80, 0w0: Word32.word);
77888
wenzelm
parents: 72661
diff changeset
   109
    val chunk = Array.nth chunk_array;
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   110
    fun init_chunk pos =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   111
      Array.modifyi (fn (i, _) =>
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   112
        if i < 16 then text (pos + i)
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   113
        else rotate 0w1 (chunk (i - 3) xorb chunk (i - 8) xorb chunk (i - 14) xorb chunk (i - 16)))
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   114
      chunk_array;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   115
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   116
    fun digest_chunks pos =
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   117
      if pos < text_len then
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   118
        let
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   119
          val _ = init_chunk pos;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   120
          val {a, b, c, d, e} = Array.foldli digest_word
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   121
            {a = hash 0,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   122
             b = hash 1,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   123
             c = hash 2,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   124
             d = hash 3,
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   125
             e = hash 4}
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   126
            chunk_array;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   127
          val _ = add_hash a 0;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   128
          val _ = add_hash b 1;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   129
          val _ = add_hash c 2;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   130
          val _ = add_hash d 3;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   131
          val _ = add_hash e 4;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   132
        in digest_chunks (pos + 16) end
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   133
      else ();
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   134
    val _  = digest_chunks 0;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   135
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   136
    val hex = hex_word o hash;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   137
  in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end;
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   138
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   139
end;
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
   140
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   141
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   142
(** external implementation in C **)
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   143
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   144
local
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   145
64334
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   146
(* C library and memory *)
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   147
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   148
val library_path =
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   149
  Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   150
72554
81518b38b316 prefer static library_call (again): avoid memory-leak within C code area;
wenzelm
parents: 72537
diff changeset
   151
val library_call =
72534
e0c6522d5d43 prefer static library_call, following recent changes to structure Foreign;
wenzelm
parents: 68087
diff changeset
   152
  Foreign.buildCall3
72661
fca4d6abebda more robust library_call (again): dynamic file name, static symbol;
wenzelm
parents: 72554
diff changeset
   153
    (Foreign.getSymbol
fca4d6abebda more robust library_call (again): dynamic file name, static symbol;
wenzelm
parents: 72554
diff changeset
   154
      (Foreign.loadLibraryIndirect (fn () => File.platform_path library_path)) "sha1_buffer",
72554
81518b38b316 prefer static library_call (again): avoid memory-leak within C code area;
wenzelm
parents: 72537
diff changeset
   155
      (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
72535
7cb68b5b103d proper build_call for interpreted ARM platform;
wenzelm
parents: 72534
diff changeset
   156
64334
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   157
fun with_memory n =
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   158
  Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   159
    let
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   160
      val mem = Foreign.Memory.malloc (Word.fromInt n);
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   161
      val res = Exn.capture (restore_attributes f) mem;
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   162
      val _ = Foreign.Memory.free mem;
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   163
    in Exn.release res end);
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   164
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   165
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   166
(* digesting *)
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   167
64334
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   168
fun hex_string byte = op ^ (apply2 hex_digit (Integer.div_mod (Word8.toInt byte) 16));
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   169
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   170
in
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   171
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   172
fun digest_string_external str =
64334
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   173
  with_memory 20 (fn mem =>
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   174
    let
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   175
      val bytes = Byte.stringToBytes str;
72534
e0c6522d5d43 prefer static library_call, following recent changes to structure Foreign;
wenzelm
parents: 68087
diff changeset
   176
      val _ = library_call (bytes, Word8Vector.length bytes, mem);
64334
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   177
      fun get i = hex_string (Foreign.Memory.get8 (mem, Word.fromInt i));
4fb8560df827 updated to new structure Foreign;
wenzelm
parents: 64275
diff changeset
   178
    in implode (map get (0 upto 19)) end);
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   179
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   180
end;
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   181
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   182
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   183
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   184
(** type digest **)
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
   185
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
   186
datatype digest = Digest of string;
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
   187
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 35628
diff changeset
   188
fun rep (Digest s) = s;
57638
ed58e740a699 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents: 41954
diff changeset
   189
val fake = Digest;
ed58e740a699 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents: 41954
diff changeset
   190
62819
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62702
diff changeset
   191
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 57638
diff changeset
   192
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   193
fun digest_string str = digest_string_external str
67202
30e863ad5a1a proper exception;
wenzelm
parents: 64334
diff changeset
   194
  handle Foreign.Foreign msg =>
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   195
    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str);
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   196
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   197
val digest = Digest o digest_string;
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   198
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   199
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   200
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   201
(** SHA1 samples found in the wild **)
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   202
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   203
local
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   204
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   205
fun check (msg, key) =
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   206
  let val key' = rep (digest msg) in
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   207
    if key = key' then ()
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   208
    else
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   209
      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   210
        key ^ " expected, but\n" ^ key' ^ " was found")
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   211
  end;
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   212
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   213
in
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   214
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   215
fun test_samples () =
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   216
  List.app check
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   217
   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   218
    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   219
    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   220
    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   221
    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   222
    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   223
    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   224
    ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   225
35628
f1456d045151 Digesting strings according to SHA-1.
wenzelm
parents:
diff changeset
   226
end;
62666
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   227
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   228
val _ = test_samples ();
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   229
00aff1da05ae clarified modules;
wenzelm
parents: 62663
diff changeset
   230
end;