val 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))
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
val 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))
let update_multi_associative
      (a: hash_alg{not (is_blake a)})
      (h: words_state a)
      (input1 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
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.hash_alg Prims.b2t Prims.op_Negation Spec.Hash.Definitions.is_blake Spec.Hash.Definitions.words_state Spec.Hash.Definitions.bytes Lib.UpdateMulti.update_multi_associative Spec.Hash.Definitions.block_length Spec.Agile.Hash.update Lib.Sequence.Lemmas.repeat_blocks_multi_split Lib.IntTypes.uint8 Spec.SHA3.state FStar.Seq.Base.length Prims.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.Seq.Base.seq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.Seq.Base.append Lib.Sequence.lseq Lib.IntTypes.U64 Spec.SHA3.absorb_inner Prims.int Prims.op_Division Spec.Hash.Definitions.rate Prims.l_and Prims.eq2 Prims.op_Modulus Prims.squash Spec.Agile.Hash.update_multi Prims.Nil 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 /\
val 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))

    a: Spec.Hash.Definitions.hash_alg{Prims.op_Negation (Spec.Hash.Definitions.is_blake a)} ->
    h: Spec.Hash.Definitions.words_state a ->
    input1: Spec.Hash.Definitions.bytes ->
    input2: Spec.Hash.Definitions.bytes
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length input1 % Spec.Hash.Definitions.block_length a == 0 /\
        FStar.Seq.Base.length input2 % Spec.Hash.Definitions.block_length a == 0)
      (ensures
        (let input = FStar.Seq.Base.append input1 input2 in
          FStar.Seq.Base.length input % Spec.Hash.Definitions.block_length a == 0 /\
          Spec.Agile.Hash.update_multi a (Spec.Agile.Hash.update_multi a h () input1) () input2 ==
          Spec.Agile.Hash.update_multi a h () input))