val stream_deltas_snoc (i: id) (frags: StAE.frags i) (f: Content.fragment i)
    : Lemma
    (project_deltas (Seq.snoc frags f) == Seq.append (project_deltas frags) (project_one_frag f))
val stream_deltas_snoc (i: id) (frags: StAE.frags i) (f: Content.fragment i)
    : Lemma
    (project_deltas (Seq.snoc frags f) == Seq.append (project_deltas frags) (project_one_frag f))
let stream_deltas_snoc (i:id) (frags:StAE.frags i) (f:Content.fragment i)
  : Lemma (project_deltas (Seq.snoc frags f) == Seq.append (project_deltas frags) (project_one_frag f))
  = MS.collect_snoc project_one_frag frags f
module MiTLS.StreamDeltas
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open FStar.HyperStack
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module HS   = FStar.HyperStack
module HST = FStar.HyperStack.ST //Added automatically; avoid.
module MS   = FStar.Monotonic.Seq
module S    = MiTLS.StAE
module C    = MiTLS.Content
module DS   = MiTLS.DataStream

let deltas i = Seq.seq (DS.delta i) //not yet handling the well-formedness condition of final deltas

let singleton (x:'a) : Tot (Seq.seq 'a) = Seq.create 1 x

#reset-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"

private type id = i:id{~(PlaintextID? i)}

val project_one_frag: #i:id -> f:C.fragment i -> Tot (Seq.seq (DS.delta i))
let project_one_frag #i = function
    | C.CT_Data rg d -> 
      let d : DS.pre_fragment i = d in //A widening coercion as a proof hint, unpacking (d:fragment i (frange i)) to a pre_fr
      singleton (DataStream.Data d)
    | C.CT_Alert _ ad -> singleton (DataStream.Alert ad)
    | _ -> Seq.empty                 // other fragments are internal to TLS

val project_deltas: #i:id -> fs:S.frags i -> GTot (deltas i)
let project_deltas #i fs = MS.collect project_one_frag fs

val stream_deltas: #i:id -> #rw:rw -> s:StAE.state i rw{authId i} -> mem -> GTot (deltas i)
let stream_deltas #i #rw s h = project_deltas (StAE.fragments s h)
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StAE.fst.checked MiTLS.Mem.fst.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
MiTLS.StreamDeltas.fst
i: MiTLS.StreamDeltas.id -> frags: MiTLS.StAE.frags i -> f: MiTLS.Content.fragment i
  -> FStar.Pervasives.Lemma
    (ensures
      MiTLS.StreamDeltas.project_deltas (FStar.Seq.Properties.snoc frags f) ==
      FStar.Seq.Base.append (MiTLS.StreamDeltas.project_deltas frags)
        (MiTLS.StreamDeltas.project_one_frag f))
MiTLS.StreamDeltas.id MiTLS.StAE.frags MiTLS.Content.fragment FStar.Monotonic.Seq.collect_snoc MiTLS.DataStream.delta MiTLS.StreamDeltas.project_one_frag Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.seq MiTLS.StreamDeltas.project_deltas FStar.Seq.Properties.snoc FStar.Seq.Base.append Prims.Nil FStar.Pervasives.pattern
let stream_deltas_snoc (i: id) (frags: StAE.frags i) (f: Content.fragment i)
    : Lemma
    (project_deltas (Seq.snoc frags f) == Seq.append (project_deltas frags) (project_one_frag f)) =
  
MS.collect_snoc project_one_frag frags f