let test_vec
  {a; entropy_input; entropy_input_reseed; nonce; personalization_string;
   additional_input_reseed; additional_input_1; additional_input_2;
   returned_bits}
=
  let returned_bytes_len       = String.strlen returned_bits / 2 in
  let entropy_input_len        = String.strlen entropy_input / 2 in
  let entropy_input_reseed_len = String.strlen entropy_input_reseed / 2 in
  let nonce_len                = String.strlen nonce / 2 in
  let personalization_string_len = String.strlen personalization_string / 2 in
  let additional_input_reseed_len = String.strlen additional_input_reseed / 2 in
  let additional_input_1_len   = String.strlen additional_input_1 / 2 in
  let additional_input_2_len   = String.strlen additional_input_2 / 2 in
  let returned_bits_len        = String.strlen returned_bits / 2 in
  if not (is_supported_alg a &&
          min_length a <= entropy_input_len &&
          entropy_input_len <= max_length &&
          min_length a / 2 <= nonce_len &&
          nonce_len <= max_length &&
          personalization_string_len <= max_personalization_string_length &&
          entropy_input_reseed_len <= max_length &&
          additional_input_reseed_len <= max_additional_input_length &&
          additional_input_1_len <= max_additional_input_length &&
          additional_input_2_len <= max_additional_input_length &&
          0 < returned_bits_len &&
          returned_bits_len <= max_output_length)
  then false
  else
    let _ = hmac_input_bound a in
    let st = instantiate #a
      (from_hex entropy_input) (from_hex nonce) (from_hex personalization_string)
    in
    let st = reseed st
      (from_hex entropy_input_reseed) (from_hex additional_input_reseed)
    in
    match generate st returned_bytes_len (from_hex additional_input_1) with
    | None -> false
    | Some (_, st) ->
      match generate st returned_bytes_len (from_hex additional_input_2) with
      | None -> false
      | Some (out, st) -> PS.print_compare true returned_bytes_len (from_hex returned_bits) out
let test_vec
      { a = a ;
          entropy_input = entropy_input ;
          entropy_input_reseed = entropy_input_reseed ;
          nonce = nonce ;
          personalization_string = personalization_string ;
          additional_input_reseed = additional_input_reseed ;
          additional_input_1 = additional_input_1 ;
          additional_input_2 = additional_input_2 ;
          returned_bits = returned_bits }
     =
let returned_bytes_len = String.strlen returned_bits / 2 in
let entropy_input_len = String.strlen entropy_input / 2 in
let entropy_input_reseed_len = String.strlen entropy_input_reseed / 2 in
let nonce_len = String.strlen nonce / 2 in
let personalization_string_len = String.strlen personalization_string / 2 in
let additional_input_reseed_len = String.strlen additional_input_reseed / 2 in
let additional_input_1_len = String.strlen additional_input_1 / 2 in
let additional_input_2_len = String.strlen additional_input_2 / 2 in
let returned_bits_len = String.strlen returned_bits / 2 in
if
  not (is_supported_alg a && min_length a <= entropy_input_len && entropy_input_len <= max_length &&
      min_length a / 2 <= nonce_len &&
      nonce_len <= max_length &&
      personalization_string_len <= max_personalization_string_length &&
      entropy_input_reseed_len <= max_length &&
      additional_input_reseed_len <= max_additional_input_length &&
      additional_input_1_len <= max_additional_input_length &&
      additional_input_2_len <= max_additional_input_length &&
      0 < returned_bits_len &&
      returned_bits_len <= max_output_length)
then false
else
  let _ = hmac_input_bound a in
  let st =
    instantiate #a (from_hex entropy_input) (from_hex nonce) (from_hex personalization_string)
  in
  let st = reseed st (from_hex entropy_input_reseed) (from_hex additional_input_reseed) in
  match generate st returned_bytes_len (from_hex additional_input_1) with
  | None -> false
  | Some (_, st) ->
    match generate st returned_bytes_len (from_hex additional_input_2) with
    | None -> false
    | Some (out, st) -> PS.print_compare true returned_bytes_len (from_hex returned_bits) out
Spec.HMAC_DRBG.Test.fst.checked
Spec.HMAC_DRBG.Test.Vectors.fst.checked Spec.HMAC_DRBG.fsti.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked Lib.PrintSequence.fsti.checked Lib.Meta.fst.checked Lib.IntTypes.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.IO.fst.checked
Spec.HMAC_DRBG.Test.fst
Spec.HMAC_DRBG.Test.Vectors.vec Spec.HMAC_DRBG.Test.Vectors.supported_alg Lib.Meta.hex_string Prims.op_Negation Prims.op_AmpAmp Spec.HMAC_DRBG.Test.Vectors.is_supported_alg Prims.op_LessThanOrEqual Spec.HMAC_DRBG.min_length Spec.HMAC_DRBG.max_length Prims.op_Division Spec.HMAC_DRBG.max_personalization_string_length Spec.HMAC_DRBG.max_additional_input_length Prims.op_LessThan Spec.HMAC_DRBG.max_output_length Prims.bool Spec.HMAC_DRBG.generate Lib.Meta.from_hex Spec.Agile.HMAC.lbytes Spec.HMAC_DRBG.state Lib.PrintSequence.print_compare Spec.HMAC_DRBG.reseed Spec.HMAC_DRBG.instantiate Prims.unit Spec.HMAC_DRBG.hmac_input_bound Prims.int FStar.String.strlen
module Spec.HMAC_DRBG.Test

open FStar.Seq
open Lib.IntTypes
open Lib.Meta

open Spec.Agile.HMAC
open Spec.HMAC_DRBG
open Spec.HMAC_DRBG.Test.Vectors

module PS = Lib.PrintSequence

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

let test_vec
  {a; entropy_input; entropy_input_reseed; nonce; personalization_string;
   additional_input_reseed; additional_input_1; additional_input_2;
val test_vec : _: Spec.HMAC_DRBG.Test.Vectors.vec -> FStar.All.ALL Prims.bool
_: Spec.HMAC_DRBG.Test.Vectors.vec -> FStar.All.ALL Prims.bool