val be_to_n_slice (s: S.seq U8.t) (i: nat): Lemma
  (requires i <= S.length s)
  (ensures FStar.Endianness.be_to_n (S.slice s i (S.length s)) =
    FStar.Endianness.be_to_n s % pow2 (8 `op_Multiply` (S.length s - i)))
  (decreases (S.length s))
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));
      }
val be_to_n_slice (s: S.seq U8.t) (i: nat): Lemma
  (requires i <= S.length s)
  (ensures FStar.Endianness.be_to_n (S.slice s i (S.length s)) =
    FStar.Endianness.be_to_n s % pow2 (8 `op_Multiply` (S.length s - i)))
  (decreases (S.length s))
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
    (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))
  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));
    }
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
FStar.Seq.Base.seq FStar.UInt8.t Prims.nat Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.bool Prims._assert Prims.b2t Prims.op_Modulus FStar.Endianness.be_to_n Prims.unit FStar.Seq.Base.empty FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Pervasives.assert_norm Prims.pow2 FStar.Mul.op_Star FStar.Endianness.reveal_be_to_n FStar.Calc.calc_finish Prims.eq2 Prims.op_Addition FStar.UInt8.v FStar.Seq.Properties.last Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.small_mod FStar.Endianness.lemma_be_to_n_is_bounded Prims.squash QUIC.Impl.Lemmas.be_to_n_slice FStar.Math.Lemmas.pow2_multiplication_modulo_lemma_2 FStar.Math.Lemmas.lemma_mod_add_distr FStar.Math.Lemmas.pow2_le_compat Prims.op_LessThan Prims.op_LessThanOrEqual Prims.op_disEquality
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
val be_to_n_slice (s: S.seq U8.t) (i: nat): Lemma
  (requires i <= S.length s)
  (ensures FStar.Endianness.be_to_n (S.slice s i (S.length s)) =
    FStar.Endianness.be_to_n s % pow2 (8 `op_Multiply` (S.length s - i)))
  (decreases (S.length s))
s: FStar.Seq.Base.seq FStar.UInt8.t -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i <= FStar.Seq.Base.length s)
      (ensures
        FStar.Endianness.be_to_n (FStar.Seq.Base.slice s i (FStar.Seq.Base.length s)) =
        FStar.Endianness.be_to_n s % Prims.pow2 (8 * (FStar.Seq.Base.length s - i)))
      (decreases FStar.Seq.Base.length s)