Constant EverCrypt_DRBG_SHA2_512_s 

pub const EverCrypt_DRBG_SHA2_512_s: u32 = 3;