val read_u64_le : leaf_reader parse_u64_le
let read_u64_le =
  decode_u64_le_injective ();
  make_total_constant_size_reader 8 8ul
    #U64.t
    decode_u64_le
    ()
    (fun #rrel #rel sl pos ->
      LE.load64_le_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) sl pos)
val read_u64_le : leaf_reader parse_u64_le
let read_u64_le =
decode_u64_le_injective ();
make_total_constant_size_reader 8
  8ul
  #U64.t
  decode_u64_le
  ()
  (fun #rrel #rel sl pos -> LE.load64_le_i sl pos)
LowParse.Low.Int.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Int.fst.checked LowParse.Low.Endianness.fst.checked LowParse.Low.Combinators.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked
LowParse.Low.Int.fst
LowParse.Low.Combinators.make_total_constant_size_reader FStar.UInt32.__uint_to_t FStar.UInt64.t LowParse.Spec.Int.decode_u64_le LowStar.Monotonic.Buffer.srel LowParse.Bytes.byte LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.t LowStar.Endianness.load64_le_i LowStar.Endianness.u64 Prims.unit LowParse.Spec.Int.decode_u64_le_injective
module LowParse.Low.Int
open LowParse.Low.Combinators

module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module E = FStar.Endianness
module LE = LowParse.Low.Endianness

friend LowParse.Spec.Int

let read_u8 : leaf_reader parse_u8 =
  decode_u8_injective ();
  leaf_reader_ext
    (make_total_constant_size_reader 1 1ul
      decode_u8
      ()
      (fun #rrel #rel b pos -> B.index b pos)
    )
    _
    (fun _ -> ())

inline_for_extraction
let read_u16 =
  decode_u16_injective ();
  make_total_constant_size_reader 2 2ul
    #U16.t
    decode_u16
    ()
    (fun #rrel #rel sl pos ->
      LE.load16_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) sl pos)

inline_for_extraction
let read_u32 =
  decode_u32_injective ();
  make_total_constant_size_reader 4 4ul
    #U32.t
    decode_u32
    ()
    (fun #rrel #rel sl pos ->
      LE.load32_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) sl pos)

inline_for_extraction
let read_u64 =
  decode_u64_injective ();
  make_total_constant_size_reader 8 8ul
    #U64.t
    decode_u64
    ()
    (fun #rrel #rel sl pos ->
      LE.load64_be_i (* #(Ghost.hide rrel) #(Ghost.hide rel) *) sl pos)

inline_for_extraction
val read_u64_le : leaf_reader parse_u64_le
LowParse.Low.Base.leaf_reader LowParse.Spec.Int.parse_u64_le