val oIDFilter_jumper: LL.jumper oIDFilter_parser
val oIDFilter_jumper: LL.jumper oIDFilter_parser
let oIDFilter_jumper =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LL.jump_synth oIDFilter'_jumper synth_oIDFilter ()
module MiTLS.Parsers.OIDFilter

(* 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
module LT = LowParse.TacLib
module LS = LowParse.SLow
module LSZ = LowParse.SLow
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' --z3rlimit 16 --z3cliopt smt.arith.nl=false --max_fuel 2 --max_ifuel 2"

(* Type of field certificate_extension_oid*)
open MiTLS.Parsers.OIDFilter_certificate_extension_oid

(* Type of field certificate_extension_values*)
open MiTLS.Parsers.OIDFilter_certificate_extension_values

type oIDFilter' = (oIDFilter_certificate_extension_oid & oIDFilter_certificate_extension_values)

inline_for_extraction let synth_oIDFilter (x: oIDFilter') : oIDFilter =
  match x with (certificate_extension_oid,certificate_extension_values) -> {
    certificate_extension_oid = certificate_extension_oid;
    certificate_extension_values = certificate_extension_values;
  }

inline_for_extraction let synth_oIDFilter_recip (x: oIDFilter) : oIDFilter' = (x.certificate_extension_oid,x.certificate_extension_values)

let synth_oIDFilter_recip_inverse () : Lemma (LP.synth_inverse synth_oIDFilter_recip synth_oIDFilter) = ()

let synth_oIDFilter_injective () : Lemma (LP.synth_injective synth_oIDFilter) =
  LP.synth_inverse_synth_injective synth_oIDFilter_recip synth_oIDFilter;
  synth_oIDFilter_recip_inverse ()

let synth_oIDFilter_inverse () : Lemma (LP.synth_inverse synth_oIDFilter synth_oIDFilter_recip) =
  assert_norm (LP.synth_inverse synth_oIDFilter synth_oIDFilter_recip)

let synth_oIDFilter_recip_injective () : Lemma (LP.synth_injective synth_oIDFilter_recip) =
  synth_oIDFilter_recip_inverse ();
  LP.synth_inverse_synth_injective synth_oIDFilter synth_oIDFilter_recip

noextract let oIDFilter'_parser : LP.parser _ oIDFilter' = (oIDFilter_certificate_extension_oid_parser `LP.nondep_then` oIDFilter_certificate_extension_values_parser)

noextract let oIDFilter'_parser_kind = LP.get_parser_kind oIDFilter'_parser

let oIDFilter_parser =
  synth_oIDFilter_injective ();
  assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind);
  oIDFilter'_parser `LP.parse_synth` synth_oIDFilter

noextract let oIDFilter'_serializer : LP.serializer oIDFilter'_parser = (oIDFilter_certificate_extension_oid_serializer `LP.serialize_nondep_then` oIDFilter_certificate_extension_values_serializer)

let oIDFilter_serializer =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = synth_oIDFilter_inverse () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LP.serialize_synth _ synth_oIDFilter oIDFilter'_serializer synth_oIDFilter_recip ()

let oIDFilter_bytesize (x:oIDFilter) : GTot nat = Seq.length (oIDFilter_serializer x)

let oIDFilter_bytesize_eq x = ()

inline_for_extraction let oIDFilter'_parser32 : LS.parser32 oIDFilter'_parser = (oIDFilter_certificate_extension_oid_parser32 `LS.parse32_nondep_then` oIDFilter_certificate_extension_values_parser32)

let oIDFilter_parser32 =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LS.parse32_synth _ synth_oIDFilter (fun x -> synth_oIDFilter x) oIDFilter'_parser32 ()

inline_for_extraction let oIDFilter'_serializer32 : LS.serializer32 oIDFilter'_serializer = (oIDFilter_certificate_extension_oid_serializer32 `LS.serialize32_nondep_then` oIDFilter_certificate_extension_values_serializer32)

let oIDFilter_serializer32 =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = synth_oIDFilter_inverse () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LS.serialize32_synth _ synth_oIDFilter _ oIDFilter'_serializer32 synth_oIDFilter_recip (fun x -> synth_oIDFilter_recip x) ()

inline_for_extraction let oIDFilter'_size32 : LSZ.size32 oIDFilter'_serializer = (oIDFilter_certificate_extension_oid_size32 `LSZ.size32_nondep_then` oIDFilter_certificate_extension_values_size32)

let oIDFilter_size32 =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = synth_oIDFilter_inverse () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LSZ.size32_synth _ synth_oIDFilter _ oIDFilter'_size32 synth_oIDFilter_recip (fun x -> synth_oIDFilter_recip x) ()

inline_for_extraction let oIDFilter'_validator : LL.validator oIDFilter'_parser = (oIDFilter_certificate_extension_oid_validator `LL.validate_nondep_then` oIDFilter_certificate_extension_values_validator)

let oIDFilter_validator =
  [@inline_let] let _ = synth_oIDFilter_injective () in
  [@inline_let] let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
  LL.validate_synth oIDFilter'_validator synth_oIDFilter ()

inline_for_extraction let oIDFilter'_jumper : LL.jumper oIDFilter'_parser = (oIDFilter_certificate_extension_oid_jumper `LL.jump_nondep_then` oIDFilter_certificate_extension_values_jumper)
/
prims.fst.checked MiTLS.Parsers.OIDFilter_certificate_extension_values.fsti.checked MiTLS.Parsers.OIDFilter_certificate_extension_oid.fsti.checked LowStar.Buffer.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.AllIntegers.fst.checked LowParse.Spec.fst.checked LowParse.SLow.fst.checked LowParse.Low.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parsers.OIDFilter.fst
LowParse.Low.Base.jumper MiTLS.Parsers.OIDFilter.oIDFilter_parser
LowParse.Low.Combinators.jump_synth LowParse.Spec.Combinators.and_then_kind MiTLS.Parsers.OIDFilter_certificate_extension_oid.oIDFilter_certificate_extension_oid_parser_kind MiTLS.Parsers.OIDFilter_certificate_extension_values.oIDFilter_certificate_extension_values_parser_kind MiTLS.Parsers.OIDFilter.oIDFilter' MiTLS.Parsers.OIDFilter.oIDFilter MiTLS.Parsers.OIDFilter.oIDFilter'_parser MiTLS.Parsers.OIDFilter.oIDFilter'_jumper MiTLS.Parsers.OIDFilter.synth_oIDFilter Prims.unit FStar.Pervasives.assert_norm Prims.eq2 LowParse.Spec.Base.parser_kind MiTLS.Parsers.OIDFilter.oIDFilter_parser_kind MiTLS.Parsers.OIDFilter.oIDFilter'_parser_kind MiTLS.Parsers.OIDFilter.synth_oIDFilter_injective
let oIDFilter_jumper =
  
[@@ inline_let ]let _ = synth_oIDFilter_injective () in
[@@ inline_let ]let _ = assert_norm (oIDFilter_parser_kind == oIDFilter'_parser_kind) in
LL.jump_synth oIDFilter'_jumper synth_oIDFilter ()