val fragments (#i: id) (#rw: rw) (s: state i rw {authId i}) (h: mem) : GTot (frags i)
val fragments (#i: id) (#rw: rw) (s: state i rw {authId i}) (h: mem) : GTot (frags i)
let fragments (#i:id) (#rw:rw) (s:state i rw{authId i}) (h:mem): GTot (frags i) =
  let entries = HS.sel #_ #MS.grows h (ilog s) in
  MS.map ptext entries
(**
Authenticated encryptions of streams of TLS fragments (from Content)
multiplexing StatefulLHAE and StreamAE with (some) length hiding
(for now, under-specifying ciphertexts lengths and values)
*)
module MiTLS.StAE
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically


open FStar.HyperStack
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open MiTLS.TLSInfo


module HS   = FStar.HyperStack

module MS   = FStar.Monotonic.Seq
module C    = MiTLS.Content

module Stream = MiTLS.StreamAE
module StLHAE = MiTLS.StatefulLHAE
module Range = MiTLS.Range
#set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"

////////////////////////////////////////////////////////////////////////////////
//Distinguishing the two multiplexing choices of StAE based on the ids
////////////////////////////////////////////////////////////////////////////////
let is_stream i = ID13? i

let is_stlhae (i:id) =
  if ID12? i && AEAD? (aeAlg_of_id i) then
    let is_aes128 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES128_GCM in
    let is_aes256 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES256_GCM in
    is_aes128 || is_aes256
  else
    false

// type id = i:id {is_stream i \/ is_stlhae i}

// PLAINTEXTS are defined in Content.fragment i
//16-06-08 see also StreamPlain and StatefulPlain.

type stae_id = i:id {is_stream i \/ is_stlhae i}

////////////////////////////////////////////////////////////////////////////////
//Various utilities related to lengths of ciphers and fragments
////////////////////////////////////////////////////////////////////////////////

let frag_plain_len (#i:id{is_stream i}) (f:C.fragment i): StreamPlain.plainLen =
  let r = snd (C.rg i f) + 1 in
  assume (StreamPlain.plainLength r);
  r

let frag_cipher_len (#i:id{is_stream i}) (f:C.fragment i) =
  frag_plain_len f + Stream.ltag i

// CONCRETE KEY MATERIALS, for leaking & coercing.
// (each implementation splits it into encryption keys, IVs, MAC keys, etc)
// ADL: this can now be factored going through the common AEADProvider interface
let aeKeySize (i:stae_id) =
  if is_stream i
  then
    UInt32.v (EverCrypt.aead_keyLen (Stream.alg i)) +
    AEADProvider.iv_length i
  else
    UInt32.v (EverCrypt.aead_keyLen (AEAD?._0 (aeAlg_of_id i))) +
    AEADProvider.salt_length i

type keyBytes (i:stae_id) = lbytes (aeKeySize i)


////////////////////////////////////////////////////////////////////////////////
//`state i rw`, a sum to cover StreamAE (1.3) and StatefulLHAE (1.2)
////////////////////////////////////////////////////////////////////////////////
#set-options "--admit_smt_queries true"
noeq type state (i:id) (rw:rw) =
  | Stream: u:unit{is_stream i} -> Stream.state i rw -> state i rw
  | StLHAE: u:unit{is_stlhae i} -> StLHAE.state i rw -> state i rw

let stream_state (#i:id{is_stream i}) (#rw:rw) (s:state i rw)
  : Tot (Stream.state i rw)
  = let Stream _ s = s in s

let stlhae_state (#i:id{is_stlhae i}) (#rw:rw) (s:state i rw)
  : Tot (StatefulLHAE.state i rw)
  = let StLHAE _ s = s in s

val region: #i:id -> #rw:rw -> state i rw -> Tot rgn
let region (#i:id) (#rw:rw) (s:state i rw): Tot rgn =
  match s with
  | Stream _ x -> Stream.State?.region x
  | StLHAE _ x -> StLHAE.region x

val log_region: #i:id -> #rw:rw -> state i rw -> Tot rgn
let log_region (#i:id) (#rw:rw) (s:state i rw): Tot rgn =
  match s with
  | Stream _ s -> Stream.State?.log_region s
  | StLHAE _ s -> AEAD_GCM.State?.log_region s

type reader i = state i Reader
type writer i = state i Writer

// For 0-RTT: we ignore a failed decryption for the
// handshake traffic key reader if the counter is 0
let tolerate_decrypt_failure (#i:id) (r:reader i)
  : ST bool
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  match r with
  | StLHAE _ _ -> false
  | Stream _ st ->
    let ctr = HST.op_Bang (StreamAE.ctr st.StreamAE.counter) in
    let ID13 (KeyID #li (ExpandedSecret _ t _)) = i in
    0 = ctr && ClientHandshakeTrafficSecret? t

let tolerate_ccs (#i:id) (r:reader i)
  : ST bool
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> modifies_none h0 h1)
  =
  match r with
  | StLHAE _ _ -> false
  | Stream _ st ->
    let ctr = ! (StreamAE.ctr st.StreamAE.counter) in
    let ID13 (KeyID #li (ExpandedSecret _ t _)) = i in
    0 = ctr && (ServerHandshakeTrafficSecret? t ||
      ClientHandshakeTrafficSecret? t || ClientEarlyTrafficSecret? t)

// our view to AE's ideal log (when idealized, ignoring ciphers) and counter
// TODO: write down their joint monotonic specification: both are monotonic,
// and seqn = length log when ideal

////////////////////////////////////////////////////////////////////////////////
//Logs of fragments, defined as projections on the underlying entry logs
////////////////////////////////////////////////////////////////////////////////
// TODO: consider adding constraint on terminator fragments
type frags (i:id{~ (PlaintextID? i)}) = Seq.seq (C.fragment i)

let ideal_log (r:rgn) (i:id) =
  if is_stream i then
    Stream.ideal_log r i
  else if is_stlhae i then
    AEAD_GCM.ideal_log r i
  else False

let ilog (#i:id) (#rw:rw) (s:state i rw{authId i}): Tot (ideal_log (log_region s) i) =
  match s with
  | Stream u s -> Stream.ilog (Stream.State?.log s)
  | StLHAE u s -> AEAD_GCM.ilog (AEAD_GCM.State?.log s)

let entry (i:id) =
   if is_stream i then
     Stream.entry i
   else if is_stlhae i then
     AEAD_GCM.entry i
   else False

private
let ptext (#i:id) (ent:entry i): Tot (C.fragment i) =
  if is_stream i then
    Stream.Entry?.p #i ent
  else
    AEAD_GCM.Entry?.p #i ent
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StreamPlain.fst.checked MiTLS.StreamAE.fst.checked MiTLS.StatefulPlain.fst.checked MiTLS.StatefulLHAE.fst.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.LHAEPlain.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Content.fst.checked MiTLS.AEADProvider.fsti.checked MiTLS.AEAD_GCM.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.StAE.fst
s: MiTLS.StAE.state i rw {MiTLS.TLSInfo.authId i} -> h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot (MiTLS.StAE.frags i)
MiTLS.TLSInfo.id MiTLS.TLSConstants.rw MiTLS.StAE.state Prims.b2t MiTLS.TLSInfo.authId FStar.Monotonic.HyperStack.mem FStar.Monotonic.Seq.map MiTLS.StAE.entry MiTLS.Content.fragment MiTLS.StAE.ptext FStar.Seq.Base.seq FStar.Monotonic.HyperStack.sel FStar.Monotonic.Seq.grows MiTLS.StAE.ilog MiTLS.StAE.frags
let fragments (#i: id) (#rw: rw) (s: state i rw {authId i}) (h: mem) : GTot (frags i) =
  
let entries = HS.sel #_ #MS.grows h (ilog s) in
MS.map ptext entries