val init (a:hash_alg): init_t a
let init a =
  match a with
  | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
      Spec.SHA2.init a
  | MD5 ->
      Spec.MD5.init
  | SHA1 ->
      Spec.SHA1.init
  | Blake2S -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2S 0 32
  | Blake2B -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2B 0 64
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 ->
      Lib.Sequence.create 25 (u64 0)
val init (a:hash_alg): init_t a
let init a =
match a with
| SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 -> Spec.SHA2.init a
| MD5 -> Spec.MD5.init
| SHA1 -> Spec.SHA1.init
| Blake2S -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2S 0 32
| Blake2B -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2B 0 64
| SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 -> Lib.Sequence.create 25 (u64 0)
Spec.Agile.Hash.fst.checked
Spec.SHA3.fst.checked Spec.SHA2.fsti.checked Spec.SHA1.fsti.checked Spec.MD5.fsti.checked Spec.Hash.MD.fst.checked Spec.Hash.Definitions.fst.checked Spec.Blake2.fst.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.Hash.fst
Spec.Hash.Definitions.hash_alg Spec.SHA2.init Spec.MD5.init Spec.SHA1.init Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2S Spec.Blake2.Blake2B Lib.Sequence.create Spec.Hash.Definitions.word Lib.IntTypes.u64 Spec.Hash.Definitions.init_t
module Spec.Agile.Hash

module S = FStar.Seq

open Spec.Hash.Definitions
open Spec.Hash.MD
open FStar.Mul
open Lib.IntTypes

unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x
val init (a:hash_alg): init_t a
a: Spec.Hash.Definitions.hash_alg -> Spec.Hash.Definitions.init_t a