val 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 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
val 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 index_n_to_be_zero_left (len n j 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
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
Prims.nat LowParse.Endianness.index_n_to_be Prims.unit FStar.Math.Lemmas.small_division_lemma_1 Prims.pow2 FStar.Mul.op_Star Prims.op_Subtraction FStar.Math.Lemmas.pow2_le_compat Prims.l_and Prims.b2t Prims.op_LessThan Prims.op_LessThanOrEqual Prims.squash Prims.eq2 Prims.int FStar.UInt8.v FStar.Seq.Base.index FStar.UInt8.t FStar.Endianness.n_to_be 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
val 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
  ))
len: Prims.nat -> n: Prims.nat -> j: Prims.nat -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i < j /\ j <= len /\ n < Prims.pow2 (8 * (len - j)))
      (ensures
        Prims.pow2 (8 * (len - j)) <= Prims.pow2 (8 * len) /\
        FStar.UInt8.v (FStar.Seq.Base.index (FStar.Endianness.n_to_be len n) i) == 0)