val serialize32_asn1_bit_string_backwards
  (len: asn1_value_int32_of_type BIT_STRING)
: (serializer32_backwards (serialize_asn1_bit_string (v len)))
val serialize32_asn1_bit_string_backwards
  (len: asn1_value_int32_of_type BIT_STRING)
: (serializer32_backwards (serialize_asn1_bit_string (v len)))
let serialize32_asn1_bit_string_backwards len
= fun (value: datatype_of_asn1_type BIT_STRING { v len == v (Mkbit_string_t?.bs_len value) })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->  (* Prf *) lemma_serialize_asn1_bit_string_unfold (v len) (value);
    (* Prf *) let h0 = HST.get () in
    // let (|len, unused_bits, s32|) = value in
    let leading_byte: byte = FStar.Int.Cast.uint32_to_uint8 value.bs_unused_bits in
    (* Prf *) writable_weaken
              (* buf *) b
              (*range*) (v pos - v len) (v pos)
              (* mem *) h0
              (* from*) (v pos - v len)
              (* to  *) (v pos - v len + 1);

    mbuffer_upd (* <-- NOTE: Serializing the leading "unused_bits" byte. *)
      (* buf *) b
      (*range*) (v pos - v len) (v pos)
      (* pos *) (pos - len)
      (* val *) leading_byte;

    (* Prf *) let h1 = HST.get () in
    (* Prf *) writable_modifies
              (* buf *) b
              (*range*) (v pos - v len) (v pos)
              (* mem *) h0
              (*other*) B.loc_none
              (* mem'*) h1;
    (* Prf *) writable_weaken
              (* buf *) b
              (*range*) (v pos - v len) (v pos)
              (* mem *) h1
              (* from*) (v pos - v len + 1)
              (* to  *) (v pos);

    store_bytes (* <-- NOTE: Serializing the following bytes. *)
      (* src *) value.bs_s
      (*range*) 0ul (len - 1ul)
      (* dst *) b
      (* pos *) (pos - len + 1ul);

    (* Prf *) let h2 = HST.get () in
    (* Prf *) B.modifies_buffer_from_to_elim
              (* buf *) b
              (*frame*) (pos - len) (pos - len + 1ul)
              (* new *) (B.loc_buffer_from_to b (pos - len + 1ul) pos)
              (* mem *) h1
              (* mem'*) h2;
    (* Prf *) Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v pos - v len) (v pos)) 1;
(*return*) (Mkbit_string_t?.bs_len value)
module ASN1.Low.Value.BIT_STRING

open ASN1.Base
open ASN1.Spec.Value.BIT_STRING

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

open LowParse.Low.Bytes

open FStar.Integers

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module B32 = FStar.Bytes

friend ASN1.Spec.Value.BIT_STRING

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length`, `ASN1.Spec.Value.OCTET_STRING` *)
/
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked LowParse.Low.Bytes.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.BIT_STRING.fst.checked ASN1.Spec.Value.BIT_STRING.fst.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.BIT_STRING.fst
len: ASN1.Base.asn1_value_int32_of_type ASN1.Base.BIT_STRING
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.BIT_STRING.serialize_asn1_bit_string (FStar.Integers.v
              len))
ASN1.Base.asn1_value_int32_of_type ASN1.Base.BIT_STRING 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 FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v ASN1.Base.__proj__Mkbit_string_t__item__bs_len LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer LowParse.Bytes.byte ASN1.Low.Base.size_t Prims.unit FStar.Seq.Properties.lemma_split FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq FStar.Integers.op_Subtraction LowStar.Monotonic.Buffer.modifies_buffer_from_to_elim FStar.Integers.op_Plus FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.loc_buffer_from_to FStar.UInt32.t FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Low.Bytes.store_bytes ASN1.Base.__proj__Mkbit_string_t__item__bs_s LowParse.Low.Base.writable_weaken LowParse.Low.Base.writable_modifies LowStar.Monotonic.Buffer.loc_none LowParse.Low.Base.mbuffer_upd FStar.Ghost.hide Prims.nat FStar.Int.Cast.uint32_to_uint8 ASN1.Base.__proj__Mkbit_string_t__item__bs_unused_bits ASN1.Spec.Value.BIT_STRING.lemma_serialize_asn1_bit_string_unfold
let serialize32_asn1_bit_string_backwards len =
  
fun
  (value: datatype_of_asn1_type BIT_STRING {v len == v (Mkbit_string_t?.bs_len value)})
  (#rrel: _)
  (#rel: _)
  (b: B.mbuffer byte rrel rel)
  (pos: size_t)
  ->
  lemma_serialize_asn1_bit_string_unfold (v len) (value);
  let h0 = HST.get () in
  let leading_byte:byte = FStar.Int.Cast.uint32_to_uint8 value.bs_unused_bits in
  writable_weaken b (v pos - v len) (v pos) h0 (v pos - v len) (v pos - v len + 1);
  mbuffer_upd b (v pos - v len) (v pos) (pos - len) leading_byte;
  let h1 = HST.get () in
  writable_modifies b (v pos - v len) (v pos) h0 B.loc_none h1;
  writable_weaken b (v pos - v len) (v pos) h1 (v pos - v len + 1) (v pos);
  store_bytes value.bs_s 0ul (len - 1ul) b (pos - len + 1ul);
  let h2 = HST.get () in
  B.modifies_buffer_from_to_elim b
    (pos - len)
    (pos - len + 1ul)
    (B.loc_buffer_from_to b (pos - len + 1ul) pos)
    h1
    h2;
  Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v pos - v len) (v pos)) 1;
  (Mkbit_string_t?.bs_len value)