val serialize32_asn1_string_TLV_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) })
: serializer32_backwards (serialize_asn1_string_TLV t len_of_string filter_string synth_string synth_string_inverse prf)
val serialize32_asn1_string_TLV_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) })
: serializer32_backwards (serialize_asn1_string_TLV t len_of_string filter_string synth_string synth_string_inverse prf)
let serialize32_asn1_string_TLV_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) })
: serializer32_backwards (serialize_asn1_string_TLV t len_of_string filter_string synth_string synth_string_inverse prf)
= serialize32_tagged_union_backwards
  (* lst*) (serialize32_asn1_tag_of_type_backwards t
            `serialize32_nondep_then_backwards`
            serialize32_asn1_length_of_type_backwards t)
  (* tg *) (fun x -> parser_tag_of_asn1_string t len_of_string x)
  (* ls *) (fun x -> (serialize32_synth_backwards
                    (* ls *) (weak_kind_of_type t
                              `serialize32_weaken_backwards`
                              serialize32_asn1_string_backwards t len_of_string filter_string synth_string synth_string_inverse prf (msnd x))
                    (* f2 *) (synth_asn1_string_V t len_of_string x)
                    (* g1 *) (synth_asn1_string_V_inverse t len_of_string x)
                    (* g1'*) (synth_asn1_string_V_inverse t len_of_string x)
                    (* prf*) ()))
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

noextract inline_for_extraction
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

#push-options "--z3rlimit 32 --fuel 2 --ifuel 2"
/
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) }
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.StringCombinator.serialize_asn1_string_TLV
          t
          len_of_string
          filter_string
          synth_string
          synth_string_inverse
          prf)
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 ASN1.Low.Base.serialize32_tagged_union_backwards LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Spec.Length.parse_asn1_length_kind_of_type FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag LowParse.Spec.Combinators.nondep_then ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Length.parse_asn1_length_of_type LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Low.Base.serialize32_nondep_then_backwards ASN1.Low.Tag.serialize32_asn1_tag_of_type_backwards ASN1.Low.Length.serialize32_asn1_length_of_type_backwards ASN1.Spec.Value.StringCombinator.parser_tag_of_asn1_string ASN1.Base.weak_kind_of_type LowParse.Spec.Combinators.parse_synth ASN1.Low.Base.msnd LowParse.Spec.Base.refine_with_tag LowParse.Spec.Base.weaken LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Value.StringCombinator.parse_asn1_string ASN1.Spec.Value.StringCombinator.synth_asn1_string_V LowParse.Spec.Base.parser LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.serialize_weaken ASN1.Spec.Value.StringCombinator.serialize_asn1_string ASN1.Spec.Value.StringCombinator.synth_asn1_string_V_inverse LowParse.Spec.Base.serializer ASN1.Low.Base.serialize32_synth_backwards ASN1.Low.Base.serialize32_weaken_backwards ASN1.Low.Value.StringCombinator.serialize32_asn1_string_backwards ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_kind ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV ASN1.Spec.Value.StringCombinator.serialize_asn1_string_TLV
let serialize32_asn1_string_TLV_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)})
    : serializer32_backwards (serialize_asn1_string_TLV t
          len_of_string
          filter_string
          synth_string
          synth_string_inverse
          prf) =
  
serialize32_tagged_union_backwards ((serialize32_asn1_tag_of_type_backwards t)
    `serialize32_nondep_then_backwards`
    (serialize32_asn1_length_of_type_backwards t))
  (fun x -> parser_tag_of_asn1_string t len_of_string x)
  (fun x ->
      (serialize32_synth_backwards ((weak_kind_of_type t)
            `serialize32_weaken_backwards`
            (serialize32_asn1_string_backwards t
                len_of_string
                filter_string
                synth_string
                synth_string_inverse
                prf
                (msnd x)))
          (synth_asn1_string_V t len_of_string x)
          (synth_asn1_string_V_inverse t len_of_string x)
          (synth_asn1_string_V_inverse t len_of_string x)
          ()))