val serialize32_asn1_ASN1_NULL_TLV_backwards (_:unit)
: (serializer32_backwards serialize_asn1_ASN1_NULL_TLV)
val serialize32_asn1_ASN1_NULL_TLV_backwards (_:unit)
: (serializer32_backwards serialize_asn1_ASN1_NULL_TLV)
let serialize32_asn1_ASN1_NULL_TLV_backwards ()
= serialize32_synth_backwards
   (* ls1*) (serialize32_asn1_tag_of_type_backwards ASN1_NULL
             `serialize32_nondep_then_backwards`
             serialize32_asn1_length_of_type_backwards ASN1_NULL
             `serialize32_nondep_then_backwards`
             serialize32_asn1_ASN1_NULL_backwards ())
   (* f2 *) (synth_asn1_ASN1_NULL_TLV)
   (* g1 *) (synth_asn1_ASN1_NULL_TLV_inverse)
   (* lg1*) (synth_asn1_ASN1_NULL_TLV_inverse_impl)
   (* Prf*) ()
module ASN1.Low.Value.NULL

open ASN1.Base
open ASN1.Spec.Value.NULL
open ASN1.Low.Base

open FStar.Integers

module B = LowStar.Buffer

friend ASN1.Spec.Value.NULL

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)

let serialize32_asn1_ASN1_NULL_backwards ()
= fun (_: datatype_of_asn1_type ASN1_NULL)
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
-> 0ul

open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Low.Tag
open ASN1.Low.Length

inline_for_extraction
let synth_asn1_ASN1_NULL_TLV_inverse_impl
  (x: datatype_of_asn1_type ASN1_NULL)
: Tot (a: ((the_asn1_tag ASN1_NULL & asn1_value_int32_of_type ASN1_NULL) & datatype_of_asn1_type ASN1_NULL){a == synth_asn1_ASN1_NULL_TLV_inverse x})
= ((ASN1_NULL, 0ul), x)
/
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.NULL.fst
_: Prims.unit
  -> ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.NULL.serialize_asn1_ASN1_NULL_TLV
Prims.unit ASN1.Low.Base.serialize32_synth_backwards LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Spec.Length.parse_asn1_length_kind_of_type ASN1.Base.ASN1_NULL ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL_kind FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.asn1_value_int32_of_type ASN1.Base.datatype_of_asn1_type LowParse.Spec.Combinators.nondep_then ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Length.parse_asn1_length_of_type ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Spec.Value.NULL.serialize_asn1_ASN1_NULL ASN1.Low.Base.serialize32_nondep_then_backwards ASN1.Low.Tag.serialize32_asn1_tag_of_type_backwards ASN1.Low.Length.serialize32_asn1_length_of_type_backwards ASN1.Low.Value.NULL.serialize32_asn1_ASN1_NULL_backwards ASN1.Spec.Value.NULL.synth_asn1_ASN1_NULL_TLV ASN1.Spec.Value.NULL.synth_asn1_ASN1_NULL_TLV_inverse ASN1.Low.Value.NULL.synth_asn1_ASN1_NULL_TLV_inverse_impl ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL_TLV_kind ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL_TLV ASN1.Spec.Value.NULL.serialize_asn1_ASN1_NULL_TLV
let serialize32_asn1_ASN1_NULL_TLV_backwards () =
  
serialize32_synth_backwards (((serialize32_asn1_tag_of_type_backwards ASN1_NULL)
      `serialize32_nondep_then_backwards`
      (serialize32_asn1_length_of_type_backwards ASN1_NULL))
    `serialize32_nondep_then_backwards`
    (serialize32_asn1_ASN1_NULL_backwards ()))
  (synth_asn1_ASN1_NULL_TLV)
  (synth_asn1_ASN1_NULL_TLV_inverse)
  (synth_asn1_ASN1_NULL_TLV_inverse_impl)
  ()