val prefix:lbytes 11
val prefix:lbytes 11
let prefix: lbytes 11 =
  Seq.seq_of_list prefix_l
module QUIC.Spec.Crypto

module U8 = FStar.UInt8
module Seq = QUIC.Secret.Seq
module HKDF = Spec.Agile.HKDF

inline_for_extraction
noextract
let prefix_l: List.Tot.llist U8.t 11 =
  // : "tls13 quic "
  [@inline_let]
  let l = [0x74uy; 0x6cuy; 0x73uy; 0x31uy; 0x33uy;
           0x20uy; 0x71uy; 0x75uy; 0x69uy; 0x63uy; 0x20uy] in
  assert_norm (List.Tot.length l == 11);
  l
/
Spec.Agile.HKDF.fsti.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
QUIC.Spec.Crypto.fst
QUIC.Spec.Base.lbytes 11
FStar.Seq.Base.seq_of_list FStar.UInt8.t QUIC.Spec.Crypto.prefix_l
let prefix:lbytes 11 =
  
Seq.seq_of_list prefix_l