val project: i:id -> fs:seq (fragment i) -> Tot (seq (DataStream.delta i))
  (decreases %[Seq.length fs])
val project: i:id -> fs:seq (fragment i) -> Tot (seq (DataStream.delta i))
  (decreases %[Seq.length fs])
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
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))
/
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 -> fs: FStar.Seq.Base.seq (MiTLS.Content.fragment i)
  -> Prims.Tot (FStar.Seq.Base.seq (MiTLS.DataStream.delta i))
MiTLS.TLSInfo.id FStar.Seq.Base.seq MiTLS.Content.fragment Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Base.empty MiTLS.DataStream.delta Prims.bool MiTLS.Range.frange MiTLS.DataStream.fragment FStar.Seq.Properties.snoc MiTLS.DataStream.Data MiTLS.DataStream.pre_fragment Prims.b2t MiTLS.Range.wider MiTLS.Range.point MiTLS.Parsers.Alert.alert MiTLS.DataStream.Alert MiTLS.Content.project FStar.Pervasives.Native.tuple2 MiTLS.Content.split
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
    snoc ds (DataStream.Data d)
  | CT_Alert rg ad -> snoc ds (DataStream.Alert ad)
  | _ -> ds