val index_32_be (b: B.buffer UInt8.t) (i: UInt32.t)
    : Stack UInt32.t
      (requires (fun h -> B.live h b /\ B.length b % 4 = 0 /\ UInt32.v i < B.length b / 4))
      (ensures
        (fun h0 r h1 ->
            B.(modifies loc_none h0 h1) /\
            r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i)))
let index_32_be (b: B.buffer UInt8.t) (i: UInt32.t):
  Stack UInt32.t
    (requires (fun h ->
      B.live h b /\ B.length b % 4 = 0 /\
      UInt32.v i < B.length b / 4))
    (ensures (fun h0 r h1 ->
      B.(modifies loc_none h0 h1) /\
      r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i)))
=
  load32_be (B.sub b FStar.UInt32.(4ul *^ i) 4ul)
val index_32_be (b: B.buffer UInt8.t) (i: UInt32.t)
    : Stack UInt32.t
      (requires (fun h -> B.live h b /\ B.length b % 4 = 0 /\ UInt32.v i < B.length b / 4))
      (ensures
        (fun h0 r h1 ->
            B.(modifies loc_none h0 h1) /\
            r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i)))
let index_32_be (b: B.buffer UInt8.t) (i: UInt32.t)
    : Stack UInt32.t
      (requires (fun h -> B.live h b /\ B.length b % 4 = 0 /\ UInt32.v i < B.length b / 4))
      (ensures
        (fun h0 r h1 ->
            B.(modifies loc_none h0 h1) /\
            r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i))) =
load32_be (B.sub b FStar.UInt32.(4ul *^ i) 4ul)
C.Endianness.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Krml.Endianness.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Classical.fsti.checked
C.Endianness.fst
LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t C.Endianness.load32_be Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder LowStar.Buffer.sub FStar.UInt32.op_Star_Hat FStar.UInt32.__uint_to_t FStar.Ghost.hide LowStar.Monotonic.Buffer.mbuffer FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.live Prims.b2t Prims.op_Equality Prims.op_Modulus Prims.op_LessThan FStar.UInt32.v Prims.op_Division LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none FStar.Seq.Base.index FStar.Krml.Endianness.seq_uint32_of_be LowStar.Monotonic.Buffer.as_seq
module C.Endianness

module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.Krml.Endianness
open LowStar.BufferOps

// Byte-level functions
[@(deprecated "LowStar.Endianness.htole16")]
assume val htole16: UInt16.t -> Tot UInt16.t
[@(deprecated "LowStar.Endianness.le16toh")]
assume val le16toh: UInt16.t -> Tot UInt16.t

[@(deprecated "LowStar.Endianness.htole32")]
assume val htole32: UInt32.t -> Tot UInt32.t
[@(deprecated "LowStar.Endianness.le32toh")]
assume val le32toh: UInt32.t -> Tot UInt32.t

[@(deprecated "LowStar.Endianness.htole64")]
assume val htole64: UInt64.t -> Tot UInt64.t
[@(deprecated "LowStar.Endianness.le64toh")]
assume val le64toh: UInt64.t -> Tot UInt64.t

[@(deprecated "LowStar.Endianness.htobe16")]
assume val htobe16: UInt16.t -> Tot UInt16.t
[@(deprecated "LowStar.Endianness.be16toh")]
assume val be16toh: UInt16.t -> Tot UInt16.t

[@(deprecated "LowStar.Endianness.htobe32")]
assume val htobe32: UInt32.t -> Tot UInt32.t
[@(deprecated "LowStar.Endianness.be32toh")]
assume val be32toh: UInt32.t -> Tot UInt32.t

[@(deprecated "LowStar.Endianness.htobe64")]
assume val htobe64: UInt64.t -> Tot UInt64.t
[@(deprecated "LowStar.Endianness.be64toh")]
assume val be64toh: UInt64.t -> Tot UInt64.t

[@(deprecated "LowStar.Endianness.store16_le")]
assume val store16_le:
  b:B.buffer UInt8.t{B.length b == 2} ->
  z:UInt16.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt16.v z))

[@(deprecated "LowStar.Endianness.load16_le")]
assume val load16_le:
  b:B.buffer UInt8.t{B.length b == 2} ->
  Stack UInt16.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt16.v z))


[@(deprecated "LowStar.Endianness.store16_be")]
assume val store16_be:
  b:B.buffer UInt8.t{B.length b == 2} ->
  z:UInt16.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt16.v z))

[@(deprecated "LowStar.Endianness.load16_be")]
assume val load16_be:
  b:B.buffer UInt8.t{B.length b == 2} ->
  Stack UInt16.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt16.v z))


[@(deprecated "LowStar.Endianness.store32_le")]
assume val store32_le:
  b:B.buffer UInt8.t{B.length b == 4} ->
  z:UInt32.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt32.v z))

[@(deprecated "LowStar.Endianness.load32_le")]
assume val load32_le:
  b:B.buffer UInt8.t{B.length b == 4} ->
  Stack UInt32.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt32.v z))


[@(deprecated "LowStar.Endianness.store32_be")]
assume val store32_be:
  b:B.buffer UInt8.t{B.length b == 4} ->
  z:UInt32.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt32.v z))

[@(deprecated "LowStar.Endianness.load32_be")]
assume val load32_be:
  b:B.buffer UInt8.t{B.length b == 4} ->
  Stack UInt32.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt32.v z))


[@(deprecated "LowStar.Endianness.store64_le")]
assume val store64_le:
  b:B.buffer UInt8.t{B.length b == 8} ->
  z:UInt64.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt64.v z))

[@(deprecated "LowStar.Endianness.load64_le")]
assume val load64_le:
  b:B.buffer UInt8.t{B.length b == 8} ->
  Stack UInt64.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt64.v z))


[@(deprecated "LowStar.Endianness.load64_be")]
assume val load64_be:
  b:B.buffer UInt8.t{B.length b == 8} ->
  Stack UInt64.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt64.v z))

[@(deprecated "LowStar.Endianness.store64_be")]
assume val store64_be:
  b:B.buffer UInt8.t{B.length b == 8} ->
  z:UInt64.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt64.v z))


[@(deprecated "LowStar.Endianness.load128_le")]
assume val load128_le:
  b:B.buffer UInt8.t{B.length b == 16} ->
  Stack UInt128.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt128.v z))

[@(deprecated "LowStar.Endianness.store128_le")]
assume val store128_le:
  b:B.buffer UInt8.t{B.length b == 16} ->
  z:UInt128.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           le_to_n (B.as_seq h1 b) == UInt128.v z))


[@(deprecated "LowStar.Endianness.load128_be")]
assume val load128_be:
  b:B.buffer UInt8.t{B.length b == 16} ->
  Stack UInt128.t
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt128.v z))

[@(deprecated "LowStar.Endianness.store128_be")]
assume val store128_be:
  b:B.buffer UInt8.t{B.length b = 16} ->
  z:UInt128.t ->
  Stack unit
    (requires (fun h -> B.live h b))
    (ensures  (fun h0 _ h1 -> B.(modifies (loc_buffer b) h0 h1) /\ B.live h1 b /\
                           be_to_n (B.as_seq h1 b) == UInt128.v z))


inline_for_extraction
[@(deprecated "LowStar.Endianness.index_32_be")]
let index_32_be (b: B.buffer UInt8.t) (i: UInt32.t):
  Stack UInt32.t
    (requires (fun h ->
      B.live h b /\ B.length b % 4 = 0 /\
      UInt32.v i < B.length b / 4))
    (ensures (fun h0 r h1 ->
      B.(modifies loc_none h0 h1) /\
      r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i)))
val index_32_be (b: B.buffer UInt8.t) (i: UInt32.t)
    : Stack UInt32.t
      (requires (fun h -> B.live h b /\ B.length b % 4 = 0 /\ UInt32.v i < B.length b / 4))
      (ensures
        (fun h0 r h1 ->
            B.(modifies loc_none h0 h1) /\
            r = Seq.index (seq_uint32_of_be (B.length b / 4) (B.as_seq h0 b)) (UInt32.v i)))
b: LowStar.Buffer.buffer FStar.UInt8.t -> i: FStar.UInt32.t
  -> FStar.HyperStack.ST.Stack FStar.UInt32.t