val label_key : (label_key: IB.ibuffer U8.t {
  IB.frameOf label_key == HS.root /\
  IB.length label_key == Seq.length Spec.label_key /\
  IB.recallable label_key /\
  IB.witnessed label_key (IB.cpred Spec.label_key)
})
let label_key = LowStar.ImmutableBuffer.igcmalloc_of_list HS.root label_key_l
val label_key : (label_key: IB.ibuffer U8.t {
  IB.frameOf label_key == HS.root /\
  IB.length label_key == Seq.length Spec.label_key /\
  IB.recallable label_key /\
  IB.witnessed label_key (IB.cpred Spec.label_key)
})
let label_key =
LowStar.ImmutableBuffer.igcmalloc_of_list HS.root label_key_l
QUIC.Impl.Crypto.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fsti.checked QUIC.Spec.Crypto.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked EverCrypt.HKDF.fsti.checked EverCrypt.CTR.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.Impl.Crypto.fst
LowStar.ImmutableBuffer.igcmalloc_of_list FStar.UInt8.t FStar.Monotonic.HyperHeap.root QUIC.Spec.Crypto.label_key_l LowStar.ImmutableBuffer.libuffer FStar.Pervasives.normalize_term Prims.nat FStar.List.Tot.Base.length FStar.Seq.Properties.seq_of_list Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.ImmutableBuffer.immutable_preorder LowStar.Monotonic.Buffer.recallable
module QUIC.Impl.Crypto

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF
module CTR = EverCrypt.CTR
module IB = LowStar.ImmutableBuffer
module U32 = FStar.UInt32

module Seq = QUIC.Secret.Seq
module SecretBuffer = QUIC.Secret.Buffer

module SHKDF = Spec.Agile.HKDF
module SHD = Spec.Hash.Definitions

friend QUIC.Spec.Crypto (* for the _l list constants *)
module Spec = QUIC.Spec.Crypto

open LowStar.BufferOps (* for the !* notation *)


/// Helpers & globals
/// -----------------

open QUIC.Impl.Lemmas

inline_for_extraction noextract
let u32_of_u8 = FStar.Int.Cast.uint8_to_uint32
inline_for_extraction noextract
let u64_of_u8 = FStar.Int.Cast.uint8_to_uint64
inline_for_extraction noextract
let u64_of_u32 = FStar.Int.Cast.uint32_to_uint64
val label_key : (label_key: IB.ibuffer U8.t {
  IB.frameOf label_key == HS.root /\
  IB.length label_key == Seq.length Spec.label_key /\
  IB.recallable label_key /\
  IB.witnessed label_key (IB.cpred Spec.label_key)
})
label_key:
LowStar.ImmutableBuffer.ibuffer FStar.UInt8.t
  { LowStar.Monotonic.Buffer.frameOf label_key == FStar.Monotonic.HyperHeap.root /\
    LowStar.Monotonic.Buffer.length label_key == FStar.Seq.Base.length QUIC.Spec.Crypto.label_key /\
    LowStar.Monotonic.Buffer.recallable label_key /\
    LowStar.Monotonic.Buffer.witnessed label_key
      (LowStar.ImmutableBuffer.cpred QUIC.Spec.Crypto.label_key) }