val len_of_aliasKeyTBS_extensions (version: datatype_of_asn1_type INTEGER)
    : Tot (asn1_TLV_int32_of_type SEQUENCE)
val len_of_aliasKeyTBS_extensions (version: datatype_of_asn1_type INTEGER)
    : Tot (asn1_TLV_int32_of_type SEQUENCE)
let len_of_aliasKeyTBS_extensions
  (version: datatype_of_asn1_type INTEGER)
: Tot (asn1_TLV_int32_of_type SEQUENCE)
= //lemma_aliasKeyTBS_extensions_ingredients_valid version;
  len_of_TLV SEQUENCE
    (len_of_aliasKeyTBS_extensions_payload version)
module L0.X509.AliasKeyTBS.Extensions

open ASN1.Spec
open ASN1.Low
open X509
open L0.X509.Base
open L0.X509.FWID
open L0.X509.CompositeDeviceID
open L0.X509.Extension
open L0.X509.AliasKeyTBS.Extensions.BasicConstraints
open L0.X509.AliasKeyTBS.Extensions.AuthKeyIdentifier
open L0.X509.AliasKeyTBS.Extensions.ExtendedKeyUsage
open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 128 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

val decl : unit

(* Extensions of the AliasKey Certificate
 * Includes the L0 Extension (`CompositeDeviceID`) and others
 * This is the SEQUENCE under the outmost explicit tag
 * Contains SEQUENCEs of individual extensions ({extID, extValue})
 * [3] {               <--- The outmost explicit tag
 *   SEQUENCE {        <--- *HERE*
 *     SEQUENCE {      <--- Individual extension
 *       extID   : OID
 *       extValue: OCTET STRING {..}  <--- Actual extension content enveloped by tag OCTET STRING
 *     };
 *     SEQUENCE {..};
 *     SEQUENCE {..};  <--- Other extensions
 *   }
 * }
 *)

noeq
type aliasKeyTBS_extensions_payload_t = {
  (* More extensions could be added here.
   * For example:
   * aliasKeyTBS_extensions_key_usage: key_usage_t;
   *)
  aliasKeyTBS_extensions_key_usage: key_usage_t;
  aliasKeyTBS_extensions_extendedKeyUsage: aliasKeyTBS_extensions_extendedKeyUsage_t;
                                           //P.norm
                                           // (norm_steps_x509_keyPurposeIDs (`%aliasKeyCrt_extendedKeyUsage_oids))
                                           // (x509_ext_key_usage_t aliasKeyCrt_extendedKeyUsage_oids);
  aliasKeyTBS_extensions_basicConstraints: aliasKeyTBS_extensions_basicConstraints_t;
  aliasKeyTBS_extensions_authKeyID: aliasKeyTBS_extensions_authKeyID_t;
  aliasKeyTBS_extensions_l0: l0_extension_t
}

noextract
let parse_aliasKeyTBS_extensions_payload_kind
: parser_kind
= parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  parse_x509_extension_sequence_TLV_kind

(* Parser Specification for VALUE *)
noextract
val parse_aliasKeyTBS_extensions_payload
: parser parse_aliasKeyTBS_extensions_payload_kind (aliasKeyTBS_extensions_payload_t)

(* Serializer Specification for VALUE *)
noextract
val serialize_aliasKeyTBS_extensions_payload
: serializer (parse_aliasKeyTBS_extensions_payload)

(* Lemmas for serialization *)
val lemma_serialize_aliasKeyTBS_extensions_payload_unfold
  (x: aliasKeyTBS_extensions_payload_t)
: Lemma (
  serialize_aliasKeyTBS_extensions_payload `serialize` x ==
  (serialize_x509_key_usage `serialize` x.aliasKeyTBS_extensions_key_usage)
  `Seq.append`
  (serialize_aliasKeyTBS_extensions_extendedKeyUsage
                            `serialize` x.aliasKeyTBS_extensions_extendedKeyUsage)
  `Seq.append`
  (serialize_aliasKeyTBS_extensions_basicConstraints
                            `serialize` x.aliasKeyTBS_extensions_basicConstraints)
  `Seq.append`
  (serialize_aliasKeyTBS_extensions_authKeyID
                            `serialize` x.aliasKeyTBS_extensions_authKeyID)
  `Seq.append`
  (serialize_l0_extension `serialize` x.aliasKeyTBS_extensions_l0)
)

// let valid_aliasKeyTBS_extensions_payload_ingredients
//   (version: datatype_of_asn1_type INTEGER)
// : Type0
// = v (len_of_x509_key_usage ()) +
//   length_of_aliasKeyTBS_extensions_extendedKeyUsage () +
//   length_of_aliasKeyTBS_extensions_basicConstraints () +
//   length_of_aliasKeyTBS_extensions_authKeyID () +
//   length_of_l0_extension version
//   <= asn1_value_length_max_of_type SEQUENCE

// val lemma_aliasKeyTBS_extensions_payload_ingredients_valid
//   (version: datatype_of_asn1_type INTEGER)
// : Lemma (
//   valid_aliasKeyTBS_extensions_payload_ingredients version
// )

noextract inline_for_extraction unfold
[@@ "opaque_to_smt"]
let len_of_aliasKeyTBS_extensions_payload_max ()
: Tot (asn1_value_int32_of_type SEQUENCE)
= len_of_x509_key_usage () +
  len_of_aliasKeyTBS_extensions_extendedKeyUsage () +
  len_of_aliasKeyTBS_extensions_basicConstraints () +
  len_of_aliasKeyTBS_extensions_authKeyID () +
  len_of_l0_extension_max ()

let len_of_aliasKeyTBS_extensions_payload
  (version: datatype_of_asn1_type INTEGER)
: Tot (asn1_value_int32_of_type SEQUENCE)
= //lemma_aliasKeyTBS_extensions_payload_ingredients_valid version;
  len_of_x509_key_usage () +
  len_of_aliasKeyTBS_extensions_extendedKeyUsage () +
  len_of_aliasKeyTBS_extensions_basicConstraints () +
  len_of_aliasKeyTBS_extensions_authKeyID () +
  len_of_l0_extension version

let lemma_length_of_aliasKeyTBS_extensions_payload_size_max
  (version: datatype_of_asn1_type INTEGER)
: Lemma (
  v (len_of_aliasKeyTBS_extensions_payload version)
  <= v (len_of_aliasKeyTBS_extensions_payload_max ())
)
= ()

val lemma_serialize_aliasKeyTBS_extensions_payload_size
  (x: aliasKeyTBS_extensions_payload_t)
: Lemma (
  (* unfold *)
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_payload)      x ==
  length_of_opaque_serialization (serialize_x509_key_usage)              x.aliasKeyTBS_extensions_key_usage +
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_extendedKeyUsage)
                                                                         x.aliasKeyTBS_extensions_extendedKeyUsage +
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_basicConstraints)
                                                                         x.aliasKeyTBS_extensions_basicConstraints +
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_authKeyID)
                                                                         x.aliasKeyTBS_extensions_authKeyID +
  length_of_opaque_serialization (serialize_l0_extension)              x.aliasKeyTBS_extensions_l0 /\
  (* exact size *)
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_payload)      x
  == v (len_of_aliasKeyTBS_extensions_payload
         (x.aliasKeyTBS_extensions_l0.x509_extValue_l0.l0_version)) /\
  length_of_opaque_serialization (serialize_aliasKeyTBS_extensions_payload)      x
  <= v (len_of_aliasKeyTBS_extensions_payload_max ())
)
// = lemma_length_of_aliasKeyTBS_extensions_payload_size_max x.aliasKeyTBS_extensions_l0.x509_extValue_l0.l0_version;
//   lemma_serialize_aliasKeyTBS_extensions_payload_unfold x;
//     lemma_serialize_x509_key_usage_size_exact x.aliasKeyTBS_extensions_key_usage;
//     lemma_x509_keyPurposeIDs_unique aliasKeyCrt_extendedKeyUsage_oids;
//     lemma_serialize_aliasKeyTBS_extensions_extendedKeyUsage_size_exact
//                                               x.aliasKeyTBS_extensions_extendedKeyUsage;
//     lemma_serialize_aliasKeyTBS_extensions_basicConstraints_size_exact
//                                               x.aliasKeyTBS_extensions_basicConstraints;
//     lemma_serialize_aliasKeyTBS_extensions_authKeyID_size_exact
//                                               x.aliasKeyTBS_extensions_authKeyID;
//     lemma_serialize_l0_extension_size_exact x.aliasKeyTBS_extensions_l0

(*
 * SEQUENCE serializer
 *)
(* aliasKeyTBS_extensions: inbound sub type for SEQUENCE TLV*)
let aliasKeyTBS_extensions_t
= inbound_sequence_value_of (serialize_aliasKeyTBS_extensions_payload)

(* aliasKeyTBS_extensions: parser for TLV *)
noextract
let parse_aliasKeyTBS_extensions
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) (aliasKeyTBS_extensions_t)
= aliasKeyTBS_extensions_t
  `coerce_parser`
  parse_asn1_sequence_TLV (serialize_aliasKeyTBS_extensions_payload)

(* aliasKeyTBS_extensions: serializer for TLV *)
noextract
let serialize_aliasKeyTBS_extensions
: serializer (parse_aliasKeyTBS_extensions)
= coerce_parser_serializer
  (* t *) (parse_aliasKeyTBS_extensions)
  (* s *) (serialize_asn1_sequence_TLV (serialize_aliasKeyTBS_extensions_payload))
  (*prf*) ()

(* aliasKeyTBS_extensions: lemmas for TLV *)
val lemma_serialize_aliasKeyTBS_extensions_unfold
  (x: aliasKeyTBS_extensions_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_unfold serialize_aliasKeyTBS_extensions_payload x )

val lemma_serialize_aliasKeyTBS_extensions_size
  (x: aliasKeyTBS_extensions_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size serialize_aliasKeyTBS_extensions_payload x )

// let valid_aliasKeyTBS_extensions_ingredients
//   (version: datatype_of_asn1_type INTEGER)
// : Type0
// = valid_aliasKeyTBS_extensions_payload_ingredients version /\
//   v (len_of_aliasKeyTBS_extensions_payload version)
//   <= asn1_value_length_max_of_type SEQUENCE

// val lemma_aliasKeyTBS_extensions_ingredients_valid
//   (version: datatype_of_asn1_type INTEGER)
// : Lemma (
//   valid_aliasKeyTBS_extensions_ingredients version
// )

// let valid_aliasKeyTBS_extensions
//   (x: aliasKeyTBS_extensions_t)
// : Type0
// = valid_aliasKeyTBS_extensions_ingredients
//           (x.aliasKeyTBS_extensions_l0.x509_extValue_l0.l0_version)

// val lemma_aliasKeyTBS_extensions_valid
//   (x: aliasKeyTBS_extensions_t)
// : Lemma (
//   valid_aliasKeyTBS_extensions x
// )

noextract inline_for_extraction unfold
[@@ "opaque_to_smt"]
let len_of_aliasKeyTBS_extensions_max ()
: Tot (asn1_TLV_int32_of_type SEQUENCE)
= SEQUENCE `len_of_TLV`
  (**) (len_of_aliasKeyTBS_extensions_payload_max ())
/
X509.BasicFields.Extension2.fsti.checked X509.fst.checked prims.fst.checked L0.X509.FWID.fsti.checked L0.X509.Extension.fst.checked L0.X509.CompositeDeviceID.fsti.checked L0.X509.Base.fst.checked L0.X509.AliasKeyTBS.Extensions.ExtendedKeyUsage.fst.checked L0.X509.AliasKeyTBS.Extensions.BasicConstraints.fst.checked L0.X509.AliasKeyTBS.Extensions.AuthKeyIdentifier.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
L0.X509.AliasKeyTBS.Extensions.fsti
version: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER
  -> ASN1.Base.asn1_TLV_int32_of_type ASN1.Base.SEQUENCE
ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER ASN1.Low.TLV.len_of_TLV ASN1.Base.SEQUENCE L0.X509.AliasKeyTBS.Extensions.len_of_aliasKeyTBS_extensions_payload ASN1.Base.asn1_TLV_int32_of_type
let len_of_aliasKeyTBS_extensions (version: datatype_of_asn1_type INTEGER)
    : Tot (asn1_TLV_int32_of_type SEQUENCE) =
  
len_of_TLV SEQUENCE (len_of_aliasKeyTBS_extensions_payload version)