val create_raw
      (ip: ipkg)
      (len_of_i: (ip.t -> keylen))
      (i: ip.t{ip.registered i})
      (len: keylen{len = len_of_i i})
    : ST (raw ip len_of_i i) (requires fun h0 -> model) (ensures fun h0 p h1 -> modifies_none h0 h1)
val create_raw
      (ip: ipkg)
      (len_of_i: (ip.t -> keylen))
      (i: ip.t{ip.registered i})
      (len: keylen{len = len_of_i i})
    : ST (raw ip len_of_i i) (requires fun h0 -> model) (ensures fun h0 p h1 -> modifies_none h0 h1)
let create_raw (ip:ipkg) (len_of_i:ip.t -> keylen)
  (i:ip.t{ip.registered i}) (len:keylen {len = len_of_i i}):
  ST (raw ip len_of_i i)
  (requires fun h0 -> model)
  (ensures fun h0 p h1 -> modifies_none h0 h1)
  = Random.sample32 len
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)

noextract inline_for_extraction
let shared_footprint_raw (ip:ipkg) (len_of_i:ip.t -> keylen): rset = Set.empty

noextract inline_for_extraction
let footprint_raw (ip:ipkg) (len_of_i:ip.t -> keylen)
  (#i:ip.t {ip.registered i}) (k:raw ip len_of_i i)
  : GTot (s:rset{s `Set.disjoint` shared_footprint_raw ip len_of_i})
  =
  let fp = Set.empty in
  let sfp = shared_footprint_raw ip len_of_i in
  Set.lemma_equal_elim (fp `Set.intersect` sfp) Set.empty;
  fp
/
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) ->
    i: Idx?.t ip {Idx?.registered ip i} ->
    len: MiTLS.Pkg.keylen{len = len_of_i i}
  -> FStar.HyperStack.ST.ST (MiTLS.IV.raw ip len_of_i i)
MiTLS.Pkg.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.keylen MiTLS.Pkg.__proj__Idx__item__registered Prims.b2t Prims.op_Equality MiTLS.Random.sample32 FStar.Bytes.lbytes FStar.UInt32.v MiTLS.IV.raw FStar.Monotonic.HyperStack.mem MiTLS.Mem.model FStar.HyperStack.ST.modifies_none
let create_raw
      (ip: ipkg)
      (len_of_i: (ip.t -> keylen))
      (i: ip.t{ip.registered i})
      (len: keylen{len = len_of_i i})
    : ST (raw ip len_of_i i) (requires fun h0 -> model) (ensures fun h0 p h1 -> modifies_none h0 h1) =
  
Random.sample32 len