val serialize32_bounded_integer_3 : unit -> Tot (serializer32 (serialize_bounded_integer 3))
let serialize32_bounded_integer_3 () =
  fun (v: bounded_integer 3) #rrel #rel out pos ->
  bounded_integer_prop_equiv 3 v;
  E.reveal_n_to_be 3 (U32.v v);
  assert_norm (pow2 8 == 256);
  let lo = Cast.uint32_to_uint8 v in
  mbuffer_upd out (Ghost.hide (U32.v pos)) (Ghost.hide (U32.v pos + 3)) (pos `U32.add` 2ul) lo;
  let hi' = div256 v in
  FStar.Math.Lemmas.small_mod (U32.v hi') (pow2 16);
  let hi = Cast.uint32_to_uint16 hi' in
  let h1 = HST.get () in
  LE.writable_weaken out (U32.v pos) (U32.v pos + 3) h1 (U32.v pos) (U32.v pos + 2);
  LE.writable_store_pre out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v hi) h1;
  LE.store16_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) out pos hi;
  let h2 = HST.get () in
  LE.store_post_modifies out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v hi) h1 h2;
  B.modifies_buffer_from_to_elim out (pos `U32.add` 2ul) (pos `U32.add` 3ul) (B.loc_buffer_from_to out pos (pos `U32.add` 2ul)) h1 h2;
  assert (Seq.slice (B.as_seq h2 out) (U32.v pos + 2) (U32.v pos + 3) `Seq.equal` Seq.create 1 lo);
  3ul
val serialize32_bounded_integer_3 : unit -> Tot (serializer32 (serialize_bounded_integer 3))
let serialize32_bounded_integer_3 () =
fun (v: bounded_integer 3) #rrel #rel out pos ->
  bounded_integer_prop_equiv 3 v;
  E.reveal_n_to_be 3 (U32.v v);
  assert_norm (pow2 8 == 256);
  let lo = Cast.uint32_to_uint8 v in
  mbuffer_upd out (Ghost.hide (U32.v pos)) (Ghost.hide (U32.v pos + 3)) (pos `U32.add` 2ul) lo;
  let hi' = div256 v in
  FStar.Math.Lemmas.small_mod (U32.v hi') (pow2 16);
  let hi = Cast.uint32_to_uint16 hi' in
  let h1 = HST.get () in
  LE.writable_weaken out (U32.v pos) (U32.v pos + 3) h1 (U32.v pos) (U32.v pos + 2);
  LE.writable_store_pre out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v hi) h1;
  LE.store16_be_i out pos hi;
  let h2 = HST.get () in
  LE.store_post_modifies out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v hi) h1 h2;
  B.modifies_buffer_from_to_elim out
    (pos `U32.add` 2ul)
    (pos `U32.add` 3ul)
    (B.loc_buffer_from_to out pos (pos `U32.add` 2ul))
    h1
    h2;
  assert ((Seq.slice (B.as_seq h2 out) (U32.v pos + 2) (U32.v pos + 3))
      `Seq.equal`
      (Seq.create 1 lo));
  3ul
LowParse.Low.BoundedInt.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.BoundedInt.fst.checked LowParse.Low.Endianness.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Endianness.BitFields.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
LowParse.Low.BoundedInt.fst
Prims.unit LowParse.Spec.BoundedInt.bounded_integer LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t FStar.UInt32.__uint_to_t Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq Prims.op_Addition FStar.UInt32.v FStar.Seq.Base.create LowStar.Monotonic.Buffer.modifies_buffer_from_to_elim FStar.UInt32.add LowStar.Monotonic.Buffer.loc_buffer_from_to LowParse.Low.Endianness.store_post_modifies FStar.Seq.Base.seq Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt16.n FStar.Endianness.be_to_n FStar.UInt16.v FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Endianness.store16_be_i LowParse.Low.Endianness.writable_store_pre LowParse.Low.Base.writable_weaken FStar.UInt16.t Prims.op_Equality Prims.op_Modulus Prims.pow2 FStar.Int.Cast.uint32_to_uint16 FStar.Math.Lemmas.small_mod Prims.op_Division LowParse.Low.BoundedInt.div256 LowParse.Low.Base.mbuffer_upd FStar.Ghost.hide Prims.nat FStar.UInt8.t FStar.UInt8.v FStar.Int.Cast.uint32_to_uint8 FStar.Pervasives.assert_norm LowParse.Endianness.reveal_n_to_be LowParse.Spec.BoundedInt.bounded_integer_prop_equiv
module LowParse.Low.BoundedInt
open LowParse.Low.Combinators
module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module E = LowParse.Endianness.BitFields
module BF = LowParse.BitFields
module LE = LowParse.Low.Endianness
module Cast = FStar.Int.Cast

friend LowParse.Spec.BoundedInt

inline_for_extraction
let mul256 (x: U16.t) : Tot (y: U32.t { U32.v y == 256 `Prims.op_Multiply` U16.v x }) =
  assert_norm (pow2 8 == 256);
  FStar.Math.Lemmas.pow2_lt_compat 32 24;
  FStar.Math.Lemmas.pow2_lt_compat 24 16;
  FStar.Math.Lemmas.pow2_lt_compat 16 8;
  FStar.Math.Lemmas.pow2_plus 8 16;
  FStar.Math.Lemmas.small_mod (U16.v x `Prims.op_Multiply` 256) (pow2 32);
  FStar.UInt.shift_left_value_lemma #32 (U16.v x) 8;
  Cast.uint16_to_uint32 x `U32.shift_left` 8ul

inline_for_extraction
let div256 (x: U32.t) : Tot (y: U32.t { U32.v y == U32.v x / 256 }) =
  assert_norm (pow2 8 == 256);
  FStar.UInt.shift_right_value_lemma #32 (U32.v x) 8;
  x `U32.shift_right` 8ul

(* bounded integers *)

let read_bounded_integer_1 () =
  [@inline_let]
  let _ =
    decode_bounded_integer_injective 1
  in
  make_total_constant_size_reader 1 1ul #(bounded_integer 1) (decode_bounded_integer 1) () (fun #rrel #rel input pos ->
    let h = HST.get () in
    E.index_be_to_n (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 1)) 0;
    E.lemma_be_to_n_is_bounded (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 1));
    let r = B.index input pos in
    Cast.uint8_to_uint32 r
  )

let read_bounded_integer_2 () =
  [@inline_let] let _ =
    decode_bounded_integer_injective 2
  in
  make_total_constant_size_reader 2 2ul #(bounded_integer 2) (decode_bounded_integer 2) () (fun #rrel #rel input pos ->
    let h = HST.get () in
    let r = LE.load16_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) input pos in
    E.lemma_be_to_n_is_bounded (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 2));
    Cast.uint16_to_uint32 r
  )

#push-options "--z3rlimit 16"

let read_bounded_integer_3 () =
  [@inline_let] let _ =
    decode_bounded_integer_injective 3
  in
  make_total_constant_size_reader 3 3ul #(bounded_integer 3) (decode_bounded_integer 3) () (fun #rrel #rel input pos ->
    let h = HST.get () in
    Seq.lemma_split (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 3)) 2;
    E.reveal_be_to_n (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 3));
    let lo = B.index input (pos `U32.add` 2ul) in
    let hi = LE.load16_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) input pos in
    E.lemma_be_to_n_is_bounded (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 2));
    E.lemma_be_to_n_is_bounded (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 3));
    assert_norm (pow2 8 == 256);
    Cast.uint8_to_uint32 lo `U32.add` (mul256 hi)
  )

#pop-options

let read_bounded_integer_4 () =
  [@inline_let] let _ =
    decode_bounded_integer_injective 4
  in
  make_total_constant_size_reader 4 4ul #(bounded_integer 4) (decode_bounded_integer 4) () (fun #rrel #rel input pos ->
    let h = HST.get () in
    E.lemma_be_to_n_is_bounded (Seq.slice (B.as_seq h input) (U32.v pos) (U32.v pos + 4));
    LE.load32_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) input pos
  )

let read_bounded_integer_ct
  i #rrel #rel sl pos
= let h = HST.get () in
  valid_total_constant_size h (parse_bounded_integer (U32.v i)) (U32.v i) sl pos;
  valid_facts (parse_bounded_integer (U32.v i)) h sl pos;
  valid_total_constant_size h parse_u32 4 sl pos;
  valid_facts parse_u32 h sl pos;
  decode_bounded_integer_injective (U32.v i);
  parse_u32_spec (bytes_of_slice_from h sl pos);
  E.bitfield_be_to_n_slice (Seq.slice (bytes_of_slice_from h sl pos) 0 4) 0 (U32.v i);
  let r = LE.load32_be_i sl.base pos in
  BF.uint32.BF.get_bitfield_gen r (8ul `U32.mul` (4ul `U32.sub` i)) 32ul

let serialize32_bounded_integer_1 () =
  fun (v: bounded_integer 1) #rrel #rel out pos ->
  bounded_integer_prop_equiv 1 v;
  E.index_n_to_be 1 (U32.v v) 0;
  mbuffer_upd out (Ghost.hide (U32.v pos)) (Ghost.hide (U32.v pos + 1)) pos (Cast.uint32_to_uint8 v);
  1ul

let serialize32_bounded_integer_2 () =
  fun (v: bounded_integer 2) #rrel #rel out pos ->
  bounded_integer_prop_equiv 2 v;
  let h = HST.get () in
  let v' = (Cast.uint32_to_uint16 v) in
  LE.writable_store_pre out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v v') h;
  LE.store16_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) out pos v';
  let h' = HST.get () in
  LE.store_post_modifies out (U32.v pos) 2 (fun s -> E.be_to_n s == U16.v v') h h';
  2ul

#push-options "--z3rlimit 16"
val serialize32_bounded_integer_3 : unit -> Tot (serializer32 (serialize_bounded_integer 3))
_: Prims.unit
  -> LowParse.Low.Base.serializer32 (LowParse.Spec.BoundedInt.serialize_bounded_integer 3)