val ticket_enc:reference (option ticket_key)
val ticket_enc:reference (option ticket_key)
let ticket_enc : reference (option ticket_key) = ralloc region None
module MiTLS.Ticket
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
module Parse = MiTLS.Parse
open MiTLS.Parse
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module AE = MiTLS.AEADProvider

module PTL = MiTLS.Parsers.Ticket.Low // just to 1/ verify that module, and 2/ pollute the context with some Spec definitions (integers, vlbytes), and see what happens

#set-options "--admit_smt_queries true"

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

// verification-only
type hostname = string
type tlabel (h:hostname) = t:bytes * tls13:bool

noextract
private let region:rgn = new_region tls_tables_region

type ticket_key =
  | Key: i:AE.id -> wr:AE.writer i -> rd:AE.reader i -> ticket_key

private let dummy_id (a:aeadAlg) : St AE.id =
  assume false;
  let h = Hashing.Spec.SHA2_256 in
  let li = LogInfo_CH0 ({
    li_ch0_cr = Bytes.create 32ul 0z;
    li_ch0_ed_psk = empty_bytes;
    li_ch0_ed_ae = a;
    li_ch0_ed_hash = h;
  }) in
  let log : hashed_log li = empty_bytes in
  ID13 (KeyID #li (ExpandedSecret (EarlySecretID (NoPSK h)) ApplicationTrafficSecret log))

// The ticket encryption key is a module global, but it must be lazily initialized
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Random.fst.checked MiTLS.PMS.fst.checked MiTLS.Parsers.TicketContents13.fsti.checked MiTLS.Parsers.TicketContents12.fsti.checked MiTLS.Parsers.TicketContents.fsti.checked MiTLS.Parsers.Ticket.Low.fst.checked MiTLS.Parsers.Boolean.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.AEADProvider.fsti.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Ticket.fst
FStar.HyperStack.ST.reference (FStar.Pervasives.Native.option MiTLS.Ticket.ticket_key)
FStar.HyperStack.ST.ralloc FStar.Pervasives.Native.option MiTLS.Ticket.ticket_key FStar.Heap.trivial_preorder MiTLS.Ticket.region FStar.Pervasives.Native.None FStar.HyperStack.ST.mref
let ticket_enc:reference (option ticket_key) =
  
ralloc region None