val print : s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
let print s = discard (IO.debug_print_string ("TCK| "^s^"\n"))
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))
/
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
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
Prims.string MiTLS.Ticket.discard FStar.IO.debug_print_string Prims.op_Hat Prims.unit
let print s =
  
discard (IO.debug_print_string ("TCK| " ^ s ^ "\n"))