val uint_from_be: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
let uint_from_be #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.be16toh u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.be16toh (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.be32toh u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.be32toh (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.be64toh u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.be64toh (Raw.u64_to_UInt64 u))
val uint_from_be: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
let uint_from_be #t #l u =
match t, l with
| U1, _ -> u
| U8, _ -> u
| U16, PUB -> LowStar.Endianness.be16toh u
| U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.be16toh (Raw.u16_to_UInt16 u))
| U32, PUB -> LowStar.Endianness.be32toh u
| U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.be32toh (Raw.u32_to_UInt32 u))
| U64, PUB -> LowStar.Endianness.be64toh u
| U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.be64toh (Raw.u64_to_UInt64 u))
Lib.ByteBuffer.fst.checked
prims.fst.checked LowStar.Endianness.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fst.checked Lib.Buffer.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Endianness.fst.checked
Lib.ByteBuffer.fst
Lib.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.l_not Lib.IntTypes.uu___is_U128 Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t FStar.Pervasives.Native.Mktuple2 LowStar.Endianness.be16toh Lib.RawIntTypes.u16_from_UInt16 Lib.RawIntTypes.u16_to_UInt16 LowStar.Endianness.be32toh Lib.RawIntTypes.u32_from_UInt32 Lib.RawIntTypes.u32_to_UInt32 LowStar.Endianness.be64toh Lib.RawIntTypes.u64_from_UInt64 Lib.RawIntTypes.u64_to_UInt64
module Lib.ByteBuffer

open FStar.HyperStack
open FStar.HyperStack.ST
open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators
module Raw = Lib.RawIntTypes

friend Lib.ByteSequence
friend Lib.IntTypes
friend FStar.Endianness

module E = LowStar.Endianness

(*
 * Despite befriending IntTypes this module enforces secrecy. The only exception,
 * for backwards compatibility, is `lbytes_eq`, which declassifies its result.
 *
 * We befriend IntTypes (or use RawIntTypes) to call into LowStar.Endianness library
 * for endianness conversions, which uses public machine integers.
 * E.g. `uint_to_bytes_le` loads a secret integer into a buffer of secret bytes by
 * internally casting the integer to a public machine integer, calling into LowStar,
 * and converting the result back to secret bytes.
 *
 * We use RawIntTypes when possible and only when this would be inconvenient
 * rely on opening the definitions in IntTypes. Specifically, only
 * `uint_from_bytes_le`, uint_from_bytes_be`, `uint_to_bytes_le`, and `uint_to_bytes_be`
 * rely on definitions in IntTypes. Alternatively, RawIntTypes could be used to cast
 * sequences and buffers of secret integers to sequences and buffers of machine integers,
 * but this would be too cumbersome.
*)

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 1"

let uint_to_be #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.htobe16 u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.htobe16 (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.htobe32 u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.htobe32 (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.htobe64 u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.htobe64 (Raw.u64_to_UInt64 u))

let uint_to_le #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.htole16 u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.htole16 (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.htole32 u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.htole32 (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.htole64 u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.htole64 (Raw.u64_to_UInt64 u))
val uint_from_be: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
u11: Lib.IntTypes.uint_t t l -> Lib.IntTypes.uint_t t l