val lemma_parse_asn1_ASN1_NULL_TLV_unfold
  (input_TLV: bytes)
: Lemma (
  parse parse_asn1_ASN1_NULL_TLV input_TLV ==
 (match parse (parse_asn1_tag_of_type ASN1_NULL) input_TLV with
  | None -> None
  | Some (ASN1_NULL, consumed_T) ->
    (let input_LV = Seq.slice input_TLV consumed_T (Seq.length input_TLV) in
     match parse (parse_asn1_length_of_type ASN1_NULL) input_LV with
     | None -> None
     | Some (0ul, consumed_L) ->
       (let input_V = Seq.slice input_LV consumed_L (Seq.length input_LV) in
        match parse parse_asn1_ASN1_NULL input_V with
        | None -> None
        | Some (value, consumed_V) -> Some (value, (consumed_T + consumed_L + consumed_V <: consumed_length input_TLV)))))
)
val lemma_parse_asn1_ASN1_NULL_TLV_unfold
  (input_TLV: bytes)
: Lemma (
  parse parse_asn1_ASN1_NULL_TLV input_TLV ==
 (match parse (parse_asn1_tag_of_type ASN1_NULL) input_TLV with
  | None -> None
  | Some (ASN1_NULL, consumed_T) ->
    (let input_LV = Seq.slice input_TLV consumed_T (Seq.length input_TLV) in
     match parse (parse_asn1_length_of_type ASN1_NULL) input_LV with
     | None -> None
     | Some (0ul, consumed_L) ->
       (let input_V = Seq.slice input_LV consumed_L (Seq.length input_LV) in
        match parse parse_asn1_ASN1_NULL input_V with
        | None -> None
        | Some (value, consumed_V) -> Some (value, (consumed_T + consumed_L + consumed_V <: consumed_length input_TLV)))))
)
let lemma_parse_asn1_ASN1_NULL_TLV_unfold input_TLV
= nondep_then_eq
  (* p1 *) (parse_asn1_tag_of_type ASN1_NULL)
  (* p2 *) (parse_asn1_length_of_type ASN1_NULL)
  (* in *) (input_TLV);
  nondep_then_eq
  (* p1 *) (parse_asn1_tag_of_type ASN1_NULL
            `nondep_then`
            parse_asn1_length_of_type ASN1_NULL)
  (* p2 *) (parse_asn1_ASN1_NULL)
  (* in *) (input_TLV);
  parse_synth_eq
  (* p1 *) (parse_asn1_tag_of_type ASN1_NULL
            `nondep_then`
            parse_asn1_length_of_type ASN1_NULL
            `nondep_then`
            parse_asn1_ASN1_NULL)
  (* f2 *) (synth_asn1_ASN1_NULL_TLV)
  (* in *) (input_TLV)
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
///////////////////////////////////////////////////////////////

/// Synthesize the TLV of a `ASN1_NULL` value
let synth_asn1_ASN1_NULL_TLV a
= snd a

/// Synthesize th `ASN1_NULL` value from a `ASN1_NULL` TLV
noextract
let synth_asn1_ASN1_NULL_TLV_inverse x
= ((ASN1_NULL, 0ul), x)


///
/// `ASN1_NULL` TLV parser
///
let parse_asn1_ASN1_NULL_TLV
= parse_asn1_tag_of_type ASN1_NULL
  `nondep_then`
  parse_asn1_length_of_type ASN1_NULL
  `nondep_then`
  parse_asn1_ASN1_NULL
  `parse_synth`
  synth_asn1_ASN1_NULL_TLV

///
/// `ASN1_NULL` TLV serialzier
///
let serialize_asn1_ASN1_NULL_TLV
= serialize_synth
  (* p1 *) (parse_asn1_tag_of_type ASN1_NULL
            `nondep_then`
            parse_asn1_length_of_type ASN1_NULL
            `nondep_then`
            parse_asn1_ASN1_NULL)
  (* f2 *) (synth_asn1_ASN1_NULL_TLV)
  (* s1 *) (serialize_asn1_tag_of_type ASN1_NULL
            `serialize_nondep_then`
            serialize_asn1_length_of_type ASN1_NULL
            `serialize_nondep_then`
            serialize_asn1_ASN1_NULL)
  (* g1 *) (synth_asn1_ASN1_NULL_TLV_inverse)
  (* Prf*) ()

///
/// Lemmas
///
/
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
input_TLV: ASN1.Base.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.parse ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL_TLV input_TLV ==
      (match
          LowParse.Spec.Base.parse (ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Base.ASN1_NULL)
            input_TLV
        with
        | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
        | FStar.Pervasives.Native.Some
          #_
          (FStar.Pervasives.Native.Mktuple2 #_ #_ ASN1.Base.ASN1_NULL consumed_T) ->
          let input_LV =
            FStar.Seq.Base.slice input_TLV consumed_T (FStar.Seq.Base.length input_TLV)
          in
          (match
              LowParse.Spec.Base.parse (ASN1.Spec.Length.parse_asn1_length_of_type ASN1.Base.ASN1_NULL
                  )
                input_LV
            with
            | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
            | FStar.Pervasives.Native.Some
              #_
              (FStar.Pervasives.Native.Mktuple2 #_ #_ 0ul consumed_L) ->
              let input_V =
                FStar.Seq.Base.slice input_LV consumed_L (FStar.Seq.Base.length input_LV)
              in
              (match LowParse.Spec.Base.parse ASN1.Spec.Value.NULL.parse_asn1_ASN1_NULL input_V with
                | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
                | FStar.Pervasives.Native.Some
                  #_
                  (FStar.Pervasives.Native.Mktuple2 #_ #_ value consumed_V) ->
                  FStar.Pervasives.Native.Some (value, consumed_T + consumed_L + consumed_V))
              <:
              FStar.Pervasives.Native.option (ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL *
                  LowParse.Spec.Base.consumed_length input_TLV))
          <:
          FStar.Pervasives.Native.option (ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL *
              LowParse.Spec.Base.consumed_length input_TLV)))
ASN1.Base.bytes LowParse.Spec.Combinators.parse_synth_eq 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 ASN1.Spec.Value.NULL.synth_asn1_ASN1_NULL_TLV Prims.unit LowParse.Spec.Combinators.nondep_then_eq
let lemma_parse_asn1_ASN1_NULL_TLV_unfold input_TLV =
  
nondep_then_eq (parse_asn1_tag_of_type ASN1_NULL) (parse_asn1_length_of_type ASN1_NULL) (input_TLV);
nondep_then_eq ((parse_asn1_tag_of_type ASN1_NULL)
    `nondep_then`
    (parse_asn1_length_of_type ASN1_NULL))
  (parse_asn1_ASN1_NULL)
  (input_TLV);
parse_synth_eq (((parse_asn1_tag_of_type ASN1_NULL)
      `nondep_then`
      (parse_asn1_length_of_type ASN1_NULL))
    `nondep_then`
    parse_asn1_ASN1_NULL)
  (synth_asn1_ASN1_NULL_TLV)
  (input_TLV)