val within : n: Prims.nat -> r: MiTLS.Range.range -> Prims.bool
let within (n:nat) (r:range) = fst r <= n && n <= snd r
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

let hashLen = Hacl.Hash.Definitions.hash_len

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

#set-options "--initial_fuel 0 --initial_ifuel 1 --max_fuel 0 --max_ifuel 2"

type id2 = i:id { ID12? i } // gradually adding TLS 1.3...

(* ranges *)
/
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
n: Prims.nat -> r: MiTLS.Range.range -> Prims.bool
Prims.nat MiTLS.Range.range Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd Prims.bool
let within (n: nat) (r: range) =
  
fst r <= n && n <= snd r