
  0 | module Crypto.Hash.Interfaces
  1 | 
  2 | import Data.Vect
  3 | 
  4 | public export
  5 | interface Digest (0 algo : Type) where
  6 |   digest_nbyte : Nat
  7 |   update : List Bits8 -> algo -> algo
  8 |   finalize : algo -> Vect digest_nbyte Bits8
  9 | 
 10 | public export
 11 | interface Digest algo => Hash algo where
 12 |   block_nbyte : Nat
 13 |   initialize : algo
 14 | 
 15 | public export
 16 | interface Digest algo => MAC (0 key : Type) algo where
 17 |   initialize_mac : key -> algo
 18 |