val ct_rg : i: MiTLS.TLSInfo.id -> f: MiTLS.Content.fragment i
  -> MiTLS.Content.contentType * MiTLS.Range.frange i
let ct_rg i f = ct i f, rg i f
module MiTLS.Content // was TLSFragment
open MiTLS

// Multiplexing protocol payloads into record-layer plaintext
// fragments, and defining their projection to application-level
// streams.

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

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.Range
open MiTLS.DataStream
module Parse = MiTLS.Parse
open MiTLS.Parse
module Range = MiTLS.Range

// this description is detailed enough to compute the size of the plaintext and ciphertext
type fragment (i:id) =
  | CT_Alert    : rg:frange i {wider rg (point 2)} -> alert -> fragment i
  | CT_Handshake: rg:frange i -> f:rbytes rg                -> fragment i  // concrete for now
  | CT_CCS      : rg:frange i {wider rg (point 1)}         -> fragment i
  | CT_Data     : rg:frange i -> f:DataStream.fragment i rg -> fragment i // abstract
// for TLS 1.3
//  | CT_EncryptedHandshake: rg:frange i -> f:Handshake.fragment i rg  -> fragment i // abstract
//  | CT_EarlyData         : rg:frange i -> f:DataStream.fragment i rg -> fragment i // abstract

// move to Seq?
private val split: #a: Type -> s:seq a {Seq.length s > 0} -> Tot(seq a * a)
let split #a s =
  let last = Seq.length s - 1 in
  Seq.slice s 0 last, Seq.index s last

// Alert fragmentation is forbidden in TLS 1.3; as a slight deviation
// from the standard, we also forbid it in earlier version.
// Anyway, this is internal to the Alert protocol.

// Ghost projection from low-level multiplexed fragments to application-level deltas
// Some fragments won't parse; they are ignored in the projection.
// We may prove that they are never written on authentic streams.

val project: i:id -> fs:seq (fragment i) -> Tot (seq (DataStream.delta i))
  (decreases %[Seq.length fs]) // not-quite-stuctural termination
let rec project i fs =
  if Seq.length fs = 0 then Seq.empty
  else
    let fs, f = split #(fragment i) fs in
    let ds = project i fs in
    match f with
    | CT_Data rg d ->
      let d:pre_fragment i = d in //A widening coercion as a proof hint, unpacking (d:fragment i (frange i)) to a pre_fragment i
      snoc ds (DataStream.Data d)   //so that it can be repackaged as a fragment i fragment_range
    | CT_Alert rg ad -> snoc ds (DataStream.Alert ad)
    | _ -> ds     // other fragments are internal to TLS


// try out a few lemmas
// we may also need a projection that takes a low-level pos and yields a high-level pos

val project_ignores_Handshake: i:id -> s:seq (fragment i) {Seq.length s > 0 /\ CT_Handshake? (Seq.index s (Seq.length s - 1))} ->
  Lemma(project i s == project i (Seq.slice s 0 (Seq.length s - 1)))
let project_ignores_Handshake i s = ()
#reset-options


// --------------- parsing and formatting content types ---------------------

type contentType =
  | Change_cipher_spec
  | Alert
  | Handshake
  | Application_data

type contentType13 = ct: contentType { ct <> Change_cipher_spec }

val ctBytes: contentType -> Tot (lbytes 1)
let ctBytes = function
  | Change_cipher_spec -> abyte 20z
  | Alert              -> abyte 21z
  | Handshake          -> abyte 22z
  | Application_data   -> abyte 23z

val parseCT: pinverse_t ctBytes
let parseCT b =
  match b.[0ul] with
  | 20z -> Correct Change_cipher_spec
  | 21z -> Correct Alert
  | 22z -> Correct Handshake
  | 23z -> Correct Application_data

  | _	-> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")

#set-options "--admit_smt_queries true"
val inverse_ct: x:_ -> Lemma
  (requires True)
  (ensures lemma_inverse_g_f ctBytes parseCT x)
  [SMTPat (parseCT (ctBytes x))]
let inverse_ct x = ()

val pinverse_ct: x:_ -> Lemma
  (requires True)
  (ensures (lemma_pinverse_f_g Bytes.equal ctBytes parseCT x))
  [SMTPat (ctBytes (Correct?._0 (parseCT x)))]
let pinverse_ct x = ()
#reset-options

let ctToString = function
  | Change_cipher_spec -> "CCS"
  | Alert              -> "Alert"
  | Handshake          -> "Handshake"
  | Application_data   -> "Data"


// --------------- conditional access to fragment representation ---------------------

val rg: i:id -> fragment i -> Tot (frange i)
let rg i = function
  | CT_Data rg _      -> rg
  | CT_Handshake rg _ -> rg
  | CT_CCS rg         -> rg
  | CT_Alert rg _     -> rg

val ct: i:id -> fragment i -> Tot contentType
let ct i = function
  | CT_Data _ _      -> Application_data
  | CT_Handshake _ _ -> Handshake
  | CT_CCS _         -> Change_cipher_spec
  | CT_Alert _ _     -> Alert
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.DataStream.fst.checked MiTLS.Alert.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Content.fst
i: MiTLS.TLSInfo.id -> f: MiTLS.Content.fragment i
  -> MiTLS.Content.contentType * MiTLS.Range.frange i
MiTLS.TLSInfo.id MiTLS.Content.fragment FStar.Pervasives.Native.Mktuple2 MiTLS.Content.contentType MiTLS.Range.frange MiTLS.Content.ct MiTLS.Content.rg FStar.Pervasives.Native.tuple2
let ct_rg i f =
  
ct i f, rg i f