val shared_footprint_raw (ip: ipkg) (len_of_i: (ip.t -> keylen)) : rset
val shared_footprint_raw (ip: ipkg) (len_of_i: (ip.t -> keylen)) : rset
let shared_footprint_raw (ip:ipkg) (len_of_i:ip.t -> keylen): rset = Set.empty
module MiTLS.IV
open MiTLS

open MiTLS.Mem
open MiTLS.Pkg



/// A sample functionality for fresh, public initialization vectors,
/// with the length of the byte vector as a basic agility
/// parameter. We use this functionality e.g. for generating the
/// static IV for TLS AEAD as part of the TLS key schedule.
///
/// There is no need for an idealization flag: the main (unconditional)
/// property is that the vector is a function of the index; this
/// vector is fresh whenever create is called instead of coerce.
type idealRaw = b2t Flags.flag_Raw

// SZ: [len_of_i] was implicit, but it can't be inferred from [i]. Made it explicit
type rawlen (#ip:ipkg) (len_of_i:ip.t -> keylen) (i:ip.t) = len:keylen {len == len_of_i i}

type raw (ip:ipkg) (len_of_i:ip.t -> keylen) (i:ip.t{ip.registered i}) = Bytes.lbytes32 (len_of_i i)
/
prims.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Bytes.fsti.checked
MiTLS.IV.fst
ip: MiTLS.Pkg.ipkg -> len_of_i: (_: Idx?.t ip -> MiTLS.Pkg.keylen) -> MiTLS.Mem.rset
MiTLS.Pkg.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.keylen FStar.Set.empty FStar.Monotonic.HyperHeap.rid MiTLS.Mem.rset
let shared_footprint_raw (ip: ipkg) (len_of_i: (ip.t -> keylen)) : rset =
  
Set.empty