val app_psk_table:MDM.t psk_region psk_identifier app_psk_entry psk_table_invariant
val app_psk_table:MDM.t psk_region psk_identifier app_psk_entry psk_table_invariant
let app_psk_table : MDM.t psk_region psk_identifier app_psk_entry psk_table_invariant =
  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
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

let pskInfo_hash pi = pi.early_hash
let pskInfo_ae pi = pi.early_ae

// We rule out all PSK that do not have at least one non-null byte
// thus avoiding possible confusion with non-PSK for all possible hash algs
type app_psk (i:psk_identifier) =
  b:bytes{exists i.{:pattern b.[i]} b.[i] <> 0z}

type app_psk_entry (i:psk_identifier) =
  (app_psk i) * pskInfo * bool

// Global invariant on the PSK idealization table
// No longer necessary now that FStar.Monotonic.DependentMap uses eqtype
//type app_psk_injective (m:MDM.map' psk_identifier app_psk_entry) =
//  forall i1 i2.{:pattern (MDM.sel m i1); (MDM.sel m i2)}
//      Seq.equal i1 i2 <==> (match MDM.sel m i1, MDM.sel m i2 with
//                  | Some (psk1, pski1, h1), Some (psk2, pski2, h2) -> Seq.equal psk1 psk2 /\ h1 == h2
//                  | _ -> True)
type psk_table_invariant (m:MDM.partial_dependent_map psk_identifier app_psk_entry) = True

/// Ideal table for application PSKs

noextract
/
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.psk_region
  MiTLS.TLSConstants.psk_identifier
  MiTLS.PSK.app_psk_entry
  MiTLS.PSK.psk_table_invariant
FStar.Monotonic.DependentMap.alloc MiTLS.TLSConstants.psk_identifier MiTLS.PSK.app_psk_entry MiTLS.PSK.psk_table_invariant MiTLS.PSK.psk_region FStar.Monotonic.DependentMap.t
let app_psk_table:MDM.t psk_region psk_identifier app_psk_entry psk_table_invariant =
  
MDM.alloc ()