val parseHeader (h5: header) : Tot parsed_header
val parseHeader (h5: header) : Tot parsed_header
let parseHeader (h5:header) : Tot parsed_header =
    let (ct1,b4)   = FStar.Bytes.split h5 1ul in
    let (pv2,len2) = FStar.Bytes.split b4 2ul in
    match parseCT ct1 with
    | Error z -> Error z
    | Correct ct ->
      match parseVersion pv2 with
      | Error z -> Error z
      | Correct (Unknown_protocolVersion _) ->
        fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Parsed unknown protocol version")
      | Correct pv ->
          let len = int_of_bytes len2 in
          if len <= 0 || len > max_TLSCiphertext_fragment_length
          then fatal Illegal_parameter (perror __SOURCE_FILE__ __LINE__ "Wrong fragment length")
          else correct(ct,pv,len)
module MiTLS.Record
open MiTLS

(* (optional) encryption and processing of the outer, untrusted record format *)

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

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.Range
open MiTLS.Content

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

// Consider merging some of this module with Content?

(* A flag for runtime debugging of record data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false. *)
private let discard (_:bool) : ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) = ()
private let print s = discard (IO.debug_print_string ("REC| "^s^"\n"))
private unfold let trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_Record then print else (fun _ -> ())


private let p_of_f (f:bytes): (p:FStar.Bytes.bytes{ FStar.Bytes.length p = FStar.Bytes.length f }) = f
private let f_of_p (p:FStar.Bytes.bytes): (f:bytes{ FStar.Bytes.length p = FStar.Bytes.length f }) = p
private let ctBytes x = f_of_p (ctBytes x)
private let parseCT (x: lbytes 1) = parseCT (p_of_f x)
private let versionBytes x = f_of_p (versionBytes x) 
private let parseVersion (x: lbytes 2) = parseVersion (p_of_f x)


// ------------------------outer packet format -------------------------------

// the "outer" header has the same format for all versions of TLS
// but TLS 1.3 fakes its content type and protocol version.

private let headerLen = 5ul 
private (* noextract *) let headerLength = v headerLen 
private type header = b:lbytes headerLength // for all TLS versions

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

private let fake = ctBytes Application_data @| versionBytes TLS_1p2

// this is the outer packet; to comply with legacy version signalling,
// the *caller* should switch from 1.3 to 1.0 whenever data is
// encrypted.
#set-options "--z3rlimit 10" //18-04-20 now required; why?
private inline_for_extraction 
let makeHeader ct plain ver (length:nat {repr_bytes length <= 2}): header =
  let ct_ver = 
    if TLS_1p3? ver then if plain then 
      (ctBytes ct @| versionBytes TLS_1p2) 
    else 
      fake 
    else 
      (ctBytes ct @| versionBytes ver) in
  ct_ver @| bytes_of_int 2 length 

// used only for testing
let makePacket ct plain ver (data: (b:bytes { repr_bytes (length b) <= 2})) =
  makeHeader ct plain ver (length data) @| data

let sendPacket tcp ct plain ver (data: (b:bytes { repr_bytes (length b) <= 2})) =
  // still some margin for progress to avoid intermediate copies
  let header = makeHeader ct plain ver (length data) in 
  trace ("record headers: "^print_bytes header);
  let res = Transport.send tcp (BufferBytes.from_bytes header) headerLen in
  if res = Int.Cast.uint32_to_int32 headerLen then 
    let res = Transport.send tcp (BufferBytes.from_bytes data) (len data) in
    if Int32.v res = length data
    then Correct()
    else Error(Printf.sprintf "Transport.send(header) returned %l" res)
  else   Error(Printf.sprintf "Transport.send(payload) returned %l" res)

private type parsed_header = result (contentType
                           * protocolVersion
                           * l:nat { l <= max_TLSCiphertext_fragment_length})
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.DebugFlags.fst.checked MiTLS.Content.fst.checked MiTLS.BufferBytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Int32.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked FStar.Buffer.fst.checked
MiTLS.Record.fsti
h5: MiTLS.Record.header -> MiTLS.Record.parsed_header
MiTLS.Record.header FStar.Bytes.bytes MiTLS.Record.parseCT MiTLS.TLSError.error FStar.Error.Error FStar.Pervasives.Native.tuple3 MiTLS.Content.contentType MiTLS.TLSConstants.protocolVersion Prims.nat Prims.b2t Prims.op_LessThanOrEqual MiTLS.TLSConstants.max_TLSCiphertext_fragment_length MiTLS.Record.parseVersion FStar.UInt16.t Prims.op_Negation MiTLS.Parsers.ProtocolVersion.known_protocolVersion_repr MiTLS.TLSError.fatal MiTLS.Parsers.AlertDescription.Decode_error FStar.Error.perror MiTLS.TLSConstants.protocolVersion' Prims.op_BarBar Prims.op_GreaterThan MiTLS.Parsers.AlertDescription.Illegal_parameter Prims.bool FStar.Error.correct FStar.Pervasives.Native.Mktuple3 MiTLS.Record.parsed_header FStar.Bytes.uint_k FStar.UInt32.v FStar.Bytes.len FStar.Bytes.int_of_bytes FStar.Pervasives.Native.tuple2 Prims.eq2 FStar.Seq.Base.seq FStar.UInt8.t FStar.Pervasives.Native.Mktuple2 FStar.Bytes.reveal FStar.Seq.Properties.split FStar.UInt32.uint_to_t FStar.UInt32.t FStar.Bytes.split FStar.UInt32.__uint_to_t
let parseHeader (h5: header) : Tot parsed_header =
  
let ct1, b4 = FStar.Bytes.split h5 1ul in
let pv2, len2 = FStar.Bytes.split b4 2ul in
match parseCT ct1 with
| Error z -> Error z
| Correct ct ->
  match parseVersion pv2 with
  | Error z -> Error z
  | Correct (Unknown_protocolVersion _) ->
    fatal Decode_error (perror "MiTLS.Record.fsti" 10 "Parsed unknown protocol version")
  | Correct pv ->
    let len = int_of_bytes len2 in
    if len <= 0 || len > max_TLSCiphertext_fragment_length
    then fatal Illegal_parameter (perror "MiTLS.Record.fsti" 14 "Wrong fragment length")
    else correct (ct, pv, len)