val update_multi_zero_blake (a: hash_alg { is_blake a } ) (prevlen: extra_state a) (h: words_state a): Lemma
  (requires (update_multi_pre a prevlen S.empty))
  (ensures (update_multi a h prevlen S.empty == 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
val update_multi_zero_blake (a: hash_alg { is_blake a } ) (prevlen: extra_state a) (h: words_state a): Lemma
  (requires (update_multi_pre a prevlen S.empty))
  (ensures (update_multi a h prevlen S.empty == 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
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 Spec.Hash.Definitions.is_blake Spec.Hash.Definitions.extra_state Spec.Hash.Definitions.words_state Lib.LoopCombinators.eq_repeati0 Spec.Blake2.state Spec.Hash.Definitions.to_blake_alg Prims.op_Division Spec.Hash.Definitions.block_length Spec.Blake2.blake2_update1 FStar.Seq.Base.empty Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.unit
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
val update_multi_zero_blake (a: hash_alg { is_blake a } ) (prevlen: extra_state a) (h: words_state a): Lemma
  (requires (update_multi_pre a prevlen S.empty))
  (ensures (update_multi a h prevlen S.empty == h))

    a: Spec.Hash.Definitions.hash_alg{Spec.Hash.Definitions.is_blake a} ->
    prevlen: Spec.Hash.Definitions.extra_state a ->
    h: Spec.Hash.Definitions.words_state a
  -> FStar.Pervasives.Lemma
      (requires Spec.Agile.Hash.update_multi_pre a prevlen FStar.Seq.Base.empty)
      (ensures Spec.Agile.Hash.update_multi a h prevlen FStar.Seq.Base.empty == h)