let nat_to_len (a:maxed_hash_alg) (n:nat{n <= maxint (len_int_type a)}) =
  mk_int #(len_int_type a ) #PUB n
let nat_to_len (a: maxed_hash_alg) (n: nat{n <= maxint (len_int_type a)}) =
mk_int #(len_int_type a) #PUB n
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.maxed_hash_alg Prims.nat Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.maxint Spec.Hash.Definitions.len_int_type Lib.IntTypes.mk_int Lib.IntTypes.PUB Lib.IntTypes.int_t Prims.eq2 Lib.IntTypes.range_t Lib.IntTypes.v
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. *)

inline_for_extraction
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

let maxed_hash_alg = a:hash_alg { Some? (max_input_length a) }

let sha2_alg_is_maxed (a: hash_alg): Lemma (requires (is_sha2 a)) (ensures (Some? (max_input_length a))) [ SMTPat (is_sha2 a) ] = ()
let md_alg_is_maxed (a: hash_alg): Lemma (requires (is_md a)) (ensures (Some? (max_input_length a))) [ SMTPat (is_md a) ] = ()
let blake_alg_is_maxed (a: hash_alg): Lemma (requires (is_blake a)) (ensures (Some? (max_input_length a))) [ SMTPat (is_blake a) ] = ()

// TODO: many of these definitions are only used by the MD padding scheme,
// meaning they should be defined over md_alg!

(* A type that can hold a maximum length, in bits. *)
inline_for_extraction
let len_int_type: maxed_hash_alg -> inttype = function
  | MD5 | SHA1
  | SHA2_224 | SHA2_256 -> U64
  | SHA2_384 | SHA2_512 -> U128
  | Blake2S -> U64
  | Blake2B -> U128

inline_for_extraction
val nat_to_len : a: Spec.Hash.Definitions.maxed_hash_alg ->
    n: Prims.nat{n <= Lib.IntTypes.maxint (Spec.Hash.Definitions.len_int_type a)}
  -> u37:
    Lib.IntTypes.int_t (Spec.Hash.Definitions.len_int_type a) Lib.IntTypes.PUB
      {Lib.IntTypes.v u37 == n}

    a: Spec.Hash.Definitions.maxed_hash_alg ->
    n: Prims.nat{n <= Lib.IntTypes.maxint (Spec.Hash.Definitions.len_int_type a)}
  -> u37:
    Lib.IntTypes.int_t (Spec.Hash.Definitions.len_int_type a) Lib.IntTypes.PUB
      {Lib.IntTypes.v u37 == n}