val hash_len (a: keccak_alg { not (is_shake a) }): Lib.IntTypes.(n:size_t { v n = hash_length a })
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
val hash_len (a: keccak_alg { not (is_shake a) }): Lib.IntTypes.(n:size_t { v n = hash_length a })
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
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 Prims.b2t Prims.op_Negation Spec.Hash.Definitions.is_shake FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U32 Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.PUB Spec.Hash.Definitions.hash_length
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
val hash_len (a: keccak_alg { not (is_shake a) }): Lib.IntTypes.(n:size_t { v n = hash_length a })
a: Spec.Hash.Definitions.keccak_alg{Prims.op_Negation (Spec.Hash.Definitions.is_shake a)}
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}