val read_bounded_integer_1 : unit -> Tot (leaf_reader (parse_bounded_integer 1))
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
  )
val read_bounded_integer_1 : unit -> Tot (leaf_reader (parse_bounded_integer 1))
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)
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.Low.Combinators.make_total_constant_size_reader FStar.UInt32.__uint_to_t LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.decode_bounded_integer LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t FStar.Int.Cast.uint8_to_uint32 LowStar.Monotonic.Buffer.index FStar.Endianness.lemma_be_to_n_is_bounded FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq FStar.UInt32.v Prims.op_Addition LowParse.Endianness.index_be_to_n FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Spec.BoundedInt.decode_bounded_integer_injective LowParse.Low.Base.leaf_reader LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.parse_bounded_integer
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 *)
val read_bounded_integer_1 : unit -> Tot (leaf_reader (parse_bounded_integer 1))
_: Prims.unit -> LowParse.Low.Base.leaf_reader (LowParse.Spec.BoundedInt.parse_bounded_integer 1)