val op_Array_Access : s: FStar.Seq.Base.seq a -> n: i: Prims.nat{i < FStar.Seq.Base.length s} -> a
let op_Array_Access (#a:Type) (s:Seq.seq a) n = Seq.index s n
module MiTLS.TLS
open MiTLS
module HS = FStar.HyperStack //Added automatically

open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo


module Range = MiTLS.Range
let range = Range.range
let point = Range.point
let frange = Range.frange
let valid_clen = Range.valid_clen
let fragment_range = Range.fragment_range

//open Negotiation
open MiTLS.Old.Epochs
open MiTLS.Connection

module ST   = FStar.HyperStack.ST
module HST  = FStar.HyperStack
module MS   = FStar.Monotonic.Seq
module DS   = MiTLS.DataStream
module SD   = MiTLS.StreamDeltas
module Conn = MiTLS.Connection

module Epochs    = MiTLS.Old.Epochs
module Handshake = MiTLS.Old.Handshake

(* A flag for runtime debugging of TLS data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false *)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("TLS| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_TLS then print else (fun _ -> ())
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.StreamDeltas.fst.checked MiTLS.StreamAE.fst.checked MiTLS.StAE.fst.checked MiTLS.Record.fsti.checked MiTLS.Range.fst.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Old.Epochs.fsti.checked MiTLS.Mem.fst.checked MiTLS.HandshakeLog.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked MiTLS.Connection.fst.checked MiTLS.Cert.fsti.checked FStar.UInt8.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.TLS.fst
s: FStar.Seq.Base.seq a -> n: i: Prims.nat{i < FStar.Seq.Base.length s} -> a
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length FStar.Seq.Base.index
let ( .() ) (#a: Type) (s: Seq.seq a) n =
  
Seq.index s n