val n_to_be_lower'
  (len: nat)
  (len' : nat)
  (n: nat)
: Lemma
  (requires (
    len <= len' /\
    n < pow2 (8 * len)
  ))
  (ensures (
    let open FStar.Endianness in
    n < pow2 (8 * len') /\
    n_to_be len' n `S.equal` (S.create (len' - len) 0uy `S.append` n_to_be len n)
  ))
let n_to_be_lower'
  len len' n
= let open FStar.Math.Lemmas in
  let open FStar.Endianness in
  pow2_le_compat (8 * len') (8 * len);
  let s1 = n_to_be len' n in
  let s2 = S.create (len' - len) 0uy `S.append` n_to_be len n in 
  let phi
    (i: nat {i < len'})
  : Lemma
    (S.index s1 i == S.index s2 i)
  = QSL.index_n_to_be len' n i;
    assert (len' - 1 - i == len - 1 - (i - (len' - len)));
    if len' - len <= i
    then begin
      QSL.index_n_to_be len n (i - (len' - len))
    end else begin
      pow2_le_compat (8 * (len' - 1 - i)) (8 * len);
      FStar.Math.Lemmas.small_div n (pow2 (8 * (len' - 1 - i)));
      assert (n / pow2 (8 * (len' - 1 - i)) == 0);
      assert (S.index s1 i == 0uy)
    end
  in
  Classical.forall_intro phi
val n_to_be_lower'
  (len: nat)
  (len' : nat)
  (n: nat)
: Lemma
  (requires (
    len <= len' /\
    n < pow2 (8 * len)
  ))
  (ensures (
    let open FStar.Endianness in
    n < pow2 (8 * len') /\
    n_to_be len' n `S.equal` (S.create (len' - len) 0uy `S.append` n_to_be len n)
  ))
let n_to_be_lower' len len' n =
let open FStar.Math.Lemmas in
let open FStar.Endianness in
pow2_le_compat (8 * len') (8 * len);
let s1 = n_to_be len' n in
let s2 = (S.create (len' - len) 0uy) `S.append` (n_to_be len n) in
let phi (i: nat{i < len'}) : Lemma (S.index s1 i == S.index s2 i) =
  QSL.index_n_to_be len' n i;
  assert (len' - 1 - i == len - 1 - (i - (len' - len)));
  if len' - len <= i
  then QSL.index_n_to_be len n (i - (len' - len))
  else
    (pow2_le_compat (8 * (len' - 1 - i)) (8 * len);
      FStar.Math.Lemmas.small_div n (pow2 (8 * (len' - 1 - i)));
      assert (n / pow2 (8 * (len' - 1 - i)) == 0);
      assert (S.index s1 i == 0uy))
in
Classical.forall_intro phi
QUIC.Impl.Lemmas.fst.checked
Spec.Loops.fst.checked QUIC.Spec.Lemmas.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked EverCrypt.CTR.fsti.checked C.Loops.fst.checked
QUIC.Impl.Lemmas.fst
Prims.nat FStar.Classical.forall_intro Prims.b2t Prims.op_LessThan Prims.eq2 FStar.UInt8.t FStar.Seq.Base.index Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.op_LessThanOrEqual Prims.op_Subtraction QUIC.Spec.Lemmas.index_n_to_be Prims.bool Prims._assert FStar.UInt8.__uint_to_t Prims.int Prims.op_Division Prims.pow2 FStar.Mul.op_Star FStar.Math.Lemmas.small_div FStar.Math.Lemmas.pow2_le_compat FStar.Seq.Base.seq FStar.Seq.Base.append FStar.Seq.Base.create FStar.Endianness.n_to_be FStar.Endianness.bytes Prims.l_and FStar.Seq.Base.length FStar.Endianness.be_to_n
module QUIC.Impl.Lemmas
include QUIC.Spec.Lemmas

#set-options "--max_fuel 0 --max_ifuel 0"

/// The usual sequence lemmas
/// -------------------------

let lemma_five_cuts
  s i1 i2 i3 i4 i5 s0 s1 s2 s3 s4 s5
=
  ()

let hash_is_keysized_
  a
=
  assert_norm (512 < pow2 61);
  assert_norm (512 < pow2 125)

let lemma_slice
  #t s i
=
  ()

let lemma_slice3
  #a s i j
=
  ()

let lemma_slice0
  #a s
= ()

let lemma_slice1
  #a s i j
=
  ()


open FStar.Mul

#push-options "--max_fuel 1 --z3rlimit 100"
let pointwise_upd
  #a f b1 b2 i pos x
=
  calc (S.equal) {
    QSL.pointwise_op f (S.upd b1 i x) b2 pos;
  (S.equal) { lemma_slice (S.upd b1 i x) (i + 1) }
    QSL.pointwise_op f
      S.(slice (S.upd b1 i x) 0 (i + 1) @| S.slice (S.upd b1 i x) (i + 1) (S.length b1))
      b2 pos;
  (S.equal) { }
    QSL.pointwise_op f
      S.(slice (S.upd b1 i x) 0 (i + 1) @| S.slice b1 (i + 1) (S.length b1))
      b2 pos;
  (S.equal) {
    QSL.pointwise_op_suff f
      (S.slice (S.upd b1 i x) 0 (i + 1))
      (S.slice b1 (i + 1) (S.length b1)) b2 pos
  }
    S.slice (S.upd b1 i x) 0 (i + 1) `S.append`
    QSL.pointwise_op f
      (S.slice b1 (i + 1) (S.length b1))
      b2 (pos - (i + 1));
  (S.equal) { }
    S.upd (S.slice b1 0 (i + 1)) i x `S.append`
    QSL.pointwise_op f
      (S.slice b1 (i + 1) (S.length b1))
      b2 (pos - (i + 1));
  (S.equal) { }
    S.upd (S.slice b1 0 (i + 1) `S.append`
    QSL.pointwise_op f
      (S.slice b1 (i + 1) (S.length b1))
      b2 (pos - (i + 1))
    ) i x;
  (S.equal) {
    QSL.pointwise_op_suff f
      (S.slice b1 0 (i + 1))
      (S.slice b1 (i + 1) (S.length b1)) b2 pos
  }
    S.upd (
      QSL.pointwise_op f
      (S.slice b1 0 (i + 1) `S.append` S.slice b1 (i + 1) (S.length b1))
      b2 pos
    ) i x;
  (S.equal) { lemma_slice b1 (i + 1) }
    S.upd (QSL.pointwise_op f b1 b2 pos) i x;
  }

let rec pointwise_seq_map2
  #a f s1 s2 i
=
  if S.length s2 = 0 then
    ()
  else
    let l = S.length s1 in
    calc (S.equal) {
      Spec.Loops.seq_map2 f (S.slice s1 i l) s2;
    (S.equal) {}
      S.cons (f (S.head (S.slice s1 i l)) (S.head s2))
        (Spec.Loops.seq_map2 f (S.tail (S.slice s1 i l)) (S.tail s2));
    (S.equal) {}
      S.cons (f (S.head (S.slice s1 i l)) (S.head s2))
        (Spec.Loops.seq_map2 f (S.slice s1 (i + 1) l) (S.tail s2));
    (S.equal) { pointwise_seq_map2 f s1 (S.slice s2 1 (S.length s2)) (i + 1) }
      S.cons (f (S.head (S.slice s1 i l)) (S.head s2))
        (S.slice (QSL.pointwise_op f s1 (S.tail s2) (i + 1)) (i + 1) l);
    (S.equal) { }
      S.slice (
        S.upd (QSL.pointwise_op f s1 (S.tail s2) (i + 1))
          i
          (f (S.head (S.slice s1 i l)) (S.head s2)))
        i
        l;
    (S.equal) { }
      S.slice (
        S.upd (QSL.pointwise_op f s1 (S.slice s2 1 (S.length s2)) (i + 1))
          i
          (f (S.head (S.slice s1 i l)) (S.head s2)))
        i
        l;
    (S.equal) {
      pointwise_upd f s1 (S.slice s2 1 (S.length s2)) i (i + 1)
        (f (S.head (S.slice s1 i l)) (S.head s2))
    }
      S.slice
        (QSL.pointwise_op f
          (S.upd s1 i (f (S.head (S.slice s1 i l)) (S.head s2)))
          (S.slice s2 1 (S.length s2))
          (i + 1))
        i l;

    };
    ()
#pop-options

#push-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"
let rec and_inplace_commutative
  s1 s2
=
  if S.length s1 = 0 then
    ()
  else (
    FStar.UInt.logand_commutative #8 (U8.v (S.head s1)) (U8.v (S.head s2));
    assert (U8.logand (S.head s1) (S.head s2) = U8.logand (S.head s2) (S.head s1));
    and_inplace_commutative (S.tail s1) (S.tail s2);
    assert (Spec.Loops.seq_map2 U8.logand (S.tail s1) (S.tail s2) `S.equal`
      Spec.Loops.seq_map2 U8.logand (S.tail s2) (S.tail s1))
  )
#pop-options

#push-options "--max_fuel 1"
let rec seq_map2_xor0
  s1 s2
=
  if S.length s1 = 0 then
    ()
  else
    let open FStar.UInt in
    logxor_lemma_1 #8 (Secret.v (S.head s2));
    logxor_lemma_1 #8 (Secret.v (S.head s1));
    logxor_commutative #8 (Secret.v (S.head s1)) (Secret.v (S.head s2));
    assert (Secret.v (S.head (Spec.Loops.seq_map2 EverCrypt.CTR.xor8 s1 s2)) == Secret.v (S.head s2));
    seq_map2_xor0 (S.tail s1) (S.tail s2)
#pop-options

#push-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"
let upd_op_inplace
  #a op s x
=
  ()
#pop-options

/// Endianness lemmas
/// -----------------

#push-options "--z3rlimit 16"
#restart-solver
let rec be_to_n_slice
  s i
=
  FStar.Endianness.reveal_be_to_n s;
  if S.length s = 0 then
    ()
  else
    let open FStar.Endianness in
    if i = S.length s then begin
      reveal_be_to_n S.empty;
      assert_norm (pow2 (8 * 0) = 1);
      assert (S.slice s (S.length s) (S.length s) `S.equal` S.empty);
      assert (be_to_n S.empty = 0);
      assert (be_to_n s % 1 = 0)
    end else
      let s' = (S.slice s i (S.length s)) in
      let s_prefix = (S.slice s 0 (S.length s - 1)) in
      assert (S.length s' <> 0);
      assert (8 <= 8 * (S.length s - i));
      FStar.Math.Lemmas.pow2_le_compat (8 * (S.length s - i)) 8;
      assert_norm (pow2 (8 * 1) = 256);
      assert (U8.v (S.last s) < pow2 (8 * (S.length s - i)));
      assert (S.length s' = S.length s_prefix - i + 1);
      FStar.Math.Lemmas.pow2_le_compat (8 * (S.length s')) (8 * (S.length s - i));
      calc (==) {
        be_to_n s';
      (==) {
        lemma_be_to_n_is_bounded s';
        FStar.Math.Lemmas.small_mod (be_to_n s') (pow2 (8 * (S.length s - i)))
      }
        (be_to_n s') % (pow2 (8 * (S.length s - i)));
      (==) { reveal_be_to_n s' }
        (U8.v (S.last s') + pow2 8 * be_to_n (S.slice s' 0 (S.length s' - 1))) %
          (pow2 (8 * (S.length s - i)));
      (==) { }
        (U8.v (S.last s) + pow2 8 * be_to_n (S.slice s i (S.length s - 1))) %
          (pow2 (8 * (S.length s - i)));
      (==) { }
        (U8.v (S.last s) + pow2 8 * (be_to_n (S.slice s_prefix i (S.length s_prefix)))) %
          (pow2 (8 * (S.length s - i)));
      (==) { be_to_n_slice s_prefix i }
        (U8.v (S.last s) + pow2 8 * (be_to_n s_prefix % pow2 (8 * (S.length s_prefix - i)))) %
          (pow2 (8 * (S.length s - i)));
      (==) { FStar.Math.Lemmas.pow2_multiplication_modulo_lemma_2
        (be_to_n s_prefix) (8 * (S.length s_prefix - i) + 8) 8
      }
        (U8.v (S.last s) +
          ((be_to_n s_prefix * pow2 8) % pow2 (8 * (S.length s_prefix - i) + 8))
        ) %
          (pow2 (8 * (S.length s - i)));
      (==) { }
        (U8.v (S.last s) +
          ((be_to_n s_prefix * pow2 8) % pow2 (8 * (S.length s - i)))
        ) %
          (pow2 (8 * (S.length s - i)));
      (==) { FStar.Math.Lemmas.lemma_mod_add_distr
        (U8.v (S.last s))
        (be_to_n s_prefix * pow2 8)
        (pow2 (8 * (S.length s - i)))
      }
        (U8.v (S.last s) + pow2 8 * be_to_n (S.slice s 0 (S.length s - 1))) %
          pow2 (8 * (S.length s - i));
      }
#pop-options

let n_to_be_lower
  len len' n
= let open FStar.Math.Lemmas in
  let open FStar.Endianness in
  pow2_le_compat (8 * len') (8 * len);
  let s1 = n_to_be len n in
  let s2 = FStar.Seq.slice (n_to_be len' n) (len' - len) len' in
  let phi
    (i: nat {i < len})
  : Lemma
    (S.index s1 i == S.index s2 i)
  = QSL.index_n_to_be len n i;
    QSL.index_n_to_be len' n (i + len' - len)
  in
  Classical.forall_intro phi

#restart-solver

let n_to_be_lower'
val n_to_be_lower'
  (len: nat)
  (len' : nat)
  (n: nat)
: Lemma
  (requires (
    len <= len' /\
    n < pow2 (8 * len)
  ))
  (ensures (
    let open FStar.Endianness in
    n < pow2 (8 * len') /\
    n_to_be len' n `S.equal` (S.create (len' - len) 0uy `S.append` n_to_be len n)
  ))
len: Prims.nat -> len': Prims.nat -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires len <= len' /\ n < Prims.pow2 (8 * len))
      (ensures
        n < Prims.pow2 (8 * len') /\
        FStar.Seq.Base.equal (FStar.Endianness.n_to_be len' n)
          (FStar.Seq.Base.append (FStar.Seq.Base.create (len' - len) 0uy)
              (FStar.Endianness.n_to_be len n)))