val derive_secret:
  a: ha ->
  prk:HD.bytes_hash a ->
  label: bytes ->
  len: nat ->
  Pure (Seq.seq Secret.uint8)
  (requires len <= 255 /\
    Seq.length label <= 244 /\
    keysized a (Seq.length prk)
    )
  (ensures fun out ->
    Seq.length out == len
  )
val derive_secret:
  a: ha ->
  prk:HD.bytes_hash a ->
  label: bytes ->
  len: nat ->
  Pure (Seq.seq Secret.uint8)
  (requires len <= 255 /\
    Seq.length label <= 244 /\
    keysized a (Seq.length prk)
    )
  (ensures fun out ->
    Seq.length out == len
  )
let derive_secret a prk label len =
  let open Seq in
  let z = Seq.create 1 0uy in
  let lb = Seq.create 1 (U8.uint_to_t len) in // len <= 255
  let llen = Seq.create 1 (U8.uint_to_t (11 + Seq.length label)) in
  let info = z @| lb @| llen @| prefix @| label @| z in
  lemma_hash_lengths a;
  assert_norm(452 < pow2 61);
  HKDF.expand a prk (Seq.seq_hide info) len
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
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

let label_iv =
  Seq.seq_of_list label_iv_l

inline_for_extraction
noextract
let label_hp_l: List.Tot.llist U8.t 2 =
  [@inline_let]
  let l = [ 0x68uy; 0x70uy ] in
  assert_norm (List.Tot.length l = 2);
  l

let label_hp =
  Seq.seq_of_list label_hp_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

    a: QUIC.Spec.Crypto.ha ->
    prk: Spec.Hash.Definitions.bytes_hash a ->
    label: QUIC.Spec.Base.bytes ->
    len: Prims.nat
  -> Prims.Pure (FStar.Seq.Base.seq Lib.IntTypes.uint8)
QUIC.Spec.Crypto.ha Spec.Hash.Definitions.bytes_hash QUIC.Spec.Base.bytes Prims.nat Spec.Agile.HKDF.expand QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 QUIC.Spec.Crypto.lemma_hash_lengths FStar.Seq.Base.seq QUIC.Spec.Base.byte FStar.Seq.Base.op_At_Bar QUIC.Spec.Crypto.prefix FStar.Seq.Base.create FStar.UInt8.uint_to_t Prims.op_Addition FStar.Seq.Base.length FStar.UInt8.__uint_to_t Lib.IntTypes.uint8
let derive_secret a prk label len =
  
let open Seq in
let z = Seq.create 1 0uy in
let lb = Seq.create 1 (U8.uint_to_t len) in
let llen = Seq.create 1 (U8.uint_to_t (11 + Seq.length label)) in
let info = z @| lb @| llen @| prefix @| label @| z in
lemma_hash_lengths a;
assert_norm (452 < pow2 61);
HKDF.expand a prk (Seq.seq_hide info) len