| author | steckerm | 
| Sat, 20 Sep 2014 10:42:08 +0200 | |
| changeset 58401 | b8ca69d9897b | 
| 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; |