val zero_element: a:Spec.alg -> m:m_spec -> element_t a m
let zero_element (a:Spec.alg) (m:m_spec) : element_t a m =
  match a,m with
  | Spec.Blake2S,M128 -> (vec_zero U32 4)
  | Spec.Blake2S,M256 -> (vec_zero U32 4)
  | Spec.Blake2B,M256 -> (vec_zero U64 4)
  | _ -> Spec.zero a
val zero_element: a:Spec.alg -> m:m_spec -> element_t a m
let zero_element (a: Spec.alg) (m: m_spec) : element_t a m =
match a, m with
| Spec.Blake2S, M128 -> (vec_zero U32 4)
| Spec.Blake2S, M256 -> (vec_zero U32 4)
| Spec.Blake2B, M256 -> (vec_zero U64 4)
| _ -> Spec.zero a
Hacl.Impl.Blake2.Core.fst.checked
Spec.Blake2.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.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.Seq.fst.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.fst
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec FStar.Pervasives.Native.Mktuple2 Lib.IntVector.vec_zero Lib.IntTypes.U32 Lib.IntTypes.U64 FStar.Pervasives.Native.tuple2 Spec.Blake2.zero Hacl.Impl.Blake2.Core.element_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"

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