0 |
  1 | ||| SipHash24 copied from C [reference implementation](https://github.com/veorq/SipHash/blob/master/siphash.c)
  2 | ||| and rust https://doc.rust-lang.org/src/core/hash/sip.rs.html
  3 | module Data.Hashable.SipHashV2
  4 |
  5 | import Data.Buffer
  6 |
  7 | %default total
  8 |
  9 | %inline
 10 | CROUNDS : Nat
 11 | CROUNDS = 2
 12 |
 13 | %inline
 14 | DROUNDS : Nat
 15 | DROUNDS = 4
 16 |
 17 | record HashState where
 18 |     constructor MkST
 19 |     v0 : Bits64
 20 |     v1 : Bits64
 21 |     v2 : Bits64
 22 |     v3 : Bits64
 23 |
 24 | initHashState : HashState
 25 | initHashState = MkST
 26 |     { v0 = 0x736f6d6570736575
 27 |     , v1 = 0x646f72616e646f6d
 28 |     , v2 = 0x6c7967656e657261
 29 |     , v3 = 0x7465646279746573
 30 |     }
 31 |
 32 | record PartialHash where
 33 |     constructor MkPartial
 34 |     tail : Bits64
 35 |     index : Bits64
 36 |     length : Bits64
 37 |     hst : HashState
 38 |
 39 | initPartial : PartialHash
 40 | initPartial = MkPartial 0 0 0 initHashState
 41 |
 42 | %inline
 43 | shl : Bits64 -> Bits64 -> Bits64
 44 | shl = prim__shl_Bits64
 45 |
 46 | %inline
 47 | shr : Bits64 -> Bits64 -> Bits64
 48 | shr = prim__shr_Bits64
 49 |
 50 | %inline
 51 | bor : Bits64 -> Bits64 -> Bits64
 52 | bor = prim__or_Bits64
 53 |
 54 | %inline
 55 | xor : Bits64 -> Bits64 -> Bits64
 56 | xor = prim__xor_Bits64
 57 |
 58 | %inline
 59 | and : Bits64 -> Bits64 -> Bits64
 60 | and = prim__and_Bits64
 61 |
 62 | %inline
 63 | shr16 : Bits16 -> Bits16 -> Bits16
 64 | shr16 = prim__shr_Bits16
 65 |
 66 | %inline
 67 | shr32 : Bits32 -> Bits32 -> Bits32
 68 | shr32 = prim__shr_Bits32
 69 |
 70 | %inline
 71 | andInt : Int -> Int -> Int
 72 | andInt = prim__and_Int
 73 |
 74 | %inline
 75 | %spec b
 76 | rotl : Bits64 -> (b : Bits64) -> Bits64
 77 | rotl x b = (x `shl` b) `bor` (x `shr` (64 - b))
 78 |
 79 | -- Make the length the smallest multiple of 8 tail >= the given number
 80 | %inline
 81 | fullSize : Int -> Int
 82 | fullSize x =
 83 |     let left = x `andInt` 7
 84 |      in if (x `andInt` 7) == 0
 85 |         then x
 86 |         else x - left + 8
 87 |
 88 | compress : HashState -> HashState
 89 | compress (MkST v0 v1 v2 v3) =
 90 |     let v0 = v0 + v1;
 91 |         v1 = v1 `rotl` 13;
 92 |         v1 = v1 `xor` v0;
 93 |         v0 = v0 `rotl` 32;
 94 |         v2 = v2 + v3;
 95 |         v3 = v3 `rotl` 16;
 96 |         v3 = v3 `xor` v2;
 97 |         v0 = v0 + v3;
 98 |         v3 = v3 `rotl` 21;
 99 |         v3 = v3 `xor` v0;
100 |         v2 = v2 + v1;
101 |         v1 = v1 `rotl` 17;
102 |         v1 = v1 `xor` v2;
103 |         v2 = v2 `rotl` 32;
104 |     in MkST v0 v1 v2 v3
105 |
106 | %inline
107 | %spec rounds, f
108 | repeat : (rounds : Nat) -> (f : a -> a) -> a -> a
109 | repeat Z f x = x
110 | repeat (S k) f x = repeat k f (f x)
111 |
112 | %inline
113 | hashBits64 : HashState -> Bits64 -> HashState
114 | hashBits64 (MkST v0 v1 v2 v3) m =
115 |     let v3 = v3 `xor` m
116 |         MkST v0 v1 v2 v3 = repeat CROUNDS compress $ MkST v0 v1 v2 v3
117 |         v0 = v0 `xor` m
118 |      in MkST v0 v1 v2 v3
119 |
120 | export
121 | finish : PartialHash -> Bits64
122 | finish (MkPartial tail index length hst) =
123 |     let MkST v0 v1 v2 v3 = hst
124 |         rest = ((length `and` 0xff) `shl` 56) `bor` tail
125 |         v3 = v3 `xor` rest
126 |         MkST v0 v1 v2 v3 = repeat CROUNDS compress $ MkST v0 v1 v2 v3
127 |         v0 = v0 `xor` rest
128 |         v2 = v2 `xor` 0xff
129 |         MkST v0 v1 v2 v3 = repeat DROUNDS compress $ MkST v0 v1 v2 v3
130 |      in (v0 `xor` v1) `xor` (v2 `xor` v3)
131 |
132 | export
133 | addBits8 : PartialHash -> Bits8 -> PartialHash
134 | addBits8 (MkPartial tail index len hs) x = case index of
135 |     -- finished a set of tail
136 |     56 => MkPartial 0 0 (len + 1) $ hashBits64 hs (tail `bor` (cast x `shl` 56))
137 |     -- add byte to partial
138 |     _ => MkPartial (tail `bor` (cast x `shl` index)) (index + 8) (len + 1) hs
139 |
140 | export
141 | addBits16 : PartialHash -> Bits16 -> PartialHash
142 | addBits16 ph x = addBits8 (addBits8 ph $ cast x) (cast $ x `shr16` 8)
143 |
144 | export
145 | addBits32 : PartialHash -> Bits32 -> PartialHash
146 | addBits32 ph x = addBits16 (addBits16 ph $ cast x) (cast $ x `shr32` 16)
147 |
148 | export
149 | addBits64 : PartialHash -> Bits64 -> PartialHash
150 | addBits64 (MkPartial tail index length hst) x = MkPartial tail index (length + 8) $ hashBits64 hst x
151 |
152 | hashBuffer' : PartialHash -> Buffer -> Int -> Int -> IO PartialHash
153 | hashBuffer' ph buf len idx = if idx >= len
154 |     then pure ph
155 |     else do
156 |         word <- getBits64 buf idx
157 |         let ph = addBits64 ph word
158 |         hashBuffer' ph buf len (assert_smaller idx $ idx + 8)
159 |
160 | hashBuffer : PartialHash -> Buffer -> IO PartialHash
161 | hashBuffer ph buf = do
162 |     rawLen <- rawSize buf
163 |     let len = fullSize rawLen
164 |     Just buf' <- resizeBuffer buf len
165 |         | Nothing => hashBuffer' ph buf (rawLen `andInt` (- 7)) 0
166 |     hashBuffer' ph buf' len 0
167 |