Type Alias EverCrypt_Hash_broken_alg 

pub type EverCrypt_Hash_broken_alg = Spec_Hash_Definitions_hash_alg;