val le_of_uint32 (x: UInt32.t) : b: bytes{S.length b = 4}
let le_of_uint32 (x: UInt32.t): b:bytes{ S.length b = 4 } =
  n_to_le 4 (UInt32.v x)
val le_of_uint32 (x: UInt32.t) : b: bytes{S.length b = 4}
let le_of_uint32 (x: UInt32.t) : b: bytes{S.length b = 4} =
n_to_le 4 (UInt32.v x)
FStar.Endianness.fsti.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
FStar.Endianness.fsti
FStar.UInt32.t FStar.Endianness.n_to_le FStar.UInt32.v FStar.Endianness.bytes Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.UInt8.t
module FStar.Endianness

/// A library of lemmas for reasoning about sequences of machine integers and
/// their (little|big)-endian representation as a sequence of bytes.
///
/// The functions in this module aim to be as generic as possible, in order to
/// facilitate compatibility with:
/// - Vale's model of machine integers (nat64 et al.), which does not rely on
///   FStar's machine integers
/// - HACL*'s Lib.IntTypes module, which exposes a universal indexed integer
///   type but uses F* machine integers under the hood.
///
/// To achieve maximum compatibility, we try to state most lemmas using nat
/// rather than UIntX.
///
/// To limit context pollution, the definitions of the recursive functions are
/// abstract; please add lemmas as you see fit. In extreme cases, ``friend``'ing
/// might be de rigueur.
///
/// .. note::
///
///    This module supersedes the poorly-named ``FStar.Krml.Endianness``.

module U8 = FStar.UInt8
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Math = FStar.Math.Lemmas
module S = FStar.Seq

[@@ noextract_to "krml"]
type bytes = S.seq U8.t

open FStar.Mul


/// Definition of little and big-endianness
/// ---------------------------------------
///
/// This is our spec, to be audited. From bytes to nat.

/// lt_to_n interprets a byte sequence as a little-endian natural number
val le_to_n : b:bytes -> Tot nat

/// be_to_n interprets a byte sequence as a big-endian natural number
val be_to_n : b:bytes -> Tot nat

/// Induction for le_to_n and be_to_n

val reveal_le_to_n (b:bytes)
  : Lemma
    (le_to_n b ==
     (match Seq.length b with
      | 0 -> 0
      | _ -> U8.v (S.head b) + pow2 8 * le_to_n (S.tail b)))

val reveal_be_to_n (b:bytes)
  : Lemma
    (be_to_n b ==
     (match Seq.length b with
      | 0 -> 0
      | _ -> U8.v (S.last b) + pow2 8 * be_to_n (S.slice b 0 (S.length b - 1))))

val lemma_le_to_n_is_bounded: b:bytes -> Lemma
  (requires True)
  (ensures  (le_to_n b < pow2 (8 * Seq.length b)))
  (decreases (Seq.length b))

val lemma_be_to_n_is_bounded: b:bytes -> Lemma
  (requires True)
  (ensures  (be_to_n b < pow2 (8 * Seq.length b)))
  (decreases (Seq.length b))


/// Inverse operations
/// ------------------
///
/// From nat to bytes, and their functional correctness.

/// n_to_le encodes a number as a little-endian byte sequence of a fixed,
/// sufficiently large length.
val n_to_le : len:nat -> n:nat{n < pow2 (8 * len)} ->
  Tot (b:bytes{S.length b == len /\ n == le_to_n b})
  (decreases len)

/// n_to_be encodes a numbers as a big-endian byte sequence of a fixed,
/// sufficiently large length
val n_to_be:
  len:nat -> n:nat{n < pow2 (8 * len)} ->
  Tot (b:bytes{S.length b == len /\ n == be_to_n b})
  (decreases len)

/// Injectivity
/// -----------

val n_to_le_inj (len: nat) (n1 n2: (n:nat{n < pow2 (8 * len)})):
  Lemma (requires (n_to_le len n1 == n_to_le len n2))
        (ensures (n1 == n2))

val n_to_be_inj (len: nat) (n1 n2: (n:nat{n < pow2 (8 * len)})) :
  Lemma (requires (n_to_be len n1 == n_to_be len n2))
        (ensures (n1 == n2))

val be_to_n_inj
  (b1 b2: Seq.seq U8.t)
: Lemma
  (requires (Seq.length b1 == Seq.length b2 /\ be_to_n b1 == be_to_n b2))
  (ensures (Seq.equal b1 b2))
  (decreases (Seq.length b1))

val le_to_n_inj
  (b1 b2: Seq.seq U8.t)
: Lemma
  (requires (Seq.length b1 == Seq.length b2 /\ le_to_n b1 == le_to_n b2))
  (ensures (Seq.equal b1 b2))
  (decreases (Seq.length b1))

/// Roundtripping
/// -------------

val n_to_be_be_to_n (len: nat) (s: Seq.seq U8.t) : Lemma
  (requires (Seq.length s == len))
  (ensures (
    be_to_n s < pow2 (8 * len) /\
    n_to_be len (be_to_n s) == s
  ))
  [SMTPat (n_to_be len (be_to_n s))]

val n_to_le_le_to_n (len: nat) (s: Seq.seq U8.t) : Lemma
  (requires (Seq.length s == len))
  (ensures (
    le_to_n s < pow2 (8 * len) /\
    n_to_le len (le_to_n s) == s
  ))
  [SMTPat (n_to_le len (le_to_n s))]


/// Specializations for F* machine integers
/// ---------------------------------------
///
/// These are useful because they take care of calling the right ``*_is_bounded`` lemmas.

let uint32_of_le (b: bytes { S.length b = 4 }) =
  let n = le_to_n b in
  lemma_le_to_n_is_bounded b;
  UInt32.uint_to_t n
val le_of_uint32 (x: UInt32.t) : b: bytes{S.length b = 4}
x: FStar.UInt32.t -> b: FStar.Endianness.bytes{FStar.Seq.Base.length b = 4}