val pointwise_upd (#a: Type) (f: a -> a -> Tot a) (b1 b2: S.seq a) (i: nat) (pos: nat) (x: a): Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ i < pos))
  (ensures (S.upd (QSL.pointwise_op f b1 b2 pos) i x `S.equal`
    QSL.pointwise_op f (S.upd b1 i x) b2 pos))
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;
  }
val pointwise_upd (#a: Type) (f: a -> a -> Tot a) (b1 b2: S.seq a) (i: nat) (pos: nat) (x: a): Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ i < pos))
  (ensures (S.upd (QSL.pointwise_op f b1 b2 pos) i x `S.equal`
    QSL.pointwise_op f (S.upd b1 i x) b2 pos))
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;
}
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 FStar.Calc.calc_finish FStar.Seq.Base.equal QUIC.Spec.Lemmas.pointwise_op FStar.Seq.Base.upd Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Seq.Base.append FStar.Seq.Base.slice Prims.op_Addition FStar.Seq.Base.length Prims.op_Subtraction FStar.Seq.Base.op_At_Bar FStar.Calc.calc_init FStar.Calc.calc_pack QUIC.Impl.Lemmas.lemma_slice Prims.squash QUIC.Spec.Lemmas.pointwise_op_suff
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
val pointwise_upd (#a: Type) (f: a -> a -> Tot a) (b1 b2: S.seq a) (i: nat) (pos: nat) (x: a): Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ i < pos))
  (ensures (S.upd (QSL.pointwise_op f b1 b2 pos) i x `S.equal`
    QSL.pointwise_op f (S.upd b1 i x) b2 pos))

    f: (_: a -> _: a -> a) ->
    b1: FStar.Seq.Base.seq a ->
    b2: FStar.Seq.Base.seq a ->
    i: Prims.nat ->
    pos: Prims.nat ->
    x: a
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.length b2 + pos <= FStar.Seq.Base.length b1 /\ i < pos)
      (ensures
        FStar.Seq.Base.equal (FStar.Seq.Base.upd (QUIC.Spec.Lemmas.pointwise_op f b1 b2 pos) i x)
          (QUIC.Spec.Lemmas.pointwise_op f (FStar.Seq.Base.upd b1 i x) b2 pos))