val pointwise_seq_map2 (#a: Type) (f: a -> a -> a) (s1 s2: S.seq a) (i: nat): Lemma
  (requires (
    let l = S.length s1 in
    S.length s2 = l - i /\ i <= S.length s1))
  (ensures (
    let l = S.length s1 in
    Spec.Loops.seq_map2 f (S.slice s1 i l) s2 `S.equal`
    S.slice (QSL.pointwise_op f s1 s2 i) i l))
  (decreases (S.length s2))
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;

    };
    ()
val pointwise_seq_map2 (#a: Type) (f: a -> a -> a) (s1 s2: S.seq a) (i: nat): Lemma
  (requires (
    let l = S.length s1 in
    S.length s2 = l - i /\ i <= S.length s1))
  (ensures (
    let l = S.length s1 in
    Spec.Loops.seq_map2 f (S.slice s1 i l) s2 `S.equal`
    S.slice (QSL.pointwise_op f s1 s2 i) i l))
  (decreases (S.length s2))
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;
  };
  ()
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 Prims.nat Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.bool Prims.unit FStar.Calc.calc_finish FStar.Seq.Base.equal Spec.Loops.seq_map2 FStar.Seq.Base.slice QUIC.Spec.Lemmas.pointwise_op FStar.Seq.Base.upd FStar.Seq.Properties.head Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Seq.Properties.tail FStar.Seq.Properties.cons FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash QUIC.Impl.Lemmas.pointwise_seq_map2 QUIC.Impl.Lemmas.pointwise_upd
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
val pointwise_seq_map2 (#a: Type) (f: a -> a -> a) (s1 s2: S.seq a) (i: nat): Lemma
  (requires (
    let l = S.length s1 in
    S.length s2 = l - i /\ i <= S.length s1))
  (ensures (
    let l = S.length s1 in
    Spec.Loops.seq_map2 f (S.slice s1 i l) s2 `S.equal`
    S.slice (QSL.pointwise_op f s1 s2 i) i l))
  (decreases (S.length s2))
f: (_: a -> _: a -> a) -> s1: FStar.Seq.Base.seq a -> s2: FStar.Seq.Base.seq a -> i: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        (let l = FStar.Seq.Base.length s1 in
          FStar.Seq.Base.length s2 = l - i /\ i <= FStar.Seq.Base.length s1))
      (ensures
        (let l = FStar.Seq.Base.length s1 in
          FStar.Seq.Base.equal (Spec.Loops.seq_map2 f (FStar.Seq.Base.slice s1 i l) s2)
            (FStar.Seq.Base.slice (QUIC.Spec.Lemmas.pointwise_op f s1 s2 i) i l)))
      (decreases FStar.Seq.Base.length s2)