val serialize32_asn1_string_backwards
  (t: asn1_type { t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING })
  (len_of_string: datatype_of_asn1_type t -> asn1_value_int32_of_type t)
  (filter_string: (len: asn1_value_int32_of_type t)
                  -> (s32: B32.lbytes32 len)
                  -> GTot (bool))
  (synth_string: (len: asn1_value_int32_of_type t)
                 -> (s32: parse_filter_refine (filter_string len))
                 -> GTot (x: datatype_of_asn1_type t
                            { len_of_string x== len }))
  (synth_string_inverse: (len: asn1_value_int32_of_type t)
                         -> (x: datatype_of_asn1_type t { len_of_string x== len })
                         -> (s32: parse_filter_refine (filter_string len)
                                 { x == synth_string len s32 }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (len: asn1_value_int32_of_type t)
: (serializer32_backwards (serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf len))
val serialize32_asn1_string_backwards
  (t: asn1_type { t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING })
  (len_of_string: datatype_of_asn1_type t -> asn1_value_int32_of_type t)
  (filter_string: (len: asn1_value_int32_of_type t)
                  -> (s32: B32.lbytes32 len)
                  -> GTot (bool))
  (synth_string: (len: asn1_value_int32_of_type t)
                 -> (s32: parse_filter_refine (filter_string len))
                 -> GTot (x: datatype_of_asn1_type t
                            { len_of_string x== len }))
  (synth_string_inverse: (len: asn1_value_int32_of_type t)
                         -> (x: datatype_of_asn1_type t { len_of_string x== len })
                         -> (s32: parse_filter_refine (filter_string len)
                                 { x == synth_string len s32 }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (len: asn1_value_int32_of_type t)
: (serializer32_backwards (serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf len))
let serialize32_asn1_string_backwards
  (t: asn1_type { t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING })
  (len_of_string: datatype_of_asn1_type t -> asn1_value_int32_of_type t)
  (filter_string: (len: asn1_value_int32_of_type t)
                  -> (s32: B32.lbytes32 len)
                  -> GTot (bool))
  (synth_string: (len: asn1_value_int32_of_type t)
                 -> (s32: parse_filter_refine (filter_string len))
                 -> GTot (x: datatype_of_asn1_type t
                            { len_of_string x== len }))
  (synth_string_inverse: (len: asn1_value_int32_of_type t)
                         -> (x: datatype_of_asn1_type t { len_of_string x== len })
                         -> (s32: parse_filter_refine (filter_string len)
                                 { x == synth_string len s32 }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (len: asn1_value_int32_of_type t)
: Tot (serializer32_backwards (serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf len))
= fun (x: datatype_of_asn1_type t { v (len_of_string x) == v len })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
-> (* Prf *) lemma_serialize_asn1_string_unfold t len_of_string filter_string synth_string synth_string_inverse prf len x;

    store_bytes
    (* src *) (synth_string_inverse len x)
    (* from*) 0ul
    (* to  *) len
    (* dst *) b
    (* pos *) (pos - len);

(* return *) len
module ASN1.Low.Value.StringCombinator

open ASN1.Base
open ASN1.Spec.Value.StringCombinator
open ASN1.Low.Base
open LowParse.Low.Bytes

open ASN1.Low.Tag
open ASN1.Low.Length

open FStar.Integers

module B = LowStar.Buffer

module B32 = FStar.Bytes

friend ASN1.Spec.Value.StringCombinator
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Bytes.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fst.checked ASN1.Spec.Value.StringCombinator.fst.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.StringCombinator.fst

    t:
      ASN1.Base.asn1_type
        { t == ASN1.Base.IA5_STRING \/ t == ASN1.Base.PRINTABLE_STRING \/
          t == ASN1.Base.OCTET_STRING } ->
    len_of_string: (_: ASN1.Base.datatype_of_asn1_type t -> ASN1.Base.asn1_value_int32_of_type t) ->
    filter_string:
      (len: ASN1.Base.asn1_value_int32_of_type t -> s32: FStar.Bytes.lbytes32 len
          -> Prims.GTot Prims.bool) ->
    synth_string:
      (
            len: ASN1.Base.asn1_value_int32_of_type t ->
            s32: LowParse.Spec.Combinators.parse_filter_refine (filter_string len)
          -> Prims.GTot (x: ASN1.Base.datatype_of_asn1_type t {len_of_string x == len})) ->
    synth_string_inverse:
      (
            len: ASN1.Base.asn1_value_int32_of_type t ->
            x: ASN1.Base.datatype_of_asn1_type t {len_of_string x == len}
          -> s32:
            LowParse.Spec.Combinators.parse_filter_refine (filter_string len)
              {x == synth_string len s32}) ->
    prf:
      Prims.unit
        { forall (len: ASN1.Base.asn1_value_int32_of_type t).
            LowParse.Spec.Combinators.synth_injective (synth_string len) } ->
    len: ASN1.Base.asn1_value_int32_of_type t
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.StringCombinator.serialize_asn1_string t
          len_of_string
          filter_string
          synth_string
          synth_string_inverse
          prf
          len)
ASN1.Base.asn1_type Prims.l_or Prims.eq2 ASN1.Base.asn1_tag_t ASN1.Base.IA5_STRING ASN1.Base.PRINTABLE_STRING ASN1.Base.OCTET_STRING ASN1.Base.datatype_of_asn1_type ASN1.Base.asn1_value_int32_of_type FStar.Bytes.lbytes32 Prims.bool LowParse.Spec.Combinators.parse_filter_refine Prims.unit Prims.l_Forall LowParse.Spec.Combinators.synth_injective FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer LowParse.Bytes.byte ASN1.Low.Base.size_t FStar.UInt32.t LowParse.Low.Bytes.store_bytes FStar.UInt32.__uint_to_t FStar.Integers.op_Subtraction ASN1.Spec.Value.StringCombinator.lemma_serialize_asn1_string_unfold ASN1.Low.Base.serializer32_backwards LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Base.total_constant_size_parser_kind ASN1.Spec.Value.StringCombinator.parse_asn1_string ASN1.Spec.Value.StringCombinator.serialize_asn1_string
let serialize32_asn1_string_backwards
      (t: asn1_type{t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING})
      (len_of_string: (datatype_of_asn1_type t -> asn1_value_int32_of_type t))
      (filter_string: (len: asn1_value_int32_of_type t -> s32: B32.lbytes32 len -> GTot (bool)))
      (synth_string:
          (len: asn1_value_int32_of_type t -> s32: parse_filter_refine (filter_string len)
              -> GTot (x: datatype_of_asn1_type t {len_of_string x == len})))
      (synth_string_inverse:
          (len: asn1_value_int32_of_type t -> x: datatype_of_asn1_type t {len_of_string x == len}
              -> (s32: parse_filter_refine (filter_string len) {x == synth_string len s32})))
      (prf: unit{forall len. synth_injective (synth_string len)})
      (len: asn1_value_int32_of_type t)
    : Tot
    (serializer32_backwards (serialize_asn1_string t
            len_of_string
            filter_string
            synth_string
            synth_string_inverse
            prf
            len)) =
  
fun
  (x: datatype_of_asn1_type t {v (len_of_string x) == v len})
  (#rrel: _)
  (#rel: _)
  (b: B.mbuffer byte rrel rel)
  (pos: size_t)
  ->
  lemma_serialize_asn1_string_unfold t
    len_of_string
    filter_string
    synth_string
    synth_string_inverse
    prf
    len
    x;
  store_bytes (synth_string_inverse len x) 0ul len b (pos - len);
  len