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_NGO then print else (fun _ -> ())
module MiTLS.Negotiation
open MiTLS

open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.HandshakeMessages

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

//16-05-31 these opens are implementation-only; overall we should open less
open MiTLS.Extensions

(**
  Debugging flag.
  F* normalizer will erase debug prints at extraction when set to false.
*)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("NGO| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.Random.fst.checked MiTLS.PSK.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Mem.fst.checked MiTLS.List.Helpers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.fsti.checked MiTLS.Extensions.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Negotiation.fst
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.DebugFlags.debug_NGO MiTLS.Negotiation.print Prims.bool Prims.string Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let trace =
  
if DebugFlags.debug_NGO then print else (fun _ -> ())