val sRTPProtectionProfiles_clens_nth (i: nat)
    : Tot (LL.clens sRTPProtectionProfiles sRTPProtectionProfile)
val sRTPProtectionProfiles_clens_nth (i: nat)
    : Tot (LL.clens sRTPProtectionProfiles sRTPProtectionProfile)
let sRTPProtectionProfiles_clens_nth (i: nat) : Tot (LL.clens sRTPProtectionProfiles sRTPProtectionProfile) = {
  LL.clens_cond = (fun (l: sRTPProtectionProfiles) -> i < L.length l);
  LL.clens_get = (fun (l: sRTPProtectionProfiles) -> L.index l i);
}
module MiTLS.Parsers.SRTPProtectionProfiles

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

open MiTLS.Parsers.SRTPProtectionProfile

inline_for_extraction noextract let min_count = 1
inline_for_extraction noextract let max_count = 32767
type sRTPProtectionProfiles = l:list sRTPProtectionProfile{1 <= L.length l /\ L.length l <= 32767}

inline_for_extraction noextract let sRTPProtectionProfiles_parser_kind = LP.strong_parser_kind 4 65537 None

noextract val sRTPProtectionProfiles_parser: LP.parser sRTPProtectionProfiles_parser_kind sRTPProtectionProfiles

noextract val sRTPProtectionProfiles_serializer: LP.serializer sRTPProtectionProfiles_parser

noextract val sRTPProtectionProfiles_bytesize (x:sRTPProtectionProfiles) : GTot nat

noextract val sRTPProtectionProfiles_bytesize_eq (x:sRTPProtectionProfiles) : Lemma (sRTPProtectionProfiles_bytesize x == Seq.length (LP.serialize sRTPProtectionProfiles_serializer x))

val sRTPProtectionProfiles_parser32: LS.parser32 sRTPProtectionProfiles_parser

val sRTPProtectionProfiles_serializer32: LS.serializer32 sRTPProtectionProfiles_serializer

val sRTPProtectionProfiles_size32: LSZ.size32 sRTPProtectionProfiles_serializer

val sRTPProtectionProfiles_validator: LL.validator sRTPProtectionProfiles_parser

val sRTPProtectionProfiles_jumper: LL.jumper sRTPProtectionProfiles_parser

inline_for_extraction val finalize_sRTPProtectionProfiles (#rrel: _) (#rel: _) (sl: LL.slice rrel rel) (pos pos' : U32.t) : HST.Stack unit
(requires (fun h ->
  U32.v pos + 2 < 4294967296 /\
  LL.writable sl.LL.base (U32.v pos) (U32.v pos + 2) h /\
  LL.valid_list sRTPProtectionProfile_parser h sl (pos `U32.add` 2ul) pos' /\ (
  let count = L.length (LL.contents_list sRTPProtectionProfile_parser h sl (pos `U32.add` 2ul) pos') in
  let len = U32.v pos' - (U32.v pos + 2) in
  ((2 <= len /\ len <= 65535) \/ (1 <= count /\ count <= 32767))
)))
(ensures (fun h _ h' ->
  B.modifies (LL.loc_slice_from_to sl pos (pos `U32.add` 2ul)) h h' /\ (
  let l = LL.contents_list sRTPProtectionProfile_parser h sl (pos `U32.add` 2ul) pos' in
  1 <= L.length l /\ L.length l <= 32767 /\
  LL.valid_content_pos sRTPProtectionProfiles_parser h' sl pos l pos'
)))

val sRTPProtectionProfiles_count (#rrel: _) (#rel: _) (input: LL.slice rrel rel) (pos: U32.t) : HST.Stack U32.t
  (requires (fun h -> LL.valid sRTPProtectionProfiles_parser h input pos))
  (ensures (fun h res h' ->
    let x = LL.contents sRTPProtectionProfiles_parser h input pos in
    let pos' = LL.get_valid_pos sRTPProtectionProfiles_parser h input pos in
    B.modifies B.loc_none h h' /\
    U32.v res == L.length x /\
    U32.v pos' == U32.v pos + 2 + (U32.v res `FStar.Mul.op_Star` 2) /\
    LL.valid_list sRTPProtectionProfile_parser h input (pos `U32.add` 2ul) pos' /\
    LL.contents_list sRTPProtectionProfile_parser h input (pos `U32.add` 2ul) pos' == x
/
prims.fst.checked MiTLS.Parsers.SRTPProtectionProfile.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.SRTPProtectionProfiles.fsti
i: Prims.nat
  -> LowParse.Low.Base.Spec.clens MiTLS.Parsers.SRTPProtectionProfiles.sRTPProtectionProfiles
      MiTLS.Parsers.SRTPProtectionProfile.sRTPProtectionProfile
Prims.nat LowParse.Low.Base.Spec.Mkclens MiTLS.Parsers.SRTPProtectionProfiles.sRTPProtectionProfiles MiTLS.Parsers.SRTPProtectionProfile.sRTPProtectionProfile Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length FStar.List.Tot.Base.index LowParse.Low.Base.Spec.clens
let sRTPProtectionProfiles_clens_nth (i: nat)
    : Tot (LL.clens sRTPProtectionProfiles sRTPProtectionProfile) =
  
{
  LL.clens_cond = (fun (l: sRTPProtectionProfiles) -> i < L.length l);
  LL.clens_get = (fun (l: sRTPProtectionProfiles) -> L.index l i)
}