let hash_len (a:supported_alg) = Hacl.Hash.Definitions.hash_len a
let hash_len (a: supported_alg) =
Hacl.Hash.Definitions.hash_len a
Hacl.HMAC_DRBG.fst.checked
Spec.HMAC_DRBG.fst.checked Spec.HMAC_DRBG.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.HMAC_DRBG.fst
Hacl.HMAC_DRBG.supported_alg Hacl.Hash.Definitions.hash_len Lib.IntTypes.size_t Prims.b2t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U32 Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.PUB Spec.Hash.Definitions.hash_length
module Hacl.HMAC_DRBG

open FStar.HyperStack.ST
module ST = FStar.HyperStack.ST

open Spec.Hash.Definitions

open Lib.IntTypes
open Lib.Buffer

module HS = FStar.HyperStack
module B = LowStar.Buffer
module LSeq = Lib.Sequence

module HMAC = Hacl.HMAC
module S = Spec.HMAC_DRBG

friend Spec.HMAC_DRBG
val hash_len : a: Hacl.HMAC_DRBG.supported_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}
a: Hacl.HMAC_DRBG.supported_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}