val be_to_n_append' (hi lo: bytes)
    : Lemma
      (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
      (decreases (S.length lo))
let rec be_to_n_append'
  (hi lo: bytes)
: Lemma
  (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
  (decreases (S.length lo))
= reveal_be_to_n lo;
  let hilo = hi `S.append` lo in
  if S.length lo = 0
  then
    assert (hilo `S.equal` hi)
  else begin
    let lo' = S.slice lo 0 (S.length lo - 1) in
    assert (S.slice hilo 0 (S.length hilo - 1) `S.equal` (hi `S.append` lo'));
    assert (S.last hilo == S.last lo);
    reveal_be_to_n hilo;
    be_to_n_append' hi lo';
    pow2_plus (8 * S.length lo') 8
  end
val be_to_n_append' (hi lo: bytes)
    : Lemma
      (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
      (decreases (S.length lo))
let rec be_to_n_append' (hi lo: bytes)
    : Lemma
      (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
      (decreases (S.length lo)) =
reveal_be_to_n lo;
let hilo = hi `S.append` lo in
if S.length lo = 0
then assert (hilo `S.equal` hi)
else
  let lo' = S.slice lo 0 (S.length lo - 1) in
  assert ((S.slice hilo 0 (S.length hilo - 1)) `S.equal` (hi `S.append` lo'));
  assert (S.last hilo == S.last lo);
  reveal_be_to_n hilo;
  be_to_n_append' hi lo';
  pow2_plus (8 * S.length lo') 8
LowParse.Endianness.fst.checked
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
LowParse.Endianness.fst
FStar.Endianness.bytes Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.UInt8.t Prims._assert FStar.Seq.Base.equal Prims.bool FStar.Math.Lemmas.pow2_plus FStar.Mul.op_Star Prims.unit LowParse.Endianness.be_to_n_append' FStar.Endianness.reveal_be_to_n Prims.eq2 FStar.Seq.Properties.last FStar.Seq.Base.slice Prims.op_Subtraction FStar.Seq.Base.append FStar.Seq.Base.seq Prims.l_True Prims.squash FStar.Endianness.be_to_n Prims.op_Addition Prims.pow2 Prims.Nil FStar.Pervasives.pattern
module LowParse.Endianness

let rec index_be_to_n'
  (b: bytes)
  (i: nat)
: Lemma
  (requires (
    i < S.length b
  ))
  (ensures (
    U8.v (S.index b i) == (be_to_n b / pow2 (8 * (S.length b - 1 - i))) % pow2 8
  ))
  (decreases (S.length b))
= reveal_be_to_n b;
  if i = S.length b - 1
  then ()
  else begin
    let l = S.length b in
    let l' = l - 1 in
    let b' = S.slice b 0 l' in
    index_be_to_n' b' i;
    assert (S.index b i == S.index b' i);
    let open FStar.Math.Lemmas in
    let x = be_to_n b in
    let x' = be_to_n b' in
    assert (U8.v (S.index b i) == x' / pow2 (8 * (l' - 1 - i)) % pow2 8);
    let y = (U8.v (S.last b) + pow2 8 * x') / pow2 (8 * (l - 1 - i)) % pow2 8 in
    pow2_plus 8 (8 * (l' - 1 - i));
    division_multiplication_lemma (U8.v (S.last b) + pow2 8 * x') (pow2 8) (pow2 (8 * (l' - 1 - i)));
    assert (pow2 8 * x' == x' * pow2 8);
    division_addition_lemma (U8.v (S.last b)) (pow2 8) x';
    small_division_lemma_1 (U8.v (S.last b)) (pow2 8);
    assert (y == x' / pow2 (8 * (l' - 1 - i)) % pow2 8)
  end

let index_be_to_n = index_be_to_n'

let index_n_to_be
  (len: nat)
  (n: nat)
  (i: nat)
: Lemma
  (requires (
    i < len /\
    n < pow2 (8 * len)
  ))
  (ensures (
    U8.v (S.index (n_to_be len n) i)) == (n / pow2 (8 * (len - 1 - i)) % pow2 8
  ))
= index_be_to_n (n_to_be len n) i

let index_n_to_be_zero_left
  (len: nat)
  (n: nat)
  (j: nat)
  (i: nat)
: Lemma
  (requires (
    i < j /\
    j <= len /\
    n < pow2 (8 * (len - j))
  ))
  (ensures (
    pow2 (8 * (len - j)) <= pow2 (8 * len) /\
    U8.v (S.index (n_to_be len n) i) == 0
  ))
= let open FStar.Math.Lemmas in
  pow2_le_compat (8 * len) (8 * (len - j));
  pow2_le_compat (8 * (len - 1 - i)) (8 * (len - j));
  small_division_lemma_1 n (pow2 (8 * (len - 1 - i)));
  index_n_to_be len n i

let index_n_to_be_zero_right
  (len: nat)
  (n: nat)
  (i: nat)
: Lemma
  (requires (
    i < len /\
    n < pow2 (8 * len) /\
    n % pow2 (8 * (len - i)) == 0
  ))
  (ensures (
    U8.v (S.index (n_to_be len n) i) == 0
  ))
= index_n_to_be len n i;
  let open FStar.Math.Lemmas in
  modulo_division_lemma n (pow2 (8 * (len - 1 - i))) (pow2 8);
  pow2_plus (8 * (len - 1 - i)) 8
  
open FStar.Math.Lemmas

let rec be_to_n_append'
  (hi lo: bytes)
: Lemma
  (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
val be_to_n_append' (hi lo: bytes)
    : Lemma
      (ensures (be_to_n (hi `S.append` lo) == be_to_n hi * pow2 (8 * S.length lo) + be_to_n lo))
      (decreases (S.length lo))
hi: FStar.Endianness.bytes -> lo: FStar.Endianness.bytes
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Endianness.be_to_n (FStar.Seq.Base.append hi lo) ==
        FStar.Endianness.be_to_n hi * Prims.pow2 (8 * FStar.Seq.Base.length lo) +
        FStar.Endianness.be_to_n lo) (decreases FStar.Seq.Base.length lo)