Constant EverCrypt_Hash_MD5_s 

pub const EverCrypt_Hash_MD5_s: u32 = 0;