val gen: r0:rid{is_eternal_region r0 /\ witnessed(region_contains_pred r0)} -> i:id -> HyperStack.All.ML (state i * state i)
val gen: r0:rid{is_eternal_region r0 /\ witnessed(region_contains_pred r0)} -> i:id -> HyperStack.All.ML (state i * state i)
let gen r0 (i:id) =
  let r = new_region r0 in
  empty_is_well_formed i;
  let t = ralloc r [] in
  let log = if authId i then Some t else None in
  let ctr = ralloc r 0 in
  let enc = State #i #r log ( ctr) in
  let dec = State #i #r log ( ctr) in
  enc, dec
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

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

let rec finalized (i:id) (s:list (delta i)): bool =
  match s with 
  | [] -> false
  | hd::tl -> final i hd || finalized i tl

val wellformed: i:id -> list (delta i) -> Tot bool
let rec wellformed ki s =
  match s with
  | [] | [_] -> true
  | d::s -> not (final ki d)

(*
 * AR: this is strange. For some reason, this takes a long time to go through.
 * And without this, gen below seems to time out.
 *)
private val empty_is_well_formed: i:id -> Lemma (requires (True)) (ensures (wellformed i []))
let empty_is_well_formed i = ()

type stream (i:id) = s: list (delta i) { wellformed i s }

// on authentic encrypted streams, 
// the (ghost, viewed) writer state is the current stream contents;
// the (ghost, viewed) reader state is an index in the stream.


// --- experimental
//* not much point sharing the two? is it re-implementing AppData?
//* maybe the state is just an rref?

noeq type state (i:id) =
  | State: #region:rid ->
           log: option (r: ref (stream i) {frameOf r = region}) { Some? log <==> authId i } ->
           ctr: ref nat {frameOf ctr = region} ->
           state i

(*
 * AR: adding the is_eternal_region refinement to satify the precondition of new_region.
 *)
/
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

    r0:
      FStar.Monotonic.HyperHeap.rid
        { FStar.HyperStack.ST.is_eternal_region r0 /\
          FStar.HyperStack.ST.witnessed (FStar.HyperStack.ST.region_contains_pred r0) } ->
    i: MiTLS.TLSInfo.id
  -> FStar.HyperStack.All.ML (MiTLS.DataStream.state i * MiTLS.DataStream.state i)
FStar.Monotonic.HyperHeap.rid Prims.l_and FStar.HyperStack.ST.is_eternal_region FStar.HyperStack.ST.witnessed FStar.HyperStack.ST.region_contains_pred MiTLS.TLSInfo.id FStar.Pervasives.Native.Mktuple2 MiTLS.DataStream.state MiTLS.DataStream.State FStar.Pervasives.Native.tuple2 FStar.HyperStack.ST.mref Prims.nat FStar.Heap.trivial_preorder FStar.HyperStack.ST.ralloc FStar.Pervasives.Native.option FStar.HyperStack.ST.ref MiTLS.DataStream.stream Prims.b2t Prims.op_Equality FStar.Monotonic.HyperStack.frameOf Prims.l_iff FStar.Pervasives.Native.uu___is_Some MiTLS.TLSInfo.authId FStar.Pervasives.Native.Some Prims.bool FStar.Pervasives.Native.None Prims.Nil MiTLS.DataStream.delta Prims.unit MiTLS.DataStream.empty_is_well_formed FStar.HyperStack.ST.new_region
let gen r0 (i: id) =
  
let r = new_region r0 in
empty_is_well_formed i;
let t = ralloc r [] in
let log = if authId i then Some t else None in
let ctr = ralloc r 0 in
let enc = State #i #r log (ctr) in
let dec = State #i #r log (ctr) in
enc, dec