let test () =
  let result = List.for_all test_vec test_vectors in
  if result then
    begin
    IO.print_string "\n\n[HMAC-DRBG] PASS\n";
    true
    end
  else
    begin
    IO.print_string "\n\n[HMAC-DRBG] FAIL\n";
    false
    end
let test () =
let result = List.for_all test_vec test_vectors in
if result
then
  (IO.print_string "\n\n[HMAC-DRBG] PASS\n";
    true)
else
  (IO.print_string "\n\n[HMAC-DRBG] FAIL\n";
    false)
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
Prims.unit Prims.bool FStar.IO.print_string FStar.List.for_all Spec.HMAC_DRBG.Test.Vectors.vec Spec.HMAC_DRBG.Test.test_vec Spec.HMAC_DRBG.Test.Vectors.test_vectors
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;
   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
val test : _: Prims.unit -> FStar.All.ALL Prims.bool
_: Prims.unit -> FStar.All.ALL Prims.bool