val parse_x509_ext_key_usage (oids: keyPurposeIDs_oids_t)
    : parser parse_x509_extension_kind (x509_ext_key_usage_t oids)
val parse_x509_ext_key_usage (oids: keyPurposeIDs_oids_t)
    : parser parse_x509_extension_kind (x509_ext_key_usage_t oids)
let parse_x509_ext_key_usage
  (oids: keyPurposeIDs_oids_t)
: parser parse_x509_extension_kind (x509_ext_key_usage_t oids)
= x509_ext_key_usage_t oids
  `coerce_parser`
  parse_x509_extension
  (**) (OID_EXTENDED_KEY_USAGE)
  (**) (serialize_x509_ext_key_usage_payload oids)
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`
            parse_asn1_oid_TLV_of oid )
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 )
noextract
let rec serialize32_x509_keyPurposeIDs_backwards
  (oids: keyPurposeIDs_oids_t)
: Tot (serializer32_backwards (serialize_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
  | [] -> ( serialize32_asn1_oid_TLV_of_backwards oid )
  | _  -> ( serialize32_x509_keyPurposeIDs_backwards oids'
            `serialize32_nondep_then_backwards`
            serialize32_asn1_oid_TLV_of_backwards oid )
// [@@T.postprocess_with postprocess_listops]
let rec serialize_x509_keyPurposeIDs_unfold_spec
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: GTot (_)
  (decreases (List.length oids))
= let x = get_x509_keyPurposeIDs oids in
  let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( serialize (serialize_asn1_oid_TLV_of oid) x )
  | _  -> ( let x = x <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            serialize_x509_keyPurposeIDs_unfold_spec oids'
            `Seq.append`
            serialize (serialize_asn1_oid_TLV_of oid) (snd x) )
// [@@T.postprocess_with postprocess_listops]
let rec lemma_serialize_x509_keyPurposeIDs_unfold
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: Lemma (ensures
  serialize (serialize_x509_keyPurposeIDs oids) (get_x509_keyPurposeIDs oids) ==
  serialize_x509_keyPurposeIDs_unfold_spec oids
)
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ()
  | _  -> ( let x = (get_x509_keyPurposeIDs oids)
                     <: x509_keyPurposeIDs_t oids' `tuple2`
                        get_parser_type (parse_asn1_oid_TLV_of oid) in
            serialize_nondep_then_eq
            (* s1 *) (serialize_x509_keyPurposeIDs oids')
            (* s2 *) (serialize_asn1_oid_TLV_of oid)
            (* in *) x;
            lemma_serialize_x509_keyPurposeIDs_unfold oids' )
(*
 * Reveals the structure and size of all oids
 * Use with fuels or `lemma_serialize_x509_keyPurposeIDs_size_norm` (defined later)
 *)
let rec predicate_serialize_x509_keyPurposeIDs_size_oids
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: GTot (Type0)
  (decreases (List.length oids))
= lemma_serialize_x509_keyPurposeIDs_unfold oids;
  let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( length_of_opaque_serialization (serialize_asn1_oid_TLV_of (get_x509_keyPurposeIDs oids)) (get_x509_keyPurposeIDs oids) ==
            length_of_TLV OID (length_of_oid (get_x509_keyPurposeIDs oids)) )
  | _  -> ( let x = (get_x509_keyPurposeIDs oids) <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            length_of_opaque_serialization (serialize_asn1_oid_TLV_of (snd x)) (snd x) ==
            length_of_TLV OID (length_of_oid (snd x)) /\
            predicate_serialize_x509_keyPurposeIDs_size_oids oids' )
let rec serialize_x509_keyPurposeIDs_size_spec
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: GTot (nat)
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( length_of_opaque_serialization (serialize_asn1_oid_TLV_of oid) (get_x509_keyPurposeIDs oids) )
  | _  -> ( let x = (get_x509_keyPurposeIDs oids) <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            serialize_x509_keyPurposeIDs_size_spec oids' +
            length_of_opaque_serialization (serialize_asn1_oid_TLV_of (snd x)) (snd x) )
let rec lemma_serialize_x509_keyPurposeIDs_size
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: Lemma (ensures
  length_of_opaque_serialization (serialize_x509_keyPurposeIDs oids) (get_x509_keyPurposeIDs oids) ==
  serialize_x509_keyPurposeIDs_size_spec oids /\
  predicate_serialize_x509_keyPurposeIDs_size_oids oids
)
  (decreases (List.length oids))
= lemma_serialize_x509_keyPurposeIDs_unfold oids;
  let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  match oids' with
  | [] -> ( lemma_serialize_asn1_oid_TLV_of_size (get_x509_keyPurposeIDs oids) (get_x509_keyPurposeIDs oids) )
  | _  -> ( let x = (get_x509_keyPurposeIDs oids) <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            lemma_serialize_asn1_oid_TLV_of_size (snd x) (snd x);
            lemma_serialize_x509_keyPurposeIDs_unfold oids';
            lemma_serialize_x509_keyPurposeIDs_size   oids' )
let valid_x509_ext_keyPurposeIDs_ingredients
  (oids: keyPurposeIDs_oids_t)
  // (x: x509_keyPurposeIDs_t oids)
: Type0
= serialize_x509_keyPurposeIDs_size_spec oids // (get_x509_keyPurposeIDs oids)
  <= asn1_value_length_max_of_type SEQUENCE
let rec length_of_x509_keyPurposeIDs
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_keyPurposeIDs_ingredients oids })
  // (x: x509_keyPurposeIDs_t oids
  //     { valid_x509_ext_keyPurposeIDs_ingredients oids x })
: GTot (l: asn1_value_length_of_type SEQUENCE
           { l == serialize_x509_keyPurposeIDs_size_spec oids })
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  lemma_serialize_x509_keyPurposeIDs_size oids;
  match oids' with
  | [] -> ( length_of_asn1_primitive_TLV #OID (get_x509_keyPurposeIDs oids) )
  | _  -> ( let x = (get_x509_keyPurposeIDs oids) <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            lemma_serialize_x509_keyPurposeIDs_size oids';
            length_of_x509_keyPurposeIDs oids' +
            length_of_asn1_primitive_TLV #OID (snd x) )
noextract
let rec len_of_x509_keyPurposeIDs
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_keyPurposeIDs_ingredients oids })
  // (x: x509_keyPurposeIDs_t oids
  //     { valid_x509_ext_keyPurposeIDs_ingredients oids x })
: Tot (len: asn1_value_int32_of_type SEQUENCE
           { v len == length_of_x509_keyPurposeIDs oids })
  (decreases (List.length oids))
= let oids', oid = List.Tot.Base.unsnoc oids in
  List.Tot.Properties.lemma_unsnoc_length oids;
  lemma_serialize_x509_keyPurposeIDs_size oids;
  match oids' with
  | [] -> ( len_of_asn1_primitive_TLV #OID (get_x509_keyPurposeIDs oids) )
  | _  -> ( let x = (get_x509_keyPurposeIDs oids) <: x509_keyPurposeIDs_t oids' `tuple2` get_parser_type (parse_asn1_oid_TLV_of oid) in
            lemma_serialize_x509_keyPurposeIDs_size oids';
            len_of_x509_keyPurposeIDs oids' +
            len_of_asn1_primitive_TLV #OID (snd x) )
(*
 * Payload
 *)
open X509.BasicFields.Extension2
unfold inline_for_extraction
let x509_ext_key_usage_payload_t
  (oids: keyPurposeIDs_oids_t)
= inbound_sequence_value_of
  (**) (serialize_x509_keyPurposeIDs oids)
let parse_x509_ext_key_usage_payload
  (oids: keyPurposeIDs_oids_t)
: parser _ (x509_ext_key_usage_payload_t oids)
= x509_ext_key_usage_payload_t oids
  `coerce_parser`
  parse_asn1_sequence_TLV
  (**) (serialize_x509_keyPurposeIDs oids)
let serialize_x509_ext_key_usage_payload
  (oids: keyPurposeIDs_oids_t)
: serializer (parse_x509_ext_key_usage_payload oids)
= coerce_parser_serializer
    (_)
    (serialize_asn1_sequence_TLV
    (**) (serialize_x509_keyPurposeIDs oids))
    ()
noextract inline_for_extraction
let serialize32_x509_ext_key_usage_payload_backwards
  (oids: keyPurposeIDs_oids_t)
: serializer32_backwards (serialize_x509_ext_key_usage_payload oids)
= coerce_serializer32_backwards
    (_)
    (serialize32_asn1_sequence_TLV_backwards
    (**) (serialize32_x509_keyPurposeIDs_backwards oids))
    ()
let lemma_serialize_x509_ext_key_usage_payload_unfold
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_keyPurposeIDs_ingredients oids })
  // (x: x509_ext_key_usage_payload_t oids)
: Lemma (
  lemma_serialize_x509_keyPurposeIDs_size oids;
  predicate_serialize_asn1_sequence_TLV_unfold
  (**) (serialize_x509_keyPurposeIDs oids)
  (**) (get_x509_keyPurposeIDs oids)
)
= lemma_serialize_x509_keyPurposeIDs_size oids;
  lemma_serialize_asn1_sequence_TLV_unfold
  (**) (serialize_x509_keyPurposeIDs oids)
  (**) (get_x509_keyPurposeIDs oids)
let lemma_serialize_x509_ext_key_usage_payload_size
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_keyPurposeIDs_ingredients oids })
  // (x: x509_ext_key_usage_payload_t oids)
: Lemma (
  lemma_serialize_x509_keyPurposeIDs_size oids;
  predicate_serialize_asn1_sequence_TLV_size
  (**) (serialize_x509_keyPurposeIDs oids)
  (**) (get_x509_keyPurposeIDs oids)
)
= lemma_serialize_x509_keyPurposeIDs_size oids;
  lemma_serialize_asn1_sequence_TLV_size
  (**) (serialize_x509_keyPurposeIDs oids)
  (**) (get_x509_keyPurposeIDs oids)
let length_of_x509_ext_key_usage_payload_unbounded
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_keyPurposeIDs_ingredients oids })
: GTot (asn1_TLV_length_of_type SEQUENCE)
= length_of_TLV
    (SEQUENCE)
    (length_of_x509_keyPurposeIDs oids)
let valid_x509_ext_key_usage_payload_ingredients
  (oids: keyPurposeIDs_oids_t)
= valid_x509_ext_keyPurposeIDs_ingredients oids /\
  length_of_x509_ext_key_usage_payload_unbounded oids
  <= asn1_value_length_max_of_type OCTET_STRING
let length_of_x509_ext_key_usage_payload
  (oids: keyPurposeIDs_oids_t
      { valid_x509_ext_key_usage_payload_ingredients oids })
: GTot (l: asn1_value_length_of_type OCTET_STRING
           { l == length_of_x509_ext_key_usage_payload_unbounded oids })
= length_of_TLV
    (SEQUENCE)
    (length_of_x509_keyPurposeIDs oids)
noextract inline_for_extraction
let len_of_x509_ext_key_usage_payload
  (oids: keyPurposeIDs_oids_t
      { valid_x509_ext_key_usage_payload_ingredients oids })
: Tot (len: asn1_value_int32_of_type OCTET_STRING
            { v len == length_of_x509_ext_key_usage_payload oids })
= len_of_TLV
    (SEQUENCE)
    (len_of_x509_keyPurposeIDs oids)
let lemma_serialize_x509_ext_key_usage_payload_size_exact
  (oids: keyPurposeIDs_oids_t
         { valid_x509_ext_key_usage_payload_ingredients oids })
  // (x: x509_ext_key_usage_payload_t oids)
: Lemma (
  lemma_serialize_x509_keyPurposeIDs_size oids;
  length_of_opaque_serialization (serialize_x509_ext_key_usage_payload oids) (get_x509_keyPurposeIDs oids) ==
  length_of_x509_ext_key_usage_payload oids
)
= lemma_serialize_x509_ext_key_usage_payload_unfold oids;
  lemma_serialize_x509_ext_key_usage_payload_size oids;
    lemma_serialize_x509_keyPurposeIDs_size oids
(*
 * Main
 *)
let x509_ext_key_usage_t
  (oids: keyPurposeIDs_oids_t)
= x509_extension_t
  (**) (OID_EXTENDED_KEY_USAGE)
/
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
  -> LowParse.Spec.Base.parser X509.BasicFields.Extension2.parse_x509_extension_kind
      (X509.ExtFields.ExtendedKeyUsage.x509_ext_key_usage_t oids)
X509.ExtFields.ExtendedKeyUsage.keyPurposeIDs_oids_t LowParse.Spec.Base.coerce_parser X509.ExtFields.ExtendedKeyUsage.x509_ext_key_usage_t X509.BasicFields.Extension2.parse_x509_extension_kind X509.BasicFields.Extension2.x509_extension_t ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE X509.ExtFields.ExtendedKeyUsage.x509_ext_key_usage_payload_t X509.ExtFields.ExtendedKeyUsage.parse_x509_ext_key_usage_payload ASN1.Base.OID_EXTENDED_KEY_USAGE X509.ExtFields.ExtendedKeyUsage.serialize_x509_ext_key_usage_payload X509.BasicFields.Extension2.parse_x509_extension LowParse.Spec.Base.parser
let parse_x509_ext_key_usage (oids: keyPurposeIDs_oids_t)
    : parser parse_x509_extension_kind (x509_ext_key_usage_t oids) =
  
(x509_ext_key_usage_t oids)
`coerce_parser`
(parse_x509_extension (OID_EXTENDED_KEY_USAGE) (serialize_x509_ext_key_usage_payload oids))