val lemma_serialize_x509_version_size
  (x: x509_version_t)
: Lemma (
  predicate_serialize_asn1_envelop_tag_with_TLV_size
    (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
    (serialize_x509_version_payload)
    (x)
)
val lemma_serialize_x509_version_size
  (x: x509_version_t)
: Lemma (
  predicate_serialize_asn1_envelop_tag_with_TLV_size
    (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
    (serialize_x509_version_payload)
    (x)
)
let lemma_serialize_x509_version_size x
= lemma_serialize_asn1_envelop_tag_with_TLV_size
    (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
    (serialize_x509_version_payload)
    (x)
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)

let serialize32_x509_version_payload_backwards
= serialize32_asn1_TLV_backwards_of_type INTEGER
  `serialize32_filter_backwards`
  filter_x509_version

noextract inline_for_extraction
let x509_version_1: x509_version_t = 0l

noextract inline_for_extraction
let x509_version_2: x509_version_t = 1l

noextract inline_for_extraction
let x509_version_3: x509_version_t = 2l

let lemma_serialize_x509_version_unfold x
= lemma_serialize_asn1_envelop_tag_with_TLV_unfold
    (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
    (serialize_x509_version_payload)
    (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
x: X509.BasicFields.Version.x509_version_t
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Value.Envelop.predicate_serialize_asn1_envelop_tag_with_TLV_size (ASN1.Base.CUSTOM_TAG
            ASN1.Base.CONTEXT_SPECIFIC ASN1.Base.CONSTRUCTED 0uy)
        X509.BasicFields.Version.serialize_x509_version_payload
        x)
X509.BasicFields.Version.x509_version_t ASN1.Spec.Value.Envelop.lemma_serialize_asn1_envelop_tag_with_TLV_size X509.BasicFields.Version.parse_x509_version_payload_kind X509.BasicFields.Version.x509_version_payload_t X509.BasicFields.Version.parse_x509_version_payload ASN1.Base.CUSTOM_TAG ASN1.Base.CONTEXT_SPECIFIC ASN1.Base.CONSTRUCTED FStar.UInt8.__uint_to_t X509.BasicFields.Version.serialize_x509_version_payload Prims.unit
let lemma_serialize_x509_version_size x =
  
lemma_serialize_asn1_envelop_tag_with_TLV_size (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
  (serialize_x509_version_payload)
  (x)