val serialize32_asn1_integer_backwards_3byte_with_leading_zero
      (len: asn1_value_int32_of_type INTEGER)
    : Tot
    (serializer32_backwards ((serialize_asn1_integer (v len))
          `serialize_filter`
          (fun (value: datatype_of_asn1_type INTEGER {v len == length_of_asn1_integer value}) ->
              0x7FFFl < value && value <= 0xFFFFl)))
val serialize32_asn1_integer_backwards_3byte_with_leading_zero
      (len: asn1_value_int32_of_type INTEGER)
    : Tot
    (serializer32_backwards ((serialize_asn1_integer (v len))
          `serialize_filter`
          (fun (value: datatype_of_asn1_type INTEGER {v len == length_of_asn1_integer value}) ->
              0x7FFFl < value && value <= 0xFFFFl)))
let serialize32_asn1_integer_backwards_3byte_with_leading_zero
  (len: asn1_value_int32_of_type INTEGER)
: Tot (serializer32_backwards (serialize_asn1_integer (v len)
                               `serialize_filter`
                              (fun (value: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
                                 -> 0x7FFFl < value && value <= 0xFFFFl)))
= fun (value)//: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->(* Prf *) lemma_serialize_asn1_integer_unfold (length_of_asn1_integer value) value;
  (* Prf *) lemma_serialize_asn1_integer_size (length_of_asn1_integer value) value;
  (* Prf *) let h0 = HST.get () in
  (* Prf *) writable_weaken
            (* buf *) b
            (*range*) (v pos - 3) (v pos)
            (* mem *) h0
            (* from*) (v pos - 3)
            (* to  *) (v pos - 2);
  mbuffer_upd  (* <-- NOTE: Serializing the leading zero. *)
    (* buf *) b
    (*range*) (v pos - 3) (v pos)
    (* pos *) (pos - 3ul)
    (* val *) 0x00uy;
  (* Prf *) let h1 = HST.get () in
  (* Prf *) writable_modifies
            (* buf *) b
            (*range*) (v pos - 3) (v pos)
            (* mem *) h0
            (*other*) B.loc_none
            (* mem'*) h1;
  (* Prf *) writable_weaken
            (* buf *) b
            (*range*) (v pos - 3) (v pos)
            (* mem *) h1
            (* from*) (v pos - 2)
            (* to  *) (v pos);
  (* Prf *) LE.writable_store_pre
            (* buf *) b
            (* from*) (v pos - 2)
            (* len *) 2
            (*  p  *) (fun s -> E.be_to_n s == v #(Signed W32) value)
            (* mem *) h1;
  LE.store16_be_i (* <-- NOTE: Serializing the 2-byte integer. *)
    (* buf *) b
    (* pos *) (pos - 2ul)
    (* val *) (FStar.Int.Cast.int32_to_uint16 value);
  (* Prf *) let h2 = HST.get () in
  (* Prf *) LE.store_post_modifies
            (* buf *) b
            (* from*) (v pos - 2)
            (* len *) 2
            (*  p  *) (fun s -> E.be_to_n s == v #(Signed W32) value)
            (* mem *) h1
            (* mem'*) h2;
  (* Prf *) B.modifies_buffer_from_to_elim
            (* buf *) b
            (*frame*) (pos - 3ul) (pos - 2ul)
            (* new *) (B.loc_buffer_from_to b (pos - 2ul) pos)
            (* mem *) h1
            (* mem'*) h2;
  (* Prf *) Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v pos - 3) (v pos)) 1;
(*return*) 3ul
module ASN1.Low.Value.INTEGER

open ASN1.Base
open ASN1.Spec.Value.INTEGER
open ASN1.Low.Base
open LowParse.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 E = LowParse.Endianness
module LE = LowParse.Low.Endianness

friend ASN1.Spec.Value.INTEGER

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)

#set-options "--z3rlimit 256 --fuel 0 --ifuel 0"

(*
NOTE: Since there are no low-level machine-integer to bytes implementations
      available, the (big-endian) serialization of integers are tricky. For
      1-byte, 2-byte and 4-byte integers, we could use `LowStar.Endianness`
      16-bit, 32-bit integer store interfaces. For 3-byte, we need to store
      the first 2 bytes and the last byte separately.
*)
inline_for_extraction noextract
let serialize32_asn1_integer_backwards_1byte_without_leading_zero
  (len: asn1_value_int32_of_type INTEGER)
: Tot (serializer32_backwards (serialize_asn1_integer (v len)
                               `serialize_filter`
                              (fun (value: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
                                 -> 0l <= value && value <= 0x7Fl)))
= fun (value)//: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->(* Prf *) lemma_serialize_asn1_integer_unfold (length_of_asn1_integer value) value;
  (* Prf *) lemma_serialize_asn1_integer_size (length_of_asn1_integer value) value;
  let b0: byte = FStar.Int.Cast.int32_to_uint8 value in
  (* Prf *) E.reveal_be_to_n (Seq.create 1 b0);
  (* Prf *) E.reveal_be_to_n (Seq.slice (Seq.create 1 b0) 1 1);
  mbuffer_upd (* <-- NOTE: Serializing the 1-byte integer. *)
    (* dst *) b
    (*range*) (v pos - 1) (v pos)
    (* pos *) (pos - 1ul)
    (* val *) b0;
(*return*) 1ul

inline_for_extraction noextract
let serialize32_asn1_integer_backwards_2byte_with_leading_zero
  (len: asn1_value_int32_of_type INTEGER)
: Tot (serializer32_backwards (serialize_asn1_integer (v len)
                               `serialize_filter`
                              (fun (value: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
                                 -> 0x7Fl < value && value <= 0xFFl)))
= fun (value)//: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->(* Prf *) lemma_serialize_asn1_integer_unfold (length_of_asn1_integer value) value;
  (* Prf *) lemma_serialize_asn1_integer_size (length_of_asn1_integer value) value;
  (* Prf *) let h0 = HST.get () in
  (* Prf *) writable_weaken
            (* buf *) b
            (*range*) (v pos - 2) (v pos)
            (* mem *) h0
            (* from*) (v pos - 2)
            (* to  *) (v pos - 1);
  mbuffer_upd (* <-- NOTE: Serializing the leading zero. *)
    (* dst *) b
    (*range*) (v pos - 2) (v pos - 1)
    (* pos *) (pos - 2ul)
    (* val *) 0x00uy;
  (* Prf *) let h1 = HST.get () in
  (* Prf *) writable_modifies
            (* buf *) b
            (*range*) (v pos - 2) (v pos)
            (* mem *) h0
            (* loc *) (B.loc_none)
            (* mem *) h1;
  (* Prf *) writable_weaken
            (* buf *) b
            (*range*) (v pos - 2) (v pos)
            (* mem *) h1
            (* from*) (v pos - 1)
            (* to  *) (v pos);
  let b0: byte = FStar.Int.Cast.int32_to_uint8 value in
  (* Prf *) E.reveal_be_to_n (Seq.create 1 b0);
  (* Prf *) E.reveal_be_to_n (Seq.slice (Seq.create 1 b0) 1 1);
  mbuffer_upd (* <-- NOTE: Serializing the 1-byte integer. *)
    (* dst *) b
    (*range*) (v pos - 2) (v pos)
    (* pos *) (pos - 1ul)
    (* val *) b0;
  (* Prf *) let h2 = HST.get () in
  (* Prf *) B.modifies_buffer_from_to_elim
            (* buf *) b
            (*frame*) (pos - 2ul) (pos - 1ul)
            (* new *) (B.loc_buffer_from_to b (pos - 1ul) (pos))
            (* mem *) h1 h2;
  (* Prf *) Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v pos - 2) (v pos)) 1;
(*return*) 2ul

inline_for_extraction noextract
let serialize32_asn1_integer_backwards_2byte_without_leading_zero
  (len: asn1_value_int32_of_type INTEGER)
: Tot (serializer32_backwards (serialize_asn1_integer (v len)
                               `serialize_filter`
                              (fun (value: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
                                 -> 0xFFl < value && value <= 0x7FFFl)))
= fun (value)//: datatype_of_asn1_type INTEGER { v len == length_of_asn1_integer value })
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
->(* Prf *) lemma_serialize_asn1_integer_unfold (length_of_asn1_integer value) value;
  (* Prf *) lemma_serialize_asn1_integer_size (length_of_asn1_integer value) value;
  (* Prf *) let h0 = HST.get () in
  (* Prf *) LE.writable_store_pre
            (* buf *) b
            (* from*) (v pos - 2)
            (* len *) 2
            (*  p  *) (fun s -> E.be_to_n s == v #(Signed W32) value)
            (* mem *) h0;
  LE.store16_be_i  (* <-- NOTE: Serializing the 2-byte integer. *)
    (* buf *) b
    (* pos *) (pos - 2ul)
    (* val *) (FStar.Int.Cast.int32_to_uint16 value);
  (* Prf *) let h1 = HST.get () in
  (* Prf *) LE.store_post_modifies
            (* buf *) b
            (* from*) (v pos - 2)
            (* len *) 2
            (*  p  *) (fun s -> E.be_to_n s == v #(Signed W32) value)
            (* mem *) h0 h1;
(*return*) 2ul
/
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Failure.fsti.checked LowStar.Buffer.fst.checked LowParse.Low.Endianness.fst.checked LowParse.Endianness.fsti.checked LowParse.Bytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked ASN1.Spec.Value.INTEGER.fst.checked ASN1.Spec.Value.INTEGER.fst.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.INTEGER.fst
len: ASN1.Base.asn1_value_int32_of_type ASN1.Base.INTEGER
  -> ASN1.Low.Base.serializer32_backwards (LowParse.Spec.Combinators.serialize_filter (ASN1.Spec.Value.INTEGER.serialize_asn1_integer
              (FStar.Integers.v len))
          (fun value -> 0x7FFFl < value && value <= 0xFFFFl))
ASN1.Base.asn1_value_int32_of_type ASN1.Base.INTEGER LowParse.Spec.Combinators.parse_filter_refine ASN1.Base.datatype_of_asn1_type Prims.eq2 ASN1.Base.asn1_value_length_of_type FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Value.INTEGER.length_of_asn1_integer FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.l_or FStar.Integers.within_bounds Prims.l_and Prims.b2t FStar.Integers.op_Greater_Equals ASN1.Base.asn1_value_length_inbound_of_type Prims.op_AmpAmp FStar.Integers.op_Less FStar.Int32.__int_to_t FStar.Integers.op_Less_Equals Prims.bool LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer LowParse.Bytes.byte ASN1.Low.Base.size_t FStar.UInt32.__uint_to_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 LowStar.Monotonic.Buffer.loc_buffer_from_to LowParse.Low.Endianness.store_post_modifies FStar.Seq.Base.seq Prims.int Prims.op_GreaterThanOrEqual FStar.Endianness.be_to_n FStar.UInt32.t FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Endianness.store16_be_i FStar.Int.Cast.int32_to_uint16 LowParse.Low.Endianness.writable_store_pre 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.UInt8.__uint_to_t ASN1.Spec.Value.INTEGER.lemma_serialize_asn1_integer_size ASN1.Spec.Value.INTEGER.lemma_serialize_asn1_integer_unfold ASN1.Low.Base.serializer32_backwards LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.INTEGER.parse_asn1_integer_kind LowParse.Spec.Combinators.parse_filter ASN1.Spec.Value.INTEGER.parse_asn1_integer LowParse.Spec.Combinators.serialize_filter ASN1.Spec.Value.INTEGER.serialize_asn1_integer
let serialize32_asn1_integer_backwards_3byte_with_leading_zero
      (len: asn1_value_int32_of_type INTEGER)
    : Tot
    (serializer32_backwards ((serialize_asn1_integer (v len))
          `serialize_filter`
          (fun (value: datatype_of_asn1_type INTEGER {v len == length_of_asn1_integer value}) ->
              0x7FFFl < value && value <= 0xFFFFl))) =
  
fun value (#rrel: _) (#rel: _) (b: B.mbuffer byte rrel rel) (pos: size_t) ->
  lemma_serialize_asn1_integer_unfold (length_of_asn1_integer value) value;
  lemma_serialize_asn1_integer_size (length_of_asn1_integer value) value;
  let h0 = HST.get () in
  writable_weaken b (v pos - 3) (v pos) h0 (v pos - 3) (v pos - 2);
  mbuffer_upd b (v pos - 3) (v pos) (pos - 3ul) 0x00uy;
  let h1 = HST.get () in
  writable_modifies b (v pos - 3) (v pos) h0 B.loc_none h1;
  writable_weaken b (v pos - 3) (v pos) h1 (v pos - 2) (v pos);
  LE.writable_store_pre b (v pos - 2) 2 (fun s -> E.be_to_n s == v #(Signed W32) value) h1;
  LE.store16_be_i b (pos - 2ul) (FStar.Int.Cast.int32_to_uint16 value);
  let h2 = HST.get () in
  LE.store_post_modifies b (v pos - 2) 2 (fun s -> E.be_to_n s == v #(Signed W32) value) h1 h2;
  B.modifies_buffer_from_to_elim b
    (pos - 3ul)
    (pos - 2ul)
    (B.loc_buffer_from_to b (pos - 2ul) pos)
    h1
    h2;
  Seq.lemma_split (Seq.slice (B.as_seq h2 b) (v pos - 3) (v pos)) 1;
  3ul