val serialize32_asn1_envelop_tag_with_TLV_backwards
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (#s: serializer p)
  (a: asn1_tag_t)
  (s32: serializer32_backwards s)
: (serializer32_backwards (serialize_asn1_envelop_tag_with_TLV a s))
val serialize32_asn1_envelop_tag_with_TLV_backwards
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (#s: serializer p)
  (a: asn1_tag_t)
  (s32: serializer32_backwards s)
: (serializer32_backwards (serialize_asn1_envelop_tag_with_TLV a s))
let serialize32_asn1_envelop_tag_with_TLV_backwards #k #t #p #s a s32
= fun x #rrel #rel b pos ->
  (* Prf *) lemma_serialize_asn1_envelop_tag_with_unfold a s (parser_tag_of_asn1_envelop_tag_with a s x) x;
  (* Prf *) lemma_serialize_asn1_envelop_tag_with_TLV_unfold a s x;
  (* Prf *) lemma_serialize_asn1_envelop_tag_with_TLV_size a s x;
  (* Prf *) serialize_tagged_union_eq
            (* st *) (serialize_asn1_tag_of_type a
                      `serialize_nondep_then`
                      serialize_asn1_length_of_type a)
            (* tg *) (parser_tag_of_asn1_envelop_tag_with a s)
            (* s  *) (serialize_asn1_envelop_tag_with_weak a s)
            (* in *) (x);
  (* Prf *) let posl = Ghost.hide (pos - u (Seq.length (serialize (serialize_asn1_envelop_tag_with_TLV a s) x))) in
  (* Prf *) let posr = Ghost.hide pos in

  let offset_data = frame_serializer32_backwards s32 x b posl posr pos in

  [@inline_let]
  let pos = pos - offset_data in

  let offset_tag_len = frame_serializer32_backwards
                       (serialize32_asn1_tag_of_type_backwards a
                        `serialize32_nondep_then_backwards`
                        serialize32_asn1_length_of_type_backwards a)
                       (a, offset_data) b posl posr pos in

(* return *) (offset_tag_len + offset_data)
module ASN1.Low.Value.Envelop
///
/// ASN.1 Low
///
open LowParse.Low.Base
open LowParse.Low.Combinators
open LowParse.Low.FLData

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open ASN1.Spec.Value.Envelop
open ASN1.Low.Base
open ASN1.Low.Tag
open ASN1.Low.Length

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
open FStar.Integers

friend ASN1.Spec.Value.Envelop

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length`, `ASN1.Spec.Value.*` *)
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.FLData.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked ASN1.Spec.Value.Envelop.fst.checked ASN1.Spec.Value.Envelop.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.Envelop.fst
a: ASN1.Base.asn1_tag_t -> s32: ASN1.Low.Base.serializer32_backwards s
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV
          a
          s)
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer ASN1.Base.asn1_tag_t ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t FStar.Integers.op_Plus FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Low.Base.frame_serializer32_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 ASN1.Base.asn1_value_int32_of_type 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 FStar.Pervasives.Native.Mktuple2 FStar.Integers.int_t FStar.Integers.op_Subtraction FStar.Ghost.erased ASN1.Low.Base.size_t FStar.Ghost.hide FStar.Integers.u FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV Prims.unit LowParse.Spec.Combinators.serialize_tagged_union_eq ASN1.Spec.Value.Envelop.parser_tag_of_asn1_envelop_tag_with ASN1.Base.weak_kind_of_type ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_weak ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_weak ASN1.Spec.Value.Envelop.lemma_serialize_asn1_envelop_tag_with_TLV_size ASN1.Spec.Value.Envelop.lemma_serialize_asn1_envelop_tag_with_TLV_unfold ASN1.Spec.Value.Envelop.lemma_serialize_asn1_envelop_tag_with_unfold
let serialize32_asn1_envelop_tag_with_TLV_backwards #k #t #p #s a s32 =
  
fun x #rrel #rel b pos ->
  lemma_serialize_asn1_envelop_tag_with_unfold a s (parser_tag_of_asn1_envelop_tag_with a s x) x;
  lemma_serialize_asn1_envelop_tag_with_TLV_unfold a s x;
  lemma_serialize_asn1_envelop_tag_with_TLV_size a s x;
  serialize_tagged_union_eq ((serialize_asn1_tag_of_type a)
      `serialize_nondep_then`
      (serialize_asn1_length_of_type a))
    (parser_tag_of_asn1_envelop_tag_with a s)
    (serialize_asn1_envelop_tag_with_weak a s)
    (x);
  let posl =
    Ghost.hide (pos - u (Seq.length (serialize (serialize_asn1_envelop_tag_with_TLV a s) x)))
  in
  let posr = Ghost.hide pos in
  let offset_data = frame_serializer32_backwards s32 x b posl posr pos in
  [@@ inline_let ]let pos = pos - offset_data in
  let offset_tag_len =
    frame_serializer32_backwards ((serialize32_asn1_tag_of_type_backwards a)
        `serialize32_nondep_then_backwards`
        (serialize32_asn1_length_of_type_backwards a))
      (a, offset_data)
      b
      posl
      posr
      pos
  in
  (offset_tag_len + offset_data)