let vector = D.hash_alg & vec8 & vec8 & vec8 & vec8 & vec8 & (vec8 & vec8) & vec8
let vector =
D.hash_alg & vec8 & vec8 & vec8 & vec8 & vec8 & (vec8 & vec8) & vec8
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.Pervasives.Native.tuple8 Spec.Hash.Definitions.hash_alg Hacl.Test.HMAC_DRBG.vec8 FStar.Pervasives.Native.tuple2
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 *)
noextract
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

%splice[vectors_low] (lowstarize_toplevel "vectors_tmp" "vectors_low")

// Cheap alternative to friend Lib.IntTypes needed because Test.Lowstarize uses UInt8.t
assume val declassify_uint8: squash (uint8 == UInt8.t)

let vec8 = L.lbuffer UInt8.t
val vector : Type0
Type0