val serialize32_big_integer_as_octet_string_TLV_backwards (_:unit)
: Tot (serializer32_backwards (serialize_big_integer_as_octet_string_TLV))
val serialize32_big_integer_as_octet_string_TLV_backwards (_:unit)
: Tot (serializer32_backwards (serialize_big_integer_as_octet_string_TLV))
let serialize32_big_integer_as_octet_string_TLV_backwards ()
= serialize32_tagged_union_backwards
  (* lst *) (serialize32_asn1_tag_of_type_backwards INTEGER
             `serialize32_nondep_then_backwards`
             serialize32_asn1_length_of_big_integer_backwards)
  (* ltg *) (parser_tag_of_big_integer_as_octet_string_impl)
  (* ls  *) (fun parser_tag -> (serialize32_synth_backwards
                              (* ls *) (weak_kind_of_big_integer
                                        `serialize32_weaken_backwards`
                                        serialize32_big_integer_as_octet_string_backwards (msnd parser_tag))
                              (* f2 *) (synth_big_integer_as_octet_string_V parser_tag)
                              (* g1 *) (synth_big_integer_as_octet_string_V_inverse parser_tag)
                              (* g1'*) (synth_big_integer_as_octet_string_V_inverse parser_tag)
                              (* prf*) ()))
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)

inline_for_extraction
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

// noextract inline_for_extraction
// let parser_tag_of_big_integer_as_octet_string_impl
//   (x: big_integer_as_octet_string_t)
// : Tot (tg: (the_asn1_tag INTEGER & asn1_value_int32_of_big_integer)
//            { tg == parser_tag_of_big_integer_as_octet_string x })
// = let (.[]) = B32.index in
//   if ((dsnd x).[0] >= 0x80uy) then
//   ( (INTEGER, dfst x + 1ul) )
//   else
//   ( (INTEGER, dfst x) )
/
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
_: Prims.unit
  -> ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.BigInteger.serialize_big_integer_as_octet_string_TLV

Prims.unit 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_of_bound_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 FStar.UInt32.__uint_to_t FStar.Integers.op_Subtraction ASN1.Base.asn1_int32_max FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag ASN1.Base.INTEGER FStar.UInt32.t Prims.b2t Prims.op_Negation Prims.op_BarBar Prims.op_LessThan FStar.UInt32.v Prims.op_Subtraction LowParse.Spec.Combinators.nondep_then ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Value.BigInteger.parse_asn1_length_of_big_integer LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Value.BigInteger.serialize_asn1_length_of_big_integer ASN1.Low.Base.serialize32_nondep_then_backwards ASN1.Low.Tag.serialize32_asn1_tag_of_type_backwards ASN1.Low.Value.BigInteger.serialize32_asn1_length_of_big_integer_backwards ASN1.Spec.Value.BigInteger.big_integer_as_octet_string_t ASN1.Spec.Value.BigInteger.parser_tag_of_big_integer_as_octet_string ASN1.Low.Value.BigInteger.parser_tag_of_big_integer_as_octet_string_impl ASN1.Spec.Value.BigInteger.weak_kind_of_big_integer LowParse.Spec.Combinators.parse_synth ASN1.Spec.Value.BigInteger.valid_big_integer_as_octet_string_prop ASN1.Low.Base.msnd LowParse.Spec.Base.refine_with_tag LowParse.Spec.Base.weaken ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_kind ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string_V LowParse.Spec.Base.parser LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.serialize_weaken ASN1.Spec.Value.BigInteger.serialize_big_integer_as_octet_string ASN1.Spec.Value.BigInteger.synth_big_integer_as_octet_string_V_inverse LowParse.Spec.Base.serializer ASN1.Low.Base.serialize32_synth_backwards ASN1.Low.Base.serialize32_weaken_backwards ASN1.Low.Value.BigInteger.serialize32_big_integer_as_octet_string_backwards ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_TLV_kind ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_TLV ASN1.Spec.Value.BigInteger.serialize_big_integer_as_octet_string_TLV
let serialize32_big_integer_as_octet_string_TLV_backwards () =
  
serialize32_tagged_union_backwards ((serialize32_asn1_tag_of_type_backwards INTEGER)
    `serialize32_nondep_then_backwards`
    serialize32_asn1_length_of_big_integer_backwards)
  (parser_tag_of_big_integer_as_octet_string_impl)
  (fun parser_tag ->
      (serialize32_synth_backwards (weak_kind_of_big_integer
            `serialize32_weaken_backwards`
            (serialize32_big_integer_as_octet_string_backwards (msnd parser_tag)))
          (synth_big_integer_as_octet_string_V parser_tag)
          (synth_big_integer_as_octet_string_V_inverse parser_tag)
          (synth_big_integer_as_octet_string_V_inverse parser_tag)
          ()))