val serialize32_asn1_string_TLV_with_character_bound_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) })
  (count_character: (x: datatype_of_asn1_type t) -> Tot (asn1_int32))
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_asn1_string_TLV_with_character_bound t len_of_string filter_string synth_string synth_string_inverse prf count_character lb ub)
val serialize32_asn1_string_TLV_with_character_bound_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) })
  (count_character: (x: datatype_of_asn1_type t) -> Tot (asn1_int32))
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_asn1_string_TLV_with_character_bound t len_of_string filter_string synth_string synth_string_inverse prf count_character lb ub)
let serialize32_asn1_string_TLV_with_character_bound_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) })
  (count_character: (x: datatype_of_asn1_type t) -> Tot (asn1_int32))
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_asn1_string_TLV_with_character_bound t len_of_string filter_string synth_string synth_string_inverse prf count_character lb ub)
= serialize32_asn1_string_TLV_backwards t len_of_string filter_string synth_string synth_string_inverse prf
  `serialize32_filter_backwards`
  filter_asn1_string_with_character_bound t count_character lb ub
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"
noextract inline_for_extraction
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*) ()))
/
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) } ->
    count_character: (x: ASN1.Base.datatype_of_asn1_type t -> ASN1.Base.asn1_int32) ->
    lb: ASN1.Base.asn1_value_int32_of_type t ->
    ub: ASN1.Base.asn1_value_int32_of_type t {lb <= ub}
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.StringCombinator.serialize_asn1_string_TLV_with_character_bound
          t
          len_of_string
          filter_string
          synth_string
          synth_string_inverse
          prf
          count_character
          lb
          ub)
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.Base.asn1_int32 Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Low.Base.serialize32_filter_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 ASN1.Low.Value.StringCombinator.serialize32_asn1_string_TLV_backwards ASN1.Spec.Value.StringCombinator.filter_asn1_string_with_character_bound ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.StringCombinator.asn1_string_with_character_bound_t ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_with_character_bound ASN1.Spec.Value.StringCombinator.serialize_asn1_string_TLV_with_character_bound
let serialize32_asn1_string_TLV_with_character_bound_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)})
      (count_character: (x: datatype_of_asn1_type t -> Tot (asn1_int32)))
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer32_backwards (serialize_asn1_string_TLV_with_character_bound t
          len_of_string
          filter_string
          synth_string
          synth_string_inverse
          prf
          count_character
          lb
          ub) =
  
(serialize32_asn1_string_TLV_backwards t
    len_of_string
    filter_string
    synth_string
    synth_string_inverse
    prf)
`serialize32_filter_backwards`
(filter_asn1_string_with_character_bound t count_character lb ub)