val read_bounded_integer_ct
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
  (#rrel: _)
  (#rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: HST.Stack (bounded_integer (U32.v i))
  (requires (fun h ->
    live_slice h sl /\
    U32.v pos + 4 <= U32.v sl.len
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    valid_content (parse_bounded_integer (U32.v i)) h sl pos res
  ))
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
val read_bounded_integer_ct
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
  (#rrel: _)
  (#rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: HST.Stack (bounded_integer (U32.v i))
  (requires (fun h ->
    live_slice h sl /\
    U32.v pos + 4 <= U32.v sl.len
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    valid_content (parse_bounded_integer (U32.v i)) h sl pos res
  ))
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
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
FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice LowParse.BitFields.__proj__Mkuint_t__item__get_bitfield_gen LowParse.BitFields.uint32 FStar.UInt32.mul FStar.UInt32.__uint_to_t FStar.UInt32.sub LowParse.Spec.BoundedInt.bounded_integer LowStar.Endianness.u32 LowStar.Endianness.load32_be_i LowParse.Slice.buffer_srel_of_srel LowParse.Slice.__proj__Mkslice__item__base Prims.unit LowParse.Endianness.BitFields.bitfield_be_to_n_slice FStar.Seq.Base.slice LowParse.Slice.bytes_of_slice_from LowParse.Spec.Int.parse_u32_spec LowParse.Spec.BoundedInt.decode_bounded_integer_injective LowParse.Low.Base.Spec.valid_facts LowParse.Spec.Int.parse_u32_kind LowParse.Spec.Int.parse_u32 LowParse.Low.Base.valid_total_constant_size LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
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
val read_bounded_integer_ct
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
  (#rrel: _)
  (#rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: HST.Stack (bounded_integer (U32.v i))
  (requires (fun h ->
    live_slice h sl /\
    U32.v pos + 4 <= U32.v sl.len
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    valid_content (parse_bounded_integer (U32.v i)) h sl pos res
  ))

    i: FStar.UInt32.t{1 <= FStar.UInt32.v i /\ FStar.UInt32.v i <= 4} ->
    sl: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> FStar.HyperStack.ST.Stack (LowParse.Spec.BoundedInt.bounded_integer (FStar.UInt32.v i))