val update_multi
  (a:hash_alg)
  (hash:words_state a)
  (prev:extra_state a)
  (blocks:bytes_blocks a):
  Pure (words_state a)
    (requires update_multi_pre a prev blocks)
    (ensures fun _ -> True)
let update_multi a hash prev blocks =
  match a with
  | MD5 | SHA1 | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
      Lib.UpdateMulti.mk_update_multi (block_length a) (update a) hash blocks
  | Blake2B | Blake2S ->
      let nb = S.length blocks / block_length a in
      let a' = to_blake_alg a in
      Lib.LoopCombinators.repeati #(words_state a) nb (Spec.Blake2.blake2_update1 a' prev blocks) hash
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 ->
      let open Spec.SHA3 in
      let rateInBytes = rate a / 8 in
      Lib.Sequence.repeat_blocks_multi #_ #(words_state a) rateInBytes blocks (absorb_inner rateInBytes) hash
val update_multi
  (a:hash_alg)
  (hash:words_state a)
  (prev:extra_state a)
  (blocks:bytes_blocks a):
  Pure (words_state a)
    (requires update_multi_pre a prev blocks)
    (ensures fun _ -> True)
let update_multi a hash prev blocks =
match a with
| MD5
| SHA1
| SHA2_224
| SHA2_256
| SHA2_384
| SHA2_512 -> Lib.UpdateMulti.mk_update_multi (block_length a) (update a) hash blocks
| Blake2B
| Blake2S ->
  let nb = S.length blocks / block_length a in
  let a' = to_blake_alg a in
  Lib.LoopCombinators.repeati #(words_state a) nb (Spec.Blake2.blake2_update1 a' prev blocks) hash
| SHA3_224
| SHA3_256
| SHA3_384
| SHA3_512
| Shake128
| Shake256 ->
  let open Spec.SHA3 in
  let rateInBytes = rate a / 8 in
  Lib.Sequence.repeat_blocks_multi #_
    #(words_state a)
    rateInBytes
    blocks
    (absorb_inner rateInBytes)
    hash
Spec.Agile.Hash.fst.checked
Spec.SHA3.fst.checked Spec.SHA2.fsti.checked Spec.SHA1.fsti.checked Spec.MD5.fsti.checked Spec.Hash.MD.fst.checked Spec.Hash.Definitions.fst.checked Spec.Blake2.fst.checked prims.fst.checked Lib.UpdateMulti.fst.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
Spec.Agile.Hash.fst
Spec.Hash.Definitions.hash_alg Spec.Hash.Definitions.words_state Spec.Hash.Definitions.extra_state Spec.Hash.Definitions.bytes_blocks Lib.UpdateMulti.mk_update_multi Spec.Hash.Definitions.block_length Spec.Agile.Hash.update Lib.LoopCombinators.repeati Spec.Blake2.blake2_update1 Spec.Blake2.alg Spec.Hash.Definitions.to_blake_alg Prims.int Prims.op_Division FStar.Seq.Base.length Lib.IntTypes.uint8 Lib.Sequence.repeat_blocks_multi Spec.SHA3.absorb_inner Spec.Hash.Definitions.rate
module Spec.Agile.Hash

module S = FStar.Seq

open Spec.Hash.Definitions
open Spec.Hash.MD
open FStar.Mul
open Lib.IntTypes

unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x

let init a =
  match a with
  | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
      Spec.SHA2.init a
  | MD5 ->
      Spec.MD5.init
  | SHA1 ->
      Spec.SHA1.init
  | Blake2S -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2S 0 32
  | Blake2B -> Spec.Blake2.blake2_init_hash Spec.Blake2.Blake2B 0 64
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 ->
      Lib.Sequence.create 25 (u64 0)

// Intentionally restricting this one to MD hashes... we want clients to AVOID
// juggling between mk_update_multi update vs. repeati for non-MD hashes.
let update (a: md_alg) =
  match a with
  | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 ->
      Spec.SHA2.update a
  | MD5 ->
      Spec.MD5.update
  | SHA1 ->
      Spec.SHA1.update
val update_multi
  (a:hash_alg)
  (hash:words_state a)
  (prev:extra_state a)
  (blocks:bytes_blocks a):
  Pure (words_state a)
    (requires update_multi_pre a prev blocks)
    (ensures fun _ -> True)

    a: Spec.Hash.Definitions.hash_alg ->
    hash: Spec.Hash.Definitions.words_state a ->
    prev: Spec.Hash.Definitions.extra_state a ->
    blocks: Spec.Hash.Definitions.bytes_blocks a
  -> Prims.Pure (Spec.Hash.Definitions.words_state a)