val parse_x509_validity_payload_kind:parser_kind
val parse_x509_validity_payload_kind:parser_kind
let parse_x509_validity_payload_kind
: parser_kind
= parse_asn1_TLV_kind_of_type UTC_TIME
  `and_then_kind`
  parse_asn1_TLV_kind_of_type Generalized_Time
module X509.BasicFields.Validity

open LowParse.Low.Base

open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

(*
 4.1.2.5.  Validity

   The certificate validity period is the time interval during which the
   CA warrants that it will maintain information about the status of the
   certificate.  The field is represented as a SEQUENCE of two dates:
   the date on which the certificate validity period begins (notBefore)
   and the date on which the certificate validity period ends
   (notAfter).  Both notBefore and notAfter may be encoded as UTCTime or
   GeneralizedTime.

   CAs conforming to this profile MUST always encode certificate
   validity dates through the year 2049 as UTCTime; certificate validity
   dates in 2050 or later MUST be encoded as GeneralizedTime.
   Conforming applications MUST be able to process validity dates that
   are encoded in either UTCTime or GeneralizedTime.

   The validity period for a certificate is the period of time from
   notBefore through notAfter, inclusive.

   In some situations, devices are given certificates for which no good
   expiration date can be assigned.  For example, a device could be
   issued a certificate that binds its model and serial number to its
   public key; such a certificate is intended to be used for the entire
   lifetime of the device.

   To indicate that a certificate has no well-defined expiration date,
   the notAfter SHOULD be assigned the GeneralizedTime value of
   99991231235959Z.
*)

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

module HS = FStar.HyperStack
module IB = LowStar.ImmutableBuffer

let x509_validity_notBefore_default_buffer
: b: IB.libuffer byte 13 asn1_utc_time_for_x509_validity_notBefore_default_seq
  { IB.frameOf b == HS.root /\
    IB.recallable b }
= IB.igcmalloc_of_list HS.root (asn1_utc_time_for_x509_validity_notBefore_default_list)

val x509_validity_notAfter_default_buffer
: b: IB.libuffer byte 15 asn1_generalized_time_for_x509_validity_notAfter_default_seq
  { IB.frameOf b == HS.root /\
    IB.recallable b }

type x509_validity_payload_t: Type = {
  notBefore: utc_time_t;
  notAfter: generalized_time_t
}
/
X509.Base.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.Validity.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Combinators.and_then_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.UTC_TIME ASN1.Base.Generalized_Time
let parse_x509_validity_payload_kind:parser_kind =
  
(parse_asn1_TLV_kind_of_type UTC_TIME)
`and_then_kind`
(parse_asn1_TLV_kind_of_type Generalized_Time)