val ghost_repr: #i:id -> pre_fragment i -> GTot bytes
val ghost_repr: #i:id -> pre_fragment i -> GTot bytes
let ghost_repr #i 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
/
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
f: MiTLS.DataStream.pre_fragment i -> Prims.GTot FStar.Bytes.bytes
MiTLS.TLSInfo.id MiTLS.DataStream.pre_fragment FStar.Bytes.bytes
let ghost_repr #i f =
  
f