val sample (len: nat{len < pow2 32})
    : ST (lbytes len) (requires fun h0 -> True) (ensures fun h0 _ h1 -> modifies_none h0 h1)
val sample (len: nat{len < pow2 32})
    : ST (lbytes len) (requires fun h0 -> True) (ensures fun h0 _ h1 -> modifies_none h0 h1)
let sample (len:nat{len < pow2 32}) : ST (lbytes len)
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  sample32 (UInt32.uint_to_t len)
module MiTLS.Random
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError

val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("RNG| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_KS then print else (fun _ -> ())

(*
RNG is provided by EverCrypt and must be seeded before use
This is done by FF_mitls_init and automatically in Evercrypt
when possible
*)

let init () : ST UInt32.t
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
//  let h0 = get() in
//  assume(EverCrypt.Specs.random_init_pre h0);
  assume false;
  EverCrypt.AutoConfig2.(init ());
  EverCrypt.random_init ()

let cleanup () : ST unit
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  assume false; // Precondition of random_cleanup in EverCrypt
  EverCrypt.random_cleanup ()

let sample32 (len:UInt32.t) : ST (lbytes (UInt32.v len))
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  if len = 0ul then Bytes.empty_bytes else (
  push_frame ();
  let b = LowStar.Buffer.alloca 0uy len in
  assume false; // Precondition of random_sample in EverCrypt
  EverCrypt.random_sample len b;
  let r = Bytes.of_buffer len b in
  trace ("Sampled: "^(hex_of_bytes r));
  pop_frame ();
  r)
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked EverCrypt.AutoConfig2.fsti.checked
MiTLS.Random.fst
len: Prims.nat{len < Prims.pow2 32} -> FStar.HyperStack.ST.ST (FStar.Bytes.lbytes len)
Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 MiTLS.Random.sample32 FStar.UInt32.uint_to_t FStar.Bytes.lbytes FStar.UInt32.v FStar.Monotonic.HyperStack.mem Prims.l_True FStar.HyperStack.ST.modifies_none
let sample (len: nat{len < pow2 32})
    : ST (lbytes len) (requires fun h0 -> True) (ensures fun h0 _ h1 -> modifies_none h0 h1) =
  
sample32 (UInt32.uint_to_t len)