val x509_keyPurposeIDs_t (oids: keyPurposeIDs_oids_t) : Tot (Type0) (decreases (List.length oids))
val x509_keyPurposeIDs_t (oids: keyPurposeIDs_oids_t) : Tot (Type0) (decreases (List.length oids))
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) )
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 }
/
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 Type0
X509.ExtFields.ExtendedKeyUsage.keyPurposeIDs_oids_t Prims.list ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.get_parser_type 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 FStar.Pervasives.Native.tuple2 X509.ExtFields.ExtendedKeyUsage.x509_keyPurposeIDs_t Prims.unit FStar.List.Tot.Properties.lemma_unsnoc_length FStar.List.Tot.Base.unsnoc
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)))