let update_multi_sha3_st (a:keccak_alg) =
  s:B.buffer uint64 { B.length s = 25 } ->
  ev:unit ->
  blocks:blocks_t a ->
  n:size_t { B.length blocks = block_length a * v n } ->
  ST.Stack unit
    (requires (fun h ->
      Spec.Agile.Hash.update_multi_pre a () (B.as_seq h blocks) /\
      B.live h s /\ B.live h blocks /\ B.disjoint s blocks))
    (ensures (fun h0 _ h1 ->
      B.(modifies (loc_buffer s) h0 h1) /\
      B.as_seq h1 s ==
        Spec.Agile.Hash.update_multi a (B.as_seq h0 s) () (B.as_seq h0 blocks)))
let update_multi_sha3_st (a: keccak_alg) =

    s: B.buffer uint64 {B.length s = 25} ->
    ev: unit ->
    blocks: blocks_t a ->
    n: size_t{B.length blocks = block_length a * v n}
  -> ST.Stack unit
      (requires
        (fun h ->
            Spec.Agile.Hash.update_multi_pre a () (B.as_seq h blocks) /\ B.live h s /\
            B.live h blocks /\ B.disjoint s blocks))
      (ensures
        (fun h0 _ h1 ->
            B.(modifies (loc_buffer s) h0 h1) /\
            B.as_seq h1 s == Spec.Agile.Hash.update_multi a (B.as_seq h0 s) () (B.as_seq h0 blocks))
      )
Hacl.Hash.SHA3.fst.checked
Spec.SHA3.fst.checked Spec.Hash.Incremental.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.SHA3.fst.checked Hacl.Impl.SHA3.fst.checked Hacl.Hash.PadFinish.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked
Hacl.Hash.SHA3.fst
Spec.Hash.Definitions.keccak_alg LowStar.Buffer.buffer Lib.IntTypes.uint64 Prims.b2t Prims.op_Equality Prims.int LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Prims.unit Hacl.Hash.Definitions.blocks_t Lib.IntTypes.size_t Lib.IntTypes.uint8 FStar.Mul.op_Star Spec.Hash.Definitions.block_length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Monotonic.HyperStack.mem Prims.l_and Spec.Agile.Hash.update_multi_pre LowStar.Monotonic.Buffer.as_seq LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.disjoint LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer Prims.eq2 FStar.Seq.Base.seq Spec.Hash.Definitions.word Spec.Agile.Hash.update_multi
module Hacl.Hash.SHA3

open Spec.Hash.Definitions
open Hacl.Hash.Definitions
open FStar.Mul

module B = LowStar.Buffer
module S = FStar.Seq
module ST = FStar.HyperStack.ST
open Lib.IntTypes

module LB = Lib.Buffer

friend Spec.Agile.Hash

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

/// We name this function used in Lib.Sequence spec combinators to avoid Z3 reasoning on anonymous functions
inline_for_extraction noextract
let spec_l (a: keccak_alg)
  (len:size_nat{len < block_length a})
  (inp:Lib.Sequence.lseq uint8 len)
  (s:Lib.Sequence.lseq uint64 25) = s

// TODO: for some reason, doing `let block_len = block_len` still results in excessive inlining.
let block_len (a: keccak_alg): n:size_t { v n = block_length a } =
  let open Spec.Hash.Definitions in
  let open FStar.Mul in
  [@inline_let]
  let _ = allow_inversion hash_alg in
  match a with
  | SHA3_224 -> assert_norm (rate SHA3_224/8/8*8 = 144); 144ul
  | SHA3_256 -> assert_norm (rate SHA3_256/8/8*8 = 136); 136ul
  | SHA3_384 -> assert_norm (rate SHA3_384/8/8*8 = 104); 104ul
  | SHA3_512 -> assert_norm (rate SHA3_512/8/8*8 = 72); 72ul
  | Shake128 -> assert_norm (rate Shake128/8/8*8 = 168); 168ul
  | Shake256 -> assert_norm (rate Shake256/8/8*8 = 136); 136ul

let hash_len (a: keccak_alg { not (is_shake a) }): Lib.IntTypes.(n:size_t { v n = hash_length a }) =
  match a with
  | SHA3_224 -> 28ul
  | SHA3_256 -> 32ul
  | SHA3_384 -> 48ul
  | SHA3_512 -> 64ul

let init a s =
  [@inline_let] let s: s:B.buffer uint64 { B.length s = 25 } = s in
  LowStar.Buffer.fill s (Lib.IntTypes.u64 0) 25ul

noextract inline_for_extraction
let is_shake a = a = Shake128 || a = Shake256

noextract inline_for_extraction
val update_multi_sha3_st : a: Spec.Hash.Definitions.keccak_alg -> Type0
a: Spec.Hash.Definitions.keccak_alg -> Type0