val split: #a: Type -> s:seq a {Seq.length s > 0} -> Tot(seq a * a)
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
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?
/
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
s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s > 0} -> FStar.Seq.Base.seq a * a
FStar.Seq.Base.seq Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.slice FStar.Seq.Base.index Prims.int Prims.op_Subtraction FStar.Pervasives.Native.tuple2
let split #a s =
  
let last = Seq.length s - 1 in
Seq.slice s 0 last, Seq.index s last