let disjoint_st (#a:supported_alg) (st:state a) (b:buffer uint8) =
  B.loc_disjoint (footprint st) (B.loc_buffer b)
let disjoint_st (#a: supported_alg) (st: state a) (b: buffer uint8) =
B.loc_disjoint (footprint st) (B.loc_buffer b)
Hacl.HMAC_DRBG.fsti.checked
Spec.HMAC_DRBG.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.HMAC.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.HMAC_DRBG.fsti
Hacl.HMAC_DRBG.supported_alg Hacl.HMAC_DRBG.state Lib.Buffer.buffer Lib.IntTypes.uint8 LowStar.Monotonic.Buffer.loc_disjoint Hacl.HMAC_DRBG.footprint LowStar.Monotonic.Buffer.loc_buffer LowStar.Buffer.trivial_preorder
module Hacl.HMAC_DRBG

open 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

/// HMAC-DRBG
///
/// See 10.1.2 and B.2 of
/// https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-90Ar1.pdf
///
/// This module implements the hash-algorithm-agile algorithms
/// - HMAC_DRBG_Update (not exposed by the interface)
/// - HMAC_DRBG_Instantiate_algorithm
/// - HMAC_DRBG_Reseed_algorithm
/// - HMAC_DRBG_Generate_algorithm
///
/// This is not linked to an appropriate Get_entropy_input function,
/// so these algorithms should be combined to get entropy from Get_entropy_input
/// for instantiation, reseeding, and optional prediction resistance.
///
/// - Supports SHA-1, SHA2-256, SHA2-384 and SHA2-512 hash algorithms
///
/// - Supports reseeding
///
/// - Supports optional personalization_string for instantiation
///
/// - Supports optional additional_input for reseeding and generation
///
/// - The internal state is (Key,V,reseed_counter)
///
/// - The security_strength is the HMAC-strength of the hash algorithm as per p.54 of
///   https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-57pt1r4.pdf
///
/// - The minimum entropy for instantiation is 3/2 * security_strength.
///    - entropy_input must have at least security_strength bits.
///    - nonce must have at least 1/2 security_strength bits.
///    - entropy_input and nonce can have at most max_length = 2^16 bits.
///
/// - At most max_number_of_bits_per_request = 2^16 bits can be generated per request.
///
/// - The reseed_interval is 2^10

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

unfold
let supported_alg = S.supported_alg

let reseed_interval: n:size_t{v n == S.reseed_interval} =
  assert_norm (S.reseed_interval < pow2 32);
  normalize_term (mk_int S.reseed_interval)

let max_output_length: n:size_t{v n == S.max_output_length} =
  assert_norm (S.max_output_length < pow2 32);
  normalize_term (mk_int S.max_output_length)

let max_length: n:size_t{v n == S.max_length} =
  assert_norm (S.max_length < pow2 32);
  normalize_term (mk_int S.max_length)

let max_personalization_string_length: n:size_t{v n == S.max_personalization_string_length} =
  assert_norm (S.max_personalization_string_length < pow2 32);
  normalize_term (mk_int S.max_personalization_string_length)

let max_additional_input_length: n:size_t{v n == S.max_additional_input_length} =
  assert_norm (S.max_additional_input_length < pow2 32);
  normalize_term (mk_int S.max_additional_input_length)

[@@ Comment "Return the minimal entropy input length of the desired hash function.

@param a Hash algorithm to use."]
let min_length (a:supported_alg) : n:size_t{v n == S.min_length a} =
  assert_norm (S.min_length a < pow2 32);
  match a with
  | SHA1 -> normalize_term (mk_int (S.min_length SHA1))
  | SHA2_256 | SHA2_384 | SHA2_512 -> normalize_term (mk_int (S.min_length SHA2_256))

val state: supported_alg -> Type0

inline_for_extraction noextract
val freeable: #a:supported_alg -> st:state a -> Type0

val footprint: #a:supported_alg -> st:state a -> GTot B.loc

inline_for_extraction noextract
val invariant: #a:supported_alg -> st:state a -> h:HS.mem -> Type0

inline_for_extraction noextract
val disjoint_st : st: Hacl.HMAC_DRBG.state a -> b: Lib.Buffer.buffer Lib.IntTypes.uint8 -> Type0
st: Hacl.HMAC_DRBG.state a -> b: Lib.Buffer.buffer Lib.IntTypes.uint8 -> Type0