val serialize_asn1_utc_time
: serializer (parse_asn1_utc_time)
val serialize_asn1_utc_time
: serializer (parse_asn1_utc_time)
let serialize_asn1_utc_time
: serializer (parse_asn1_utc_time)
= serialize_flbytes32 13ul
  `serialize_filter`
  valid_utc_time
module ASN1.Spec.Value.UTC_TIME

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Bytes32

open FStar.Integers

module B32 = FStar.Bytes

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

let parse_asn1_utc_time
: parser parse_asn1_utc_time_kind (datatype_of_asn1_type UTC_TIME)
= parse_flbytes32 13ul
  `parse_filter`
  valid_utc_time
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Bytes32.fst.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.UTC_TIME.fst
LowParse.Spec.Base.serializer ASN1.Spec.Value.UTC_TIME.parse_asn1_utc_time
LowParse.Spec.Combinators.serialize_filter LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 FStar.UInt32.__uint_to_t FStar.Bytes.lbytes32 ASN1.Spec.Bytes32.parse_flbytes32 ASN1.Spec.Bytes32.serialize_flbytes32 ASN1.Base.valid_utc_time LowParse.Spec.Base.serializer ASN1.Spec.Value.UTC_TIME.parse_asn1_utc_time_kind ASN1.Base.datatype_of_asn1_type ASN1.Base.UTC_TIME ASN1.Spec.Value.UTC_TIME.parse_asn1_utc_time
let serialize_asn1_utc_time:serializer (parse_asn1_utc_time) =
  
(serialize_flbytes32 13ul) `serialize_filter` valid_utc_time