val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let trace = if DebugFlags.debug_KS then print else (fun _ -> ())
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))
/
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
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.DebugFlags.debug_KS MiTLS.Random.print Prims.bool Prims.string Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let trace =
  
if DebugFlags.debug_KS then print else (fun _ -> ())