val synth_asn1_octet_string_V
      (a: asn1_tag_t)
      (tag: (the_asn1_tag a & asn1_value_int32_of_type OCTET_STRING))
      (value: datatype_of_asn1_type OCTET_STRING {v (value.len) == v (snd tag)})
    : GTot (refine_with_tag (parser_tag_of_octet_string a) tag)
val synth_asn1_octet_string_V
      (a: asn1_tag_t)
      (tag: (the_asn1_tag a & asn1_value_int32_of_type OCTET_STRING))
      (value: datatype_of_asn1_type OCTET_STRING {v (value.len) == v (snd tag)})
    : GTot (refine_with_tag (parser_tag_of_octet_string a) tag)
let synth_asn1_octet_string_V
  (a: asn1_tag_t)
  (tag: (the_asn1_tag a & asn1_value_int32_of_type OCTET_STRING))
  (value: datatype_of_asn1_type OCTET_STRING { v (value.len) == v (snd tag) })
: GTot (refine_with_tag (parser_tag_of_octet_string a) tag)
= value
module ASN1.Spec.Value.OCTET_STRING

open ASN1.Spec.Base
open LowParse.Spec.Bytes

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

open FStar.Integers

module B32 = FStar.Bytes

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

(* NOTE: This module defines:
         1) The ASN1 `OCTET_STRING` Value Parser and Serializer
         2) The ASN1 `OCTET_STRING` TLV Parser and Serializer

         And each part is organized as:
         1) Aux (ghost) functions with prefix `filter_` to filter out invalid input bytes
         2) Aux (ghost) functions with prefix `synth_` to decode the valid input bytes into our
            representation of OCTET_STRING values. These functions are injective.
         3) Aux (ghost) functions with prefix `synth_` and suffix `_inverse` to encode our
            representation of OCTET_STRING into bytes. These functions are the inverse of
            corresponding synth functions.
         4) Functions with the prefix `parse_` are parsers constructed using parser combinators and
            aux functions.
         5) Functions with the prefix `serialize_` are serializers constructed using serializer
            combinators and aux functions.
         6) Lemma with suffix `_unfold` reveals the computation of parser/serialzier.
         7) Lemma with suffix `_size` reveals the length of a serialization.
*)

///////////////////////////////////////////////////////////
//// ASN1 `OCTET_STRING` Value Parser and Serializer
//////////////////////////////////////////////////////////

/// Decodes input bytes into our representation of a OCTET_STRING value
let synth_asn1_octet_string l s32
= { len = u l; s = s32 }


/// Encodes our representation of a OCTET_STRING into bytes
let synth_asn1_octet_string_inverse l value
= value.s

///
/// Parser
///
let parse_asn1_octet_string l
= parse_flbytes l
  `parse_synth`
  synth_asn1_octet_string l

///
/// Serializer
///
let serialize_asn1_octet_string l
= serialize_synth
  (* p1 *) (parse_flbytes l)
  (* f2 *) (synth_asn1_octet_string l)
  (* s1 *) (serialize_flbytes l)
  (* g1 *) (synth_asn1_octet_string_inverse l)
  (* Prf*) ()


///
/// Lemmas
///

/// Reveal the computation of parse
let lemma_parse_asn1_octet_string_unfold l input
= parse_synth_eq
  (* p1 *) (parse_flbytes l)
  (* f2 *) (synth_asn1_octet_string l)
  (* in *) (input)

/// Reveal the computation of serialize
let lemma_serialize_asn1_octet_string_unfold l value
= serialize_synth_eq
  (* p1 *) (parse_flbytes l)
  (* f2 *) (synth_asn1_octet_string l)
  (* s1 *) (serialize_flbytes l)
  (* g1 *) (synth_asn1_octet_string_inverse l)
  (* Prf*) ()
  (* in *) (value)

/// Reveal the length of a serialzation
let lemma_serialize_asn1_octet_string_size l value
= parser_kind_prop_equiv (parse_asn1_octet_string_kind l) (parse_asn1_octet_string l);
  lemma_serialize_asn1_octet_string_unfold l value


///////////////////////////////////////////////////////////
//// ASN1 `OCTET_STRING` TLV Parser and Serializer
///////////////////////////////////////////////////////////

/// parser tag for the `tagged_union` combinators
noextract
let parser_tag_of_octet_string
  (a: asn1_tag_t)
  (x: datatype_of_asn1_type OCTET_STRING)
: GTot (the_asn1_tag a & asn1_value_int32_of_type OCTET_STRING)
= (a, x.len)

///
/// A pair of aux parser/serializer, which explicitly coerce the `OCTET_STRING` value
/// between the subtype used by `OCTET_STRING` value parser/serialzier and `OCTET_STRING`
/// TLV parser/serializer.
///
/// NOTE: I found that have this aux parser explicitly defined will make the prove of
///       `_unfold` lemmas simpler.
///

/// Convert an `OCTET_STRING` value from the subtype used by its value parser to the subtype
/// used by its TLV parser/serializer
/// (value : subtype_{value}) <: subtype_{TLV}
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.OCTET_STRING.fst

    a: ASN1.Base.asn1_tag_t ->
    tag: (ASN1.Base.the_asn1_tag a * ASN1.Base.asn1_value_int32_of_type ASN1.Base.OCTET_STRING) ->
    value:
      ASN1.Base.datatype_of_asn1_type ASN1.Base.OCTET_STRING
        { FStar.Integers.v (Mkoctet_string_t?.len value) ==
          FStar.Integers.v (FStar.Pervasives.Native.snd tag) }
  -> Prims.GTot
    (LowParse.Spec.Base.refine_with_tag (ASN1.Spec.Value.OCTET_STRING.parser_tag_of_octet_string a)
        tag)
ASN1.Base.asn1_tag_t FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.asn1_value_int32_of_type ASN1.Base.OCTET_STRING ASN1.Base.datatype_of_asn1_type Prims.eq2 FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.l_or FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v ASN1.Base.__proj__Mkoctet_string_t__item__len FStar.Pervasives.Native.snd LowParse.Spec.Base.refine_with_tag ASN1.Spec.Value.OCTET_STRING.parser_tag_of_octet_string
let synth_asn1_octet_string_V
      (a: asn1_tag_t)
      (tag: (the_asn1_tag a & asn1_value_int32_of_type OCTET_STRING))
      (value: datatype_of_asn1_type OCTET_STRING {v (value.len) == v (snd tag)})
    : GTot (refine_with_tag (parser_tag_of_octet_string a) tag) =
  
value