0 | module Pack.Core.Hash

  2 | import Data.Array

  3 | import Data.Array.Core as AC

  4 | import Data.Array.Mutable

  5 | import Data.Bits

  6 | import Data.Buffer

  7 | import Data.Buffer.Core as BC

  8 | import Data.Buffer.Indexed

  9 | import Data.ByteString

 10 | import Data.ByteVect

 11 | import Data.Vect

 12 | import Text.ParseError

 13 | import Syntax.T1

 15 | %hide Data.Linear.(.)

 16 | %default total

 22 | %foreign "scheme:(lambda (buf o) (bytevector-u64-ref buf o 'little))"

 23 | prim__getBits64 : Buffer -> (offset : Integer) -> Bits64

 26 | o64 : Fin 16 -> Nat -> Integer

 27 | o64 x o = cast o + 8 * cast x

 30 | shr, shl, xor, or : Bits64 -> Bits64 -> Bits64

 31 | shr = prim__shr_Bits64

 32 | shl = prim__shl_Bits64

 33 | xor = prim__xor_Bits64

 34 | or  = prim__or_Bits64

 36 | rotr : Bits64 -> Bits64 -> Bits64

 37 | rotr w c = (w `shr` c) `or` (w `shl` (64-c))

 39 | parameters (v : MArray t n Bits64)

 41 |   %inline

 42 |   add : (x,y : Fin n) -> F1' t

 43 |   add x y = T1.do

 44 |     vx <- get v x

 45 |     vy <- get v y

 46 |     set v x (vx+vy)

 48 |   %inline

 49 |   addI : (x,y : Fin n) -> Bits64 -> F1' t

 50 |   addI x y i = T1.do

 51 |     vx <- get v x

 52 |     vy <- get v y

 53 |     set v x (vx+vy+i)

 55 |   %inline

 56 |   xorrot : (x,y : Fin n) -> Bits64 -> F1' t

 57 |   xorrot x y r = T1.do

 58 |     vx <- get v x

 59 |     vy <- get v y

 60 |     set v x (rotr (xor vx vy) r)

 62 |   %inline

 63 |   xorat : (x : Fin n) -> Bits64 -> F1' t

 64 |   xorat x r = T1.do

 65 |     vx <- get v x

 66 |     set v x (xor vx r)

 68 |   mix : (a,b,c,d : Fin n) -> (x,y : Bits64) -> F1' t

 69 |   mix a b c d x y = T1.do

 70 |     addI a b x    -- Va ← Va + Vb + x

 71 |     xorrot d a 32 -- Vd ← (Vd xor Va) rotateright 32

 72 |     add c d       -- Vc ← Vc + Vd

 73 |     xorrot b c 24 -- Vb ← (Vb xor Vc) rotateright 24

 74 |     addI a b y    -- Va ← Va + Vb + y

 75 |     xorrot d a 16 -- Vd ← (Vd xor Va) rotateright 16

 76 |     add c d       -- Vc ← Vc + Vd

 77 |     xorrot b c 63 -- Vb ← (Vb xor Vc) rotateright 63

 83 | sigma : IArray 12 (IArray 16 (Fin 16))

 84 | sigma =

 85 |   array

 86 |     [ array [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15]

 87 |     , array [14,10, 4, 8, 9,15,13, 6, 1,12, 0, 2,11, 7, 5, 3]

 88 |     , array [11, 8,12, 0, 5, 2,15,13,10,14, 3, 6, 7, 1, 9, 4]

 89 |     , array [ 7, 9, 3, 1,13,12,11,14, 2, 6, 5,10, 4, 0,15, 8]

 90 |     , array [ 9, 0, 5, 7, 2, 4,10,15,14, 1,11,12, 6, 8, 3,13]

 91 |     , array [ 2,12, 6,10, 0,11, 8, 3, 4,13, 7, 5,15,14, 1, 9]

 92 |     , array [12, 5, 1,15,14,13, 4,10, 0, 7, 6, 3, 9, 2, 8,11]

 93 |     , array [13,11, 7,14,12, 1, 3, 9, 5, 0,15, 4, 8, 6, 2,10]

 94 |     , array [ 6,15,14, 9,11, 3, 0, 8,12, 2,13, 7, 1, 4,10, 5]

 95 |     , array [10, 2, 8, 4, 7, 6, 1, 5,15,11, 9,14, 3,12,13, 0]

 96 |     , array [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15]

 97 |     , array [14,10, 4, 8, 9,15,13, 6, 1,12, 0, 2,11, 7, 5, 3]

 98 |     ]

100 | IV : IArray 8 Bits64

101 | IV =

102 |   array

103 |     [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b

104 |     , 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1

105 |     , 0x510e527fade682d1, 0x9b05688c2b3e6c1f

106 |     , 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179

107 |     ]

113 | mixIntoH : IArray 16 Bits64 -> MArray s 8 Bits64 -> F1' s

114 | mixIntoH i m = T1.do

115 |   xorat m 0 ((i `at` 0) `xor` (i `at` 8))

116 |   xorat m 1 ((i `at` 1) `xor` (i `at` 9))

117 |   xorat m 2 ((i `at` 2) `xor` (i `at` 10))

118 |   xorat m 3 ((i `at` 3) `xor` (i `at` 11))

119 |   xorat m 4 ((i `at` 4) `xor` (i `at` 12))

120 |   xorat m 5 ((i `at` 5) `xor` (i `at` 13))

121 |   xorat m 6 ((i `at` 6) `xor` (i `at` 14))

122 |   xorat m 7 ((i `at` 7) `xor` (i `at` 15))

125 | 0 lte816 : LTE 8 16

126 | lte816 = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTEZero))))))))

128 | parameters (h     : MArray s 8 Bits64)

129 |            (chunk : ByteVect 128)

131 |   %inline

132 |   initV : F1 s (MArray s 16 Bits64)

133 |   initV = T1.do

134 |     v <- marray1 16 0

135 |     AC.copy  h  0 0 8 v {p1 = refl} {p2 = lte816}

136 |     AC.icopy IV 0 8 8 v {p1 = refl} {p2 = refl}

137 |     pure v

139 |   %inline

140 |   m : Fin 16 -> Bits64

141 |   m x = let BV b o _ := chunk in prim__getBits64 (unsafeGetBuffer b) (o64 x o)

143 |   round : MArray s 16 Bits64 -> IArray 16 (Fin 16) -> F1' s

144 |   round v sig = T1.do

145 |     mix v 0 4 8  12 (m (sig `at` 0)) (m (sig `at` 1))

146 |     mix v 1 5 9  13 (m (sig `at` 2)) (m (sig `at` 3))

147 |     mix v 2 6 10 14 (m (sig `at` 4)) (m (sig `at` 5))

148 |     mix v 3 7 11 15 (m (sig `at` 6)) (m (sig `at` 7))

150 |     mix v 0 5 10 15 (m (sig `at` 8))  (m (sig `at` 9))

151 |     mix v 1 6 11 12 (m (sig `at` 10)) (m (sig `at` 11))

152 |     mix v 2 7 8  13 (m (sig `at` 12)) (m (sig `at` 13))

153 |     mix v 3 4 9  14 (m (sig `at` 14)) (m (sig `at` 15))

155 |   compress : (t : Integer) -> (isLastBlock : Bool) -> F1' s

156 |   compress t isLastBlock = T1.do

157 |     v <- initV

158 |     xorat v 12 (cast t)

159 |     xorat v 13 (cast $ prim__shr_Integer t 64)

161 |     when1 isLastBlock $ T1.do

162 |       xorat v 14 0xffff_ffff_ffff_ffff

164 |     round v (sigma `at` 0)

165 |     round v (sigma `at` 1)

166 |     round v (sigma `at` 2)

167 |     round v (sigma `at` 3)

168 |     round v (sigma `at` 4)

169 |     round v (sigma `at` 5)

170 |     round v (sigma `at` 6)

171 |     round v (sigma `at` 7)

172 |     round v (sigma `at` 8)

173 |     round v (sigma `at` 9)

174 |     round v (sigma `at` 10)

175 |     round v (sigma `at` 11)

176 |     vv <- freeze v

177 |     mixIntoH vv h

183 | loop : {k : _} -> MArray s 8 Bits64 -> ByteVect k -> Integer -> F1' s

184 | loop h bv i t =

185 |   case tryLTE {n = k} 128 of

186 |     Just0 p =>

187 |      let (pre,pst) := splitAt 128 bv

188 |          i2        := i+128

189 |          _ # t     := compress h pre i2 False t

190 |       in loop h (assert_smaller bv pst) i2 t

191 |     Nothing0 => case tryLTE {n = 128} k of

192 |       Nothing0 => () # t -- impossible

193 |       Just0 p  =>

194 |        let BV ib o q := bv

195 |            mb # t    := mbuffer1 128 t

196 |            _  # t    := BC.icopy ib o 0 k mb {p1 = q} {p2 = p} t

197 |            bb # t    := BC.freeze mb t

198 |         in compress h (BV bb 0 refl) (i+cast k) True t

200 | littleEndian : Nat -> SnocList Char -> Bits64 -> SnocList Char

201 | littleEndian 0     ss m = ss

202 | littleEndian (S k) ss m =

203 |  let b := cast {to = Bits8} m

204 |      y := hexChar (shiftR b 4)

205 |      x := hexChar (b .&. 0xf)

206 |   in littleEndian k (ss:<y:<x) (shr m 8)

208 | initH : Nat -> F1 s (MArray s 8 Bits64)

209 | initH n = T1.do

210 |   h <- marray1 8 0

211 |   AC.icopy IV 0 0 8 h {p1 = refl} {p2 = refl}

212 |   xorat h 0 (0x01010000 + cast n * 8)

213 |   pure h

216 | blake2b : (out : Nat) -> (0 p : LTE out 8) => ByteString -> IArray out Bits64

217 | blake2b out (BS _ bv) =

218 |   run1 $ T1.do

219 |     h <- initH out

220 |     loop h bv 0

221 |     AC.freezeLTE h out

224 | encodeLE : {k : _} -> IArray k Bits64 -> String

225 | encodeLE = fastPack . (<>> []) . foldl (littleEndian 8) [<]

228 | hashStrings : List String -> String

229 | hashStrings = encodeLE . blake2b 2 . fromString . fastConcat