val synth_asn1_oid_V_inverse
      (tag: (the_asn1_tag UTC_TIME) `tuple2` (asn1_value_int32_of_type UTC_TIME))
      (x': refine_with_tag parser_tag_of_utc_time tag)
    : Tot (x: datatype_of_asn1_type UTC_TIME {x' == synth_asn1_oid_V tag x})
val synth_asn1_oid_V_inverse
      (tag: (the_asn1_tag UTC_TIME) `tuple2` (asn1_value_int32_of_type UTC_TIME))
      (x': refine_with_tag parser_tag_of_utc_time tag)
    : Tot (x: datatype_of_asn1_type UTC_TIME {x' == synth_asn1_oid_V tag x})
let synth_asn1_oid_V_inverse
  (tag: the_asn1_tag UTC_TIME `tuple2` asn1_value_int32_of_type UTC_TIME)
  (x': refine_with_tag parser_tag_of_utc_time tag)
: Tot (x: datatype_of_asn1_type UTC_TIME
          { x' == synth_asn1_oid_V tag x })
= x'
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

let serialize_asn1_utc_time
: serializer (parse_asn1_utc_time)
= serialize_flbytes32 13ul
  `serialize_filter`
  valid_utc_time

inline_for_extraction
let parser_tag_of_utc_time
  (x: datatype_of_asn1_type UTC_TIME)
: Tot (the_asn1_tag UTC_TIME `tuple2` asn1_value_int32_of_type UTC_TIME)
= (UTC_TIME, 13ul)

#push-options "--ifuel 1"
let synth_asn1_oid_V
  (tag: the_asn1_tag UTC_TIME `tuple2` asn1_value_int32_of_type UTC_TIME)
  (x: datatype_of_asn1_type UTC_TIME)
: GTot (refine_with_tag parser_tag_of_utc_time tag)
= x
#pop-options
/
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

    tag:
      (ASN1.Base.the_asn1_tag ASN1.Base.UTC_TIME *
        ASN1.Base.asn1_value_int32_of_type ASN1.Base.UTC_TIME) ->
    x': LowParse.Spec.Base.refine_with_tag ASN1.Spec.Value.UTC_TIME.parser_tag_of_utc_time tag
  -> x:
    ASN1.Base.datatype_of_asn1_type ASN1.Base.UTC_TIME
      {x' == ASN1.Spec.Value.UTC_TIME.synth_asn1_oid_V tag x}
FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.UTC_TIME ASN1.Base.asn1_value_int32_of_type LowParse.Spec.Base.refine_with_tag ASN1.Base.datatype_of_asn1_type ASN1.Spec.Value.UTC_TIME.parser_tag_of_utc_time Prims.eq2 ASN1.Spec.Value.UTC_TIME.synth_asn1_oid_V
let synth_asn1_oid_V_inverse
      (tag: (the_asn1_tag UTC_TIME) `tuple2` (asn1_value_int32_of_type UTC_TIME))
      (x': refine_with_tag parser_tag_of_utc_time tag)
    : Tot (x: datatype_of_asn1_type UTC_TIME {x' == synth_asn1_oid_V tag x}) =
  
x'