let element_t (a:Spec.alg) (m:m_spec) =
  match a,m with
  | Spec.Blake2S,M128 -> (vec_t U32 4)
  | Spec.Blake2S,M256 -> (vec_t U32 4)
  | Spec.Blake2B,M256 -> (vec_t U64 4)
  | _ -> (word_t a)
let element_t (a: Spec.alg) (m: m_spec) =
match a, m with
| Spec.Blake2S, M128 -> (vec_t U32 4)
| Spec.Blake2S, M256 -> (vec_t U32 4)
| Spec.Blake2B, M256 -> (vec_t U64 4)
| _ -> (word_t a)
Hacl.Impl.Blake2.Core.fsti.checked
Spec.Blake2.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Blake2.Core.fsti
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec FStar.Pervasives.Native.Mktuple2 Lib.IntVector.vec_t Lib.IntTypes.U32 Lib.IntTypes.U64 FStar.Pervasives.Native.tuple2 Hacl.Impl.Blake2.Core.word_t
module Hacl.Impl.Blake2.Core
module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.IntVector

module Spec = Spec.Blake2

#set-options "--max_fuel 0 --max_ifuel 1"

type m_spec =
  | M32
  | M128
  | M256

noextract inline_for_extraction
type word_t (a:Spec.alg) = Spec.word_t a

noextract inline_for_extraction
val element_t : a: Spec.Blake2.alg -> m: Hacl.Impl.Blake2.Core.m_spec -> Type0
a: Spec.Blake2.alg -> m: Hacl.Impl.Blake2.Core.m_spec -> Type0