val ffiConfig : host: FStar.Bytes.bytes -> MiTLS.TLSConstants.config
let ffiConfig (host:bytes) =
  let h = if length host = 0 then None else Some host in
  { defaultConfig with
    min_version = TLS_1p3;
    max_version = TLS_1p3;
    is_quic = true;
    peer_name = h;
    non_blocking_read = true;
    send_ticket = None;
  }
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))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_QUIC then print else (fun _ -> ())


// an integer carrying the fatal alert descriptor
// we could also write txt into the application error log
type error = UInt16.t
private let errno description txt: ST error
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> h0 == h1)
=
  let open MiTLS.TLSError in 
  trace ("returning error"^
    (match description with
    | Some ad -> " "^string_of_alert ad
    | None    -> "")^": "^txt);
  let a = match description with | Some a -> a | None -> fatalAlert Internal_error in
  Parse.uint16_of_bytes (Alert.alertBytes a)

module Handshake = MiTLS.Old.Handshake

let quic_check config =
  if config.min_version <> TLS_1p3 then trace "WARNING: not TLS 1.3";
  if not config.non_blocking_read then trace "WARNING: reads are blocking";
  if None? config.alpn            then trace "WARNING: missing ALPN";
  if not config.is_quic           then trace "WARNING: missing QUIC config, using TLS key labels"
/
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
host: FStar.Bytes.bytes -> MiTLS.TLSConstants.config
FStar.Bytes.bytes MiTLS.TLSConstants.Mkconfig MiTLS.Parsers.ProtocolVersion.TLS_1p3 MiTLS.TLSConstants.__proj__Mkconfig__item__cipher_suites MiTLS.TLSInfo.defaultConfig MiTLS.TLSConstants.__proj__Mkconfig__item__named_groups MiTLS.TLSConstants.__proj__Mkconfig__item__signature_algorithms MiTLS.TLSConstants.__proj__Mkconfig__item__hello_retry MiTLS.TLSConstants.__proj__Mkconfig__item__offer_shares MiTLS.TLSConstants.__proj__Mkconfig__item__custom_extensions MiTLS.TLSConstants.__proj__Mkconfig__item__use_tickets FStar.Pervasives.Native.None MiTLS.TLSConstants.__proj__Mkconfig__item__check_client_version_in_pms_for_old_tls MiTLS.TLSConstants.__proj__Mkconfig__item__request_client_certificate MiTLS.TLSConstants.__proj__Mkconfig__item__max_early_data MiTLS.TLSConstants.__proj__Mkconfig__item__max_ticket_age MiTLS.TLSConstants.__proj__Mkconfig__item__safe_renegotiation MiTLS.TLSConstants.__proj__Mkconfig__item__extended_master_secret MiTLS.TLSConstants.__proj__Mkconfig__item__enable_tickets MiTLS.TLSConstants.__proj__Mkconfig__item__ticket_callback MiTLS.TLSConstants.__proj__Mkconfig__item__nego_callback MiTLS.TLSConstants.__proj__Mkconfig__item__cert_callbacks MiTLS.TLSConstants.__proj__Mkconfig__item__alpn FStar.Pervasives.Native.option Prims.op_Equality Prims.int FStar.Bytes.length Prims.bool FStar.Pervasives.Native.Some MiTLS.TLSConstants.config
let ffiConfig (host: bytes) =
  
let h = if length host = 0 then None else Some host in
{
  defaultConfig with
  min_version = TLS_1p3;
  max_version = TLS_1p3;
  is_quic = true;
  peer_name = h;
  non_blocking_read = true;
  send_ticket = None
}