val hash_is_keysized_ (a: QS.ha): Lemma
  (ensures (QS.keysized a (Spec.Hash.Definitions.hash_length a)))
let hash_is_keysized_
  a
=
  assert_norm (512 < pow2 61);
  assert_norm (512 < pow2 125)
val hash_is_keysized_ (a: QS.ha): Lemma
  (ensures (QS.keysized a (Spec.Hash.Definitions.hash_length a)))
let hash_is_keysized_ a =
assert_norm (512 < pow2 61);
assert_norm (512 < pow2 125)
QUIC.Impl.Lemmas.fst.checked
Spec.Loops.fst.checked QUIC.Spec.Lemmas.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked EverCrypt.CTR.fsti.checked C.Loops.fst.checked
QUIC.Impl.Lemmas.fst
QUIC.Spec.Crypto.ha FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Prims.unit
module QUIC.Impl.Lemmas
include QUIC.Spec.Lemmas

#set-options "--max_fuel 0 --max_ifuel 0"

/// The usual sequence lemmas
/// -------------------------

let lemma_five_cuts
  s i1 i2 i3 i4 i5 s0 s1 s2 s3 s4 s5
=
  ()

let hash_is_keysized_
  a
val hash_is_keysized_ (a: QS.ha): Lemma
  (ensures (QS.keysized a (Spec.Hash.Definitions.hash_length a)))
a: QUIC.Spec.Crypto.ha
  -> FStar.Pervasives.Lemma
    (ensures QUIC.Spec.Crypto.keysized a (Spec.Hash.Definitions.hash_length a))