0 | module Crypto.Hash
 1 |
 2 | import Data.Bits
 3 | import Data.List
 4 | import Data.Nat
 5 | import Data.Vect
 6 | import public Crypto.Hash.Interfaces
 7 | import public Crypto.Hash.SHA2
 8 | import public Crypto.Hash.SHA1
 9 | import public Crypto.Hash.MD5
10 |
11 | ||| basically `Hash.initialize` but with explicit type argument
12 | public export
13 | init : (0 algo : Type) -> Hash algo => algo
14 | init algo = initialize
15 |
16 | ||| hash a sequence of bytes and produce a digest
17 | public export
18 | hash : (0 algo : Type) -> Hash algo => (message : List Bits8) -> Vect (digest_nbyte {algo}) Bits8
19 | hash algo xs = finalize $ update xs $ Hash.init algo
20 |
21 | ||| basically `MAC.initialize` but with explicit type argument
22 | public export
23 | init_mac : (0 algo : Type) -> MAC key algo => key -> algo
24 | init_mac algo key = initialize_mac key
25 |
26 | ||| hash a sequence of bytes with key and produce a digest
27 | public export
28 | mac : (0 algo : Type) -> MAC key algo => key -> (message : List Bits8) -> Vect (digest_nbyte {algo}) Bits8
29 | mac algo key xs = finalize $ update xs $ Hash.init_mac algo key
30 |