0 | module Data.Cryptography.Hash.SHA
 1 |
 2 | import Data.Bits
 3 | import Data.Buffer
 4 | import Data.Vect
 5 |
 6 | import Data.Cryptography.Hash
 7 |
 8 | %foreign "C:hs_cryptohash_sha1_init,libsha-idris"
 9 | prim__sha1_init: Buffer -> PrimIO Unit
10 |
11 | %foreign "C:hs_cryptohash_sha1_update,libsha-idris"
12 | prim__sha1_update: Buffer -> Buffer -> Int -> PrimIO Unit
13 |
14 | %foreign "C:hs_cryptohash_sha1_finalize,libsha-idris"
15 | prim__sha1_finalize: Buffer -> Buffer -> PrimIO Bits64
16 |
17 | %foreign "C:hs_cryptohash_sha256_init,libsha-idris"
18 | prim__sha256_init: Buffer -> PrimIO Unit
19 |
20 | %foreign "C:hs_cryptohash_sha256_update,libsha-idris"
21 | prim__sha256_update: Buffer -> Buffer -> Int -> PrimIO Unit
22 |
23 | %foreign "C:hs_cryptohash_sha256_finalize,libsha-idris"
24 | prim__sha256_finalize: Buffer -> Buffer -> PrimIO Bits64
25 |
26 | setBytes : Buffer -> Int -> List Bits8 -> IO Unit
27 | setBytes buf offset [] = pure ()
28 | setBytes buf offset (x :: xs) = do
29 |   Buffer.setBits8 buf offset x
30 |   setBytes buf (offset + 1) xs
31 |
32 | mkMaker: {sz: Nat} -> (Buffer -> PrimIO Unit) -> Vect sz Bits8
33 | mkMaker initter = assert_total $ unsafePerformIO $ do
34 |   Just bufCtx <- newBuffer . the (Nat -> Int) cast $ sz
35 |   | Nothing => idris_crash "Buffer alloc failed"
36 |   primIO $ initter bufCtx
37 |   bits8 <- bufferData' bufCtx
38 |   Just vec <- pure $ toVect sz bits8
39 |   | Nothing => idris_crash "Unexpected buf length"
40 |   pure vec
41 |
42 | mkAppender :  {sz: Nat}
43 |            -> (Buffer -> Buffer -> Int -> PrimIO Unit)
44 |            -> List Bits8
45 |            -> Vect sz Bits8
46 |            -> Vect sz Bits8
47 | mkAppender updater listBits8 ctx = assert_total $ unsafePerformIO $ do
48 |   Just toHash <- newBuffer (the (Nat -> Int) cast $ List.length listBits8)
49 |   | Nothing => idris_crash "Buffer alloc failed"
50 |   setBytes toHash 0 listBits8
51 |   Just bufCtx <- newBuffer . the (Nat -> Int) cast $ sz
52 |   | Nothing => idris_crash "Buffer alloc failed"
53 |   setBytes bufCtx 0 (toList ctx)
54 |   primIO $ updater bufCtx toHash (the (Nat -> Int) cast $ List.length listBits8)
55 |   bits8 <- bufferData' bufCtx
56 |   Just vec <- pure $ toVect sz bits8
57 |   | Nothing => idris_crash "Unexpected buf length"
58 |   the (IO (Vect sz Bits8)) (pure vec)
59 |
60 | mkFinalizer:  {sz, outputSize: Nat}
61 |            -> (Buffer -> Buffer -> PrimIO Bits64)
62 |            -> Vect sz Bits8
63 |            -> Vect outputSize Bits8
64 | mkFinalizer finalizer ctx = assert_total $ unsafePerformIO $ do
65 |   Just bufCtx <- newBuffer 104
66 |   | Nothing => idris_crash "Buffer alloc failed"
67 |   setBytes bufCtx 0 (toList ctx)
68 |   Just out <- newBuffer . the (Nat -> Int) cast $ outputSize
69 |   | Nothing => idris_crash "Buffer alloc failed"
70 |   totalBytes <- primIO $ finalizer bufCtx out
71 |   bits8List <- bufferData' out
72 |   Just bits8Vec <- pure $ toVect outputSize bits8List
73 |   | Nothing => idris_crash "Unexpected buf length"
74 |   pure bits8Vec
75 |
76 | ||| Note that as of 2020, chosen-prefix attacks against SHA-1 are practical.
77 | public export
78 | sha1: HashAlgorithm
79 | sha1 = MkHashAlgorithm
80 |   { outputSize = 20
81 |   , ctxType = Vect 92 Bits8
82 |   , mkHashCtx = mkMaker {sz=92} prim__sha1_init
83 |   , appendHash = mkAppender {sz=92} prim__sha1_update
84 |   , finalizeHash = mkFinalizer {sz=92, outputSize=20} prim__sha1_finalize
85 |   }
86 |
87 | ||| SHA-256 belongs to the SHA-2 family of algorithms.
88 | public export
89 | sha256: HashAlgorithm
90 | sha256 = MkHashAlgorithm
91 |   { outputSize = 32
92 |   , ctxType = Vect 104 Bits8
93 |   , mkHashCtx = mkMaker {sz=104} prim__sha256_init
94 |   , appendHash = mkAppender {sz=104} prim__sha256_update
95 |   , finalizeHash = mkFinalizer {sz=104, outputSize=32} prim__sha256_finalize
96 |   }
97 |