let vectors_tmp = List.Tot.map 
  (fun x -> x.a, h x.entropy_input, h x.nonce, h x.personalization_string, 
         h x.entropy_input_reseed, h x.additional_input_reseed,
         (h x.additional_input_1, h x.additional_input_2),
         h x.returned_bits)
  test_vectors
let vectors_tmp =
List.Tot.map (fun x ->
      x.a,
      h x.entropy_input,
      h x.nonce,
      h x.personalization_string,
      h x.entropy_input_reseed,
      h x.additional_input_reseed,
      (h x.additional_input_1, h x.additional_input_2),
      h x.returned_bits)
  test_vectors
Hacl.Test.HMAC_DRBG.fst.checked
Test.Lowstarize.fst.checked Spec.HMAC_DRBG.Test.Vectors.fst.checked Spec.HMAC_DRBG.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.Printf.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.HMAC_DRBG.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked C.String.fsti.checked C.Loops.fst.checked C.fst.checked
Hacl.Test.HMAC_DRBG.fst
FStar.List.Tot.Base.map Spec.HMAC_DRBG.Test.Vectors.vec FStar.Pervasives.Native.tuple8 Spec.HMAC_DRBG.Test.Vectors.supported_alg Test.Lowstarize.hex_encoded FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple8 Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__a Test.Lowstarize.h Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__entropy_input Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__nonce Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__personalization_string Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__entropy_input_reseed Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__additional_input_reseed FStar.Pervasives.Native.Mktuple2 Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__additional_input_1 Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__additional_input_2 Spec.HMAC_DRBG.Test.Vectors.__proj__Mkvec__item__returned_bits Spec.HMAC_DRBG.Test.Vectors.test_vectors
module Hacl.Test.HMAC_DRBG

open FStar.HyperStack.ST
open Test.Lowstarize

open Lib.IntTypes

open Hacl.HMAC_DRBG
open Spec.HMAC_DRBG.Test.Vectors

module D = Spec.Hash.Definitions
module L = Test.Lowstarize
module B = LowStar.Buffer

#set-options "--fuel 0 --ifuel 0 --z3rlimit 100"

(* FStar.Reflection only supports up to 8-tuples *)
val vectors_tmp : Prims.list (((((((Spec.HMAC_DRBG.Test.Vectors.supported_alg * Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    (Test.Lowstarize.hex_encoded * Test.Lowstarize.hex_encoded)) *
    Test.Lowstarize.hex_encoded)
Prims.list (((((((Spec.HMAC_DRBG.Test.Vectors.supported_alg * Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    Test.Lowstarize.hex_encoded) *
    (Test.Lowstarize.hex_encoded * Test.Lowstarize.hex_encoded)) *
    Test.Lowstarize.hex_encoded)