val ilog (#r: rgn) (#i: id) (l: log_ref r i {authId i}) : ideal_log r i
val ilog (#r: rgn) (#i: id) (l: log_ref r i {authId i}) : ideal_log r i
let ilog (#r:rgn) (#i:id) (l:log_ref r i{authId i}): ideal_log r i = l
module MiTLS.AEAD_GCM
open MiTLS
// AEAD-GCM mode for the TLS record layer, as specified in RFC 5288.
// We support both AES_128_GCM and AES_256_GCM, differing only in their key sizes

open FStar.Heap
open FStar.HyperStack
open FStar.Seq
open FStar.Bytes

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

module Range = MiTLS.Range
open MiTLS.Range

open FStar.Monotonic.Seq

module Range = MiTLS.Range
module AEAD = MiTLS.AEADProvider
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

type id = i:id{ ID12? i /\ AEAD? (aeAlg_of_id i) }
let alg (i:id) = let AEAD ae _ = aeAlg_of_id i in ae

type cipher (i:id) = c:bytes{ valid_clen i (length c) }

type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i

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

// this is the same as a sequence number and in bytes, GCMNonce.nonce_explicit[8]
type counter a = c:nat{c <= max_ctr a}

type dplain (i:id) (ad:adata i) (c:cipher i) =
  plain i ad (cipherRangeClass i (length c))

type entry (i:id) = // records that c is an encryption of p with ad
  | Entry: c:cipher i -> ad:adata i -> p:dplain i ad c -> entry i

let ideal_log (r:rgn) (i:id) = log_t r (entry i)

let log_ref (r:rgn) (i:id): Tot Type0 =
  if authId i then ideal_log r i else unit
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StatefulPlain.fst.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.LHAEPlain.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.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.AEAD_GCM.fst
l: MiTLS.AEAD_GCM.log_ref r i {MiTLS.TLSInfo.authId i} -> MiTLS.AEAD_GCM.ideal_log r i
MiTLS.Mem.rgn MiTLS.AEAD_GCM.id MiTLS.AEAD_GCM.log_ref Prims.b2t MiTLS.TLSInfo.authId MiTLS.AEAD_GCM.ideal_log
let ilog (#r: rgn) (#i: id) (l: log_ref r i {authId i}) : ideal_log r i =
  
l