val serialize32_asn1_generalized_time_backwards
: serializer32_backwards (serialize_asn1_generalized_time)
val serialize32_asn1_generalized_time_backwards
: serializer32_backwards (serialize_asn1_generalized_time)
let serialize32_asn1_generalized_time_backwards
= serialize32_flbytes32_backwards 15ul
  `serialize32_filter_backwards`
  valid_generalized_time
module ASN1.Low.Value.Generalized_Time

open ASN1.Low.Base

open ASN1.Base
open ASN1.Low.Tag
open ASN1.Low.Length
open ASN1.Low.Bytes32
open ASN1.Spec.Value.Generalized_Time

open FStar.Integers

module B32 = FStar.Bytes

friend ASN1.Spec.Value.Generalized_Time

#set-options "--fuel 0 --ifuel 2"
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.Generalized_Time.fst.checked ASN1.Spec.Value.Generalized_Time.fst.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Bytes32.fst.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.Generalized_Time.fst
ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.Generalized_Time.serialize_asn1_generalized_time

ASN1.Low.Base.serialize32_filter_backwards 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.Low.Bytes32.serialize32_flbytes32_backwards ASN1.Base.valid_generalized_time
let serialize32_asn1_generalized_time_backwards =
  
(serialize32_flbytes32_backwards 15ul) `serialize32_filter_backwards` valid_generalized_time