val max_input_length: hash_alg -> option pos
let max_input_length: hash_alg -> option pos = function
  | MD5 | SHA1
  | SHA2_224 | SHA2_256 -> Some (pow2 61 - 1)
  | SHA2_384 | SHA2_512 -> Some (pow2 125 - 1)
  | Blake2S -> Some (pow2 64 - 1)
  | Blake2B -> Some (pow2 128 - 1)
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 -> None
val max_input_length: hash_alg -> option pos
let max_input_length: hash_alg -> option pos =
function
| MD5 | SHA1 | SHA2_224 | SHA2_256 -> Some (pow2 61 - 1)
| SHA2_384 | SHA2_512 -> Some (pow2 125 - 1)
| Blake2S -> Some (pow2 64 - 1)
| Blake2B -> Some (pow2 128 - 1)
| SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 -> None
Spec.Hash.Definitions.fst.checked
Spec.Blake2.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Hash.Definitions.fst
Spec.Hash.Definitions.hash_alg FStar.Pervasives.Native.Some Prims.pos Prims.op_Subtraction Prims.pow2 FStar.Pervasives.Native.None FStar.Pervasives.Native.option
module Spec.Hash.Definitions

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

(* This module contains shared definitions across all hash algorithms. It
 * defines a common, shared `hash_alg` type, along with word sizes, type of the
 * working state, and other helpers. It also defines the type of the core functions
 * init / update / pad / finish that any algorithm must implement in order to be
 * turned into a complete hash construction.
 *
 * Some notes about terminology:
 * - this module uses the HACL* naming convention, namely init/update/finish
 *   (Cédric uses init/compress/extract in EverCrypt.HMAC and above)
 * - this module defines maximum lengths to be *bounds* (i.e. max_value + 1), a
 *   somewhat dubious convention that persists for historical reasons, but that
 *   is abandoned in miTLS via an extra indirection
 *
 * The following naming conventions are (tentatively) enforced.
 * - underscores (no camelCase)
 * - suffixes: _length for nat, _len for machine integer
 * - by default, lengths are in bytes; we use _word_length or _bit_len as suffixes
 * - for names that might conflict with their stateful counterparts, we prefix
 *   with the type, e.g. words_state or bytes_block
 *)

(** Supported hash algorithms.

  NOTE: this inductive is *append-only* because the constructors generate macro
  definitions that various bindings (OCaml, Rust) have taken a dependency on.
  So, in order to keep the numbering stable, we only append new cases, which is
  why SHA3_224 comes after SHA3_256 (the former was added *after* the latter).
  *)
type hash_alg =
  | SHA2_224
  | SHA2_256
  | SHA2_384
  | SHA2_512
  | SHA1
  | MD5
  | Blake2S
  | Blake2B
  | SHA3_256
  | SHA3_224
  | SHA3_384
  | SHA3_512
  | Shake128
  | Shake256

inline_for_extraction noextract
let is_sha2 = function
  | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 -> true
  | _ -> false

inline_for_extraction noextract
let is_keccak = function
  | SHA3_224 | SHA3_256 | SHA3_384 | SHA3_512 | Shake128 | Shake256 -> true
  | _ -> false

inline_for_extraction noextract
let is_shake = function
  | Shake128 | Shake256 -> true
  | _ -> false

inline_for_extraction noextract
let is_blake = function
  | Blake2S | Blake2B -> true
  | _ -> false

inline_for_extraction noextract
let is_md = function
  | MD5 | SHA1 | SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512 -> true
  | _ -> false

let sha2_alg = a:hash_alg { is_sha2 a }
let keccak_alg = a:hash_alg { is_keccak a }
let blake_alg = a:hash_alg { is_blake a }
let md_alg = a:hash_alg { is_md a }
let fixed_len_alg = a:hash_alg { not (is_shake a) }

inline_for_extraction
let to_blake_alg (a:blake_alg) = match a with
  | Blake2S -> Spec.Blake2.Blake2S
  | Blake2B -> Spec.Blake2.Blake2B

inline_for_extraction
let to_hash_alg (a : Spec.Blake2.alg) =
  match a with
  | Spec.Blake2.Blake2S -> Blake2S
  | Spec.Blake2.Blake2B -> Blake2B

(** Maximum input data length. *)

(* In bytes. *)
val max_input_length: hash_alg -> option pos
_: Spec.Hash.Definitions.hash_alg -> FStar.Pervasives.Native.option Prims.pos