val label_iv_l:List.Tot.llist U8.t 2
let label_iv_l: List.Tot.llist U8.t 2 =
  [@inline_let]
  let l = [ 0x69uy; 0x76uy ] in
  assert_norm (List.Tot.length l = 2);
  l
val label_iv_l:List.Tot.llist U8.t 2
let label_iv_l:List.Tot.llist U8.t 2 =
[@@ inline_let ]let l = [0x69uy; 0x76uy] in
assert_norm (List.Tot.length l = 2);
l
QUIC.Spec.Crypto.fst.checked
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
Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int FStar.List.Tot.Base.length FStar.UInt8.t Prims.list Prims.Cons FStar.UInt8.__uint_to_t Prims.Nil
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

noextract
let prefix: lbytes 11 =
  Seq.seq_of_list prefix_l

#push-options "--z3rlimit 10"
let lemma_hash_lengths (a:ha)
  : Lemma (HD.hash_length a <= 64 /\ HD.word_length a <= 8 /\
    HD.block_length a <= 128 /\
    (if Some? (HD.max_input_length a) then Some?.v (HD.max_input_length a) >= pow2 61 - 1 else True))
  =
  assert_norm(pow2 61 < pow2 125)
#pop-options

inline_for_extraction
noextract
let label_key_l: List.Tot.llist U8.t 3 =
  [@inline_let]
  let l = [ 0x6buy; 0x65uy; 0x79uy ] in
  assert_norm (List.Tot.length l = 3);
  l

let label_key =
  Seq.seq_of_list label_key_l

inline_for_extraction
noextract
val label_iv_l:List.Tot.llist U8.t 2
FStar.List.Tot.Properties.llist FStar.UInt8.t 2