val synth_asn1_ASN1_NULL_TLV
  (a: (the_asn1_tag ASN1_NULL * asn1_value_int32_of_type ASN1_NULL) * datatype_of_asn1_type ASN1_NULL)
: GTot (datatype_of_asn1_type ASN1_NULL)
val synth_asn1_ASN1_NULL_TLV
  (a: (the_asn1_tag ASN1_NULL * asn1_value_int32_of_type ASN1_NULL) * datatype_of_asn1_type ASN1_NULL)
: GTot (datatype_of_asn1_type ASN1_NULL)
let synth_asn1_ASN1_NULL_TLV a
= snd a
module ASN1.Spec.Value.NULL

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)
(* NOTE: This module defines:
         1) The ASN1 `ASN1_NULL` Value Parser and Serializer
         2) The ASN1 `ASN1_NULL` TLV Parser and Serializer
*)

///////////////////////////////////////////////////////////////
////  ASN1 `ASN1_NULL` Value Parser/Serializer
///////////////////////////////////////////////////////////////

///
/// ASN1 `ASN1_NULL` value parser parses nothing and returns `()`
/// using the `parse_ret` combinator
///
let parse_asn1_ASN1_NULL
= parse_ret
  (* v *) ()

///
/// ASN1 `ASN1_NULL` value parser serialize `()` to empty bytes
/// using the `serialize_ret` combinator
///
let serialize_asn1_ASN1_NULL
= serialize_ret
  (* v *) ()
  (*prf*) (fun n -> ())

///
/// Lemmas
///

/// Reveal the computation of serialize
let lemma_serialize_asn1_ASN1_NULL_unfold value
= ()

/// Reveal the size of a serialiaztion
let lemma_serialize_asn1_ASN1_NULL_size value
= parser_kind_prop_equiv parse_asn1_ASN1_NULL_kind parse_asn1_ASN1_NULL;
  lemma_serialize_asn1_ASN1_NULL_unfold value

///////////////////////////////////////////////////////////////
////  ASN1 `ASN1_NULL` TLV Parser/Serializer
///////////////////////////////////////////////////////////////
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.NULL.fst

    a:
      ((ASN1.Base.the_asn1_tag ASN1.Base.ASN1_NULL *
        ASN1.Base.asn1_value_int32_of_type ASN1.Base.ASN1_NULL) *
        ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL)
  -> Prims.GTot (ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL)
FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.ASN1_NULL ASN1.Base.asn1_value_int32_of_type ASN1.Base.datatype_of_asn1_type FStar.Pervasives.Native.snd
let synth_asn1_ASN1_NULL_TLV a =
  
snd a