val final: i:id -> delta i -> Tot bool
val final: i:id -> delta i -> Tot bool
let final i d =
  match d with
  | Data f  -> false
  | Close   -> true
  | Alert a -> a.level = Fatal
module MiTLS.DataStream
open MiTLS

(* Application-level bytes streams exchanged over TLS;            *)
(* depending on the safety of their indexes,                      *)
(* these streams are treated abstractly by miTLS                  *)

//* now generalized to include signals; rename to Stream?

open FStar.Heap
open FStar.HyperStack
open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
module Range = MiTLS.Range
open MiTLS.Range

module HS = FStar.HyperStack

//--------- application data fragments ------------------------------

// The implementation of this type is application-specific
// but it must provide a few functions to TLS, declared below.
// On safe connections, TLS ensures privacy by type abstraction
// we care about the range mostly on the sender side.

// this style enables structural subtyping on range indexes
// JP, NS: XXX temporarily removing the abstraction for the sake of extraction
//private type id = i:id{~ (PlaintextID? i)}

type pre_fragment (i:id) = bytes

val ghost_repr: #i:id -> pre_fragment i -> GTot bytes
let ghost_repr #i f = f

type fragment (i:id) (rg:range) = f:pre_fragment i { within (length (ghost_repr f)) rg}

val repr: #i:id { ~(safeId i)} -> rg:frange i -> p:fragment i rg -> Tot (b:rbytes rg {b = ghost_repr #i p})
let repr #i rg f = f

val mk_fragment: #i:id { ~(authId i)} -> rg:frange i -> b:rbytes rg -> Tot (p:fragment i rg {b = ghost_repr #i p})
let mk_fragment #i rg b = b

// these two functions are used only by the application (or ghostly)
val appFragment: i:id -> rg:frange i -> rbytes rg -> Tot (fragment i rg)
val appBytes:  #i:id -> #rg:frange i -> fragment i rg -> Tot (rbytes rg)

let appFragment i rg f = f
let appBytes  #i #rg f = f

(* revisit:

// these two functions are used only on unsafe epochs
//* how to specify both abstraction & functional correctness? see AppData.fs7
val deltaPlain: i:id { ~(authId i)}-> rg:range -> rbytes rg -> Tot (fragment i rg)
val deltaRepr:  i:id { ~(safeId i)}-> rg:range -> fragment i rg -> Tot (rbytes rg)

let deltaPlain i rg f = f
let deltaRepr  i rg f = f
*)


//----------application events (data + control) -------------------

type delta (i:id) =
  | Data of fragment i fragment_range
  | Close
  | Alert of alert
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.DataStream.fst
i: MiTLS.TLSInfo.id -> d: MiTLS.DataStream.delta i -> Prims.bool
MiTLS.TLSInfo.id MiTLS.DataStream.delta MiTLS.DataStream.fragment MiTLS.Range.fragment_range MiTLS.Parsers.Alert.alert Prims.op_Equality MiTLS.Parsers.AlertLevel.alertLevel MiTLS.Parsers.Alert.__proj__Mkalert__item__level MiTLS.Parsers.AlertLevel.Fatal Prims.bool
let final i d =
  
match d with
| Data f -> false
| Close -> true
| Alert a -> a.level = Fatal