val ctr (#l #r: erid) (#i: id) (#log: log_ref l i) (c: ctr_ref r i log)
    : Tot (m_rref r (if authId i then seqn_val #l #(entry i) r log max_ctr else counter) increases)
val ctr (#l #r: erid) (#i: id) (#log: log_ref l i) (c: ctr_ref r i log)
    : Tot (m_rref r (if authId i then seqn_val #l #(entry i) r log max_ctr else counter) increases)
let ctr (#l:erid) (#r:erid) (#i:id) (#log:log_ref l i) (c:ctr_ref r i log)
  : Tot (m_rref r (if authId i
		   then seqn_val #l #(entry i) r log max_ctr
		   else counter)
		increases) =
  c
(**
Provides authenticated encryption for a stream of variable-length plaintexts;
concretely, we use AES_GCM but any other AEAD algorithm would do.
*)
module MiTLS.StreamAE
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically

open FStar.HyperStack
open FStar.Seq
open FStar.Monotonic.Seq
open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.StreamPlain

module AEAD = MiTLS.AEADProvider
module HS = FStar.HyperStack

type rid = HST.erid

type id = i:id { ID13? i }

let alg (i:id) =
  let AEAD ae _ = aeAlg_of_id i in ae

let ltag i : nat = UInt32.v (EverCrypt.aead_tagLen (alg i))
let cipherLen i (l:plainLen) : nat = l + ltag i
type cipher i (l:plainLen) = lbytes (cipherLen i l)

// will require proving before decryption
let lenCipher i (c:bytes { ltag i <= length c }) : nat = length c - ltag i

type entry (i:id) =
  | Entry: l:plainLen -> c:cipher i l -> p:plain i l -> entry i

// key materials (from the AEAD provider)
type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i
 
let ideal_log (r:erid) (i:id) = log_t r (entry i)

let log_ref (r:erid) (i:id) : Tot Type0 =
  if authId i then ideal_log r i else unit

noextract
let ilog (#r:erid) (#i:id) (l:log_ref r i{authId i}) : Tot (ideal_log r i) =
  l

irreducible let max_ctr: n:nat{n = 18446744073709551615} =
  assert_norm (pow2 64 - 1 = 18446744073709551615);
  pow2 64 - 1

type counter = c:nat{c <= max_ctr}

let ideal_ctr (#l:erid) (r: erid) (i:id) (log:ideal_log l i) : Tot Type0 =
  FStar.Monotonic.Seq.seqn r log max_ctr
  // An increasing counter, at most min(length log, 2^64-1)

let concrete_ctr (r:erid) (i:id) : Tot Type0 =
  m_rref r counter increases

let ctr_ref (#l:erid) (r:erid) (i:id) (log:log_ref l i) : Tot Type0 =
  if authId i
  then ideal_ctr r i (log <: ideal_log l i)
  else m_rref r counter increases
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StreamPlain.fst.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.StreamAE.fst
c: MiTLS.StreamAE.ctr_ref r i log
  -> FStar.HyperStack.ST.m_rref r
      (match MiTLS.TLSInfo.authId i with
        | true -> FStar.Monotonic.Seq.seqn_val r log MiTLS.StreamAE.max_ctr
        | _ -> MiTLS.StreamAE.counter)
      FStar.Monotonic.Seq.increases
FStar.HyperStack.ST.erid MiTLS.StreamAE.id MiTLS.StreamAE.log_ref MiTLS.StreamAE.ctr_ref FStar.HyperStack.ST.m_rref MiTLS.TLSInfo.authId FStar.Monotonic.Seq.seqn_val MiTLS.StreamAE.entry MiTLS.StreamAE.max_ctr Prims.bool MiTLS.StreamAE.counter FStar.Monotonic.Seq.increases
let ctr (#l #r: erid) (#i: id) (#log: log_ref l i) (c: ctr_ref r i log)
    : Tot (m_rref r (if authId i then seqn_val #l #(entry i) r log max_ctr else counter) increases) =
  
c