val synth_asn1_octet_string
  (l: asn1_value_length_of_type OCTET_STRING)
  (s32: B32.lbytes l)
: GTot (value: datatype_of_asn1_type OCTET_STRING{v (value.len) == l})
val synth_asn1_octet_string
  (l: asn1_value_length_of_type OCTET_STRING)
  (s32: B32.lbytes l)
: GTot (value: datatype_of_asn1_type OCTET_STRING{v (value.len) == l})
let synth_asn1_octet_string l s32
= { len = u l; s = s32 }
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
//////////////////////////////////////////////////////////
/
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
l: ASN1.Base.asn1_value_length_of_type ASN1.Base.OCTET_STRING -> s32: FStar.Bytes.lbytes l
  -> Prims.GTot
    (value:
      ASN1.Base.datatype_of_asn1_type ASN1.Base.OCTET_STRING
        {FStar.Integers.v (Mkoctet_string_t?.len value) == l})
ASN1.Base.asn1_value_length_of_type ASN1.Base.OCTET_STRING FStar.Bytes.lbytes ASN1.Base.Mkoctet_string_t FStar.Integers.u FStar.Integers.Unsigned FStar.Integers.W32 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 Prims.l_and Prims.b2t FStar.Integers.op_Greater_Equals ASN1.Base.asn1_value_length_inbound_of_type FStar.Integers.v ASN1.Base.__proj__Mkoctet_string_t__item__len
let synth_asn1_octet_string l s32 =
  
{ len = u l; s = s32 }