val create_aliasKeyTBS_spec
      (crt_version: x509_version_t)
      (serialNumber: x509_serialNumber_t)
      (i_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (i_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (i_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (notBefore: datatype_of_asn1_type UTC_TIME)
      (notAfter: datatype_of_asn1_type Generalized_Time)
      (s_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (s_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (s_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (ku: key_usage_payload_t)
      (keyID: lbytes_pub 20)
      (version: datatype_of_asn1_type INTEGER)
      (fwid deviceID_pub aliasKey_pub: lbytes_pub 32)
    : GTot (aliasKeyTBS_t)
val create_aliasKeyTBS_spec
      (crt_version: x509_version_t)
      (serialNumber: x509_serialNumber_t)
      (i_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (i_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (i_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (notBefore: datatype_of_asn1_type UTC_TIME)
      (notAfter: datatype_of_asn1_type Generalized_Time)
      (s_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (s_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (s_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (ku: key_usage_payload_t)
      (keyID: lbytes_pub 20)
      (version: datatype_of_asn1_type INTEGER)
      (fwid deviceID_pub aliasKey_pub: lbytes_pub 32)
    : GTot (aliasKeyTBS_t)
let create_aliasKeyTBS_spec
  (crt_version: x509_version_t)
  (serialNumber: x509_serialNumber_t)
  (i_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
  (i_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
  (i_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
  (notBefore: datatype_of_asn1_type UTC_TIME)
  (notAfter : datatype_of_asn1_type Generalized_Time)
  (s_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
  (s_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
  (s_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
  (ku: key_usage_payload_t)
  (keyID: lbytes_pub 20)
  (version: datatype_of_asn1_type INTEGER)
  (fwid: lbytes_pub 32)
  (deviceID_pub: lbytes_pub 32)
  (aliasKey_pub: lbytes_pub 32)
: GTot (aliasKeyTBS_t)
=
(* Create AliasKeyTBS *)
  let deviceID_pub32: B32.lbytes32 32ul = B32.hide deviceID_pub in
  let fwid32        : B32.lbytes32 32ul = B32.hide fwid in
  let aliasKey_pub32: B32.lbytes32 32ul = B32.hide aliasKey_pub in
  let aliasKeyTBS = x509_get_AliasKeyTBS
                                     crt_version
                                     serialNumber
                                     i_common i_org i_country
                                     notBefore notAfter
                                     s_common s_org s_country
                                     ku
                                     ({ len = 20ul; s = B32.hide keyID })
                                     version
                                     fwid32
                                     deviceID_pub32
                                     aliasKey_pub32 in
  (* Prf *) lemma_serialize_aliasKeyTBS_payload_size aliasKeyTBS;
  (* Prf *) lemma_serialize_aliasKeyTBS_size_exact aliasKeyTBS;

(* return *) aliasKeyTBS
module L0.Spec.Certificate

open ASN1.Spec
open X509

open L0.Base
open L0.Declassify
open L0.X509

open Lib.IntTypes

module B32 = FStar.Bytes

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

(* Create AliasKey To-Be-Signed Certificate
  =======================================
  RFC 5280:
     TBSCertificate  ::=  SEQUENCE  {
        version         [0]  EXPLICIT Version DEFAULT v1,
        serialNumber         CertificateSerialNumber,
        signature            AlgorithmIdentifier,
        issuer               Name,
        validity             Validity,
        subject              Name,
        subjectPublicKeyInfo SubjectPublicKeyInfo,
        issuerUniqueID  [1]  IMPLICIT UniqueIdentifier OPTIONAL,
                             -- If present, version MUST be v2 or v3
        subjectUniqueID [2]  IMPLICIT UniqueIdentifier OPTIONAL,
                             -- If present, version MUST be v2 or v3
        extensions      [3]  EXPLICIT Extensions OPTIONAL
                             -- If present, version MUST be v3
        }
*)

(* A predicate says that the length of created TBS (computed
   from `template_len` and `version`) is valid, i.e., less than
   or equal to 2^32 - 6 *)
// let valid_aliasKeyTBS_ingredients
//   (serialNumber: x509_serialNumber_t)
//   (i_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
//   (i_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
//   (i_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
//   (s_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
//   (s_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
//   (s_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
//   (ku: key_usage_payload_t)
//   (version: datatype_of_asn1_type INTEGER)
// = length_of_aliasKeyTBS_payload
//     serialNumber
//     i_common i_org i_country
//     s_common s_org s_country
//     ku version
//   <= asn1_value_length_max_of_type SEQUENCE
/
X509.fst.checked Spec.Ed25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked L0.X509.fst.checked L0.Declassify.fsti.checked L0.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked
L0.Spec.Certificate.fst

    crt_version: X509.BasicFields.Version.x509_version_t ->
    serialNumber: X509.BasicFields.SerialNumber.x509_serialNumber_t ->
    i_common:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME
        ASN1.Base.IA5_STRING ->
    i_org:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
        ASN1.Base.IA5_STRING ->
    i_country:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COUNTRY
        ASN1.Base.PRINTABLE_STRING ->
    notBefore: ASN1.Base.datatype_of_asn1_type ASN1.Base.UTC_TIME ->
    notAfter: ASN1.Base.datatype_of_asn1_type ASN1.Base.Generalized_Time ->
    s_common:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME
        ASN1.Base.IA5_STRING ->
    s_org:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
        ASN1.Base.IA5_STRING ->
    s_country:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COUNTRY
        ASN1.Base.PRINTABLE_STRING ->
    ku: X509.ExtFields.KeyUsage.key_usage_payload_t ->
    keyID: L0.Base.lbytes_pub 20 ->
    version: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER ->
    fwid: L0.Base.lbytes_pub 32 ->
    deviceID_pub: L0.Base.lbytes_pub 32 ->
    aliasKey_pub: L0.Base.lbytes_pub 32
  -> Prims.GTot L0.X509.AliasKeyTBS.aliasKeyTBS_t
X509.BasicFields.Version.x509_version_t X509.BasicFields.SerialNumber.x509_serialNumber_t X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME ASN1.Base.IA5_STRING X509.BasicFields.RelativeDistinguishedName.ORGANIZATION X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.PRINTABLE_STRING ASN1.Base.datatype_of_asn1_type ASN1.Base.UTC_TIME ASN1.Base.Generalized_Time X509.ExtFields.KeyUsage.key_usage_payload_t L0.Base.lbytes_pub ASN1.Base.INTEGER Prims.unit L0.X509.AliasKeyTBS.lemma_serialize_aliasKeyTBS_size_exact L0.X509.AliasKeyTBS.lemma_serialize_aliasKeyTBS_payload_size L0.X509.AliasKeyTBS.aliasKeyTBS_t L0.X509.AliasKeyTBS.x509_get_AliasKeyTBS ASN1.Base.Mkoctet_string_t FStar.UInt32.__uint_to_t FStar.Bytes.hide FStar.Bytes.lbytes32 FStar.UInt32.uint_to_t FStar.UInt32.t
let create_aliasKeyTBS_spec
      (crt_version: x509_version_t)
      (serialNumber: x509_serialNumber_t)
      (i_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (i_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (i_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (notBefore: datatype_of_asn1_type UTC_TIME)
      (notAfter: datatype_of_asn1_type Generalized_Time)
      (s_common: x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
      (s_org: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
      (s_country: x509_RDN_x520_attribute_string_t COUNTRY PRINTABLE_STRING)
      (ku: key_usage_payload_t)
      (keyID: lbytes_pub 20)
      (version: datatype_of_asn1_type INTEGER)
      (fwid deviceID_pub aliasKey_pub: lbytes_pub 32)
    : GTot (aliasKeyTBS_t) =
  
let deviceID_pub32:B32.lbytes32 32ul = B32.hide deviceID_pub in
let fwid32:B32.lbytes32 32ul = B32.hide fwid in
let aliasKey_pub32:B32.lbytes32 32ul = B32.hide aliasKey_pub in
let aliasKeyTBS =
  x509_get_AliasKeyTBS crt_version serialNumber i_common i_org i_country notBefore notAfter s_common
    s_org s_country ku ({ len = 20ul; s = B32.hide keyID }) version fwid32 deviceID_pub32
    aliasKey_pub32
in
lemma_serialize_aliasKeyTBS_payload_size aliasKeyTBS;
lemma_serialize_aliasKeyTBS_size_exact aliasKeyTBS;
aliasKeyTBS