src/Pure/General/sha1_samples.ML
author wenzelm
Mon, 20 Jan 2014 19:47:31 +0100
changeset 55104 8284c0d5bf52
parent 53213 a11e55f667db
permissions -rw-r--r--
clarified scan_cartouche_depth, according to Scala version; more accurate error position;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53212
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/sha1_samples.ML
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     3
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     4
Some SHA1 samples found in the wild.
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     5
*)
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     6
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     7
signature SHA1_SAMPLES =
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     8
sig
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
     9
  val test: unit -> unit
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    10
end;
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    11
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    12
structure SHA1_Samples: SHA1_SAMPLES =
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    13
struct
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    14
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    15
fun check (msg, key) =
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    16
  let val key' = SHA1.rep (SHA1.digest msg) in
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    17
    if key = key' then ()
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    18
    else
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    19
      raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    20
        key ^ " expected, but\n" ^ key' ^ " was found")
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    21
  end;
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    22
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    23
fun test () =
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    24
  List.app check
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    25
   [("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"),
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    26
    ("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"),
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    27
    ("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"),
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    28
    ("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"),
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    29
    ("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"),
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    30
    (replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"),
53213
a11e55f667db another sample found by Stefan Berghofer;
wenzelm
parents: 53212
diff changeset
    31
    ("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"),
a11e55f667db another sample found by Stefan Berghofer;
wenzelm
parents: 53212
diff changeset
    32
    ("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")];
53212
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    33
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    34
val _ = test ();
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    35
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents:
diff changeset
    36
end;