val serialize_x509_keyPurposeIDs (oids: keyPurposeIDs_oids_t)
    : Tot (serializer (parse_x509_keyPurposeIDs oids)) (decreases (List.length oids))
val serialize_x509_keyPurposeIDs (oids: keyPurposeIDs_oids_t)
    : Tot (serializer (parse_x509_keyPurposeIDs oids)) (decreases (List.length oids))
let rec serialize_x509_keyPurposeIDs
  (oids: keyPurposeIDs_oids_t)
: Tot (serializer (parse_x509_keyPurposeIDs oids))
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( serialize_asn1_oid_TLV_of oid )
  | _  -> ( serialize_x509_keyPurposeIDs oids'
            `serialize_nondep_then`
            serialize_asn1_oid_TLV_of oid )
module X509.ExtFields.ExtendedKeyUsage

open LowParse.Spec.Base
open LowParse.Spec.Combinators

open ASN1.Base
open ASN1.Spec
open ASN1.Low

open X509.Base
open FStar.Integers
module B32 = FStar.Bytes

module T = FStar.Tactics
module P = FStar.Pervasives

(*
 * AR: TODO: this module has some scope for improvements
             it's hard to write an interface to hide defns, since a tactic requires those defns, I think *)

#set-options "--z3rlimit 32 --fuel 2 --ifuel 0"

(*
 * KeyPurposeIDs
 *)

noextract unfold
let valid_keyPurposeIDs
  (oids: list (datatype_of_asn1_type OID))
: Type0
= 0 < List.length oids /\ (List.length oids) < 10

let keyPurposeIDs_oids_t
: Type
= oids: list (datatype_of_asn1_type OID) { valid_keyPurposeIDs oids }

noextract inline_for_extraction
let rec x509_keyPurposeIDs_t
  (oids: keyPurposeIDs_oids_t)
: Tot (Type0)
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( get_parser_type (parse_asn1_oid_TLV_of oid) )
  | _  -> ( x509_keyPurposeIDs_t oids'
            `tuple2`
            get_parser_type (parse_asn1_oid_TLV_of oid) )

let lemma_x509_keyPurposeIDs_unique
  (oids: keyPurposeIDs_oids_t)
: Lemma
  (ensures forall (x1: x509_keyPurposeIDs_t oids)
             (x2: x509_keyPurposeIDs_t oids).
               x1 == x2 )
= let rec lemma_x509_keyPurposeIDs_unique_prf
    (oids: keyPurposeIDs_oids_t)
    (x1 x2: x509_keyPurposeIDs_t oids)
  : Lemma
    (ensures x1 == x2 )
    (decreases (List.length oids))
  = let oids', oid = List.Tot.Base.unsnoc oids in
    List.Tot.Properties.lemma_unsnoc_length oids;
    match oids' with
    | [] -> ( () )
    | _  -> ( let x1 = x1 <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
              let x2 = x2 <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
              assert ( snd x1 == snd x2 );
              lemma_x509_keyPurposeIDs_unique_prf oids' (fst x1) (fst x2) ) in
  Classical.forall_intro_2 (lemma_x509_keyPurposeIDs_unique_prf oids)

noextract inline_for_extraction
let rec get_x509_keyPurposeIDs
  (oids: keyPurposeIDs_oids_t)
: Tot (x509_keyPurposeIDs_t oids)
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( oid )
  | _  -> ( (get_x509_keyPurposeIDs oids', oid)
             <: x509_keyPurposeIDs_t oids'
                `tuple2`
                get_parser_type (parse_asn1_oid_TLV_of oid) )

let rec parse_x509_keyPurposeIDs_kind
  (oids: keyPurposeIDs_oids_t)
: Tot (k: parser_kind { Mkparser_kind'?.parser_kind_subkind k == Some ParserStrong })
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( get_parser_kind (parse_asn1_oid_TLV_of oid) )
  | _  -> ( parse_x509_keyPurposeIDs_kind oids'
            `and_then_kind`
            get_parser_kind (parse_asn1_oid_TLV_of oid) )
let rec parse_x509_keyPurposeIDs
  (oids: keyPurposeIDs_oids_t)
: Tot (parser (parse_x509_keyPurposeIDs_kind oids) (x509_keyPurposeIDs_t oids))
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( parse_asn1_oid_TLV_of oid )
  | _  -> ( parse_x509_keyPurposeIDs oids'
            `nondep_then`
/
X509.BasicFields.Extension2.fsti.checked X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.fst.checked FStar.Integers.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.ExtFields.ExtendedKeyUsage.fst
oids: X509.ExtFields.ExtendedKeyUsage.keyPurposeIDs_oids_t
  -> Prims.Tot
    (LowParse.Spec.Base.serializer (X509.ExtFields.ExtendedKeyUsage.parse_x509_keyPurposeIDs oids))
X509.ExtFields.ExtendedKeyUsage.keyPurposeIDs_oids_t Prims.list ASN1.Base.datatype_of_asn1_type ASN1.Base.OID ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of LowParse.Spec.Combinators.serialize_nondep_then X509.ExtFields.ExtendedKeyUsage.parse_x509_keyPurposeIDs_kind X509.ExtFields.ExtendedKeyUsage.x509_keyPurposeIDs_t X509.ExtFields.ExtendedKeyUsage.parse_x509_keyPurposeIDs X509.ExtFields.ExtendedKeyUsage.serialize_x509_keyPurposeIDs LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.Value.OID.the_asn1_oid ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of LowParse.Spec.Base.serializer Prims.unit FStar.List.Tot.Properties.lemma_unsnoc_length FStar.Pervasives.Native.tuple2 FStar.List.Tot.Base.unsnoc
let rec serialize_x509_keyPurposeIDs (oids: keyPurposeIDs_oids_t)
    : Tot (serializer (parse_x509_keyPurposeIDs oids)) (decreases (List.length oids)) =
  
let oids', oid = List.Tot.Base.unsnoc oids in
List.Tot.Properties.lemma_unsnoc_length oids;
match oids' with
| [] -> (serialize_asn1_oid_TLV_of oid)
| _ ->
  ((serialize_x509_keyPurposeIDs oids') `serialize_nondep_then` (serialize_asn1_oid_TLV_of oid))