let valid_m_spec (a : Spec.alg) = m:m_spec{is_valid_blake2_config a m}
let valid_m_spec (a: Spec.alg) =
m: m_spec{is_valid_blake2_config a m}
Hacl.Impl.Blake2.Generic.fst.checked
Spec.Blake2.fst.checked prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Impl.Blake2.Constants.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.Blake2.Generic.fst
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec Prims.b2t Hacl.Impl.Blake2.Generic.is_valid_blake2_config
module Hacl.Impl.Blake2.Generic

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.LoopCombinators

module ST = FStar.HyperStack.ST
module Seq = Lib.Sequence
module Loops = Lib.LoopCombinators
module Spec = Spec.Blake2

open Hacl.Impl.Blake2.Constants
open Hacl.Impl.Blake2.Core

#set-options "--z3rlimit 50 --max_ifuel 0 --max_fuel 0"

noextract
let is_valid_blake2_config (a : Spec.alg) (m : m_spec) =
  match a, m with
  | Spec.Blake2S, M32 | Spec.Blake2S, M128
  | Spec.Blake2B, M32 | Spec.Blake2B, M256 -> true
  | _ -> false
val valid_m_spec : a: Spec.Blake2.alg -> Type0
a: Spec.Blake2.alg -> Type0