val outerPV (c: connection)
    : ST protocolVersion (requires (Handshake.hs_inv c.hs)) (ensures (fun h0 pv h1 -> h0 == h1))
val outerPV (c: connection)
    : ST protocolVersion (requires (Handshake.hs_inv c.hs)) (ensures (fun h0 pv h1 -> h0 == h1))
let outerPV (c:connection) : ST protocolVersion
  (requires (Handshake.hs_inv c.hs))
  (ensures (fun h0 pv h1 -> h0 == h1)) =
  match Handshake.version_of c.hs with
  | TLS_1p3 -> TLS_1p0
  | pv      -> pv
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 _ -> ())


unfold let op_Array_Access (#a:Type) (s:Seq.seq a) n = Seq.index s n // s.[n]

// using also DataStream, Content, Record
#set-options "--initial_ifuel 0 --max_ifuel 0 --initial_fuel 0 --max_fuel 0 --admit_smt_queries true"


(** misc ***)
/
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
c: MiTLS.Connection.connection -> FStar.HyperStack.ST.ST MiTLS.TLSConstants.protocolVersion
MiTLS.Connection.connection MiTLS.Parsers.ProtocolVersion.TLS_1p0 MiTLS.Parsers.ProtocolVersion.protocolVersion MiTLS.TLSConstants.protocolVersion MiTLS.Old.Handshake.version_of MiTLS.Connection.__proj__C__item__hs MiTLS.Old.Handshake.hs_inv FStar.Monotonic.HyperStack.mem Prims.eq2
let outerPV (c: connection)
    : ST protocolVersion (requires (Handshake.hs_inv c.hs)) (ensures (fun h0 pv h1 -> h0 == h1)) =
  
match Handshake.version_of c.hs with
| TLS_1p3 -> TLS_1p0
| pv -> pv