val sessions12:MDM.t tregion bytes session12 (fun _ -> True)
val sessions12:MDM.t tregion bytes session12 (fun _ -> True)
let sessions12 : MDM.t tregion bytes session12 (fun _ -> True) =
  MDM.alloc ()
module MiTLS.PSK
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants

module DM = FStar.DependentMap
module MDM = FStar.Monotonic.DependentMap
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

// Has been moved to TLSConstants as it appears in config for ticket callbacks
type pskInfo = TLSConstants.pskInfo

// SESSION TICKET DATABASE (TLS 1.3)
// Note that the associated PSK are stored in the PSK table defined below in this file
let hostname : eqtype = string

let tlabel (h:hostname) = bytes

noextract
private let tregion:rgn = new_region tls_tables_region
private let tickets : MDM.t tregion hostname tlabel (fun _ -> True) =
  MDM.alloc ()

let lookup (h:hostname) = MDM.lookup tickets h
let extend (h:hostname) (t:tlabel h) = MDM.extend tickets h t

// SESSION TICKET DATABASE (TLS 1.2)
// Note that this table also stores the master secret
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.PSK.fst
FStar.Monotonic.DependentMap.t MiTLS.PSK.tregion
  FStar.Bytes.bytes
  MiTLS.PSK.session12
  (fun _ -> Prims.l_True)
FStar.Monotonic.DependentMap.alloc FStar.Bytes.bytes MiTLS.PSK.session12 FStar.DependentMap.t FStar.Monotonic.DependentMap.opt Prims.l_True MiTLS.PSK.tregion FStar.Monotonic.DependentMap.t
let sessions12:MDM.t tregion bytes session12 (fun _ -> True) =
  
MDM.alloc ()