Constant EverCrypt_Hash_Blake2B_s 

pub const EverCrypt_Hash_Blake2B_s: u32 = 7;