val 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))
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)
val 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))
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)
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
QUIC.Spec.Crypto.ha FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Prims.unit Prims.l_True Prims.squash Prims.l_and Prims.op_LessThanOrEqual Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.word_length Spec.Hash.Definitions.block_length FStar.Pervasives.Native.uu___is_Some Prims.pos Spec.Hash.Definitions.max_input_length Prims.op_GreaterThanOrEqual FStar.Pervasives.Native.__proj__Some__item__v Prims.op_Subtraction Prims.bool Prims.logical Prims.Nil FStar.Pervasives.pattern
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))
val 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))
a: QUIC.Spec.Crypto.ha
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Hash.Definitions.hash_length a <= 64 /\ Spec.Hash.Definitions.word_length a <= 8 /\
      Spec.Hash.Definitions.block_length a <= 128 /\
      (match Some? (Spec.Hash.Definitions.max_input_length a) with
        | true -> Some?.v (Spec.Hash.Definitions.max_input_length a) >= Prims.pow2 61 - 1
        | _ -> Prims.l_True))