val alg : Type0
let alg = a:alg { is_md a }
﻿(** hash algorithms and providers

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

*)
module MiTLS.Hashing.Spec
open MiTLS

include EverCrypt.Hash
include Spec.Hash.Definitions

open FStar.Bytes

open MiTLS.Declassify

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 10"
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.Declassify.fsti.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
MiTLS.Hashing.Spec.fst
Type0
EverCrypt.Hash.alg Prims.b2t Spec.Hash.Definitions.is_md
let alg =
  
a: alg{is_md a}