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
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
  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)
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.Krml.Endianness.bytes Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.UInt8.t Prims.bool FStar.Krml.Endianness.lemma_factorise Prims.op_Subtraction Prims.unit FStar.Math.Lemmas.pow2_plus FStar.Mul.op_Star Prims._assert Prims.b2t Prims.op_LessThanOrEqual FStar.Krml.Endianness.le_to_n Prims.pow2 Prims.op_Addition FStar.Krml.Endianness.lemma_euclidean_division FStar.UInt8.v FStar.Seq.Base.index Prims.op_LessThan FStar.Krml.Endianness.lemma_le_to_n_is_bounded FStar.Seq.Base.seq FStar.Seq.Base.slice
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))
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))
b: FStar.Krml.Endianness.bytes
  -> FStar.Pervasives.Lemma
      (ensures FStar.Krml.Endianness.le_to_n b < Prims.pow2 (8 * FStar.Seq.Base.length b))
      (decreases FStar.Seq.Base.length b)