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

/// QUIC-specific interface on top of our main TLS API
/// * establishes session & exported keys: no application-data traffic!
/// * simplified configuration, with reasonable defaults
/// * TCP-like send/recv callbacks operate on caller-provided buffers
///   recv may yield (not enough input)
///   send is guaranteed to succeed (large enough output buffer expected)
///
/// See https://tools.ietf.org/html/draft-ietf-quic-tls-04
///
/// Relying on FFI for accessing configs, callbacks, etc.
/// Testing both in OCaml (TCP-based, TestQUIC ~ TestFFI) and in C.

open FStar.Bytes
open FStar.Error
open FStar.HyperStack.All

open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.DataStream
open MiTLS.TLS
open MiTLS.FFICallbacks

module HS = FStar.HyperStack
module FFI = MiTLS.FFI
module Range = MiTLS.Range
open MiTLS.Range
module Parse = MiTLS.Parse

#set-options "--admit_smt_queries true"

(* A flag for runtime debugging of ffi data.
   The F* normalizer will erase debug prints at extraction
   when this flag is 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 ("QIC| "^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.TLS.fst.checked MiTLS.Ticket.fst.checked MiTLS.StreamAE.fst.checked MiTLS.Record.fsti.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.Old.KeySchedule.fsti.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Old.Epochs.fsti.checked MiTLS.Negotiation.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.fsti.checked MiTLS.FFICallbacks.fst.checked MiTLS.FFI.fst.checked MiTLS.Extensions.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked MiTLS.AEADProvider.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.IO.fst.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.QUIC.fst
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.DebugFlags.debug_QUIC MiTLS.QUIC.print Prims.bool Prims.string Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let trace =
  
if DebugFlags.debug_QUIC then print else (fun _ -> ())