val write_bounded_integer_2_weak: unit -> Tot (leaf_writer_weak (serialize_bounded_integer 2))
let write_bounded_integer_2_weak (_ : unit) : Tot (leaf_writer_weak (serialize_bounded_integer 2)) =
  leaf_writer_weak_of_strong_constant_size (write_bounded_integer_2 ()) 2ul ()
val write_bounded_integer_2_weak: unit -> Tot (leaf_writer_weak (serialize_bounded_integer 2))
let write_bounded_integer_2_weak (_: unit) : Tot (leaf_writer_weak (serialize_bounded_integer 2)) =
leaf_writer_weak_of_strong_constant_size (write_bounded_integer_2 ()) 2ul ()
LowParse.Low.BoundedInt.fsti.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowParse.Spec.BoundedInt.fsti.checked LowParse.Low.Base.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked
LowParse.Low.BoundedInt.fsti
Prims.unit LowParse.Low.Base.leaf_writer_weak_of_strong_constant_size LowParse.Spec.BoundedInt.parse_bounded_integer_kind LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.BoundedInt.serialize_bounded_integer LowParse.Low.BoundedInt.write_bounded_integer_2 FStar.UInt32.__uint_to_t LowParse.Low.Base.leaf_writer_weak
module LowParse.Low.BoundedInt
include LowParse.Spec.BoundedInt
include LowParse.Low.Base

module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Monotonic.Buffer
module U64 = FStar.UInt64

(* bounded integers *)

inline_for_extraction
val read_bounded_integer_1 : unit -> Tot (leaf_reader (parse_bounded_integer 1))

inline_for_extraction
val read_bounded_integer_2 : unit -> Tot (leaf_reader (parse_bounded_integer 2))

inline_for_extraction
val read_bounded_integer_3 : unit -> Tot (leaf_reader (parse_bounded_integer 3))

inline_for_extraction
val read_bounded_integer_4 : unit -> Tot (leaf_reader (parse_bounded_integer 4))

inline_for_extraction
noextract
let read_bounded_integer
  (i: integer_size)
: Tot (leaf_reader (parse_bounded_integer i))
= [@inline_let]
  let _ = integer_size_values i in
  match i with
  | 1 -> read_bounded_integer_1 ()
  | 2 -> read_bounded_integer_2 ()
  | 3 -> read_bounded_integer_3 ()
  | 4 -> read_bounded_integer_4 ()

let read_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
: Tot (leaf_reader (parse_bounded_integer (U32.v i)))
= fun #rrel #rel sl pos ->
  if i = 1ul
  then read_bounded_integer_1 () sl pos
  else if i = 2ul
  then read_bounded_integer_2 () sl pos
  else if i = 3ul
  then read_bounded_integer_3 () sl pos
  else read_bounded_integer_4 () sl pos

inline_for_extraction
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
  ))

inline_for_extraction
noextract
let validate_bounded_integer
  (i: integer_size) // must be a constant
: Tot (validator (parse_bounded_integer i))
= validate_total_constant_size (parse_bounded_integer i) (U64.uint_to_t i) ()

inline_for_extraction
let validate_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
: Tot (validator (parse_bounded_integer (U32.v i)))
= validate_total_constant_size (parse_bounded_integer (U32.v i)) (FStar.Int.Cast.uint32_to_uint64 i) ()

inline_for_extraction
noextract
let validate_bounded_integer_le
  (i: integer_size) // must be a constant
: Tot (validator (parse_bounded_integer_le i))
= validate_total_constant_size (parse_bounded_integer_le i) (U64.uint_to_t i) ()

inline_for_extraction
noextract
let jump_bounded_integer
  (i: integer_size) // must be a constant
: Tot (jumper (parse_bounded_integer i))
= jump_constant_size (parse_bounded_integer i) (U32.uint_to_t i) ()

inline_for_extraction
let jump_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
: Tot (jumper (parse_bounded_integer (U32.v i)))
= jump_constant_size (parse_bounded_integer (U32.v i)) (i) ()

inline_for_extraction
noextract
let jump_bounded_integer_le
  (i: integer_size) // must be a constant
: Tot (jumper (parse_bounded_integer_le i))
= jump_constant_size (parse_bounded_integer_le i) (U32.uint_to_t i) ()

inline_for_extraction
val serialize32_bounded_integer_1 : unit -> Tot (serializer32 (serialize_bounded_integer 1))

inline_for_extraction
val serialize32_bounded_integer_2 : unit -> Tot (serializer32 (serialize_bounded_integer 2))

inline_for_extraction
val serialize32_bounded_integer_3 : unit -> Tot (serializer32 (serialize_bounded_integer 3))

inline_for_extraction
val serialize32_bounded_integer_4 : unit -> Tot (serializer32 (serialize_bounded_integer 4))

inline_for_extraction
let write_bounded_integer_1 () = leaf_writer_strong_of_serializer32 (serialize32_bounded_integer_1 ()) ()

inline_for_extraction
let write_bounded_integer_2 () = leaf_writer_strong_of_serializer32 (serialize32_bounded_integer_2 ()) ()

inline_for_extraction
let write_bounded_integer_3 () = leaf_writer_strong_of_serializer32 (serialize32_bounded_integer_3 ()) ()

inline_for_extraction
let write_bounded_integer_4 () = leaf_writer_strong_of_serializer32 (serialize32_bounded_integer_4 ()) ()

inline_for_extraction
noextract
let write_bounded_integer
  (i: integer_size)
: Tot (leaf_writer_strong (serialize_bounded_integer i))
= [@inline_let]
  let _ = integer_size_values i in
  match i with
  | 1 -> write_bounded_integer_1 ()
  | 2 -> write_bounded_integer_2 ()
  | 3 -> write_bounded_integer_3 ()
  | 4 -> write_bounded_integer_4 ()

inline_for_extraction
let write_bounded_integer'
  (i: U32.t { 1 <= U32.v i /\ U32.v i <= 4 })
: Tot (leaf_writer_strong (serialize_bounded_integer (U32.v i)))
= fun v #rrel #rel sl pos ->
  if i = 1ul
  then write_bounded_integer_1 () v sl pos
  else if i = 2ul
  then write_bounded_integer_2 () v sl pos
  else if i = 3ul
  then write_bounded_integer_3 () v sl pos
  else write_bounded_integer_4 () v sl pos

inline_for_extraction
let write_bounded_integer_1_weak (_ : unit) : Tot (leaf_writer_weak (serialize_bounded_integer 1)) =
  leaf_writer_weak_of_strong_constant_size (write_bounded_integer_1 ()) 1ul ()

inline_for_extraction
val write_bounded_integer_2_weak: unit -> Tot (leaf_writer_weak (serialize_bounded_integer 2))
_: Prims.unit
  -> LowParse.Low.Base.leaf_writer_weak (LowParse.Spec.BoundedInt.serialize_bounded_integer 2)