Constant EverCrypt_Error_DecodeError 

pub const EverCrypt_Error_DecodeError: u32 = 5;