val lemma_update_aux2
      (a: blake_alg)
      (s1 s2: bytes)
      (nb1 nb2 prevlen1 prevlen2: nat)
      (i: nat{i < nb2})
      (acc: words_state a)
    : Lemma
      (requires
        S.length s1 == nb1 * block_length a /\ S.length s2 == nb2 * block_length a /\
        prevlen1 % block_length a == 0 /\ prevlen2 = prevlen1 + S.length s1 /\
        (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
      (ensures
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen2 s2 i acc)
let lemma_update_aux2 (a:blake_alg) (s1 s2:bytes) (nb1 nb2:nat) (prevlen1 prevlen2:nat) (i:nat{i < nb2}) (acc:words_state a)
  : Lemma
    (requires
      S.length s1 == nb1 * block_length a /\
      S.length s2 == nb2 * block_length a /\
      prevlen1 % block_length a == 0 /\
      prevlen2 = prevlen1 + S.length s1 /\
      (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
    (ensures
      Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
      Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen2 s2 i acc)
  = let s = s1 `S.append` s2 in
    let a' = to_blake_alg a in

    let open Spec.Blake2 in
    let f1 = blake2_update1 (to_blake_alg a) prevlen1 s in
    let f2 = blake2_update1 (to_blake_alg a) prevlen2 s2 in
    let totlen1 = prevlen1 + (i + nb1 + 1) * size_block a' in
    let totlen2 = prevlen2 + (i + 1) * size_block a' in
    // Proving totlen1 == totlen2 for the last calc step below
    calc (==) {
      totlen2;
      (==) { }
      prevlen2 + (i + 1) * block_length a;
      (==) { }
      prevlen1 + S.length s1 + (i + 1) * block_length a;
      (==) { }
      prevlen1 + nb1 * block_length a + (i + 1) * block_length a;
      (==) { Math.Lemmas.distributivity_add_left (i + 1) nb1 (block_length a) }
      prevlen1 + (i + 1 + nb1) * block_length a;
      (==) { }
      totlen1;
    };

    calc (==) {
      f1 (i + nb1) acc;
      (==) { }
      blake2_update_block a' false totlen1 (get_blocki a' s (i + nb1)) acc;
      (==) { lemma_blocki_aux2 a s1 s2 nb1 nb2 i }
      blake2_update_block a' false totlen1 (get_blocki a' s2 i) acc;
      (==) { }
      f2 i acc;

    }
val lemma_update_aux2
      (a: blake_alg)
      (s1 s2: bytes)
      (nb1 nb2 prevlen1 prevlen2: nat)
      (i: nat{i < nb2})
      (acc: words_state a)
    : Lemma
      (requires
        S.length s1 == nb1 * block_length a /\ S.length s2 == nb2 * block_length a /\
        prevlen1 % block_length a == 0 /\ prevlen2 = prevlen1 + S.length s1 /\
        (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
      (ensures
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen2 s2 i acc)
let lemma_update_aux2
      (a: blake_alg)
      (s1 s2: bytes)
      (nb1 nb2 prevlen1 prevlen2: nat)
      (i: nat{i < nb2})
      (acc: words_state a)
    : Lemma
      (requires
        S.length s1 == nb1 * block_length a /\ S.length s2 == nb2 * block_length a /\
        prevlen1 % block_length a == 0 /\ prevlen2 = prevlen1 + S.length s1 /\
        (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
      (ensures
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen2 s2 i acc) =
let s = s1 `S.append` s2 in
let a' = to_blake_alg a in
let open Spec.Blake2 in
let f1 = blake2_update1 (to_blake_alg a) prevlen1 s in
let f2 = blake2_update1 (to_blake_alg a) prevlen2 s2 in
let totlen1 = prevlen1 + (i + nb1 + 1) * size_block a' in
let totlen2 = prevlen2 + (i + 1) * size_block a' in
calc ( == ) {
  totlen2;
  ( == ) { () }
  prevlen2 + (i + 1) * block_length a;
  ( == ) { () }
  prevlen1 + S.length s1 + (i + 1) * block_length a;
  ( == ) { () }
  prevlen1 + nb1 * block_length a + (i + 1) * block_length a;
  ( == ) { Math.Lemmas.distributivity_add_left (i + 1) nb1 (block_length a) }
  prevlen1 + (i + 1 + nb1) * block_length a;
  ( == ) { () }
  totlen1;
};
calc ( == ) {
  f1 (i + nb1) acc;
  ( == ) { () }
  blake2_update_block a' false totlen1 (get_blocki a' s (i + nb1)) acc;
  ( == ) { lemma_blocki_aux2 a s1 s2 nb1 nb2 i }
  blake2_update_block a' false totlen1 (get_blocki a' s2 i) acc;
  ( == ) { () }
  f2 i acc;
}
Spec.Hash.Lemmas.fst.checked
Spec.SHA3.fst.checked Spec.Hash.Definitions.fst.checked Spec.Blake2.fst.checked Spec.Agile.Hash.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.Lemmas.fsti.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Spec.Hash.Lemmas.fst
Spec.Hash.Definitions.blake_alg Spec.Hash.Definitions.bytes Prims.nat Prims.b2t Prims.op_LessThan Spec.Hash.Definitions.words_state FStar.Calc.calc_finish Spec.Blake2.state Spec.Hash.Definitions.to_blake_alg Prims.eq2 Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Spec.Blake2.blake2_update_block Spec.Blake2.get_blocki FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Spec.Hash.Lemmas.lemma_blocki_aux2 Prims.int FStar.Mul.op_Star Spec.Hash.Definitions.block_length FStar.Seq.Base.length Lib.IntTypes.uint8 FStar.Math.Lemmas.distributivity_add_left Spec.Blake2.size_block Prims.l_and Prims.op_Division Lib.Sequence.length Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.op_LessThanOrEqual Spec.Blake2.max_limb Lib.Sequence.lseq Spec.Blake2.wt Spec.Blake2.blake2_update1 Spec.Blake2.alg FStar.Seq.Base.seq FStar.Seq.Base.append Prims.op_Modulus Prims.op_Equality Spec.Hash.Definitions.less_than_max_input_length FStar.Pervasives.pattern
module Spec.Hash.Lemmas

module S = FStar.Seq
open Lib.IntTypes

open Spec.Agile.Hash
open Spec.Hash.Definitions

friend Spec.Agile.Hash

(** Lemmas about the behavior of update_multi / update_last *)

#push-options "--fuel 0 --ifuel 1 --z3rlimit 50"

let update_multi_zero a h =
  match a with
  | MD5 | SHA1 | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
    Lib.UpdateMulti.update_multi_zero (block_length a) (Spec.Agile.Hash.update a) h
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 ->
    let rateInBytes = rate a / 8 in
    let f = Spec.SHA3.absorb_inner rateInBytes in
    Lib.Sequence.lemma_repeat_blocks_multi rateInBytes S.empty f h;

    let nb = 0 / rateInBytes in
    Lib.LoopCombinators.eq_repeati0 nb (Lib.Sequence.repeat_blocks_f rateInBytes S.empty f nb) h

let update_multi_zero_blake a prevlen h =
  Lib.LoopCombinators.eq_repeati0 (0 / block_length a) (Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen S.empty) h
#pop-options

#push-options "--fuel 1"
let update_multi_update (a: md_alg) (h: words_state a) (input: bytes_block a): Lemma
  (ensures (update_multi a h () input) == (update a h input))
=
  let h1 = update_multi a h () input in
  assert(h1 == Lib.UpdateMulti.mk_update_multi (block_length a) (update a) h input);
  if S.length input = 0 then
    begin
    assert(h1 == h)
    end
  else
    begin
    let block, rem = Lib.UpdateMulti.split_block (block_length a) input 1 in
    let h2 = update a h block in
    assert(rem `Seq.equal` Seq.empty);
    assert(block `Seq.equal` input);
    let h3 = Lib.UpdateMulti.mk_update_multi (block_length a) (update a) h2 rem in
    assert(h1 == h3)
    end
#pop-options

let update_multi_associative (a: hash_alg{not (is_blake a)})
  (h: words_state a)
  (input1: bytes)
  (input2: bytes):
  Lemma
  (requires
    S.length input1 % block_length a == 0 /\
    S.length input2 % block_length a == 0)
  (ensures (
    let input = S.append input1 input2 in
    S.length input % block_length a == 0 /\
    update_multi a (update_multi a h () input1) () input2 == update_multi a h () input))
  = match a with
  | MD5 | SHA1 | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
    Lib.UpdateMulti.update_multi_associative (block_length a) (Spec.Agile.Hash.update a) h input1 input2
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 ->
    let rateInBytes = rate a /8 in
    let f = Spec.SHA3.absorb_inner rateInBytes in
    let input = input1 `S.append` input2 in
    assert (input1 `S.equal` S.slice input 0 (S.length input1));
    assert (input2 `S.equal` S.slice input (S.length input1) (S.length input));
    Lib.Sequence.Lemmas.repeat_blocks_multi_split (block_length a) (S.length input1) input f h

let lemma_blocki_aux1 (a:blake_alg) (s1 s2:bytes) (i:nat{i < S.length s1 / block_length a})
  : Lemma (Spec.Blake2.get_blocki (to_blake_alg a) s1 i == Spec.Blake2.get_blocki (to_blake_alg a) (S.append s1 s2) i)
  = assert (Spec.Blake2.get_blocki (to_blake_alg a) s1 i `S.equal` Spec.Blake2.get_blocki (to_blake_alg a) (S.append s1 s2) i)

#push-options "--fuel 0 --ifuel 0 --z3rlimit 300"

open FStar.Mul

let lemma_blocki_aux2 (a:blake_alg) (s1 s2:bytes) (nb1 nb2:nat) (i:nat{i < nb2})
  : Lemma
    (requires
      S.length s1 == nb1 * block_length a /\
      S.length s2 == nb2 * block_length a)
    (ensures Spec.Blake2.get_blocki (to_blake_alg a) s2 i ==
           Spec.Blake2.get_blocki (to_blake_alg a) (S.append s1 s2) (i + nb1))
  = let s = s1 `S.append` s2 in
    let a' = to_blake_alg a in
    calc (==) {
          Spec.Blake2.get_blocki a' s (i + nb1);
          (==) { }
          S.slice s ((i + nb1) * block_length a) ((i + nb1 + 1) * block_length a);
          (==) { }
          S.slice s (i * block_length a + nb1 * block_length a) ((i + 1) * block_length a + nb1 * block_length a);
          (==) { }
          S.slice s (i * block_length a + S.length s1) ((i + 1) * block_length a + S.length s1);
          (==) { S.slice_slice s (S.length s1) (S.length s) (i * block_length a) ((i+1) * block_length a) }
          S.slice (S.slice s (S.length s1) (S.length s)) (i * block_length a) ((i+1) * block_length a);
          (==) { S.append_slices s1 s2; assert (s2 `S.equal` S.slice s (S.length s1) (S.length s)) }
          S.slice s2 (i * block_length a) ((i+1) * block_length a);
          (==) { }
          Spec.Blake2.get_blocki a' s2 i;
        }

let lemma_update_aux2 (a:blake_alg) (s1 s2:bytes) (nb1 nb2:nat) (prevlen1 prevlen2:nat) (i:nat{i < nb2}) (acc:words_state a)
  : Lemma
    (requires
      S.length s1 == nb1 * block_length a /\
      S.length s2 == nb2 * block_length a /\
      prevlen1 % block_length a == 0 /\
      prevlen2 = prevlen1 + S.length s1 /\
      (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
    (ensures
      Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
val lemma_update_aux2
      (a: blake_alg)
      (s1 s2: bytes)
      (nb1 nb2 prevlen1 prevlen2: nat)
      (i: nat{i < nb2})
      (acc: words_state a)
    : Lemma
      (requires
        S.length s1 == nb1 * block_length a /\ S.length s2 == nb2 * block_length a /\
        prevlen1 % block_length a == 0 /\ prevlen2 = prevlen1 + S.length s1 /\
        (S.length (S.append s1 s2) + prevlen1) `less_than_max_input_length` a)
      (ensures
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen1 (s1 `S.append` s2) (i + nb1) acc ==
        Spec.Blake2.blake2_update1 (to_blake_alg a) prevlen2 s2 i acc)

    a: Spec.Hash.Definitions.blake_alg ->
    s1: Spec.Hash.Definitions.bytes ->
    s2: Spec.Hash.Definitions.bytes ->
    nb1: Prims.nat ->
    nb2: Prims.nat ->
    prevlen1: Prims.nat ->
    prevlen2: Prims.nat ->
    i: Prims.nat{i < nb2} ->
    acc: Spec.Hash.Definitions.words_state a
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length s1 == nb1 * Spec.Hash.Definitions.block_length a /\
        FStar.Seq.Base.length s2 == nb2 * Spec.Hash.Definitions.block_length a /\
        prevlen1 % Spec.Hash.Definitions.block_length a == 0 /\
        prevlen2 = prevlen1 + FStar.Seq.Base.length s1 /\
        Spec.Hash.Definitions.less_than_max_input_length (FStar.Seq.Base.length (FStar.Seq.Base.append
                  s1
                  s2) +
            prevlen1)
          a)
      (ensures
        Spec.Blake2.blake2_update1 (Spec.Hash.Definitions.to_blake_alg a)
          prevlen1
          (FStar.Seq.Base.append s1 s2)
          (i + nb1)
          acc ==
        Spec.Blake2.blake2_update1 (Spec.Hash.Definitions.to_blake_alg a) prevlen2 s2 i acc)