val serialize32_big_integer_as_octet_string_backwards
  (len: asn1_value_int32_of_big_integer)
: Tot (serializer32_backwards (serialize_big_integer_as_octet_string len))
val serialize32_big_integer_as_octet_string_backwards
  (len: asn1_value_int32_of_big_integer)
: Tot (serializer32_backwards (serialize_big_integer_as_octet_string len))
let serialize32_big_integer_as_octet_string_backwards len
= fun (x)
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->  (* prf *) let h0 = HST.get () in
    (* Prf *) lemma_serialize_big_integer_as_octet_string_unfold len (x);
    (* Prf *) writable_weaken
              (* buf *) b
              (*range*) (v (pos - len)) (v pos)
              (* mem *) h0
              (* from*) (v (pos - x.ASN1.Base.len))
              (* to  *) (v pos);
    store_bytes
      (* src *) (x.s)
      (* from*) 0ul
      (* to  *) (x.ASN1.Base.len)
      (* dst *) b
      (* pos *) (pos - (x.ASN1.Base.len));

    if (B32.get (x.s) 0ul >= 0x80uy) then
    ( let h1 = HST.get () in
      (* Prf *) writable_modifies
                (* buf *) b
                (*range*) (v (pos - len)) (v pos)
                (* mem *) h0
                (*other*) B.loc_none
                (* mem'*) h1;
      (* Prf *) writable_weaken
                (* buf *) b
                (*range*) (v (pos - len)) (v pos)
                (* mem *) h1
                (* from*) (v (pos - len))
                (* to  *) (v (pos - x.ASN1.Base.len));
      mbuffer_upd
        (* buf *) b
        (*range*) (v (pos - len)) (v pos)
        (* pos *) (pos - len)
        (* val *) 0x00uy;
      (* Prf *) let h2 = HST.get () in
      (* Prf *) B.modifies_buffer_from_to_elim
            (* buf *) b
            (*frame*) (pos - x.ASN1.Base.len) (pos)
            (* new *) (B.loc_buffer_from_to b (pos - len) (pos - x.ASN1.Base.len))
            (* mem *) h1
            (* mem'*) h2;
  (* Prf *) Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v (pos - len)) (v pos)) 1 );

(* retuen *) len
module ASN1.Low.Value.BigInteger

open ASN1.Base
open ASN1.Low.Base
open ASN1.Low.Tag
open ASN1.Low.Length
open ASN1.Low.Value.OCTET_STRING
open ASN1.Low.Bytes32
open ASN1.Spec.Value.BigInteger
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
open LowParse.Low.Bytes

open FStar.Integers
module B32 = FStar.Bytes

friend ASN1.Spec.Value.BigInteger

#set-options "--z3rlimit 32 --ifuel 0 --ifuel 0"

// let serialize32_asn1_length_of_big_integer_backwards
// : serializer32_backwards (serialize_asn1_length_of_big_integer)
// = serialize32_asn1_length_of_bound_backwards 1ul (asn1_int32_max - 6ul)
/
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked LowParse.Low.Bytes.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.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.BigInteger.fst.checked ASN1.Spec.Value.BigInteger.fst.checked ASN1.Low.Value.OCTET_STRING.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Bytes32.fst.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.BigInteger.fst
len: ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.BigInteger.serialize_big_integer_as_octet_string
          len)
ASN1.Spec.Value.BigInteger.asn1_value_int32_of_big_integer ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string_prop LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer LowParse.Bytes.byte ASN1.Low.Base.size_t FStar.UInt32.t Prims.unit FStar.Integers.op_Greater_Equals FStar.Integers.Unsigned FStar.Integers.W8 FStar.Bytes.get ASN1.Base.__proj__Mkoctet_string_t__item__s FStar.UInt32.__uint_to_t FStar.UInt8.__uint_to_t FStar.Seq.Properties.lemma_split FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq FStar.Integers.v FStar.Integers.W32 FStar.Integers.op_Subtraction LowStar.Monotonic.Buffer.modifies_buffer_from_to_elim ASN1.Base.__proj__Mkoctet_string_t__item__len LowStar.Monotonic.Buffer.loc_buffer_from_to FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Low.Base.mbuffer_upd FStar.Ghost.hide Prims.nat LowParse.Low.Base.writable_weaken LowParse.Low.Base.writable_modifies LowStar.Monotonic.Buffer.loc_none Prims.bool LowParse.Low.Bytes.store_bytes ASN1.Spec.Value.BigInteger.lemma_serialize_big_integer_as_octet_string_unfold
let serialize32_big_integer_as_octet_string_backwards len =
  
fun x (#rrel: _) (#rel: _) (b: B.mbuffer byte rrel rel) (pos: size_t) ->
  let h0 = HST.get () in
  lemma_serialize_big_integer_as_octet_string_unfold len (x);
  writable_weaken b (v (pos - len)) (v pos) h0 (v (pos - x.ASN1.Base.len)) (v pos);
  store_bytes (x.s) 0ul (x.ASN1.Base.len) b (pos - (x.ASN1.Base.len));
  if (B32.get (x.s) 0ul >= 0x80uy)
  then
    (let h1 = HST.get () in
      writable_modifies b (v (pos - len)) (v pos) h0 B.loc_none h1;
      writable_weaken b (v (pos - len)) (v pos) h1 (v (pos - len)) (v (pos - x.ASN1.Base.len));
      mbuffer_upd b (v (pos - len)) (v pos) (pos - len) 0x00uy;
      let h2 = HST.get () in
      B.modifies_buffer_from_to_elim b
        (pos - x.ASN1.Base.len)
        (pos)
        (B.loc_buffer_from_to b (pos - len) (pos - x.ASN1.Base.len))
        h1
        h2;
      Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v (pos - len)) (v pos)) 1);
  len