val n_to_be:
  len:U32.t -> n:nat{n < pow2 (8 * U32.v len)} ->
  Tot (b:bytes{S.length b == U32.v len /\ n == be_to_n b})
  (decreases (U32.v len))
let rec n_to_be len n =
  if len = 0ul then
    S.empty
  else
    let len = U32.(len -^ 1ul) in
    let byte = U8.uint_to_t (n % 256) in
    let n' = n / 256 in
    Math.pow2_plus 8 (8 * U32.v len);
    assert(n' < pow2 (8 * U32.v len ));
    let b' = n_to_be len n' in
    let b'' = S.create 1 byte in
    let b = S.append b' b'' in
    S.lemma_eq_intro b' (S.slice b 0 (U32.v len));
    b
val n_to_be:
  len:U32.t -> n:nat{n < pow2 (8 * U32.v len)} ->
  Tot (b:bytes{S.length b == U32.v len /\ n == be_to_n b})
  (decreases (U32.v len))
let rec n_to_be len n =
if len = 0ul
then S.empty
else
  let len = let open U32 in len -^ 1ul in
  let byte = U8.uint_to_t (n % 256) in
  let n' = n / 256 in
  Math.pow2_plus 8 (8 * U32.v len);
  assert (n' < pow2 (8 * U32.v len));
  let b' = n_to_be len n' in
  let b'' = S.create 1 byte in
  let b = S.append b' b'' in
  S.lemma_eq_intro b' (S.slice b 0 (U32.v len));
  b
FStar.Krml.Endianness.fst.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.HyperStack.All.fst.checked FStar.Classical.fsti.checked
FStar.Krml.Endianness.fst
FStar.UInt32.t Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Mul.op_Star FStar.UInt32.v Prims.op_Equality FStar.UInt32.__uint_to_t FStar.Seq.Base.empty FStar.UInt8.t Prims.bool Prims.unit FStar.Seq.Base.lemma_eq_intro FStar.Seq.Base.slice FStar.Seq.Base.seq FStar.Seq.Base.append FStar.Seq.Base.create FStar.Krml.Endianness.bytes Prims.l_and Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.Seq.Base.length FStar.Krml.Endianness.be_to_n FStar.Krml.Endianness.n_to_be Prims._assert FStar.Math.Lemmas.pow2_plus Prims.op_Division FStar.UInt8.uint_to_t Prims.op_Modulus FStar.UInt32.op_Subtraction_Hat FStar.UInt32.n
module FStar.Krml.Endianness

open FStar.Mul
open FStar.HyperStack.All

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

(* Selectively imported from Hacl*'s FStar.Endianness.fst library, with several
name changes *)

inline_for_extraction noextract
type bytes = S.seq U8.t

/// lt_to_n interprets a byte sequence as a little-endian natural number
[@(deprecated "FStar.Endianness.le_to_n")]
val le_to_n : b:bytes -> Tot nat (decreases (S.length b))
let rec le_to_n b =
  if S.length b = 0 then 0
  else U8.v (S.head b) + pow2 8 * le_to_n (S.tail b)

/// be_to_n interprets a byte sequence as a big-endian natural number
[@(deprecated "FStar.Endianness.be_to_n")]
val be_to_n : b:bytes -> Tot nat (decreases (S.length b))
let rec be_to_n b =
  if S.length b = 0 then 0
  else U8.v (S.last b) + pow2 8 * be_to_n (S.slice b 0 (S.length b - 1))

[@(deprecated "FStar.Endianness.lemma_euclidean_division")]
private val lemma_euclidean_division: r:nat -> b:nat -> q:pos -> Lemma
  (requires (r < q))
  (ensures  (r + q * b < q * (b+1)))
let lemma_euclidean_division r b q = ()

[@(deprecated "FStar.Endianness.lemma_factorise")]
private val lemma_factorise: a:nat -> b:nat -> Lemma (a + a * b == a * (b + 1))
let lemma_factorise a b = ()

[@(deprecated "FStar.Endianness.lemma_le_to_n_is_bounded")]
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))
let rec lemma_le_to_n_is_bounded b =
  if Seq.length b = 0 then ()
  else
    begin
    let s = Seq.slice b 1 (Seq.length b) in
    assert(Seq.length s = Seq.length b - 1);
    lemma_le_to_n_is_bounded s;
    assert(UInt8.v (Seq.index b 0) < pow2 8);
    assert(le_to_n s < pow2 (8 * Seq.length s));
    assert(le_to_n b < pow2 8 + pow2 8 * pow2 (8 * (Seq.length b - 1)));
    lemma_euclidean_division (UInt8.v (Seq.index b 0)) (le_to_n s) (pow2 8);
    assert(le_to_n b <= pow2 8 * (le_to_n s + 1));
    assert(le_to_n b <= pow2 8 * pow2 (8 * (Seq.length b - 1)));
    Math.Lemmas.pow2_plus 8 (8 * (Seq.length b - 1));
    lemma_factorise 8 (Seq.length b - 1)
    end

[@(deprecated "FStar.Endianness.lemma_be_to_n_is_bounded")]
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))
let rec lemma_be_to_n_is_bounded b =
  if Seq.length b = 0 then ()
  else
    begin
    let s = Seq.slice b 0 (Seq.length b - 1) in
    assert(Seq.length s = Seq.length b - 1);
    lemma_be_to_n_is_bounded s;
    assert(UInt8.v (Seq.last b) < pow2 8);
    assert(be_to_n s < pow2 (8 * Seq.length s));
    assert(be_to_n b < pow2 8 + pow2 8 * pow2 (8 * (Seq.length b - 1)));
    lemma_euclidean_division (UInt8.v (Seq.last b)) (be_to_n s) (pow2 8);
    assert(be_to_n b <= pow2 8 * (be_to_n s + 1));
    assert(be_to_n b <= pow2 8 * pow2 (8 * (Seq.length b - 1)));
    Math.Lemmas.pow2_plus 8 (8 * (Seq.length b - 1));
    lemma_factorise 8 (Seq.length b - 1)
    end

/// n_to_le encodes a number as a little-endian byte sequence of a fixed,
/// sufficiently large length
[@(deprecated "FStar.Endianness.n_to_le")]
val n_to_le : len:U32.t -> n:nat{n < pow2 (8 * U32.v len)} ->
  Tot (b:bytes{S.length b == U32.v len /\ n == le_to_n b})
  (decreases (U32.v len))
let rec n_to_le len n =
  if len = 0ul then
    S.empty
  else
    let len = U32.(len -^ 1ul) in
    let byte = U8.uint_to_t (n % 256) in
    let n' = n / 256 in
    Math.pow2_plus 8 (8 * U32.v len);
    assert(n' < pow2 (8 * U32.v len ));
    let b' = n_to_le len n' in
    let b = S.cons byte b' in
    S.lemma_eq_intro b' (S.tail b);
    b

/// n_to_be encodes a numbers as a big-endian byte sequence of a fixed,
/// sufficiently large length
[@(deprecated "FStar.Endianness.n_to_be")]
val n_to_be:
  len:U32.t -> n:nat{n < pow2 (8 * U32.v len)} ->
  Tot (b:bytes{S.length b == U32.v len /\ n == be_to_n b})
  (decreases (U32.v len))
val n_to_be:
  len:U32.t -> n:nat{n < pow2 (8 * U32.v len)} ->
  Tot (b:bytes{S.length b == U32.v len /\ n == be_to_n b})
  (decreases (U32.v len))
len: FStar.UInt32.t -> n: Prims.nat{n < Prims.pow2 (8 * FStar.UInt32.v len)}
  -> Prims.Tot
    (b:
      FStar.Krml.Endianness.bytes
        {FStar.Seq.Base.length b == FStar.UInt32.v len /\ n == FStar.Krml.Endianness.be_to_n b})