val rekey_secrets (#li:_) (i:expandId li) : Type0
val rekey_secrets (#li:_) (i:expandId li) : Type0
let rekey_secrets #li (i:expandId li) =
  H.tag (expandId_hash i) * H.tag (expandId_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"

let psk (i:esId) =
  b:bytes{len b = Hacl.Hash.Definitions.hash_len (esId_hash i)}

let es (i:esId) = H.tag (esId_hash i)

let hs (i:hsId) = H.tag (hsId_hash i)

let ams (i:asId) = H.tag (asId_hash i)
/
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.expandId li -> Type0
MiTLS.TLSInfo.logInfo MiTLS.TLSInfo.expandId FStar.Pervasives.Native.tuple2 MiTLS.Hashing.Spec.tag MiTLS.TLSInfo.expandId_hash
let rekey_secrets #li (i: expandId li) =
  
H.tag (expandId_hash i) * H.tag (expandId_hash i)