val hash_len (a: alg) : n: UInt32.t{UInt32.v n == hash_length a}
let hash_len (a:alg)
  : n:UInt32.t{UInt32.v n == hash_length a}
  = Hacl.Hash.Definitions.hash_len a
val hash_len (a: alg) : n: UInt32.t{UInt32.v n == hash_length a}
let hash_len (a: alg) : n: UInt32.t{UInt32.v n == hash_length a} =
Hacl.Hash.Definitions.hash_len a
Hashing.Spec.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.Hash.fsti.checked Declassify.fsti.checked
Hashing.Spec.fst
Hashing.Spec.alg Hacl.Hash.Definitions.hash_len FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.op_GreaterThan FStar.UInt32.v Spec.Hash.Definitions.hash_length
﻿(** hash algorithms and providers

 * provides bytes-friendly API before idealization
 * no dependency on TLS: could go to EverCrypt or SecureAPI.

*)
module Hashing.Spec

include EverCrypt.Hash
include Spec.Hash.Definitions

open FStar.Bytes

open Declassify

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 10"

let alg = a:alg { is_md a }

let hash_len (a:alg)
val hash_len (a: alg) : n: UInt32.t{UInt32.v n == hash_length a}
a: Hashing.Spec.alg -> n: FStar.UInt32.t{FStar.UInt32.v n == Spec.Hash.Definitions.hash_length a}