Commits

David Lazar  committed 20e7598

Initial commit

  • Participants

Comments (0)

Files changed (2)

File siphash-tests.cry

+include "siphash.cry";
+
+allpass = alltests == ~zero;
+alltests = [t1 t2 t3 t4 t5 t6 t7];
+
+// key used in reference implementation and paper
+refKey : [128];
+refKey = join [0..15];
+
+// the example from the paper
+t0 = sipHash 2 4 refKey [0..14] == 0xa129ca6149be45e5;
+
+// simple case
+t1 = sipHash 2 4 zero [] == 0x1e924b9d737700d7;
+
+/*
+Would like to write something like this to test the refVectors
+but we can't do [0..n-1].
+
+refTests : [64];
+refTests = [| sipHash 2 4 refKey [0..n-1] == join (refVectors @ n)
+           || n <- [0..63]
+           |];
+
+Ideas?
+*/
+
+// For now, we'll only test a few of them:
+t2 = sipHash 2 4 refKey [] == join (refVectors @ 0);
+t3 = sipHash 2 4 refKey [0] == join (refVectors @ 1);
+t4 = sipHash 2 4 refKey [0 1] == join (refVectors @ 2);
+t5 = sipHash 2 4 refKey [0 .. 60] == join (refVectors @ 61);
+t6 = sipHash 2 4 refKey [0 .. 61] == join (refVectors @ 62);
+t7 = sipHash 2 4 refKey [0 .. 62] == join (refVectors @ 63);
+
+refVectors : [64][8][8];
+refVectors = [
+  [ 0x31 0x0e 0x0e 0xdd 0x47 0xdb 0x6f 0x72 ]
+  [ 0xfd 0x67 0xdc 0x93 0xc5 0x39 0xf8 0x74 ]
+  [ 0x5a 0x4f 0xa9 0xd9 0x09 0x80 0x6c 0x0d ]
+  [ 0x2d 0x7e 0xfb 0xd7 0x96 0x66 0x67 0x85 ]
+  [ 0xb7 0x87 0x71 0x27 0xe0 0x94 0x27 0xcf ]
+  [ 0x8d 0xa6 0x99 0xcd 0x64 0x55 0x76 0x18 ]
+  [ 0xce 0xe3 0xfe 0x58 0x6e 0x46 0xc9 0xcb ]
+  [ 0x37 0xd1 0x01 0x8b 0xf5 0x00 0x02 0xab ]
+  [ 0x62 0x24 0x93 0x9a 0x79 0xf5 0xf5 0x93 ]
+  [ 0xb0 0xe4 0xa9 0x0b 0xdf 0x82 0x00 0x9e ]
+  [ 0xf3 0xb9 0xdd 0x94 0xc5 0xbb 0x5d 0x7a ]
+  [ 0xa7 0xad 0x6b 0x22 0x46 0x2f 0xb3 0xf4 ]
+  [ 0xfb 0xe5 0x0e 0x86 0xbc 0x8f 0x1e 0x75 ]
+  [ 0x90 0x3d 0x84 0xc0 0x27 0x56 0xea 0x14 ]
+  [ 0xee 0xf2 0x7a 0x8e 0x90 0xca 0x23 0xf7 ]
+  [ 0xe5 0x45 0xbe 0x49 0x61 0xca 0x29 0xa1 ]
+  [ 0xdb 0x9b 0xc2 0x57 0x7f 0xcc 0x2a 0x3f ]
+  [ 0x94 0x47 0xbe 0x2c 0xf5 0xe9 0x9a 0x69 ]
+  [ 0x9c 0xd3 0x8d 0x96 0xf0 0xb3 0xc1 0x4b ]
+  [ 0xbd 0x61 0x79 0xa7 0x1d 0xc9 0x6d 0xbb ]
+  [ 0x98 0xee 0xa2 0x1a 0xf2 0x5c 0xd6 0xbe ]
+  [ 0xc7 0x67 0x3b 0x2e 0xb0 0xcb 0xf2 0xd0 ]
+  [ 0x88 0x3e 0xa3 0xe3 0x95 0x67 0x53 0x93 ]
+  [ 0xc8 0xce 0x5c 0xcd 0x8c 0x03 0x0c 0xa8 ]
+  [ 0x94 0xaf 0x49 0xf6 0xc6 0x50 0xad 0xb8 ]
+  [ 0xea 0xb8 0x85 0x8a 0xde 0x92 0xe1 0xbc ]
+  [ 0xf3 0x15 0xbb 0x5b 0xb8 0x35 0xd8 0x17 ]
+  [ 0xad 0xcf 0x6b 0x07 0x63 0x61 0x2e 0x2f ]
+  [ 0xa5 0xc9 0x1d 0xa7 0xac 0xaa 0x4d 0xde ]
+  [ 0x71 0x65 0x95 0x87 0x66 0x50 0xa2 0xa6 ]
+  [ 0x28 0xef 0x49 0x5c 0x53 0xa3 0x87 0xad ]
+  [ 0x42 0xc3 0x41 0xd8 0xfa 0x92 0xd8 0x32 ]
+  [ 0xce 0x7c 0xf2 0x72 0x2f 0x51 0x27 0x71 ]
+  [ 0xe3 0x78 0x59 0xf9 0x46 0x23 0xf3 0xa7 ]
+  [ 0x38 0x12 0x05 0xbb 0x1a 0xb0 0xe0 0x12 ]
+  [ 0xae 0x97 0xa1 0x0f 0xd4 0x34 0xe0 0x15 ]
+  [ 0xb4 0xa3 0x15 0x08 0xbe 0xff 0x4d 0x31 ]
+  [ 0x81 0x39 0x62 0x29 0xf0 0x90 0x79 0x02 ]
+  [ 0x4d 0x0c 0xf4 0x9e 0xe5 0xd4 0xdc 0xca ]
+  [ 0x5c 0x73 0x33 0x6a 0x76 0xd8 0xbf 0x9a ]
+  [ 0xd0 0xa7 0x04 0x53 0x6b 0xa9 0x3e 0x0e ]
+  [ 0x92 0x59 0x58 0xfc 0xd6 0x42 0x0c 0xad ]
+  [ 0xa9 0x15 0xc2 0x9b 0xc8 0x06 0x73 0x18 ]
+  [ 0x95 0x2b 0x79 0xf3 0xbc 0x0a 0xa6 0xd4 ]
+  [ 0xf2 0x1d 0xf2 0xe4 0x1d 0x45 0x35 0xf9 ]
+  [ 0x87 0x57 0x75 0x19 0x04 0x8f 0x53 0xa9 ]
+  [ 0x10 0xa5 0x6c 0xf5 0xdf 0xcd 0x9a 0xdb ]
+  [ 0xeb 0x75 0x09 0x5c 0xcd 0x98 0x6c 0xd0 ]
+  [ 0x51 0xa9 0xcb 0x9e 0xcb 0xa3 0x12 0xe6 ]
+  [ 0x96 0xaf 0xad 0xfc 0x2c 0xe6 0x66 0xc7 ]
+  [ 0x72 0xfe 0x52 0x97 0x5a 0x43 0x64 0xee ]
+  [ 0x5a 0x16 0x45 0xb2 0x76 0xd5 0x92 0xa1 ]
+  [ 0xb2 0x74 0xcb 0x8e 0xbf 0x87 0x87 0x0a ]
+  [ 0x6f 0x9b 0xb4 0x20 0x3d 0xe7 0xb3 0x81 ]
+  [ 0xea 0xec 0xb2 0xa3 0x0b 0x22 0xa8 0x7f ]
+  [ 0x99 0x24 0xa4 0x3c 0xc1 0x31 0x57 0x24 ]
+  [ 0xbd 0x83 0x8d 0x3a 0xaf 0xbf 0x8d 0xb7 ]
+  [ 0x0b 0x1a 0x2a 0x32 0x65 0xd5 0x1a 0xea ]
+  [ 0x13 0x50 0x79 0xa3 0x23 0x1c 0xe6 0x60 ]
+  [ 0x93 0x2b 0x28 0x46 0xe4 0xd7 0x06 0x66 ]
+  [ 0xe1 0x91 0x5f 0x5c 0xb1 0xec 0xa4 0x6c ]
+  [ 0xf3 0x25 0x96 0x5c 0xa1 0x6d 0x62 0x9f ]
+  [ 0x57 0x5f 0xf2 0x8e 0x60 0x38 0x1b 0xe5 ]
+  [ 0x72 0x45 0x06 0xeb 0x4c 0x32 0x8a 0x95 ]
+];
+/* Cryptol specification of the SipHash function.
+ * Author: David Lazar <lazar6@illinois.edu>
+ * License: MIT
+ */
+
+sipHash : {b cw dw} (fin b, 8*(b/8)-b+7 >= 0) => [cw] -> [dw] -> [128] -> [b][8] -> [64];
+sipHash c d k m = finalize d (update c (parse m) (init k));
+
+initStr : [32][8];
+initStr = "somepseudorandomlygeneratedbytes";
+
+init : [128] -> [4][64];
+init k = [k0 k1 k0 k1] ^ iv
+  where {
+    [k0 k1] = split k;
+    iv = [| join (reverse x) || x <- groupBy(8, initStr) |];
+  };
+
+update : {a w} [a] -> [w][64] -> [4][64] -> [4][64];
+update c ms v' = rounds @ width ms
+  where {
+    rounds = [v'] # [| compress c m v || v <- rounds || m <- ms |];
+  };
+
+compress : {a} [a] -> [64] -> [4][64] -> [4][64];
+compress c m [v0 v1 v2 v3] = [(v0' ^ m) v1' v2' v3']
+  where {
+    [v0' v1' v2' v3'] = sipRounds [v0 v1 v2 (v3 ^ m)] @ c;
+  };
+
+finalize : {a} [a] -> [4][64] -> [64];
+finalize d [v0 v1 v2 v3] = v0' ^ v1' ^ v2' ^ v3'
+  where {
+    [v0' v1' v2' v3'] = sipRounds [v0 v1 (v2 ^ 0xff) v3] @ d;
+  };
+
+parse : {a} (fin a, 8*(a/8)-a+7 >= 0) => [a][8] -> [a/8 + 1][64];
+parse m = [| join x || x <- groupBy (8, pad m) |];
+
+// TODO why is the 8*(a/8)-a+7 >= 0 constraint needed?
+pad : {a} (fin a, 8*(a/8)-a+7 >= 0) => [a][8] -> [8 * (a/8 + 1)][8];
+pad m = m # zero # [b]
+  where {
+    // TODO this is clunky; how to improve it?
+    b = (width m % 256) @@ [0..7];
+  };
+
+sipRounds : [4][64] -> [inf][4][64];
+sipRounds v' = rounds
+  where {
+    rounds = [v'] # [| sipRound v || v <- rounds |];
+  };
+
+sipRound : [4][64] -> [4][64];
+sipRound [v0 v1 v2 v3] = [v0_3 v1_4 v2_3 v3_4]
+  where {
+    v0_1 = v0 + v1;  v1_1 = v1 <<< 13;  v1_2 = v1_1 ^ v0_1;  v0_2 = v0_1 <<< 32;
+    v2_1 = v2 + v3;  v3_1 = v3 <<< 16;  v3_2 = v3_1 ^ v2_1;
+
+    v0_3 = v0_2 + v3_2;  v3_3 = v3_2 <<< 21;  v3_4 = v3_3 ^ v0_3;
+    v2_2 = v2_1 + v1_2;  v1_3 = v1_2 <<< 17;  v1_4 = v1_3 ^ v2_2;  v2_3 = v2_2 <<< 32;
+  };