val serialize32_x509_version_payload_backwards
: serializer32_backwards serialize_x509_version_payload
val serialize32_x509_version_payload_backwards
: serializer32_backwards serialize_x509_version_payload
let serialize32_x509_version_payload_backwards
= serialize32_asn1_TLV_backwards_of_type INTEGER
  `serialize32_filter_backwards`
  filter_x509_version
module X509.BasicFields.Version

open LowParse.Low.Base

open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

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

let parse_x509_version_payload
= parse_asn1_TLV_of_type INTEGER
  `parse_filter`
  filter_x509_version

let serialize_x509_version_payload
= serialize_asn1_TLV_of_type INTEGER
  `serialize_filter`
  filter_x509_version


let lemma_serialize_x509_version_payload_size_exact x
= lemma_serialize_asn1_integer_TLV_size x;
  assert (length_of_opaque_serialization serialize_x509_version_payload x == length_of_asn1_primitive_TLV #INTEGER x)
/
X509.Base.fst.checked prims.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.Version.fst
ASN1.Low.Base.serializer32_backwards X509.BasicFields.Version.serialize_x509_version_payload
ASN1.Low.Base.serialize32_filter_backwards ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.INTEGER ASN1.Base.datatype_of_asn1_type ASN1.Spec.TLV.parse_asn1_TLV_of_type ASN1.Spec.TLV.serialize_asn1_TLV_of_type ASN1.Low.TLV.serialize32_asn1_TLV_backwards_of_type X509.BasicFields.Version.filter_x509_version
let serialize32_x509_version_payload_backwards =
  
(serialize32_asn1_TLV_backwards_of_type INTEGER) `serialize32_filter_backwards` filter_x509_version