author | wenzelm |
Mon, 20 Jan 2014 19:47:31 +0100 | |
changeset 55104 | 8284c0d5bf52 |
parent 53213 | a11e55f667db |
permissions | -rw-r--r-- |
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 | 31 |
("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"), |
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; |