val namedGroupList_clens_nth (i: nat) : Tot (LL.clens namedGroupList namedGroup)
let namedGroupList_clens_nth (i: nat) : Tot (LL.clens namedGroupList namedGroup) = {
  LL.clens_cond = (fun (l: namedGroupList) -> i < L.length l);
  LL.clens_get = (fun (l: namedGroupList) -> L.index l i);
}
val namedGroupList_clens_nth (i: nat) : Tot (LL.clens namedGroupList namedGroup)
let namedGroupList_clens_nth (i: nat) : Tot (LL.clens namedGroupList namedGroup) =
{
  LL.clens_cond = (fun (l: namedGroupList) -> i < L.length l);
  LL.clens_get = (fun (l: namedGroupList) -> L.index l i)
}
Parsers.NamedGroupList.fsti.checked
prims.fst.checked Parsers.NamedGroup.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
Parsers.NamedGroupList.fsti
Prims.nat LowParse.Low.Base.Spec.Mkclens Parsers.NamedGroupList.namedGroupList Parsers.NamedGroup.namedGroup Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length FStar.List.Tot.Base.index LowParse.Low.Base.Spec.clens
module Parsers.NamedGroupList

(* 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 Parsers.NamedGroup

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

inline_for_extraction noextract let namedGroupList_parser_kind = LP.strong_parser_kind 4 65537 None

noextract val namedGroupList_parser: LP.parser namedGroupList_parser_kind namedGroupList

noextract val namedGroupList_serializer: LP.serializer namedGroupList_parser

noextract val namedGroupList_bytesize (x:namedGroupList) : GTot nat

noextract val namedGroupList_bytesize_eq (x:namedGroupList) : Lemma (namedGroupList_bytesize x == Seq.length (LP.serialize namedGroupList_serializer x))

val namedGroupList_parser32: LS.parser32 namedGroupList_parser

val namedGroupList_serializer32: LS.serializer32 namedGroupList_serializer

val namedGroupList_size32: LSZ.size32 namedGroupList_serializer

val namedGroupList_validator: LL.validator namedGroupList_parser

val namedGroupList_jumper: LL.jumper namedGroupList_parser

inline_for_extraction val finalize_namedGroupList (#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 namedGroup_parser h sl (pos `U32.add` 2ul) pos' /\ (
  let count = L.length (LL.contents_list namedGroup_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 namedGroup_parser h sl (pos `U32.add` 2ul) pos' in
  1 <= L.length l /\ L.length l <= 32767 /\
  LL.valid_content_pos namedGroupList_parser h' sl pos l pos'
)))

val namedGroupList_count (#rrel: _) (#rel: _) (input: LL.slice rrel rel) (pos: U32.t) : HST.Stack U32.t
  (requires (fun h -> LL.valid namedGroupList_parser h input pos))
  (ensures (fun h res h' ->
    let x = LL.contents namedGroupList_parser h input pos in
    let pos' = LL.get_valid_pos namedGroupList_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 namedGroup_parser h input (pos `U32.add` 2ul) pos' /\
    LL.contents_list namedGroup_parser h input (pos `U32.add` 2ul) pos' == x
  ))
val namedGroupList_clens_nth (i: nat) : Tot (LL.clens namedGroupList namedGroup)
i: Prims.nat
  -> LowParse.Low.Base.Spec.clens Parsers.NamedGroupList.namedGroupList
      Parsers.NamedGroup.namedGroup