Constant EverCrypt_DRBG_SHA1_s 

pub const EverCrypt_DRBG_SHA1_s: u32 = 0;