val psk (i:esId) : Type0
val psk (i:esId) : Type0
let psk (i:esId) =
  b:bytes{len b = Hacl.Hash.Definitions.hash_len (esId_hash i)}
module MiTLS.Old.KeySchedule
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Seq
open FStar.Bytes
open FStar.Error
//open FStar.Integers 

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Extensions
open MiTLS.TLSInfo
open MiTLS.Range
open MiTLS.StatefulLHAE
open MiTLS.HKDF
open MiTLS.PSK

module MDM = FStar.Monotonic.DependentMap
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module H = MiTLS.Hashing.Spec

module HMAC_UFCMA = MiTLS.Old.HMAC.UFCMA

#set-options "--admit_smt_queries true"
/
prims.fst.checked MiTLS.TLSPRF.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.StreamAE.fst.checked MiTLS.StatefulLHAE.fst.checked MiTLS.StAE.fst.checked MiTLS.Range.fst.checked MiTLS.Random.fst.checked MiTLS.PSK.fst.checked MiTLS.PMS.fst.checked MiTLS.Old.HMAC.UFCMA.fsti.checked MiTLS.List.Helpers.fst.checked MiTLS.HKDF.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Extensions.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.CommonDH.fsti.checked MiTLS.AEADProvider.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.List.Tot.fst.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Old.KeySchedule.fst
i: MiTLS.TLSInfo.esId -> Type0
MiTLS.TLSInfo.esId FStar.Bytes.bytes Prims.b2t Prims.op_Equality FStar.UInt32.t FStar.Bytes.len Hacl.Hash.Definitions.hash_len MiTLS.TLSInfo.esId_hash
let psk (i: esId) =
  
b: bytes{len b = Hacl.Hash.Definitions.hash_len (esId_hash i)}