val hashLen : a: Spec.Hash.Definitions.fixed_len_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}
let hashLen = Hacl.Hash.Definitions.hash_len
module MiTLS.Range
open MiTLS

(* This module defines all range computations for the lengths of
   plaintext messages exchanged over TLS, in order to construct
   length-hiding authenticated encryption. *)

open FStar.Bytes
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module AE = MiTLS.AEADProvider
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Range.fst
a: Spec.Hash.Definitions.fixed_len_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}
Hacl.Hash.Definitions.hash_len
let hashLen =
  
Hacl.Hash.Definitions.hash_len