val zero : MiTLS.Range.range
let zero = point 0
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 *)
type range = r:(nat * nat) { fst r <= snd r }
let within (n:nat) (r:range) = fst r <= n && n <= snd r
let wider (r1:range) (r2:range) = fst r1 <= fst r2 && snd r2 <= snd r1
type rbytes (r:range) = b:bytes {within (length b) r}
/
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
MiTLS.Range.range
MiTLS.Range.point
let zero =
  
point 0