val fake : FStar.Bytes.bytes
let fake = ctBytes Application_data @| versionBytes TLS_1p2
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'"
/
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
FStar.Bytes.bytes
FStar.Bytes.op_At_Bar MiTLS.Record.ctBytes MiTLS.Content.Application_data MiTLS.Record.versionBytes MiTLS.Parsers.ProtocolVersion.TLS_1p2
let fake =
  
ctBytes Application_data @| versionBytes TLS_1p2