val 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}
val 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}
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)
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
/
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
b:
(b:
  (b:
    LowStar.Monotonic.Buffer.mbuffer ASN1.Low.Base.byte
      (LowStar.ImmutableBuffer.immutable_preorder ASN1.Low.Base.byte)
      (LowStar.ImmutableBuffer.immutable_preorder ASN1.Low.Base.byte)
      { LowStar.Monotonic.Buffer.length b == 13 /\
        Prims.op_Negation (LowStar.Monotonic.Buffer.g_is_null b) })
    { LowStar.Monotonic.Buffer.witnessed b
        (LowStar.ImmutableBuffer.cpred ASN1.Base.asn1_utc_time_for_x509_validity_notBefore_default_seq
          ) })
  { LowStar.Monotonic.Buffer.frameOf b == FStar.Monotonic.HyperHeap.root /\
    LowStar.Monotonic.Buffer.recallable b }
LowStar.ImmutableBuffer.igcmalloc_of_list ASN1.Base.byte FStar.Monotonic.HyperHeap.root ASN1.Base.asn1_utc_time_for_x509_validity_notBefore_default_list LowStar.ImmutableBuffer.libuffer FStar.Pervasives.normalize_term Prims.nat FStar.List.Tot.Base.length FStar.Seq.Base.seq_of_list Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.ImmutableBuffer.immutable_preorder LowStar.Monotonic.Buffer.recallable
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)