val seq_map2_xor0 (s1 s2: S.seq Secret.uint8): Lemma
  (requires
    S.length s1 = S.length s2 /\
    s1 `S.equal` S.create (S.length s2) (Secret.to_u8 0uy))
  (ensures
    Spec.Loops.seq_map2 EverCrypt.CTR.xor8 s1 s2 `S.equal` s2)
  (decreases (S.length s1))
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)
val seq_map2_xor0 (s1 s2: S.seq Secret.uint8): Lemma
  (requires
    S.length s1 = S.length s2 /\
    s1 `S.equal` S.create (S.length s2) (Secret.to_u8 0uy))
  (ensures
    Spec.Loops.seq_map2 EverCrypt.CTR.xor8 s1 s2 `S.equal` s2)
  (decreases (S.length s1))
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)
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 Lib.IntTypes.uint8 Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.bool QUIC.Impl.Lemmas.seq_map2_xor0 FStar.Seq.Properties.tail Prims.unit Prims._assert Prims.eq2 Lib.IntTypes.range_t Lib.IntTypes.U8 QUIC.Secret.Int.Base.v Lib.IntTypes.SEC FStar.Seq.Properties.head Lib.IntTypes.int_t Spec.Loops.seq_map2 NotEverCrypt.CTR.xor8 FStar.UInt.logxor_commutative FStar.UInt.logxor_lemma_1
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
val seq_map2_xor0 (s1 s2: S.seq Secret.uint8): Lemma
  (requires
    S.length s1 = S.length s2 /\
    s1 `S.equal` S.create (S.length s2) (Secret.to_u8 0uy))
  (ensures
    Spec.Loops.seq_map2 EverCrypt.CTR.xor8 s1 s2 `S.equal` s2)
  (decreases (S.length s1))
s1: FStar.Seq.Base.seq Lib.IntTypes.uint8 -> s2: FStar.Seq.Base.seq Lib.IntTypes.uint8
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length s1 = FStar.Seq.Base.length s2 /\
        FStar.Seq.Base.equal s1
          (FStar.Seq.Base.create (FStar.Seq.Base.length s2) (Lib.IntTypes.to_u8 0uy)))
      (ensures FStar.Seq.Base.equal (Spec.Loops.seq_map2 NotEverCrypt.CTR.xor8 s1 s2) s2)
      (decreases FStar.Seq.Base.length s1)