val certificateRequest12_certificate_types_clens_nth (i: nat)
    : Tot (LL.clens certificateRequest12_certificate_types clientCertificateType)
val certificateRequest12_certificate_types_clens_nth (i: nat)
    : Tot (LL.clens certificateRequest12_certificate_types clientCertificateType)
let certificateRequest12_certificate_types_clens_nth (i: nat) : Tot (LL.clens certificateRequest12_certificate_types clientCertificateType) = {
  LL.clens_cond = (fun (l: certificateRequest12_certificate_types) -> i < L.length l);
  LL.clens_get = (fun (l: certificateRequest12_certificate_types) -> L.index l i);
}
module MiTLS.Parsers.CertificateRequest12_certificate_types

(* 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.ClientCertificateType

inline_for_extraction noextract let min_count = 1
inline_for_extraction noextract let max_count = 255
type certificateRequest12_certificate_types = l:list clientCertificateType{1 <= L.length l /\ L.length l <= 255}

inline_for_extraction noextract let certificateRequest12_certificate_types_parser_kind = LP.strong_parser_kind 2 256 None

noextract val certificateRequest12_certificate_types_parser: LP.parser certificateRequest12_certificate_types_parser_kind certificateRequest12_certificate_types

noextract val certificateRequest12_certificate_types_serializer: LP.serializer certificateRequest12_certificate_types_parser

noextract val certificateRequest12_certificate_types_bytesize (x:certificateRequest12_certificate_types) : GTot nat

noextract val certificateRequest12_certificate_types_bytesize_eq (x:certificateRequest12_certificate_types) : Lemma (certificateRequest12_certificate_types_bytesize x == Seq.length (LP.serialize certificateRequest12_certificate_types_serializer x))

val certificateRequest12_certificate_types_parser32: LS.parser32 certificateRequest12_certificate_types_parser

val certificateRequest12_certificate_types_serializer32: LS.serializer32 certificateRequest12_certificate_types_serializer

val certificateRequest12_certificate_types_size32: LSZ.size32 certificateRequest12_certificate_types_serializer

val certificateRequest12_certificate_types_validator: LL.validator certificateRequest12_certificate_types_parser

val certificateRequest12_certificate_types_jumper: LL.jumper certificateRequest12_certificate_types_parser

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

val certificateRequest12_certificate_types_count (#rrel: _) (#rel: _) (input: LL.slice rrel rel) (pos: U32.t) : HST.Stack U32.t
  (requires (fun h -> LL.valid certificateRequest12_certificate_types_parser h input pos))
  (ensures (fun h res h' ->
    let x = LL.contents certificateRequest12_certificate_types_parser h input pos in
    let pos' = LL.get_valid_pos certificateRequest12_certificate_types_parser h input pos in
    B.modifies B.loc_none h h' /\
    U32.v res == L.length x /\
    U32.v pos' == U32.v pos + 1 + (U32.v res `FStar.Mul.op_Star` 1) /\
    LL.valid_list clientCertificateType_parser h input (pos `U32.add` 1ul) pos' /\
    LL.contents_list clientCertificateType_parser h input (pos `U32.add` 1ul) pos' == x
/
prims.fst.checked MiTLS.Parsers.ClientCertificateType.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.CertificateRequest12_certificate_types.fsti
i: Prims.nat
  -> LowParse.Low.Base.Spec.clens MiTLS.Parsers.CertificateRequest12_certificate_types.certificateRequest12_certificate_types
      MiTLS.Parsers.ClientCertificateType.clientCertificateType
Prims.nat LowParse.Low.Base.Spec.Mkclens MiTLS.Parsers.CertificateRequest12_certificate_types.certificateRequest12_certificate_types MiTLS.Parsers.ClientCertificateType.clientCertificateType Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length FStar.List.Tot.Base.index LowParse.Low.Base.Spec.clens
let certificateRequest12_certificate_types_clens_nth (i: nat)
    : Tot (LL.clens certificateRequest12_certificate_types clientCertificateType) =
  
{
  LL.clens_cond = (fun (l: certificateRequest12_certificate_types) -> i < L.length l);
  LL.clens_get = (fun (l: certificateRequest12_certificate_types) -> L.index l i)
}