val parse_asn1_ASN1_NULL_TLV_kind:parser_kind
val parse_asn1_ASN1_NULL_TLV_kind:parser_kind
let parse_asn1_ASN1_NULL_TLV_kind
: parser_kind
= strong_parser_kind 2 2 None
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
///////////////////////////////////////////////////////////////

inline_for_extraction noextract
let parse_asn1_ASN1_NULL_kind = parse_ret_kind

///
/// ASN1 `ASN1_NULL` value parser parses nothing and returns `()`
/// using the `parse_ret` combinator
///
noextract
val parse_asn1_ASN1_NULL
: parser parse_asn1_ASN1_NULL_kind (datatype_of_asn1_type ASN1_NULL)

///
/// ASN1 `ASN1_NULL` value parser serialize `()` to empty bytes
/// using the `serialize_ret` combinator
///
noextract
val serialize_asn1_ASN1_NULL
: serializer parse_asn1_ASN1_NULL

///
/// Lemmas
///

/// Reveal the computation of serialize
val lemma_serialize_asn1_ASN1_NULL_unfold
  (value: datatype_of_asn1_type ASN1_NULL)
: Lemma (
  serialize serialize_asn1_ASN1_NULL value == Seq.empty)

/// Reveal the size of a serialiaztion
val lemma_serialize_asn1_ASN1_NULL_size
  (value: datatype_of_asn1_type ASN1_NULL)
: Lemma (
  Seq.length (serialize serialize_asn1_ASN1_NULL value) == 0)

///////////////////////////////////////////////////////////////
////  ASN1 `ASN1_NULL` TLV Parser/Serializer
///////////////////////////////////////////////////////////////

/// Synthesize the TLV of a `ASN1_NULL` value
noextract
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)

/// Synthesize th `ASN1_NULL` value from a `ASN1_NULL` TLV
noextract
val synth_asn1_ASN1_NULL_TLV_inverse
  (x: datatype_of_asn1_type ASN1_NULL)
: GTot (a: ((the_asn1_tag ASN1_NULL * asn1_value_int32_of_type ASN1_NULL) * datatype_of_asn1_type ASN1_NULL){x == synth_asn1_ASN1_NULL_TLV a})
/
prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.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.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some
let parse_asn1_ASN1_NULL_TLV_kind:parser_kind =
  
strong_parser_kind 2 2 None