val compare_and_print: b1:B.buffer UInt8.t -> b2:B.buffer UInt8.t -> len:UInt32.t 
  -> Stack bool
  (requires fun h0 -> B.live h0 b1 /\ B.live h0 b2 /\ B.length b1 == v len /\ B.length b2 == v len)
  (ensures  fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
let compare_and_print b1 b2 len =
  push_frame();
  LowStar.Printf.(printf "Expected: %xuy\n" len b1 done);
  LowStar.Printf.(printf "Computed: %xuy\n" len b2 done);
  let b = Lib.ByteBuffer.lbytes_eq #len b1 b2 in
  if b then 
    LowStar.Printf.(printf "PASS\n" done)
  else
    LowStar.Printf.(printf "FAIL\n" done);
  pop_frame();
  b
val compare_and_print: b1:B.buffer UInt8.t -> b2:B.buffer UInt8.t -> len:UInt32.t 
  -> Stack bool
  (requires fun h0 -> B.live h0 b1 /\ B.live h0 b2 /\ B.length b1 == v len /\ B.length b2 == v len)
  (ensures  fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
let compare_and_print b1 b2 len =
push_frame ();
(let open LowStar.Printf in printf "Expected: %xuy\n" len b1 done);
(let open LowStar.Printf in printf "Computed: %xuy\n" len b2 done);
let b = Lib.ByteBuffer.lbytes_eq #len b1 b2 in
if b
then let open LowStar.Printf in printf "PASS\n" done
else (let open LowStar.Printf in printf "FAIL\n" done);
pop_frame ();
b
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
LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Prims.bool Prims.unit FStar.HyperStack.ST.pop_frame LowStar.Printf.printf LowStar.Printf.done Lib.ByteBuffer.lbytes_eq LowStar.Buffer.trivial_preorder FStar.HyperStack.ST.push_frame
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

let vector = D.hash_alg & vec8 & vec8 & vec8 & vec8 & vec8 & (vec8 & vec8) & vec8

// This could replace TestLib.compare_and_print
val compare_and_print: b1:B.buffer UInt8.t -> b2:B.buffer UInt8.t -> len:UInt32.t 
  -> Stack bool
  (requires fun h0 -> B.live h0 b1 /\ B.live h0 b2 /\ B.length b1 == v len /\ B.length b2 == v len)
  (ensures  fun h0 _ h1 -> B.modifies B.loc_none h0 h1)
val compare_and_print: b1:B.buffer UInt8.t -> b2:B.buffer UInt8.t -> len:UInt32.t 
  -> Stack bool
  (requires fun h0 -> B.live h0 b1 /\ B.live h0 b2 /\ B.length b1 == v len /\ B.length b2 == v len)
  (ensures  fun h0 _ h1 -> B.modifies B.loc_none h0 h1)

    b1: LowStar.Buffer.buffer FStar.UInt8.t ->
    b2: LowStar.Buffer.buffer FStar.UInt8.t ->
    len: FStar.UInt32.t
  -> FStar.HyperStack.ST.Stack Prims.bool