val pointwise_op_empty (#a: Type) (f: (a -> a -> a)) (b1 b2: S.seq a) (pos: nat)
    : Lemma (requires (S.length b2 == 0 /\ pos <= S.length b1))
      (ensures (pointwise_op f b1 b2 pos == b1))
val pointwise_op_empty (#a: Type) (f: (a -> a -> a)) (b1 b2: S.seq a) (pos: nat)
    : Lemma (requires (S.length b2 == 0 /\ pos <= S.length b1))
      (ensures (pointwise_op f b1 b2 pos == b1))
let pointwise_op_empty
  (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (pos:nat)
: Lemma
  (requires (S.length b2 == 0 /\ pos <= S.length b1))
  (ensures (pointwise_op f b1 b2 pos == b1))
= assert (b2 `S.equal` S.empty)
module QUIC.Spec.Lemmas
open QUIC.Spec.Base

module S = FStar.Seq
module U8 = FStar.UInt8

(* library lemmas *)

let suffix (b:bytes) (n:nat{n <= S.length b}) = S.slice b n (S.length b)

let max (a b:int) : Tot (n:int{n >= a /\ n >= b}) =
  if a > b then a else b // this must exist somewhere...

// Move to FStar.Math.Lemmas?
let lemma_mod_pow2 (a:nat) (b:nat) : Lemma
  (requires a >= b) (ensures pow2 a % pow2 b == 0)
  [SMTPat (pow2 a % pow2 b)]
  =
  let open FStar.Math.Lemmas in
  lemma_div_mod (pow2 a) (pow2 b);
  pow2_minus a b;
  pow2_plus b (a-b)

#push-options "--z3rlimit 16"

let lemma_divrem2 (k:nat) (a:nat) (n:nat)
  : Lemma (requires a >= k /\ n < pow2 k)
  (ensures ((pow2 a + n) % pow2 k == n /\ (pow2 a + n) / pow2 k == pow2 (a - k)))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  modulo_distributivity (pow2 a) n (pow2 k);
  small_mod n (pow2 k);
  lemma_div_mod (pow2 a + n) (pow2 k);
  pow2_minus a k

#pop-options

// We really should have this pattern already...
let lemma_mod0 (x:pos) : Lemma (0 % x == 0)
  [SMTPat (0 % x)] = ()

// Move to FStar.Math.Lemmas?
let lemma_pow2_div (a:nat) (b:nat) (k:nat)
  : Lemma (requires a >= k /\ b >= k)
    (ensures (pow2 a + pow2 b) / pow2 k == pow2 (a - k) + pow2 (b - k))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  pow2_plus k (b - k);
  division_addition_lemma (pow2 a) (pow2 k) (pow2 (b-k));
  pow2_minus b k;
  pow2_minus a k

#restart-solver

let lemma_pow2_div2 (a:nat) (b:nat) (c:nat)
  : Lemma ((a / pow2 b) / pow2 c == a / (pow2 (c + b)))
  =
  let open FStar.Math.Lemmas in
  pow2_plus b c;
  division_multiplication_lemma a (pow2 b) (pow2 c)

let lemma_div_sub_small (l:nat) (n:nat) (x:nat)
  : Lemma (requires l > 1)
  (ensures (n - n % pow2 8) / pow2 (8 `op_Multiply` (l-1)) == n / pow2 (8 `op_Multiply` (l-1)))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  lemma_mod_spec n (pow2 8);
  lemma_pow2_div2 n 8 (8*(l-2));
  lemma_pow2_div2 (n - n % pow2 8) 8 (8*(l-2))

#push-options "--z3rlimit 20"
let rec lemma_be_index (l:pos) (n:nat{n < pow2 (8 `op_Multiply` l)})
  : Lemma (ensures U8.v (S.index (FStar.Endianness.n_to_be l n) 0)
    == n / pow2 (8 `op_Multiply` (l-1)))
    (decreases %[l])
  =
  let open FStar.Endianness in
  let open FStar.Mul in
  let b = n_to_be l n in
  let b0 = S.index b 0 in
  reveal_be_to_n b;
  if l = 1 then ()
  else
    let b1 = S.last b in
    let b' = S.slice b 0 (l-1) in
    let b0' = S.index b' 0 in
    reveal_be_to_n b';
    assert(U8.v b1 == n % pow2 8);
    lemma_be_to_n_is_bounded b';
    lemma_be_index (l-1) (be_to_n b');
    lemma_pow2_div2 (n - U8.v b1) 8 (8 * (l-1) - 8);
    lemma_div_sub_small l n (U8.v b1)
#pop-options


let lemma_be_index_bytes (l:pos) (b:bytes) : Lemma
  (requires S.length b >= l)
  (ensures FStar.Endianness.be_to_n (S.slice b 0 l) / pow2 (8 `op_Multiply` (l-1)) = U8.v (S.index b 0)) =
  let open FStar.Endianness in
  let n = be_to_n (S.slice b 0 l) in
  lemma_be_to_n_is_bounded (S.slice b 0 l);
  lemma_be_index l n;
  n_to_be_be_to_n l (S.slice b 0 l)


/// generic lemmas for sequences

let append_slices1 (#a:Type) (s1 s2:S.seq a) : Lemma
  (S.equal s1 (S.slice (S.append s1 s2) 0 (S.length s1))) =
  ()

let append_slices2 (#a:Type) (s1 s2:S.seq a) : Lemma
  (Seq.equal s2 (Seq.slice (Seq.append s1 s2) (Seq.length s1) (Seq.length s1 + Seq.length s2))) =
  ()

let append_slices3 (#a:Type) (s1 s2:S.seq a) : Lemma
  ( (forall (i:nat) (j:nat).
                i <= j /\ j <= Seq.length s2 ==>
                Seq.equal (Seq.slice s2 i j)
                          (Seq.slice (Seq.append s1 s2) (Seq.length s1 + i) (Seq.length s1 + j)))) =
  ()

let lemma_create_slice b i : Lemma
  (requires S.length b >= i)
  (ensures S.(equal (create 1 (index b i)) (slice b i (i+1)))) =
  ()

let lemma_append_assoc (#a:Type) (u v w:S.seq a) : Lemma
  (S.equal S.(u @| v @| w) S.((u @| v) @| w)) =
  ()

let compose_split (#a:Type) (b:S.seq a) (i j:nat) : Lemma
  (requires i+j <= S.length b)
  (ensures snd (S.split (snd (S.split b i)) j) == snd (S.split b (i+j))) =
  ()

let lemma_compose_slice (#a:Type) (b:S.seq a) (i j k l:nat) : Lemma
  (requires i <= j /\ j <= S.length b /\ k <= l /\ k <= j - i /\ l <= j - i)
  (ensures S.slice (S.slice b i j) k l == S.slice b (i+k) (i+l)) =
  ()

let add_offset (#a:Type) (b:S.seq a) (i:nat) (p1 p2:S.seq a) : Lemma
  (requires i <= S.length b /\ S.slice b i (S.length b) == S.(p1@|p2))
  (ensures (
    S.length S.(p1@|p2) == S.length p1+S.length p2 /\
    S.slice b (i+S.length p1) (S.length b) == p2)) =
  assert (S.length S.(p1@|p2) = S.length p1+S.length p2);
  append_slices2 p1 p2;
  compose_split b i (S.length p1)

let slice_trans (#a:Type) (b:S.seq a) (i j k:nat) : Lemma
  (requires i <= j /\ j <= k /\ k <= S.length b)
  (ensures S.slice b i k == S.(slice b i j @| slice b j k)) =
  S.lemma_split (S.slice b i k) (j-i)

let extensionality_slice (#a:Type) (b1 b2:S.seq a) (i j:nat) : Lemma
  (requires
    S.length b1 = S.length b2 /\
    i <= j /\ j <= S.length b1 /\
    (forall (k:nat{i<=k /\ k<j}). S.index b1 k == S.index b2 k))
  (ensures S.equal (S.slice b1 i j) (S.slice b2 i j)) =
  let index_slice_aux (b:S.seq a) (i j k:nat) : Lemma
    (requires i <= j /\ j <= S.length b /\ k < j - i)
    (ensures S.index (S.slice b i j) k == S.index b (i+k)) =
    () in
  let index_slice (b:S.seq a{j <= S.length b}) (k:nat{k < j - i}) : Lemma
    (S.index (S.slice b i j) k == S.index b (i+k)) =
    index_slice_aux b i j k in

  FStar.Classical.forall_intro (index_slice b1);
  FStar.Classical.forall_intro (index_slice b2)


// application of a byte operation at a subposition
let rec pointwise_op (#a:Type0) (f:a->a->a) (b1 b2:S.seq a) (pos:nat) : Pure (S.seq a)
  (requires S.length b2 + pos <= S.length b1)
  (ensures fun b -> S.length b == S.length b1)
  (decreases (S.length b2)) =
  if S.length b2 = 0 then b1
  else
    let _ = S.lemma_empty b2 in
    let x = f (S.index b1 pos) (S.index b2 0) in
    pointwise_op f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) (pos + 1)
/
QUIC.Spec.Base.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
QUIC.Spec.Lemmas.fst
f: (_: a -> _: a -> a) -> b1: FStar.Seq.Base.seq a -> b2: FStar.Seq.Base.seq a -> pos: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.length b2 == 0 /\ pos <= FStar.Seq.Base.length b1)
      (ensures QUIC.Spec.Lemmas.pointwise_op f b1 b2 pos == b1)
FStar.Seq.Base.seq Prims.nat Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.empty Prims.unit Prims.l_and Prims.eq2 Prims.int FStar.Seq.Base.length Prims.b2t Prims.op_LessThanOrEqual Prims.squash QUIC.Spec.Lemmas.pointwise_op Prims.Nil FStar.Pervasives.pattern
let pointwise_op_empty (#a: Type) (f: (a -> a -> a)) (b1 b2: S.seq a) (pos: nat)
    : Lemma (requires (S.length b2 == 0 /\ pos <= S.length b1))
      (ensures (pointwise_op f b1 b2 pos == b1)) =
  
assert (b2 `S.equal` S.empty)