val pskInfo_ae : pi: MiTLS.TLSConstants.pskInfo -> MiTLS.CipherSuite.aeadAlg
let pskInfo_ae pi = pi.early_ae
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
type session12 (tid:bytes) = protocolVersion * cipherSuite * ems:bool * ms:bytes
private let sessions12 : MDM.t tregion bytes session12 (fun _ -> True) =
  MDM.alloc ()

let s12_lookup (tid:bytes) = MDM.lookup sessions12 tid
let s12_extend (tid:bytes) (s:session12 tid) = MDM.extend sessions12 tid s

// *** PSK ***

// The constraints for PSK indexes are:
//  - must be public (as psk index appears in hsId, msId and derived keys)
//  - must support application-provided PSK as well as RMS-based PSK
//  - must support dynamic compromise; we want to prove KI of 1RT keys in PSK_DHE
//    even for leaked PSK (but not PSK-based auth obivously)
// Implementation style:
//  - pskid is the TLS PSK identifier, an internal index to the PSK table
//  - for tickets, the encrypted serialized state is the PSK identifier
//  - we store in the table the PSK context and compromise status

// The pskInfo type has been moved to TLSConstants as it appears in config
// for the new ticket callback API
/
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
pi: MiTLS.TLSConstants.pskInfo -> MiTLS.CipherSuite.aeadAlg
MiTLS.TLSConstants.pskInfo MiTLS.TLSConstants.__proj__MkpskInfo__item__early_ae MiTLS.CipherSuite.aeadAlg
let pskInfo_ae pi =
  
pi.early_ae