val xor_involutive (b1 b2: byte)
    : Lemma (requires True) (ensures (b1 `U8.logxor` b2) `U8.logxor` b2 = b1)
val xor_involutive (b1 b2: byte)
    : Lemma (requires True) (ensures (b1 `U8.logxor` b2) `U8.logxor` b2 = b1)
let xor_involutive (b1 b2:byte) : Lemma
  (requires True)
  (ensures (b1 `U8.logxor` b2) `U8.logxor` b2 = b1) =
  FStar.UInt.logxor_associative (U8.v b1) (U8.v b2) (U8.v b2);
  FStar.UInt.logxor_self (U8.v b2);
  FStar.UInt.logxor_commutative (FStar.UInt.zero 8) (U8.v b1);
  FStar.UInt.logxor_lemma_1 (U8.v b1)
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)

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)

// three lemmas to recover indexes after application of bitwise_op
let rec pointwise_index1 (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (i pos:nat) : Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ i < pos))
  (ensures (S.index (pointwise_op f b1 b2 pos) i == S.index b1 i))
  (decreases (S.length b2)) =
  if Seq.length b2 = 0 then ()
  else begin
    S.lemma_empty b2;
    let x = f (S.index b1 pos) (S.index b2 0) in
    assert (pointwise_op f b1 b2 pos == pointwise_op f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) (pos + 1));
    S.lemma_index_upd2 b1 pos x i;
    assert (S.index (S.upd b1 pos x) i == S.index b1 i);
    pointwise_index1 f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) i (pos + 1)
  end


let rec pointwise_index2 (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (i pos:nat) : Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ pos <= i /\ i < S.length b2 + pos))
  (ensures (S.index (pointwise_op f b1 b2 pos) i == f (S.index b1 i) (S.index b2 (i-pos))))
  (decreases (S.length b2)) =
  if Seq.length b2 = 0 then ()
  else begin
    let x = f (S.index b1 pos) (S.index b2 0) in
    assert (pointwise_op f b1 b2 pos == pointwise_op f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) (pos+1));
    if i = pos then begin
      pointwise_index1 f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) pos (pos+1);
      S.lemma_index_upd1 b1 pos x
    end
    else
      pointwise_index2 f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) i (pos+1)
  end


let rec pointwise_index3 (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (i pos:nat) : Lemma
  (requires (S.length b2 + pos <= i /\ i < S.length b1))
  (ensures (S.index (pointwise_op f b1 b2 pos) i == S.index b1 i))
  (decreases (S.length b2)) =
  if Seq.length b2 = 0 then ()
  else begin
    S.lemma_empty b2;
    let x = f (S.index b1 pos) (S.index b2 0) in
    pointwise_index3 f (S.upd b1 pos x) (S.slice b2 1 (S.length b2)) i (pos+1)
  end

let pointwise_index
  (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (i pos:nat)
: Lemma
  (requires (S.length b2 + pos <= S.length b1 /\ i < S.length b1))
  (ensures (
    S.length b2 + pos <= S.length b1 /\ i < S.length b1 /\
    S.index (pointwise_op f b1 b2 pos) i == (
    if S.length b2 + pos <= i || i < pos
    then S.index b1 i
    else f (S.index b1 i) (S.index b2 (i-pos))
  )))
= if i < pos
  then pointwise_index1 f b1 b2 i pos
  else if S.length b2 + pos <= i
  then pointwise_index3 f b1 b2 i pos
  else pointwise_index2 f b1 b2 i pos

let pointwise_op_suff (#a:Type) (f:a->a->a) (a1 a2 b:S.seq a) (pos:nat) : Lemma
  (requires pos >= S.length a1 /\ S.length b + pos <= S.length a1 + S.length a2)
  (ensures
    S.equal
      (pointwise_op f S.(a1 @| a2) b pos)
      S.(a1 @| pointwise_op f a2 b (pos - S.length a1))) =
  let b1 = pointwise_op f S.(a1 @| a2) b pos in
  let b2 = S.(a1 @| pointwise_op f a2 b (pos - S.length a1)) in
  let step i : Lemma (S.index b1 i == S.index b2 i) =
    if i < S.length a1 then pointwise_index1 f S.(a1 @| a2) b i pos
    else begin
      if i < pos then begin
        pointwise_index1 f S.(a1 @| a2) b i pos;
        pointwise_index1 f a2 b (i-S.length a1) (pos-S.length a1)
      end else if i < S.length b + pos then begin
        pointwise_index2 f S.(a1 @| a2) b i pos;
        pointwise_index2 f a2 b (i-S.length a1) (pos-S.length a1)
      end else begin
        pointwise_index3 f S.(a1 @| a2) b i pos;
        pointwise_index3 f a2 b (i-S.length a1) (pos-S.length a1)
      end
    end in

  FStar.Classical.forall_intro step


let pointwise_op_pref (#a:Type) (f:a->a->a) (a1 a2 b:S.seq a) (pos:nat) : Lemma
  (requires S.length b + pos <= S.length a1)
  (ensures
    S.equal
      (pointwise_op f S.(a1 @| a2) b pos)
      S.(pointwise_op f a1 b pos @| a2)) =
  let b1 = pointwise_op f S.(a1 @| a2) b pos in
  let b2 = S.(pointwise_op f a1 b pos @| a2) in
  let step i : Lemma (S.index b1 i == S.index b2 i) =
    if i < pos then begin
      pointwise_index1 f S.(a1 @| a2) b i pos;
      pointwise_index1 f a1 b i pos
    end else if i < S.length b + pos then begin
      pointwise_index2 f S.(a1 @| a2) b i pos;
      pointwise_index2 f a1 b i pos
    end else begin
      pointwise_index3 f S.(a1 @| a2) b i pos;
      if i < S.length a1 then pointwise_index3 f a1 b i pos
      else ()
    end in

  FStar.Classical.forall_intro step


let pointwise_op_dec (#a:Type) (f:a->a->a) (a1 a2 b:S.seq a) (pos:nat) : Lemma
  (requires
    pos <= S.length a1 /\
    S.length a1 <= S.length b + pos /\
    S.length b + pos <= S.length a1 + S.length a2)
  (ensures (
    let open S in
    let (b1,b2) = S.split b (length a1 - pos) in
    equal
      (pointwise_op f (a1 @| a2) b pos)
      (pointwise_op f a1 b1 pos @| pointwise_op f a2 b2 0))) =
  let open S in
  let (b1,b2) = S.split b (length a1 - pos) in
  let p = pointwise_op f (a1 @| a2) b pos in
  let q = pointwise_op f a1 b1 pos @| pointwise_op f a2 b2 0 in
  let step i : Lemma (S.index p i == S.index q i) =
    if i < pos then begin
      pointwise_index1 f (a1 @| a2) b i pos;
      pointwise_index1 f a1 b1 i pos
    end else if i < length a1 then begin
      pointwise_index2 f (a1 @| a2) b i pos;
      pointwise_index2 f a1 b1 i pos
    end else if i < length b + pos then begin
      pointwise_index2 f (a1 @| a2) b i pos;
      pointwise_index2 f a2 b2 (i-length a1) 0
    end else begin
      pointwise_index3 f (a1 @| a2) b i pos;
      pointwise_index3 f a2 b2 (i-length a1) 0
    end in

  FStar.Classical.forall_intro step

#push-options "--z3rlimit 32"

let pointwise_op_append_r
  (#t: Type)
  (f: t -> t -> t)
  (a b1 b2: S.seq t)
  (pos: nat)
: Lemma
  (requires (
    pos + S.length b1 + S.length b2 <= S.length a
  ))
  (ensures (
    pointwise_op f a (S.append b1 b2) pos == (
      pointwise_op f (S.slice a 0 (pos + S.length b1)) b1 pos `S.append`
      pointwise_op f (S.slice a (pos + S.length b1) (S.length a)) b2 0
  )))
= S.lemma_split a (pos + S.length b1);
  pointwise_op_dec f (S.slice a 0 (pos + S.length b1)) (S.slice a (pos + S.length b1) (S.length a)) (S.append b1 b2) pos;
  let (b1', b2') = S.split (b1 `S.append` b2) (S.length b1) in
  assert (b1 `S.equal` b1' /\ b2 `S.equal` b2')

#pop-options

let pointwise_op_split
  (#t: Type)
  (f: t -> t -> t)
  (a b: S.seq t)
  (pos: nat)
  (pos_split: nat)
: Lemma
  (requires (
    pos <= pos_split /\
    pos_split <= pos + S.length b /\
    pos + S.length b <= S.length a
  ))
  (ensures (
    let (a1, a2) = S.split a pos_split in
    let (b1, b2) = S.split b (pos_split - pos) in
    pointwise_op f a b pos == pointwise_op f a1 b1 pos `S.append` pointwise_op f a2 b2 0
  ))
= S.lemma_split a pos_split;
  pointwise_op_dec f (S.slice a 0 pos_split) (S.slice a pos_split (S.length a)) b pos

let pointwise_op_slice_other
  (#a:Type) (f:a->a->a) (b1 b2:S.seq a) (pos:nat)
  (from to: nat)
: Lemma
  (requires (
    S.length b2 + pos <= S.length b1 /\
    from <= to /\
    to <= S.length b1 /\
    (to <= pos \/ pos + S.length b2 <= from)
  ))
  (ensures (
    S.slice (pointwise_op f b1 b2 pos) from to `S.equal` S.slice b1 from to
  ))
= let phi
    (i: nat { from <= i /\ i < to })
  : Lemma
    (S.index (pointwise_op f b1 b2 pos) i == S.index b1 i)
  = if to <= pos
    then pointwise_index1 f b1 b2 i pos
    else pointwise_index3 f b1 b2 i pos
  in
  Classical.forall_intro phi


// application: byte-wise xor
let xor_inplace (b1 b2:bytes) (pos:nat)
  : Pure bytes
  (requires S.length b2 + pos <= S.length b1)
  (ensures fun b -> S.length b == S.length b1)
  (decreases (S.length b2)) =
  pointwise_op U8.logxor b1 b2 pos


// proof of involution of the operator (uses extensionality for the
/
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
b1: QUIC.Spec.Base.byte -> b2: QUIC.Spec.Base.byte
  -> FStar.Pervasives.Lemma (ensures FStar.UInt8.logxor (FStar.UInt8.logxor b1 b2) b2 = b1)
QUIC.Spec.Base.byte FStar.UInt.logxor_lemma_1 FStar.UInt8.n FStar.UInt8.v Prims.unit FStar.UInt.logxor_commutative FStar.UInt.zero FStar.UInt.logxor_self FStar.UInt.logxor_associative Prims.l_True Prims.squash Prims.b2t Prims.op_Equality FStar.UInt8.t FStar.UInt8.logxor Prims.Nil FStar.Pervasives.pattern
let xor_involutive (b1 b2: byte)
    : Lemma (requires True) (ensures (b1 `U8.logxor` b2) `U8.logxor` b2 = b1) =
  
FStar.UInt.logxor_associative (U8.v b1) (U8.v b2) (U8.v b2);
FStar.UInt.logxor_self (U8.v b2);
FStar.UInt.logxor_commutative (FStar.UInt.zero 8) (U8.v b1);
FStar.UInt.logxor_lemma_1 (U8.v b1)