val repr: #i:id { ~(safeId i)} -> rg:frange i -> p:fragment i rg -> Tot (b:rbytes rg {b = ghost_repr #i p})
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
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}
/
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
rg: MiTLS.Range.frange i -> p: MiTLS.DataStream.fragment i rg
  -> b: MiTLS.Range.rbytes rg {b = MiTLS.DataStream.ghost_repr p}
MiTLS.TLSInfo.id Prims.l_not Prims.b2t MiTLS.TLSInfo.safeId MiTLS.Range.frange MiTLS.DataStream.fragment MiTLS.Range.rbytes Prims.op_Equality FStar.Bytes.bytes MiTLS.DataStream.ghost_repr
let repr #i rg f =
  
f